%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW477+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 : n013.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:23 PM UTC 2026 % Result : Unknown 0.59s 0.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW477+2 : TPTP v9.2.1. Released v5.3.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n013.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 13:35:42 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.59/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.63 Execution normal ended with status: gaveup % 0.59/0.63 Execution resolution_1 ended with status: gaveup % 0.59/0.63 Execution resolution_2 ended with status: gaveup % 0.59/0.63 Execution resolution_3 ended with status: gaveup % 0.59/0.63 Execution lmodel_grow ended with status: gaveup % 0.59/0.63 No successful execution. % 0.59/0.63 % 0.59/0.63 Input Clauses: % 0.59/0.64 % 0.59/0.64 Predicates: is_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 % 0.59/0.64 Fol Constants: fFalse fTrue p ha e ea nt h_a e_a wf_J_mdecl produc899768717on_val la f d e_2 t produc1441475159on_val produc1259058957on_val l_a boolean void produc2080520419t_char produc499151895on_val produc1299387215t_char produc57279289t_char produc24551831t_char produc1951691075on_val produc1564932627on_val produc870913623on_val produc1611380469on_val produc379668296on_val produc921874948t_char produc1909267824t_char produc1916172923t_char produc823076510on_val produc5062597t_char produc2128769400l_bool produc1958875245l_bool cOMBB_1718333400on_val cOMBB_383678192on_val cOMBB_1303934920on_val fconj cOMBC_2027949654l_bool cOMBB_1518282696on_val cOMBC_832625297y_bool produc1131232171r_bool produc870083295l_bool produc22827031r_bool produc1470355201r_bool produc1294339167r_bool produc376173579l_bool produc1229156571l_bool produc1193275679l_bool produc1911463199l_bool produc1815960045l_bool produc70644925l_bool produc1491230096l_bool produc2027921764r_bool produc154616760r_bool produc21910851r_bool produc392960766l_bool produc1704639885r_bool cOMBB_1033454012t_char cOMBB_1091123364t_char cOMBB_73690268t_char cOMBB_1572981887on_val cOMBB_137522603st_val cOMBB_1373881771t_char cOMBB_972090594ist_ty cOMBB_455741289t_char cOMBB_1310111461t_char cOMBB_224920158t_char cOMBB_1638169504t_char cOMBB_338347573on_val cOMBB_2073500116on_val cOMBB_506101180on_val cOMBB_740252943t_char cOMBB_466903633on_val cOMBB_672625589on_val cOMBB_1522540928on_val produc1779501634r_bool produc1741654153l_bool produc684674552r_bool produc1657965293r_bool produc19303535r_bool produc1631960005l_bool produc2085082994l_bool produc399384568l_bool produc1988544340l_bool produc457808617on_val cOMBB_1271765500t_char cOMBB_315503848t_char produc636580408on_val cOMBB_97313278t_char cOMBB_486278459on_val produc2083294131on_val cOMBB_1124198201st_val cOMBB_1539035119t_char produc534648062on_val cOMBB_1843549548ist_ty cOMBB_1115744685t_char produc726497362on_val cOMBB_889837233t_char cOMBB_1980206754t_char produc1450794278on_val cOMBB_143000234t_char cOMBB_877741809on_val produc653117369on_val cOMBB_607314500on_val cOMBB_1173566976on_val produc1174947465on_val cOMBB_819439237t_char produc1003071703on_val cOMBB_635947099on_val cOMBB_1083177073on_val produc576623071t_char cOMBB_2040779506on_val cOMBB_678146046on_val produc928527642on_val cOMBB_1962662865on_val cOMBB_1543649755on_val produc1139048085t_char cOMBB_335252392on_val cOMBB_1733006024on_val produc493500298t_char cOMBB_1472123293on_val cOMBB_95569939on_val produc1597824762t_char cOMBB_1443356337on_val cOMBB_1837440507on_val produc1202869992on_val cOMBB_157777659on_val cOMBB_1466435125on_val produc1476705295on_val cOMBB_1330725154on_val cOMBB_132741582on_val produc901351817on_val cOMBB_1466889536on_val cOMBB_171276332on_val produc1148763895on_val cOMBB_1259202826on_val cOMBB_1292453606on_val cOMBB_1153617344on_val cOMBB_1750801836on_val cOMBB_364363975on_val cOMBB_1466662571on_val cOMBB_1027621637t_char cOMBB_1759207793on_val cOMBB_1068689586on_val cOMBB_256117342on_val cOMBB_298947045t_char cOMBB_1085967610on_val cOMBB_580983202t_char cOMBB_2081530643t_char cOMBB_847301125ist_ty cOMBB_865194374t_char cOMBB_698101635st_val cOMBB_215184339t_char cOMBB_1895512847t_char cOMBB_572737002on_val cOMBB_507649738t_char cOMBB_1749175574t_char val_list_char unit c_Expr_Obop_OEq null nullPointer wwf_J_mdecl % 0.59/0.64 Fol Functions: final_list_char finals_list_char hext widen_2090681816t_char is_refT wf_pro755087577t_char wTrt wTrts hAPP_e544220455r_bool hAPP_bool_bool hAPP_list_char_bool hAPP_f1001225811y_bool hAPP_f1033709212l_bool hAPP_f61040418l_bool hAPP_f1715346603l_bool hAPP_P1708370145l_bool hAPP_P71593144l_bool hAPP_P92196306r_bool hAPP_P449474095r_bool hAPP_P1235399154l_bool hAPP_P1384137393r_bool hAPP_P1907982426r_bool hAPP_P2118621157r_bool hAPP_P159683425l_bool hAPP_P282169671l_bool hAPP_P1333315679l_bool hAPP_P824029447r_bool hAPP_P2010574925r_bool hAPP_P124632071l_bool hAPP_P1240100515r_bool hAPP_P1183499705r_bool hAPP_P1221872711l_bool hAPP_P378063101l_bool hAPP_P2028072621l_bool member840932460on_val member1972431429on_val member133545693t_char member1251428284t_char member1542417277on_val member140606439t_char member699351154t_char member763590124on_val member773094996on_val member875476972on_val member1420286996t_char member794220506t_char member1322055188on_val member125098544t_char member1161907014t_char member563141460on_val member808015754on_val member88670778on_val typeSa807100911_sconf hAPP_f1849790461on_val hAPP_f1727192346on_val fAss_list_char fAcc_list_char hAPP_e1659493427on_val hAPP_P604205461on_val hAPP_P1870962205on_val hAPP_P1886180715on_val red hconf_97414254t_char lconf_496643946t_char hAPP_f1213370163y_bool hAPP_f2060496320y_bool hp hAPP_P1071727823t_char hAPP_P1657265855t_char hAPP_P1875010047on_val hAPP_P330218428on_val hAPP_P1668407995t_char hAPP_P1220989409t_char hAPP_P1859316965t_char hAPP_P1333668416t_char hAPP_P719127871t_char hAPP_P1539798428t_char hAPP_P2015431471on_val hAPP_P1758592847on_val hAPP_P2077211775on_val hAPP_P1486793863on_val hAPP_P265246237on_val hAPP_P291613419on_val hAPP_P1526035745on_val hAPP_P658340954on_val hAPP_l1275479261on_val hAPP_P1963616220on_val hAPP_l1873467853t_char hAPP_P767818445t_char hAPP_l14371579t_char hAPP_P1392904962t_char hAPP_l1859255743t_char hAPP_e1752110927t_char hAPP_l1786340417on_val hAPP_f900686428on_val hAPP_l208357873t_char hAPP_l2100324114t_char map_ad325961431ar_val transi2024712006on_val hAPP_f2121594859l_bool hAPP_f1175813647l_bool while_list_char 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 cond_list_char hAPP_P663876415r_bool hAPP_f39862969r_bool hAPP_P416784693l_bool hAPP_f834198659l_bool hAPP_P357098431r_bool hAPP_f523402917r_bool hAPP_P1214880255r_bool hAPP_f1377529935r_bool hAPP_P1928969845r_bool hAPP_f655949763r_bool hAPP_P220718911l_bool hAPP_f1600283417l_bool hAPP_P2062527807l_bool hAPP_f1363805417l_bool hAPP_P1988153107l_bool hAPP_f662143077l_bool hAPP_P1116729363l_bool hAPP_f635218277l_bool hAPP_e1833980889l_bool hAPP_f1930574389l_bool hAPP_P1183008383l_bool hAPP_f1525114763l_bool hAPP_l146377954l_bool hAPP_f1634841927l_bool hAPP_l217977712r_bool hAPP_f1613448899r_bool hAPP_l1987619678r_bool hAPP_f102021095r_bool hAPP_l1062423959r_bool hAPP_f1697332217r_bool hAPP_l465799708l_bool hAPP_f1443410953l_bool hAPP_l1361600383r_bool hAPP_f2132060507r_bool hAPP_b589554111l_bool hAPP_f1861125939r_bool hAPP_f336522659r_bool hAPP_f1818217r_bool hAPP_f10956301l_bool hAPP_f1399435963l_bool hAPP_f624730965l_bool hAPP_f1593659251r_bool hAPP_f1334304147r_bool hAPP_f777111705r_bool hAPP_f2067364339r_bool hAPP_f897748257r_bool hAPP_f113541543r_bool hAPP_f1897969075r_bool hAPP_f146587157r_bool hAPP_f177037909r_bool hAPP_f1308714617l_bool hAPP_f95792151l_bool hAPP_f1212701859l_bool hAPP_f1359168307l_bool hAPP_f1219198883l_bool hAPP_f855183977l_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 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_f1679543815on_val hAPP_P214139537on_val hAPP_f106757449r_bool hAPP_f1165187701r_bool hAPP_f1339377933r_bool hAPP_f505735499on_val hAPP_P216502748on_val hAPP_f1346522053r_bool hAPP_f918235057r_bool hAPP_f1944156365r_bool hAPP_f2030092415on_val hAPP_P94592612on_val hAPP_f1096084527r_bool hAPP_f1691034591r_bool hAPP_f829041291r_bool hAPP_f797861231on_val hAPP_P1892658174on_val hAPP_f1825030711l_bool hAPP_f219814819l_bool hAPP_f896993613l_bool hAPP_f599509029on_val hAPP_P931655063on_val hAPP_f2131288811l_bool hAPP_f1779944471l_bool hAPP_f1909521165l_bool hAPP_f1520199827on_val hAPP_P789556885on_val hAPP_f516738477l_bool hAPP_f653692369l_bool hAPP_f394183983on_val hAPP_P1760219823on_val hAPP_f881985847l_bool hAPP_f1438732387l_bool hAPP_f1241216909l_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_f2116844091t_char hAPP_P1871645065t_char hAPP_f737797743l_bool hAPP_f154583625l_bool hAPP_f1576637933l_bool hAPP_f1401070501t_char hAPP_P616991870t_char hAPP_f962366127l_bool hAPP_f1331093087l_bool hAPP_f1121261496l_bool hAPP_f314126729t_char hAPP_P1849522950t_char hAPP_f764883801l_bool hAPP_f2012169497l_bool hAPP_f1089411340l_bool hAPP_f1027788897on_val hAPP_f1000925999l_bool hAPP_f1538372259l_bool hAPP_f556306650l_bool hAPP_f1239545903on_val hAPP_P963849987on_val hAPP_f28987375l_bool hAPP_f924423253l_bool hAPP_f1505175539l_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_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_f757259503l_bool hAPP_f2063458791l_bool hAPP_f1255886347l_bool hAPP_f1121083449l_bool hAPP_f1060117847l_bool hAPP_f1455553822l_bool hAPP_f1090377327r_bool hAPP_f2039744637r_bool hAPP_f459877466r_bool hAPP_f968085945r_bool hAPP_f770993243r_bool hAPP_f1371969732r_bool hAPP_f1672439075r_bool hAPP_f166702051r_bool hAPP_f1345728193r_bool hAPP_f1046102489l_bool hAPP_f1136596083l_bool hAPP_f21084934l_bool hAPP_f775361359r_bool hAPP_f737710471r_bool hAPP_f1633332187r_bool transi1095029602t_char transi61620055on_val transi1789604888t_char transi1257872013t_char transi122195895t_char transi208336786on_val transi910771962on_val transi921647814on_val transi1395422419t_char transi374442731on_val hAPP_v834067052t_char throw_list_char bool binOp_list_char tryCatch_list_char cast_list_char call_list_char reds seq_list_char cons_exp_list_char redsp map_va1934808527t_char append_exp_list_char cons_ty redp addr_of_sys_xcpt addr default_val eval evals hAPP_l2138409430r_bool hAPP_l2054741776r_bool block_list_char lAss_list_char cons_list_char cons_val blocks the_Addr hAPP_l512744617ion_ty some_ty hAPP_n546249108on_val some_P948696889on_val hAPP_P2094403585on_val some_val hAPP_f1371002581r_bool hAPP_f2093707285r_bool hAPP_f1074020887l_bool hAPP_f1104067989r_bool hAPP_f332734435r_bool hAPP_f1803975093l_bool hAPP_f660690413r_bool hAPP_f1675531861r_bool hAPP_f181262431l_bool hAPP_f603925568l_bool hAPP_f1326058377l_bool hAPP_f338074126t_char hAPP_f1468279871l_bool hAPP_f1555843780t_char hAPP_f1645102644l_bool hAPP_f1911830329t_char hAPP_f749256120r_bool hAPP_f1937467848l_bool hAPP_f2106552235on_val hAPP_f1145256474l_bool hAPP_f1212990632l_bool hAPP_f848628235t_char hAPP_f781588360l_bool hAPP_f2134824737l_bool hAPP_f1866631480r_bool hAPP_f1742268533r_bool hAPP_l80874262on_val hAPP_f716957699r_bool hAPP_e1410803407on_val hAPP_f926562337l_bool hAPP_f1617787571l_bool hAPP_f1008932791l_bool hAPP_f1279517141l_bool hAPP_f1915623807r_bool hAPP_f1492320500l_bool hAPP_l867549837on_val hAPP_f1261046903l_bool hAPP_f998724171on_val hAPP_f1957179113r_bool hAPP_f318082871l_bool hAPP_f1926378906on_val hAPP_l1870161525on_val hAPP_f502623122l_bool hAPP_f637291415on_val hAPP_f1628326017t_char hAPP_f1297079863t_char hAPP_f157410348t_char hAPP_l1004879342on_val hAPP_f1614126606on_val hAPP_f78832750t_char hAPP_l221195696on_val hAPP_f1301559543l_bool hAPP_P1776198677on_val hAPP_l451552092on_val hAPP_f489055607l_bool hAPP_f1712766199l_bool hAPP_f552081564l_bool hAPP_f1540354981l_bool hAPP_f1840640125on_val hAPP_f336970122on_val hAPP_f524589473l_bool hAPP_f602593190on_val hAPP_f1546656185l_bool hAPP_f1416324670on_val hAPP_e108155315on_val hAPP_l1012006762on_val hAPP_f204771371l_bool hAPP_f600512025on_val hAPP_f1800436403l_bool hAPP_f865889457on_val hAPP_P2083594489on_val hAPP_P308812685on_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 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 skf294 skf295 skf296 skf297 skf298 skf299 skf300 skf301 skf302 skf303 skf304 skf305 skf306 skf307 skf308 skf309 skf310 skf311 skf312 skf313 skf314 skf315 skf316 skf317 skf318 skf319 skf320 skf321 skf322 skf323 skf324 skf325 skf326 skf327 skf328 skf329 skf330 skf331 skf332 skf333 skf334 skf335 skf336 skf337 skf338 skf339 skf340 skf341 skf342 skf343 skf344 skf345 skf346 skf347 skf348 skf349 skf350 skf351 skf352 skf353 skf354 skf355 skf356 skf357 skf358 skf359 skf360 skf361 skf362 skf363 skf364 skf365 skf366 skf367 skf368 skf369 skf370 skf371 skf372 skf373 skf374 skf375 skf376 skf377 skf378 skf379 skf380 skf381 skf382 skf383 skf384 skf385 skf386 skf387 skf388 skf389 skf390 skf391 skf392 skf393 skf394 skf395 skf396 skf397 skf398 skf399 skf400 skf401 skf402 skf403 skf404 skf405 skf406 skf407 skf408 skf409 skf410 skf411 skf412 skf413 skf414 skf415 skf416 skf417 skf418 skf419 skf420 skf421 skf422 skf423 skf424 skf425 skf426 skf427 skf428 skf429 skf430 skf431 skf432 skf433 skf434 skf435 skf436 skf437 skf438 skf439 skf440 skf441 skf442 skf443 skf444 skf445 skf446 skf447 skf448 skf449 skf450 skf451 skf452 skf453 skf454 skf455 skf456 skf457 skf458 skf459 skf460 skf461 skf462 skf463 skf464 skf465 skf466 skf467 skf468 skf469 skf470 skf471 skf472 skf473 skf474 skf475 skf476 skf477 skf478 skf479 skf480 skf481 skf482 skf483 skf484 skf485 skf486 skf487 skf488 skf489 skf490 skf491 skf492 skf493 skf494 skf495 skf496 skf497 skf498 skf499 skf500 skf501 skf502 skf503 skf504 skf505 skf506 skf507 skf508 skf509 skf510 skf511 skf512 skf513 skf514 skf515 skf516 skf517 skf518 skf519 skf520 skf521 skf522 skf523 skf524 skf525 skf526 skf527 skf528 skf529 skf530 skf531 skf532 skf533 skf534 skf535 skf536 skf537 skf538 skf539 skf540 skf541 skf542 skf543 skf544 skf545 skf546 skf547 skf548 skf549 skf550 skf551 skf552 skf553 skf554 skf555 skf556 skf557 skf558 skf559 skf560 skf561 skf562 skf563 skf564 skf565 skf566 skf567 skf568 skf569 skf570 skf571 skf572 skf573 skf574 skf575 skf576 skf577 skf578 skf579 skf580 skf581 skf582 skf583 skf584 skf585 skf586 skf587 skf588 skf589 skf590 skf591 skf592 skf593 skf594 skf595 skf596 skf597 skf598 skf599 skf600 skf601 skf602 skf603 skf604 skf605 skf606 skf607 % 0.59/0.64 Problem Properties: % 0.59/0.64 This is a full first-order problem with equality. % 0.59/0.64 SZS status GaveUp % 0.59/0.64 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.59/0.64 %------------------------------------------------------------------------------