%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW478+1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n021.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:23 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 : SWW478+1 : TPTP v9.2.1. Released v5.3.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n021.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:36:28 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.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.63 Execution normal ended with status: gaveup % 0.42/0.63 Execution resolution_1 ended with status: gaveup % 0.42/0.63 Execution resolution_2 ended with status: gaveup % 0.42/0.63 Execution resolution_3 ended with status: gaveup % 0.42/0.63 Execution lmodel_grow ended with status: gaveup % 0.42/0.63 No successful execution. % 0.42/0.63 % 0.42/0.63 Input Clauses: % 0.42/0.64 % 0.42/0.64 Predicates: is_bool = hBOOL 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 % 0.42/0.64 Fol Constants: l_a v_1 v_2 produc1441475159on_val produc1259058957on_val ea produc899768717on_val ha la v e_a h_a p wf_J_mdecl e t_1 t produc2128769400l_bool produc1958875245l_bool cOMBB_1718333400on_val cOMBB_383678192on_val cOMBB_1303934920on_val fconj cOMBC_2027949654l_bool cOMBB_1518282696on_val cOMBC_832625297y_bool produc1911463199l_bool produc1815960045l_bool produc399384568l_bool produc1988544340l_bool produc1174947465on_val cOMBB_819439237t_char cOMBB_877741809on_val produc1003071703on_val cOMBB_635947099on_val cOMBB_1083177073on_val produc901351817on_val cOMBB_1466889536on_val cOMBB_171276332on_val produc1148763895on_val cOMBB_1259202826on_val cOMBB_1292453606on_val cOMBB_740252943t_char cOMBB_338347573on_val cOMBB_466903633on_val cOMBB_672625589on_val cOMBB_1522540928on_val cOMBB_1153617344on_val cOMBB_1750801836on_val cOMBB_364363975on_val cOMBB_1466662571on_val cOMBB_1027621637t_char cOMBB_1759207793on_val produc376702929l_bool produc20018513l_bool produc2036005791l_bool produc1275132703l_bool produc121041439l_bool produc334393759l_bool unit none_val none_ty % 0.42/0.64 Fol Functions: assigned widen_2090681816t_char wf_pro755087577t_char wTrt hAPP_bool_bool hAPP_f1001225811y_bool hAPP_f1033709212l_bool hAPP_f61040418l_bool hAPP_P1708370145l_bool hAPP_P159683425l_bool hAPP_P282169671l_bool member840932460on_val member763590124on_val member773094996on_val hAPP_l207779698on_val some_val hAPP_e1659493427on_val hAPP_f1849790461on_val fun_up1149430426on_val hAPP_f1727192346on_val hAPP_P604205461on_val hAPP_P1870962205on_val hAPP_P1886180715on_val red hAPP_l512744617ion_ty fun_up424764369ion_ty some_ty typeSa1234865140_sconf hconf_97414254t_char lconf_496643946t_char hAPP_f1213370163y_bool hAPP_f2060496320y_bool hp val_list_char lAss_list_char seq_list_char block_list_char hAPP_f2121594859l_bool hAPP_f1175813647l_bool hAPP_f592397849l_bool hAPP_f1977633121l_bool hAPP_f1452292669l_bool hAPP_f1523875321l_bool hAPP_f348318673l_bool hAPP_f857351829l_bool hAPP_f838396643l_bool hAPP_f550652027l_bool cOMBS_570216337l_bool hAPP_P1116729363l_bool hAPP_f635218277l_bool hAPP_e1833980889l_bool hAPP_f1930574389l_bool hAPP_f1520199827on_val hAPP_P789556885on_val hAPP_f1825030711l_bool hAPP_f516738477l_bool hAPP_f653692369l_bool hAPP_f394183983on_val hAPP_P1760219823on_val hAPP_f881985847l_bool hAPP_f1438732387l_bool hAPP_f1241216909l_bool hAPP_f1309113673on_val hAPP_f1233687287l_bool hAPP_f399538905l_bool hAPP_f850751421l_bool hAPP_f204556415on_val hAPP_P2024243179on_val hAPP_f2052660463l_bool hAPP_f1043869573l_bool hAPP_f927043595l_bool hAPP_b589554111l_bool hAPP_f1308714617l_bool hAPP_f917296015l_bool hAPP_f546724245l_bool hAPP_f1560238713l_bool hAPP_f2032347769l_bool hAPP_f641257349l_bool hAPP_f1863694447l_bool hAPP_f1734879897l_bool hAPP_f555424277l_bool hAPP_f2057883639l_bool hAPP_f1050935001l_bool hAPP_f1363667773l_bool hAPP_f365540729l_bool hAPP_f639265145l_bool hAPP_f1342895119l_bool hAPP_f10074679l_bool hAPP_f1725502637l_bool hAPP_f439412817l_bool hAPP_P1134042693l_bool hAPP_P595502227l_bool hAPP_f444383845l_bool hAPP_P1826803705l_bool hAPP_P1953518277l_bool hAPP_f1591648613l_bool hAPP_P678729081l_bool hAPP_e500528395l_bool hAPP_P1988153107l_bool hAPP_f468299289l_bool hAPP_e592495499l_bool hAPP_P1638898323l_bool hAPP_f1760682521l_bool hAPP_f2135509569l_bool hAPP_f396019662l_bool hAPP_f1276548047l_bool hAPP_f2144092865l_bool hAPP_f2011777102l_bool hAPP_f833559503l_bool redp cOMBK_1097134891t_char cOMBK_1294242658t_char hAPP_f1074020887l_bool hAPP_f181262431l_bool hAPP_f603925568l_bool hAPP_f1145256474l_bool hAPP_f2134824737l_bool hAPP_f926562337l_bool hAPP_f1617787571l_bool hAPP_f1008932791l_bool hAPP_f1492320500l_bool hAPP_f318082871l_bool hAPP_f1926378906on_val hAPP_f1301559543l_bool hAPP_P1776198677on_val hAPP_f489055607l_bool hAPP_f1712766199l_bool hAPP_f1840640125on_val hAPP_f524589473l_bool hAPP_f602593190on_val hAPP_e108155315on_val hAPP_f204771371l_bool hAPP_f600512025on_val hAPP_P2083594489on_val 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 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45 skf46 skf47 skf48 skf49 skf50 skf51 skf52 skf53 skf54 skf55 skf56 skf57 skf58 skf59 skf60 skf61 skf62 skf63 skf64 skf65 skf66 skf67 skf68 skf69 skf70 skf71 skf72 skf73 skf74 skf75 skf76 skf77 skf78 skf79 skf80 skf81 skf82 skf83 skf84 skf85 skf86 skf87 skf88 skf89 skf90 skf91 skf92 skf93 skf94 skf95 skf96 skf97 skf98 skf99 skf100 skf101 skf102 skf103 skf104 skf105 skf106 skf107 % 0.42/0.64 Problem Properties: % 0.42/0.64 This is a full first-order problem with equality. % 0.42/0.64 SZS status GaveUp % 0.42/0.64 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.42/0.64 %------------------------------------------------------------------------------