%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW470+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 : n019.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:18 PM UTC 2026 % Result : Unknown 0.34s 0.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470+1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n019.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 13:35:30 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.34/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.60 Execution normal ended with status: gaveup % 0.34/0.60 Execution resolution_1 ended with status: gaveup % 0.34/0.60 Execution resolution_2 ended with status: gaveup % 0.34/0.60 Execution resolution_3 ended with status: gaveup % 0.34/0.60 Execution lmodel_grow ended with status: gaveup % 0.34/0.60 No successful execution. % 0.34/0.60 % 0.34/0.60 Input Clauses: % 0.34/0.61 % 0.34/0.61 Predicates: is_bool hBOOL = ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 % 0.34/0.61 Fol Constants: bot_bot_bool fFalse fTrue bot_bo1687970473a_bool insert1871499715iple_a cOMBC_41962815e_bool cOMBC_231445413l_bool fconj cOMBC_2027030106e_bool fequal_state member564727580iple_a fequal1878252616iple_a cOMBC_2049287834a_bool cOMBS_213702372l_bool fimplies fNot fdisj cOMBC_2067518550l_bool the_el287271400iple_a skip the_Ho1745054714iple_a fequal1765155200a_bool cOMBC_1089176504a_bool finite506133020iple_a cOMBS_1378840469l_bool cOMBC_892787026e_bool g c p b % 0.34/0.61 Fol Functions: finite520909254iple_a finite1948426435iple_a hAPP_state_bool hAPP_bool_bool hAPP_H1927961489a_bool hAPP_f1753944735l_bool hoare_472868247rivs_a hoare_1050552211iple_a hAPP_H1816261935a_bool hAPP_f1400872321a_bool cOMBB_1348041619bool_a cOMBB_188601460_state cOMBB_1355796797bool_a hAPP_f1509969235l_bool hAPP_f340725611e_bool hAPP_f1824947087e_bool hAPP_b540892988e_bool hAPP_a2036067514e_bool hAPP_f817621513e_bool hAPP_s1806633685e_bool cOMBK_1458035955bool_a hAPP_H1926610125l_bool hAPP_H562195827a_bool collec1266446174iple_a hAPP_f1915402821a_bool cOMBB_633860163iple_a hAPP_f13210641l_bool hAPP_f1104866853a_bool cOMBK_1150238960iple_a cOMBB_650444389iple_a hAPP_f945663555a_bool hAPP_f1826273671iple_a semi hAPP_f1945881407l_bool cOMBB_545742339iple_a hAPP_f1874567875a_bool hAPP_f1170963427a_bool hAPP_f1447988451a_bool hAPP_b589554111l_bool finite388748825iple_a finite1734202118iple_a hAPP_H568064713iple_a hAPP_H401672213iple_a finite233325225iple_a cOMBK_bool_state cOMBB_160679318_state hAPP_f1759915619e_bool hAPP_f167292325e_bool hAPP_b2019457360e_bool hAPP_s58564346l_bool hAPP_f644196280e_bool hAPP_a723219176e_bool hAPP_f1259673775l_bool hAPP_H1877746411l_bool hAPP_f1261923407e_bool hAPP_f762886889e_bool hAPP_a1200519163e_bool hAPP_a849909144l_bool cOMBB_145932198bool_a hAPP_f963367678e_bool skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf110 skf111 skf112 skf113 skf114 skf115 skf116 skf117 skf118 skf119 skf120 skf121 skf122 skf123 skf124 skf125 skf126 skf127 skf128 skf129 skf130 skf131 skf132 skf133 skf134 skf135 skf136 skf137 skf138 skf139 skf140 skf141 skf142 skf143 skf144 skf145 skf146 skf147 % 0.34/0.61 Problem Properties: % 0.34/0.61 This is a full first-order problem with equality. % 0.34/0.61 SZS status GaveUp % 0.34/0.61 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.34/0.61 %------------------------------------------------------------------------------