%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW470+3 : 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 : n028.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:18 PM UTC 2026 % Result : Unknown 0.71s 0.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470+3 : TPTP v9.2.1. Released v5.3.0. % 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n028.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:31 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.71/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.67 Execution normal ended with status: gaveup % 0.71/0.67 Execution resolution_1 ended with status: gaveup % 0.71/0.67 Execution resolution_2 ended with status: gaveup % 0.71/0.67 Execution resolution_3 ended with status: gaveup % 0.71/0.67 Execution lmodel_grow ended with status: gaveup % 0.71/0.67 No successful execution. % 0.71/0.67 % 0.71/0.67 Input Clauses: % 0.71/0.68 % 0.71/0.68 Predicates: is_bool hBOOL = is_vname ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 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 ren1100 ren1101 ren1102 ren1103 ren1104 ren1105 ren1106 ren1107 ren1108 ren1109 ren1110 ren1111 ren1112 ren1113 ren1114 ren1115 ren1116 ren1117 ren1118 ren1119 ren1120 ren1121 ren1122 ren1123 ren1124 ren1125 ren1126 ren1127 ren1128 ren1129 ren1130 ren1131 ren1132 ren1133 ren1134 ren1135 ren1136 ren1137 ren1138 ren1139 ren1140 ren1141 ren1142 ren1143 ren1144 ren1145 ren1146 ren1147 ren1148 ren1149 ren1150 ren1151 ren1152 ren1153 ren1154 ren1155 ren1156 ren1157 ren1158 ren1159 ren1160 ren1161 ren1162 ren1163 ren1164 ren1165 ren1166 ren1167 ren1168 ren1169 ren1170 ren1171 ren1172 ren1173 ren1174 ren1175 ren1176 ren1177 ren1178 ren1179 ren1180 ren1181 ren1182 ren1183 ren1184 ren1185 % 0.71/0.68 Fol Constants: bot_bot_bool fFalse fTrue bot_bo797238721a_bool insert956547291iple_a cOMBC_41962815e_bool cOMBB_1348041619bool_a cOMBC_231445413l_bool cOMBB_1355796797bool_a cOMBB_188601460_state fconj cOMBK_1458035955bool_a cOMBC_2027030106e_bool fequal_state member_nat insert_nat member1797258804iple_a member_int insert_int bot_bot_fun_nat_bool bot_bot_fun_int_bool collect_nat fequal_nat collec351493750iple_a fequal963300192iple_a collect_int fequal_int cOMBC_nat_nat_bool cOMBC_1940896922a_bool cOMBC_int_int_bool cOMBS_nat_bool_bool cOMBB_1015721476ol_nat cOMBS_154988028l_bool cOMBB_1866391387iple_a cOMBS_int_bool_bool cOMBB_1652995168ol_int cOMBK_235286536iple_a cOMBK_bool_int cOMBK_bool_nat fimplies cOMBB_bool_bool_nat fNot cOMBB_1882975613iple_a cOMBB_bool_bool_int fdisj cOMBC_226598744l_bool cOMBC_1519416966l_bool cOMBC_94739984l_bool the_elem_nat the_el1519802624iple_a the_elem_int skip the_nat cOMBB_955900739ol_nat fequal_fun_nat_bool cOMBC_178881787t_bool the_Ho830102290iple_a cOMBB_1610959875iple_a fequal874423448a_bool cOMBC_1570214144a_bool the_int cOMBB_1418110531ol_int fequal_fun_int_bool cOMBC_1683390479t_bool cOMBC_524597097e_bool cOMBB_2139825703bool_a cOMBB_844853809_state cOMBS_777315357_state cOMBC_1193272608_state update cOMBK_1028443109iple_a cOMBK_nat_int cOMBK_2052406350iple_a cOMBK_int_int cOMBK_nat_nat cOMBK_int_nat cOMBB_nat_int_int cOMBB_int_int_nat cOMBI_int cOMBI_1301683934iple_a cOMBI_nat cOMBK_1007576201iple_a finite_finite_nat finite1738664244iple_a finite_finite_int cOMBB_683172471iple_a cOMBC_364739t_bool cOMBB_1391527205iple_a cOMBC_int_nat_bool cOMBB_1437810218ol_int cOMBC_1530706207t_bool cOMBB_1505691757iple_a cOMBC_533513393a_bool cOMBB_1063143712ol_nat cOMBB_118231410ol_int cOMBC_1719122773a_bool cOMBB_1700417404ol_int cOMBB_800536526ol_nat cOMBC_nat_int_bool cOMBB_1628441366ol_nat minus_2067140911t_bool minus_85316870a_bool minus_1449998731t_bool times_times_nat times_times_int minus_minus_bool cOMBB_1654519265ol_nat cOMBC_646315179t_bool cOMBB_1176122337iple_a cOMBC_288844080a_bool cOMBB_765314529ol_int cOMBC_922884543t_bool big_co1024481617at_int minus_minus_int big_co1977834938_a_int big_co230513141nt_int big_co387207925at_nat cOMBC_1505178355ol_nat cOMBB_1453893592at_nat big_co1740723097nt_nat cOMBC_462113011ol_nat cOMBB_1562322300at_int cOMBC_nat_int_nat cOMBC_2036134968ol_nat cOMBB_1716606670at_nat big_co1340561246_a_nat cOMBC_1159891896ol_nat cOMBB_10565751iple_a cOMBC_441305270_a_nat cOMBC_int_nat_nat cOMBC_667342884at_nat cOMBC_1218031117nt_nat cOMBB_737513486at_nat cOMBB_nat_nat_int cOMBB_963856155at_nat cOMBC_309106125_a_nat cOMBB_2005430478at_nat cOMBB_1250632933iple_a cOMBC_1294079849at_nat cOMBB_891709290at_int cOMBB_nat_nat_nat cOMBB_1601129847at_int cOMBC_1038836708at_nat cOMBB_1672982117iple_a cOMBB_789959282iple_a cOMBC_nat_nat_nat cOMBS_1756972052at_nat cOMBS_1600277268nt_int cOMBB_1885471694iple_a minus_minus_nat the_fun_int_bool the_fu1555441254a_bool the_fun_nat_bool cOMBB_161916371at_nat cOMBB_391046962ol_nat cOMBB_1381347800at_nat cOMBB_2101530536ol_nat cOMBB_1107515603iple_a cOMBB_437532599iple_a cOMBB_2018621492at_int cOMBB_591320580ol_int cOMBB_1357028143iple_a cOMBB_1870764287iple_a cOMBB_1125113304at_int cOMBB_1746576572ol_int cOMBS_1063588099ol_nat cOMBS_2106653443ol_nat cOMBS_397915080ol_nat cOMBS_1274158152ol_nat cOMBS_1333400172ol_nat cOMBB_1075417391iple_a cOMBS_202713324ol_nat cOMBB_206396714at_int cOMBC_2020858056nt_nat cOMBB_1028320654ol_int cOMBS_1999073191ol_nat cOMBB_2091167284at_int cOMBC_int_int_nat cOMBC_1917249810_a_nat plus_plus_nat plus_plus_int cOMBS_nat_nat_nat cOMBS_int_nat_nat ord_lessThan_nat ord_lessThan_int ord_le1523781517a_bool ord_le951220754t_bool ord_le1568362934t_bool ord_less_eq_int ord_less_eq_nat finite268574148a_bool collec999179778a_bool cOMBC_627599030l_bool finite1395289673t_bool collect_fun_int_bool cOMBC_605892544l_bool finite2012431853t_bool collect_fun_nat_bool cOMBC_1693257480l_bool ord_less_eq_bool bot_bot_nat ord_min_int ord_min_nat big_linorder_Min_int big_linorder_Min_nat big_linorder_Max_int big_linorder_Max_nat ord_max_nat finite_card_nat one_one_nat semiri1621563631at_int one_one_int uminus_uminus_int ord_less_nat power_power_nat power_power_int ord_less_int ord_le382113706t_bool ord_le1912455174t_bool finite_card_int zero_zero_nat zero_zero_int cOMBK_bool_state cOMBB_160679318_state cOMBS_1378840469l_bool cOMBC_892787026e_bool cOMBB_145932198bool_a g c p b skc1137 skc1138 skc1139 skc1140 % 0.71/0.68 Fol Functions: big_se1603268663iple_a big_se913005884ig_int big_se275732192ig_nat finite1428139793iple_a finite2114894759a_bool finite1973466193nt_int finite1321096241t_bool finite2130160977at_nat finite1071749497t_bool finite648855052iple_a finite1803123436a_bool finite1704255308nt_int finite58652534t_bool finite1860950092at_nat finite1956789438t_bool finite1753440478iple_a finite1626084323ne_int finite988810631ne_nat finite1033474011iple_a finite1432773856em_int finite795500164em_nat hAPP_state_bool hAPP_bool_bool hAPP_H1037229737a_bool hAPP_int_bool hAPP_nat_bool hAPP_f1695230391l_bool hAPP_f448129468l_bool hAPP_f54304608l_bool hAPP_f2110825313l_bool hAPP_f215623910l_bool hAPP_f1637334154l_bool hoare_2102800559rivs_a hoare_1916936827iple_a hAPP_H1743777351a_bool hAPP_f20753329a_bool hAPP_f1006724181e_bool hAPP_f1561913689l_bool hAPP_f1178339559l_bool hAPP_f1509969235l_bool hAPP_f340725611e_bool hAPP_f1824947087e_bool hAPP_b540892988e_bool hAPP_a2036067514e_bool hAPP_f817621513e_bool hAPP_s1806633685e_bool hAPP_f762886889e_bool hAPP_n215258509l_bool hAPP_n1512601776t_bool hAPP_f800510211t_bool hAPP_H622608077l_bool hAPP_i2112223885l_bool hAPP_i1529485324t_bool hAPP_f1805168059t_bool hAPP_n1699378549t_bool hAPP_H426895267a_bool hAPP_i1948725293t_bool hAPP_f229349961t_bool hAPP_f920293029a_bool hAPP_f428220345t_bool hAPP_f1080886329l_bool hAPP_f1146629647l_bool hAPP_f561022312t_bool hAPP_f239971723l_bool hAPP_f146754017l_bool hAPP_f607497069a_bool hAPP_f1734373249l_bool hAPP_f2144054103l_bool hAPP_f727283836t_bool hAPP_b1882817719a_bool hAPP_b396694332t_bool hAPP_b1013836512t_bool hAPP_f894608603t_bool hAPP_f604201481a_bool hAPP_f627970963t_bool hAPP_f1722879237t_bool hAPP_f247708275a_bool hAPP_f202917053t_bool hAPP_f22106695ol_nat hAPP_f1693662087iple_a hAPP_f1594865479ol_int semi hAPP_f103356543l_bool hAPP_f1777703707t_bool hAPP_f688831301t_bool hAPP_f1570313510t_bool hAPP_f158894502t_bool hAPP_f1767618879l_bool hAPP_f1697223433a_bool hAPP_f571476211a_bool hAPP_f1181346091a_bool hAPP_f1194757675a_bool hAPP_f284875647l_bool hAPP_f423804115t_bool hAPP_f472159229t_bool hAPP_f1048215610t_bool hAPP_f2119767738t_bool finite_fold1Set_nat finite1621280049iple_a finite_fold1Set_int hAPP_f635443597e_bool hAPP_f1406200875e_bool hAPP_f1460451647e_bool hAPP_f1542232213_state hAPP_v365393659_state hAPP_f851239890_state hAPP_f871651461_state hAPP_f100967412e_bool ass finite_fold1_nat finite1465856449iple_a finite_fold1_int hAPP_n1653940209_a_nat image_48635758_a_nat hAPP_nat_fun_int_nat image_int_nat hAPP_H2085992369iple_a image_533441733iple_a hAPP_int_fun_int_int image_int_int hAPP_nat_fun_nat_nat image_nat_nat hAPP_int_fun_nat_int image_nat_int hAPP_H905846293iple_a hAPP_n261501868iple_a image_1865589340iple_a hAPP_i240634960iple_a image_1844722432iple_a hAPP_H592031934_a_nat hAPP_int_int hAPP_H1229305626_a_int image_685909450_a_int hAPP_nat_nat hAPP_nat_int hAPP_f1673907925nt_int hAPP_f147134065nt_int hAPP_f1431025877at_int hAPP_f1139079189at_int hAPP_int_nat hAPP_i1475897073_a_int hAPP_b589554111l_bool finite929467206at_nat finite90892550iple_a finite772772422nt_int hAPP_f1786170683a_bool hAPP_f960023481a_bool hAPP_f1981448543t_bool hAPP_f1872860171t_bool hAPP_f228417655a_bool hAPP_n1919155532a_bool hAPP_f2026117279t_bool hAPP_f876579787t_bool hAPP_f175561985t_bool hAPP_n1082236369t_bool hAPP_f1329415375t_bool hAPP_f2142913731t_bool hAPP_f920351535a_bool hAPP_i611776424a_bool hAPP_f1930382715a_bool hAPP_f260875897a_bool hAPP_f1886543991t_bool hAPP_H144868812t_bool hAPP_f1399575567t_bool hAPP_f1791153283t_bool hAPP_f1421841531a_bool hAPP_f298605433a_bool hAPP_f936407855t_bool hAPP_H1675210280t_bool hAPP_f1505651103t_bool hAPP_f618557131t_bool hAPP_f879109391t_bool hAPP_f1533130627t_bool hAPP_f482008321t_bool hAPP_i418383825t_bool hAPP_f1730770594t_bool hAPP_f1706700729a_bool hAPP_f1223193598t_bool hAPP_f1311642927t_bool hAPP_f1115950719t_bool hAPP_f10625010t_bool hAPP_f957014749a_bool hAPP_f615286271a_bool hAPP_f550111323a_bool hAPP_f194616807t_bool hAPP_f1596157055t_bool hAPP_f1468280982t_bool hAPP_f1599440987ol_int hAPP_f659380387ol_int hAPP_f1544320301ol_int hAPP_f587450508ol_int hAPP_f1926459811ol_int big_co1705425894at_nat big_co1815942735_a_nat hAPP_f2097660464ol_nat big_co911457418nt_nat hAPP_f957591787ol_nat big_co195215938at_int big_co305732779_a_int big_co1548731110nt_int finite1578363458t_bool finite1215486064a_bool finite1827710202t_bool finite1205970312iple_a finite_fold_nat_nat finite_fold_int_int hAPP_f1632710027ol_nat hAPP_f299305025ol_nat hAPP_f630508183at_nat hAPP_f1473602334at_nat hAPP_f782000547ol_nat hAPP_f1029311995ol_nat hAPP_f446977493at_nat hAPP_f1501159417ol_nat hAPP_f261731407nt_nat hAPP_f787214110nt_nat hAPP_f1109019371ol_nat hAPP_f424754463ol_nat hAPP_f883871819ol_nat hAPP_f870149665at_nat hAPP_f2122367971at_nat hAPP_f1073041467ol_nat hAPP_f2146713109at_nat hAPP_f1669765561ol_nat hAPP_f1012303887_a_nat hAPP_f1464798435_a_nat hAPP_f1371399797ol_nat hAPP_f879494613nt_nat hAPP_f1903462933_a_nat finite1008073724t_bool hAPP_f1634429330l_bool finite1152845682a_bool hAPP_f1577095245l_bool finite758726980t_bool hAPP_f1266913334l_bool hAPP_f1701814485nt_nat hAPP_f1731313045at_nat hAPP_f1639111240at_nat hAPP_f2080483477nt_nat hAPP_f1633513941nt_nat hAPP_f237327688nt_nat hAPP_f2006236373_a_nat hAPP_f1485673429_a_nat hAPP_f145529813_a_nat hAPP_f1393576712_a_nat hAPP_f1315855317at_nat hAPP_f1087393429at_nat hAPP_f1463450952at_nat hAPP_f1033905301at_nat hAPP_f701299925at_nat hAPP_f1169617132at_nat hAPP_f481016213at_nat hAPP_f703420885at_nat hAPP_f429024520at_nat hAPP_f1879857877at_nat hAPP_f388255893at_nat hAPP_f221335601at_nat hAPP_f416620757at_nat hAPP_f1585078997at_nat hAPP_f1914919701at_nat hAPP_f901215189nt_nat hAPP_f2132704789nt_nat hAPP_f500900629_a_nat hAPP_f106743253_a_nat hAPP_f1418102009_a_nat hAPP_f1621780181nt_int hAPP_f231878828nt_int hAPP_f789902073_a_int hAPP_f1561000661_a_int hAPP_f631471077t_bool hAPP_f258822235a_bool hAPP_f582319405t_bool hAPP_f724467227at_nat hAPP_f1396758363a_bool hAPP_f2087582327a_bool hAPP_f966999552at_nat hAPP_f109563153at_nat hAPP_f1986088027t_bool hAPP_f2022049025t_bool hAPP_f389300155at_nat hAPP_f734830747_a_nat hAPP_f196067081t_bool hAPP_f27379319t_bool hAPP_f2085403241_a_nat hAPP_f2100446809nt_nat hAPP_f654702867t_bool hAPP_f1134349059nt_nat hAPP_f575660003_a_nat hAPP_f1998609161t_bool hAPP_f138254639t_bool hAPP_f342603021_a_nat hAPP_f1964560145nt_nat hAPP_f1410409747t_bool hAPP_f783004929t_bool hAPP_f1161717855nt_nat hAPP_f369809936nt_nat hAPP_f1750007732at_nat hAPP_f1052116629_a_nat hAPP_f264818750at_nat hAPP_f543861963ol_nat hAPP_f224922881ol_nat hAPP_f270087133_a_nat hAPP_f1072896543ol_nat hAPP_f183615253_a_nat hAPP_f1442126667ol_nat hAPP_f1895921634nt_nat hAPP_f481410067a_bool hAPP_f1718504751a_bool hAPP_f2050777416nt_nat hAPP_f1331458699ol_nat hAPP_f1548925761ol_nat hAPP_f446447448nt_nat hAPP_f909851349nt_nat hAPP_f1451619093nt_nat hAPP_f1408247010at_nat hAPP_f1399363134nt_nat hAPP_f2100528361l_bool hAPP_f396832789l_bool hAPP_f1399552105l_bool hAPP_f1948010709l_bool hAPP_f643944041l_bool hAPP_f1246832597l_bool partial_flat_lub_int partia1949573335iple_a partial_flat_lub_nat ord_at238088361st_nat ord_at875362053st_int if_nat ord_gr375877188st_nat hAPP_b2019457360e_bool hAPP_int_fun_int_nat hAPP_int_fun_nat_nat hAPP_i68813070l_bool hAPP_n1006566506l_bool hAPP_f2073279419e_bool hAPP_f1759915619e_bool hAPP_f167292325e_bool hAPP_s58564346l_bool hAPP_f644196280e_bool hAPP_state_state hAPP_s1892499976_state hAPP_state_nat hAPP_nat_state hAPP_f162060345e_bool hAPP_f746301080e_bool hAPP_a723219176e_bool hAPP_i1530422220ol_nat hAPP_n259507732ol_nat hAPP_i318423664ol_nat hAPP_f1259673775l_bool hAPP_s712361723_state hAPP_v594194232_state hAPP_i1313984149_a_nat hAPP_H978941973nt_nat hAPP_H1772910449at_nat hAPP_H1140854897nt_int hAPP_H2130837971l_bool hAPP_f1261923407e_bool hAPP_a1200519163e_bool hAPP_a1224971408e_bool hAPP_i1876697324at_nat hAPP_n74706760nt_nat hAPP_H1993634375ol_nat hAPP_n130255193ol_nat hAPP_H781635819ol_nat hAPP_i51375541ol_nat hAPP_a849909144l_bool hAPP_H1651200817at_nat hAPP_f375255701e_bool hAPP_f963367678e_bool hAPP_n352002696_a_nat skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 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 skf1100 skf1101 skf1102 skf1103 skf1104 skf1105 skf1106 skf1107 skf1108 skf1109 skf1110 skf1111 skf1112 skf1113 skf1114 skf1115 skf1116 skf1117 skf1118 skf1119 skf1120 skf1121 skf1122 skf1123 skf1124 skf1125 skf1126 skf1127 skf1128 skf1129 skf1130 skf1131 skf1132 skf1133 skf1134 skf1135 skf1136 skf1141 skf1142 skf1143 skf1144 skf1145 skf1146 skf1147 skf1148 skf1149 skf1150 skf1151 skf1152 skf1153 skf1154 skf1155 skf1156 skf1157 skf1158 skf1159 skf1160 skf1161 skf1162 skf1163 skf1164 skf1165 skf1166 skf1167 skf1168 skf1169 skf1170 skf1171 skf1172 skf1173 skf1174 skf1175 skf1176 skf1177 skf1178 skf1179 skf1180 skf1181 skf1182 skf1183 skf1184 skf1185 skf1186 skf1187 skf1188 skf1189 skf1190 skf1191 skf1192 skf1193 skf1194 skf1195 skf1196 skf1197 skf1198 skf1199 skf1200 skf1201 skf1202 skf1203 skf1204 skf1205 skf1206 skf1207 skf1208 skf1209 skf1210 skf1211 skf1212 skf1213 skf1214 skf1215 skf1216 skf1217 skf1218 skf1219 skf1220 skf1221 skf1222 skf1223 skf1224 skf1225 skf1226 skf1227 skf1228 % 0.71/0.68 Problem Properties: % 0.71/0.68 This is a full first-order problem with equality. % 0.71/0.68 SZS status GaveUp % 0.71/0.68 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.71/0.68 %------------------------------------------------------------------------------