%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW938+1 : 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:38:47 PM UTC 2026 % Result : Unknown 0.42s 0.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW938+1 : 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 13:37:47 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.38/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.63 Execution normal ended with status: gaveup % 0.38/0.63 Execution resolution_1 ended with status: gaveup % 0.38/0.63 Execution resolution_2 ended with status: gaveup % 0.38/0.63 Execution resolution_3 ended with status: gaveup % 0.38/0.63 Execution lmodel_grow ended with status: gaveup % 0.38/0.63 No successful execution. % 0.38/0.63 % 0.38/0.63 Input Clauses: % 0.38/0.63 % 0.38/0.63 Predicates: p__01 = 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 % 0.38/0.63 Fol Constants: cbool__00 cT__00 cF__00 c_27type_2enum_2enum_27__00 c_27type_2eone_2eone_27__00 c_27const_2earithmetic_2eZERO_27__00 c_27const_2enum_2e0_27__00 c_27const_2eoption_2eNONE_27__00 c_27const_2ebool_2ethe__value_27__00 skc12 skc13 skc14 skc15 skc16 % 0.38/0.63 Fol Functions: s__02 cfun__02 chapp__02 c_24exists__01 c_27const_2emin_2e_40_27__01 c_27const_2ecombin_2eK_27__01 c_27type_2eoption_2eoption_27__01 c_27const_2eoption_2eSOME_27__01 c_27type_2estackSem_2estate_27__02 c_27type_2elabSem_2estate_27__02 c_27const_2estack__to__labProof_2estate__rel_27__02 c_27type_2ewordSem_2eword__loc_27__01 c_27type_2efinite__map_2efmap_27__02 c_27const_2estackSem_2estate__regs_27__01 c_27const_2efinite__map_2eFLOOKUP_27__02 c_27const_2elabSem_2estate__regs_27__02 c_27type_2efcp_2ebit0_27__01 c_27type_2efcp_2ecart_27__02 c_27const_2estackSem_2estate__fp__regs_27__01 c_27const_2elabSem_2estate__fp__regs_27__02 c_27const_2elabSem_2estate__mem_27__01 c_27const_2estackSem_2estate__memory_27__01 c_27const_2elabSem_2estate__mem__domain_27__01 c_27const_2estackSem_2estate__mdomain_27__01 c_27const_2elabSem_2estate__be_27__01 c_27const_2estackSem_2estate__be_27__01 c_27type_2effi_2effi__state_27__01 c_27const_2elabSem_2estate__ffi_27__01 c_27const_2estackSem_2estate__ffi_27__01 c_27const_2elabSem_2estate__clock_27__01 c_27const_2estackSem_2estate__clock_27__01 c_27type_2estackLang_2eprog_27__01 c_27type_2esptree_2espt_27__01 c_27const_2estackSem_2estate__code_27__01 c_27const_2esptree_2elookup_27__02 c_27const_2elabSem_2estate__ptr__reg_27__01 c_27const_2elabSem_2estate__len__reg_27__01 c_27const_2elabSem_2estate__ptr2__reg_27__01 c_27const_2elabSem_2estate__len2__reg_27__01 c_27const_2elabSem_2estate__link__reg_27__01 c_27const_2estackProps_2ecall__args_27__06 c_27type_2elabLang_2eline_27__01 c_27type_2elist_2elist_27__01 c_27type_2emisc_2eapp__list_27__01 c_27type_2epair_2eprod_27__02 c_27const_2earithmetic_2eBIT1_27__01 c_27const_2earithmetic_2eNUMERAL_27__01 c_27const_2estack__alloc_2enext__lab_27__02 c_27const_2estack__to__lab_2eflatten_27__03 c_27const_2epair_2eFST_27__01 c_27const_2emisc_2eappend_27__01 c_27type_2elabLang_2esec_27__01 c_27const_2elabSem_2estate__code_27__01 c_27const_2estack__to__labProof_2ecode__installed_27__03 c_27const_2elabSem_2eloc__to__pc_27__03 c_27const_2elabSem_2estate__failed_27__01 c_27const_2estackSem_2estate__ffi__save__regs_27__01 c_27const_2ebool_2eIN_27__02 c_27const_2elabSem_2estate__io__regs_27__03 c_27const_2ewords_2ew2n_27__01 c_27type_2ebool_2eitself_27__01 c_27const_2efcp_2edimindex_27__01 c_27const_2earithmetic_2eBIT2_27__01 c_27const_2earithmetic_2eDIV_27__02 c_27const_2earithmetic_2eMOD_27__02 c_27const_2estackSem_2estate__use__stack_27__01 c_27const_2estackSem_2estate__use__store_27__01 c_27const_2estackSem_2estate__use__alloc_27__01 c_27const_2estackSem_2estate__clock__fupd_27__02 c_27const_2elabSem_2estate__clock__fupd_27__02 skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 % 0.38/0.63 Problem Properties: % 0.38/0.63 This is a full first-order problem with equality. % 0.38/0.63 SZS status GaveUp % 0.38/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.38/0.63 %------------------------------------------------------------------------------