%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW474+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:21 PM UTC 2026 % Result : Unknown 0.45s 0.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWW474+1 : TPTP v9.2.1. Released v5.3.0. % 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.33 % Computer : n021.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Thu May 7 13:35:58 EDT 2026 % 0.15/0.33 % CPUTime : % 0.15/0.33 SPASS-SCL-FOL version: % 0.23/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.63 Execution normal ended with status: gaveup % 0.45/0.63 Execution resolution_1 ended with status: gaveup % 0.45/0.63 Execution resolution_2 ended with status: gaveup % 0.45/0.63 Execution resolution_3 ended with status: gaveup % 0.45/0.63 Execution lmodel_grow ended with status: gaveup % 0.45/0.63 No successful execution. % 0.45/0.63 % 0.45/0.63 Input Clauses: % 0.45/0.64 % 0.45/0.64 Predicates: is_fun_pname_bool is_fun1661590463l_bool is_bool is_pname 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 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 % 0.45/0.64 Fol Constants: wT_bodies finite_finite_pname pname bool hoare_165779456gleton bot_bo844097828e_bool bot_bo1649642514l_bool fFalse fTrue pn bot_bo620288102e_bool ord_le1285840794e_bool hoare_Mirabelle_MGT body_1 the_com body finite595471783e_bool ord_le313189616e_bool finite364844667_state finite464017571e_bool finite786885583l_bool finite1491191519l_bool ord_le1375671464l_bool finite796539827l_bool finite34021339l_bool ord_le889598034l_bool ord_le287025148l_bool ord_le675606854l_bool bot_bo535777328l_bool bot_bo1537088220l_bool bot_bo1761158942l_bool fconj member_pname member1338687867_state member799430823e_bool member2114907555e_bool fimplies fNot fequal_pname fequal1111551311_state fequal533582459e_bool fequal1311889615e_bool fdisj fa y % 0.45/0.64 Fol Functions: cOMBB_647938656_pname cOMBB_307249310e_bool cOMBK_bool_pname cOMBK_1857069011e_bool cOMBS_568398431l_bool cOMBS_350070575l_bool wt undefined_pname fun undefi17486888e_bool undefi64961550l_bool dom_pname_com dom_fu2081503504ol_com collect_pname collec1974731493e_bool image_pname_pname image_47868345e_bool image_54689091_pname image_2131964411e_bool image_1283814551_pname image_187965177_pname image_1705983821_pname image_1619336331_pname insert_pname insert1325755072e_bool hAPP_pname_pname hAPP_pname_bool hAPP_p61793385e_bool hAPP_p338031245l_bool hAPP_bool_bool hAPP_H1621176307_pname hAPP_H78829294e_bool hAPP_H356885323e_bool hAPP_f1297739591_pname hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f560369737_pname hAPP_f971112728l_bool hAPP_f1935102916l_bool hAPP_f559147733l_bool hAPP_f166538662l_bool hAPP_f389811538l_bool hAPP_f468958928l_bool hAPP_f595608956l_bool hAPP_f1022807134l_bool hoare_1598289066_state hAPP_f72706945l_bool insert1415133716_state hAPP_pname_com hAPP_c1126217667_state hAPP_p799580910on_com hAPP_option_com_com cOMBC_1284144636l_bool cOMBC_449066458l_bool collec1823980261e_bool cOMBC_336095980l_bool hAPP_f1759205631l_bool collec792590109l_bool cOMBC_747715418l_bool hAPP_f667366769l_bool collec256567069l_bool cOMBC_1691491604l_bool hAPP_f585161855l_bool collec488126193l_bool cOMBC_7971162l_bool hAPP_f510955609l_bool collec1613912337l_bool image_2003357581_state image_677922117_state image_892968839_state image_18964633_state image_516545147_state image_1642285373l_bool image_288317893l_bool image_70449425e_bool image_1210605179l_bool image_1761575943l_bool image_1828608335e_bool insert1117693814l_bool insert203537868l_bool insert1556680138e_bool cOMBB_675860798_pname collec307967673_state cOMBB_962198420_state cOMBS_458705923l_bool cOMBB_689948150l_bool cOMBS_811933079l_bool cOMBB_404111180l_bool cOMBS_1358309691l_bool cOMBB_1585081418e_bool cOMBS_2066081387l_bool cOMBB_2095475776e_bool cOMBK_367030522_pname cOMBK_168215364_state cOMBK_2035509764_state cOMBK_1039769424_state cOMBK_37193422_pname cOMBK_1706929794_pname cOMBK_pname_pname cOMBK_1503445380e_bool cOMBK_701929478e_bool cOMBK_948730864e_bool cOMBK_1589414042e_bool hAPP_H30606679l_bool hAPP_f556039215l_bool hAPP_f210337421l_bool some_com hAPP_f2138803836on_com hAPP_f2134636538on_com dom_fu1342267980ol_com hAPP_H1049623551e_bool hAPP_p442853985e_bool hAPP_f888949707_state hAPP_f1387463497_state hAPP_p1422361149_state cOMBK_482404831l_bool cOMBK_129401207e_bool cOMBK_659609255_state cOMBC_1149511130e_bool cOMBC_654211620e_bool cOMBB_2144135922_state cOMBB_1522210668e_bool cOMBC_1058051404l_bool cOMBC_1734175330l_bool hAPP_f98417237e_bool cOMBC_1988546018l_bool cOMBC_1114453604l_bool hAPP_f1201187855l_bool hAPP_b589554111l_bool hAPP_p393069232l_bool cOMBB_923936821_pname hAPP_f1476298914l_bool cOMBB_699532858_pname hAPP_H1187982158l_bool hAPP_f32027384l_bool hAPP_f637090980l_bool hAPP_f2143399574l_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 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 % 0.45/0.64 Problem Properties: % 0.45/0.64 This is a full first-order problem with equality. % 0.45/0.64 SZS status GaveUp % 0.45/0.64 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.45/0.64 %------------------------------------------------------------------------------