%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM637+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 : n022.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:21 PM UTC 2026 % Result : Unknown 0.39s 0.61s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM637+4 : TPTP v9.2.1. Released v7.3.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n022.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 12:51:22 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.60 Execution normal ended with status: gaveup % 0.39/0.60 Execution resolution_1 ended with status: gaveup % 0.39/0.60 Execution resolution_2 ended with status: gaveup % 0.39/0.60 Execution resolution_3 ended with status: gaveup % 0.39/0.60 Execution lmodel_grow ended with status: gaveup % 0.39/0.60 No successful execution. % 0.39/0.60 % 0.39/0.60 Input Clauses: % 0.39/0.60 % 0.39/0.60 Predicates: gg_bool gg_TPTP_ind pp = scratc1595856243d_r_ec scratc172856053_orec3 scratc452916185d_and3 scratc989495034_l_iff scratc676830398d_orec scratc1717520266bvious scratc1704465857nd_wel scratc1107897982_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.39/0.60 Fol Constants: bool tPTP_ind scratc75217938ptyset scratc1886364608nd_n_1 scratc1629849924nd_nat scratc565149796_omega fFalse fTrue scratc825655750_prop1 scratc1332828795d_n_is scratc78565797n_some aTP_Lamm_aa scratc237293575_prop1 scratc1630374715nd_nis scratc1454189926rdsucc scratc529529518d_i1_s scratc1410611315_cond2 scratc1667811056_n_all aTP_Lamm_ac scratc1410611314_cond1 scratc1332828790d_n_in scratc1783603317_n_one aTP_Lamm_ad scratc672964160d_d_Pi aTP_Lamm_af scratc416169996bnd_ap scratc1266980744_power scratc360812925nempty scratc2146138160_empty scratc416694786bnd_in scratc39356126_Sigma scratc1589329583nd_imp scratc1395494583_proj1 scratc1395494582_proj0 scratc1317234423d_pair fequal_TPTP_ind fimplies scratc1310939897pair_p aTP_Lamm_bc scratc440658490munion aTP_Lamm_be scratc2143699178_d_Unj aTP_Lamm_bf scratc764430380d_repl scratc73543890d_Inj0 scratc73543891d_Inj1 aTP_Lamm_bg aTP_Lamm_bh scratc1427598970univof scratc994542188_nat_p scratc1395919862d_Sing aTP_Lamm_bi fconj scratc1774242610_union scratc1628275542nd_nIn scratc1217033503closed scratc1019404980closed scratc1184137994closed scratc1504037954closed scratc1494270744d_Subq aTP_Lamm_a aTP_Lamm_bm aTP_Lamm_bo aTP_Lamm_bp aTP_Lamm_br aTP_Lamm_bt aTP_Lamm_bu aTP_Lamm_bv aTP_Lamm_bw aTP_Lamm_by aTP_Lamm_cv aTP_Lamm_ab aTP_Lamm_bq aTP_Lamm_bs aTP_Lamm_bn % 0.39/0.60 Fol Functions: undefined_bool undefined_TPTP_ind scratc1874193181_amone scratc95353584_d_and scratc202818764_d_not scratc1555627512nd_ec3 scratc1555627577nd_ect scratc1556480363nd_eps scratc1589395170nd_ind scratc1200921453d_l_ec scratc1639226547nd_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 scratc1201577458d_l_or scratc2126585783_d_Sep scratc1638964201nd_one scratc1523171940nd_all scratc1482224803l_some scratc1470138496d_esti scratc1814168434d_e_is scratc1510196356indeq2 scratc942409518_indeq scratc1266139010d_11_i aa_TPT1424761345TP_ind aa_TPT494704832TP_ind aTP_Lamm_ae scratc1726686507fixfu2 scratc224080347all_of aTP_Lamm_aj aa_fun987228051d_bool aa_TPT60673477d_bool scratc1395888178_prop2 scratc1961340552_prop1 scratc690725371_ecect scratc228527303_fixfu aTP_Lamm_al scratc452981832d_anec scratc1814168429d_e_in scratc2123511156ectelt scratc91229385ectset scratc691315762_ecelt scratc1639423409nd_out scratc1555627573nd_ecp scratc197346731unmore aTP_Lamm_an scratc496865546etprop scratc1767637626t_disj aTP_Lamm_ao scratc255097291d_incl aTP_Lamm_ap aTP_Lamm_aq scratc1630768304nd_non scratc866396569hangef aTP_Lamm_ar aa_TPT1781712639TP_ind aa_TPT1791839040TP_ind scratc2106739830wissel scratc436235233sel_wb scratc1589788765nd_ite scratc436235232sel_wa scratc1395888177_prop1 aa_boo1142376798l_bool scratc718472113second scratc179811059_first scratc344208481d_pair scratc1626976647d_soft scratc1848002496_inj_h aTP_Lamm_as scratc256343666d_invf scratc1502012232ective scratc1318293002ective scratc32610841ective scratc137168990_image scratc852437619nverse aTP_Lamm_at aTP_Lamm_au scratc260080197d_tofs aTP_Lamm_aw aTP_Lamm_ax aa_fun1584354236d_bool aTP_Lamm_az aTP_Lamm_ba aTP_Lamm_bb aa_fun1913827119d_bool scratc1060326120eplSep scratc1088113020etprod aTP_Lamm_bd scratc1434515589nunion scratc788089700In_rec scratc918509603_rec_G scratc1350801131tminus cOMBC_1555011498d_bool cOMBB_658106424TP_ind cOMBS_2003118649l_bool aTP_Lamm_bj aa_fun1235454963TP_ind scratc416694778bnd_if scratc2081326152_UPair aTP_Lamm_bk aTP_Lamm_bl aTP_Lamm_bz aTP_Lamm_ca aTP_Lamm_cc aTP_Lamm_ce aTP_Lamm_cf aTP_Lamm_cg aTP_Lamm_ch aTP_Lamm_ci aTP_Lamm_ck aTP_Lamm_cl aTP_Lamm_cm aTP_Lamm_cn aTP_Lamm_co aTP_Lamm_cp aTP_Lamm_cs aTP_Lamm_cu aTP_Lamm_bx aTP_Lamm_cr aTP_Lamm_ct aa_fun1212484691d_bool aTP_Lamm_ay aTP_Lamm_cj aTP_Lamm_cd aTP_Lamm_cb aTP_Lamm_cq aTP_Lamm_am aTP_Lamm_av aa_TPT1123896796d_bool aTP_Lamm_ak aTP_Lamm_ai aa_fun845057962d_bool aTP_Lamm_ah aa_fun1107270209d_bool aa_TPT985247859d_bool aTP_Lamm_ag 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.39/0.60 Problem Properties: % 0.39/0.60 This is a full first-order problem with equality. % 0.39/0.60 SZS status GaveUp % 0.39/0.60 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.39/0.60 %------------------------------------------------------------------------------