%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM377+1.030 : TPTP v9.2.1. Released v3.2.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n028.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:29:57 PM UTC 2026 % Result : Unknown 0.42s 0.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM377+1.030 : TPTP v9.2.1. Released v3.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n028.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 12:49:31 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.62 Execution normal ended with status: gaveup % 0.36/0.62 Execution resolution_1 ended with status: gaveup % 0.36/0.62 Execution resolution_2 ended with status: gaveup % 0.36/0.62 Execution resolution_3 ended with status: gaveup % 0.36/0.62 Execution lmodel_grow ended with status: gaveup % 0.36/0.62 No successful execution. % 0.36/0.62 % 0.36/0.62 Input Clauses: % 0.42/0.63 % 0.42/0.63 Predicates: = % 0.42/0.63 Fol Constants: n0 n1 n2 n3 n4 n5 n6 n7 n8 n9 n10 n11 n12 n13 n14 n15 n16 n17 n18 n19 n20 n21 n22 n23 n24 n25 n26 n27 n28 n29 n30 skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33 skc34 skc35 skc36 skc37 skc38 skc39 skc40 skc41 skc42 skc43 skc44 skc45 skc46 skc47 skc48 skc49 skc50 skc51 skc52 skc53 skc54 skc55 skc56 skc57 skc58 skc59 skc60 skc61 skc62 % 0.42/0.63 Fol Functions: succ pred sum % 0.42/0.63 Problem Properties: % 0.42/0.63 This is a first-order ground problem with equality. % 0.42/0.63 SZS status GaveUp % 0.42/0.63 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.42/0.63 %------------------------------------------------------------------------------