%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN001-1.005 : TPTP v9.2.1. Released v1.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n011.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:39:06 PM UTC 2026 % Result : Unsatisfiable 0.34s 0.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN001-1.005 : TPTP v9.2.1. Released v1.0.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 : n011.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.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 13:38:48 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.34/0.53 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 Execution normal ended with status: unsatisfiable % 0.34/0.53 Used heuristic: normal % 0.34/0.53 % 0.34/0.53 Input Clauses: % 0.34/0.53 % 0.34/0.53 Predicates: p_1 p_2 p_3 p_4 p_5 % 0.34/0.53 Fol Constants: a % 0.34/0.53 Fol Functions: % 0.34/0.53 Problem Properties: % 0.34/0.53 This is a propositional problem. % 0.34/0.53 % 0.34/0.53 % 0.34/0.53 Reduced Input Clauses: % 0.34/0.53 33:4:0:[17.0,1.0]:: -> p_2,p_3,p_4,p_5 % 0.34/0.53 34:4:0:[33.4,2.0]:: -> p_1,p_2,p_3,p_4 % 0.34/0.53 35:4:0:[33.3,3.0]:: -> p_1,p_2,p_3,p_5 % 0.34/0.53 37:3:0:[34.4,4.0,35.4,36.1]:: -> p_1,p_2,p_3 % 0.34/0.53 38:4:0:[33.2,5.0]:: -> p_1,p_2,p_4,p_5 % 0.34/0.53 40:3:0:[34.3,6.0,38.4,39.1]:: -> p_1,p_2,p_4 % 0.34/0.53 42:3:0:[35.3,7.0,38.3,41.1]:: -> p_1,p_2,p_5 % 0.34/0.53 45:2:0:[37.4,8.0,40.4,43.1,42.4,44.2]:: -> p_1,p_2 % 0.34/0.53 46:4:0:[33.1,9.0]:: -> p_1,p_3,p_4,p_5 % 0.34/0.53 48:3:0:[34.2,10.0,46.4,47.1]:: -> p_1,p_3,p_4 % 0.34/0.53 50:3:0:[35.2,11.0,46.3,49.1]:: -> p_1,p_3,p_5 % 0.34/0.53 53:2:0:[37.3,12.0,48.4,51.1,50.4,52.2]:: -> p_1,p_3 % 0.34/0.53 55:3:0:[38.2,13.0,46.2,54.1]:: -> p_1,p_4,p_5 % 0.34/0.53 58:2:0:[40.3,14.0,48.3,56.1,55.4,57.2]:: -> p_1,p_4 % 0.34/0.53 61:2:0:[42.3,15.0,50.3,59.1,55.3,60.2]:: -> p_1,p_5 % 0.34/0.53 65:1:0:[45.4,16.0,53.4,62.1,58.4,63.2,61.4,64.3]:: -> p_1 % 0.34/0.53 66:4:0:[34.1,17.0]:: -> p_2,p_3,p_4,p_5 % 0.34/0.53 68:3:0:[34.1,18.0,33.4,67.1]:: -> p_2,p_3,p_4 % 0.34/0.53 70:3:0:[35.1,19.0,33.3,69.1]:: -> p_2,p_3,p_5 % 0.34/0.53 73:2:0:[37.2,20.0,68.4,71.1,70.4,72.2]:: -> p_2,p_3 % 0.34/0.53 75:3:0:[38.1,21.0,33.2,74.1]:: -> p_2,p_4,p_5 % 0.34/0.53 78:2:0:[40.2,22.0,68.3,76.1,75.4,77.2]:: -> p_2,p_4 % 0.34/0.53 81:2:0:[42.2,23.0,70.3,79.1,75.3,80.2]:: -> p_2,p_5 % 0.34/0.53 85:1:0:[45.3,24.0,73.4,82.1,78.4,83.2,81.4,84.3]:: -> p_2 % 0.34/0.53 87:3:0:[46.1,25.0,33.1,86.1]:: -> p_3,p_4,p_5 % 0.34/0.53 90:2:0:[48.2,26.0,68.2,88.1,87.4,89.2]:: -> p_3,p_4 % 0.34/0.53 93:2:0:[50.2,27.0,70.2,91.1,87.3,92.2]:: -> p_3,p_5 % 0.34/0.53 97:1:0:[53.3,28.0,73.3,94.1,90.4,95.2,93.4,96.3]:: -> p_3 % 0.34/0.53 100:2:0:[55.2,29.0,75.2,98.1,87.2,99.2]:: -> p_4,p_5 % 0.34/0.53 104:1:0:[58.3,30.0,78.3,101.1,90.3,102.2,100.4,103.3]:: -> p_4 % 0.34/0.53 108:1:0:[61.3,31.0,81.3,105.1,93.3,106.2,100.3,107.3]:: -> p_5 % 0.34/0.53 113:0:0:[65.4,32.0,85.4,109.1,97.4,110.2,104.4,111.3,108.4,112.4]:: -> % 0.34/0.53 % 0.34/0.53 SZS status Unsatisfiable % 0.34/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.53 % 0.34/0.53 SPASS-SCL-FOL Statistics: % 0.34/0.53 Number of learned clauses: 0 % 0.34/0.53 Number of propagations: 0 % 0.34/0.53 Number of decisions: 0 % 0.34/0.53 Number of resolutions: 0 % 0.34/0.53 Number of condensations: 0 % 0.34/0.53 Number of sub resolutions: 81 % 0.34/0.53 % 0.34/0.53 Needed: 0:00:00.00 % 0.34/0.53 %------------------------------------------------------------------------------