%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ015-2.006 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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.30s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ015-2.006 : TPTP v9.2.1. Released v1.2.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 : n026.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:58:09 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60 Execution resolution_1 ended with status: unsatisfiable
% 0.30/0.60 Used heuristic: resolution_1
% 0.30/0.60
% 0.30/0.60 Input Clauses:
% 0.30/0.60
% 0.30/0.60 Predicates: horizontal_1_1 vertical_1_1 horizontal_6_5 vertical_5_6 horizontal_1_2 vertical_1_2 horizontal_1_3 vertical_1_3 horizontal_1_4 vertical_1_4 horizontal_1_5 vertical_1_5 vertical_1_6 horizontal_2_1 vertical_2_1 horizontal_2_2 vertical_2_2 horizontal_2_3 vertical_2_3 horizontal_2_4 vertical_2_4 horizontal_2_5 vertical_2_5 vertical_2_6 horizontal_3_1 vertical_3_1 horizontal_3_2 vertical_3_2 horizontal_3_3 vertical_3_3 horizontal_3_4 vertical_3_4 horizontal_3_5 vertical_3_5 vertical_3_6 horizontal_4_1 vertical_4_1 horizontal_4_2 vertical_4_2 horizontal_4_3 vertical_4_3 horizontal_4_4 vertical_4_4 horizontal_4_5 vertical_4_5 vertical_4_6 horizontal_5_1 vertical_5_1 horizontal_5_2 vertical_5_2 horizontal_5_3 vertical_5_3 horizontal_5_4 vertical_5_4 horizontal_5_5 vertical_5_5 horizontal_6_1 horizontal_6_2 horizontal_6_3 horizontal_6_4
% 0.30/0.60 Fol Constants: a
% 0.30/0.60 Fol Functions:
% 0.30/0.60 Problem Properties:
% 0.30/0.60 This is a propositional problem.
% 0.30/0.60
% 0.30/0.60 After reduction: Problem Properties:
% 0.30/0.60 This is a propositional problem.
% 0.30/0.60
% 0.30/0.60
% 0.30/0.60 Reduced Input Clauses:
% 0.30/0.60 185:2:0:[1.0,5.2]:: -> horizontal_1_2,vertical_1_2
% 0.30/0.60 186:2:0:[2.0,10.2]:: -> horizontal_2_1,vertical_2_1
% 0.30/0.60 187:2:0:[4.0,33.0]:: -> horizontal_5_5,vertical_4_6
% 0.30/0.60 188:2:0:[3.0,38.0]:: -> horizontal_6_4,vertical_5_5
% 0.30/0.60
% 0.30/0.60 Most General Atoms: horizontal_1_1 vertical_1_1 horizontal_6_5 vertical_5_6 horizontal_1_2 vertical_1_2 horizontal_1_3 vertical_1_3 horizontal_1_4 vertical_1_4 horizontal_1_5 vertical_1_5 vertical_1_6 horizontal_2_1 vertical_2_1 horizontal_2_2 vertical_2_2 horizontal_2_3 vertical_2_3 horizontal_2_4 vertical_2_4 horizontal_2_5 vertical_2_5 vertical_2_6 horizontal_3_1 vertical_3_1 horizontal_3_2 vertical_3_2 horizontal_3_3 vertical_3_3 horizontal_3_4 vertical_3_4 horizontal_3_5 vertical_3_5 vertical_3_6 horizontal_4_1 vertical_4_1 horizontal_4_2 vertical_4_2 horizontal_4_3 vertical_4_3 horizontal_4_4 vertical_4_4 horizontal_4_5 vertical_4_5 vertical_4_6 horizontal_5_1 vertical_5_1 horizontal_5_2 vertical_5_2 horizontal_5_3 vertical_5_3 horizontal_5_4 vertical_5_4 horizontal_5_5 vertical_5_5 horizontal_6_1 horizontal_6_2 horizontal_6_3 horizontal_6_4
% 0.30/0.60
% 0.30/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 0.30/0.60
% 0.30/0.60 === Backtracking. Learning clause 189:3:0:[179.1,188.1,36.1]:: -> vertical_5_5,horizontal_6_2,vertical_5_3
% 0.30/0.60 === Clause set with instances from active satisfied. Growing active. New size: 56
% 0.30/0.60 === Restarting.
% 0.30/0.60 === Conflict found: 187:2:0:[4.0,33.0]:: -> horizontal_5_5,vertical_4_6 {}
% 0.30/0.60 === Backtracking. Learning clause 190:3:0:[187.1,165.1,140.1,26.2,141.1]:: vertical_3_6 -> horizontal_4_4,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 191:2:0:[164.1,187.1]:: horizontal_5_4 -> vertical_4_6
% 0.30/0.60 === Backtracking. Learning clause 192:3:0:[173.1,189.2,34.1,163.2,187.1,154.1]:: horizontal_5_2 -> vertical_5_1,vertical_4_6
% 0.30/0.60 === Backtracking. Learning clause 193:6:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,105.1,17.2]:: vertical_2_5 -> vertical_3_1,vertical_2_6,horizontal_3_2,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 194:3:0:[128.1,190.2]:: horizontal_4_3,vertical_3_6 -> vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 195:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,144.1,140.1,24.2,194.1]:: vertical_4_1,vertical_3_6 -> horizontal_4_2,vertical_3_3,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 196:5:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,115.2,195.3,22.2]:: vertical_3_6 -> vertical_3_3,vertical_3_5,horizontal_4_1,vertical_3_1
% 0.30/0.60 === Conflict found: 189:3:0:[179.1,188.1,36.1]:: -> vertical_5_5,horizontal_6_2,vertical_5_3 {}
% 0.30/0.60 === Backtracking. Learning clause 197:4:0:[189.2,174.1,163.2,187.1,155.1,29.2,156.1]:: vertical_4_3 -> vertical_4_6,horizontal_5_1,vertical_4_2
% 0.30/0.60 === Backtracking. Learning clause 198:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,107.1,105.1,94.1,193.4,84.1,83.1,80.1,14.2,81.1]:: vertical_2_1,vertical_1_6 -> vertical_2_2,horizontal_2_4,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 199:3:0:[173.1,189.2,34.1,167.1,154.1]:: vertical_4_5,horizontal_5_2 -> vertical_5_1
% 0.30/0.60 === Backtracking. Learning clause 200:5:0:[175.1,34.1,29.2,199.2,144.1,143.1,26.2]:: vertical_4_1 -> vertical_4_2,horizontal_4_5,horizontal_4_4,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 201:4:0:[175.1,34.1,29.2,192.1,144.1,143.1,139.1,200.3,129.1,119.1,22.2,120.1,103.2]:: vertical_3_4,vertical_3_2,horizontal_3_5 -> vertical_3_1
% 0.30/0.60 === Backtracking. Learning clause 202:6:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,201.3,19.2]:: vertical_3_2 -> vertical_2_6,vertical_3_1,horizontal_3_4,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 203:5:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,104.1,202.4]:: vertical_3_2 -> vertical_2_6,vertical_3_1,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 204:4:0:[175.1,34.1,29.2,192.1,144.1,143.1,139.1,200.3,128.1]:: vertical_4_1,horizontal_4_3 -> vertical_4_2,vertical_3_5
% 0.30/0.60 === Conflict found: 197:4:0:[189.2,174.1,163.2,187.1,155.1,29.2,156.1]:: vertical_4_3 -> vertical_4_6,horizontal_5_1,vertical_4_2 {}
% 0.30/0.60 === Backtracking. Learning clause 205:5:0:[197.3,143.1,139.1,200.3]:: vertical_4_3,vertical_4_1 -> vertical_4_2,horizontal_4_4,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 206:4:0:[175.1,34.1,29.2,156.1,144.1,143.1,24.2,204.2,119.1,117.1,22.2,120.1,103.2]:: vertical_3_2,horizontal_3_5 -> vertical_3_3,vertical_3_1
% 0.30/0.60 === Backtracking. Learning clause 207:6:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,206.2,91.2,203.4,17.2]:: -> vertical_2_6,vertical_3_1,vertical_2_4,horizontal_3_2,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 208:5:0:[173.1,189.2,34.1,167.1,155.1,144.1,26.2]:: vertical_4_3,vertical_4_1 -> horizontal_4_5,horizontal_4_4,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 209:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,144.1,139.1,208.3,129.1,24.2,132.1]:: vertical_4_1,vertical_3_4 -> vertical_3_5,horizontal_4_2,vertical_3_3
% 0.30/0.60 === Backtracking. Learning clause 210:5:0:[175.1,34.1,29.2,192.1,144.1,143.1,139.1,200.3,129.1,115.2,209.4,22.2]:: vertical_3_4 -> vertical_3_5,vertical_3_3,horizontal_4_1,vertical_3_1
% 0.30/0.60 === Conflict found: 189:3:0:[179.1,188.1,36.1]:: -> vertical_5_5,horizontal_6_2,vertical_5_3 {}
% 0.30/0.60 === Backtracking. Learning clause 211:4:0:[189.2,174.1,167.1,155.1,29.2,156.1]:: vertical_4_5,vertical_4_3 -> horizontal_5_1,vertical_4_2
% 0.30/0.60 === Backtracking. Learning clause 212:5:0:[173.1,189.2,34.1,167.1,155.1,142.2,211.3,26.2]:: vertical_4_3 -> vertical_4_2,horizontal_4_5,horizontal_4_4,vertical_3_5
% 0.30/0.60 === Backtracking. Learning clause 213:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,103.2]:: vertical_3_4,horizontal_3_5 -> vertical_3_3,vertical_3_1
% 0.30/0.60 === Backtracking. Learning clause 214:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,144.1,140.1,24.2,132.1]:: vertical_4_1,vertical_3_6,vertical_3_4 -> horizontal_4_2,vertical_3_3
% 0.30/0.60 === Backtracking. Learning clause 215:5:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,115.2,214.4,22.2]:: vertical_3_6,vertical_3_4 -> vertical_3_3,horizontal_4_1,vertical_3_1
% 0.30/0.60 === Backtracking. Learning clause 216:6:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,132.1,118.1,116.1,215.4,21.1,213.2,19.2]:: -> vertical_2_6,vertical_3_3,vertical_3_1,horizontal_3_4,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 217:2:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,94.1,92.1,207.4,84.1,83.1,80.1,67.2,198.4,59.1,186.2,60.1,9.1,50.1,49.1]:: vertical_1_2,horizontal_1_4 ->
% 0.30/0.60 === Backtracking. Learning clause 218:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,94.1,92.1,207.4,84.1,83.1,79.1]:: vertical_2_1,horizontal_2_5 -> vertical_2_4,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 219:5:0:[175.1,34.1,29.2,192.1,144.1,143.1,139.1,200.3,129.1,119.1,22.2,120.1,107.1,19.2,108.1]:: vertical_3_2,vertical_2_5 -> vertical_3_1,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 220:6:0:[175.1,34.1,29.2,156.1,144.1,143.1,24.2,204.2,119.1,117.1,22.2,120.1,107.1,91.2,219.4,17.2]:: vertical_2_5 -> vertical_3_1,vertical_2_4,horizontal_3_2,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 221:3:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,107.1,19.2,108.1,94.1,92.1,220.4,84.1,83.1,14.2,218.2,71.1,69.1,59.1,186.2,60.1,48.2]:: vertical_1_4,vertical_1_2,horizontal_1_5 ->
% 0.30/0.60 === Backtracking. Learning clause 222:2:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,94.1,92.1,207.4,84.1,83.1,80.1,71.1,59.1,186.2,60.1,9.1,221.3,7.2,217.2]:: vertical_1_2 -> horizontal_1_3
% 0.30/0.60 === Backtracking. Learning clause 223:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,107.1,19.2,108.1,94.1,92.1,220.4,84.1,83.1,14.2,218.2,70.1,68.1]:: vertical_2_1,horizontal_2_3 -> vertical_1_5,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 224:4:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,206.2,95.1,17.2,96.1,84.1,83.1,79.1]:: vertical_2_3,vertical_2_1,horizontal_2_5 -> vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 225:5:0:[175.1,34.1,29.2,156.1,144.1,143.1,24.2,204.2,119.1,117.1,22.2,120.1,107.1,95.1,17.2,96.1,84.1,83.1,14.2,224.3]:: vertical_2_3,vertical_2_1 -> horizontal_2_4,vertical_1_5,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 226:6:0:[175.1,34.1,29.2,156.1,144.1,143.1,24.2,132.1,119.1,117.1,22.2,120.1,19.2]:: vertical_3_2 -> vertical_3_3,vertical_3_1,horizontal_3_4,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 227:3:0:[175.1,34.1,29.2,156.1,144.1,143.1,24.2,204.2,119.1,117.1,22.2,120.1,106.1,226.4,95.1,93.1,17.2,96.1,84.1,83.1,67.2,225.3,12.2,223.2,59.1,57.1,186.2,60.1,48.2]:: vertical_1_2,horizontal_1_5 -> vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 228:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,94.1,92.1,207.4,84.1,83.1,80.1,70.1]:: vertical_2_1,vertical_1_6,horizontal_2_3 -> vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 229:1:0:[175.1,34.1,29.2,192.1,144.1,143.1,140.1,119.1,22.2,120.1,21.1,206.2,95.1,17.2,96.1,84.1,83.1,80.1,12.2,228.3,59.1,57.1,186.2,60.1,9.1,227.2,42.2,222.2,185.2]:: -> horizontal_1_2
% 0.30/0.60 === Conflict found: 190:3:0:[187.1,165.1,140.1,26.2,141.1]:: vertical_3_6 -> horizontal_4_4,vertical_3_5 {}
% 0.30/0.60 === Backtracking. Learning clause 230:4:0:[190.2,129.1,21.1,107.1,105.1,19.2,108.1]:: vertical_2_5 -> vertical_2_6,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 231:6:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,119.1,117.1,21.1,107.1,105.1,91.2,230.3,17.2]:: vertical_2_5 -> vertical_2_6,vertical_2_4,horizontal_3_2,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 232:5:0:[92.1,230.3,231.4]:: vertical_2_5 -> vertical_2_6,vertical_2_4,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 233:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,107.1,105.1,91.2,230.3,82.2,232.4,80.1,14.2,81.1,70.1,68.1]:: vertical_1_6,horizontal_2_3 -> vertical_2_2,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 234:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,119.1,117.1,21.1,107.1,105.1,95.1,17.2,96.1]:: vertical_2_5,vertical_2_3 -> vertical_2_6,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 235:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,107.1,105.1,95.1,82.2,234.4,80.1,14.2,81.1]:: vertical_2_3,vertical_1_6 -> vertical_2_2,horizontal_2_4,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 236:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,119.1,117.1,103.2]:: vertical_3_4,vertical_3_2,horizontal_3_5 -> vertical_3_3
% 0.30/0.60 === Backtracking. Learning clause 237:6:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,132.1,119.1,117.1,21.1,236.3,19.2]:: vertical_3_2 -> vertical_2_6,vertical_3_3,horizontal_3_4,horizontal_3_3,vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 238:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,119.1,117.1,21.1,106.1,104.1,237.4,95.1,93.1,17.2,96.1]:: vertical_2_3 -> vertical_2_6,vertical_2_4,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 239:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,82.2,238.4,80.1,67.2,235.4,12.2,233.2,58.1,56.1]:: vertical_1_6,horizontal_2_1 -> vertical_1_3,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 240:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,107.1,105.1,91.2,230.3,84.1,80.1,14.2,81.1,70.1,68.1]:: vertical_2_1,vertical_1_6,horizontal_2_3 -> vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 241:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,107.1,105.1,95.1,84.1,80.1,14.2,81.1]:: vertical_2_3,vertical_2_1,vertical_1_6 -> horizontal_2_4,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 242:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,84.1,80.1,67.2,241.4,12.2,240.3]:: vertical_2_1,vertical_1_6 -> horizontal_2_2,vertical_1_3,vertical_1_5
% 0.30/0.60 === Backtracking. Learning clause 243:2:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,94.1,92.1,207.4,84.1,83.1,80.1,67.2,198.4,55.2,242.3,186.2,239.2,9.1,50.1,49.1]:: horizontal_1_4 -> vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 244:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,82.2,238.4,79.1]:: vertical_2_3,horizontal_2_5 -> vertical_2_4,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 245:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,119.1,117.1,107.1,19.2,108.1,95.1,93.1,17.2,96.1]:: vertical_2_5,vertical_2_3 -> vertical_2_4,horizontal_3_1,vertical_2_2
% 0.30/0.60 === Backtracking. Learning clause 246:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,107.1,19.2,108.1,95.1,93.1,82.2,245.4,14.2,244.2,71.1,69.1,12.2,72.1,58.1,56.1]:: vertical_1_4,horizontal_2_1 -> vertical_1_5,vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 247:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,84.1,79.1]:: vertical_2_3,vertical_2_1,horizontal_2_5 -> vertical_2_4
% 0.30/0.60 === Backtracking. Learning clause 248:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,107.1,19.2,108.1,95.1,93.1,84.1,14.2,247.3,71.1,69.1,12.2,72.1]:: vertical_2_1,vertical_1_4 -> vertical_1_5,horizontal_2_2,vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 249:3:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,139.1,212.3,129.1,24.2,132.1,118.1,116.1,210.4,107.1,19.2,108.1,94.1,92.1,220.4,84.1,83.1,14.2,218.2,71.1,69.1,55.2,248.4,186.2,246.2,48.2]:: vertical_1_4,horizontal_1_5 -> vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 250:4:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,82.2,238.4,80.1,71.1,12.2,72.1,58.1,56.1]:: vertical_1_6,vertical_1_4,horizontal_2_1 -> vertical_1_3
% 0.30/0.60 === Backtracking. Learning clause 251:5:0:[173.1,189.2,34.1,163.2,187.1,155.1,142.2,197.3,140.1,24.2,194.1,118.1,116.1,196.4,21.1,106.1,104.1,216.4,95.1,93.1,84.1,80.1,71.1,12.2,72.1]:: vertical_2_1,vertical_1_6,vertical_1_4 -> horizontal_2_2,vertical_1_3
% 0.30/0.60
% 0.30/0.60 SZS status Unsatisfiable
% 0.30/0.60
% 0.30/0.60 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.60
% 0.30/0.60 SPASS-SCL-FOL Statistics:
% 0.30/0.60 Number of learned clauses: 63
% 0.30/0.60 Number of propagations: 1899
% 0.30/0.60 Number of decisions: 104
% 0.30/0.60 Number of resolutions: 1055
% 0.30/0.60 Number of condensations: 0
% 0.30/0.60 Number of sub resolutions: 4
% 0.30/0.60 Number of input literals (deduplicated): 60
% 0.30/0.60 Number of grows: 1
% 0.30/0.60 Number of considered ground atoms: 56
% 0.30/0.60
% 0.30/0.60 Needed: 0:00:00.01
% 0.30/0.60
%------------------------------------------------------------------------------