Doing: timeout --foreground --kill-after=5 --signal=SIGINT 61 time metta /opt/logicmoo_workspace/packs_sys/logicmoo_opencog/MeTTa/hyperon-wam/reports/performance/comparisons/nils_if_control_test_3.metta
[()]
[()]
[()]
[(: (((AS AS) (AS AK)) ((AK AK) (AS AS))) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) ((AK AK) (AS AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) ((AK AK) (AK AS))) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) ((AK AK) (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) ((AK AK) AS)) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) ((AK AK) AK)) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AS AK)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#14370 $a#14371) $b#14373)) (-> (: $y (-> (: $x#14370 $a#14371) (-> (: $y#14372 $b#14373) $c#14374))) (-> (: $x#14370 $a#14371) $c#14374)))) (-> (: $y (-> (: $x#14370 $a#14371) (-> (: $y#14372 $b#14373) $c#14374))) (-> (: $x (-> (: $x#14370 $a#14371) $b#14373)) (-> (: $x#14370 $a#14371) $c#14374))))), (: (((AS AS) (AS AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AS) (AS AK)) AK) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) ((AK AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#19659 $a#19660) $b#19662)) (-> (: $y (-> (: $x#19659 $a#19660) (-> (: $y#19661 $b#19662) $c#19663))) (-> (: $x#19659 $a#19660) $c#19663)))) (-> (: $y (-> (: $x#19659 $a#19660) (-> (: $y#19661 $b#19662) $c#19663))) (-> (: $x (-> (: $x#19659 $a#19660) $b#19662)) (-> (: $x#19659 $a#19660) $c#19663))))), (: (((AS AS) (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AS AS) (AK AS)) AK) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) ((AK AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AS) (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AS AS) (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#25444 $a#25445) $b#25447)) (-> (: $y (-> (: $x#25444 $a#25445) (-> (: $y#25446 $b#25447) $c#25448))) (-> (: $x#25444 $a#25445) $c#25448)))) (-> (: $y (-> (: $x#25444 $a#25445) (-> (: $y#25446 $b#25447) $c#25448))) (-> (: $x (-> (: $x#25444 $a#25445) $b#25447)) (-> (: $x#25444 $a#25445) $c#25448))))), (: (((AS AS) (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AS) (AK AK)) AK) (-> (: $f (-> (: $y $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $y $b) $c)))), (: (((AS AK) (AS AK)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AS AK)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AS AK)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AS AK)) ((AS AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AS AK)) ((AS AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AS AK)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#30805 $a#30806) (-> (: $y#30807 $b#30808) $c#30809))) (-> (: $y (-> (: $x (-> (: $x#30805 $a#30806) (-> (: $y#30807 $b#30808) $c#30809))) (-> (: $x#30805 $a#30806) $b#30808))) (-> (: $x#30805 $a#30806) $c#30809)))) (-> (: $y (-> (: $x (-> (: $x#30805 $a#30806) (-> (: $y#30807 $b#30808) $c#30809))) (-> (: $x#30805 $a#30806) $b#30808))) (-> (: $x (-> (: $x#30805 $a#30806) (-> (: $y#30807 $b#30808) $c#30809))) (-> (: $x#30805 $a#30806) $c#30809))))), (: (((AS AK) (AS AK)) (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#30623)) $c))) (-> (: $y (-> (: $x $c) $b#30623)) (-> (: $x $c) $c)))), (: (((AS AK) (AS AK)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#31130 $a#31131) (-> (: $y#31132 $b#31133) $c#31134))) (-> (: $y $b) (-> (: $f#31135 (-> (: $x#31130 $a#31131) $b#31133)) (-> (: $x#31130 $a#31131) $c#31134))))) (-> (: $y $b) (-> (: $x (-> (: $x#31130 $a#31131) (-> (: $y#31132 $b#31133) $c#31134))) (-> (: $f#31135 (-> (: $x#31130 $a#31131) $b#31133)) (-> (: $x#31130 $a#31131) $c#31134)))))), (: (((AS AK) (AS AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#31138 $b#31139) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#31138 $b#31139) $a))))), (: (((AS AK) (AS AK)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#31382 $a#31383) $b#31385)) (-> (: $y (-> (: $x#31382 $a#31383) (-> (: $y#31384 $b#31385) $c#31386))) (-> (: $x#31382 $a#31383) $c#31386)))) (-> (: $y (-> (: $x#31382 $a#31383) (-> (: $y#31384 $b#31385) $c#31386))) (-> (: $x (-> (: $x#31382 $a#31383) $b#31385)) (-> (: $x#31382 $a#31383) $c#31386))))), (: (((AS AK) (AS AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AK) (AK AS)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AS)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AS)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AS)) ((AS AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AS)) ((AS AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AS)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#34088 $a#34089) (-> (: $y#34090 $b#34091) $c#34092))) (-> (: $y (-> (: $x (-> (: $x#34088 $a#34089) (-> (: $y#34090 $b#34091) $c#34092))) (-> (: $x#34088 $a#34089) $b#34091))) (-> (: $x#34088 $a#34089) $c#34092)))) (-> (: $y (-> (: $x (-> (: $x#34088 $a#34089) (-> (: $y#34090 $b#34091) $c#34092))) (-> (: $x#34088 $a#34089) $b#34091))) (-> (: $x (-> (: $x#34088 $a#34089) (-> (: $y#34090 $b#34091) $c#34092))) (-> (: $x#34088 $a#34089) $c#34092))))), (: (((AS AK) (AK AS)) (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#34093)) $c))) (-> (: $y (-> (: $x $c) $b#34093)) (-> (: $x $c) $c)))), (: (((AS AK) (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#34094 $a#34095) (-> (: $y#34096 $b#34097) $c#34098))) (-> (: $y $b) (-> (: $f#34099 (-> (: $x#34094 $a#34095) $b#34097)) (-> (: $x#34094 $a#34095) $c#34098))))) (-> (: $y $b) (-> (: $x (-> (: $x#34094 $a#34095) (-> (: $y#34096 $b#34097) $c#34098))) (-> (: $f#34099 (-> (: $x#34094 $a#34095) $b#34097)) (-> (: $x#34094 $a#34095) $c#34098)))))), (: (((AS AK) (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#34100 $b#34101) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#34100 $b#34101) $a))))), (: (((AS AK) (AK AS)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#34102 $a#34103) $b#34104)) (-> (: $y (-> (: $x#34102 $a#34103) (-> (: $y#34105 $b#34104) $c#34106))) (-> (: $x#34102 $a#34103) $c#34106)))) (-> (: $y (-> (: $x#34102 $a#34103) (-> (: $y#34105 $b#34104) $c#34106))) (-> (: $x (-> (: $x#34102 $a#34103) $b#34104)) (-> (: $x#34102 $a#34103) $c#34106))))), (: (((AS AK) (AK AS)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AK) (AK AK)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AK)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AK)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AK)) ((AS AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AK)) ((AS AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) (AK AK)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#36128 $a#36129) (-> (: $y#36130 $b#36131) $c#36132))) (-> (: $y (-> (: $x (-> (: $x#36128 $a#36129) (-> (: $y#36130 $b#36131) $c#36132))) (-> (: $x#36128 $a#36129) $b#36131))) (-> (: $x#36128 $a#36129) $c#36132)))) (-> (: $y (-> (: $x (-> (: $x#36128 $a#36129) (-> (: $y#36130 $b#36131) $c#36132))) (-> (: $x#36128 $a#36129) $b#36131))) (-> (: $x (-> (: $x#36128 $a#36129) (-> (: $y#36130 $b#36131) $c#36132))) (-> (: $x#36128 $a#36129) $c#36132))))), (: (((AS AK) (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#36133)) $c))) (-> (: $y (-> (: $x $c) $b#36133)) (-> (: $x $c) $c)))), (: (((AS AK) (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#36134 $a#36135) (-> (: $y#36136 $b#36137) $c#36138))) (-> (: $y $b) (-> (: $f#36139 (-> (: $x#36134 $a#36135) $b#36137)) (-> (: $x#36134 $a#36135) $c#36138))))) (-> (: $y $b) (-> (: $x (-> (: $x#36134 $a#36135) (-> (: $y#36136 $b#36137) $c#36138))) (-> (: $f#36139 (-> (: $x#36134 $a#36135) $b#36137)) (-> (: $x#36134 $a#36135) $c#36138)))))), (: (((AS AK) (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#36140 $b#36141) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#36140 $b#36141) $a))))), (: (((AS AK) (AK AK)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#36142 $a#36143) $b#36144)) (-> (: $y (-> (: $x#36142 $a#36143) (-> (: $y#36145 $b#36144) $c#36146))) (-> (: $x#36142 $a#36143) $c#36146)))) (-> (: $y (-> (: $x#36142 $a#36143) (-> (: $y#36145 $b#36144) $c#36146))) (-> (: $x (-> (: $x#36142 $a#36143) $b#36144)) (-> (: $x#36142 $a#36143) $c#36146))))), (: (((AS AK) (AK AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AK) AS) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AS) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AS) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AS) ((AS AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AS) ((AS AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AS) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#38167 $a#38168) (-> (: $y#38169 $b#38170) $c#38171))) (-> (: $y (-> (: $x (-> (: $x#38167 $a#38168) (-> (: $y#38169 $b#38170) $c#38171))) (-> (: $x#38167 $a#38168) $b#38170))) (-> (: $x#38167 $a#38168) $c#38171)))) (-> (: $y (-> (: $x (-> (: $x#38167 $a#38168) (-> (: $y#38169 $b#38170) $c#38171))) (-> (: $x#38167 $a#38168) $b#38170))) (-> (: $x (-> (: $x#38167 $a#38168) (-> (: $y#38169 $b#38170) $c#38171))) (-> (: $x#38167 $a#38168) $c#38171))))), (: (((AS AK) AS) (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#38172)) $c))) (-> (: $y (-> (: $x $c) $b#38172)) (-> (: $x $c) $c)))), (: (((AS AK) AS) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#38173 $a#38174) (-> (: $y#38175 $b#38176) $c#38177))) (-> (: $y $b) (-> (: $f#38178 (-> (: $x#38173 $a#38174) $b#38176)) (-> (: $x#38173 $a#38174) $c#38177))))) (-> (: $y $b) (-> (: $x (-> (: $x#38173 $a#38174) (-> (: $y#38175 $b#38176) $c#38177))) (-> (: $f#38178 (-> (: $x#38173 $a#38174) $b#38176)) (-> (: $x#38173 $a#38174) $c#38177)))))), (: (((AS AK) AS) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#38179 $b#38180) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#38179 $b#38180) $a))))), (: (((AS AK) AS) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#38181 $a#38182) $b#38183)) (-> (: $y (-> (: $x#38181 $a#38182) (-> (: $y#38184 $b#38183) $c#38185))) (-> (: $x#38181 $a#38182) $c#38185)))) (-> (: $y (-> (: $x#38181 $a#38182) (-> (: $y#38184 $b#38183) $c#38185))) (-> (: $x (-> (: $x#38181 $a#38182) $b#38183)) (-> (: $x#38181 $a#38182) $c#38185))))), (: (((AS AK) AS) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AS AK) AK) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AK) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AK) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AK) ((AS AK) AS)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AK) ((AS AK) AK)) (-> (: $f (-> (: $x $b) (-> (: $x $b) $c))) (-> (: $x $b) (-> (: $x $b) $c)))), (: (((AS AK) AK) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#39986 $a#39987) (-> (: $y#39988 $b#39989) $c#39990))) (-> (: $y (-> (: $x (-> (: $x#39986 $a#39987) (-> (: $y#39988 $b#39989) $c#39990))) (-> (: $x#39986 $a#39987) $b#39989))) (-> (: $x#39986 $a#39987) $c#39990)))) (-> (: $y (-> (: $x (-> (: $x#39986 $a#39987) (-> (: $y#39988 $b#39989) $c#39990))) (-> (: $x#39986 $a#39987) $b#39989))) (-> (: $x (-> (: $x#39986 $a#39987) (-> (: $y#39988 $b#39989) $c#39990))) (-> (: $x#39986 $a#39987) $c#39990))))), (: (((AS AK) AK) (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#39991)) $c))) (-> (: $y (-> (: $x $c) $b#39991)) (-> (: $x $c) $c)))), (: (((AS AK) AK) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#39992 $a#39993) (-> (: $y#39994 $b#39995) $c#39996))) (-> (: $y $b) (-> (: $f#39997 (-> (: $x#39992 $a#39993) $b#39995)) (-> (: $x#39992 $a#39993) $c#39996))))) (-> (: $y $b) (-> (: $x (-> (: $x#39992 $a#39993) (-> (: $y#39994 $b#39995) $c#39996))) (-> (: $f#39997 (-> (: $x#39992 $a#39993) $b#39995)) (-> (: $x#39992 $a#39993) $c#39996)))))), (: (((AS AK) AK) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#39998 $b#39999) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#39998 $b#39999) $a))))), (: (((AS AK) AK) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#40000 $a#40001) $b#40002)) (-> (: $y (-> (: $x#40000 $a#40001) (-> (: $y#40003 $b#40002) $c#40004))) (-> (: $x#40000 $a#40001) $c#40004)))) (-> (: $y (-> (: $x#40000 $a#40001) (-> (: $y#40003 $b#40002) $c#40004))) (-> (: $x (-> (: $x#40000 $a#40001) $b#40002)) (-> (: $x#40000 $a#40001) $c#40004))))), (: (((AS AK) AK) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (((AK AS) (AS AS)) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#42776 $a#42777) (-> (: $y#42778 $c#42780) $c#42780))) (-> (: $y (-> (: $x#42776 $a#42777) (-> (: $y#42778 $c#42780) $c#42780))) (-> (: $x#42776 $a#42777) $c#42780)))) (-> (: $y (-> (: $x#42776 $a#42777) (-> (: $y#42778 $c#42780) $c#42780))) (-> (: $y (-> (: $x#42776 $a#42777) (-> (: $y#42778 $c#42780) $c#42780))) (-> (: $x#42776 $a#42777) $c#42780))))), (: (((AK AS) (AS AS)) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) (AS AS)) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#43083 $a#43084) (-> (: $y#43085 $b#43086) $c#43087))) (-> (: $y (-> (: $x#43083 $a#43084) (-> (: $y#43085 $b#43086) $c#43087))) (-> (: $f#43088 (-> (: $x#43083 $a#43084) $b#43086)) (-> (: $x#43083 $a#43084) $c#43087))))) (-> (: $y (-> (: $x#43083 $a#43084) (-> (: $y#43085 $b#43086) $c#43087))) (-> (: $y (-> (: $x#43083 $a#43084) (-> (: $y#43085 $b#43086) $c#43087))) (-> (: $f#43088 (-> (: $x#43083 $a#43084) $b#43086)) (-> (: $x#43083 $a#43084) $c#43087)))))), (: (((AK AS) (AS AS)) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#43091 $b#43092) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#43091 $b#43092) $b))))), (: (((AK AS) (AS AK)) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#44666 $a#44667) (-> (: $y#44668 $c#44669) $c#44669))) (-> (: $y (-> (: $x#44666 $a#44667) (-> (: $y#44668 $c#44669) $c#44669))) (-> (: $x#44666 $a#44667) $c#44669)))) (-> (: $y (-> (: $x#44666 $a#44667) (-> (: $y#44668 $c#44669) $c#44669))) (-> (: $y (-> (: $x#44666 $a#44667) (-> (: $y#44668 $c#44669) $c#44669))) (-> (: $x#44666 $a#44667) $c#44669))))), (: (((AK AS) (AS AK)) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) (AS AK)) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#44672 $a#44673) (-> (: $y#44674 $b#44675) $c#44676))) (-> (: $y (-> (: $x#44672 $a#44673) (-> (: $y#44674 $b#44675) $c#44676))) (-> (: $f#44677 (-> (: $x#44672 $a#44673) $b#44675)) (-> (: $x#44672 $a#44673) $c#44676))))) (-> (: $y (-> (: $x#44672 $a#44673) (-> (: $y#44674 $b#44675) $c#44676))) (-> (: $y (-> (: $x#44672 $a#44673) (-> (: $y#44674 $b#44675) $c#44676))) (-> (: $f#44677 (-> (: $x#44672 $a#44673) $b#44675)) (-> (: $x#44672 $a#44673) $c#44676)))))), (: (((AK AS) (AS AK)) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#44678 $b#44679) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#44678 $b#44679) $b))))), (: (((AK AS) (AK AS)) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#45559 $a#45560) (-> (: $y#45561 $c#45562) $c#45562))) (-> (: $y (-> (: $x#45559 $a#45560) (-> (: $y#45561 $c#45562) $c#45562))) (-> (: $x#45559 $a#45560) $c#45562)))) (-> (: $y (-> (: $x#45559 $a#45560) (-> (: $y#45561 $c#45562) $c#45562))) (-> (: $y (-> (: $x#45559 $a#45560) (-> (: $y#45561 $c#45562) $c#45562))) (-> (: $x#45559 $a#45560) $c#45562))))), (: (((AK AS) (AK AS)) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#45565 $a#45566) (-> (: $y#45567 $b#45568) $c#45569))) (-> (: $y (-> (: $x#45565 $a#45566) (-> (: $y#45567 $b#45568) $c#45569))) (-> (: $f#45570 (-> (: $x#45565 $a#45566) $b#45568)) (-> (: $x#45565 $a#45566) $c#45569))))) (-> (: $y (-> (: $x#45565 $a#45566) (-> (: $y#45567 $b#45568) $c#45569))) (-> (: $y (-> (: $x#45565 $a#45566) (-> (: $y#45567 $b#45568) $c#45569))) (-> (: $f#45570 (-> (: $x#45565 $a#45566) $b#45568)) (-> (: $x#45565 $a#45566) $c#45569)))))), (: (((AK AS) (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#45571 $b#45572) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#45571 $b#45572) $b))))), (: (((AK AS) (AK AK)) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#46452 $a#46453) (-> (: $y#46454 $c#46455) $c#46455))) (-> (: $y (-> (: $x#46452 $a#46453) (-> (: $y#46454 $c#46455) $c#46455))) (-> (: $x#46452 $a#46453) $c#46455)))) (-> (: $y (-> (: $x#46452 $a#46453) (-> (: $y#46454 $c#46455) $c#46455))) (-> (: $y (-> (: $x#46452 $a#46453) (-> (: $y#46454 $c#46455) $c#46455))) (-> (: $x#46452 $a#46453) $c#46455))))), (: (((AK AS) (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#46458 $a#46459) (-> (: $y#46460 $b#46461) $c#46462))) (-> (: $y (-> (: $x#46458 $a#46459) (-> (: $y#46460 $b#46461) $c#46462))) (-> (: $f#46463 (-> (: $x#46458 $a#46459) $b#46461)) (-> (: $x#46458 $a#46459) $c#46462))))) (-> (: $y (-> (: $x#46458 $a#46459) (-> (: $y#46460 $b#46461) $c#46462))) (-> (: $y (-> (: $x#46458 $a#46459) (-> (: $y#46460 $b#46461) $c#46462))) (-> (: $f#46463 (-> (: $x#46458 $a#46459) $b#46461)) (-> (: $x#46458 $a#46459) $c#46462)))))), (: (((AK AS) (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#46464 $b#46465) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#46464 $b#46465) $b))))), (: (((AK AS) AS) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#47344 $a#47345) (-> (: $y#47346 $c#47347) $c#47347))) (-> (: $y (-> (: $x#47344 $a#47345) (-> (: $y#47346 $c#47347) $c#47347))) (-> (: $x#47344 $a#47345) $c#47347)))) (-> (: $y (-> (: $x#47344 $a#47345) (-> (: $y#47346 $c#47347) $c#47347))) (-> (: $y (-> (: $x#47344 $a#47345) (-> (: $y#47346 $c#47347) $c#47347))) (-> (: $x#47344 $a#47345) $c#47347))))), (: (((AK AS) AS) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) AS) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#47350 $a#47351) (-> (: $y#47352 $b#47353) $c#47354))) (-> (: $y (-> (: $x#47350 $a#47351) (-> (: $y#47352 $b#47353) $c#47354))) (-> (: $f#47355 (-> (: $x#47350 $a#47351) $b#47353)) (-> (: $x#47350 $a#47351) $c#47354))))) (-> (: $y (-> (: $x#47350 $a#47351) (-> (: $y#47352 $b#47353) $c#47354))) (-> (: $y (-> (: $x#47350 $a#47351) (-> (: $y#47352 $b#47353) $c#47354))) (-> (: $f#47355 (-> (: $x#47350 $a#47351) $b#47353)) (-> (: $x#47350 $a#47351) $c#47354)))))), (: (((AK AS) AS) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#47356 $b#47357) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#47356 $b#47357) $b))))), (: (((AK AS) AK) (AK (AS AS))) (-> (: $f (-> (: $y (-> (: $x#48156 $a#48157) (-> (: $y#48158 $c#48159) $c#48159))) (-> (: $y (-> (: $x#48156 $a#48157) (-> (: $y#48158 $c#48159) $c#48159))) (-> (: $x#48156 $a#48157) $c#48159)))) (-> (: $y (-> (: $x#48156 $a#48157) (-> (: $y#48158 $c#48159) $c#48159))) (-> (: $y (-> (: $x#48156 $a#48157) (-> (: $y#48158 $c#48159) $c#48159))) (-> (: $x#48156 $a#48157) $c#48159))))), (: (((AK AS) AK) (AK (AS AK))) (-> (: $f (-> (: $y $c) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $y $c) $c)))), (: (((AK AS) AK) (AK (AK AS))) (-> (: $f (-> (: $y (-> (: $x#48162 $a#48163) (-> (: $y#48164 $b#48165) $c#48166))) (-> (: $y (-> (: $x#48162 $a#48163) (-> (: $y#48164 $b#48165) $c#48166))) (-> (: $f#48167 (-> (: $x#48162 $a#48163) $b#48165)) (-> (: $x#48162 $a#48163) $c#48166))))) (-> (: $y (-> (: $x#48162 $a#48163) (-> (: $y#48164 $b#48165) $c#48166))) (-> (: $y (-> (: $x#48162 $a#48163) (-> (: $y#48164 $b#48165) $c#48166))) (-> (: $f#48167 (-> (: $x#48162 $a#48163) $b#48165)) (-> (: $x#48162 $a#48163) $c#48166)))))), (: (((AK AS) AK) (AK (AK AK))) (-> (: $f (-> (: $y $b) (-> (: $y $b) (-> (: $y#48168 $b#48169) $b)))) (-> (: $y $b) (-> (: $y $b) (-> (: $y#48168 $b#48169) $b))))), (: (((AK AK) (AS AS)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#49323 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#49323 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#50595 $a#50596) (-> (: $y#50597 $b#50598) $c#50599))) (-> (: $y (-> (: $x (-> (: $x#50595 $a#50596) (-> (: $y#50597 $b#50598) $c#50599))) (-> (: $y#49323 (-> (: $f#50600 (-> (: $x#50595 $a#50596) $b#50598)) (-> (: $x#50595 $a#50596) $c#50599))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#50595 $a#50596) (-> (: $y#50597 $b#50598) $c#50599))) (-> (: $y#49323 (-> (: $f#50600 (-> (: $x#50595 $a#50596) $b#50598)) (-> (: $x#50595 $a#50596) $c#50599))) $c))) (-> (: $x (-> (: $x#50595 $a#50596) (-> (: $y#50597 $b#50598) $c#50599))) $c)))), (: (((AK AK) (AS AS)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#49323 (-> (: $y#50603 $b#50604) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#49323 (-> (: $y#50603 $b#50604) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#51532 $a#51533) (-> (: $y#51534 $b#51535) $c#51536))) (-> (: $y (-> (: $x (-> (: $x#51532 $a#51533) (-> (: $y#51534 $b#51535) $c#51536))) (-> (: $x#51532 $a#51533) $b#51535))) (-> (: $x#51532 $a#51533) $b#51535)))) (-> (: $y (-> (: $x (-> (: $x#51532 $a#51533) (-> (: $y#51534 $b#51535) $c#51536))) (-> (: $x#51532 $a#51533) $b#51535))) (-> (: $x (-> (: $x#51532 $a#51533) (-> (: $y#51534 $b#51535) $c#51536))) (-> (: $x#51532 $a#51533) $b#51535))))), (: (((AK AK) (AS AS)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#51362) (-> (: $y (-> (: $x $c#51362) $c)) $c))) (-> (: $y (-> (: $x $c#51362) $c)) (-> (: $x $c#51362) $c)))), (: (((AK AK) (AS AS)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#52118 $b#52119) $c#52120))) (-> (: $y#52118 $b#52119) $c#52120)))) (-> (: $y (-> (: $x $a) (-> (: $y#52118 $b#52119) $c#52120))) (-> (: $x $a) (-> (: $y#52118 $b#52119) $c#52120))))), (: (((AK AK) (AS AS)) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x#49688 $a#49689) $c#49692)))) (-> (: $y (-> (: $x#49688 $a#49689) (-> (: $y#49690 $b#49691) $c#49692))) (-> (: $x (-> (: $x#49688 $a#49689) $b#49691)) (-> (: $x#49688 $a#49689) $c#49692))))), (: (((AK AK) (AS AS)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AS)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#49934 (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736))) (-> (: $x#54732 $a#54733) $b#54735))) (-> (: $y (-> (: $x (-> (: $y#49934 (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736))) (-> (: $x#54732 $a#54733) $b#54735))) (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736)))) (-> (: $x#54732 $a#54733) $c#54736)))) (-> (: $y (-> (: $x (-> (: $y#49934 (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736))) (-> (: $x#54732 $a#54733) $b#54735))) (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736)))) (-> (: $x (-> (: $y#49934 (-> (: $x#54732 $a#54733) (-> (: $y#54734 $b#54735) $c#54736))) (-> (: $x#54732 $a#54733) $b#54735))) (-> (: $x#54732 $a#54733) $c#54736))))), (: (((AK AK) (AS AS)) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#49934 $c) $b#54550)) (-> (: $y (-> (: $x (-> (: $y#49934 $c) $b#54550)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#49934 $c) $b#54550)) $c)) (-> (: $x (-> (: $y#49934 $c) $b#54550)) $c)))), (: (((AK AK) (AS AS)) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#55057 $a#55058) (-> (: $y#55059 $b#55060) $c#55061)))) (-> (: $f#55062 (-> (: $x#55057 $a#55058) $b#55060)) (-> (: $x#55057 $a#55058) $c#55061))))) (-> (: $y (-> (: $x $a) (-> (: $x#55057 $a#55058) (-> (: $y#55059 $b#55060) $c#55061)))) (-> (: $x $a) (-> (: $f#55062 (-> (: $x#55057 $a#55058) $b#55060)) (-> (: $x#55057 $a#55058) $c#55061)))))), (: (((AK AK) (AS AS)) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#49935)) (-> (: $y#55065 $b#55066) $b#49935)))) (-> (: $y (-> (: $x $a) $b#49935)) (-> (: $x $a) (-> (: $y#55065 $b#55066) $b#49935))))), (: (((AK AK) (AS AS)) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#55309 $a#55310) (-> (: $y#55311 $b#55312) $c#55313))) (-> (: $y (-> (: $x (-> (: $x#55309 $a#55310) (-> (: $y#55311 $b#55312) $c#55313))) (-> (: $x#55309 $a#55310) $b#55312))) (-> (: $x#55309 $a#55310) $c#55313)))) (-> (: $y (-> (: $x (-> (: $x#55309 $a#55310) (-> (: $y#55311 $b#55312) $c#55313))) (-> (: $x#55309 $a#55310) $b#55312))) (-> (: $x (-> (: $x#55309 $a#55310) (-> (: $y#55311 $b#55312) $c#55313))) (-> (: $x#55309 $a#55310) $c#55313))))), (: (((AK AK) (AS AS)) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#49935)) $a))) (-> (: $y (-> (: $x $a) $b#49935)) (-> (: $x $a) $a)))), (: (((AK AK) (AS AS)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#56068 (-> (: $x#56241 $a#56242) (-> (: $y#56243 $b#56244) $c#56245))) (-> (: $x#56241 $a#56242) $b#56244))) (-> (: $y $b) (-> (: $x#56068 (-> (: $x#56241 $a#56242) (-> (: $y#56243 $b#56244) $c#56245))) (-> (: $x#56241 $a#56242) $c#56245))))) (-> (: $y $b) (-> (: $x (-> (: $x#56068 (-> (: $x#56241 $a#56242) (-> (: $y#56243 $b#56244) $c#56245))) (-> (: $x#56241 $a#56242) $b#56244))) (-> (: $x#56068 (-> (: $x#56241 $a#56242) (-> (: $y#56243 $b#56244) $c#56245))) (-> (: $x#56241 $a#56242) $c#56245)))))), (: (((AK AK) (AS AS)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#56068 $a#56069) $b#56071)) (-> (: $y $b) (-> (: $x#56068 $a#56069) $a#56069)))) (-> (: $y $b) (-> (: $x (-> (: $x#56068 $a#56069) $b#56071)) (-> (: $x#56068 $a#56069) $a#56069))))), (: (((AK AK) (AS AS)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#56549 (-> (: $x#56550 $a#56551) (-> (: $y#56552 $b#56553) $c#56554))) (-> (: $f#56555 (-> (: $x#56550 $a#56551) $b#56553)) (-> (: $x#56550 $a#56551) $c#56554)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#56549 (-> (: $x#56550 $a#56551) (-> (: $y#56552 $b#56553) $c#56554))) (-> (: $f#56555 (-> (: $x#56550 $a#56551) $b#56553)) (-> (: $x#56550 $a#56551) $c#56554))))))), (: (((AK AK) (AS AS)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#56556 $a#56557) (-> (: $y#56558 $b#56559) $a#56557))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#56556 $a#56557) (-> (: $y#56558 $b#56559) $a#56557)))))), (: (((AK AK) (AS AS)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#56801 $a#56802) (-> (: $y#56803 $b#56804) $c#56805))) (-> (: $y $b) (-> (: $f#56806 (-> (: $x#56801 $a#56802) $b#56804)) (-> (: $x#56801 $a#56802) $c#56805))))) (-> (: $y $b) (-> (: $x (-> (: $x#56801 $a#56802) (-> (: $y#56803 $b#56804) $c#56805))) (-> (: $f#56806 (-> (: $x#56801 $a#56802) $b#56804)) (-> (: $x#56801 $a#56802) $c#56805)))))), (: (((AK AK) (AS AS)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#56809 $b#56810) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#56809 $b#56810) $a))))), (: (((AK AK) (AS AS)) AS) (-> (: $f (-> (: $x (-> (: $x#57361 $a#57362) $b#57364)) (-> (: $y (-> (: $x#57361 $a#57362) (-> (: $y#57363 $b#57364) $c#57365))) (-> (: $x#57361 $a#57362) $c#57365)))) (-> (: $y (-> (: $x#57361 $a#57362) (-> (: $y#57363 $b#57364) $c#57365))) (-> (: $x (-> (: $x#57361 $a#57362) $b#57364)) (-> (: $x#57361 $a#57362) $c#57365))))), (: (((AK AK) (AS AS)) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#64305 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#64305 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#64308 $a#64309) (-> (: $y#64310 $b#64311) $c#64312))) (-> (: $y (-> (: $x (-> (: $x#64308 $a#64309) (-> (: $y#64310 $b#64311) $c#64312))) (-> (: $y#64305 (-> (: $f#64313 (-> (: $x#64308 $a#64309) $b#64311)) (-> (: $x#64308 $a#64309) $c#64312))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#64308 $a#64309) (-> (: $y#64310 $b#64311) $c#64312))) (-> (: $y#64305 (-> (: $f#64313 (-> (: $x#64308 $a#64309) $b#64311)) (-> (: $x#64308 $a#64309) $c#64312))) $c))) (-> (: $x (-> (: $x#64308 $a#64309) (-> (: $y#64310 $b#64311) $c#64312))) $c)))), (: (((AK AK) (AS AK)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#64305 (-> (: $y#64314 $b#64315) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#64305 (-> (: $y#64314 $b#64315) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#64316 $a#64317) (-> (: $y#64318 $b#64319) $c#64320))) (-> (: $y (-> (: $x (-> (: $x#64316 $a#64317) (-> (: $y#64318 $b#64319) $c#64320))) (-> (: $x#64316 $a#64317) $b#64319))) (-> (: $x#64316 $a#64317) $b#64319)))) (-> (: $y (-> (: $x (-> (: $x#64316 $a#64317) (-> (: $y#64318 $b#64319) $c#64320))) (-> (: $x#64316 $a#64317) $b#64319))) (-> (: $x (-> (: $x#64316 $a#64317) (-> (: $y#64318 $b#64319) $c#64320))) (-> (: $x#64316 $a#64317) $b#64319))))), (: (((AK AK) (AS AK)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#64321) (-> (: $y (-> (: $x $c#64321) $c)) $c))) (-> (: $y (-> (: $x $c#64321) $c)) (-> (: $x $c#64321) $c)))), (: (((AK AK) (AS AK)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#64322 $b#64323) $c#64324))) (-> (: $y#64322 $b#64323) $c#64324)))) (-> (: $y (-> (: $x $a) (-> (: $y#64322 $b#64323) $c#64324))) (-> (: $x $a) (-> (: $y#64322 $b#64323) $c#64324))))), (: (((AK AK) (AS AK)) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x#64325 $a#64326) $c#64329)))) (-> (: $y (-> (: $x#64325 $a#64326) (-> (: $y#64327 $b#64328) $c#64329))) (-> (: $x (-> (: $x#64325 $a#64326) $b#64328)) (-> (: $x#64325 $a#64326) $c#64329))))), (: (((AK AK) (AS AK)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AS AK)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#64330 (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335))) (-> (: $x#64331 $a#64332) $b#64334))) (-> (: $y (-> (: $x (-> (: $y#64330 (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335))) (-> (: $x#64331 $a#64332) $b#64334))) (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335)))) (-> (: $x#64331 $a#64332) $c#64335)))) (-> (: $y (-> (: $x (-> (: $y#64330 (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335))) (-> (: $x#64331 $a#64332) $b#64334))) (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335)))) (-> (: $x (-> (: $y#64330 (-> (: $x#64331 $a#64332) (-> (: $y#64333 $b#64334) $c#64335))) (-> (: $x#64331 $a#64332) $b#64334))) (-> (: $x#64331 $a#64332) $c#64335))))), (: (((AK AK) (AS AK)) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#64330 $c) $b#64336)) (-> (: $y (-> (: $x (-> (: $y#64330 $c) $b#64336)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#64330 $c) $b#64336)) $c)) (-> (: $x (-> (: $y#64330 $c) $b#64336)) $c)))), (: (((AK AK) (AS AK)) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#64337 $a#64338) (-> (: $y#64339 $b#64340) $c#64341)))) (-> (: $f#64342 (-> (: $x#64337 $a#64338) $b#64340)) (-> (: $x#64337 $a#64338) $c#64341))))) (-> (: $y (-> (: $x $a) (-> (: $x#64337 $a#64338) (-> (: $y#64339 $b#64340) $c#64341)))) (-> (: $x $a) (-> (: $f#64342 (-> (: $x#64337 $a#64338) $b#64340)) (-> (: $x#64337 $a#64338) $c#64341)))))), (: (((AK AK) (AS AK)) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#64343)) (-> (: $y#64344 $b#64345) $b#64343)))) (-> (: $y (-> (: $x $a) $b#64343)) (-> (: $x $a) (-> (: $y#64344 $b#64345) $b#64343))))), (: (((AK AK) (AS AK)) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#64346 $a#64347) (-> (: $y#64348 $b#64349) $c#64350))) (-> (: $y (-> (: $x (-> (: $x#64346 $a#64347) (-> (: $y#64348 $b#64349) $c#64350))) (-> (: $x#64346 $a#64347) $b#64349))) (-> (: $x#64346 $a#64347) $c#64350)))) (-> (: $y (-> (: $x (-> (: $x#64346 $a#64347) (-> (: $y#64348 $b#64349) $c#64350))) (-> (: $x#64346 $a#64347) $b#64349))) (-> (: $x (-> (: $x#64346 $a#64347) (-> (: $y#64348 $b#64349) $c#64350))) (-> (: $x#64346 $a#64347) $c#64350))))), (: (((AK AK) (AS AK)) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#64343)) $a))) (-> (: $y (-> (: $x $a) $b#64343)) (-> (: $x $a) $a)))), (: (((AK AK) (AS AK)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#64351 (-> (: $x#64352 $a#64353) (-> (: $y#64354 $b#64355) $c#64356))) (-> (: $x#64352 $a#64353) $b#64355))) (-> (: $y $b) (-> (: $x#64351 (-> (: $x#64352 $a#64353) (-> (: $y#64354 $b#64355) $c#64356))) (-> (: $x#64352 $a#64353) $c#64356))))) (-> (: $y $b) (-> (: $x (-> (: $x#64351 (-> (: $x#64352 $a#64353) (-> (: $y#64354 $b#64355) $c#64356))) (-> (: $x#64352 $a#64353) $b#64355))) (-> (: $x#64351 (-> (: $x#64352 $a#64353) (-> (: $y#64354 $b#64355) $c#64356))) (-> (: $x#64352 $a#64353) $c#64356)))))), (: (((AK AK) (AS AK)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#64351 $a#64357) $b#64358)) (-> (: $y $b) (-> (: $x#64351 $a#64357) $a#64357)))) (-> (: $y $b) (-> (: $x (-> (: $x#64351 $a#64357) $b#64358)) (-> (: $x#64351 $a#64357) $a#64357))))), (: (((AK AK) (AS AK)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#64359 (-> (: $x#64360 $a#64361) (-> (: $y#64362 $b#64363) $c#64364))) (-> (: $f#64365 (-> (: $x#64360 $a#64361) $b#64363)) (-> (: $x#64360 $a#64361) $c#64364)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#64359 (-> (: $x#64360 $a#64361) (-> (: $y#64362 $b#64363) $c#64364))) (-> (: $f#64365 (-> (: $x#64360 $a#64361) $b#64363)) (-> (: $x#64360 $a#64361) $c#64364))))))), (: (((AK AK) (AS AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#64366 $a#64367) (-> (: $y#64368 $b#64369) $a#64367))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#64366 $a#64367) (-> (: $y#64368 $b#64369) $a#64367)))))), (: (((AK AK) (AS AK)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#64370 $a#64371) (-> (: $y#64372 $b#64373) $c#64374))) (-> (: $y $b) (-> (: $f#64375 (-> (: $x#64370 $a#64371) $b#64373)) (-> (: $x#64370 $a#64371) $c#64374))))) (-> (: $y $b) (-> (: $x (-> (: $x#64370 $a#64371) (-> (: $y#64372 $b#64373) $c#64374))) (-> (: $f#64375 (-> (: $x#64370 $a#64371) $b#64373)) (-> (: $x#64370 $a#64371) $c#64374)))))), (: (((AK AK) (AS AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#64376 $b#64377) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#64376 $b#64377) $a))))), (: (((AK AK) (AS AK)) AS) (-> (: $f (-> (: $x (-> (: $x#64378 $a#64379) $b#64381)) (-> (: $y (-> (: $x#64378 $a#64379) (-> (: $y#64380 $b#64381) $c#64382))) (-> (: $x#64378 $a#64379) $c#64382)))) (-> (: $y (-> (: $x#64378 $a#64379) (-> (: $y#64380 $b#64381) $c#64382))) (-> (: $x (-> (: $x#64378 $a#64379) $b#64381)) (-> (: $x#64378 $a#64379) $c#64382))))), (: (((AK AK) (AS AK)) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#71659 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#71659 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#71662 $a#71663) (-> (: $y#71664 $b#71665) $c#71666))) (-> (: $y (-> (: $x (-> (: $x#71662 $a#71663) (-> (: $y#71664 $b#71665) $c#71666))) (-> (: $y#71659 (-> (: $f#71667 (-> (: $x#71662 $a#71663) $b#71665)) (-> (: $x#71662 $a#71663) $c#71666))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#71662 $a#71663) (-> (: $y#71664 $b#71665) $c#71666))) (-> (: $y#71659 (-> (: $f#71667 (-> (: $x#71662 $a#71663) $b#71665)) (-> (: $x#71662 $a#71663) $c#71666))) $c))) (-> (: $x (-> (: $x#71662 $a#71663) (-> (: $y#71664 $b#71665) $c#71666))) $c)))), (: (((AK AK) (AK AS)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#71659 (-> (: $y#71668 $b#71669) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#71659 (-> (: $y#71668 $b#71669) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#71670 $a#71671) (-> (: $y#71672 $b#71673) $c#71674))) (-> (: $y (-> (: $x (-> (: $x#71670 $a#71671) (-> (: $y#71672 $b#71673) $c#71674))) (-> (: $x#71670 $a#71671) $b#71673))) (-> (: $x#71670 $a#71671) $b#71673)))) (-> (: $y (-> (: $x (-> (: $x#71670 $a#71671) (-> (: $y#71672 $b#71673) $c#71674))) (-> (: $x#71670 $a#71671) $b#71673))) (-> (: $x (-> (: $x#71670 $a#71671) (-> (: $y#71672 $b#71673) $c#71674))) (-> (: $x#71670 $a#71671) $b#71673))))), (: (((AK AK) (AK AS)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#71675) (-> (: $y (-> (: $x $c#71675) $c)) $c))) (-> (: $y (-> (: $x $c#71675) $c)) (-> (: $x $c#71675) $c)))), (: (((AK AK) (AK AS)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#71676 $b#71677) $c#71678))) (-> (: $y#71676 $b#71677) $c#71678)))) (-> (: $y (-> (: $x $a) (-> (: $y#71676 $b#71677) $c#71678))) (-> (: $x $a) (-> (: $y#71676 $b#71677) $c#71678))))), (: (((AK AK) (AK AS)) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x#71679 $a#71680) $c#71683)))) (-> (: $y (-> (: $x#71679 $a#71680) (-> (: $y#71681 $b#71682) $c#71683))) (-> (: $x (-> (: $x#71679 $a#71680) $b#71682)) (-> (: $x#71679 $a#71680) $c#71683))))), (: (((AK AK) (AK AS)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AS)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#71684 (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689))) (-> (: $x#71685 $a#71686) $b#71688))) (-> (: $y (-> (: $x (-> (: $y#71684 (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689))) (-> (: $x#71685 $a#71686) $b#71688))) (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689)))) (-> (: $x#71685 $a#71686) $c#71689)))) (-> (: $y (-> (: $x (-> (: $y#71684 (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689))) (-> (: $x#71685 $a#71686) $b#71688))) (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689)))) (-> (: $x (-> (: $y#71684 (-> (: $x#71685 $a#71686) (-> (: $y#71687 $b#71688) $c#71689))) (-> (: $x#71685 $a#71686) $b#71688))) (-> (: $x#71685 $a#71686) $c#71689))))), (: (((AK AK) (AK AS)) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#71684 $c) $b#71690)) (-> (: $y (-> (: $x (-> (: $y#71684 $c) $b#71690)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#71684 $c) $b#71690)) $c)) (-> (: $x (-> (: $y#71684 $c) $b#71690)) $c)))), (: (((AK AK) (AK AS)) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#71691 $a#71692) (-> (: $y#71693 $b#71694) $c#71695)))) (-> (: $f#71696 (-> (: $x#71691 $a#71692) $b#71694)) (-> (: $x#71691 $a#71692) $c#71695))))) (-> (: $y (-> (: $x $a) (-> (: $x#71691 $a#71692) (-> (: $y#71693 $b#71694) $c#71695)))) (-> (: $x $a) (-> (: $f#71696 (-> (: $x#71691 $a#71692) $b#71694)) (-> (: $x#71691 $a#71692) $c#71695)))))), (: (((AK AK) (AK AS)) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#71697)) (-> (: $y#71698 $b#71699) $b#71697)))) (-> (: $y (-> (: $x $a) $b#71697)) (-> (: $x $a) (-> (: $y#71698 $b#71699) $b#71697))))), (: (((AK AK) (AK AS)) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#71700 $a#71701) (-> (: $y#71702 $b#71703) $c#71704))) (-> (: $y (-> (: $x (-> (: $x#71700 $a#71701) (-> (: $y#71702 $b#71703) $c#71704))) (-> (: $x#71700 $a#71701) $b#71703))) (-> (: $x#71700 $a#71701) $c#71704)))) (-> (: $y (-> (: $x (-> (: $x#71700 $a#71701) (-> (: $y#71702 $b#71703) $c#71704))) (-> (: $x#71700 $a#71701) $b#71703))) (-> (: $x (-> (: $x#71700 $a#71701) (-> (: $y#71702 $b#71703) $c#71704))) (-> (: $x#71700 $a#71701) $c#71704))))), (: (((AK AK) (AK AS)) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#71697)) $a))) (-> (: $y (-> (: $x $a) $b#71697)) (-> (: $x $a) $a)))), (: (((AK AK) (AK AS)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#71705 (-> (: $x#71706 $a#71707) (-> (: $y#71708 $b#71709) $c#71710))) (-> (: $x#71706 $a#71707) $b#71709))) (-> (: $y $b) (-> (: $x#71705 (-> (: $x#71706 $a#71707) (-> (: $y#71708 $b#71709) $c#71710))) (-> (: $x#71706 $a#71707) $c#71710))))) (-> (: $y $b) (-> (: $x (-> (: $x#71705 (-> (: $x#71706 $a#71707) (-> (: $y#71708 $b#71709) $c#71710))) (-> (: $x#71706 $a#71707) $b#71709))) (-> (: $x#71705 (-> (: $x#71706 $a#71707) (-> (: $y#71708 $b#71709) $c#71710))) (-> (: $x#71706 $a#71707) $c#71710)))))), (: (((AK AK) (AK AS)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#71705 $a#71711) $b#71712)) (-> (: $y $b) (-> (: $x#71705 $a#71711) $a#71711)))) (-> (: $y $b) (-> (: $x (-> (: $x#71705 $a#71711) $b#71712)) (-> (: $x#71705 $a#71711) $a#71711))))), (: (((AK AK) (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#71713 (-> (: $x#71714 $a#71715) (-> (: $y#71716 $b#71717) $c#71718))) (-> (: $f#71719 (-> (: $x#71714 $a#71715) $b#71717)) (-> (: $x#71714 $a#71715) $c#71718)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#71713 (-> (: $x#71714 $a#71715) (-> (: $y#71716 $b#71717) $c#71718))) (-> (: $f#71719 (-> (: $x#71714 $a#71715) $b#71717)) (-> (: $x#71714 $a#71715) $c#71718))))))), (: (((AK AK) (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#71720 $a#71721) (-> (: $y#71722 $b#71723) $a#71721))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#71720 $a#71721) (-> (: $y#71722 $b#71723) $a#71721)))))), (: (((AK AK) (AK AS)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#71724 $a#71725) (-> (: $y#71726 $b#71727) $c#71728))) (-> (: $y $b) (-> (: $f#71729 (-> (: $x#71724 $a#71725) $b#71727)) (-> (: $x#71724 $a#71725) $c#71728))))) (-> (: $y $b) (-> (: $x (-> (: $x#71724 $a#71725) (-> (: $y#71726 $b#71727) $c#71728))) (-> (: $f#71729 (-> (: $x#71724 $a#71725) $b#71727)) (-> (: $x#71724 $a#71725) $c#71728)))))), (: (((AK AK) (AK AS)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#71730 $b#71731) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#71730 $b#71731) $a))))), (: (((AK AK) (AK AS)) AS) (-> (: $f (-> (: $x (-> (: $x#71732 $a#71733) $b#71735)) (-> (: $y (-> (: $x#71732 $a#71733) (-> (: $y#71734 $b#71735) $c#71736))) (-> (: $x#71732 $a#71733) $c#71736)))) (-> (: $y (-> (: $x#71732 $a#71733) (-> (: $y#71734 $b#71735) $c#71736))) (-> (: $x (-> (: $x#71732 $a#71733) $b#71735)) (-> (: $x#71732 $a#71733) $c#71736))))), (: (((AK AK) (AK AS)) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#79013 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#79013 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#79016 $a#79017) (-> (: $y#79018 $b#79019) $c#79020))) (-> (: $y (-> (: $x (-> (: $x#79016 $a#79017) (-> (: $y#79018 $b#79019) $c#79020))) (-> (: $y#79013 (-> (: $f#79021 (-> (: $x#79016 $a#79017) $b#79019)) (-> (: $x#79016 $a#79017) $c#79020))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#79016 $a#79017) (-> (: $y#79018 $b#79019) $c#79020))) (-> (: $y#79013 (-> (: $f#79021 (-> (: $x#79016 $a#79017) $b#79019)) (-> (: $x#79016 $a#79017) $c#79020))) $c))) (-> (: $x (-> (: $x#79016 $a#79017) (-> (: $y#79018 $b#79019) $c#79020))) $c)))), (: (((AK AK) (AK AK)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#79013 (-> (: $y#79022 $b#79023) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#79013 (-> (: $y#79022 $b#79023) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#79024 $a#79025) (-> (: $y#79026 $b#79027) $c#79028))) (-> (: $y (-> (: $x (-> (: $x#79024 $a#79025) (-> (: $y#79026 $b#79027) $c#79028))) (-> (: $x#79024 $a#79025) $b#79027))) (-> (: $x#79024 $a#79025) $b#79027)))) (-> (: $y (-> (: $x (-> (: $x#79024 $a#79025) (-> (: $y#79026 $b#79027) $c#79028))) (-> (: $x#79024 $a#79025) $b#79027))) (-> (: $x (-> (: $x#79024 $a#79025) (-> (: $y#79026 $b#79027) $c#79028))) (-> (: $x#79024 $a#79025) $b#79027))))), (: (((AK AK) (AK AK)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#79029) (-> (: $y (-> (: $x $c#79029) $c)) $c))) (-> (: $y (-> (: $x $c#79029) $c)) (-> (: $x $c#79029) $c)))), (: (((AK AK) (AK AK)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#79030 $b#79031) $c#79032))) (-> (: $y#79030 $b#79031) $c#79032)))) (-> (: $y (-> (: $x $a) (-> (: $y#79030 $b#79031) $c#79032))) (-> (: $x $a) (-> (: $y#79030 $b#79031) $c#79032))))), (: (((AK AK) (AK AK)) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x#79033 $a#79034) $c#79037)))) (-> (: $y (-> (: $x#79033 $a#79034) (-> (: $y#79035 $b#79036) $c#79037))) (-> (: $x (-> (: $x#79033 $a#79034) $b#79036)) (-> (: $x#79033 $a#79034) $c#79037))))), (: (((AK AK) (AK AK)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) (AK AK)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#79038 (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043))) (-> (: $x#79039 $a#79040) $b#79042))) (-> (: $y (-> (: $x (-> (: $y#79038 (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043))) (-> (: $x#79039 $a#79040) $b#79042))) (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043)))) (-> (: $x#79039 $a#79040) $c#79043)))) (-> (: $y (-> (: $x (-> (: $y#79038 (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043))) (-> (: $x#79039 $a#79040) $b#79042))) (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043)))) (-> (: $x (-> (: $y#79038 (-> (: $x#79039 $a#79040) (-> (: $y#79041 $b#79042) $c#79043))) (-> (: $x#79039 $a#79040) $b#79042))) (-> (: $x#79039 $a#79040) $c#79043))))), (: (((AK AK) (AK AK)) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#79038 $c) $b#79044)) (-> (: $y (-> (: $x (-> (: $y#79038 $c) $b#79044)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#79038 $c) $b#79044)) $c)) (-> (: $x (-> (: $y#79038 $c) $b#79044)) $c)))), (: (((AK AK) (AK AK)) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#79045 $a#79046) (-> (: $y#79047 $b#79048) $c#79049)))) (-> (: $f#79050 (-> (: $x#79045 $a#79046) $b#79048)) (-> (: $x#79045 $a#79046) $c#79049))))) (-> (: $y (-> (: $x $a) (-> (: $x#79045 $a#79046) (-> (: $y#79047 $b#79048) $c#79049)))) (-> (: $x $a) (-> (: $f#79050 (-> (: $x#79045 $a#79046) $b#79048)) (-> (: $x#79045 $a#79046) $c#79049)))))), (: (((AK AK) (AK AK)) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#79051)) (-> (: $y#79052 $b#79053) $b#79051)))) (-> (: $y (-> (: $x $a) $b#79051)) (-> (: $x $a) (-> (: $y#79052 $b#79053) $b#79051))))), (: (((AK AK) (AK AK)) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#79054 $a#79055) (-> (: $y#79056 $b#79057) $c#79058))) (-> (: $y (-> (: $x (-> (: $x#79054 $a#79055) (-> (: $y#79056 $b#79057) $c#79058))) (-> (: $x#79054 $a#79055) $b#79057))) (-> (: $x#79054 $a#79055) $c#79058)))) (-> (: $y (-> (: $x (-> (: $x#79054 $a#79055) (-> (: $y#79056 $b#79057) $c#79058))) (-> (: $x#79054 $a#79055) $b#79057))) (-> (: $x (-> (: $x#79054 $a#79055) (-> (: $y#79056 $b#79057) $c#79058))) (-> (: $x#79054 $a#79055) $c#79058))))), (: (((AK AK) (AK AK)) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#79051)) $a))) (-> (: $y (-> (: $x $a) $b#79051)) (-> (: $x $a) $a)))), (: (((AK AK) (AK AK)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#79059 (-> (: $x#79060 $a#79061) (-> (: $y#79062 $b#79063) $c#79064))) (-> (: $x#79060 $a#79061) $b#79063))) (-> (: $y $b) (-> (: $x#79059 (-> (: $x#79060 $a#79061) (-> (: $y#79062 $b#79063) $c#79064))) (-> (: $x#79060 $a#79061) $c#79064))))) (-> (: $y $b) (-> (: $x (-> (: $x#79059 (-> (: $x#79060 $a#79061) (-> (: $y#79062 $b#79063) $c#79064))) (-> (: $x#79060 $a#79061) $b#79063))) (-> (: $x#79059 (-> (: $x#79060 $a#79061) (-> (: $y#79062 $b#79063) $c#79064))) (-> (: $x#79060 $a#79061) $c#79064)))))), (: (((AK AK) (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#79059 $a#79065) $b#79066)) (-> (: $y $b) (-> (: $x#79059 $a#79065) $a#79065)))) (-> (: $y $b) (-> (: $x (-> (: $x#79059 $a#79065) $b#79066)) (-> (: $x#79059 $a#79065) $a#79065))))), (: (((AK AK) (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#79067 (-> (: $x#79068 $a#79069) (-> (: $y#79070 $b#79071) $c#79072))) (-> (: $f#79073 (-> (: $x#79068 $a#79069) $b#79071)) (-> (: $x#79068 $a#79069) $c#79072)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#79067 (-> (: $x#79068 $a#79069) (-> (: $y#79070 $b#79071) $c#79072))) (-> (: $f#79073 (-> (: $x#79068 $a#79069) $b#79071)) (-> (: $x#79068 $a#79069) $c#79072))))))), (: (((AK AK) (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#79074 $a#79075) (-> (: $y#79076 $b#79077) $a#79075))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#79074 $a#79075) (-> (: $y#79076 $b#79077) $a#79075)))))), (: (((AK AK) (AK AK)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#79078 $a#79079) (-> (: $y#79080 $b#79081) $c#79082))) (-> (: $y $b) (-> (: $f#79083 (-> (: $x#79078 $a#79079) $b#79081)) (-> (: $x#79078 $a#79079) $c#79082))))) (-> (: $y $b) (-> (: $x (-> (: $x#79078 $a#79079) (-> (: $y#79080 $b#79081) $c#79082))) (-> (: $f#79083 (-> (: $x#79078 $a#79079) $b#79081)) (-> (: $x#79078 $a#79079) $c#79082)))))), (: (((AK AK) (AK AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#79084 $b#79085) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#79084 $b#79085) $a))))), (: (((AK AK) (AK AK)) AS) (-> (: $f (-> (: $x (-> (: $x#79086 $a#79087) $b#79089)) (-> (: $y (-> (: $x#79086 $a#79087) (-> (: $y#79088 $b#79089) $c#79090))) (-> (: $x#79086 $a#79087) $c#79090)))) (-> (: $y (-> (: $x#79086 $a#79087) (-> (: $y#79088 $b#79089) $c#79090))) (-> (: $x (-> (: $x#79086 $a#79087) $b#79089)) (-> (: $x#79086 $a#79087) $c#79090))))), (: (((AK AK) (AK AK)) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#86366 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#86366 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#86369 $a#86370) (-> (: $y#86371 $b#86372) $c#86373))) (-> (: $y (-> (: $x (-> (: $x#86369 $a#86370) (-> (: $y#86371 $b#86372) $c#86373))) (-> (: $y#86366 (-> (: $f#86374 (-> (: $x#86369 $a#86370) $b#86372)) (-> (: $x#86369 $a#86370) $c#86373))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#86369 $a#86370) (-> (: $y#86371 $b#86372) $c#86373))) (-> (: $y#86366 (-> (: $f#86374 (-> (: $x#86369 $a#86370) $b#86372)) (-> (: $x#86369 $a#86370) $c#86373))) $c))) (-> (: $x (-> (: $x#86369 $a#86370) (-> (: $y#86371 $b#86372) $c#86373))) $c)))), (: (((AK AK) AS) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#86366 (-> (: $y#86375 $b#86376) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#86366 (-> (: $y#86375 $b#86376) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#86377 $a#86378) (-> (: $y#86379 $b#86380) $c#86381))) (-> (: $y (-> (: $x (-> (: $x#86377 $a#86378) (-> (: $y#86379 $b#86380) $c#86381))) (-> (: $x#86377 $a#86378) $b#86380))) (-> (: $x#86377 $a#86378) $b#86380)))) (-> (: $y (-> (: $x (-> (: $x#86377 $a#86378) (-> (: $y#86379 $b#86380) $c#86381))) (-> (: $x#86377 $a#86378) $b#86380))) (-> (: $x (-> (: $x#86377 $a#86378) (-> (: $y#86379 $b#86380) $c#86381))) (-> (: $x#86377 $a#86378) $b#86380))))), (: (((AK AK) AS) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#86382) (-> (: $y (-> (: $x $c#86382) $c)) $c))) (-> (: $y (-> (: $x $c#86382) $c)) (-> (: $x $c#86382) $c)))), (: (((AK AK) AS) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#86383 $b#86384) $c#86385))) (-> (: $y#86383 $b#86384) $c#86385)))) (-> (: $y (-> (: $x $a) (-> (: $y#86383 $b#86384) $c#86385))) (-> (: $x $a) (-> (: $y#86383 $b#86384) $c#86385))))), (: (((AK AK) AS) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x#86386 $a#86387) $c#86390)))) (-> (: $y (-> (: $x#86386 $a#86387) (-> (: $y#86388 $b#86389) $c#86390))) (-> (: $x (-> (: $x#86386 $a#86387) $b#86389)) (-> (: $x#86386 $a#86387) $c#86390))))), (: (((AK AK) AS) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AS) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#86391 (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396))) (-> (: $x#86392 $a#86393) $b#86395))) (-> (: $y (-> (: $x (-> (: $y#86391 (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396))) (-> (: $x#86392 $a#86393) $b#86395))) (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396)))) (-> (: $x#86392 $a#86393) $c#86396)))) (-> (: $y (-> (: $x (-> (: $y#86391 (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396))) (-> (: $x#86392 $a#86393) $b#86395))) (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396)))) (-> (: $x (-> (: $y#86391 (-> (: $x#86392 $a#86393) (-> (: $y#86394 $b#86395) $c#86396))) (-> (: $x#86392 $a#86393) $b#86395))) (-> (: $x#86392 $a#86393) $c#86396))))), (: (((AK AK) AS) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#86391 $c) $b#86397)) (-> (: $y (-> (: $x (-> (: $y#86391 $c) $b#86397)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#86391 $c) $b#86397)) $c)) (-> (: $x (-> (: $y#86391 $c) $b#86397)) $c)))), (: (((AK AK) AS) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#86398 $a#86399) (-> (: $y#86400 $b#86401) $c#86402)))) (-> (: $f#86403 (-> (: $x#86398 $a#86399) $b#86401)) (-> (: $x#86398 $a#86399) $c#86402))))) (-> (: $y (-> (: $x $a) (-> (: $x#86398 $a#86399) (-> (: $y#86400 $b#86401) $c#86402)))) (-> (: $x $a) (-> (: $f#86403 (-> (: $x#86398 $a#86399) $b#86401)) (-> (: $x#86398 $a#86399) $c#86402)))))), (: (((AK AK) AS) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#86404)) (-> (: $y#86405 $b#86406) $b#86404)))) (-> (: $y (-> (: $x $a) $b#86404)) (-> (: $x $a) (-> (: $y#86405 $b#86406) $b#86404))))), (: (((AK AK) AS) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#86407 $a#86408) (-> (: $y#86409 $b#86410) $c#86411))) (-> (: $y (-> (: $x (-> (: $x#86407 $a#86408) (-> (: $y#86409 $b#86410) $c#86411))) (-> (: $x#86407 $a#86408) $b#86410))) (-> (: $x#86407 $a#86408) $c#86411)))) (-> (: $y (-> (: $x (-> (: $x#86407 $a#86408) (-> (: $y#86409 $b#86410) $c#86411))) (-> (: $x#86407 $a#86408) $b#86410))) (-> (: $x (-> (: $x#86407 $a#86408) (-> (: $y#86409 $b#86410) $c#86411))) (-> (: $x#86407 $a#86408) $c#86411))))), (: (((AK AK) AS) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#86404)) $a))) (-> (: $y (-> (: $x $a) $b#86404)) (-> (: $x $a) $a)))), (: (((AK AK) AS) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#86412 (-> (: $x#86413 $a#86414) (-> (: $y#86415 $b#86416) $c#86417))) (-> (: $x#86413 $a#86414) $b#86416))) (-> (: $y $b) (-> (: $x#86412 (-> (: $x#86413 $a#86414) (-> (: $y#86415 $b#86416) $c#86417))) (-> (: $x#86413 $a#86414) $c#86417))))) (-> (: $y $b) (-> (: $x (-> (: $x#86412 (-> (: $x#86413 $a#86414) (-> (: $y#86415 $b#86416) $c#86417))) (-> (: $x#86413 $a#86414) $b#86416))) (-> (: $x#86412 (-> (: $x#86413 $a#86414) (-> (: $y#86415 $b#86416) $c#86417))) (-> (: $x#86413 $a#86414) $c#86417)))))), (: (((AK AK) AS) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#86412 $a#86418) $b#86419)) (-> (: $y $b) (-> (: $x#86412 $a#86418) $a#86418)))) (-> (: $y $b) (-> (: $x (-> (: $x#86412 $a#86418) $b#86419)) (-> (: $x#86412 $a#86418) $a#86418))))), (: (((AK AK) AS) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#86420 (-> (: $x#86421 $a#86422) (-> (: $y#86423 $b#86424) $c#86425))) (-> (: $f#86426 (-> (: $x#86421 $a#86422) $b#86424)) (-> (: $x#86421 $a#86422) $c#86425)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#86420 (-> (: $x#86421 $a#86422) (-> (: $y#86423 $b#86424) $c#86425))) (-> (: $f#86426 (-> (: $x#86421 $a#86422) $b#86424)) (-> (: $x#86421 $a#86422) $c#86425))))))), (: (((AK AK) AS) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#86427 $a#86428) (-> (: $y#86429 $b#86430) $a#86428))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#86427 $a#86428) (-> (: $y#86429 $b#86430) $a#86428)))))), (: (((AK AK) AS) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#86431 $a#86432) (-> (: $y#86433 $b#86434) $c#86435))) (-> (: $y $b) (-> (: $f#86436 (-> (: $x#86431 $a#86432) $b#86434)) (-> (: $x#86431 $a#86432) $c#86435))))) (-> (: $y $b) (-> (: $x (-> (: $x#86431 $a#86432) (-> (: $y#86433 $b#86434) $c#86435))) (-> (: $f#86436 (-> (: $x#86431 $a#86432) $b#86434)) (-> (: $x#86431 $a#86432) $c#86435)))))), (: (((AK AK) AS) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#86437 $b#86438) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#86437 $b#86438) $a))))), (: (((AK AK) AS) AS) (-> (: $f (-> (: $x (-> (: $x#86439 $a#86440) $b#86442)) (-> (: $y (-> (: $x#86439 $a#86440) (-> (: $y#86441 $b#86442) $c#86443))) (-> (: $x#86439 $a#86440) $c#86443)))) (-> (: $y (-> (: $x#86439 $a#86440) (-> (: $y#86441 $b#86442) $c#86443))) (-> (: $x (-> (: $x#86439 $a#86440) $b#86442)) (-> (: $x#86439 $a#86440) $c#86443))))), (: (((AK AK) AS) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#93019 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#93019 $a) $c))) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#93022 $a#93023) (-> (: $y#93024 $b#93025) $c#93026))) (-> (: $y (-> (: $x (-> (: $x#93022 $a#93023) (-> (: $y#93024 $b#93025) $c#93026))) (-> (: $y#93019 (-> (: $f#93027 (-> (: $x#93022 $a#93023) $b#93025)) (-> (: $x#93022 $a#93023) $c#93026))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#93022 $a#93023) (-> (: $y#93024 $b#93025) $c#93026))) (-> (: $y#93019 (-> (: $f#93027 (-> (: $x#93022 $a#93023) $b#93025)) (-> (: $x#93022 $a#93023) $c#93026))) $c))) (-> (: $x (-> (: $x#93022 $a#93023) (-> (: $y#93024 $b#93025) $c#93026))) $c)))), (: (((AK AK) AK) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#93019 (-> (: $y#93028 $b#93029) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#93019 (-> (: $y#93028 $b#93029) $a)) $c))) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#93030 $a#93031) (-> (: $y#93032 $b#93033) $c#93034))) (-> (: $y (-> (: $x (-> (: $x#93030 $a#93031) (-> (: $y#93032 $b#93033) $c#93034))) (-> (: $x#93030 $a#93031) $b#93033))) (-> (: $x#93030 $a#93031) $b#93033)))) (-> (: $y (-> (: $x (-> (: $x#93030 $a#93031) (-> (: $y#93032 $b#93033) $c#93034))) (-> (: $x#93030 $a#93031) $b#93033))) (-> (: $x (-> (: $x#93030 $a#93031) (-> (: $y#93032 $b#93033) $c#93034))) (-> (: $x#93030 $a#93031) $b#93033))))), (: (((AK AK) AK) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#93035) (-> (: $y (-> (: $x $c#93035) $c)) $c))) (-> (: $y (-> (: $x $c#93035) $c)) (-> (: $x $c#93035) $c)))), (: (((AK AK) AK) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#93036 $b#93037) $c#93038))) (-> (: $y#93036 $b#93037) $c#93038)))) (-> (: $y (-> (: $x $a) (-> (: $y#93036 $b#93037) $c#93038))) (-> (: $x $a) (-> (: $y#93036 $b#93037) $c#93038))))), (: (((AK AK) AK) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x#93039 $a#93040) $c#93043)))) (-> (: $y (-> (: $x#93039 $a#93040) (-> (: $y#93041 $b#93042) $c#93043))) (-> (: $x (-> (: $x#93039 $a#93040) $b#93042)) (-> (: $x#93039 $a#93040) $c#93043))))), (: (((AK AK) AK) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (((AK AK) AK) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#93044 (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049))) (-> (: $x#93045 $a#93046) $b#93048))) (-> (: $y (-> (: $x (-> (: $y#93044 (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049))) (-> (: $x#93045 $a#93046) $b#93048))) (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049)))) (-> (: $x#93045 $a#93046) $c#93049)))) (-> (: $y (-> (: $x (-> (: $y#93044 (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049))) (-> (: $x#93045 $a#93046) $b#93048))) (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049)))) (-> (: $x (-> (: $y#93044 (-> (: $x#93045 $a#93046) (-> (: $y#93047 $b#93048) $c#93049))) (-> (: $x#93045 $a#93046) $b#93048))) (-> (: $x#93045 $a#93046) $c#93049))))), (: (((AK AK) AK) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#93044 $c) $b#93050)) (-> (: $y (-> (: $x (-> (: $y#93044 $c) $b#93050)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#93044 $c) $b#93050)) $c)) (-> (: $x (-> (: $y#93044 $c) $b#93050)) $c)))), (: (((AK AK) AK) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#93051 $a#93052) (-> (: $y#93053 $b#93054) $c#93055)))) (-> (: $f#93056 (-> (: $x#93051 $a#93052) $b#93054)) (-> (: $x#93051 $a#93052) $c#93055))))) (-> (: $y (-> (: $x $a) (-> (: $x#93051 $a#93052) (-> (: $y#93053 $b#93054) $c#93055)))) (-> (: $x $a) (-> (: $f#93056 (-> (: $x#93051 $a#93052) $b#93054)) (-> (: $x#93051 $a#93052) $c#93055)))))), (: (((AK AK) AK) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#93057)) (-> (: $y#93058 $b#93059) $b#93057)))) (-> (: $y (-> (: $x $a) $b#93057)) (-> (: $x $a) (-> (: $y#93058 $b#93059) $b#93057))))), (: (((AK AK) AK) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#93060 $a#93061) (-> (: $y#93062 $b#93063) $c#93064))) (-> (: $y (-> (: $x (-> (: $x#93060 $a#93061) (-> (: $y#93062 $b#93063) $c#93064))) (-> (: $x#93060 $a#93061) $b#93063))) (-> (: $x#93060 $a#93061) $c#93064)))) (-> (: $y (-> (: $x (-> (: $x#93060 $a#93061) (-> (: $y#93062 $b#93063) $c#93064))) (-> (: $x#93060 $a#93061) $b#93063))) (-> (: $x (-> (: $x#93060 $a#93061) (-> (: $y#93062 $b#93063) $c#93064))) (-> (: $x#93060 $a#93061) $c#93064))))), (: (((AK AK) AK) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#93057)) $a))) (-> (: $y (-> (: $x $a) $b#93057)) (-> (: $x $a) $a)))), (: (((AK AK) AK) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#93065 (-> (: $x#93066 $a#93067) (-> (: $y#93068 $b#93069) $c#93070))) (-> (: $x#93066 $a#93067) $b#93069))) (-> (: $y $b) (-> (: $x#93065 (-> (: $x#93066 $a#93067) (-> (: $y#93068 $b#93069) $c#93070))) (-> (: $x#93066 $a#93067) $c#93070))))) (-> (: $y $b) (-> (: $x (-> (: $x#93065 (-> (: $x#93066 $a#93067) (-> (: $y#93068 $b#93069) $c#93070))) (-> (: $x#93066 $a#93067) $b#93069))) (-> (: $x#93065 (-> (: $x#93066 $a#93067) (-> (: $y#93068 $b#93069) $c#93070))) (-> (: $x#93066 $a#93067) $c#93070)))))), (: (((AK AK) AK) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#93065 $a#93071) $b#93072)) (-> (: $y $b) (-> (: $x#93065 $a#93071) $a#93071)))) (-> (: $y $b) (-> (: $x (-> (: $x#93065 $a#93071) $b#93072)) (-> (: $x#93065 $a#93071) $a#93071))))), (: (((AK AK) AK) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#93073 (-> (: $x#93074 $a#93075) (-> (: $y#93076 $b#93077) $c#93078))) (-> (: $f#93079 (-> (: $x#93074 $a#93075) $b#93077)) (-> (: $x#93074 $a#93075) $c#93078)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#93073 (-> (: $x#93074 $a#93075) (-> (: $y#93076 $b#93077) $c#93078))) (-> (: $f#93079 (-> (: $x#93074 $a#93075) $b#93077)) (-> (: $x#93074 $a#93075) $c#93078))))))), (: (((AK AK) AK) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#93080 $a#93081) (-> (: $y#93082 $b#93083) $a#93081))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#93080 $a#93081) (-> (: $y#93082 $b#93083) $a#93081)))))), (: (((AK AK) AK) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#93084 $a#93085) (-> (: $y#93086 $b#93087) $c#93088))) (-> (: $y $b) (-> (: $f#93089 (-> (: $x#93084 $a#93085) $b#93087)) (-> (: $x#93084 $a#93085) $c#93088))))) (-> (: $y $b) (-> (: $x (-> (: $x#93084 $a#93085) (-> (: $y#93086 $b#93087) $c#93088))) (-> (: $f#93089 (-> (: $x#93084 $a#93085) $b#93087)) (-> (: $x#93084 $a#93085) $c#93088)))))), (: (((AK AK) AK) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#93090 $b#93091) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#93090 $b#93091) $a))))), (: (((AK AK) AK) AS) (-> (: $f (-> (: $x (-> (: $x#93092 $a#93093) $b#93095)) (-> (: $y (-> (: $x#93092 $a#93093) (-> (: $y#93094 $b#93095) $c#93096))) (-> (: $x#93092 $a#93093) $c#93096)))) (-> (: $y (-> (: $x#93092 $a#93093) (-> (: $y#93094 $b#93095) $c#93096))) (-> (: $x (-> (: $x#93092 $a#93093) $b#93095)) (-> (: $x#93092 $a#93093) $c#93096))))), (: (((AK AK) AK) AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: ((AS (AK AS)) (AS AK)) (-> (: $f (-> (: $x (-> (: $y#9055 $b#9056) $c)) (-> (: $y (-> (: $x (-> (: $y#9055 $b#9056) $c)) $b#9056)) $c))) (-> (: $y (-> (: $x (-> (: $y#9055 $b#9056) $c)) $b#9056)) (-> (: $x (-> (: $y#9055 $b#9056) $c)) $c)))), (: ((AS (AK AS)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $y#9055 (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523))) (-> (: $x#101519 $a#101520) $b#101522))) (-> (: $y (-> (: $x (-> (: $y#9055 (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523))) (-> (: $x#101519 $a#101520) $b#101522))) (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523)))) (-> (: $x#101519 $a#101520) $c#101523)))) (-> (: $y (-> (: $x (-> (: $y#9055 (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523))) (-> (: $x#101519 $a#101520) $b#101522))) (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523)))) (-> (: $x (-> (: $y#9055 (-> (: $x#101519 $a#101520) (-> (: $y#101521 $b#101522) $c#101523))) (-> (: $x#101519 $a#101520) $b#101522))) (-> (: $x#101519 $a#101520) $c#101523))))), (: ((AS (AK AS)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $y#9055 $c) $b#101337)) (-> (: $y (-> (: $x (-> (: $y#9055 $c) $b#101337)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#9055 $c) $b#101337)) $c)) (-> (: $x (-> (: $y#9055 $c) $b#101337)) $c)))), (: ((AS (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#101844 $a#101845) (-> (: $y#101846 $b#101847) $c#101848)))) (-> (: $f#101849 (-> (: $x#101844 $a#101845) $b#101847)) (-> (: $x#101844 $a#101845) $c#101848))))) (-> (: $y (-> (: $x $a) (-> (: $x#101844 $a#101845) (-> (: $y#101846 $b#101847) $c#101848)))) (-> (: $x $a) (-> (: $f#101849 (-> (: $x#101844 $a#101845) $b#101847)) (-> (: $x#101844 $a#101845) $c#101848)))))), (: ((AS (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#9056)) (-> (: $y#101852 $b#101853) $b#9056)))) (-> (: $y (-> (: $x $a) $b#9056)) (-> (: $x $a) (-> (: $y#101852 $b#101853) $b#9056))))), (: ((AS (AK AS)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#102096 $a#102097) (-> (: $y#102098 $b#102099) $c#102100))) (-> (: $y (-> (: $x (-> (: $x#102096 $a#102097) (-> (: $y#102098 $b#102099) $c#102100))) (-> (: $x#102096 $a#102097) $b#102099))) (-> (: $x#102096 $a#102097) $c#102100)))) (-> (: $y (-> (: $x (-> (: $x#102096 $a#102097) (-> (: $y#102098 $b#102099) $c#102100))) (-> (: $x#102096 $a#102097) $b#102099))) (-> (: $x (-> (: $x#102096 $a#102097) (-> (: $y#102098 $b#102099) $c#102100))) (-> (: $x#102096 $a#102097) $c#102100))))), (: ((AS (AK AS)) (AK AK)) (-> (: $f (-> (: $x $c) (-> (: $y (-> (: $x $c) $b#9056)) $c))) (-> (: $y (-> (: $x $c) $b#9056)) (-> (: $x $c) $c)))), (: ((AS (AK AK)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $b) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $x $b) $c)))), (: ((AS (AK AK)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#105910 $a#105911) (-> (: $y#105912 $b#105913) $c#105914))) (-> (: $y (-> (: $f#105915 (-> (: $x#105910 $a#105911) $b#105913)) (-> (: $x#105910 $a#105911) $c#105914))) $c))) (-> (: $y (-> (: $f#105915 (-> (: $x#105910 $a#105911) $b#105913)) (-> (: $x#105910 $a#105911) $c#105914))) (-> (: $x (-> (: $x#105910 $a#105911) (-> (: $y#105912 $b#105913) $c#105914))) $c)))), (: ((AS (AK AK)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $y#105918 $b#105919) $a)) $c))) (-> (: $y (-> (: $y#105918 $b#105919) $a)) (-> (: $x $a) $c)))), (: ((AS (AK AK)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#105240 (-> (: $y $b) (-> (: $y $b) $c#106937))) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $y $b) $c#106937)))) (-> (: $y $b) (-> (: $x (-> (: $y#105240 (-> (: $y $b) (-> (: $y $b) $c#106937))) (-> (: $y $b) $b))) (-> (: $y $b) $c#106937))))), (: ((AS (AK AK)) (AS AS)) (-> (: $f (-> (: $x (-> (: $y $b) (-> (: $y#107183 (-> (: $y $b) $c#107185)) $c#107185))) (-> (: $y $b) (-> (: $y $b) $c#107185)))) (-> (: $y $b) (-> (: $x (-> (: $y $b) (-> (: $y#107183 (-> (: $y $b) $c#107185)) $c#107185))) (-> (: $y $b) $c#107185))))), (: ((AS (AK AK)) (AS AK)) (-> (: $f (-> (: $x $c) (-> (: $y $b) $c))) (-> (: $y $b) (-> (: $x $c) $c)))), (: ((AS (AK AK)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#107771 (-> (: $x#107944 $a#107945) (-> (: $y#107946 $b#107947) $c#107948))) (-> (: $x#107944 $a#107945) $b#107947))) (-> (: $y $b) (-> (: $x#107771 (-> (: $x#107944 $a#107945) (-> (: $y#107946 $b#107947) $c#107948))) (-> (: $x#107944 $a#107945) $c#107948))))) (-> (: $y $b) (-> (: $x (-> (: $x#107771 (-> (: $x#107944 $a#107945) (-> (: $y#107946 $b#107947) $c#107948))) (-> (: $x#107944 $a#107945) $b#107947))) (-> (: $x#107771 (-> (: $x#107944 $a#107945) (-> (: $y#107946 $b#107947) $c#107948))) (-> (: $x#107944 $a#107945) $c#107948)))))), (: ((AS (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#107771 $c#107775) $b#107774)) (-> (: $y $b) (-> (: $x#107771 $c#107775) $c#107775)))) (-> (: $y $b) (-> (: $x (-> (: $x#107771 $c#107775) $b#107774)) (-> (: $x#107771 $c#107775) $c#107775))))), (: ((AS (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#108258 (-> (: $x#108259 $a#108260) (-> (: $y#108261 $b#108262) $c#108263))) (-> (: $f#108264 (-> (: $x#108259 $a#108260) $b#108262)) (-> (: $x#108259 $a#108260) $c#108263)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#108258 (-> (: $x#108259 $a#108260) (-> (: $y#108261 $b#108262) $c#108263))) (-> (: $f#108264 (-> (: $x#108259 $a#108260) $b#108262)) (-> (: $x#108259 $a#108260) $c#108263))))))), (: ((AS (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#108265 $a#108266) (-> (: $y#108267 $b#108268) $a#108266))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#108265 $a#108266) (-> (: $y#108267 $b#108268) $a#108266)))))), (: ((AS (AK AK)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#108510 $a#108511) (-> (: $y#108512 $b#108513) $c#108514))) (-> (: $y $b) (-> (: $f#108515 (-> (: $x#108510 $a#108511) $b#108513)) (-> (: $x#108510 $a#108511) $c#108514))))) (-> (: $y $b) (-> (: $x (-> (: $x#108510 $a#108511) (-> (: $y#108512 $b#108513) $c#108514))) (-> (: $f#108515 (-> (: $x#108510 $a#108511) $b#108513)) (-> (: $x#108510 $a#108511) $c#108514)))))), (: ((AS (AK AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#108518 $b#108519) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#108518 $b#108519) $a))))), (: ((AS AK) ((AS AS) (AS AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AS AK) (AS AK))) (-> (: $f (-> (: $y $c#113445) (-> (: $y $c#113445) $c))) (-> (: $y $c#113445) (-> (: $y $c#113445) $c)))), (: ((AS AK) ((AS AK) (AK AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AS AK) (AK AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AS AK) AS)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AS AK) AK)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) (AS AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) (AS AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) (AK AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) (AK AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) AS)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AS) AK)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) (AS AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) (AS AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) (AK AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) (AK AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) AS)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) ((AK AK) AK)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AS (AK AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) (-> (: $y#116785 $b#116786) $c#116787)))) (-> (: $y $a) (-> (: $y $a) (-> (: $y#116785 $b#116786) $c#116787))))), (: ((AS AK) (AS (AK AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AS AK)) (-> (: $f (-> (: $y $c#112578) (-> (: $y $c#112578) $c))) (-> (: $y $c#112578) (-> (: $y $c#112578) $c)))), (: ((AS AK) (AK (AS AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AK (AS AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AK (AK AS))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AK (AK AK))) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AK AS)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) (AK AK)) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) AS) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AS AK) AK) (-> (: $f (-> (: $y $a) (-> (: $y $a) $c))) (-> (: $y $a) (-> (: $y $a) $c)))), (: ((AK (AK AS)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) AS)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AS AK) AK)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) AS)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) ((AK AK) AK)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS AS)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AS AK)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK (AK AK))) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK AS)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) (AK AK)) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) AS) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AS)) AK) (-> (: $f (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x#10330 $a#10331) $c#10334)))) (-> (: $y (-> (: $x#10330 $a#10331) (-> (: $y#10332 $b#10333) $c#10334))) (-> (: $x (-> (: $x#10330 $a#10331) $b#10333)) (-> (: $x#10330 $a#10331) $c#10334))))), (: ((AK (AK AK)) ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AS) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AS) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS AS)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK AS)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) AS) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: ((AK (AK AK)) AK) (-> (: $f (-> (: $x $a) (-> (: $y $b) $b))) (-> (: $y $b) (-> (: $x $a) $b)))), (: (AS (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#138877 $a#138878) (-> (: $y#138879 $b#138880) $b#138880))) (-> (: $x (-> (: $x#138877 $a#138878) (-> (: $y#138879 $b#138880) $b#138880))) (-> (: $x#138877 $a#138878) $b#138880)))) (-> (: $x (-> (: $x#138877 $a#138878) (-> (: $y#138879 $b#138880) $b#138880))) (-> (: $x (-> (: $x#138877 $a#138878) (-> (: $y#138879 $b#138880) $b#138880))) (-> (: $x#138877 $a#138878) $b#138880))))), (: (AS (AK (AS AK))) (-> (: $f (-> (: $x $c) (-> (: $x $c) $c))) (-> (: $x $c) (-> (: $x $c) $c)))), (: (AS (AK (AK AS))) (-> (: $f (-> (: $x (-> (: $x#139184 $a#139185) (-> (: $y#139186 $b#139187) $c#139188))) (-> (: $x (-> (: $x#139184 $a#139185) (-> (: $y#139186 $b#139187) $c#139188))) (-> (: $f#139189 (-> (: $x#139184 $a#139185) $b#139187)) (-> (: $x#139184 $a#139185) $c#139188))))) (-> (: $x (-> (: $x#139184 $a#139185) (-> (: $y#139186 $b#139187) $c#139188))) (-> (: $x (-> (: $x#139184 $a#139185) (-> (: $y#139186 $b#139187) $c#139188))) (-> (: $f#139189 (-> (: $x#139184 $a#139185) $b#139187)) (-> (: $x#139184 $a#139185) $c#139188)))))), (: (AS (AK (AK AK))) (-> (: $f (-> (: $x $b) (-> (: $x $b) (-> (: $y#139192 $b#139193) $b)))) (-> (: $x $b) (-> (: $x $b) (-> (: $y#139192 $b#139193) $b))))), (: (AK ((AS AS) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#140508 $a) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#140508 $a) $c))) (-> (: $x $a) $c)))), (: (AK ((AS AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#140511 $a#140512) (-> (: $y#140513 $b#140514) $c#140515))) (-> (: $y (-> (: $x (-> (: $x#140511 $a#140512) (-> (: $y#140513 $b#140514) $c#140515))) (-> (: $y#140508 (-> (: $f#140516 (-> (: $x#140511 $a#140512) $b#140514)) (-> (: $x#140511 $a#140512) $c#140515))) $c))) $c))) (-> (: $y (-> (: $x (-> (: $x#140511 $a#140512) (-> (: $y#140513 $b#140514) $c#140515))) (-> (: $y#140508 (-> (: $f#140516 (-> (: $x#140511 $a#140512) $b#140514)) (-> (: $x#140511 $a#140512) $c#140515))) $c))) (-> (: $x (-> (: $x#140511 $a#140512) (-> (: $y#140513 $b#140514) $c#140515))) $c)))), (: (AK ((AS AS) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#140508 (-> (: $y#140517 $b#140518) $a)) $c))) $c))) (-> (: $y (-> (: $x $a) (-> (: $y#140508 (-> (: $y#140517 $b#140518) $a)) $c))) (-> (: $x $a) $c)))), (: (AK ((AS AK) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#140519 $a#140520) (-> (: $y#140521 $b#140522) $c#140523))) (-> (: $y (-> (: $x (-> (: $x#140519 $a#140520) (-> (: $y#140521 $b#140522) $c#140523))) (-> (: $x#140519 $a#140520) $b#140522))) (-> (: $x#140519 $a#140520) $b#140522)))) (-> (: $y (-> (: $x (-> (: $x#140519 $a#140520) (-> (: $y#140521 $b#140522) $c#140523))) (-> (: $x#140519 $a#140520) $b#140522))) (-> (: $x (-> (: $x#140519 $a#140520) (-> (: $y#140521 $b#140522) $c#140523))) (-> (: $x#140519 $a#140520) $b#140522))))), (: (AK ((AS AK) (AS AK))) (-> (: $f (-> (: $x $c#140524) (-> (: $y (-> (: $x $c#140524) $c)) $c))) (-> (: $y (-> (: $x $c#140524) $c)) (-> (: $x $c#140524) $c)))), (: (AK ((AS AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (AK ((AS AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (AK ((AS AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $y#140525 $b#140526) $c#140527))) (-> (: $y#140525 $b#140526) $c#140527)))) (-> (: $y (-> (: $x $a) (-> (: $y#140525 $b#140526) $c#140527))) (-> (: $x $a) (-> (: $y#140525 $b#140526) $c#140527))))), (: (AK ((AS AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $c)) $c))) (-> (: $y (-> (: $x $a) $c)) (-> (: $x $a) $c)))), (: (AK ((AK AS) (AS AS))) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AS) (AS AK))) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AS) (AK AS))) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AS) (AK AK))) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AS) AS)) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AS) AK)) (-> (: $f (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x#140528 $a#140529) $c#140532)))) (-> (: $y (-> (: $x#140528 $a#140529) (-> (: $y#140530 $b#140531) $c#140532))) (-> (: $x (-> (: $x#140528 $a#140529) $b#140531)) (-> (: $x#140528 $a#140529) $c#140532))))), (: (AK ((AK AK) (AS AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK ((AK AK) (AS AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK ((AK AK) (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK ((AK AK) (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK ((AK AK) AS)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK ((AK AK) AK)) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c)))), (: (AK (AS (AS AS))) (-> (: $f (-> (: $x (-> (: $y#140533 (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538))) (-> (: $x#140534 $a#140535) $b#140537))) (-> (: $y (-> (: $x (-> (: $y#140533 (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538))) (-> (: $x#140534 $a#140535) $b#140537))) (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538)))) (-> (: $x#140534 $a#140535) $c#140538)))) (-> (: $y (-> (: $x (-> (: $y#140533 (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538))) (-> (: $x#140534 $a#140535) $b#140537))) (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538)))) (-> (: $x (-> (: $y#140533 (-> (: $x#140534 $a#140535) (-> (: $y#140536 $b#140537) $c#140538))) (-> (: $x#140534 $a#140535) $b#140537))) (-> (: $x#140534 $a#140535) $c#140538))))), (: (AK (AS (AS AK))) (-> (: $f (-> (: $x (-> (: $y#140533 $c) $b#140539)) (-> (: $y (-> (: $x (-> (: $y#140533 $c) $b#140539)) $c)) $c))) (-> (: $y (-> (: $x (-> (: $y#140533 $c) $b#140539)) $c)) (-> (: $x (-> (: $y#140533 $c) $b#140539)) $c)))), (: (AK (AS (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) (-> (: $x#140540 $a#140541) (-> (: $y#140542 $b#140543) $c#140544)))) (-> (: $f#140545 (-> (: $x#140540 $a#140541) $b#140543)) (-> (: $x#140540 $a#140541) $c#140544))))) (-> (: $y (-> (: $x $a) (-> (: $x#140540 $a#140541) (-> (: $y#140542 $b#140543) $c#140544)))) (-> (: $x $a) (-> (: $f#140545 (-> (: $x#140540 $a#140541) $b#140543)) (-> (: $x#140540 $a#140541) $c#140544)))))), (: (AK (AS (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#140546)) (-> (: $y#140547 $b#140548) $b#140546)))) (-> (: $y (-> (: $x $a) $b#140546)) (-> (: $x $a) (-> (: $y#140547 $b#140548) $b#140546))))), (: (AK (AS AS)) (-> (: $f (-> (: $x (-> (: $x#140549 $a#140550) (-> (: $y#140551 $b#140552) $c#140553))) (-> (: $y (-> (: $x (-> (: $x#140549 $a#140550) (-> (: $y#140551 $b#140552) $c#140553))) (-> (: $x#140549 $a#140550) $b#140552))) (-> (: $x#140549 $a#140550) $c#140553)))) (-> (: $y (-> (: $x (-> (: $x#140549 $a#140550) (-> (: $y#140551 $b#140552) $c#140553))) (-> (: $x#140549 $a#140550) $b#140552))) (-> (: $x (-> (: $x#140549 $a#140550) (-> (: $y#140551 $b#140552) $c#140553))) (-> (: $x#140549 $a#140550) $c#140553))))), (: (AK (AS AK)) (-> (: $f (-> (: $x $a) (-> (: $y (-> (: $x $a) $b#140546)) $a))) (-> (: $y (-> (: $x $a) $b#140546)) (-> (: $x $a) $a)))), (: (AK (AK (AS AS))) (-> (: $f (-> (: $x (-> (: $x#140554 (-> (: $x#140555 $a#140556) (-> (: $y#140557 $b#140558) $c#140559))) (-> (: $x#140555 $a#140556) $b#140558))) (-> (: $y $b) (-> (: $x#140554 (-> (: $x#140555 $a#140556) (-> (: $y#140557 $b#140558) $c#140559))) (-> (: $x#140555 $a#140556) $c#140559))))) (-> (: $y $b) (-> (: $x (-> (: $x#140554 (-> (: $x#140555 $a#140556) (-> (: $y#140557 $b#140558) $c#140559))) (-> (: $x#140555 $a#140556) $b#140558))) (-> (: $x#140554 (-> (: $x#140555 $a#140556) (-> (: $y#140557 $b#140558) $c#140559))) (-> (: $x#140555 $a#140556) $c#140559)))))), (: (AK (AK (AS AK))) (-> (: $f (-> (: $x (-> (: $x#140554 $a#140560) $b#140561)) (-> (: $y $b) (-> (: $x#140554 $a#140560) $a#140560)))) (-> (: $y $b) (-> (: $x (-> (: $x#140554 $a#140560) $b#140561)) (-> (: $x#140554 $a#140560) $a#140560))))), (: (AK (AK (AK AS))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $g#140562 (-> (: $x#140563 $a#140564) (-> (: $y#140565 $b#140566) $c#140567))) (-> (: $f#140568 (-> (: $x#140563 $a#140564) $b#140566)) (-> (: $x#140563 $a#140564) $c#140567)))))) (-> (: $y $b) (-> (: $x $a) (-> (: $g#140562 (-> (: $x#140563 $a#140564) (-> (: $y#140565 $b#140566) $c#140567))) (-> (: $f#140568 (-> (: $x#140563 $a#140564) $b#140566)) (-> (: $x#140563 $a#140564) $c#140567))))))), (: (AK (AK (AK AK))) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $x#140569 $a#140570) (-> (: $y#140571 $b#140572) $a#140570))))) (-> (: $y $b) (-> (: $x $a) (-> (: $x#140569 $a#140570) (-> (: $y#140571 $b#140572) $a#140570)))))), (: (AK (AK AS)) (-> (: $f (-> (: $x (-> (: $x#140573 $a#140574) (-> (: $y#140575 $b#140576) $c#140577))) (-> (: $y $b) (-> (: $f#140578 (-> (: $x#140573 $a#140574) $b#140576)) (-> (: $x#140573 $a#140574) $c#140577))))) (-> (: $y $b) (-> (: $x (-> (: $x#140573 $a#140574) (-> (: $y#140575 $b#140576) $c#140577))) (-> (: $f#140578 (-> (: $x#140573 $a#140574) $b#140576)) (-> (: $x#140573 $a#140574) $c#140577)))))), (: (AK (AK AK)) (-> (: $f (-> (: $x $a) (-> (: $y $b) (-> (: $y#140579 $b#140580) $a)))) (-> (: $y $b) (-> (: $x $a) (-> (: $y#140579 $b#140580) $a))))), (: (AK AS) (-> (: $f (-> (: $x (-> (: $x#140581 $a#140582) $b#140584)) (-> (: $y (-> (: $x#140581 $a#140582) (-> (: $y#140583 $b#140584) $c#140585))) (-> (: $x#140581 $a#140582) $c#140585)))) (-> (: $y (-> (: $x#140581 $a#140582) (-> (: $y#140583 $b#140584) $c#140585))) (-> (: $x (-> (: $x#140581 $a#140582) $b#140584)) (-> (: $x#140581 $a#140582) $c#140585))))), (: (AK AK) (-> (: $f (-> (: $x $a) (-> (: $y $c) $c))) (-> (: $y $c) (-> (: $x $a) $c))))]
53.68user 0.11system 0:53.80elapsed 99%CPU (0avgtext+0avgdata 171212maxresident)k
0inputs+0outputs (0major+38198minor)pagefaults 0swaps