%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWV516-1.040 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n004.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:37:25 PM UTC 2026 % Result : Unknown 0.37s 0.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV516-1.040 : TPTP v9.2.1. Released v4.0.0. % 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n004.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:30:33 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.37/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.37/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.37/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.37/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.37/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.37/0.62 Execution normal ended with status: gaveup % 0.37/0.62 Execution resolution_1 ended with status: gaveup % 0.37/0.62 Execution resolution_2 ended with status: gaveup % 0.37/0.62 Execution resolution_3 ended with status: gaveup % 0.37/0.62 Execution lmodel_grow ended with status: gaveup % 0.37/0.62 No successful execution. % 0.37/0.62 % 0.37/0.62 Input Clauses: % 0.37/0.62 % 0.37/0.62 Predicates: = % 0.37/0.62 Fol Constants: i39 i40 i38 i37 i36 i35 i34 i33 i32 i31 i30 i29 i28 i27 i26 i25 i24 i23 i22 i21 i20 i19 i18 i17 i16 i15 i14 i13 i12 i11 i10 i9 i8 i7 i6 i5 i4 i3 i2 i1 a1 e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 e11 e12 e13 e14 e15 e16 e17 e18 e19 e20 e21 e22 e23 e24 e25 e26 e27 e28 e29 e30 e31 e32 e33 e34 e35 e36 e37 e38 e39 e40 % 0.37/0.62 Fol Functions: store select % 0.37/0.62 Problem Properties: % 0.37/0.62 This is a full first-order problem with equality. % 0.37/0.62 SZS status GaveUp % 0.37/0.62 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.37/0.62 %------------------------------------------------------------------------------