%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW471+1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n002.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.36s 0.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW471+1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n002.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:32 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.36/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.36/0.61 Execution normal ended with status: gaveup % 0.36/0.61 Execution resolution_1 ended with status: gaveup % 0.36/0.61 Execution resolution_2 ended with status: gaveup % 0.36/0.61 Execution resolution_3 ended with status: gaveup % 0.36/0.61 Execution lmodel_grow ended with status: gaveup % 0.36/0.61 No successful execution. % 0.36/0.61 % 0.36/0.61 Input Clauses: % 0.36/0.61 % 0.36/0.61 Predicates: is_fun_pname_bool is_pname 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 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 % 0.36/0.61 Fol Constants: pname bool bot_bo844097828e_bool fFalse fTrue procs hoare_1050552211iple_a member564727580iple_a body the_com body_1 member_pname fdisj bot_bo1687970473a_bool zero_zero_nat fequal1878252616iple_a fequal_pname fconj fimplies fNot g p q n skc37 % 0.36/0.61 Fol Functions: cOMBB_647938656_pname cOMBC_1149511130e_bool cOMBC_1058051404l_bool cOMBK_bool_pname cOMBS_568398431l_bool undefined_pname fun undefi17486888e_bool hoare_472868247rivs_a hoare_810701593lids_a semila1168014441p_bool semila278973382e_bool evalc collect_pname image_pname_pname image_1474161344_pname insert_pname hAPP_pname_pname hAPP_pname_bool hAPP_p61793385e_bool hAPP_bool_bool hAPP_H82695184_pname hAPP_H1927961489a_bool hAPP_f1664156314l_bool hAPP_f1753944735l_bool hAPP_f841604374iple_a hAPP_c1572710133iple_a hAPP_f1148670082iple_a hAPP_H1926610125l_bool hoare_426900819alid_a cOMBB_1500441031_pname cOMBS_121941143iple_a cOMBS_1258869540iple_a image_505679754iple_a semila2005279307a_bool cOMBB_923936821_pname hAPP_p338031245l_bool hAPP_p1261697242iple_a cOMBC_2067518550l_bool cOMBB_633860163iple_a cOMBS_213702372l_bool collec1266446174iple_a cOMBB_675860798_pname cOMBB_548833416iple_a image_29267653iple_a cOMBB_1314377293_pname hAPP_p799580910on_com hAPP_option_com_com suc hAPP_pname_com hAPP_p635540397e_bool insert1871499715iple_a cOMBK_1150238960iple_a hAPP_H562195827a_bool cOMBC_2049287834a_bool cOMBB_650444389iple_a cOMBK_1932526739iple_a cOMBK_753524681_pname cOMBK_1548232270iple_a cOMBK_pname_pname hAPP_b589554111l_bool hAPP_p393069232l_bool hAPP_H1877746411l_bool hAPP_H401672213iple_a hAPP_p510058747iple_a hAPP_p297245038iple_a 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 % 0.36/0.61 Problem Properties: % 0.36/0.61 This is a full first-order problem with equality. % 0.36/0.61 SZS status GaveUp % 0.36/0.61 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.36/0.61 %------------------------------------------------------------------------------