%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM656+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 : n003.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:24 PM UTC 2026 % Result : Unknown 0.45s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM656+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 : n003.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:27 EDT 2026 % 0.16/0.35 % CPUTime : % 0.16/0.35 SPASS-SCL-FOL version: % 0.20/0.44 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.45/0.63 % 0.45/0.63 Predicates: gg_bool gg_TPTP_ind pp = scratc1659957750d_r_ec scratc236957560_orec3 scratc1573815958d_and3 scratc1211269943_l_iff scratc1797730171d_orec scratc728060557bvious scratc1283916740nd_wel scratc1329672891_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.45/0.63 Fol Constants: bool tPTP_ind scratc201028047ptyset scratc859780733nd_n_1 scratc1209300807nd_nat scratc629251303_omega fFalse fTrue scratc120891389lessis scratc1168518063nd_iii scratc1396930302d_n_is scratc254875001moreis scratc364131377_29_ii scratc1892517117_prop1 scratc1236589736n_some scratc1209825598nd_nis scratc715792767_prop1 scratc127430592_prop1 scratc213164361bnd_ap scratc382314292d_plus scratc737065667d_d_Pi aTP_Lamm_ac scratc1098189891_prop2 scratc578307707d_24_g scratc165166235_Sigma scratc1459989687_prop4 scratc464730217rdsucc scratc1098189890_prop1 scratc1889585965_n_all aTP_Lamm_ae scratc509827715_prop1 aTP_Lamm_af scratc2068949188_prop1 scratc593631025d_i1_s scratc1474712822_cond2 aTP_Lamm_ag scratc1474712821_cond1 scratc1396930297d_n_in scratc2005378226_n_one aTP_Lamm_ah aTP_Lamm_aj scratc1331082251_power scratc486623034nempty scratc62756019_empty scratc213689151bnd_in scratc1168780466nd_imp scratc1459596090_proj1 scratc1459596089_proj0 scratc290650548d_pair fequal_TPTP_ind fimplies scratc321480188pair_p aTP_Lamm_bg scratc566468599munion aTP_Lamm_bi scratc217990439_d_Unj aTP_Lamm_bj scratc1885330153d_repl scratc1231567829d_Inj0 scratc1231567830d_Inj1 aTP_Lamm_bk aTP_Lamm_bl scratc1649373879univof scratc1216317097_nat_p scratc406460153d_Sing aTP_Lamm_bm fconj scratc1838344117_union scratc1207726425nd_nIn scratc2136001442closed scratc328851057closed scratc493584071closed scratc656609605closed scratc504811035d_Subq aTP_Lamm_a aTP_Lamm_br aTP_Lamm_bt aTP_Lamm_bv aTP_Lamm_bx aTP_Lamm_bz aTP_Lamm_cb aTP_Lamm_cd aTP_Lamm_cf aTP_Lamm_ch aTP_Lamm_cj aTP_Lamm_cl aTP_Lamm_cn aTP_Lamm_cp aTP_Lamm_ct aTP_Lamm_cv aTP_Lamm_cy aTP_Lamm_db aTP_Lamm_dd aTP_Lamm_df aTP_Lamm_di aTP_Lamm_dk aTP_Lamm_dl aTP_Lamm_dn aTP_Lamm_do aTP_Lamm_dq aTP_Lamm_dr aTP_Lamm_dt aTP_Lamm_du aTP_Lamm_dw aTP_Lamm_dx aTP_Lamm_dy aTP_Lamm_dz aTP_Lamm_eb aTP_Lamm_ec aTP_Lamm_ee aTP_Lamm_eg aTP_Lamm_eh aTP_Lamm_ei aTP_Lamm_ej aTP_Lamm_el aTP_Lamm_fi aTP_Lamm_dv aTP_Lamm_ed aTP_Lamm_ef aTP_Lamm_ea aTP_Lamm_ds aTP_Lamm_dp aTP_Lamm_dm aTP_Lamm_dj aTP_Lamm_dh aTP_Lamm_de aTP_Lamm_dc aTP_Lamm_da aTP_Lamm_cx aTP_Lamm_cu aTP_Lamm_cs aTP_Lamm_co aTP_Lamm_cm aTP_Lamm_ck aTP_Lamm_ci aTP_Lamm_cg aTP_Lamm_ce aTP_Lamm_cc aTP_Lamm_ca aTP_Lamm_by aTP_Lamm_bw aTP_Lamm_bu aTP_Lamm_bs aTP_Lamm_bq aTP_Lamm_ab aTP_Lamm_aa % 0.45/0.63 Fol Functions: undefined_bool undefined_TPTP_ind scratc1938294688_amone scratc317128493_d_and scratc424593673_d_not scratc1135078395nd_ec3 scratc1135078460nd_ect scratc1135931246nd_eps scratc1168846053nd_ind scratc1265022960d_l_ec scratc1218677430nd_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 aa_TPT43085870d_bool scratc1265678965d_l_or scratc1482924994ffprop scratc1397389488d_n_pl scratc1304154942_prop1 scratc1686552065_prop1 aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ad scratc492765094l_some scratc1459989686_prop3 scratc200877044_d_Sep scratc1218415084nd_one scratc1102622823nd_all scratc443554621d_esti scratc1878269941d_e_is scratc1731971265indeq2 scratc1006511025_indeq scratc1391949119d_11_i aTP_Lamm_ai scratc1948461416fixfu2 scratc1382104286all_of aTP_Lamm_an aa_fun987228051d_bool aa_TPT60673477d_bool scratc1459989685_prop2 scratc1645512517_prop1 scratc754826878_ecect scratc292628810_fixfu aTP_Lamm_ap scratc1573881605d_anec scratc1878269936d_e_in scratc197802417ectelt scratc313004294ectset scratc755417269_ecelt scratc1218874292nd_out scratc1135078456nd_ecp scratc419121640unmore aTP_Lamm_ar scratc1403271239etprop scratc1893447735t_disj aTP_Lamm_as scratc1375997064d_incl aTP_Lamm_at aTP_Lamm_au scratc1210219187nd_non scratc2024420508hangef aTP_Lamm_av aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc181031091wissel scratc1342640926sel_wb scratc1169239648nd_ite scratc1342640925sel_wa scratc1459989684_prop1 aa_boo1142376798l_bool scratc940247022second scratc243912566_first scratc1502232420d_pair scratc600392772d_soft scratc2069777405_inj_h aTP_Lamm_aw scratc1377243439d_invf scratc1739693259ective scratc1555974029ective scratc939016534ective scratc201270497_image scratc2010461558nverse aTP_Lamm_ax aTP_Lamm_ay scratc1380979970d_tofs aTP_Lamm_ba aTP_Lamm_bb aa_fun1584354236d_bool aTP_Lamm_bd aTP_Lamm_be aTP_Lamm_bf aa_fun1913827119d_bool scratc1966731813eplSep scratc98653311etprod aTP_Lamm_bh scratc1560325698nunion scratc1694495393In_rec scratc1837477542_rec_G scratc1476611240tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bn aa_fun1235454963TP_ind scratc213689143bnd_if scratc59652613_UPair aTP_Lamm_bo aTP_Lamm_bp aTP_Lamm_em aTP_Lamm_en aTP_Lamm_ep aTP_Lamm_er aTP_Lamm_es aTP_Lamm_et aTP_Lamm_eu aTP_Lamm_ev aTP_Lamm_ex aTP_Lamm_ey aTP_Lamm_ez aTP_Lamm_fa aTP_Lamm_fb aTP_Lamm_fc aTP_Lamm_ff aTP_Lamm_fh aTP_Lamm_cq aTP_Lamm_cr aTP_Lamm_ek aTP_Lamm_dg aTP_Lamm_cz aTP_Lamm_cw aTP_Lamm_fe aTP_Lamm_fg aa_fun1212484691d_bool aTP_Lamm_bc aTP_Lamm_ew aTP_Lamm_eq aTP_Lamm_eo aTP_Lamm_fd aTP_Lamm_aq aTP_Lamm_az aa_TPT1123896796d_bool aTP_Lamm_ao aTP_Lamm_am aa_fun845057962d_bool aTP_Lamm_al aa_fun1107270209d_bool aa_TPT985247859d_bool aTP_Lamm_ak 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.45/0.63 Problem Properties: % 0.45/0.63 This is a full first-order problem with equality. % 0.45/0.63 SZS status GaveUp % 0.45/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.45/0.63 %------------------------------------------------------------------------------