%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM660+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 : n006.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:25 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 : NUM660+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 : n006.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:31 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.45/0.63 Execution normal ended with status: gaveup % 0.45/0.63 Execution resolution_1 ended with status: gaveup % 0.45/0.63 Execution resolution_2 ended with status: gaveup % 0.45/0.63 Execution resolution_3 ended with status: gaveup % 0.45/0.63 Execution lmodel_grow ended with status: gaveup % 0.45/0.63 No successful execution. % 0.45/0.63 % 0.45/0.63 Input Clauses: % 0.45/0.63 % 0.45/0.63 Predicates: gg_bool gg_TPTP_ind pp = scratc2063910333d_r_ec scratc640910143_orec3 scratc640045327d_and3 scratc148545840_l_iff scratc863959540d_orec scratc851292884bvious scratc1471679243nd_wel scratc266948788_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 scratc989995848ptyset scratc2073493750nd_n_1 scratc1397063310nd_nat scratc1033203886_omega fFalse fTrue scratc1205650934lessis scratc1356280566nd_iii scratc1800882885d_n_is scratc1339634546moreis scratc1506992376_29_ii scratc1648106870_prop1 scratc1359822063n_some scratc1397588101nd_nis scratc471382520_prop1 scratc2030503993_prop1 scratc99244098bnd_ap scratc1596027309d_plus scratc1141018250d_d_Pi aTP_Lamm_ac scratc853779644_prop2 scratc1367275508d_24_g scratc954134036_Sigma scratc1863942270_prop4 scratc587962544rdsucc scratc853779643_prop1 scratc826861862_n_all aTP_Lamm_ae scratc265417468_prop1 aTP_Lamm_af scratc1824538941_prop1 scratc997583608d_i1_s scratc1878665405_cond2 aTP_Lamm_ag scratc1878665404_cond1 scratc1800882880d_n_in scratc942654123_n_one aTP_Lamm_ah aTP_Lamm_aj scratc1735034834_power scratc1275590835nempty scratc466708602_empty scratc99768888bnd_in scratc1356542969nd_imp scratc1863548673_proj1 scratc1863548672_proj0 scratc1504363565d_pair fequal_TPTP_ind fimplies scratc444712515pair_p aTP_Lamm_bg scratc1355436400munion aTP_Lamm_bi scratc1302749984_d_Unj aTP_Lamm_bj scratc951559522d_repl scratc1354800156d_Inj0 scratc1354800157d_Inj1 aTP_Lamm_bk aTP_Lamm_bl scratc586649776univof scratc153592994_nat_p scratc529692480d_Sing aTP_Lamm_bm fconj scratc94813052_union scratc1395488928nd_nIn scratc33640809closed scratc1244225002closed scratc1408958016closed scratc836707212closed scratc628043362d_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_ch aTP_Lamm_cj aTP_Lamm_cm aTP_Lamm_cp aTP_Lamm_cr aTP_Lamm_ct aTP_Lamm_cw aTP_Lamm_cy aTP_Lamm_cz aTP_Lamm_db aTP_Lamm_dc aTP_Lamm_de aTP_Lamm_df aTP_Lamm_dh aTP_Lamm_di aTP_Lamm_dk aTP_Lamm_dl aTP_Lamm_dm aTP_Lamm_dn aTP_Lamm_dp aTP_Lamm_dq aTP_Lamm_ds aTP_Lamm_du aTP_Lamm_dv aTP_Lamm_dw aTP_Lamm_dx aTP_Lamm_dz aTP_Lamm_ew aTP_Lamm_dj aTP_Lamm_dr aTP_Lamm_dt aTP_Lamm_do aTP_Lamm_dg aTP_Lamm_dd aTP_Lamm_da aTP_Lamm_cx aTP_Lamm_cv aTP_Lamm_cs aTP_Lamm_cq aTP_Lamm_co aTP_Lamm_cl aTP_Lamm_ci aTP_Lamm_cg 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 scratc194763623_amone scratc1401888038_d_and scratc1509353218_d_not scratc1322840898nd_ec3 scratc1322840963nd_ect scratc1323693749nd_eps scratc1356608556nd_ind scratc1668975543d_l_ec scratc1406439933nd_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 scratc1669631548d_l_or scratc124409147ffprop scratc1801342071d_n_pl scratc1059744695_prop1 scratc1442141818_prop1 aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ad scratc615997421l_some scratc1863942269_prop3 scratc1285636589_d_Sep scratc1406177587nd_one scratc1290385326nd_all scratc1657267638d_esti scratc134738876d_e_is scratc669247162indeq2 scratc1410463608_indeq scratc33433272d_11_i aTP_Lamm_ai scratc885737313fixfu2 scratc1505336613all_of aTP_Lamm_an aa_fun987228051d_bool aa_TPT60673477d_bool scratc1863942268_prop2 scratc1401102270_prop1 scratc1158779461_ecect scratc696581393_fixfu aTP_Lamm_ap scratc640110974d_anec scratc134738871d_e_in scratc1282561962ectelt scratc1397763839ectset scratc1159369852_ecelt scratc1406636795nd_out scratc1322840959nd_ecp scratc1503881185unmore aTP_Lamm_ar scratc1140309312etprop scratc534931888t_disj aTP_Lamm_as scratc442226433d_incl aTP_Lamm_at aTP_Lamm_au scratc1397981690nd_non scratc169187hangef aTP_Lamm_av aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc1265790636wissel scratc1079678999sel_wb scratc1357002151nd_ite scratc1079678998sel_wa scratc1863942267_prop1 aa_boo1142376798l_bool scratc2025006567second scratc647865149_first scratc1625464747d_pair scratc1814105789d_soft scratc1007053302_inj_h aTP_Lamm_aw scratc443472808d_invf scratc735070610ective scratc551351380ective scratc676054607ective scratc605223080_image scratc2133693885nverse aTP_Lamm_ax aTP_Lamm_ay scratc447209339d_tofs aTP_Lamm_ba aTP_Lamm_bb aa_fun1584354236d_bool aTP_Lamm_bd aTP_Lamm_be aTP_Lamm_bf aa_fun1913827119d_bool scratc1703769886eplSep scratc221885638etprod aTP_Lamm_bh scratc201809851nunion scratc1431533466In_rec scratc1882600557_rec_G scratc118095393tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bn aa_fun1235454963TP_ind scratc99768880bnd_if scratc848620414_UPair aTP_Lamm_bo aTP_Lamm_bp aTP_Lamm_ea aTP_Lamm_eb aTP_Lamm_ed aTP_Lamm_ef aTP_Lamm_eg aTP_Lamm_eh aTP_Lamm_ei aTP_Lamm_ej aTP_Lamm_el aTP_Lamm_em aTP_Lamm_en aTP_Lamm_eo aTP_Lamm_ep aTP_Lamm_eq aTP_Lamm_et aTP_Lamm_ev aTP_Lamm_ce aTP_Lamm_cf aTP_Lamm_dy aTP_Lamm_cu aTP_Lamm_cn aTP_Lamm_ck aTP_Lamm_es aTP_Lamm_eu aa_fun1212484691d_bool aTP_Lamm_bc aTP_Lamm_ek aTP_Lamm_ee aTP_Lamm_ec aTP_Lamm_er 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 %------------------------------------------------------------------------------