%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW471+3 : 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 : n001.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:19 PM UTC 2026 % Result : Unknown 0.69s 0.71s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW471+3 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n001.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 13:36:04 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.36/0.69 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.69 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.69 Execution normal ended with status: gaveup % 0.36/0.69 Execution resolution_1 ended with status: gaveup % 0.36/0.69 Execution resolution_2 ended with status: gaveup % 0.36/0.69 Execution resolution_3 ended with status: gaveup % 0.36/0.69 Execution lmodel_grow ended with status: gaveup % 0.36/0.69 No successful execution. % 0.36/0.69 % 0.36/0.69 Input Clauses: % 0.69/0.70 % 0.69/0.70 Predicates: is_bool is_fun1661590463l_bool is_pname is_fun_pname_bool is_fun_bool_bool = hBOOL 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 ren1186 ren1187 ren1188 ren1189 ren1190 ren1191 ren1192 ren1193 ren1194 ren1195 ren1196 ren1197 ren1198 ren1199 ren1200 ren1201 ren1202 ren1203 ren1204 ren1205 ren1206 ren1207 ren1208 ren1209 ren1210 ren1211 ren1212 ren1213 ren1214 ren1215 ren1216 ren1217 ren1218 ren1219 ren1220 ren1221 ren1222 ren1223 ren1224 ren1225 ren1226 ren1227 ren1228 ren1229 % 0.69/0.70 Fol Constants: finite_finite_pname pname bool bot_bot_bool bot_bo844097828e_bool bot_bo806936373l_bool bot_bo1649642514l_bool fFalse fNot fTrue procs hoare_1916936827iple_a hoare_1191504582_state member1667945571_state hoare_446535894_state member1797258804iple_a hoare_2056833131alid_a semila176469292e_bool cOMBS_1524960158_state cOMBS_1020065803_state body the_com body_1 semila1114547555a_bool cOMBS_343917116iple_a cOMBS_839225263iple_a member_nat semila465093516t_bool member769771716a_bool semila834425101l_bool member_pname semila278973382e_bool semila1168014441p_bool semila972727038up_nat collec999179778a_bool cOMBS_824156748l_bool fdisj cOMBC_996544418l_bool collec637225377_state cOMBS_865875691l_bool cOMBC_538205282l_bool collec351493750iple_a cOMBS_154988028l_bool cOMBC_1519416966l_bool collect_nat cOMBS_nat_bool_bool cOMBC_226598744l_bool collect_pname cOMBS_568398431l_bool cOMBC_1058051404l_bool cOMBI_nat suc insert1744391420_state bot_bo784226126e_bool insert956547291iple_a bot_bo797238721a_bool zero_zero_nat bot_bot_fun_nat_bool bot_bo332163887l_bool insert_nat insert1421434205a_bool insert_pname cOMBK_bool_pname cOMBK_235286536iple_a cOMBK_404565488a_bool cOMBK_988866959_state cOMBK_bool_nat fequal874423448a_bool fequal_pname fequal963300192iple_a fequal1440809015_state fequal_nat cOMBC_627599030l_bool cOMBC_1149511130e_bool cOMBC_1940896922a_bool cOMBC_1967329268e_bool cOMBC_nat_nat_bool fconj fimplies cOMBK_nat_nat cOMBK_2086841362_pname cOMBK_523903665_pname cOMBK_nat_pname cOMBK_1667642481_pname cOMBK_pname_pname cOMBC_41962815e_bool cOMBC_231445413l_bool cOMBC_471052088e_bool cOMBK_1458035955bool_a cOMBC_2027030106e_bool fequal_state cOMBK_631994958_state size_s399404919iple_a size_s255495008_state the_elem_nat the_el979963640a_bool the_elem_pname the_el1519802624iple_a the_el2080696983_state bot_bot_nat skip cOMBC_892787026e_bool cOMBS_1378840469l_bool cOMBC_952831051e_bool the_nat fequal_fun_nat_bool cOMBC_178881787t_bool the_fu1555441254a_bool fequal1455900568l_bool cOMBC_1324894996l_bool the_pname fequal533582459e_bool cOMBC_1123258281e_bool the_Ho830102290iple_a cOMBC_1570214144a_bool the_Ho2067184133_state fequal1475827639e_bool cOMBC_1229155955e_bool finite1738664244iple_a cOMBS_1744968921iple_a cOMBS_1597898188iple_a finite268574148a_bool cOMBS_1097875753iple_a cOMBS_1949899292iple_a cOMBS_1860286139_state cOMBS_1436317352_state cOMBS_988488459_state cOMBS_1113512696_state finite_finite_nat cOMBS_1417107330iple_a cOMBS_519355893iple_a cOMBS_1390821348_state cOMBS_183256401_state finite694102371_state cOMBC_594836627t_bool cOMBC_364739t_bool cOMBC_pname_nat_bool cOMBC_533513393a_bool cOMBC_805992879l_bool cOMBC_nat_pname_bool cOMBC_19854728e_bool cOMBC_173670761l_bool cOMBC_1309726071a_bool cOMBC_59067399e_bool cOMBC_288844080a_bool cOMBC_1645572109l_bool cOMBC_1771919087e_bool cOMBC_1584660393a_bool cOMBC_1048264781e_bool cOMBC_2103945827a_bool finite2012431853t_bool bot_bo1701429464l_bool big_la1704749377t_bool semila653644470l_bool finite1823766380l_bool bot_bo156414585l_bool big_la914314008l_bool semila1803437851l_bool finite627955595e_bool bot_bo942947096l_bool big_la1369269047e_bool semila1672697786l_bool finite595471783e_bool big_la841148155e_bool semila1782091504l_bool finite_finite_bool big_la1480321694n_bool semila1866150931l_bool big_la1609103640a_bool big_la43341705in_nat member_fun_nat_bool insert_fun_nat_bool member38210668l_bool insert2046103699l_bool member131361931e_bool insert1720618162e_bool member799430823e_bool insert1325755072e_bool member_bool insert_bool semila753742375l_bool semila1635148844e_bool semila1874263622e_bool semila286921929a_bool semila840543986t_bool minus_98295210l_bool minus_1015773161e_bool minus_85316870a_bool minus_1805465033e_bool minus_2067140911t_bool semila80283416nf_nat minus_minus_bool semila310582991f_bool minus_minus_nat one_one_nat plus_plus_nat size_size_com times_times_nat ord_less_eq_nat finite_card_nat ord_less_nat g p q n skc1231 % 0.69/0.70 Fol Functions: big_co2022808324_pname finite1282449217_pname finite1753440478iple_a finite683959609_state finite988810631ne_nat finite2103247258a_bool finite89670078_pname finite1033474011iple_a finite416071164_state finite795500164em_nat finite927518301a_bool undefined_pname fun undefi17486888e_bool hAPP_pname_pname hAPP_pname_bool hAPP_p61793385e_bool hAPP_p393069232l_bool hAPP_p338031245l_bool hAPP_state_bool hAPP_s58564346l_bool hAPP_bool_bool hAPP_b76515610e_bool hAPP_b589554111l_bool hAPP_H2000557816_pname hAPP_H1037229737a_bool hAPP_H1078816262e_bool hAPP_H2130837971l_bool hAPP_H242767318e_bool hAPP_H1776011827e_bool hAPP_H1270401638l_bool hAPP_nat_pname hAPP_nat_bool hAPP_n1025906991e_bool hAPP_n1006566506l_bool hAPP_f1297739591_pname hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f42430548e_bool hAPP_f387058535l_bool hAPP_f961197973l_bool hAPP_f1764134762_pname hAPP_f1695230391l_bool hAPP_f1216026388e_bool hAPP_f244528453l_bool hAPP_f1378282496l_bool hAPP_f54304608l_bool hAPP_f654413245e_bool hAPP_f1935102916l_bool hAPP_f674760225e_bool hAPP_f559147733l_bool hAPP_f2110825313l_bool hAPP_f147139262e_bool hAPP_f1410040974l_bool hAPP_f1637334154l_bool hAPP_f670355311l_bool hAPP_f1350218798iple_a hAPP_c142510605iple_a hAPP_f233717658iple_a hAPP_f274181323_state hAPP_c27135337_state hAPP_f497755132_state hoare_919241616_state hAPP_H2039996199l_bool hAPP_n1497837059e_bool hoare_293150257lids_a hAPP_H622608077l_bool hAPP_n1919155532a_bool hAPP_f1794460506e_bool cOMBB_2084106034_pname hAPP_f804744487_state hAPP_f1922754332_state hAPP_f460309545_state hAPP_f1811131990_state hAPP_f914896950_state image_185131637_state hAPP_f360545851e_bool hAPP_f806699093e_bool hoare_512830354_state cOMBB_923936821_pname hAPP_f96342628me_com hAPP_f1706700729a_bool cOMBB_2054374575_pname hAPP_f854147694iple_a hAPP_f1559918364iple_a hAPP_f316273229iple_a hAPP_f327379420iple_a hAPP_f961776218iple_a image_1738210978iple_a hAPP_f2034373396a_bool hAPP_f20753329a_bool hoare_2102800559rivs_a hAPP_n215258509l_bool hAPP_f1730770594t_bool hAPP_f800510211t_bool hAPP_f293818473l_bool hAPP_f1340058745l_bool hAPP_f396832789l_bool hAPP_f1388330588e_bool hAPP_nat_nat image_nat_nat hAPP_p1751618853_state hAPP_pname_nat image_pname_nat hAPP_f1066163005t_bool hAPP_p1743421830a_bool image_2016317142a_bool hAPP_f290545180l_bool image_nat_pname image_2037030074_pname image_1244540328_pname hAPP_p346744818iple_a image_48635758_a_nat hAPP_f1968395738t_bool image_2034400499a_bool hAPP_f1767618879l_bool image_1599849618_state hAPP_f101573982e_bool image_1865589340iple_a hAPP_f420957402a_bool image_1153683671iple_a hAPP_f258822235a_bool image_299066104iple_a hAPP_f1029392762a_bool hAPP_nat_fun_nat_nat cOMBB_703864541a_bool hAPP_f754896967l_bool hAPP_f1675405437l_bool hAPP_f288270593l_bool cOMBB_1291456124_state hAPP_f1184122441e_bool hAPP_f832587837l_bool hAPP_f1702629984e_bool cOMBB_1866391387iple_a hAPP_f247708275a_bool hAPP_f146754017l_bool hAPP_f607497069a_bool cOMBB_1015721476ol_nat hAPP_f1722879237t_bool hAPP_f1146629647l_bool hAPP_f561022312t_bool cOMBB_675860798_pname hAPP_f661147897e_bool hAPP_f1402196763l_bool hAPP_f649174806e_bool cOMBB_452540923_pname hAPP_f922567064_state cOMBB_1824120853_pname hAPP_f1273628548iple_a hAPP_p799580910on_com hAPP_option_com_com hAPP_pname_com hAPP_p1637813682e_bool hAPP_H1902130436e_bool hAPP_p635540397e_bool hAPP_H1743777351a_bool evalc hAPP_s1806633685e_bool hAPP_n1512601776t_bool hAPP_f1376242083l_bool hAPP_p905327722e_bool hAPP_b1882817719a_bool hAPP_b83765433l_bool hAPP_b974863576e_bool hAPP_b1013836512t_bool hAPP_H426895267a_bool hAPP_H216526335e_bool hAPP_n1699378549t_bool hAPP_f2100528361l_bool hAPP_f22061361e_bool hAPP_f920293029a_bool hAPP_f1902016361e_bool hAPP_f229349961t_bool cOMBB_193631803a_bool cOMBB_647938656_pname cOMBB_1882975613iple_a cOMBB_325909978_state cOMBB_bool_bool_nat hAPP_H1938877132_state hAPP_H327714446iple_a hAPP_n362732366me_nat hAPP_f624861966a_bool hAPP_p1170154830_pname image_pname_pname cOMBB_1348041619bool_a cOMBB_188601460_state cOMBB_1355796797bool_a hAPP_f1509969235l_bool hAPP_f340725611e_bool hAPP_f1824947087e_bool hAPP_b540892988e_bool cOMBB_1757942702_state cOMBB_1759179140_state hAPP_f1283379615l_bool hAPP_f873506917e_bool hAPP_f701449317e_bool hAPP_b1095269219e_bool hAPP_a2036067514e_bool hAPP_f817621513e_bool hAPP_f762886889e_bool hAPP_f1863945078e_bool hoare_571935964size_a hAPP_H592031934_a_nat hoare_163978021_state hAPP_H175283793te_nat hoare_Mirabelle_MGT hAPP_f22106695ol_nat hAPP_f1693662087iple_a hAPP_f718417177_state evaln cOMBB_145932198bool_a hAPP_f963367678e_bool hAPP_f1261923407e_bool cOMBB_160679318_state hAPP_f1759915619e_bool while cOMBB_20296667_state hAPP_f1138284024e_bool hAPP_f915354021e_bool semi hAPP_f103356543l_bool cOMBB_955900739ol_nat hAPP_f688831301t_bool hAPP_f1570313510t_bool hAPP_f158894502t_bool hAPP_f1303207443l_bool cOMBB_1575464575a_bool hAPP_f254338943l_bool hAPP_f759941367l_bool hAPP_f536631715l_bool cOMBB_530759491_pname hAPP_f698292281e_bool hAPP_f180827860e_bool cOMBB_1610959875iple_a hAPP_f571476211a_bool hAPP_f1181346091a_bool hAPP_f1194757675a_bool hAPP_f849457489l_bool cOMBB_1282391997_state hAPP_f1802364479e_bool hAPP_f874203478e_bool hAPP_f1900156034e_bool hAPP_H1893885264e_bool hAPP_H463278718_a_com cOMBB_1799328076iple_a hAPP_f338450734iple_a hAPP_f51865337iple_a hAPP_f524917645iple_a hAPP_f2004506425iple_a hAPP_f1766326554iple_a image_533441733iple_a hAPP_f477771714e_bool hAPP_f1968907248ol_com cOMBB_1013749676a_bool hAPP_f1787234632iple_a hAPP_f2023640211iple_a hAPP_f159541635iple_a hAPP_f410259831iple_a hAPP_f1255935540iple_a hAPP_H838560847e_bool cOMBB_1269509967iple_a hAPP_f1874377965_state hAPP_f1527065593_state hAPP_f1573424489_state hAPP_f461066925_state hAPP_f1551299824_state hAPP_f1246524253e_bool cOMBB_989249001a_bool hAPP_f868277077_state hAPP_f1151038867_state hAPP_f1235235423_state hAPP_f1784570101_state hAPP_f582141064_state image_821490176_state hAPP_f1513075764e_bool hAPP_n1063102567e_bool hAPP_nat_com cOMBB_1443236341_a_nat hAPP_f1921807086iple_a hAPP_f803745506iple_a hAPP_f1857794253iple_a hAPP_f311800994iple_a hAPP_f817035994iple_a hAPP_n1252169848e_bool cOMBB_1531938296te_nat hAPP_f432895259_state hAPP_f459571426_state hAPP_f1158791849_state hAPP_f1172439208_state hAPP_f634763074_state image_1730813499_state hAPP_f375948533e_bool image_1590538908a_bool hAPP_f1098153174l_bool image_1769043840ol_nat hAPP_f1900748420t_bool cOMBB_85437587a_bool hAPP_f1144745493t_bool hAPP_f1852971749l_bool hAPP_f2097660464ol_nat hAPP_n37219812l_bool cOMBB_1391527205iple_a hAPP_f1872860171t_bool hAPP_f228417655a_bool cOMBB_523834888_pname hAPP_f1358769483t_bool hAPP_f1715247037e_bool cOMBB_800536526ol_nat hAPP_f618557131t_bool cOMBB_1063143712ol_nat hAPP_f260875897a_bool hAPP_f1886543991t_bool hAPP_n261501868iple_a hAPP_H144868812t_bool cOMBB_1370228356ol_nat hAPP_f635381775l_bool hAPP_f2110185157t_bool cOMBB_1212655066ol_nat hAPP_f414474559e_bool hAPP_f998021053t_bool hAPP_p1499970991t_bool cOMBB_181781758_pname hAPP_f472107739e_bool hAPP_f343137017e_bool cOMBB_1363536318_pname hAPP_f1577042203l_bool hAPP_f1415030585e_bool cOMBB_542850580_pname hAPP_f1336811455e_bool cOMBB_1388879450_pname hAPP_f2085416313a_bool hAPP_f421895915e_bool hAPP_H280516760_state hAPP_H574424047_state hAPP_H2085992369iple_a hAPP_H905846293iple_a cOMBB_667059641_pname hAPP_f2028971360e_bool hAPP_f376349141e_bool hAPP_f103229774e_bool finite1443934175_pname hAPP_f447027986e_bool cOMBB_1722563443iple_a hAPP_f181951559a_bool finite1750867337iple_a cOMBB_734913733a_bool hAPP_f2116512939a_bool hAPP_f957014749a_bool finite576419631a_bool hAPP_f1748906467a_bool cOMBB_1141542387ol_nat hAPP_f934069744t_bool finite2098682953ol_nat cOMBB_1467678496ol_nat hAPP_f992030835l_bool hAPP_f1384990677l_bool hAPP_f924569416l_bool finite183661956ol_nat hAPP_f1659318414l_bool cOMBB_1209446585ol_nat hAPP_f446737578e_bool hAPP_f883303749e_bool hAPP_f1501416730e_bool finite491497871ol_nat hAPP_f1319825314e_bool cOMBB_2115959324ol_nat hAPP_f1402630535a_bool hAPP_f816688069a_bool hAPP_f1938783956a_bool finite658192434ol_nat hAPP_f1023496418a_bool cOMBB_1524346879ol_nat hAPP_f953597140e_bool hAPP_f1696618965e_bool hAPP_f1718442376e_bool finite1171393829ol_nat hAPP_f1502860876e_bool cOMBB_1481150806_pname hAPP_f682420871a_bool hAPP_f843217465a_bool finite1174086764_pname hAPP_f490436380a_bool image_696316513a_bool image_661047967_state hAPP_f1234324863a_bool hAPP_f540020688l_bool hAPP_f1246832597l_bool hAPP_f582319405t_bool hAPP_f1120848625l_bool hAPP_f1841260065l_bool hAPP_f2060061063l_bool hAPP_f1847120l_bool hAPP_f734420447l_bool hAPP_f1216288071e_bool hAPP_f230953622l_bool hAPP_f1172769267l_bool hAPP_f1951378235l_bool hAPP_f633452666l_bool hAPP_f21712077l_bool hAPP_f1499754623l_bool hAPP_f631019661l_bool hAPP_f1472090462l_bool hAPP_f556039215l_bool hAPP_f1320879424l_bool hAPP_b1787118453l_bool hAPP_b496459037l_bool nat_case_nat com_size hAPP_com_nat cond nat_case_bool hAPP_f167292325e_bool hAPP_b2019457360e_bool hAPP_f644196280e_bool hAPP_a723219176e_bool hAPP_f1259673775l_bool hAPP_s1874344717e_bool hAPP_a1200519163e_bool hAPP_p606792009e_bool hAPP_n60670500e_bool hAPP_s1226857760e_bool hAPP_p1910214954l_bool hAPP_a849909144l_bool hAPP_n83983309iple_a hAPP_s2001034685l_bool hAPP_p1227342867iple_a hAPP_H923660098_state hAPP_H1770360232iple_a hAPP_n1036200171_state hAPP_n766730025_state hAPP_p1331349103_state hAPP_n1753616192iple_a hAPP_p805859462iple_a hAPP_H1401668662iple_a hAPP_n131076574a_bool hAPP_n2011101340_state hAPP_p624562724a_bool hAPP_p357103842_state hAPP_H1275418130_state hAPP_H189037865iple_a hAPP_f1820482984iple_a hAPP_n525995272e_bool hAPP_p105983054e_bool hAPP_H1476318469_state hAPP_f1874848592_state hAPP_f1310841988_state hAPP_f1784500635iple_a hAPP_n2002774088l_bool hAPP_f1439241847_state 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 skf1137 skf1138 skf1139 skf1140 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 skf1229 skf1230 % 0.69/0.70 Problem Properties: % 0.69/0.70 This is a full first-order problem with equality. % 0.69/0.70 SZS status GaveUp % 0.69/0.70 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.69/0.70 %------------------------------------------------------------------------------