%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM647+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 : n018.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.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM647+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 : n018.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:51:32 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.62 Execution normal ended with status: gaveup % 0.36/0.62 Execution resolution_1 ended with status: gaveup % 0.36/0.62 Execution resolution_2 ended with status: gaveup % 0.36/0.62 Execution resolution_3 ended with status: gaveup % 0.36/0.62 Execution lmodel_grow ended with status: gaveup % 0.36/0.62 No successful execution. % 0.36/0.62 % 0.36/0.62 Input Clauses: % 0.36/0.62 % 0.36/0.62 Predicates: gg_bool gg_TPTP_ind pp = scratc1360517445d_r_ec scratc2085000903_orec3 scratc1819138951d_and3 scratc1259630504_l_iff scratc2043053164d_orec scratc1299153500bvious scratc512647827nd_wel scratc1378033452_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.36/0.62 Fol Constants: bool tPTP_ind scratc474756544ptyset scratc1105103726nd_n_1 scratc438031894nd_nat scratc329810998_omega fFalse fTrue scratc438556685nd_nis scratc1759335536_prop1 scratc1170973361_prop1 scratc1097489997d_n_is scratc576560826bnd_ap scratc627637285d_plus scratc437625362d_d_Pi aTP_Lamm_ad scratc2141732660_prop2 scratc852036204d_24_g scratc438894732_Sigma scratc1160549382_prop4 scratc1035823160rdsucc scratc2141732659_prop1 scratc1937946526_n_all aTP_Lamm_af scratc1553370484_prop1 scratc1807682679n_some aTP_Lamm_ag scratc965008309_prop1 scratc294190720d_i1_s scratc1175272517_cond2 aTP_Lamm_ah scratc1175272516_cond1 scratc1097489992d_n_in scratc2053738787_n_one aTP_Lamm_ai aTP_Lamm_ak scratc1031641946_power scratc760351531nempty scratc1910799362_empty scratc577085616bnd_in scratc397511553nd_imp scratc1160155785_proj1 scratc1160155784_proj0 scratc535973541d_pair fequal_TPTP_ind fimplies scratc892573131pair_p aTP_Lamm_bh scratc840197096munion aTP_Lamm_bj scratc266351000_d_Unj aTP_Lamm_bk scratc2130653146d_repl scratc1802660772d_Inj0 scratc1802660773d_Inj1 aTP_Lamm_bl aTP_Lamm_bm scratc1697734440univof scratc1264677658_nat_p scratc977553096d_Sing aTP_Lamm_bn fconj scratc1538903812_union scratc436457512nd_nIn scratc14374129closed scratc1524662370closed scratc1689395384closed scratc551543572closed scratc1075903978d_Subq aTP_Lamm_a aTP_Lamm_bt aTP_Lamm_bv aTP_Lamm_bx aTP_Lamm_ca aTP_Lamm_cc aTP_Lamm_cd aTP_Lamm_cf aTP_Lamm_cg aTP_Lamm_ci aTP_Lamm_cj aTP_Lamm_cl aTP_Lamm_cm aTP_Lamm_co aTP_Lamm_cp aTP_Lamm_cq aTP_Lamm_cr aTP_Lamm_ct aTP_Lamm_cu aTP_Lamm_cw aTP_Lamm_cy aTP_Lamm_cz aTP_Lamm_da aTP_Lamm_db aTP_Lamm_dd aTP_Lamm_ea aTP_Lamm_cn aTP_Lamm_cv aTP_Lamm_cx aTP_Lamm_cs aTP_Lamm_ck aTP_Lamm_ch aTP_Lamm_ce aTP_Lamm_cb aTP_Lamm_bz aTP_Lamm_bw aTP_Lamm_bu aTP_Lamm_bs aTP_Lamm_ac aTP_Lamm_ab % 0.36/0.62 Fol Functions: undefined_bool undefined_TPTP_ind scratc1638854383_amone scratc365489054_d_and scratc472954234_d_not scratc363809482nd_ec3 scratc363809547nd_ect scratc364662333nd_eps scratc397577140nd_ind scratc965582655d_l_ec scratc447408517nd_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 scratc200214063_prop1 aa_TPT43085870d_bool scratc1097949183d_n_pl scratc582611186_prop1 aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ae scratc1063858037l_some scratc1160549381_prop3 scratc966238660d_l_or scratc249237605_d_Sep scratc447146171nd_one scratc331353910nd_all scratc688877614d_esti scratc1578829636d_e_is scratc1780331826indeq2 scratc707070720_indeq scratc1665677616d_11_i aTP_Lamm_aj scratc1996821977fixfu2 scratc1953197229all_of aTP_Lamm_ao aa_fun987228051d_bool aa_TPT60673477d_bool scratc1160549380_prop2 scratc541571638_prop1 scratc455386573_ecect scratc2140672153_fixfu aTP_Lamm_aq scratc1819204598d_anec scratc1578829631d_e_in scratc246162978ectelt scratc361364855ectset scratc455976964_ecelt scratc447605379nd_out scratc363809543nd_ecp scratc467482201unmore aTP_Lamm_as scratc946869176etprop scratc19692584t_disj aTP_Lamm_at scratc1621320057d_incl aTP_Lamm_au aTP_Lamm_av scratc438950274nd_non scratc448029803hangef aTP_Lamm_aw aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc229391652wissel scratc886238863sel_wb scratc397970735nd_ite scratc886238862sel_wa scratc1160549379_prop1 aa_boo1142376798l_bool scratc988607583second scratc2091955909_first scratc2073325363d_pair scratc845715765d_soft scratc2118137966_inj_h aTP_Lamm_ax scratc1622566432d_invf scratc797103386ective scratc613384156ective scratc482614471ective scratc2049313840_image scratc434070853nverse aTP_Lamm_ay aTP_Lamm_az scratc1626302963d_tofs aTP_Lamm_bb aTP_Lamm_bc aa_fun1584354236d_bool aTP_Lamm_be aTP_Lamm_bf aTP_Lamm_bg aa_fun1913827119d_bool scratc1510329750eplSep scratc669746254etprod aTP_Lamm_bi scratc1834054195nunion scratc1238093330In_rec scratc1863333877_rec_G scratc1750339737tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bo aa_fun1235454963TP_ind scratc577085608bnd_if scratc333381110_UPair aTP_Lamm_bp aTP_Lamm_bq aTP_Lamm_de aTP_Lamm_df aTP_Lamm_dh aTP_Lamm_dj aTP_Lamm_dk aTP_Lamm_dl aTP_Lamm_dm aTP_Lamm_dn aTP_Lamm_dp aTP_Lamm_dq aTP_Lamm_dr aTP_Lamm_ds aTP_Lamm_dt aTP_Lamm_du aTP_Lamm_dx aTP_Lamm_dz aTP_Lamm_dc aTP_Lamm_by aTP_Lamm_br aTP_Lamm_aa aTP_Lamm_dw aTP_Lamm_dy aa_fun1212484691d_bool aTP_Lamm_bd aTP_Lamm_do aTP_Lamm_di aTP_Lamm_dg aTP_Lamm_dv 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.36/0.62 Problem Properties: % 0.36/0.62 This is a full first-order problem with equality. % 0.36/0.62 SZS status GaveUp % 0.36/0.62 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.36/0.62 %------------------------------------------------------------------------------