%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW473+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 : n023.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:20 PM UTC 2026 % Result : Unknown 0.44s 0.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW473+1 : TPTP v9.2.1. Released v5.3.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n023.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:36:09 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.44/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.44/0.61 Execution normal ended with status: gaveup % 0.44/0.61 Execution resolution_1 ended with status: gaveup % 0.44/0.61 Execution resolution_2 ended with status: gaveup % 0.44/0.61 Execution resolution_3 ended with status: gaveup % 0.44/0.61 Execution lmodel_grow ended with status: gaveup % 0.44/0.61 No successful execution. % 0.44/0.61 % 0.44/0.61 Input Clauses: % 0.44/0.61 % 0.44/0.61 Predicates: is_fun_a_bool is_fun_pname_bool is_fun949378684l_bool is_fun1661590463l_bool is_a 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 ren47 ren48 ren49 ren50 % 0.44/0.61 Fol Constants: finite_finite_a finite_finite_pname x_a pname bool g u pn ord_le1311769555a_bool finite_finite_nat finite2012431853t_bool ord_le1568362934t_bool finite595471783e_bool ord_le313189616e_bool finite347923420a_bool finite1701474069l_bool finite719726885l_bool ord_le65145710l_bool finite786885583l_bool finite1491191519l_bool ord_le1375671464l_bool finite1381704300l_bool finite1343359508l_bool ord_le967226251l_bool ord_le1375614389l_bool ord_le675606854l_bool ord_le1454342156l_bool ord_less_eq_nat finite_card_nat finite_card_pname finite_card_a finite346522414t_bool finite1340463720e_bool finite1306199131a_bool finite1352710292l_bool finite269641166l_bool finite1659325229l_bool member_fun_nat_bool suc member799430823e_bool member_fun_a_bool member_nat member_pname member_a fconj fdisj fequal_a fequal_nat fequal_pname fequal_fun_nat_bool fequal533582459e_bool fequal_fun_a_bool fimplies fNot mgt_call na % 0.44/0.61 Fol Functions: cOMBB_bool_bool_a cOMBB_647938656_pname cOMBB_2140588453a_bool cOMBB_307249310e_bool cOMBS_a_bool_bool cOMBS_568398431l_bool cOMBS_1035972772l_bool cOMBS_350070575l_bool undefined_a undefined_pname fun undefined_fun_a_bool undefi17486888e_bool undefi1699038445l_bool undefi64961550l_bool collect_a collect_pname collect_fun_a_bool collec1974731493e_bool image_a_a image_a_pname image_pname_a image_pname_pname image_112932426a_bool image_47868345e_bool image_nat_a image_nat_pname image_nat_fun_a_bool image_1655916159e_bool image_fun_a_bool_a image_1854862208_pname image_876012084bool_a image_1283814551_pname image_fun_nat_bool_a image_1921560913_pname image_573985017bool_a image_990671762_pname image_349102846bool_a image_1705983821_pname image_526090948bool_a image_1604018183_pname insert_a insert_pname insert_fun_a_bool insert1325755072e_bool hAPP_a_bool hAPP_a_fun_a_bool hAPP_a93125764e_bool hAPP_a85458249l_bool hAPP_pname_a hAPP_pname_bool hAPP_p1534023578a_bool hAPP_p61793385e_bool hAPP_p338031245l_bool hAPP_bool_bool hAPP_nat_bool hAPP_nat_fun_a_bool hAPP_n1025906991e_bool hAPP_fun_a_bool_bool hAPP_f2050579477a_bool hAPP_f1631501043l_bool hAPP_f1664156314l_bool hAPP_f759274231e_bool hAPP_f434788991l_bool hAPP_f54304608l_bool hAPP_f621171935l_bool hAPP_f2117159681l_bool hAPP_f1935102916l_bool hAPP_f559147733l_bool hAPP_f1637334154l_bool hAPP_f292226953l_bool hAPP_f389811538l_bool hAPP_f937997336l_bool hAPP_f1363661463l_bool hAPP_f595608956l_bool hAPP_f1295398978l_bool p cOMBC_1693257480l_bool hAPP_f103356543l_bool collect_fun_nat_bool cOMBC_1284144636l_bool cOMBC_1732670874l_bool cOMBC_1269652216l_bool hAPP_f760187903l_bool collec1874991203l_bool cOMBC_336095980l_bool hAPP_f1759205631l_bool collec792590109l_bool cOMBC_636888218l_bool hAPP_f1050622307l_bool collec1635217238l_bool cOMBC_331553030l_bool hAPP_f1434722111l_bool collec707592106l_bool cOMBC_7971162l_bool hAPP_f510955609l_bool collec1613912337l_bool cOMBC_595898202l_bool hAPP_f1772781669l_bool collec1015864663l_bool image_2089570637ol_nat image_1079571347ol_nat image_1802975832ol_nat image_fun_a_bool_nat image_1551609309ol_nat image_496248727ol_nat image_a_nat image_1607900221l_bool image_1874789623l_bool image_1208015684l_bool image_26036933t_bool image_1154884483l_bool image_1642285373l_bool image_1420695166l_bool image_2129980159t_bool image_pname_nat insert_nat insert2003652156l_bool insert1117693814l_bool insert1457093509l_bool insert_fun_nat_bool hAPP_f22106695ol_nat hAPP_n1699378549t_bool hAPP_f921600141ol_nat hAPP_fun_a_bool_nat hAPP_f696928925ol_nat hAPP_f55526627ol_nat hAPP_f2009550088ol_nat hAPP_f1690079119ol_nat hAPP_f98387925ol_nat hAPP_f1253658590ol_nat hAPP_f1951378235l_bool hAPP_nat_nat hAPP_f556039215l_bool hAPP_f285962445l_bool hAPP_n215258509l_bool cOMBB_444170502t_bool cOMBS_1187019125l_bool cOMBB_2095475776e_bool cOMBB_338059395a_bool cOMBB_1972296269bool_a cOMBB_675860798_pname collect_nat cOMBB_1015721476ol_nat cOMBS_nat_bool_bool minus_minus_nat cOMBC_nat_nat_bool cOMBC_1058051404l_bool cOMBB_1897541054_pname cOMBC_pname_a_bool cOMBC_226598744l_bool hAPP_f800510211t_bool cOMBC_1149511130e_bool cOMBC_a_a_bool cOMBC_1355376034l_bool cOMBC_1245412066l_bool hAPP_f1246832597l_bool cOMBC_1988546018l_bool cOMBC_1880041174l_bool cOMBB_bool_bool_nat cOMBB_238756964t_bool hAPP_b589554111l_bool hAPP_a_fun_bool_bool hAPP_n1006566506l_bool hAPP_p393069232l_bool hAPP_f198738859l_bool hAPP_f1748468828l_bool hAPP_f1476298914l_bool skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 % 0.44/0.61 Problem Properties: % 0.44/0.61 This is a full first-order problem with equality. % 0.44/0.61 SZS status GaveUp % 0.44/0.61 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.44/0.61 %------------------------------------------------------------------------------