%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV008-2.002 : TPTP v9.2.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.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:24:05 PM UTC 2026
% Result : Unsatisfiable 182.51s 46.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV008-2.002 : TPTP v9.2.1. Bugfixed v2.7.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n022.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:05:52 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]
% 182.51/46.15 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15 Execution lmodel_grow ended with status: unsatisfiable
% 182.51/46.15 Used heuristic: lmodel_grow
% 182.51/46.15
% 182.51/46.15 Input Clauses:
% 182.51/46.15
% 182.51/46.15 Predicates: connection zero one and_ok abnormal logic_and or_ok logic_or not_ok logic_not halfadder fulladder nbit_adder2
% 182.51/46.15 Fol Constants: a
% 182.51/46.15 Fol Functions: in1 out1 in2 and1 and2 not1 or1 outs outc h1 h2 inc f1 f2 out2 ina1 inb1 ina2 inb2
% 182.51/46.15 Problem Properties:
% 182.51/46.15 This is a full first-order problem without equality.
% 182.51/46.15
% 182.51/46.15 After reduction: Problem Properties:
% 182.51/46.15 This is a full first-order problem without equality.
% 182.51/46.15
% 182.51/46.15
% 182.51/46.15 Reduced Input Clauses:
% 182.51/46.15
% 182.51/46.15 Most General Atoms: connection(x0,x1) zero(x1) one(x1) and_ok(x0) abnormal(x0) logic_and(x0) or_ok(x0) logic_or(x0) not_ok(x0) logic_not(x0) halfadder(x0) fulladder(x0) nbit_adder2(x0)
% 182.51/46.15
% 182.51/46.15 === Starting SPASS-SCL-FOL A Little Less Naive, considering 65 atoms initially, heuristics mode: lmodel_grow ===
% 182.51/46.15
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 86
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 97
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 104
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 109
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 114
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 125
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 156
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 172
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 186
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 192
% 182.51/46.15 === Backtracking. Learning clause 75:2:1:[29.1,41.2]:Top: fulladder(x0) -> logic_and(and2(h1(x0)))
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 204
% 182.51/46.15 === Backtracking. Learning clause 76:3:1:[14.2,24.3,5.2]:Top: or_ok(x0),not_ok(x0),zero(out1(x0)) ->
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 212
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 217
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 221
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 225
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 233
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 238
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 242
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 249
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 256
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 262
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 269
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 277
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 286
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 295
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 303
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 310
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 321
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 331
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 342
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 351
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 361
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 365
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 369
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 379
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 386
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 392
% 182.51/46.15 === Backtracking. Learning clause 77:7:3:[2.3,8.3,35.2,2.3,2.3]:TopTopTop: and_ok(and2(x0)),one(in1(and2(x0))),halfadder(x0),connection(x1,in2(x0)),connection(x2,x1),one(x2) -> one(out1(and2(x0)))
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 401
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 409
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 413
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 417
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 422
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 428
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 433
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 436
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 442
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 449
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 455
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 467
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 478
% 182.51/46.15 === Backtracking. Learning clause 78:7:3:[4.2,17.3,2.2,10.2]:TopTopTop: connection(x0,in1(x1)),or_ok(x1),one(out1(x1)),connection(x0,out1(x2)),and_ok(x2) -> one(in2(x1)),one(in1(x2))
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 486
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 493
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 496
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 503
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 509
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 519
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 527
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 539
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 545
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 551
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 558
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 563
% 182.51/46.15 === Backtracking. Learning clause 79:5:3:[3.2,19.3,1.2]:TopTopTop: connection(x0,in2(x1)),or_ok(x1),zero(out1(x1)),connection(x0,x2) -> zero(x2)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 570
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 579
% 182.51/46.15 === Backtracking. Learning clause 80:5:4:[4.2,2.3,2.2]:TopTopTopTop: connection(x0,x1),connection(x2,x1),one(x2),connection(x0,x3) -> one(x3)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 590
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 596
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 604
% 182.51/46.15 === Backtracking. Learning clause 81:3:1:[37.2,1.1]:Top: halfadder(x0),zero(outc(x0)) -> zero(out1(and2(x0)))
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 615
% 182.51/46.15 === Backtracking. Learning clause 82:4:2:[4.2,11.3]:TopTop: connection(x0,in2(x1)),and_ok(x1),one(out1(x1)) -> one(x0)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 622
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 627
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 634
% 182.51/46.15 === Conflict found: 79:5:3:[3.2,19.3,1.2]:TopTopTop: connection(x0,in2(x1)),or_ok(x1),zero(out1(x1)),connection(x0,x2) -> zero(x2) {x0 -> outc(h1(f1(a))), x1 -> or1(f1(a)), x2 -> out1(and2(h1(a)))}
% 182.51/46.15 === Backtracking. Learning clause 83:6:4:[79.3,1.3]:TopTopTopTop: connection(x0,in2(x1)),or_ok(x1),connection(x0,x2),connection(x3,out1(x1)),zero(x3) -> zero(x2)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 651
% 182.51/46.15 === Backtracking. Learning clause 84:6:4:[5.2,80.5,18.3]:TopTopTopTop: connection(x0,x1),connection(x2,x1),one(x2),connection(x0,in1(x3)),or_ok(x3),zero(out1(x3)) ->
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 665
% 182.51/46.15 === Backtracking. Learning clause 85:4:3:[1.2,3.3]:TopTopTop: connection(x0,x1),connection(x0,x2),zero(x2) -> zero(x1)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 672
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 685
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 695
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 705
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 713
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 722
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 731
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 737
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 747
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 757
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 766
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 774
% 182.51/46.15 === Backtracking. Learning clause 86:6:3:[4.1,34.2,4.2,4.2,10.3]:TopTopTop: halfadder(x0),connection(x1,in1(x0)),connection(x2,x1),and_ok(and2(x0)),one(out1(and2(x0))) -> one(x2)
% 182.51/46.15 === Backtracking. Learning clause 87:14:7:[4.2,78.6,80.3,86.5,37.2,37.2]:TopTopTopTopTopTopTop: connection(x0,in2(x1)),connection(outc(x2),in1(x1)),or_ok(x1),one(out1(x1)),and_ok(and2(x2)),connection(outc(x3),x4),connection(x0,x4),connection(x5,in1(x3)),connection(x6,x5),and_ok(and2(x3)),halfadder(x2),halfadder(x3) -> one(in1(and2(x2))),one(x6)
% 182.51/46.15 === Clause set with instances from active satisfied. Growing active. New size: 789
% 182.51/46.15
% 182.51/46.15 SZS status Unsatisfiable
% 182.51/46.15
% 182.51/46.15 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.51/46.15
% 182.51/46.15 SPASS-SCL-FOL Statistics:
% 182.51/46.15 Number of learned clauses: 13
% 182.51/46.15 Number of propagations: 3309
% 182.51/46.15 Number of decisions: 2392
% 182.51/46.15 Number of resolutions: 61
% 182.51/46.15 Number of condensations: 0
% 182.51/46.15 Number of sub resolutions: 0
% 182.51/46.15 Number of input literals (deduplicated): 65
% 182.51/46.15 Number of grows: 86
% 182.51/46.15 Number of considered ground atoms: 789
% 182.51/46.15
% 182.51/46.15 Needed: 0:0:45.59
% 182.51/46.16
%------------------------------------------------------------------------------