%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV007-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 : n025.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 33.61s 8.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : HWV007-2 : TPTP v9.2.1. Bugfixed v2.7.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.32 % Computer : n025.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Thu May 7 12:05:59 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.32 SPASS-SCL-FOL version:
% 0.19/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 33.61/8.80 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80 Execution resolution_1 ended with status: unsatisfiable
% 33.61/8.80 Used heuristic: resolution_1
% 33.61/8.80
% 33.61/8.80 Input Clauses:
% 33.61/8.80
% 33.61/8.80 Predicates: connection zero one and_ok abnormal logic_and or_ok logic_or not_ok logic_not halfadder fulladder
% 33.61/8.80 Fol Constants: f
% 33.61/8.80 Fol Functions: in1 out1 in2 and1 and2 not1 or1 outs outc h1 h2 inc
% 33.61/8.80 Problem Properties:
% 33.61/8.80 This is a full first-order problem without equality.
% 33.61/8.80
% 33.61/8.80 After reduction: Problem Properties:
% 33.61/8.80 This is a full first-order problem without equality.
% 33.61/8.80
% 33.61/8.80
% 33.61/8.80 Reduced Input Clauses:
% 33.61/8.80
% 33.61/8.80 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)
% 33.61/8.80
% 33.61/8.80 === Starting SPASS-SCL-FOL A Little Less Naive, considering 52 atoms initially, heuristics mode: resolution_1 ===
% 33.61/8.80
% 33.61/8.80 === Backtracking. Learning clause 63:2:0:[24.3,5.2,6.3,53.1]:: not_ok(f),and_ok(f) ->
% 33.61/8.80 === Backtracking. Learning clause 64:2:0:[5.2,54.1,19.3,6.3,53.1]:: or_ok(f),and_ok(f) ->
% 33.61/8.80 === Backtracking. Learning clause 65:1:0:[5.2,54.1]:: zero(in2(f)) ->
% 33.61/8.80 === Backtracking. Learning clause 66:1:0:[5.2,56.1]:: zero(outs(f)) ->
% 33.61/8.80 === Backtracking. Learning clause 67:3:1:[13.1,28.2]:Top: halfadder(x0) -> and_ok(and1(x0)),abnormal(and1(x0))
% 33.61/8.80 === Backtracking. Learning clause 68:3:1:[13.1,29.2]:Top: halfadder(x0) -> and_ok(and2(x0)),abnormal(and2(x0))
% 33.61/8.80 === Backtracking. Learning clause 69:3:1:[21.1,31.2]:Top: halfadder(x0) -> or_ok(or1(x0)),abnormal(or1(x0))
% 33.61/8.80 === Backtracking. Learning clause 70:3:1:[27.1,30.2]:Top: halfadder(x0) -> not_ok(not1(x0)),abnormal(not1(x0))
% 33.61/8.80 === Backtracking. Learning clause 71:3:1:[1.1,34.2]:Top: zero(in1(x0)),halfadder(x0) -> zero(in1(and2(x0)))
% 33.61/8.80 === Backtracking. Learning clause 72:3:1:[1.1,32.2]:Top: zero(in1(x0)),halfadder(x0) -> zero(in1(or1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 73:3:1:[2.1,35.2]:Top: one(in2(x0)),halfadder(x0) -> one(in2(and2(x0)))
% 33.61/8.80 === Backtracking. Learning clause 74:4:1:[2.1,33.2,5.2,19.3]:Top: one(in2(x0)),halfadder(x0),or_ok(or1(x0)),zero(out1(or1(x0))) ->
% 33.61/8.80 === Backtracking. Learning clause 75:3:1:[2.1,36.2]:Top: one(outs(x0)),halfadder(x0) -> one(out1(and1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 76:3:1:[1.1,37.2]:Top: zero(outc(x0)),halfadder(x0) -> zero(out1(and2(x0)))
% 33.61/8.80 === Backtracking. Learning clause 77:3:1:[1.1,39.2,76.3]:Top: zero(outc(x0)),halfadder(x0) -> zero(in1(not1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 78:3:1:[2.1,38.2]:Top: one(out1(or1(x0))),halfadder(x0) -> one(in1(and1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 79:4:1:[2.1,33.2,15.2,78.1]:Top: one(in2(x0)),or_ok(or1(x0)),halfadder(x0) -> one(in1(and1(x0)))
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 96
% 33.61/8.80 === Restarting.
% 33.61/8.80 === Backtracking. Learning clause 80:3:1:[21.1,43.2]:Top: fulladder(x0) -> or_ok(or1(x0)),abnormal(or1(x0))
% 33.61/8.80 === Backtracking. Learning clause 81:3:1:[24.3,5.2,6.3]:Top: not_ok(x0),and_ok(x0),zero(in1(x0)) ->
% 33.61/8.80 === Backtracking. Learning clause 82:3:1:[2.1,48.2]:Top: one(in2(x0)),fulladder(x0) -> one(in1(h1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 83:3:1:[2.1,50.2,5.2]:Top: one(outs(x0)),fulladder(x0),zero(outs(h2(x0))) ->
% 33.61/8.80 === Backtracking. Learning clause 84:3:1:[2.1,50.2]:Top: one(outs(x0)),fulladder(x0) -> one(outs(h2(x0)))
% 33.61/8.80 === Backtracking. Learning clause 85:4:1:[1.1,51.2,18.2]:Top: zero(outc(x0)),fulladder(x0),or_ok(or1(x0)) -> zero(in1(or1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 86:5:1:[4.1,51.2,22.3,85.4]:Top: not_ok(or1(x0)),zero(outc(x0)),fulladder(x0),or_ok(or1(x0)) -> one(outc(x0))
% 33.61/8.80 === Backtracking. Learning clause 87:3:1:[4.1,51.2]:Top: one(out1(or1(x0))),fulladder(x0) -> one(outc(x0))
% 33.61/8.80 === Backtracking. Learning clause 88:3:1:[1.1,51.2]:Top: zero(outc(x0)),fulladder(x0) -> zero(out1(or1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 89:3:1:[2.1,49.2,5.2]:Top: one(inc(x0)),fulladder(x0),zero(in2(h1(x0))) ->
% 33.61/8.80 === Backtracking. Learning clause 90:3:1:[2.1,44.2]:Top: one(outs(h1(x0))),fulladder(x0) -> one(in2(h2(x0)))
% 33.61/8.80 === Backtracking. Learning clause 91:3:1:[3.1,44.2]:Top: zero(in2(h2(x0))),fulladder(x0) -> zero(outs(h1(x0)))
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 102
% 33.61/8.80 === Restarting.
% 33.61/8.80 === Conflict found: 81:3:1:[24.3,5.2,6.3]:Top: not_ok(x0),and_ok(x0),zero(in1(x0)) -> {x0 -> not1(f)}
% 33.61/8.80 === Backtracking. Learning clause 92:3:1:[81.3,77.3,70.2,12.2]:Top: zero(outc(x0)),halfadder(x0),and_ok(not1(x0)) ->
% 33.61/8.80 === Conflict found: 74:4:1:[2.1,33.2,5.2,19.3]:Top: one(in2(x0)),halfadder(x0),or_ok(or1(x0)),zero(out1(or1(x0))) -> {x0 -> f}
% 33.61/8.80 === Backtracking. Learning clause 93:5:1:[74.4,88.3,69.2]:Top: one(in2(x0)),zero(outc(x0)),fulladder(x0),halfadder(x0) -> abnormal(or1(x0))
% 33.61/8.80 === Backtracking. Learning clause 94:5:1:[23.2,82.3,18.2,81.3]:Top: one(in2(x0)),fulladder(x0),or_ok(h1(x0)),not_ok(h1(x0)),and_ok(h1(x0)) ->
% 33.61/8.80 === Backtracking. Learning clause 95:3:1:[5.2,73.3]:Top: zero(in2(and2(x0))),one(in2(x0)),halfadder(x0) ->
% 33.61/8.80 === Conflict found: 67:3:1:[13.1,28.2]:Top: halfadder(x0) -> and_ok(and1(x0)),abnormal(and1(x0)) {x0 -> h1(f)}
% 33.61/8.80 === Backtracking. Learning clause 96:3:0:[67.3,59.2]:: halfadder(h1(f)),abnormal(or1(f)) -> and_ok(and1(h1(f)))
% 33.61/8.80 === Conflict found: 68:3:1:[13.1,29.2]:Top: halfadder(x0) -> and_ok(and2(x0)),abnormal(and2(x0)) {x0 -> h1(f)}
% 33.61/8.80 === Backtracking. Learning clause 97:2:0:[68.3,58.1]:: halfadder(h1(f)) -> and_ok(and2(h1(f)))
% 33.61/8.80 === Backtracking. Learning clause 98:3:1:[2.1,33.2,5.2]:Top: one(in2(x0)),halfadder(x0),zero(in2(or1(x0))) ->
% 33.61/8.80 === Backtracking. Learning clause 99:3:1:[2.1,49.2]:Top: one(inc(x0)),fulladder(x0) -> one(in2(h1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 100:4:1:[2.1,40.2,5.2,22.3]:Top: halfadder(x0),zero(in2(and1(x0))),not_ok(not1(x0)),zero(in1(not1(x0))) ->
% 33.61/8.80 === Backtracking. Learning clause 101:4:1:[4.1,38.2,87.1]:Top: one(in1(and1(x0))),halfadder(x0),fulladder(x0) -> one(outc(x0))
% 33.61/8.80 === Backtracking. Learning clause 102:4:1:[1.1,38.2,88.3]:Top: halfadder(x0),zero(outc(x0)),fulladder(x0) -> zero(in1(and1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 103:3:1:[4.1,45.2]:Top: one(in2(or1(x0))),fulladder(x0) -> one(outc(h1(x0)))
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 106
% 33.61/8.80 === Restarting.
% 33.61/8.80 === Backtracking. Learning clause 104:1:0:[5.2,55.1]:: zero(inc(f)) ->
% 33.61/8.80 === Backtracking. Learning clause 105:5:1:[9.4,89.3]:Top: and_ok(h1(x0)),zero(out1(h1(x0))),one(inc(x0)),fulladder(x0) -> zero(in1(h1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 106:5:1:[23.2,82.3,105.2,81.3]:Top: one(in2(x0)),one(inc(x0)),fulladder(x0),not_ok(h1(x0)),and_ok(h1(x0)) ->
% 33.61/8.80 === Backtracking. Learning clause 107:3:1:[5.2,82.3]:Top: zero(in1(h1(x0))),one(in2(x0)),fulladder(x0) ->
% 33.61/8.80 === Backtracking. Learning clause 108:3:1:[4.1,44.2]:Top: one(in2(h2(x0))),fulladder(x0) -> one(outs(h1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 109:3:1:[2.1,45.2]:Top: one(outc(h1(x0))),fulladder(x0) -> one(in2(or1(x0)))
% 33.61/8.80 === Backtracking. Learning clause 110:3:1:[3.1,45.2]:Top: zero(in2(or1(x0))),fulladder(x0) -> zero(outc(h1(x0)))
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 170
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 234
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 298
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 362
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 426
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 490
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 554
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 618
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 682
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 746
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 810
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 874
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 938
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1002
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1066
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1130
% 33.61/8.80 === Backtracking. Learning clause 115:1:0:[55.0,111.0,57.0,112.1,54.0,113.2,52.0,114.3,9.3,3.2,95.1,76.3,34.2,97.2,99.3,110.3,19.3,88.3,107.1,41.2,80.2,12.2]:: and_ok(or1(f)) ->
% 33.61/8.80 === Conflict found: 82:3:1:[2.1,48.2]:Top: one(in2(x0)),fulladder(x0) -> one(in1(h1(x0))) {x0 -> f}
% 33.61/8.80 === Backtracking. Learning clause 116:1:0:[82.2,52.1,54.1,5.2]:: zero(in1(h1(f))) ->
% 33.61/8.80 === Conflict found: 82:3:1:[2.1,48.2]:Top: one(in2(x0)),fulladder(x0) -> one(in1(h1(x0))) {x0 -> f}
% 33.61/8.80 === Backtracking. Learning clause 117:1:0:[82.2,52.1,54.1]:: -> one(in1(h1(f)))
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1194
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1258
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1322
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1386
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1450
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1514
% 33.61/8.80 === Backtracking. Learning clause 118:5:2:[9.4,3.2]:TopTop: and_ok(x0),zero(out1(x0)),connection(x1,in2(x0)) -> zero(in1(x0)),zero(x1)
% 33.61/8.80 === Backtracking. Learning clause 119:4:2:[1.3,3.2,34.2,1.3,42.2,47.2]:TopTop: connection(x0,in1(and2(h2(x1)))),zero(in1(x1)),fulladder(x1) -> zero(x0)
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1578
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1642
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1706
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1770
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1834
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1898
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 1962
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 2026
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 2090
% 33.61/8.80 === Backtracking. Learning clause 120:7:3:[17.4,4.2,4.3,108.1]:TopTopTop: or_ok(x0),connection(in2(h2(x1)),in2(x0)),connection(out1(x0),x2),one(x2),fulladder(x1) -> one(in1(x0)),one(outs(h1(x1)))
% 33.61/8.80 === Backtracking. Learning clause 121:3:1:[13.3,26.2,81.2]:Top: logic_and(x0),not_ok(x0),zero(in1(x0)) ->
% 33.61/8.80 === Backtracking. Learning clause 123:8:1:[52.0,122.2,10.2,75.3,120.4,21.2,67.2,5.2,62.2,31.2,33.2]:Top: one(outs(x0)),connection(out1(or1(h2(f))),in1(and1(x0))),halfadder(x0),zero(in1(or1(h2(f)))),abnormal(or1(f)),halfadder(h2(f)) -> one(outs(h1(f))),abnormal(and1(x0))
% 33.61/8.80 === Backtracking. Learning clause 124:3:1:[27.2,81.1,12.2]:Top: logic_not(x0),zero(in1(x0)),and_ok(x0) ->
% 33.61/8.80 === Backtracking. Learning clause 125:3:1:[5.1,23.3,14.3]:Top: not_ok(x0),or_ok(x0),one(in1(x0)) ->
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 2154
% 33.61/8.80 === Backtracking. Learning clause 126:5:2:[21.3,12.2,18.1,3.2]:TopTop: logic_or(x0),and_ok(x0),zero(out1(x0)),connection(x1,in1(x0)) -> zero(x1)
% 33.61/8.80 === Clause set with instances from active satisfied. Growing active. New size: 2218
% 33.61/8.80 === Backtracking. Learning clause 131:4:1:[97.1,127.0,41.1,128.3,49.1,129.4,52.0,130.6,4.2,11.3,5.2,23.3,2.3,27.2,60.2,8.4,73.3,30.2,39.2,2.3,75.3,40.2,123.7,38.2,61.2,72.3,2.3,56.1,1.3,47.2,42.2,53.1,50.2,96.3,2.3,55.1,80.3,19.1,110.1]:Top: connection(x0,in1(and2(h1(f)))),one(x0),zero(out1(or1(f))) -> zero(outc(h1(f)))
% 33.61/8.80 === Backtracking. Learning clause 133:6:0:[52.0,132.4,61.2,123.8,80.3]:: one(outs(h2(f))),connection(out1(or1(h2(f))),in1(and1(h2(f)))),zero(in1(or1(h2(f)))),halfadder(h2(f)) -> one(outs(h1(f))),or_ok(or1(f))
% 33.61/8.80 === Backtracking. Learning clause 137:1:0:[117.0,134.0,52.0,135.2,116.0,136.3,9.2,76.3,95.1,3.2,99.3,55.1,131.4,34.2,97.2,41.2]:: zero(out1(or1(f))) ->
% 33.61/8.80 === Conflict found: 123:8:1:[52.0,122.2,10.2,75.3,120.4,21.2,67.2,5.2,62.2,31.2,33.2]:Top: one(outs(x0)),connection(out1(or1(h2(f))),in1(and1(x0))),halfadder(x0),zero(in1(or1(h2(f)))),abnormal(or1(f)),halfadder(h2(f)) -> one(outs(h1(f))),abnormal(and1(x0)) {x0 -> h2(f)}
% 33.61/8.80 === Backtracking. Learning clause 138:2:0:[123.4,72.3,38.2,1.3,53.1,2.3,56.1,50.2,47.2,42.2,52.1,61.2]:: abnormal(or1(f)) -> one(outs(h1(f)))
% 33.61/8.80
% 33.61/8.80 SZS status Unsatisfiable
% 33.61/8.80
% 33.61/8.80 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/8.80
% 33.61/8.80 SPASS-SCL-FOL Statistics:
% 33.61/8.80 Number of learned clauses: 63
% 33.61/8.80 Number of propagations: 7381
% 33.61/8.80 Number of decisions: 4790
% 33.61/8.80 Number of resolutions: 176
% 33.61/8.80 Number of condensations: 0
% 33.61/8.80 Number of sub resolutions: 13
% 33.61/8.80 Number of input literals (deduplicated): 53
% 33.61/8.80 Number of grows: 36
% 33.61/8.80 Number of considered ground atoms: 2218
% 33.61/8.80
% 33.61/8.80 Needed: 0:00:08.29
% 33.61/8.80
%------------------------------------------------------------------------------