%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM651+4 : TPTP v9.2.1. Released v7.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n025.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:23 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 : NUM651+4 : TPTP v9.2.1. Released v7.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n025.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:44 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/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/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 = scratc1864283839d_r_ec scratc441283649_orec3 scratc1953890189d_and3 scratc205451438_l_iff scratc30320754d_orec scratc1475035862bvious scratc891215117nd_wel scratc323854386_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 scratc1899664326ptyset scratc1239854964nd_n_1 scratc816599184nd_nat scratc833577392_omega fFalse fTrue scratc945508340_prop1 scratc1601256391d_n_is scratc573870074_29_ii scratc775816440nd_iii scratc1983565041n_some scratc817123975nd_nis scratc1916267638_prop1 scratc1327905463_prop1 scratc1688528320bnd_ap scratc762388523d_plus scratc941391756d_d_Pi aTP_Lamm_ac scratc151181114_prop2 scratc129460338d_24_g scratc1863802514_Sigma scratc1664315776_prop4 scratc1211705522rdsucc scratc151181113_prop1 scratc883767460_n_all aTP_Lamm_ae scratc1710302586_prop1 aTP_Lamm_af scratc1121940411_prop1 scratc797957114d_i1_s scratc1679038911_cond2 aTP_Lamm_ag scratc1679038910_cond1 scratc1601256386d_n_in scratc999559721_n_one aTP_Lamm_ah aTP_Lamm_aj scratc1535408340_power scratc37775665nempty scratc267082108_empty scratc1689053110bnd_in scratc776078843nd_imp scratc1663922179_proj1 scratc1663922178_proj0 scratc670724779d_pair fequal_TPTP_ind fimplies scratc1068455493pair_p aTP_Lamm_bg scratc117621230munion aTP_Lamm_bi scratc1359655582_d_Unj aTP_Lamm_bj scratc117920736d_repl scratc1978543134d_Inj0 scratc1978543135d_Inj1 aTP_Lamm_bk aTP_Lamm_bl scratc643555374univof scratc210498592_nat_p scratc1153435458d_Sing aTP_Lamm_bm fconj scratc2042670206_union scratc815024802nd_nIn scratc1714208363closed scratc976048744closed scratc1140781758closed scratc1579167630closed scratc1251786340d_Subq aTP_Lamm_a aTP_Lamm_br aTP_Lamm_bv aTP_Lamm_bx aTP_Lamm_ca aTP_Lamm_cd aTP_Lamm_cf aTP_Lamm_ch aTP_Lamm_ck aTP_Lamm_cm aTP_Lamm_cn aTP_Lamm_cp aTP_Lamm_cq aTP_Lamm_cs aTP_Lamm_ct aTP_Lamm_cv aTP_Lamm_cw aTP_Lamm_cy aTP_Lamm_cz aTP_Lamm_da aTP_Lamm_db aTP_Lamm_dd aTP_Lamm_de aTP_Lamm_dg aTP_Lamm_di aTP_Lamm_dj aTP_Lamm_dk aTP_Lamm_dl aTP_Lamm_dn aTP_Lamm_ek aTP_Lamm_cx aTP_Lamm_df aTP_Lamm_dh aTP_Lamm_dc aTP_Lamm_cu aTP_Lamm_cr aTP_Lamm_co aTP_Lamm_cl aTP_Lamm_cj aTP_Lamm_cg aTP_Lamm_ce aTP_Lamm_cc aTP_Lamm_bz aTP_Lamm_bw aTP_Lamm_bu aTP_Lamm_bq aTP_Lamm_ab aTP_Lamm_aa % 0.36/0.62 Fol Functions: undefined_bool undefined_TPTP_ind scratc2142620777_amone scratc1458793636_d_and scratc1566258816_d_not scratc742376772nd_ec3 scratc742376837nd_ect scratc743229623nd_eps scratc776144430nd_ind scratc1469349049d_l_ec scratc825975807nd_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 scratc1034077625ffprop scratc1601715577d_n_pl scratc357146165_prop1 scratc739543288_prop1 aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ad scratc1239740399l_some scratc1664315775_prop3 scratc1470005054d_l_or scratc1342542187_d_Sep scratc825713461nd_one scratc709921200nd_all scratc823628852d_esti scratc2082596030d_e_is scratc726152760indeq2 scratc1210837114_indeq scratc943101750d_11_i aTP_Lamm_ai scratc942642911fixfu2 scratc2129079591all_of aTP_Lamm_an aa_fun987228051d_bool aa_TPT60673477d_bool scratc1664315774_prop2 scratc698503740_prop1 scratc959152967_ecect scratc496954899_fixfu aTP_Lamm_ap scratc1953955836d_anec scratc2082596025d_e_in scratc1339467560ectelt scratc1454669437ectset scratc959743358_ecelt scratc826172669nd_out scratc742376833nd_ecp scratc1560786783unmore aTP_Lamm_ar scratc1124323006etprop scratc1444600366t_disj aTP_Lamm_as scratc1756071295d_incl aTP_Lamm_at aTP_Lamm_au scratc817517564nd_non scratc623912165hangef aTP_Lamm_av aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc1322696234wissel scratc1063692693sel_wb scratc776538025nd_ite scratc1063692692sel_wa scratc1664315773_prop1 aa_boo1142376798l_bool scratc2081912165second scratc448238655_first scratc101724077d_pair scratc980467003d_soft scratc1063958900_inj_h aTP_Lamm_aw scratc1757317670d_invf scratc1949431956ective scratc1765712726ective scratc660068301ective scratc405596586_image scratc609953215nverse aTP_Lamm_ax aTP_Lamm_ay scratc1761054201d_tofs aTP_Lamm_ba aTP_Lamm_bb aa_fun1584354236d_bool aTP_Lamm_bd aTP_Lamm_be aTP_Lamm_bf aa_fun1913827119d_bool scratc1687783580eplSep scratc845628616etprod aTP_Lamm_bh scratc1111478329nunion scratc1415547160In_rec scratc1415684463_rec_G scratc1027763871tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bn aa_fun1235454963TP_ind scratc1689053102bnd_if scratc1758288892_UPair aTP_Lamm_bo aTP_Lamm_bp aTP_Lamm_do aTP_Lamm_dp aTP_Lamm_dr aTP_Lamm_dt aTP_Lamm_du aTP_Lamm_dv aTP_Lamm_dw aTP_Lamm_dx aTP_Lamm_dz aTP_Lamm_ea aTP_Lamm_eb aTP_Lamm_ec aTP_Lamm_ed aTP_Lamm_ee aTP_Lamm_eh aTP_Lamm_ej aTP_Lamm_bs aTP_Lamm_bt aTP_Lamm_dm aTP_Lamm_ci aTP_Lamm_cb aTP_Lamm_by aTP_Lamm_eg aTP_Lamm_ei aa_fun1212484691d_bool aTP_Lamm_bc aTP_Lamm_dy aTP_Lamm_ds aTP_Lamm_dq aTP_Lamm_ef 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.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 %------------------------------------------------------------------------------