%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM286-3 : TPTP v9.2.1. Released v2.5.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n024.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:51 PM UTC 2026 % Result : Unknown 0.18s 0.45s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : NUM286-3 : TPTP v9.2.1. Released v2.5.0. % 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.05/0.24 % Computer : n024.cluster.edu % 0.05/0.24 % Model : x86_64 x86_64 % 0.05/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.24 % Memory : 8042.1875MB % 0.05/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.05/0.24 % CPULimit : 300 % 0.05/0.24 % WCLimit : 300 % 0.05/0.24 % DateTime : Thu May 7 07:48:57 EDT 2026 % 0.05/0.24 % CPUTime : % 0.05/0.24 SPASS-SCL-FOL version: % 0.05/0.29 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.18/0.44 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 Execution normal ended with status: gaveup % 0.18/0.44 Execution resolution_1 ended with status: gaveup % 0.18/0.44 Execution resolution_2 ended with status: gaveup % 0.18/0.44 Execution resolution_3 ended with status: gaveup % 0.18/0.44 Execution lmodel_grow ended with status: gaveup % 0.18/0.44 No successful execution. % 0.18/0.44 % 0.18/0.44 Input Clauses: % 0.18/0.44 % 0.18/0.44 Predicates: member little_set = ordered_pair_predicate subset proper_subset relation single_valued_set function disjoint one_to_one_function maps closed homomorphism associative identity inverse group commutes finite % 0.18/0.44 Fol Constants: estin empty_set universal_set infinity f25 identity_relation natural_numbers plus times prime_numbers twin_prime_numbers even_numbers % 0.18/0.44 Fol Functions: f1 non_ordered_pair singleton_set ordered_pair f2 f3 first f4 f5 second f6 f7 intersection complement union domain_of f8 cross_product converse rotate_right f9 f10 f11 flip_range_of f12 f13 f14 successor sigma f16 f17 powerset f18 f19 f20 f21 image f22 f23 f24 f26 range_of f27 restrict apply f28 apply_to_two_arguments compose f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 % 0.18/0.44 Problem Properties: % 0.18/0.44 This is a full first-order problem with equality. % 0.18/0.44 SZS status GaveUp % 0.18/0.44 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 0.18/0.44 %------------------------------------------------------------------------------