%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW478+2 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n009.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:38:24 PM UTC 2026 % Result : Unknown 0.56s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW478+2 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.14/0.34 % Computer : n009.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu May 7 13:35:27 EDT 2026 % 0.14/0.34 % CPUTime : % 0.14/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.62 Execution normal ended with status: gaveup % 0.47/0.62 Execution resolution_1 ended with status: gaveup % 0.47/0.62 Execution resolution_2 ended with status: gaveup % 0.47/0.62 Execution resolution_3 ended with status: gaveup % 0.47/0.62 Execution lmodel_grow ended with status: gaveup % 0.47/0.62 No successful execution. % 0.47/0.62 % 0.47/0.62 Input Clauses: % 0.56/0.63 % 0.56/0.63 Predicates: is_bool is_bop = 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 % 0.56/0.63 Fol Constants: add c_Expr_Obop_OEq bop fFalse fTrue l_a v_1 some_val v_2 produc1441475159on_val produc1259058957on_val ea produc899768717on_val ha la v e_a h_a p wf_J_mdecl some_ty some_P948696889on_val e produc823076510on_val produc5062597t_char produc621191550al_val product_Pair_val_val t_1 t produc2128769400l_bool produc1958875245l_bool cOMBB_1718333400on_val cOMBB_383678192on_val cOMBB_1303934920on_val fconj cOMBC_2027949654l_bool cOMBB_1518282696on_val cOMBC_832625297y_bool some_f80346385r_bool produc1911463199l_bool produc1815960045l_bool produc392960766l_bool produc1704639885r_bool produc1326056646l_bool produc769963999l_bool produc1401528596l_bool produc85367547l_bool produc1779501634r_bool produc1741654153l_bool produc399384568l_bool produc1988544340l_bool produc226467351on_val cOMBB_263586492ol_val cOMBB_660939282ol_val produc996400752on_val cOMBB_1150072860ol_bop cOMBB_840638159al_val produc457808617on_val cOMBB_1271765500t_char cOMBB_315503848t_char produc636580408on_val cOMBB_97313278t_char cOMBB_486278459on_val produc1174947465on_val cOMBB_819439237t_char cOMBB_877741809on_val produc1003071703on_val cOMBB_635947099on_val cOMBB_1083177073on_val produc1260869559al_val cOMBB_223841226on_val cOMBB_558176806on_val produc234747160al_val cOMBB_1210977579on_val cOMBB_448128005on_val produc576623071t_char cOMBB_2040779506on_val cOMBB_678146046on_val produc928527642on_val cOMBB_1962662865on_val cOMBB_1543649755on_val produc901351817on_val cOMBB_1466889536on_val cOMBB_171276332on_val produc1148763895on_val cOMBB_1259202826on_val cOMBB_1292453606on_val cOMBB_1056322480ol_val cOMBB_bool_bool_val cOMBB_292554190ol_bop cOMBB_2121771659al_val cOMBB_1033454012t_char cOMBB_1091123364t_char cOMBB_73690268t_char cOMBB_1572981887on_val cOMBB_740252943t_char cOMBB_338347573on_val cOMBB_466903633on_val cOMBB_672625589on_val cOMBB_1522540928on_val cOMBB_1153617344on_val cOMBB_1750801836on_val cOMBB_364363975on_val cOMBB_1466662571on_val cOMBB_1027621637t_char cOMBB_1759207793on_val cOMBB_1895512847t_char cOMBB_572737002on_val cOMBB_507649738t_char cOMBB_1749175574t_char cOMBB_1718324963ol_bop cOMBB_1353907126al_val cOMBB_1730140646ol_val cOMBB_1583755916ol_val unit produc1205785024r_bool produc778642754t_bool produc1231332391l_bool produc820564232l_bool produc1837990498l_bool produc376702929l_bool produc20018513l_bool produc111276146r_bool produc2102986512t_bool produc240246489l_bool produc286289338l_bool produc1973453616l_bool produc2036005791l_bool produc1275132703l_bool produc278452722r_bool produc155418000t_bool produc655738969l_bool produc1759631162l_bool produc1994406320l_bool produc121041439l_bool produc334393759l_bool produc1810874273r_bool produc1282419105t_bool produc737906696l_bool produc367277545l_bool produc877244993l_bool produc1812634928l_bool produc828791728l_bool produc1215886546r_bool produc2098256560t_bool produc1925718841l_bool produc1552159258l_bool produc1428203216l_bool produc2075733823l_bool produc848137919l_bool produc1780328409r_bool produc654114665t_bool produc301664320l_bool produc1596270113l_bool produc107777033l_bool produc1512975096l_bool produc530227576l_bool produc726689536r_bool produc445472770t_bool produc1289468263l_bool produc970139208l_bool produc10100002l_bool produc1267303057l_bool produc1722298385l_bool none_val void none_P179726773on_val wwf_J_mdecl classCast null nt nullPointer binop fequal_val % 0.56/0.63 Fol Functions: final_list_char conf_P373316194t_char d_list_char undefined_bop hext assigned widen_2090681816t_char is_refT wf_pro755087577t_char wTrt hAPP_bool_bool hAPP_list_char_bool hAPP_nat_bool hAPP_val_bool hAPP_f1001225811y_bool hAPP_f1033709212l_bool hAPP_f61040418l_bool hAPP_f1715346603l_bool hAPP_P943837928l_bool hAPP_P1708370145l_bool hAPP_P449474095r_bool hAPP_P1235399154l_bool hAPP_P1384137393r_bool hAPP_P929938951l_bool hAPP_P159683425l_bool hAPP_P282169671l_bool member_list_char member_nat member1417904245al_val member840932460on_val member1251428284t_char member1542417277on_val member649088532al_val member763590124on_val member773094996on_val hAPP_l207779698on_val hAPP_val_option_val hAPP_e1659493427on_val hAPP_f1849790461on_val fun_up1149430426on_val hAPP_f1727192346on_val hAPP_P604205461on_val hAPP_P1870962205on_val hAPP_P1886180715on_val red hAPP_l512744617ion_ty fun_up424764369ion_ty hAPP_n546249108on_val fun_up2041264236on_val hAPP_P2094403585on_val fun_up204312361on_val hAPP_ty_option_ty hAPP_P1510515380on_val typeSa807100911_sconf hAPP_l1786340417on_val hAPP_f900686428on_val hAPP_l208357873t_char hAPP_l2100324114t_char hAPP_b1229254591al_val hAPP_P929466802al_val hAPP_v1519391al_val hAPP_v852496844al_val hconf_97414254t_char lconf_496643946t_char hAPP_f1213370163y_bool hAPP_f2060496320y_bool hp val_list_char lAss_list_char seq_list_char block_list_char hAPP_f2121594859l_bool hAPP_f1175813647l_bool hAPP_f592397849l_bool hAPP_f1977633121l_bool hAPP_f1452292669l_bool hAPP_f1523875321l_bool hAPP_f348318673l_bool hAPP_f857351829l_bool hAPP_f838396643l_bool hAPP_f550652027l_bool cOMBS_570216337l_bool produc1159035454l_bool hAPP_P1116729363l_bool produc1911975310l_bool hAPP_e1833980889l_bool produc2062775566l_bool produc481748255l_bool hAPP_l465799708l_bool produc95371820r_bool hAPP_l1361600383r_bool produc1555310053l_bool hAPP_b97269396l_bool produc886919678l_bool hAPP_v1392248405l_bool dom_list_char_val hAPP_f363827556r_bool map_ad325961431ar_val hAPP_f635218277l_bool hAPP_f1930574389l_bool hAPP_f1443410953l_bool hAPP_f2132060507r_bool hAPP_f340876351l_bool hAPP_f1534412387l_bool dom_na996029170on_val map_ad61982421on_val dom_list_char_ty map_add_list_char_ty dom_Pr695701035ar_val map_ad1185064968ar_val hAPP_f1939255213on_val hAPP_P147338735on_val hAPP_f40221303l_bool hAPP_f1000689699l_bool hAPP_f1024478733l_bool hAPP_f1090181127on_val hAPP_P294971854on_val hAPP_f1936466825l_bool hAPP_f295212021l_bool hAPP_f1150574413l_bool hAPP_f48091733on_val hAPP_P1883022279on_val hAPP_f1683814075r_bool hAPP_f26812903r_bool hAPP_f1056413453r_bool hAPP_f372404869on_val hAPP_P1066308164on_val hAPP_f1508793015l_bool hAPP_f1138830003l_bool hAPP_f1440866903l_bool hAPP_f1520199827on_val hAPP_P789556885on_val hAPP_f1825030711l_bool hAPP_f516738477l_bool hAPP_f653692369l_bool hAPP_f394183983on_val hAPP_P1760219823on_val hAPP_f881985847l_bool hAPP_f1438732387l_bool hAPP_f1241216909l_bool hAPP_f902010623al_val hAPP_P2013623467al_val hAPP_f1589017327l_bool hAPP_f151189509l_bool hAPP_f1153851723l_bool hAPP_f928795841al_val hAPP_P1067836940al_val hAPP_f1777594159l_bool hAPP_f1572306499l_bool hAPP_f828778154l_bool hAPP_f15579599t_char hAPP_P193916115t_char hAPP_f1804599279l_bool hAPP_f1550515381l_bool hAPP_f1996106275l_bool hAPP_f1271281289on_val hAPP_P1936714534on_val hAPP_f2020099865l_bool hAPP_f630712985l_bool hAPP_f1145600492l_bool hAPP_f1309113673on_val hAPP_f1233687287l_bool hAPP_f399538905l_bool hAPP_f850751421l_bool hAPP_f204556415on_val hAPP_P2024243179on_val hAPP_f2052660463l_bool hAPP_f1043869573l_bool hAPP_f927043595l_bool hAPP_b589554111l_bool hAPP_f2051274555l_bool hAPP_f1432609211l_bool hAPP_f902521097l_bool hAPP_f653851379l_bool hAPP_f1830813581l_bool hAPP_f2092385043l_bool hAPP_f1861125939r_bool hAPP_f336522659r_bool hAPP_f1818217r_bool hAPP_f10956301l_bool hAPP_f1399435963l_bool hAPP_f624730965l_bool hAPP_f1308714617l_bool hAPP_f917296015l_bool hAPP_f546724245l_bool hAPP_f1560238713l_bool hAPP_f2032347769l_bool hAPP_f641257349l_bool hAPP_f1863694447l_bool hAPP_f1734879897l_bool hAPP_f555424277l_bool dom_nat_val fun_up846528380on_val map_add_nat_val dom_Pr1854948307al_val fun_up2650881on_val map_ad1139121712al_val dom_Pr934474290al_val fun_up1370188258on_val map_ad1808327055al_val dom_Pr881307234al_val fun_up958248092on_val map_ad1443463365al_val dom_Pr1286015283al_val fun_up106272779on_val map_ad2099161878al_val dom_Pr594962099al_val fun_up1250448779on_val map_ad1263605142al_val dom_li347256130r_bool fun_up1686981986r_bool map_ad172895647r_bool dom_na1091370954r_bool fun_up1256311364r_bool map_ad1655582893r_bool dom_Pr482007707r_bool fun_up387678665r_bool map_ad1572886776r_bool dom_Pr122328314r_bool fun_up965897386r_bool map_ad2023008343r_bool dom_Pr1770328362r_bool fun_up1281163108r_bool map_ad1209909133r_bool dom_Pr713105403r_bool fun_up1114451667r_bool map_ad1863687646r_bool dom_Pr548306299r_bool fun_up1836969043r_bool map_ad478808158r_bool dom_nat_ty fun_up421284275ion_ty map_add_nat_ty dom_Pr1536367242val_ty fun_up638349240ion_ty map_ad1402016615val_ty dom_Pr585943145val_ty fun_up430376729ion_ty map_ad1877333574val_ty dom_Pr1623760025val_ty fun_up576032467ion_ty map_ad689713276val_ty dom_Pr1523486698val_ty fun_up359791042ion_ty map_ad451392333val_ty dom_Pr1305783658val_ty fun_up160134978ion_ty map_ad860315085val_ty dom_li2046124138on_val fun_up252238218on_val map_ad1982313927on_val dom_Pr1291804355on_val fun_up768537841on_val map_ad564247072on_val dom_Pr717813794on_val fun_up307314898on_val map_ad784656511on_val dom_Pr1989649490on_val fun_up1995148684on_val map_ad2048931253on_val dom_Pr364577827on_val fun_up1177725947on_val map_ad181331206on_val dom_Pr805691811on_val fun_up683731323on_val map_ad435015558on_val hAPP_nat_option_val hAPP_P2074628057on_val hAPP_P930111162on_val hAPP_P2111013316on_val hAPP_P509577523on_val hAPP_P1594728115on_val hAPP_l1288616506r_bool hAPP_n2063106924r_bool hAPP_P926760609r_bool hAPP_P584663426r_bool hAPP_P1501097100r_bool hAPP_P1529692155r_bool hAPP_P1989760379r_bool hAPP_nat_option_ty hAPP_P1578317968ion_ty hAPP_P50259953ion_ty hAPP_P1228500987ion_ty hAPP_P142343914ion_ty hAPP_P121427050ion_ty hAPP_l195239522on_val hAPP_P1788447177on_val hAPP_P1230564778on_val hAPP_P722986275on_val hAPP_P89750179on_val hAPP_f2057883639l_bool hAPP_f1050935001l_bool hAPP_f1363667773l_bool hAPP_f365540729l_bool hAPP_f639265145l_bool hAPP_f1342895119l_bool hAPP_f10074679l_bool hAPP_f1725502637l_bool hAPP_f439412817l_bool hAPP_f1046102489l_bool hAPP_f1136596083l_bool hAPP_f21084934l_bool hAPP_f775361359r_bool hAPP_f737710471r_bool hAPP_f1633332187r_bool hAPP_f967695645l_bool hAPP_f1561329507l_bool hAPP_f42352062l_bool hAPP_f664873147l_bool hAPP_f1631509563l_bool hAPP_f2044570451l_bool hAPP_P1510984930r_bool hAPP_P1366871678r_bool hAPP_f1973249537r_bool hAPP_P576112536r_bool hAPP_P712854582t_bool hAPP_P1717724164t_bool hAPP_f1857971237t_bool hAPP_P947230058t_bool hAPP_P87436745l_bool hAPP_P1696703717l_bool hAPP_f1608665167l_bool hAPP_P912976383l_bool hAPP_P39917866l_bool hAPP_P1354850246l_bool hAPP_f1400730257l_bool hAPP_P536162016l_bool hAPP_P1232134614l_bool hAPP_P1637755428l_bool hAPP_f1341053989l_bool hAPP_P1138140810l_bool hAPP_P1134042693l_bool hAPP_P595502227l_bool hAPP_f444383845l_bool hAPP_P1826803705l_bool hAPP_P1953518277l_bool hAPP_f1591648613l_bool hAPP_P678729081l_bool hAPP_e2128781980r_bool hAPP_P599819262r_bool hAPP_f1491134931r_bool hAPP_e41879804t_bool hAPP_P107417220t_bool hAPP_f284805883t_bool hAPP_e1372786563l_bool hAPP_P698243685l_bool hAPP_f1817272339l_bool hAPP_e2019828964l_bool hAPP_P171414854l_bool hAPP_f1992719827l_bool hAPP_e1610291612l_bool hAPP_P1591874724l_bool hAPP_f802896187l_bool hAPP_e500528395l_bool hAPP_P1988153107l_bool hAPP_f468299289l_bool hAPP_e592495499l_bool hAPP_P1638898323l_bool hAPP_f1760682521l_bool hAPP_f1685556710r_bool hAPP_f774767491r_bool hAPP_f104936073r_bool hAPP_f1927197746t_bool hAPP_f235082303t_bool hAPP_f61570481t_bool hAPP_f910354125l_bool hAPP_f195923946l_bool hAPP_f800545225l_bool hAPP_f338507310l_bool hAPP_f1203390411l_bool hAPP_f2048668297l_bool hAPP_f1928083410l_bool hAPP_f57041375l_bool hAPP_f416690673l_bool hAPP_f2135509569l_bool hAPP_f396019662l_bool hAPP_f1276548047l_bool hAPP_f2144092865l_bool hAPP_f2011777102l_bool hAPP_f833559503l_bool hAPP_l1778295065r_bool hAPP_f990102836r_bool hAPP_f1650812869r_bool hAPP_P1167611309r_bool hAPP_l1460960191t_bool hAPP_f118445774t_bool hAPP_f745235151t_bool hAPP_P1120259733t_bool hAPP_l1694815232l_bool hAPP_f193834907l_bool hAPP_f1965627013l_bool hAPP_P808259092l_bool hAPP_l1294179937l_bool hAPP_f1608921212l_bool hAPP_f1140566725l_bool hAPP_P1374609397l_bool hAPP_l803240415l_bool hAPP_f192981486l_bool hAPP_f2039548047l_bool hAPP_P416784693l_bool hAPP_l989484238l_bool hAPP_f1817800029l_bool hAPP_f854417517l_bool hAPP_P733122084l_bool hAPP_l313577550l_bool hAPP_f522522333l_bool hAPP_f953970029l_bool hAPP_P1605474468l_bool hAPP_l1064716406r_bool hAPP_f1048754599r_bool hAPP_P2143028400r_bool hAPP_l1930116514t_bool hAPP_l1691929923t_bool hAPP_f477896859t_bool hAPP_P1802178130t_bool hAPP_l130580829l_bool hAPP_l780727270l_bool hAPP_f1661550453l_bool hAPP_P1988097815l_bool hAPP_l256041150l_bool hAPP_l1110132679l_bool hAPP_f507696695l_bool hAPP_P921015288l_bool hAPP_l5978434l_bool hAPP_l750759651l_bool hAPP_f1182128795l_bool hAPP_P177222514l_bool hAPP_l258171825l_bool hAPP_l1278066386l_bool hAPP_f8993627l_bool hAPP_P2034098401l_bool hAPP_l287304753l_bool hAPP_l1369340754l_bool hAPP_f499947099l_bool hAPP_P731332193l_bool hAPP_b1505407649r_bool hAPP_P343853784r_bool hAPP_f1706021209r_bool hAPP_P1308752439r_bool hAPP_b617716791t_bool hAPP_P292217386t_bool hAPP_f243373951t_bool hAPP_P1020760203t_bool hAPP_b940299656l_bool hAPP_P1815899455l_bool hAPP_f1157264807l_bool hAPP_P1882136222l_bool hAPP_b653060073l_bool hAPP_P553120288l_bool hAPP_f1353090281l_bool hAPP_P323054207l_bool hAPP_b1434170967l_bool hAPP_P1971671882l_bool hAPP_f702440703l_bool hAPP_P1354839595l_bool hAPP_b1930329414l_bool hAPP_P1389845689l_bool hAPP_f281022143l_bool hAPP_P665696794l_bool hAPP_b108134598l_bool hAPP_P693658169l_bool hAPP_f1590577855l_bool hAPP_P33140378l_bool hAPP_v1814257440r_bool hAPP_v1940296605r_bool hAPP_f1623341439r_bool hAPP_v897668472t_bool hAPP_v618097829t_bool hAPP_f1203122723t_bool hAPP_v2145502215l_bool hAPP_v1285778436l_bool hAPP_f1336948941l_bool hAPP_v620871016l_bool hAPP_v1775873509l_bool hAPP_f820838927l_bool hAPP_v1499173912l_bool hAPP_v572032837l_bool hAPP_f1724962851l_bool hAPP_v1921713543l_bool hAPP_v958864436l_bool hAPP_f727795555l_bool hAPP_v1739888647l_bool hAPP_v1688016564l_bool hAPP_f647637603l_bool oconf_1869808039t_char redp transi2024712006on_val the_val hAPP_l2138409430r_bool hAPP_l2054741776r_bool eval addr fAss_list_char fAcc_list_char throw_list_char subcls851966956t_char transi1395422419t_char tryCatch_list_char class cast_list_char has_fi1183600461t_char addr_of_sys_xcpt subcls744239332t_char transi1065307915t_char is_cla570604648t_char binOp_list_char bool while_list_char hAPP_f176769507l_bool hAPP_f1371002581r_bool hAPP_f1859015701l_bool hAPP_f414190381l_bool hAPP_f1074020887l_bool hAPP_f451093418l_bool hAPP_f332734435r_bool hAPP_f1935223905l_bool hAPP_f1181212006al_val hAPP_f1803975093l_bool hAPP_f2061154754l_bool hAPP_f384373191al_val hAPP_f181262431l_bool hAPP_f603925568l_bool hAPP_f1326058377l_bool hAPP_f338074126t_char hAPP_f1937467848l_bool hAPP_f2106552235on_val hAPP_f1145256474l_bool hAPP_f781588360l_bool hAPP_f2134824737l_bool hAPP_f496905015l_bool hAPP_v1173428276on_val hAPP_f1742268533r_bool hAPP_l80874262on_val hAPP_f497008323l_bool hAPP_v906492983on_val hAPP_f926562337l_bool hAPP_f1617787571l_bool hAPP_f1008932791l_bool hAPP_f1492320500l_bool hAPP_b420404024on_val hAPP_l867549837on_val hAPP_f1261046903l_bool hAPP_f998724171on_val hAPP_f1695781849al_val hAPP_f318082871l_bool hAPP_f1926378906on_val hAPP_f1779904442al_val hAPP_f1628326017t_char hAPP_f1614126606on_val hAPP_l221195696on_val hAPP_f1301559543l_bool hAPP_P1776198677on_val hAPP_f489055607l_bool hAPP_f1712766199l_bool hAPP_f1840640125on_val hAPP_f524589473l_bool hAPP_f602593190on_val hAPP_e108155315on_val hAPP_f204771371l_bool hAPP_f600512025on_val hAPP_P2083594489on_val skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 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 skf174 skf175 skf176 skf177 skf178 skf179 skf180 skf181 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 % 0.56/0.63 Problem Properties: % 0.56/0.63 This is a full first-order problem with equality. % 0.56/0.63 SZS status GaveUp % 0.56/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.56/0.63 %------------------------------------------------------------------------------