%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ016-2.005 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:31:24 PM UTC 2026
% Result : Unsatisfiable 0.36s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ016-2.005 : TPTP v9.2.1. Released v1.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n006.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 12:57:47 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.36/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57 Execution normal ended with status: unsatisfiable
% 0.36/0.57 Used heuristic: normal
% 0.36/0.57
% 0.36/0.57 Input Clauses:
% 0.36/0.57
% 0.36/0.57 Predicates: horizontal_1_2 horizontal_1_3 vertical_1_2 vertical_1_3 horizontal_1_1 vertical_1_1 horizontal_1_4 vertical_1_4 vertical_1_5 horizontal_2_1 vertical_2_1 horizontal_2_2 vertical_2_2 horizontal_2_3 vertical_2_3 horizontal_2_4 vertical_2_4 vertical_2_5 horizontal_3_1 vertical_3_1 horizontal_3_2 vertical_3_2 horizontal_3_3 vertical_3_3 horizontal_3_4 vertical_3_4 vertical_3_5 horizontal_4_1 vertical_4_1 horizontal_4_2 vertical_4_2 horizontal_4_3 vertical_4_3 horizontal_4_4 vertical_4_4 vertical_4_5 horizontal_5_1 horizontal_5_2 horizontal_5_3 horizontal_5_4
% 0.36/0.57 Fol Constants: a
% 0.36/0.57 Fol Functions:
% 0.36/0.57 Problem Properties:
% 0.36/0.57 This is a propositional problem.
% 0.36/0.57
% 0.36/0.57 After reduction: Problem Properties:
% 0.36/0.57 This is a propositional problem.
% 0.36/0.57
% 0.36/0.57
% 0.36/0.57 Reduced Input Clauses:
% 0.36/0.57 118:1:0:[5.0,7.0]:: -> vertical_1_1
% 0.36/0.57 119:2:0:[2.0,8.2]:: -> horizontal_1_4,vertical_1_4
% 0.36/0.57 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1
% 0.36/0.57 121:3:0:[4.0,12.3]:: -> horizontal_2_3,vertical_2_3,horizontal_2_2
% 0.36/0.57 122:1:0:[118.1,36.1]:: horizontal_2_1 ->
% 0.36/0.57 123:1:0:[118.1,37.1]:: vertical_2_1 ->
% 0.36/0.57
% 0.36/0.57 Most General Atoms: horizontal_5_4 vertical_4_5 horizontal_1_3 vertical_1_2 vertical_1_3 horizontal_1_1 horizontal_1_2 vertical_1_1 horizontal_1_4 vertical_1_4 vertical_1_5 horizontal_5_3 vertical_4_4 horizontal_2_2 vertical_2_2 horizontal_2_1 horizontal_2_3 vertical_2_3 horizontal_2_4 vertical_2_4 vertical_2_5 horizontal_3_1 vertical_3_1 vertical_2_1 horizontal_3_2 vertical_3_2 horizontal_3_3 vertical_3_3 horizontal_3_4 vertical_3_4 vertical_3_5 horizontal_4_1 vertical_4_1 horizontal_4_2 vertical_4_2 horizontal_4_3 vertical_4_3 horizontal_4_4 horizontal_5_1 horizontal_5_2
% 0.36/0.57
% 0.36/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 40 atoms initially, heuristics mode: normal ===
% 0.36/0.57
% 0.36/0.57 === Backtracking. Learning clause 126:4:0:[123.0,124.2,122.0,125.3,21.4,66.1,97.1,110.2,17.2,25.1,64.1,77.2,84.1,85.1,15.2,67.1,120.2,45.2,13.3,78.2]:: vertical_3_4 -> vertical_2_3,horizontal_2_4,vertical_1_4
% 0.36/0.57 === Backtracking. Learning clause 127:5:0:[29.1,114.1,104.1,23.1,116.2,93.1,27.1,95.1,21.1,62.2]:: horizontal_3_2 -> vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1
% 0.36/0.57 === Backtracking. Learning clause 128:5:0:[104.2,23.1,29.2,114.1,116.2,27.1,95.1,93.1,21.1]:: -> vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1,vertical_3_2
% 0.36/0.57 === Backtracking. Learning clause 130:6:0:[122.0,129.6,13.2,79.2,45.1,17.1,120.1,94.2]:: horizontal_4_3 -> horizontal_2_4,vertical_1_4,horizontal_3_2,vertical_2_3,vertical_2_2
% 0.36/0.57 === Backtracking. Learning clause 133:4:0:[122.0,131.1,126.0,132.5,104.1,29.2,23.1,116.2,114.1,27.1,96.1,17.2,79.1,13.2,45.1,120.1,130.1,66.2,127.1,128.5,108.1,110.2,84.1,25.1,85.1]:: vertical_3_1 -> horizontal_2_4,vertical_1_4,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 135:4:0:[123.0,134.2,63.2,15.1,17.3,79.1]:: vertical_2_4 -> vertical_3_1,vertical_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 137:4:0:[123.0,136.1,63.2,15.1,17.3]:: -> vertical_3_1,horizontal_3_3,vertical_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 139:4:0:[123.0,138.1,67.2,130.6,15.1,69.2,137.2,133.1,94.2]:: horizontal_4_3 -> horizontal_2_4,vertical_1_4,vertical_2_3
% 0.36/0.57 === Conflict found: 137:4:0:[123.0,136.1,63.2,15.1,17.3]:: -> vertical_3_1,horizontal_3_3,vertical_3_3,vertical_2_3 {}
% 0.36/0.57 === Backtracking. Learning clause 142:3:0:[69.0,140.1,73.1,141.4,137.1,133.1,71.1]:: horizontal_3_2 -> horizontal_2_4,vertical_1_4
% 0.36/0.57 === Backtracking. Learning clause 143:4:0:[83.1,21.3,25.2,108.2,109.2,27.2,114.2]:: horizontal_5_4 -> horizontal_4_2,vertical_3_2,vertical_4_3
% 0.36/0.57 === Backtracking. Learning clause 145:5:0:[139.0,144.2,23.4,126.1,116.2]:: horizontal_5_3 -> horizontal_4_4,vertical_2_3,horizontal_2_4,vertical_1_4
% 0.36/0.57 === Backtracking. Learning clause 147:5:0:[59.1,146.3,83.1,21.3,25.2,108.2,109.2,27.2,145.1,104.2,29.2,143.1,97.1,96.1,65.1,137.3]:: horizontal_3_1 -> horizontal_2_4,vertical_1_4,horizontal_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 148:4:0:[104.1,29.2,145.2,114.1]:: horizontal_5_3 -> vertical_2_3,horizontal_2_4,vertical_1_4
% 0.36/0.57 === Backtracking. Learning clause 150:4:0:[123.0,149.0,15.1,147.1,133.1]:: -> horizontal_3_3,horizontal_2_4,vertical_1_4,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 153:2:0:[122.0,151.1,123.0,152.2,45.2,120.1,13.3,67.2,79.2,15.1,133.1,150.1,31.2,9.2,57.2,56.2]:: vertical_2_5 -> vertical_2_3
% 0.36/0.57 === Conflict found: 142:3:0:[69.0,140.1,73.1,141.4,137.1,133.1,71.1]:: horizontal_3_2 -> horizontal_2_4,vertical_1_4 {}
% 0.36/0.57 === Backtracking. Learning clause 154:2:0:[142.2,50.1,54.2]:: horizontal_3_2,vertical_2_4 ->
% 0.36/0.57 === Backtracking. Learning clause 156:5:0:[73.1,155.5,19.1,105.2,74.1,127.2,153.1]:: vertical_4_5,horizontal_3_2 -> horizontal_5_2,vertical_4_2,horizontal_4_1
% 0.36/0.57 === Conflict found: 133:4:0:[122.0,131.1,126.0,132.5,104.1,29.2,23.1,116.2,114.1,27.1,96.1,17.2,79.1,13.2,45.1,120.1,130.1,66.2,127.1,128.5,108.1,110.2,84.1,25.1,85.1]:: vertical_3_1 -> horizontal_2_4,vertical_1_4,vertical_2_3 {}
% 0.36/0.57 === Backtracking. Learning clause 157:3:0:[133.2,50.1,54.2]:: vertical_3_1,vertical_2_4 -> vertical_2_3
% 0.36/0.57 === Conflict found: 156:5:0:[73.1,155.5,19.1,105.2,74.1,127.2,153.1]:: vertical_4_5,horizontal_3_2 -> horizontal_5_2,vertical_4_2,horizontal_4_1 {}
% 0.36/0.57 === Backtracking. Learning clause 159:3:0:[114.0,158.3,156.3,111.2,110.2,25.1,85.1,84.1,29.2]:: horizontal_3_2,horizontal_5_3,vertical_3_1 ->
% 0.36/0.57 === Backtracking. Learning clause 161:4:0:[114.0,160.4,19.1,105.2,74.1,23.4,116.2,94.1,153.1,104.2,17.2,29.2,159.1]:: horizontal_5_3,vertical_3_1 -> horizontal_3_3,vertical_2_3
% 0.36/0.57 === Conflict found: 137:4:0:[123.0,136.1,63.2,15.1,17.3]:: -> vertical_3_1,horizontal_3_3,vertical_3_3,vertical_2_3 {}
% 0.36/0.57 === Backtracking. Learning clause 164:2:0:[69.0,162.2,73.1,163.3,137.3,71.1,161.2]:: horizontal_3_2,horizontal_5_3 ->
% 0.36/0.57 === Backtracking. Learning clause 166:3:0:[72.1,165.3,19.1,105.2,74.1,23.4,116.2,94.1,153.1,104.2]:: horizontal_5_3,vertical_3_3,vertical_4_5 ->
% 0.36/0.57 === Backtracking. Learning clause 167:3:0:[29.1,114.1,166.3,17.2,164.1]:: horizontal_5_3 -> horizontal_3_3,vertical_2_3
% 0.36/0.57 === Conflict found: 127:5:0:[29.1,114.1,104.1,23.1,116.2,93.1,27.1,95.1,21.1,62.2]:: horizontal_3_2 -> vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1 {}
% 0.36/0.57 === Backtracking. Learning clause 169:4:0:[17.2,168.0,127.3,108.1,84.1,110.2,25.1,85.1,102.2,28.3,117.1,167.1,137.1]:: vertical_4_5 -> horizontal_3_3,vertical_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 172:1:0:[69.0,170.1,73.1,171.2,95.2,21.1,27.3,62.2,108.1,110.2,25.1,85.1,84.1,167.1,137.1,71.1]:: horizontal_3_2 ->
% 0.36/0.57 === Backtracking. Learning clause 173:2:0:[9.1,57.2,31.1]:: vertical_2_5,vertical_1_4 ->
% 0.36/0.57 === Backtracking. Learning clause 175:3:0:[172.0,174.3,44.2,17.4,13.3,56.2,173.2,19.3,105.2,74.1,78.2,77.2]:: vertical_4_5,vertical_3_4 -> vertical_3_3
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 177:7:0:[127.0,176.2,120.3,122.1,47.2,66.2,17.4,128.5,75.2,19.2,173.1]:: vertical_1_4 -> vertical_3_3,vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1,vertical_3_5
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 178:5:0:[120.3,122.1,47.2,66.2,153.2,128.5]:: vertical_2_5 -> vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1
% 0.36/0.57 === Conflict found: 177:7:0:[127.0,176.2,120.3,122.1,47.2,66.2,17.4,128.5,75.2,19.2,173.1]:: vertical_1_4 -> vertical_3_3,vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1,vertical_3_5 {}
% 0.36/0.57 === Backtracking. Learning clause 180:6:0:[175.1,179.3,177.7,105.2]:: vertical_1_4,vertical_4_5 -> vertical_3_3,horizontal_5_2,vertical_4_2,horizontal_4_1
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 182:3:0:[159.0,181.3,120.3,122.1,47.2,66.2,17.4,128.5,75.2,19.2,105.2,178.1,111.2,110.2,25.1,85.1,84.1,175.2,166.2]:: vertical_3_1,horizontal_5_3,vertical_4_5 ->
% 0.36/0.57 === Conflict found: 178:5:0:[120.3,122.1,47.2,66.2,153.2,128.5]:: vertical_2_5 -> vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1 {}
% 0.36/0.57 === Backtracking. Learning clause 183:3:0:[178.3,108.1,175.2,72.1,153.2,84.1,110.2,25.1,85.1]:: vertical_4_5,vertical_2_5,vertical_3_1 ->
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 185:6:0:[156.1,184.4,120.3,122.1,47.2,66.2,128.5,17.4,75.2,19.2,105.2,175.2]:: vertical_4_5 -> horizontal_5_2,vertical_4_2,horizontal_4_1,vertical_2_5,vertical_3_3
% 0.36/0.57 === Backtracking. Learning clause 186:2:0:[27.3,96.1,182.2,185.6,108.1,110.2,25.1,85.1,84.1,183.2]:: vertical_4_5,vertical_3_1 ->
% 0.36/0.57 === Backtracking. Learning clause 187:2:0:[114.1,29.1]:: horizontal_5_3 -> vertical_4_5
% 0.36/0.57 === Backtracking. Learning clause 188:2:0:[24.2,100.1,186.1,81.1,178.2,108.1,110.2,84.1,25.1,85.1]:: vertical_2_5,vertical_3_1 ->
% 0.36/0.57 === Backtracking. Learning clause 189:3:0:[19.2,74.1]:: vertical_3_4 -> vertical_3_5,vertical_2_5
% 0.36/0.57 === Backtracking. Learning clause 192:5:0:[84.0,190.3,172.0,191.6,95.2,21.1,27.3,66.1,120.2,122.1,47.2,17.4,77.2,187.1,186.1]:: vertical_3_4,vertical_3_1 -> vertical_4_2,horizontal_5_2,vertical_3_3
% 0.36/0.57 === Backtracking. Learning clause 193:4:0:[27.3,96.1,187.1,186.1,192.5]:: vertical_3_4,vertical_3_1 -> vertical_4_2,horizontal_5_2
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 195:4:0:[62.0,194.2,120.3,122.1,47.2,66.2,17.4,75.2,19.2]:: vertical_3_2 -> vertical_3_3,vertical_3_5,vertical_2_5
% 0.36/0.57 === Backtracking. Learning clause 198:6:0:[185.0,196.0,178.0,197.3,23.3,92.1,115.2,106.1,29.1,27.3,195.3,128.5]:: -> horizontal_5_3,vertical_3_3,vertical_3_4,horizontal_5_2,vertical_4_2,horizontal_4_1
% 0.36/0.57 === Backtracking. Learning clause 199:1:0:[96.1,27.3,198.2,187.1,186.1,193.1,108.1,110.2,25.1,85.1,84.1]:: vertical_3_1 ->
% 0.36/0.57 === Backtracking. Learning clause 200:3:0:[75.1,19.2,167.2,153.1]:: horizontal_5_3 -> vertical_3_5,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 201:1:0:[15.3,123.1,67.1,199.1,120.2,122.1,47.2,200.3,105.2,187.2]:: horizontal_5_3 ->
% 0.36/0.57 === Backtracking. Learning clause 203:3:0:[105.1,202.1,75.1,19.2,169.2,153.1]:: vertical_4_5 -> vertical_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 204:2:0:[15.3,123.1,67.1,199.1,120.2,122.1,47.2,203.3]:: vertical_4_5 -> vertical_3_3
% 0.36/0.57 === Conflict found: 137:4:0:[123.0,136.1,63.2,15.1,17.3]:: -> vertical_3_1,horizontal_3_3,vertical_3_3,vertical_2_3 {}
% 0.36/0.57 === Backtracking. Learning clause 206:3:0:[153.0,205.3,137.1,199.1,75.2,19.2]:: -> vertical_3_3,vertical_2_3,vertical_3_5
% 0.36/0.57 === Conflict found: 137:4:0:[123.0,136.1,63.2,15.1,17.3]:: -> vertical_3_1,horizontal_3_3,vertical_3_3,vertical_2_3 {}
% 0.36/0.57 === Backtracking. Learning clause 207:3:0:[137.1,199.1]:: -> horizontal_3_3,vertical_3_3,vertical_2_3
% 0.36/0.57 === Backtracking. Learning clause 209:1:0:[199.0,208.1,15.3,123.1,67.1]:: vertical_2_2 ->
% 0.36/0.57 === Backtracking. Learning clause 211:2:0:[199.0,210.0,21.1,97.1,65.1,15.1,123.1,83.1,25.2,108.2,109.2,27.2,96.1,201.1,137.3]:: -> horizontal_3_3,vertical_2_3
% 0.36/0.57 === Conflict found: 120:3:0:[3.0,11.3]:: -> horizontal_2_2,vertical_2_2,horizontal_2_1 {}
% 0.36/0.57 === Backtracking. Learning clause 212:1:0:[120.3,122.1,47.2,209.1,211.2]:: -> horizontal_3_3
% 0.36/0.57 === Backtracking. Learning clause 215:4:0:[105.0,213.2,201.0,214.4,23.3,93.1,115.2,106.1,29.1,21.1,83.1,25.2,108.2,109.2,27.2]:: vertical_3_5 -> vertical_3_4,vertical_3_2,vertical_4_3
% 0.36/0.57
% 0.36/0.57 SZS status Unsatisfiable
% 0.36/0.57
% 0.36/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.57
% 0.36/0.57 SPASS-SCL-FOL Statistics:
% 0.36/0.57 Number of learned clauses: 52
% 0.36/0.57 Number of propagations: 781
% 0.36/0.57 Number of decisions: 92
% 0.36/0.57 Number of resolutions: 349
% 0.36/0.57 Number of condensations: 0
% 0.36/0.57 Number of sub resolutions: 46
% 0.36/0.57 Number of input literals (deduplicated): 40
% 0.36/0.57 Number of grows: 0
% 0.36/0.57 Number of considered ground atoms: 40
% 0.36/0.57
% 0.36/0.57 Needed: 0:00:00.01
% 0.36/0.57
%------------------------------------------------------------------------------