%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN037-2 : TPTP v9.2.1. Released v1.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n015.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:09 PM UTC 2026 % Result : Unsatisfiable 0.30s 0.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN037-2 : TPTP v9.2.1. Released v1.0.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.33 % Computer : n015.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Thu May 7 13:39:47 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.22/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.30/0.54 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 Execution resolution_1 ended with status: unsatisfiable % 0.30/0.54 Used heuristic: resolution_1 % 0.30/0.54 % 0.30/0.54 Input Clauses: % 0.30/0.54 % 0.30/0.54 Predicates: m1 m3 p m2 q % 0.30/0.54 Fol Constants: cx cw cvv cuu cv cu % 0.30/0.54 Fol Functions: fy fz5 fz2 fy3 % 0.30/0.54 Problem Properties: % 0.30/0.54 This is a full first-order problem without equality. % 0.30/0.54 % 0.30/0.54 After reduction: Problem Properties: % 0.30/0.54 This is a full first-order problem without equality. % 0.30/0.54 % 0.30/0.54 % 0.30/0.54 Reduced Input Clauses: % 0.30/0.54 % 0.30/0.54 Most General Atoms: m1 m3 m2 q(x1) p(x1) % 0.30/0.54 % 0.30/0.54 === Starting SPASS-SCL-FOL A Little Less Naive, considering 14 atoms initially, heuristics mode: resolution_1 === % 0.30/0.54 % 0.30/0.54 === Backtracking. Learning clause 23:4:1:[18.3,1.4,18.3]:Top: m1,m3,m2,p(x0) -> % 0.30/0.54 === Backtracking. Learning clause 24:3:0:[2.4,23.4,23.4]:: m1,m3,m2 -> % 0.30/0.54 === Backtracking. Learning clause 26:3:1:[24.2,25.2,17.2,12.4,17.2]:Top: m3,m1 -> q(x0) % 0.30/0.54 === Backtracking. Learning clause 27:2:0:[11.3,26.3,26.3,24.3]:: m1,m3 -> % 0.30/0.54 === Backtracking. Learning clause 29:3:1:[24.1,28.2,8.4,17.2]:Top: m2,m1 -> q(x0) % 0.30/0.54 === Backtracking. Learning clause 31:2:0:[24.1,30.2,7.3,29.3,29.3]:: m2,m1 -> % 0.30/0.54 === Backtracking. Learning clause 34:2:0:[27.1,32.2,31.0,33.3,3.4,19.1]:: m1,p(cx) -> % 0.30/0.54 === Backtracking. Learning clause 35:1:0:[4.2,21.2,34.2,31.1,27.2]:: m1 -> % 0.30/0.54 === Backtracking. Learning clause 37:3:1:[24.0,36.2,6.3,22.2,5.3]:Top: m2,m3 -> q(x0) % 0.30/0.54 === Backtracking. Learning clause 39:2:0:[24.0,38.2,5.4,20.1,37.3]:: m2,m3 -> % 0.30/0.54 === Backtracking. Learning clause 42:2:0:[27.0,40.2,39.0,41.3,9.4,19.1]:: m3,p(cx) -> % 0.30/0.54 === Backtracking. Learning clause 44:1:0:[27.0,43.1,10.2,21.2,42.2,39.1]:: m3 -> % 0.30/0.54 === Backtracking. Learning clause 47:2:1:[31.1,45.2,39.1,46.3,13.2,18.3]:Top: m2,p(x0) -> % 0.30/0.54 === Backtracking. Learning clause 50:1:0:[31.1,48.1,39.1,49.2,16.4,47.2,47.2]:: m2 -> % 0.30/0.54 === Backtracking. Learning clause 54:1:1:[35.0,51.0,50.0,52.1,44.0,53.2,15.1,22.2,14.1]:Top: -> q(x0) % 0.30/0.54 % 0.30/0.54 SZS status Unsatisfiable % 0.30/0.54 % 0.30/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.54 % 0.30/0.54 SPASS-SCL-FOL Statistics: % 0.30/0.54 Number of learned clauses: 15 % 0.30/0.54 Number of propagations: 106 % 0.30/0.54 Number of decisions: 31 % 0.30/0.54 Number of resolutions: 32 % 0.30/0.54 Number of condensations: 4 % 0.30/0.54 Number of sub resolutions: 17 % 0.30/0.54 Number of input literals (deduplicated): 15 % 0.30/0.54 Number of grows: 0 % 0.30/0.54 Number of considered ground atoms: 14 % 0.30/0.54 % 0.30/0.54 Needed: 0:00:00.00 % 0.30/0.54 %------------------------------------------------------------------------------