%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SCT170+2 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:32:19 PM UTC 2026 % Result : Unknown 0.61s 0.68s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SCT170+2 : TPTP v9.2.1. Released v5.3.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 13:01:13 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.61/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.61/0.66 Execution normal ended with status: gaveup % 0.61/0.66 Execution resolution_1 ended with status: gaveup % 0.61/0.66 Execution resolution_2 ended with status: gaveup % 0.61/0.66 Execution resolution_3 ended with status: gaveup % 0.61/0.66 Execution lmodel_grow ended with status: gaveup % 0.61/0.66 No successful execution. % 0.61/0.66 % 0.61/0.66 Input Clauses: % 0.61/0.67 % 0.61/0.67 Predicates: is_fun292781289l_bool is_fun1420103068l_bool is_fun701126715l_bool is_fun20916972t_bool is_fun866579754t_bool is_fun2015243113i_bool is_Arr723427730le_alt is_Arr859726945e_indi is_bool is_fun1264457267t_bool is_fun48324065t_bool is_Pro1004667236le_alt is_fun1651000642t_bool is_fun_bool_bool hBOOL = ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 % 0.61/0.67 Fol Constants: arrow_885770895le_IIA arrow_912654623le_Lin arrow_583275979e_Prof arrow_1550141362nimity arrow_1486210539le_alt arrow_132732488e_indi bool top_top_bool top_to186242507t_bool top_to207207712i_bool top_to1647826457l_bool top_to935749874l_bool top_to1849101472l_bool top_to846262053l_bool top_to1773227171t_bool fFalse fNot fTrue fequal21574094le_alt f p_1 p a b c member1265098019t_bool distin85347314le_alt cons_A77766063le_alt nil_Ar1135217151le_alt member720722004le_alt produc1456060119le_alt cOMBC_325526267t_bool cOMBC_1377016489t_bool cOMBB_930893948e_indi arrow_207701375_below member1704306684t_bool produc2031778509le_alt member1373125444le_alt member1619170513t_bool cOMBK_1918246033t_bool cOMBK_776703103e_indi arrow_1549387998ctator member_bool member442467260le_alt member2080870050le_alt member219620739le_alt member161528657e_indi member1097202038le_alt member300433020le_alt member1423816203t_bool member104322770t_bool member30324165t_bool member1024929995t_bool member1194332074t_bool member1770643824t_bool member1258284266t_bool member821152697t_bool member689634176t_bool member1712829811t_bool member930088569t_bool member385159430le_alt member220564739e_indi member2074697974le_alt member1464733303le_alt member1618799570e_indi member39203141le_alt member1402889547l_bool member2142449782le_alt member1935624595e_indi member1687274886le_alt member2021375116l_bool member567993161le_alt member234310528e_indi member1953881075le_alt member48503289l_bool cOMBK_1673635960le_alt cOMBK_980874600le_alt cOMBK_520250367le_alt cOMBK_1634281074le_alt cOMBK_242036279t_bool cOMBK_948333518t_bool cOMBK_1264040257t_bool cOMBK_874213703t_bool cOMBK_339579368t_bool cOMBK_1399131793t_bool cOMBK_509674590t_bool cOMBK_753699544t_bool cOMBK_1961253349t_bool cOMBK_1847391868t_bool cOMBK_906927855t_bool cOMBK_1068969205t_bool cOMBK_78615028le_alt cOMBK_1925322610le_alt cOMBK_1685845624l_bool cOMBK_1744976613le_alt cOMBK_1217667022e_indi cOMBK_1549622337le_alt cOMBK_391161927l_bool cOMBK_549130676le_alt cOMBK_740566962le_alt cOMBK_1028572856l_bool cOMBK_1435997879le_alt cOMBK_472365180e_indi cOMBK_165199855le_alt cOMBK_1377637877l_bool cOMBK_350223551e_indi null_A1369988103le_alt equal_732151074le_alt member694465108le_alt produc1707341143le_alt cons_l882637220le_alt lexord717456039le_alt lexord807118444le_alt top_to818291475t_bool cOMBB_966447723le_alt cOMBC_2032358938t_bool cOMBK_577652221t_bool cOMBK_776847951t_bool cOMBK_1733734784le_alt cOMBK_1391252605e_indi cOMBK_507931254le_alt cOMBK_715978704t_bool append28105492le_alt lex_Ar1264540259le_alt append1413540863le_alt nil_li7342420le_alt listre868094907le_alt listre1913026136le_alt cOMBB_521986850le_alt cOMBC_168079159le_alt cOMBC_1169281096le_alt lex_li910676976le_alt cOMBS_1569784209le_alt cOMBB_1988247237le_alt cOMBS_1626428525le_alt cOMBB_215060470le_alt cOMBB_1675847172le_alt cOMBB_1236261828le_alt cOMBC_72147604le_alt cOMBB_96247696le_alt cOMBB_1303549321le_alt listre1769678631le_alt listre870705708le_alt cOMBK_1825575856le_alt cOMBC_441619036t_bool cOMBB_333235735le_alt cOMBC_943734388l_bool cOMBB_885534287le_alt cOMBB_711698847le_alt cOMBC_1696964078t_bool cOMBB_1326560562le_alt cOMBC_1827582133l_bool cOMBB_1150645560le_alt cOMBB_1407335828le_alt fequal1028827333le_alt drop_A1195732799le_alt distin1906002420le_alt cOMBB_1957338939le_alt cOMBC_1094121654t_bool fequal1025934616le_alt distin26300929e_indi cOMBB_1957128648e_indi cOMBC_553632464i_bool fequal2012472101e_indi distinct_bool cOMBB_bool_bool_bool cOMBC_bool_bool_bool fequal_bool distin943033217t_bool cOMBB_410960200t_bool cOMBC_921123792l_bool fequal547890341t_bool distin751056204t_bool cOMBB_1517321413t_bool cOMBC_906425754l_bool fequal318101288t_bool distin526492627t_bool cOMBB_1376111258t_bool cOMBC_1887456628l_bool fequal1289369847t_bool distin135982852le_alt cOMBB_1860605643le_alt cOMBC_518322134t_bool fequal1881358376le_alt cons_P1245424375le_alt cons_A920022916e_indi cons_bool cons_f1113423620t_bool cons_f476294153t_bool cons_f160345174t_bool cons_P272751751le_alt cOMBC_1158490499le_alt drop_P635442535le_alt drop_A1853358580e_indi drop_bool drop_f1274868084t_bool drop_f1849462169t_bool drop_f1584869062t_bool drop_P1440509687le_alt append1768277586le_alt append968919903e_indi append_bool append1480696031t_bool append2131097198t_bool append352340785t_bool append1735936098le_alt nil_Pr1710246567le_alt nil_Ar637146932e_indi nil_bool nil_fu1180010164t_bool nil_fu1714546777t_bool nil_fu247759878t_bool nil_Pr1368032311le_alt member1245674225le_alt member985525226le_alt produc218110963le_alt member1805745300le_alt produc499297815le_alt lexord170366202le_alt member258426884e_indi produc2070216205e_indi member912023252e_indi produc1849892183e_indi lexord1918670343e_indi member624253174l_bool produc1246214911l_bool member1058364180t_bool produc1067887767t_bool lexord_bool member205384452t_bool produc882973453t_bool member200634580t_bool produc49085783t_bool lexord1145600903t_bool member2100323796t_bool produc1802651735t_bool member1477971960t_bool produc1134856577t_bool lexord1692326342t_bool member1765007528t_bool produc999701681t_bool member976989780t_bool produc436944087t_bool lexord373145049t_bool member852432522le_alt produc744410643le_alt member1353676180le_alt produc1787549079le_alt lexord1008325386le_alt ord_less_nat ord_less_eq_nat skc1 skc21 skc22 skc23 skc24 skc174 skc175 skc176 skc177 skc178 skc179 skc180 skc181 skc294 % 0.61/0.67 Fol Functions: in_rel1361124802le_alt pi_Arr1801471756t_bool pi_fun1555365306t_bool pi_Pro1873779901t_bool undefi1471133025le_alt undefi1052853330e_indi undefined_bool product_prod fun undefi426827556t_bool undefi396693458t_bool undefi541132219t_bool undefi1522782549le_alt hd_Arr1814706386le_alt hd_Arr1280875809e_indi hd_bool hd_fun780865267t_bool hd_fun1289819809t_bool hd_fun1937506860t_bool hd_Pro804272676le_alt last_A1066338328le_alt last_A560832347e_indi last_bool last_f1921219373t_bool last_f584510683t_bool last_f1172522866t_bool last_P15572062le_alt set_Ar426477344le_alt set_Ar1035526739e_indi set_bool set_fu222164517t_bool set_fu1433968595t_bool set_fu444796538t_bool set_Pr2031705942le_alt order_1844940151le_alt produc616221118t_bool produc278404511t_bool collec591097828le_alt collec279390863e_indi collec1567922785t_bool collec1517527055t_bool collec612883262t_bool collec1376511890le_alt hAPP_A1120018583t_bool hAPP_A1781286015t_bool hAPP_A630236912t_bool hAPP_A1745457982l_bool hAPP_A88621982t_bool hAPP_A990651116l_bool hAPP_A433435097l_bool hAPP_A1014090479t_bool hAPP_A1561816353le_alt hAPP_A416869060i_bool hAPP_A1609075839i_bool hAPP_A739031709t_bool hAPP_A701636433l_bool hAPP_A1433148491t_bool hAPP_A955165183l_bool hAPP_A659996934l_bool hAPP_A340536322t_bool hAPP_A503573454le_alt hAPP_bool_bool hAPP_b287951269t_bool hAPP_b2116075462i_bool hAPP_b821377302t_bool hAPP_b589554111l_bool hAPP_b1461182872l_bool hAPP_b327863236t_bool hAPP_b651754310l_bool hAPP_b805997823l_bool hAPP_b763490121t_bool hAPP_b1482008903le_alt hAPP_l300482276t_bool hAPP_l479254477i_bool hAPP_list_bool_bool hAPP_l784127213t_bool hAPP_l4338847l_bool hAPP_l1936415565l_bool hAPP_l1684828478l_bool hAPP_l548550096t_bool hAPP_l1642116416t_bool hAPP_nat_bool hAPP_f87553445l_bool hAPP_f246757773t_bool hAPP_f271508829t_bool hAPP_f160177134l_bool hAPP_f1282033109i_bool hAPP_f1287961430le_alt hAPP_f350403485e_indi hAPP_f1378099862l_bool hAPP_f3167870t_bool hAPP_f1570138413i_bool hAPP_f591334822l_bool hAPP_f1901083135l_bool hAPP_f1895971544l_bool hAPP_f1817389232t_bool hAPP_f387058535l_bool hAPP_f961197973l_bool hAPP_f1472889102l_bool hAPP_f2140553640l_bool hAPP_f1134444118l_bool hAPP_f640821677l_bool hAPP_f2129568089l_bool hAPP_f1898839893l_bool hAPP_f2016919811l_bool hAPP_f147218624l_bool hAPP_f189058133l_bool hAPP_f1273877800le_alt hAPP_f2043811403e_indi hAPP_f446648900l_bool hAPP_f1741989420t_bool hAPP_f783549695i_bool hAPP_f721327224l_bool hAPP_f656614015l_bool hAPP_f1291635206l_bool hAPP_f620747982l_bool hAPP_f740740988l_bool hAPP_f937100551l_bool hAPP_f2053170815l_bool hAPP_f412569108l_bool hAPP_f882250837l_bool hAPP_f1138659662l_bool hAPP_f322109294l_bool hAPP_f1028172757l_bool hAPP_f505027144l_bool hAPP_f1094272486l_bool hAPP_f742658307l_bool hAPP_f750478076l_bool hAPP_f1484382710l_bool hAPP_f1518247545l_bool hAPP_f1021828400l_bool hAPP_f560261801l_bool hAPP_f270557859l_bool hAPP_f784749731l_bool hAPP_f817344902l_bool hAPP_f560517119l_bool hAPP_f574392641l_bool hAPP_f437011961l_bool hAPP_f404365000l_bool hAPP_f2139503478l_bool hAPP_f1488127117l_bool hAPP_f2031902329l_bool hAPP_f459545019le_alt hAPP_f1283454584e_indi hAPP_f1733357041l_bool hAPP_f1068593625t_bool hAPP_f1840820673t_bool hAPP_f431432850i_bool hAPP_f590186314t_bool hAPP_f812095627l_bool hAPP_f1344932147l_bool hAPP_f137597973t_bool hAPP_f511649569l_bool hAPP_f1098788115l_bool hAPP_f890578273l_bool hAPP_f1140617841l_bool hAPP_f263022001l_bool hAPP_f2099712241l_bool hAPP_f288803825l_bool hAPP_f1456773233l_bool hAPP_f1422872597l_bool hAPP_f1342253361l_bool hAPP_f2078996785l_bool hAPP_f1508705733l_bool hAPP_f140107297l_bool hAPP_f891725169l_bool hAPP_f1720639399l_bool hAPP_f704486919l_bool hAPP_P870295781le_alt hAPP_P1645359566e_indi hAPP_P1813625415t_bool hAPP_P1116266031t_bool hAPP_P957402556i_bool hAPP_P1122857141l_bool hAPP_P1151433609l_bool hAPP_P1999019327t_bool hAPP_P1373277879t_bool hAPP_P1689126160t_bool hAPP_P2049543454l_bool hAPP_P482525630t_bool hAPP_P1533476044l_bool hAPP_P467353593l_bool hAPP_P651748559t_bool hAPP_P802532161le_alt hAPP_f621397159l_bool hAPP_A1660609715le_alt hAPP_l372964747le_alt hAPP_A1171966089le_alt hAPP_f2020174441t_bool hAPP_f1044120523t_bool hAPP_f114580065t_bool hAPP_A711952286t_bool hAPP_f832306437t_bool arrow_163947511_mkbot arrow_312654597_mktop hAPP_f1332197581l_bool hAPP_f684072049t_bool hAPP_A28770973t_bool hAPP_l1148780281le_alt hAPP_l591780830le_alt in_rel264468792le_alt hAPP_l2066632447t_bool hAPP_P2032392041l_bool hAPP_f881677315l_bool hAPP_f633903640l_bool arrow_1046586475_above hAPP_b1787118453l_bool hAPP_f884817497l_bool pi_Arr914263595le_alt hAPP_A86021709l_bool hAPP_f1234917389l_bool pi_Arr1064242500le_alt hAPP_A45661955l_bool hAPP_f772908877l_bool pi_Pro1742482359le_alt hAPP_f452450509l_bool pi_boo1542163389le_alt hAPP_f1101355639l_bool pi_Arr425730554t_bool hAPP_f1836999501l_bool pi_Arr656802323t_bool hAPP_f4855309l_bool pi_Pro54111110t_bool hAPP_f1518101645l_bool pi_boo679625100t_bool hAPP_f1475191373l_bool pi_Arr1752452453t_bool hAPP_f1070625729l_bool pi_Pro1560469721t_bool hAPP_f840347317l_bool pi_boo1746012499t_bool hAPP_f850619859l_bool pi_Arr1120237736t_bool hAPP_f1063991245l_bool pi_Arr742795713t_bool hAPP_f115737741l_bool pi_Pro519450164t_bool hAPP_f2134766349l_bool pi_boo68262458t_bool hAPP_f731818989l_bool pi_Pro222743023le_alt hAPP_f1387788301l_bool pi_Pro58544964e_indi hAPP_f1325762381l_bool pi_Pro368504503le_alt hAPP_P1576037953le_alt hAPP_P1436281263t_bool hAPP_f1136111951l_bool pi_fun1083455072le_alt hAPP_f1140532045l_bool pi_fun268174099e_indi hAPP_f1140553229l_bool pi_fun1110020102le_alt hAPP_f597551504le_alt hAPP_f1329247136t_bool hAPP_f1338606733l_bool pi_fun1236347660l_bool hAPP_f599048525l_bool pi_fun1197906993le_alt hAPP_f2022872455l_bool pi_fun596906370e_indi hAPP_f635489773l_bool pi_fun404660213le_alt hAPP_f1643422699le_alt hAPP_f1681297285t_bool hAPP_f1171266041l_bool pi_fun568395771l_bool hAPP_f1880077555l_bool pi_fun158009906le_alt hAPP_f749156301l_bool pi_fun1353458625e_indi hAPP_f1894818957l_bool pi_fun481655732le_alt hAPP_f444731198le_alt hAPP_f1114489970t_bool hAPP_f2087408397l_bool pi_fun187048122l_bool hAPP_f719005683l_bool hAPP_f342341961t_bool hAPP_f3439105i_bool hAPP_f2022891751t_bool hAPP_f1698272152t_bool hAPP_f1274922098i_bool hAPP_f303195352t_bool hAPP_f498119908l_bool hAPP_f391873743t_bool hAPP_f1077635369i_bool hAPP_f684471657t_bool hAPP_f2062029545l_bool hAPP_f1300833606t_bool hAPP_f1377869636i_bool hAPP_f1228246954t_bool hAPP_f1459432374l_bool hAPP_f102394819t_bool hAPP_f1737373975t_bool hAPP_f581841297t_bool hAPP_f1973254019l_bool hAPP_f1932802664l_bool hAPP_f978113205l_bool hAPP_f1768325679l_bool hAPP_f1954218281l_bool hAPP_f905851705l_bool hAPP_f118515775l_bool hAPP_f1136405251l_bool hAPP_f206814660l_bool hAPP_f1197671953l_bool hAPP_f1756719499l_bool hAPP_f1639180358l_bool splice1369921490le_alt insert1969589781le_alt produc930723380t_bool hAPP_l1663319606le_alt hAPP_l1425181461le_alt hAPP_l400262709le_alt hAPP_l2112442743le_alt hAPP_P142941065l_bool hAPP_f664322981t_bool butlas123970891le_alt hAPP_f1211148133t_bool takeWh1545314552le_alt partit1336600824le_alt hAPP_l1390889510le_alt hAPP_l1626273389le_alt rotate184372300le_alt hAPP_f268020663le_alt hAPP_f239458941le_alt hAPP_f18365135le_alt hAPP_l1693669363le_alt hAPP_f904937452le_alt list_c1434691767le_alt size_s101148091le_alt size_s2106320494le_alt dropWh1165804960le_alt hAPP_f1558754397le_alt if_Pro1659200999le_alt hAPP_f1654251593le_alt hAPP_f1949171529le_alt hAPP_f1124725731le_alt hAPP_f670565125le_alt hAPP_f1504748473le_alt hAPP_f310101886le_alt hAPP_f2122335314le_alt hAPP_f332249751le_alt hAPP_f593033837le_alt hAPP_f351228915le_alt hAPP_f794134621le_alt produc1250814607le_alt hAPP_P2096362161le_alt lexn_A19384479le_alt produc1802641557t_bool tl_Arr314474198le_alt hAPP_f921948995le_alt hAPP_f1682340965t_bool hAPP_f1585690341l_bool hAPP_f274832101l_bool hAPP_f1747206697l_bool hAPP_f1092358369t_bool hAPP_f775987425t_bool listre1062185049le_alt hAPP_f1503353479t_bool hAPP_f1224738111l_bool hAPP_f1418100887l_bool hAPP_f1893731349l_bool hAPP_f1837837439t_bool hAPP_f1997384703t_bool hAPP_f1895633847t_bool listre1064220282le_alt hAPP_l508185643t_bool rev_Ar955429983le_alt replic1360561849le_alt hAPP_n344665784le_alt set_Pr1756729158le_alt hAPP_f2036795507t_bool hAPP_f1542885353t_bool hAPP_P1133336895t_bool hAPP_f2073680917t_bool rev_Pr816629831le_alt takeWh768831342le_alt dropWh1957015750le_alt tl_Pro645285392le_alt hAPP_f1765349427i_bool hAPP_f791932009i_bool rev_Ar758908116e_indi takeWh1088896635e_indi dropWh1417102291e_indi tl_Arr282712093e_indi hAPP_f1172769267l_bool hAPP_f1897201897l_bool rev_bool takeWhile_bool dropWhile_bool tl_bool hAPP_f920654899l_bool hAPP_f1031027817l_bool rev_fu580432980t_bool takeWh1268567035t_bool dropWh1122107731t_bool tl_fun1512606109t_bool hAPP_f2007076633l_bool hAPP_f574303429l_bool rev_fu101184185t_bool takeWh572506194t_bool dropWh193383674t_bool tl_fun1131179056t_bool hAPP_f2048491699l_bool hAPP_f576161641l_bool rev_fu313987494t_bool takeWh1813199437t_bool dropWh2056378277t_bool tl_fun542205423t_bool hAPP_f2063770867t_bool hAPP_f1381403369t_bool rev_Pr1722970583le_alt takeWh808795006le_alt dropWh1186971862le_alt tl_Pro1439282464le_alt hAPP_P469465955le_alt hAPP_l182884309le_alt hAPP_A273991894e_indi hAPP_l1557274901e_indi hAPP_b994696797t_bool hAPP_l1189022293t_bool hAPP_f597269334t_bool hAPP_l1149974805t_bool hAPP_f1916337549t_bool hAPP_l342779967t_bool hAPP_f1337535236t_bool hAPP_l1130749077t_bool hAPP_P465197523le_alt hAPP_l850073941le_alt hAPP_f1660378693le_alt hAPP_l1244209582le_alt nat_ca247420624le_alt foldl_107212092le_alt hAPP_n323901960le_alt hAPP_n568645704e_indi hAPP_n479129736t_bool hAPP_n587545160t_bool hAPP_n2058955628t_bool hAPP_n2099236808t_bool hAPP_n2100915976le_alt butlas1808913499le_alt butlas1811107560e_indi butlast_bool butlas423814760t_bool butlas217264037t_bool butlas813551546t_bool butlas1168145387le_alt insert531176721le_alt insert1731565726e_indi insert_bool insert897399838t_bool insert1409495663t_bool insert22093680t_bool insert1683711393le_alt hAPP_l2076130586le_alt hAPP_l203258125e_indi hAPP_l1947611924t_bool hAPP_l1032792973t_bool hAPP_l1392153600t_bool hAPP_l1438053435t_bool hAPP_l595508106le_alt last_P1076199502le_alt hd_Pro53798164le_alt hAPP_l1197505987l_bool set_li1879521523le_alt hAPP_P1109943007le_alt hAPP_P937918807le_alt hAPP_P1992806581l_bool hAPP_l1615793307le_alt hAPP_l1556767370le_alt hAPP_P1085061129l_bool hAPP_f304790207t_bool hAPP_A785351481e_indi hAPP_A2054143614e_indi hAPP_P1435933929l_bool hAPP_l1484722549e_indi hAPP_l2129529815e_indi hAPP_P173682825l_bool hAPP_f695049061i_bool hAPP_b1115999851l_bool hAPP_b2048821609l_bool hAPP_P738148045l_bool hAPP_l218095399t_bool hAPP_l1349316624t_bool hAPP_P1870454025l_bool hAPP_f1114274611l_bool hAPP_f1596466233t_bool hAPP_f38433022t_bool hAPP_P1099469545l_bool hAPP_l1784712821t_bool hAPP_l1242238295t_bool hAPP_P776750217l_bool hAPP_f357296741l_bool hAPP_f1999636669t_bool hAPP_f1265889019t_bool hAPP_P1919864457l_bool hAPP_l131013165t_bool hAPP_l839073004t_bool hAPP_P328558801l_bool hAPP_f2031254713l_bool hAPP_f1785736029t_bool hAPP_f1639289588t_bool hAPP_P1374173745l_bool hAPP_l1064263321t_bool hAPP_l607015721t_bool hAPP_P981043081l_bool hAPP_f363884353l_bool hAPP_P1725284223le_alt hAPP_P29732487le_alt hAPP_P626359285l_bool hAPP_l794402875le_alt hAPP_l309028378le_alt hAPP_P585301513l_bool hAPP_f846944031t_bool hAPP_n1699378549t_bool suc hAPP_P1891191097le_alt hAPP_n2108195705le_alt hAPP_A1849759038le_alt hAPP_f372913425t_bool hAPP_A85603248t_bool hAPP_f921250311t_bool hAPP_f4315714t_bool hAPP_l1493471510l_bool hAPP_A64811457t_bool hAPP_f879032165le_alt hAPP_f1216999144le_alt hAPP_A1202525278t_bool hAPP_f1656652505l_bool hAPP_l2144750563t_bool hAPP_f1928725626le_alt hAPP_f1427069397le_alt hAPP_l1791846092le_alt hAPP_f622637325l_bool hAPP_l486475401le_alt hAPP_A643475905l_bool hAPP_l486097526le_alt hAPP_f1291634731le_alt hAPP_l1748807729l_bool hAPP_l436896263le_alt skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf25 skf26 skf27 skf28 skf29 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45 skf46 skf47 skf48 skf49 skf50 skf51 skf52 skf53 skf54 skf55 skf56 skf57 skf58 skf59 skf60 skf61 skf62 skf63 skf64 skf65 skf66 skf67 skf68 skf69 skf70 skf71 skf72 skf73 skf74 skf75 skf76 skf77 skf78 skf79 skf80 skf81 skf82 skf83 skf84 skf85 skf86 skf87 skf88 skf89 skf90 skf91 skf92 skf93 skf94 skf95 skf96 skf97 skf98 skf99 skf100 skf101 skf102 skf103 skf104 skf105 skf106 skf107 skf108 skf109 skf110 skf111 skf112 skf113 skf114 skf115 skf116 skf117 skf118 skf119 skf120 skf121 skf122 skf123 skf124 skf125 skf126 skf127 skf128 skf129 skf130 skf131 skf132 skf133 skf134 skf135 skf136 skf137 skf138 skf139 skf140 skf141 skf142 skf143 skf144 skf145 skf146 skf147 skf148 skf149 skf150 skf151 skf152 skf153 skf154 skf155 skf156 skf157 skf158 skf159 skf160 skf161 skf162 skf163 skf164 skf165 skf166 skf167 skf168 skf169 skf170 skf171 skf172 skf173 skf182 skf183 skf184 skf185 skf186 skf187 skf188 skf189 skf190 skf191 skf192 skf193 skf194 skf195 skf196 skf197 skf198 skf199 skf200 skf201 skf202 skf203 skf204 skf205 skf206 skf207 skf208 skf209 skf210 skf211 skf212 skf213 skf214 skf215 skf216 skf217 skf218 skf219 skf220 skf221 skf222 skf223 skf224 skf225 skf226 skf227 skf228 skf229 skf230 skf231 skf232 skf233 skf234 skf235 skf236 skf237 skf238 skf239 skf240 skf241 skf242 skf243 skf244 skf245 skf246 skf247 skf248 skf249 skf250 skf251 skf252 skf253 skf254 skf255 skf256 skf257 skf258 skf259 skf260 skf261 skf262 skf263 skf264 skf265 skf266 skf267 skf268 skf269 skf270 skf271 skf272 skf273 skf274 skf275 skf276 skf277 skf278 skf279 skf280 skf281 skf282 skf283 skf284 skf285 skf286 skf287 skf288 skf289 skf290 skf291 skf292 skf293 % 0.61/0.67 Problem Properties: % 0.61/0.67 This is a full first-order problem with equality. % 0.61/0.67 SZS status GaveUp % 0.61/0.67 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.61/0.67 %------------------------------------------------------------------------------