%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM926+2 : 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 : n016.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:30:53 PM UTC 2026 % Result : Unknown 0.49s 0.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM926+2 : 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.16/0.34 % Computer : n016.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.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Thu May 7 12:54:37 EDT 2026 % 0.16/0.35 % CPUTime : % 0.16/0.35 SPASS-SCL-FOL version: % 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.49/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 Execution normal ended with status: gaveup % 0.49/0.63 Execution resolution_1 ended with status: gaveup % 0.49/0.63 Execution resolution_2 ended with status: gaveup % 0.49/0.63 Execution resolution_3 ended with status: gaveup % 0.49/0.63 Execution lmodel_grow ended with status: gaveup % 0.49/0.63 No successful execution. % 0.49/0.63 % 0.49/0.63 Input Clauses: % 0.49/0.64 % 0.49/0.64 Predicates: is_int ord_less_eq_int = ord_less_int zprime twoSqu142715416sum2sq ord_less_eq_real ord_less_real ord_less_eq_nat ord_less_nat dvd_dvd_int zcong dvd_dvd_nat dvd_dvd_real quadRes 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 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 % 0.49/0.64 Fol Constants: one_one_int zero_zero_int int min pls m s1 s t one_one_real one_one_nat zero_zero_real zero_zero_nat skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc9 % 0.49/0.64 Fol Functions: minus_minus_int plus_plus_int times_times_int undefined_int bit0 bit1 number_number_of_int power_power_int legendre twoSqu140629262sum2sq number_number_of_nat plus_plus_real power_power_real number267125858f_real times_times_real plus_plus_nat power_power_nat times_times_nat product_Pair_int_int minus_minus_nat minus_minus_real skf8 skf10 skf11 skf12 skf13 % 0.49/0.64 Problem Properties: % 0.49/0.64 This is a full first-order problem with equality. % 0.49/0.64 SZS status GaveUp % 0.49/0.64 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.49/0.64 %------------------------------------------------------------------------------