%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV006-2 : TPTP v9.2.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 1.74s 0.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV006-2 : TPTP v9.2.1. Bugfixed v2.7.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 : n017.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:04:28 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]
% 1.74/0.86 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86 Execution lmodel_grow ended with status: unsatisfiable
% 1.74/0.86 Used heuristic: lmodel_grow
% 1.74/0.86
% 1.74/0.86 Input Clauses:
% 1.74/0.86
% 1.74/0.86 Predicates: connection zero one and_ok abnormal logic_and or_ok logic_or not_ok logic_not halfadder fulladder
% 1.74/0.86 Fol Constants: f
% 1.74/0.86 Fol Functions: in1 out1 in2 and1 and2 not1 or1 outs outc h1 h2 inc
% 1.74/0.86 Problem Properties:
% 1.74/0.86 This is a full first-order problem without equality.
% 1.74/0.86
% 1.74/0.86 After reduction: Problem Properties:
% 1.74/0.86 This is a full first-order problem without equality.
% 1.74/0.86
% 1.74/0.86
% 1.74/0.86 Reduced Input Clauses:
% 1.74/0.86
% 1.74/0.86 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)
% 1.74/0.86
% 1.74/0.86 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: lmodel_grow ===
% 1.74/0.86
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 73
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 86
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 105
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 114
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 126
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 133
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 145
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 151
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 159
% 1.74/0.86 === Backtracking. Learning clause 65:4:2:[1.1,37.2,1.2]:TopTop: zero(outc(x0)),halfadder(x0),connection(out1(and2(x0)),x1) -> zero(x1)
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 164
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 169
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 173
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 177
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 180
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 184
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 191
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 197
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 208
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 218
% 1.74/0.86 === Backtracking. Learning clause 66:6:3:[21.1,31.2,19.1,3.3,3.2]:TopTopTop: halfadder(x0),connection(out1(or1(x0)),x1),zero(x1),connection(x2,in2(or1(x0))) -> abnormal(or1(x0)),zero(x2)
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 226
% 1.74/0.86 === Backtracking. Learning clause 67:5:2:[9.3,3.2]:TopTop: and_ok(x0),zero(out1(x0)),connection(x1,in1(x0)) -> zero(in2(x0)),zero(x1)
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 235
% 1.74/0.86 === Backtracking. Learning clause 68:8:4:[13.1,29.2,67.1,3.2,5.1,2.3]:TopTopTopTop: halfadder(x0),zero(out1(and2(x0))),connection(x1,in1(and2(x0))),connection(x2,in2(and2(x0))),connection(x3,x2),one(x3) -> abnormal(and2(x0)),zero(x1)
% 1.74/0.86 === Backtracking. Learning clause 69:19:7:[8.3,2.3,4.2,22.3,65.4,13.2,3.3,68.6,34.2,28.2,27.2,1.3,39.2,1.3,3.3,2.3,15.3,30.2,2.3,36.2,37.2,21.2,31.2,33.2,40.2,3.2,38.2,2.3,18.3,1.3,35.2,21.2,60.1]:TopTopTopTopTopTopTop: connection(outc(x0),x1),connection(outs(x0),in2(x2)),connection(x3,x1),zero(x3),connection(outc(x2),in1(or1(f))),connection(x4,in1(x2)),halfadder(x0),connection(x5,in2(x0)),one(x5),connection(x6,out1(or1(f))),zero(x6),halfadder(x2),logic_or(or1(f)),abnormal(and1(h2(f))) -> abnormal(and1(x0)),abnormal(and2(x2)),abnormal(not1(x0)),abnormal(or1(x0)),zero(x4)
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 246
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 253
% 1.74/0.86 === Backtracking. Learning clause 70:4:3:[4.2,2.3]:TopTopTop: connection(x0,x1),connection(x2,x1),one(x2) -> one(x0)
% 1.74/0.86 === Backtracking. Learning clause 71:2:0:[21.3,61.1]:: logic_or(or1(h1(f))) -> or_ok(or1(h1(f)))
% 1.74/0.86 === Clause set with instances from active satisfied. Growing active. New size: 267
% 1.74/0.86 === Backtracking. Learning clause 72:4:3:[1.2,3.3]:TopTopTop: connection(x0,x1),connection(x0,x2),zero(x2) -> zero(x1)
% 1.74/0.86 === Backtracking. Learning clause 74:11:4:[52.0,73.9,11.3,4.2,2.3,25.2,2.3,13.2,3.2,39.2,56.1,27.2,30.2,40.2,58.2,60.2,21.3,18.1,1.3,57.1,36.2,72.3,68.2,59.1,28.2,51.2,3.2,47.2]:TopTopTopTop: connection(outs(f),outs(h2(f))),logic_or(or1(f)),connection(x0,out1(and2(h2(f)))),connection(x0,in1(or1(f))),connection(in1(h2(x1)),in1(and2(h2(f)))),connection(x2,in2(and2(h2(f)))),connection(x3,x2),one(x3),halfadder(h2(f)),fulladder(x1) -> zero(in1(x1))
% 1.74/0.86 === Backtracking. Learning clause 75:11:3:[25.2,4.3,27.2,11.3,58.2,13.2,3.2,60.2,21.3,18.1,72.3]:TopTopTop: connection(out1(not1(h2(f))),in2(and1(h2(f)))),logic_not(not1(h2(f))),one(out1(and1(h2(f)))),logic_and(and1(h2(f))),connection(x0,in1(not1(h2(f)))),logic_or(or1(f)),zero(out1(or1(f))),connection(x1,x2),connection(x1,in1(or1(f))) -> zero(x0),zero(x2)
% 1.74/0.86 === Conflict found: 69:19:7:[8.3,2.3,4.2,22.3,65.4,13.2,3.3,68.6,34.2,28.2,27.2,1.3,39.2,1.3,3.3,2.3,15.3,30.2,2.3,36.2,37.2,21.2,31.2,33.2,40.2,3.2,38.2,2.3,18.3,1.3,35.2,21.2,60.1]:TopTopTopTopTopTopTop: connection(outc(x0),x1),connection(outs(x0),in2(x2)),connection(x3,x1),zero(x3),connection(outc(x2),in1(or1(f))),connection(x4,in1(x2)),halfadder(x0),connection(x5,in2(x0)),one(x5),connection(x6,out1(or1(f))),zero(x6),halfadder(x2),logic_or(or1(f)),abnormal(and1(h2(f))) -> abnormal(and1(x0)),abnormal(and2(x2)),abnormal(not1(x0)),abnormal(or1(x0)),zero(x4) {x0 -> h1(f), x1 -> in2(or1(f)), x2 -> h2(f), x3 -> outc(h1(f)), x4 -> in1(f), x5 -> inc(f), x6 -> outc(f)}
% 1.74/0.86 === Backtracking. Learning clause 78:15:5:[3.2,76.8,61.0,77.15,69.15,64.1,62.1,55.1,3.3,19.3,21.2,60.1]:TopTopTopTopTop: connection(outc(h1(f)),x0),connection(outs(h1(f)),in2(x1)),connection(x2,x0),connection(outc(x1),in1(or1(f))),connection(x3,in1(x1)),halfadder(h1(f)),connection(inc(f),in2(h1(f))),connection(x4,out1(or1(f))),halfadder(x1),connection(x2,in2(or1(f))),zero(out1(or1(f))),logic_or(or1(f)),abnormal(and1(h2(f))) -> abnormal(and2(x1)),zero(x3)
% 1.74/0.86 === Backtracking. Learning clause 79:12:3:[8.3,2.3,2.3,22.3,15.3,2.3,2.3,27.2,30.2,40.2,33.2,4.2,65.4,39.2,13.2,55.1,62.1,64.1,3.3,19.3,21.2]:TopTopTop: connection(out1(or1(x0)),in1(and1(h1(f)))),or_ok(or1(x0)),connection(inc(f),in2(x0)),halfadder(x0),connection(x1,out1(and1(h1(f)))),halfadder(h1(f)),logic_and(and1(h1(f))),connection(outc(h1(f)),in2(x2)),zero(out1(x2)),logic_or(x2) -> one(x1),abnormal(x2)
% 1.74/0.86 === Backtracking. Learning clause 80:6:2:[4.1,40.2,11.3,2.3,2.3,56.1,25.2,27.2,30.2,36.2,3.2]:TopTop: and_ok(and1(x0)),connection(outs(f),outs(x0)),halfadder(x0),connection(x1,in1(not1(x0))) -> abnormal(not1(x0)),zero(x1)
% 1.74/0.86
% 1.74/0.86 SZS status Unsatisfiable
% 1.74/0.86
% 1.74/0.86 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.74/0.86
% 1.74/0.86 SPASS-SCL-FOL Statistics:
% 1.74/0.86 Number of learned clauses: 13
% 1.74/0.86 Number of propagations: 1068
% 1.74/0.86 Number of decisions: 278
% 1.74/0.86 Number of resolutions: 164
% 1.74/0.86 Number of condensations: 0
% 1.74/0.86 Number of sub resolutions: 3
% 1.74/0.86 Number of input literals (deduplicated): 55
% 1.74/0.86 Number of grows: 24
% 1.74/0.86 Number of considered ground atoms: 267
% 1.74/0.86
% 1.74/0.86 Needed: 0:00:00.32
% 1.74/0.86
%------------------------------------------------------------------------------