%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM643+4 : TPTP v9.2.1. Released v7.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n014.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:30:22 PM UTC 2026 % Result : Unknown 0.44s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM643+4 : TPTP v9.2.1. Released v7.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n014.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 12:52:07 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.35/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.35/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.35/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.35/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.35/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.35/0.62 Execution normal ended with status: gaveup % 0.35/0.62 Execution resolution_1 ended with status: gaveup % 0.35/0.62 Execution resolution_2 ended with status: gaveup % 0.35/0.62 Execution resolution_3 ended with status: gaveup % 0.35/0.62 Execution lmodel_grow ended with status: gaveup % 0.35/0.62 No successful execution. % 0.35/0.62 % 0.35/0.62 Input Clauses: % 0.35/0.62 % 0.35/0.62 Predicates: gg_bool gg_TPTP_ind pp = scratc1205095538d_r_ec scratc1929578996_orec3 scratc1275120922d_and3 scratc1990313915_l_iff scratc1499035135d_orec scratc1565208329bvious scratc1187437632nd_wel scratc2108716863_is_of 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 % 0.35/0.62 Fol Constants: bool tPTP_ind scratc805876819ptyset scratc561085697nd_n_1 scratc1112821699nd_nat scratc174389091_omega fFalse fTrue scratc942068090d_n_is scratc1351281101bnd_ap scratc83619256d_plus scratc282203455d_d_Pi aTP_Lamm_ad scratc786516679_prop2 scratc1183156479d_24_g scratc770015007_Sigma scratc1005127475_prop4 scratc1301877989rdsucc scratc786516678_prop1 scratc521146289_n_all aTP_Lamm_af scratc198154503_prop1 scratc2073737508n_some aTP_Lamm_ag scratc1757275976_prop1 scratc1113346490nd_nis scratc138768813d_i1_s scratc1019850610_cond2 aTP_Lamm_ah scratc1019850609_cond1 scratc942068085d_n_in scratc636938550_n_one aTP_Lamm_ai aTP_Lamm_ak scratc876220039_power scratc1091471806nempty scratc1755377455_empty scratc1351805891bnd_in scratc1072301358nd_imp scratc1004733878_proj1 scratc1004733877_proj0 scratc2139439160d_pair fequal_TPTP_ind fimplies scratc1158627960pair_p aTP_Lamm_bh scratc1171317371munion aTP_Lamm_bj scratc997034411_d_Unj aTP_Lamm_bk scratc1586635117d_repl scratc2068715601d_Inj0 scratc2068715602d_Inj1 aTP_Lamm_bl aTP_Lamm_bm scratc280934203univof scratc1995361069_nat_p scratc1243607925d_Sing aTP_Lamm_bn fconj scratc1383481905_union scratc1111247317nd_nIn scratc729296414closed scratc1508448501closed scratc1673181515closed scratc784922049closed scratc1341958807d_Subq aTP_Lamm_a aTP_Lamm_bs aTP_Lamm_bt aTP_Lamm_bv aTP_Lamm_bw aTP_Lamm_by aTP_Lamm_bz aTP_Lamm_cb aTP_Lamm_cc aTP_Lamm_ce aTP_Lamm_cf aTP_Lamm_cg aTP_Lamm_ch aTP_Lamm_cj aTP_Lamm_ck aTP_Lamm_cm aTP_Lamm_co aTP_Lamm_cp aTP_Lamm_cq aTP_Lamm_cr aTP_Lamm_ct aTP_Lamm_dq aTP_Lamm_cd aTP_Lamm_cl aTP_Lamm_cn aTP_Lamm_ci aTP_Lamm_ca aTP_Lamm_bx aTP_Lamm_bu aTP_Lamm_br aTP_Lamm_ac aTP_Lamm_ab % 0.35/0.62 Fol Functions: undefined_bool undefined_TPTP_ind scratc1483432476_amone scratc1096172465_d_and scratc1203637645_d_not scratc1038599287nd_ec3 scratc1038599352nd_ect scratc1039452138nd_eps scratc1072366945nd_ind scratc810160748d_l_ec scratc1122198322nd_or3 aa_bool_bool aa_TPTP_ind_bool aa_TPTP_ind_TPTP_ind aa_fun171081125l_bool aa_fun1431113780TP_ind aa_fun277296641TP_ind fEx_TPTP_ind scratc1374878853_prop1 aa_TPT43085870d_bool scratc942527276d_n_pl aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ae scratc1329912866l_some scratc1005127474_prop3 scratc810816753d_l_or scratc979921016_d_Sep scratc1121935976nd_one scratc1006143715nd_all scratc144859585d_esti scratc1423407729d_e_is scratc363531589indeq2 scratc551648813_indeq scratc1996797891d_11_i aTP_Lamm_aj scratc580021740fixfu2 scratc71768410all_of aTP_Lamm_ao aa_fun987228051d_bool aa_TPT60673477d_bool scratc1005127473_prop2 scratc1333839305_prop1 scratc299964666_ecect scratc1985250246_fixfu aTP_Lamm_aq scratc1275186569d_anec scratc1423407724d_e_in scratc976846389ectelt scratc1092048266ectset scratc300555057_ecelt scratc1122395184nd_out scratc1038599348nd_ecp scratc1198165612unmore aTP_Lamm_as scratc36731083etprop scratc350812859t_disj aTP_Lamm_at scratc1077302028d_incl aTP_Lamm_au aTP_Lamm_av scratc1113740079nd_non scratc714084632hangef aTP_Lamm_aw aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc960075063wissel scratc2123584418sel_wb scratc1072760540nd_ite scratc2123584417sel_wa scratc1005127472_prop1 aa_boo1142376798l_bool scratc1719290994second scratc1936534002_first scratc191896544d_pair scratc301697736d_soft scratc701337729_inj_h aTP_Lamm_ax scratc1078548403d_invf scratc158923591ective scratc2122688009ective scratc1719960026ective scratc1893891933_image scratc700125682nverse aTP_Lamm_ay aTP_Lamm_az scratc1082284934d_tofs aTP_Lamm_bb aTP_Lamm_bc aa_fun1584354236d_bool aTP_Lamm_be aTP_Lamm_bf aTP_Lamm_bg aa_fun1913827119d_bool scratc600191657eplSep scratc935801083etprod aTP_Lamm_bi scratc17690822nunion scratc327955237In_rec scratc430772514_rec_G scratc2081460012tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bo aa_fun1235454963TP_ind scratc1351805883bnd_if scratc664501385_UPair aTP_Lamm_bp aTP_Lamm_bq aTP_Lamm_cu aTP_Lamm_cv aTP_Lamm_cx aTP_Lamm_cz aTP_Lamm_da aTP_Lamm_db aTP_Lamm_dc aTP_Lamm_dd aTP_Lamm_df aTP_Lamm_dg aTP_Lamm_dh aTP_Lamm_di aTP_Lamm_dj aTP_Lamm_dk aTP_Lamm_dn aTP_Lamm_dp aTP_Lamm_cs aTP_Lamm_aa aTP_Lamm_dm aTP_Lamm_do aa_fun1212484691d_bool aTP_Lamm_bd aTP_Lamm_de aTP_Lamm_cy aTP_Lamm_cw aTP_Lamm_dl aTP_Lamm_ar aTP_Lamm_ba aa_TPT1123896796d_bool aTP_Lamm_ap aTP_Lamm_an aa_fun845057962d_bool aTP_Lamm_am aa_fun1107270209d_bool aa_TPT985247859d_bool aTP_Lamm_al aa_TPT125613450d_bool aa_TPT2142672771l_bool 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 % 0.35/0.62 Problem Properties: % 0.35/0.62 This is a full first-order problem with equality. % 0.35/0.62 SZS status GaveUp % 0.35/0.62 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.35/0.62 %------------------------------------------------------------------------------