%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV008-1.001 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n021.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 117.24s 24.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV008-1.001 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n021.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:06:43 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 117.24/24.00 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00 Execution resolution_2 ended with status: unsatisfiable
% 117.24/24.00 Used heuristic: resolution_2
% 117.24/24.00
% 117.24/24.00 Input Clauses:
% 117.24/24.00
% 117.24/24.00 Predicates: connection value equal_value mode type
% 117.24/24.00 Fol Constants: n0 n1 ok abnormal and n2 or not halfadder s c fulladder a1 b1 a
% 117.24/24.00 Fol Functions: in out and1 and2 not1 or1 h1 h2 nbit_adder v
% 117.24/24.00 Problem Properties:
% 117.24/24.00 This is a full first-order problem without equality.
% 117.24/24.00
% 117.24/24.00 After reduction: Problem Properties:
% 117.24/24.00 This is a full first-order problem without equality.
% 117.24/24.00
% 117.24/24.00
% 117.24/24.00 Reduced Input Clauses:
% 117.24/24.00
% 117.24/24.00 Most General Atoms: connection(x0,x1) value(x0,x1) equal_value(x1,x2) mode(x0,ok) mode(x0,abnormal) type(x0,x1)
% 117.24/24.00
% 117.24/24.00 === Starting SPASS-SCL-FOL A Little Less Naive, considering 60 atoms initially, heuristics mode: resolution_2 ===
% 117.24/24.00
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 61
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 61:2:1:[3.3,4.1]:Top: value(x0,n0),value(x0,n1) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 61
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 69
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 62:2:0:[7.1,52.1]:: -> mode(a,ok),mode(a,abnormal)
% 117.24/24.00 === Backtracking. Learning clause 63:1:0:[46.1,52.1]:: -> type(v(n1,a),fulladder)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 73
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 64:1:0:[3.1,56.1]:: -> equal_value(n0,n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 137
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 137
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 65:2:1:[2.2,54.1]:Top: connection(x0,in(b1,a)) -> value(x0,n0)
% 117.24/24.00 === Backtracking. Learning clause 66:2:1:[1.2,54.1]:Top: connection(in(b1,a),x0) -> value(x0,n0)
% 117.24/24.00 === Conflict found: 61:2:1:[3.3,4.1]:Top: value(x0,n0),value(x0,n1) -> {x0 -> in(b1,a)}
% 117.24/24.00 === Backtracking. Learning clause 67:1:0:[61.1,54.1]:: value(in(b1,a),n1) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 137
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 68:2:1:[2.2,55.1]:Top: connection(x0,in(c,a)) -> value(x0,n0)
% 117.24/24.00 === Backtracking. Learning clause 69:2:1:[1.2,55.1]:Top: connection(in(c,a),x0) -> value(x0,n0)
% 117.24/24.00 === Conflict found: 61:2:1:[3.3,4.1]:Top: value(x0,n0),value(x0,n1) -> {x0 -> in(c,a)}
% 117.24/24.00 === Backtracking. Learning clause 70:1:0:[61.1,55.1]:: value(in(c,a),n1) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 139
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 71:2:1:[2.2,57.1]:Top: connection(x0,out(c,a)) -> value(x0,n1)
% 117.24/24.00 === Backtracking. Learning clause 72:2:1:[1.2,57.1]:Top: connection(out(c,a),x0) -> value(x0,n1)
% 117.24/24.00 === Conflict found: 61:2:1:[3.3,4.1]:Top: value(x0,n0),value(x0,n1) -> {x0 -> out(c,a)}
% 117.24/24.00 === Backtracking. Learning clause 73:1:0:[61.2,57.1]:: value(out(c,a),n0) ->
% 117.24/24.00 === Backtracking. Learning clause 74:4:2:[7.2,8.1]:TopTop: type(x0,and),value(in(x1,x0),n0) -> mode(x0,abnormal),value(out(n1,x0),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 144
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 74:4:2:[7.2,8.1]:TopTop: type(x0,and),value(in(x1,x0),n0) -> mode(x0,abnormal),value(out(n1,x0),n0) {x0 -> or1(v(n1,a)), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 75:3:1:[74.3,58.1]:Top: type(or1(v(n1,a)),and),value(in(x0,or1(v(n1,a))),n0) -> value(out(n1,or1(v(n1,a))),n0)
% 117.24/24.00 === Backtracking. Learning clause 76:2:1:[7.3,58.1]:Top: type(or1(v(n1,a)),x0) -> mode(or1(v(n1,a)),ok)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 208
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 212
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 74:4:2:[7.2,8.1]:TopTop: type(x0,and),value(in(x1,x0),n0) -> mode(x0,abnormal),value(out(n1,x0),n0) {x0 -> and2(h1(v(n1,a))), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 77:3:1:[74.3,59.1]:Top: type(and2(h1(v(n1,a))),and),value(in(x0,and2(h1(v(n1,a)))),n0) -> value(out(n1,and2(h1(v(n1,a)))),n0)
% 117.24/24.00 === Backtracking. Learning clause 78:2:1:[7.3,59.1]:Top: type(and2(h1(v(n1,a))),x0) -> mode(and2(h1(v(n1,a))),ok)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 216
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 74:4:2:[7.2,8.1]:TopTop: type(x0,and),value(in(x1,x0),n0) -> mode(x0,abnormal),value(out(n1,x0),n0) {x0 -> and2(h2(v(n1,a))), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 79:3:1:[74.3,60.1]:Top: type(and2(h2(v(n1,a))),and),value(in(x0,and2(h2(v(n1,a)))),n0) -> value(out(n1,and2(h2(v(n1,a)))),n0)
% 117.24/24.00 === Backtracking. Learning clause 80:2:1:[7.3,60.1]:Top: type(and2(h2(v(n1,a))),x0) -> mode(and2(h2(v(n1,a))),ok)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 218
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 81:2:0:[7.1,63.1]:: -> mode(v(n1,a),ok),mode(v(n1,a),abnormal)
% 117.24/24.00 === Backtracking. Learning clause 82:1:0:[35.1,63.1]:: -> type(h1(v(n1,a)),halfadder)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 218
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 83:2:1:[2.3,67.1]:Top: connection(in(b1,a),x0),value(x0,n1) ->
% 117.24/24.00 === Conflict found: 83:2:1:[2.3,67.1]:Top: connection(in(b1,a),x0),value(x0,n1) -> {x0 -> out(c,a)}
% 117.24/24.00 === Backtracking. Learning clause 84:1:0:[83.2,57.1]:: connection(in(b1,a),out(c,a)) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 282
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 282
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 85:2:1:[2.3,70.1]:Top: connection(in(c,a),x0),value(x0,n1) ->
% 117.24/24.00 === Conflict found: 85:2:1:[2.3,70.1]:Top: connection(in(c,a),x0),value(x0,n1) -> {x0 -> out(c,a)}
% 117.24/24.00 === Backtracking. Learning clause 86:1:0:[85.2,57.1]:: connection(in(c,a),out(c,a)) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 282
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 87:2:1:[2.3,73.1]:Top: connection(out(c,a),x0),value(x0,n0) ->
% 117.24/24.00 === Conflict found: 65:2:1:[2.2,54.1]:Top: connection(x0,in(b1,a)) -> value(x0,n0) {x0 -> out(c,a)}
% 117.24/24.00 === Backtracking. Learning clause 88:1:0:[65.2,73.1]:: connection(out(c,a),in(b1,a)) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 284
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 89:2:0:[7.1,82.1]:: -> mode(h1(v(n1,a)),ok),mode(h1(v(n1,a)),abnormal)
% 117.24/24.00 === Backtracking. Learning clause 90:1:0:[22.1,82.1]:: -> type(and1(h1(v(n1,a))),and)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 293
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 91:3:1:[8.2,90.1]:Top: mode(and1(h1(v(n1,a))),ok),value(in(x0,and1(h1(v(n1,a)))),n0) -> value(out(n1,and1(h1(v(n1,a)))),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 357
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 359
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 71:2:1:[2.2,57.1]:Top: connection(x0,out(c,a)) -> value(x0,n1) {x0 -> in(a1,a)}
% 117.24/24.00 === Backtracking. Learning clause 92:2:1:[71.2,61.2]:Top: connection(x0,out(c,a)),value(x0,n0) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 368
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 93:4:2:[8.2,22.2,61.1]:TopTop: mode(and1(x0),ok),value(in(x1,and1(x0)),n0),type(x0,halfadder),value(out(n1,and1(x0)),n1) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 373
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 74:4:2:[7.2,8.1]:TopTop: type(x0,and),value(in(x1,x0),n0) -> mode(x0,abnormal),value(out(n1,x0),n0) {x0 -> and2(h1(v(n1,a))), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 95:2:1:[82.0,94.1,74.1,23.2,61.1,59.1]:Top: value(in(x0,and2(h1(v(n1,a)))),n0),value(out(n1,and2(h1(v(n1,a)))),n1) ->
% 117.24/24.00 === Conflict found: 78:2:1:[7.3,59.1]:Top: type(and2(h1(v(n1,a))),x0) -> mode(and2(h1(v(n1,a))),ok) {x0 -> and}
% 117.24/24.00 === Backtracking. Learning clause 97:1:0:[82.0,96.0,78.1,23.2]:: -> mode(and2(h1(v(n1,a))),ok)
% 117.24/24.00 === Conflict found: 66:2:1:[1.2,54.1]:Top: connection(in(b1,a),x0) -> value(x0,n0) {x0 -> in(n2,v(n1,a))}
% 117.24/24.00 === Backtracking. Learning clause 101:2:0:[63.0,98.0,82.0,99.1,78.1,100.2,66.1,50.2,1.2,1.2,42.2,28.2,8.3,52.1]:: type(and2(h1(v(n1,a))),and) -> value(out(n1,and2(h1(v(n1,a)))),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 376
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 61:2:1:[3.3,4.1]:Top: value(x0,n0),value(x0,n1) -> {x0 -> out(n1,and2(h1(v(n1,a))))}
% 117.24/24.00 === Backtracking. Learning clause 102:2:0:[61.1,101.2]:: value(out(n1,and2(h1(v(n1,a)))),n1),type(and2(h1(v(n1,a))),and) ->
% 117.24/24.00 === Backtracking. Learning clause 103:5:2:[13.4,15.3]:TopTop: value(in(x1,x0),n1),mode(x0,ok),type(x0,or) -> value(in(n1,x0),n1),value(in(n2,x0),n1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 440
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 446
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 104:4:1:[18.2,24.2]:Top: mode(not1(x0),ok),value(in(n1,not1(x0)),n0),type(x0,halfadder) -> value(out(n1,not1(x0)),n1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 452
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 76:2:1:[7.3,58.1]:Top: type(or1(v(n1,a)),x0) -> mode(or1(v(n1,a)),ok) {x0 -> or}
% 117.24/24.00 === Backtracking. Learning clause 105:2:0:[76.1,25.2]:: type(v(n1,a),halfadder) -> mode(or1(v(n1,a)),ok)
% 117.24/24.00 === Backtracking. Learning clause 106:1:0:[23.1,82.1,101.1]:: -> value(out(n1,and2(h1(v(n1,a)))),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 454
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 107:4:1:[21.3,72.2]:Top: mode(x0,ok),type(x0,not),connection(out(c,a),out(n1,x0)) -> value(in(n1,x0),n0)
% 117.24/24.00 === Backtracking. Learning clause 109:2:0:[78.1,108.0,16.3,106.1]:: type(and2(h1(v(n1,a))),or) -> value(in(n1,and2(h1(v(n1,a)))),n0)
% 117.24/24.00 === Conflict found: 92:2:1:[71.2,61.2]:Top: connection(x0,out(c,a)),value(x0,n0) -> {x0 -> out(n1,and2(h1(v(n1,a))))}
% 117.24/24.00 === Backtracking. Learning clause 110:1:0:[92.2,106.1]:: connection(out(n1,and2(h1(v(n1,a)))),out(c,a)) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 455
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 111:3:2:[1.1,26.2]:TopTop: value(in(n1,x0),x1),type(x0,halfadder) -> value(in(n1,or1(x0)),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 519
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 520
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 112:3:2:[2.1,27.2]:TopTop: value(in(n2,or1(x0)),x1),type(x0,halfadder) -> value(in(n2,x0),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 521
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 113:3:2:[1.1,29.2]:TopTop: value(in(n2,x0),x1),type(x0,halfadder) -> value(in(n2,and2(x0)),x1)
% 117.24/24.00 === Backtracking. Learning clause 120:3:1:[76.1,114.0,25.1,115.1,106.0,116.3,82.0,117.4,63.0,118.6,52.0,119.7,14.4,1.3,111.3,1.3,53.1,2.3,3.2,1.3,49.2,31.2,1.3,45.2,39.2,48.2]:Top: type(v(n1,a),halfadder),value(out(c,a),x0) -> equal_value(x0,n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 522
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 121:3:2:[2.1,30.2]:TopTop: value(out(n1,and1(x0)),x1),type(x0,halfadder) -> value(out(s,x0),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 523
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 122:3:2:[1.1,32.2]:TopTop: value(out(n1,or1(x0)),x1),type(x0,halfadder) -> value(in(n1,and1(x0)),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 587
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 588
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 123:3:2:[2.1,33.2]:TopTop: value(in(n1,not1(x0)),x1),type(x0,halfadder) -> value(out(n1,and2(x0)),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 588
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 124:3:2:[1.1,34.2]:TopTop: value(out(n1,not1(x0)),x1),type(x0,halfadder) -> value(in(n2,and1(x0)),x1)
% 117.24/24.00 === Backtracking. Learning clause 125:2:1:[27.1,36.2]:Top: type(x0,fulladder) -> connection(in(n2,h2(x0)),in(n2,or1(h2(x0))))
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 611
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 126:3:1:[7.1,35.2]:Top: type(x0,fulladder) -> mode(h1(x0),ok),mode(h1(x0),abnormal)
% 117.24/24.00 === Conflict found: 124:3:2:[1.1,34.2]:TopTop: value(out(n1,not1(x0)),x1),type(x0,halfadder) -> value(in(n2,and1(x0)),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 127:3:2:[124.2,35.2]:TopTop: value(out(n1,not1(h1(x0))),x1),type(x0,fulladder) -> value(in(n2,and1(h1(x0))),x1)
% 117.24/24.00 === Conflict found: 123:3:2:[2.1,33.2]:TopTop: value(in(n1,not1(x0)),x1),type(x0,halfadder) -> value(out(n1,and2(x0)),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 128:3:2:[123.2,35.2]:TopTop: value(in(n1,not1(h1(x0))),x1),type(x0,fulladder) -> value(out(n1,and2(h1(x0))),x1)
% 117.24/24.00 === Conflict found: 122:3:2:[1.1,32.2]:TopTop: value(out(n1,or1(x0)),x1),type(x0,halfadder) -> value(in(n1,and1(x0)),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 129:3:2:[122.2,35.2]:TopTop: value(out(n1,or1(h1(x0))),x1),type(x0,fulladder) -> value(in(n1,and1(h1(x0))),x1)
% 117.24/24.00 === Conflict found: 121:3:2:[2.1,30.2]:TopTop: value(out(n1,and1(x0)),x1),type(x0,halfadder) -> value(out(s,x0),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 130:3:2:[121.2,35.2]:TopTop: value(out(n1,and1(h1(x0))),x1),type(x0,fulladder) -> value(out(s,h1(x0)),x1)
% 117.24/24.00 === Conflict found: 112:3:2:[2.1,27.2]:TopTop: value(in(n2,or1(x0)),x1),type(x0,halfadder) -> value(in(n2,x0),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 131:3:2:[112.2,35.2]:TopTop: value(in(n2,or1(h1(x0))),x1),type(x0,fulladder) -> value(in(n2,h1(x0)),x1)
% 117.24/24.00 === Conflict found: 111:3:2:[1.1,26.2]:TopTop: value(in(n1,x0),x1),type(x0,halfadder) -> value(in(n1,or1(x0)),x1) {x0 -> h1(n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 132:3:2:[111.2,35.2]:TopTop: value(in(n1,h1(x0)),x1),type(x0,fulladder) -> value(in(n1,or1(h1(x0))),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 611
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 133:4:1:[17.2,37.2]:Top: mode(or1(x0),ok),value(out(n1,or1(x0)),n0),type(x0,fulladder) -> value(in(n2,or1(x0)),n0)
% 117.24/24.00 === Backtracking. Learning clause 134:4:2:[13.2,37.2]:TopTop: mode(or1(x0),ok),value(in(x1,or1(x0)),n1),type(x0,fulladder) -> value(out(n1,or1(x0)),n1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 675
% 117.24/24.00 === Backtracking. Learning clause 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2)
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> out(c,h2(v(n1,a))), x1 -> out(n1,and2(h2(v(n1,a)))), x2 -> n0, x3 -> in(n1,or1(v(n1,a)))}
% 117.24/24.00 === Backtracking. Learning clause 137:3:2:[36.1,136.2,135.3,40.2,31.2]:TopTop: value(out(n1,and2(h2(x0))),x1),type(x0,fulladder) -> value(in(n1,or1(x0)),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 677
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> out(s,h1(n0)), x1 -> in(n2,h2(n0)), x2 -> n0, x3 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 138:4:3:[135.1,38.2]:TopTopTop: value(in(n2,h2(x0)),x1),connection(out(s,h1(x0)),x2),type(x0,fulladder) -> value(x2,x1)
% 117.24/24.00 === Backtracking. Learning clause 139:1:0:[37.1,63.1]:: -> type(or1(v(n1,a)),or)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 677
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 103:5:2:[13.4,15.3]:TopTop: value(in(x1,x0),n1),mode(x0,ok),type(x0,or) -> value(in(n1,x0),n1),value(in(n2,x0),n1) {x0 -> or1(v(n1,a)), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 140:4:1:[103.3,139.1]:Top: value(in(x0,or1(v(n1,a))),n1),mode(or1(v(n1,a)),ok) -> value(in(n1,or1(v(n1,a))),n1),value(in(n2,or1(v(n1,a))),n1)
% 117.24/24.00 === Backtracking. Learning clause 141:3:0:[16.2,139.1]:: mode(or1(v(n1,a)),ok),value(out(n1,or1(v(n1,a))),n0) -> value(in(n1,or1(v(n1,a))),n0)
% 117.24/24.00 === Backtracking. Learning clause 142:3:2:[31.1,36.2,1.1]:TopTop: type(x0,fulladder),value(out(c,h2(x0)),x1) -> value(out(n1,and2(h2(x0))),x1)
% 117.24/24.00 === Backtracking. Learning clause 143:1:0:[48.1,52.1,72.1,1.2,45.2,63.1,61.2]:: value(out(n1,or1(v(n1,a))),n0) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 680
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 138:4:3:[135.1,38.2]:TopTopTop: value(in(n2,h2(x0)),x1),connection(out(s,h1(x0)),x2),type(x0,fulladder) -> value(x2,x1) {x0 -> n0, x1 -> n0, x2 -> out(n1,or1(v(n1,a)))}
% 117.24/24.00 === Backtracking. Learning clause 144:3:1:[138.4,143.1]:Top: value(in(n2,h2(x0)),n0),connection(out(s,h1(x0)),out(n1,or1(v(n1,a)))),type(x0,fulladder) ->
% 117.24/24.00 === Backtracking. Learning clause 145:2:1:[1.3,143.1]:Top: connection(x0,out(n1,or1(v(n1,a)))),value(x0,n0) ->
% 117.24/24.00 === Conflict found: 66:2:1:[1.2,54.1]:Top: connection(in(b1,a),x0) -> value(x0,n0) {x0 -> out(n1,or1(v(n1,a)))}
% 117.24/24.00 === Backtracking. Learning clause 146:1:0:[66.2,143.1]:: connection(in(b1,a),out(n1,or1(v(n1,a)))) ->
% 117.24/24.00 === Backtracking. Learning clause 151:1:0:[139.0,147.0,106.0,148.1,63.0,149.3,143.0,150.4,14.1,76.2,135.4,31.2,39.2,82.1,137.3]:: value(out(n1,and2(h2(v(n1,a)))),n0) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 693
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 138:4:3:[135.1,38.2]:TopTopTop: value(in(n2,h2(x0)),x1),connection(out(s,h1(x0)),x2),type(x0,fulladder) -> value(x2,x1) {x0 -> n0, x1 -> n0, x2 -> out(n1,and2(h2(v(n1,a))))}
% 117.24/24.00 === Backtracking. Learning clause 152:3:1:[138.4,151.1]:Top: value(in(n2,h2(x0)),n0),connection(out(s,h1(x0)),out(n1,and2(h2(v(n1,a))))),type(x0,fulladder) ->
% 117.24/24.00 === Backtracking. Learning clause 153:2:1:[1.3,151.1]:Top: connection(x0,out(n1,and2(h2(v(n1,a))))),value(x0,n0) ->
% 117.24/24.00 === Conflict found: 68:2:1:[2.2,55.1]:Top: connection(x0,in(c,a)) -> value(x0,n0) {x0 -> out(n1,and2(h2(v(n1,a))))}
% 117.24/24.00 === Backtracking. Learning clause 154:1:0:[68.2,151.1]:: connection(out(n1,and2(h2(v(n1,a)))),in(c,a)) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 757
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 759
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> in(n1,n0), x1 -> in(n1,h2(n0)), x2 -> n0, x3 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 155:4:3:[135.1,41.2]:TopTopTop: value(in(n1,h2(x0)),x1),connection(in(n1,x0),x2),type(x0,fulladder) -> value(x2,x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 763
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 85:2:1:[2.3,70.1]:Top: connection(in(c,a),x0),value(x0,n1) -> {x0 -> in(n2,h1(a))}
% 117.24/24.00 === Backtracking. Learning clause 156:2:0:[85.1,43.2]:: value(in(n2,h1(a)),n1),type(a,fulladder) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 766
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 157:6:4:[1.1,44.2,2.3,138.4]:TopTopTopTop: type(x0,fulladder),connection(out(s,x0),x1),value(in(n2,h2(x2)),x3),connection(out(s,h1(x2)),x1),type(x2,fulladder) -> value(out(s,h2(x0)),x3)
% 117.24/24.00 === Conflict found: 157:6:4:[1.1,44.2,2.3,138.4]:TopTopTopTop: type(x0,fulladder),connection(out(s,x0),x1),value(in(n2,h2(x2)),x3),connection(out(s,h1(x2)),x1),type(x2,fulladder) -> value(out(s,h2(x0)),x3) {x0 -> h1(n0), x1 -> out(s,h2(h1(n0))), x2 -> n0, x3 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 158:4:2:[157.2,44.2]:TopTop: value(in(n2,h2(x0)),x1),type(x0,fulladder),type(h1(x0),fulladder) -> value(out(s,h2(h1(x0))),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 803
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 159:3:1:[7.1,46.2]:Top: type(x0,nbit_adder(n1)) -> mode(v(n1,x0),ok),mode(v(n1,x0),abnormal)
% 117.24/24.00 === Conflict found: 157:6:4:[1.1,44.2,2.3,138.4]:TopTopTopTop: type(x0,fulladder),connection(out(s,x0),x1),value(in(n2,h2(x2)),x3),connection(out(s,h1(x2)),x1),type(x2,fulladder) -> value(out(s,h2(x0)),x3) {x0 -> v(n1,n0), x1 -> n0, x2 -> v(n1,n0), x3 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 160:5:3:[157.1,46.2]:TopTopTop: connection(out(s,v(n1,x0)),x1),value(in(n2,h2(v(n1,x0))),x2),connection(out(s,h1(v(n1,x0))),x1),type(x0,nbit_adder(n1)) -> value(out(s,h2(v(n1,x0))),x2)
% 117.24/24.00 === Conflict found: 155:4:3:[135.1,41.2]:TopTopTop: value(in(n1,h2(x0)),x1),connection(in(n1,x0),x2),type(x0,fulladder) -> value(x2,x1) {x0 -> v(n1,n0), x1 -> n0, x2 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 161:4:3:[155.3,46.2]:TopTopTop: value(in(n1,h2(v(n1,x0))),x1),connection(in(n1,v(n1,x0)),x2),type(x0,nbit_adder(n1)) -> value(x2,x1)
% 117.24/24.00 === Conflict found: 138:4:3:[135.1,38.2]:TopTopTop: value(in(n2,h2(x0)),x1),connection(out(s,h1(x0)),x2),type(x0,fulladder) -> value(x2,x1) {x0 -> v(n1,n0), x1 -> n0, x2 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 162:5:4:[138.3,46.2,2.2]:TopTopTopTop: value(in(n2,h2(v(n1,x0))),x1),connection(out(s,h1(v(n1,x0))),x2),type(x0,nbit_adder(n1)),connection(x3,x2) -> value(x3,x1)
% 117.24/24.00 === Conflict found: 137:3:2:[36.1,136.2,135.3,40.2,31.2]:TopTop: value(out(n1,and2(h2(x0))),x1),type(x0,fulladder) -> value(in(n1,or1(x0)),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 163:3:2:[137.2,46.2]:TopTop: value(out(n1,and2(h2(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(in(n1,or1(v(n1,x0))),x1)
% 117.24/24.00 === Conflict found: 132:3:2:[111.2,35.2]:TopTop: value(in(n1,h1(x0)),x1),type(x0,fulladder) -> value(in(n1,or1(h1(x0))),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 164:3:2:[132.2,46.2]:TopTop: value(in(n1,h1(v(n1,x0))),x1),type(x0,nbit_adder(n1)) -> value(in(n1,or1(h1(v(n1,x0)))),x1)
% 117.24/24.00 === Conflict found: 131:3:2:[112.2,35.2]:TopTop: value(in(n2,or1(h1(x0))),x1),type(x0,fulladder) -> value(in(n2,h1(x0)),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 165:3:2:[131.2,46.2]:TopTop: value(in(n2,or1(h1(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(in(n2,h1(v(n1,x0))),x1)
% 117.24/24.00 === Conflict found: 130:3:2:[121.2,35.2]:TopTop: value(out(n1,and1(h1(x0))),x1),type(x0,fulladder) -> value(out(s,h1(x0)),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 166:3:2:[130.2,46.2]:TopTop: value(out(n1,and1(h1(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(out(s,h1(v(n1,x0))),x1)
% 117.24/24.00 === Conflict found: 129:3:2:[122.2,35.2]:TopTop: value(out(n1,or1(h1(x0))),x1),type(x0,fulladder) -> value(in(n1,and1(h1(x0))),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 167:3:2:[129.2,46.2]:TopTop: value(out(n1,or1(h1(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(in(n1,and1(h1(v(n1,x0)))),x1)
% 117.24/24.00 === Conflict found: 128:3:2:[123.2,35.2]:TopTop: value(in(n1,not1(h1(x0))),x1),type(x0,fulladder) -> value(out(n1,and2(h1(x0))),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 168:3:2:[128.2,46.2]:TopTop: value(in(n1,not1(h1(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(out(n1,and2(h1(v(n1,x0)))),x1)
% 117.24/24.00 === Conflict found: 127:3:2:[124.2,35.2]:TopTop: value(out(n1,not1(h1(x0))),x1),type(x0,fulladder) -> value(in(n2,and1(h1(x0))),x1) {x0 -> v(n1,n0), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 169:3:2:[127.2,46.2]:TopTop: value(out(n1,not1(h1(v(n1,x0)))),x1),type(x0,nbit_adder(n1)) -> value(in(n2,and1(h1(v(n1,x0)))),x1)
% 117.24/24.00 === Conflict found: 126:3:1:[7.1,35.2]:Top: type(x0,fulladder) -> mode(h1(x0),ok),mode(h1(x0),abnormal) {x0 -> v(n1,n0)}
% 117.24/24.00 === Backtracking. Learning clause 170:3:1:[126.1,46.2]:Top: type(x0,nbit_adder(n1)) -> mode(h1(v(n1,x0)),ok),mode(h1(v(n1,x0)),abnormal)
% 117.24/24.00 === Conflict found: 125:2:1:[27.1,36.2]:Top: type(x0,fulladder) -> connection(in(n2,h2(x0)),in(n2,or1(h2(x0)))) {x0 -> v(n1,n0)}
% 117.24/24.00 === Backtracking. Learning clause 171:2:1:[125.1,46.2]:Top: type(x0,nbit_adder(n1)) -> connection(in(n2,h2(v(n1,x0))),in(n2,or1(h2(v(n1,x0)))))
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 867
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 870
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 162:5:4:[138.3,46.2,2.2]:TopTopTopTop: value(in(n2,h2(v(n1,x0))),x1),connection(out(s,h1(v(n1,x0))),x2),type(x0,nbit_adder(n1)),connection(x3,x2) -> value(x3,x1) {x0 -> n0, x1 -> n0, x2 -> out(s,v(n1,n0)), x3 -> out(n1,n0)}
% 117.24/24.00 === Backtracking. Learning clause 172:5:3:[162.4,47.2]:TopTopTop: value(in(n2,h2(v(n1,x0))),x1),connection(out(s,h1(v(n1,x0))),out(s,v(n1,x2))),type(x0,nbit_adder(n1)),type(x2,nbit_adder(n1)) -> value(out(n1,x2),x1)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 871
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> in(c,a), x1 -> n0, x2 -> n0, x3 -> in(c,v(n1,a))}
% 117.24/24.00 === Backtracking. Learning clause 173:4:2:[135.3,51.2,69.2]:TopTop: connection(in(c,x0),x1),type(x0,nbit_adder(n1)),connection(in(c,a),x1) -> value(in(c,v(n1,x0)),n0)
% 117.24/24.00 === Conflict found: 173:4:2:[135.3,51.2,69.2]:TopTop: connection(in(c,x0),x1),type(x0,nbit_adder(n1)),connection(in(c,a),x1) -> value(in(c,v(n1,x0)),n0) {x0 -> a, x1 -> in(c,v(n1,a))}
% 117.24/24.00 === Backtracking. Learning clause 175:1:0:[52.0,174.0,173.1,51.2]:: -> value(in(c,v(n1,a)),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 874
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 176:2:1:[1.2,175.1]:Top: connection(in(c,v(n1,a)),x0) -> value(x0,n0)
% 117.24/24.00 === Conflict found: 145:2:1:[1.3,143.1]:Top: connection(x0,out(n1,or1(v(n1,a)))),value(x0,n0) -> {x0 -> in(c,v(n1,a))}
% 117.24/24.00 === Backtracking. Learning clause 177:1:0:[145.2,175.1]:: connection(in(c,v(n1,a)),out(n1,or1(v(n1,a)))) ->
% 117.24/24.00 === Backtracking. Learning clause 180:1:0:[63.0,178.0,52.0,179.1,1.1,44.2,1.3,47.2,56.1]:: -> value(out(s,h2(v(n1,a))),n0)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 877
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> n0, x1 -> out(s,h2(v(n1,a))), x2 -> n0, x3 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 181:3:2:[135.2,180.1]:TopTop: connection(x0,out(s,h2(v(n1,a)))),connection(x0,x1) -> value(x1,n0)
% 117.24/24.00 === Conflict found: 87:2:1:[2.3,73.1]:Top: connection(out(c,a),x0),value(x0,n0) -> {x0 -> out(s,h2(v(n1,a)))}
% 117.24/24.00 === Backtracking. Learning clause 182:1:0:[87.2,180.1]:: connection(out(c,a),out(s,h2(v(n1,a)))) ->
% 117.24/24.00 === Backtracking. Learning clause 183:1:0:[51.1,52.1]:: -> connection(in(c,a),in(c,v(n1,a)))
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 941
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 942
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 184:3:2:[1.3,85.2]:TopTop: connection(x0,x1),value(x0,n1),connection(in(c,a),x1) ->
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 942
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 185:2:0:[43.2,69.1]:: type(a,fulladder) -> value(in(n2,h1(a)),n0)
% 117.24/24.00 === Backtracking. Learning clause 186:4:1:[18.1,7.2]:Top: type(x0,not),value(in(n1,x0),n0) -> value(out(n1,x0),n1),mode(x0,abnormal)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 942
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Backtracking. Learning clause 187:2:0:[23.2,80.1]:: type(h2(v(n1,a)),halfadder) -> mode(and2(h2(v(n1,a))),ok)
% 117.24/24.00 === Backtracking. Learning clause 188:1:0:[36.1,63.1,187.1]:: -> mode(and2(h2(v(n1,a))),ok)
% 117.24/24.00 === Clause set with instances from active satisfied. Growing active. New size: 946
% 117.24/24.00 === Restarting.
% 117.24/24.00 === Conflict found: 107:4:1:[21.3,72.2]:Top: mode(x0,ok),type(x0,not),connection(out(c,a),out(n1,x0)) -> value(in(n1,x0),n0) {x0 -> and2(h2(v(n1,a)))}
% 117.24/24.00 === Backtracking. Learning clause 189:3:0:[107.1,188.1]:: type(and2(h2(v(n1,a))),not),connection(out(c,a),out(n1,and2(h2(v(n1,a))))) -> value(in(n1,and2(h2(v(n1,a)))),n0)
% 117.24/24.00 === Backtracking. Learning clause 190:3:0:[21.1,188.1]:: type(and2(h2(v(n1,a))),not),value(out(n1,and2(h2(v(n1,a)))),n1) -> value(in(n1,and2(h2(v(n1,a)))),n0)
% 117.24/24.00 === Conflict found: 103:5:2:[13.4,15.3]:TopTop: value(in(x1,x0),n1),mode(x0,ok),type(x0,or) -> value(in(n1,x0),n1),value(in(n2,x0),n1) {x0 -> and2(h2(v(n1,a))), x1 -> n0}
% 117.24/24.00 === Backtracking. Learning clause 191:4:1:[103.2,188.1]:Top: value(in(x0,and2(h2(v(n1,a)))),n1),type(and2(h2(v(n1,a))),or) -> value(in(n1,and2(h2(v(n1,a)))),n1),value(in(n2,and2(h2(v(n1,a)))),n1)
% 117.24/24.00 === Backtracking. Learning clause 192:4:0:[15.1,188.1]:: type(and2(h2(v(n1,a))),or),value(out(n1,and2(h2(v(n1,a)))),n1) -> value(in(n1,and2(h2(v(n1,a)))),n1),value(in(n2,and2(h2(v(n1,a)))),n1)
% 117.24/24.00 === Backtracking. Learning clause 193:3:0:[12.1,188.1]:: type(and2(h2(v(n1,a))),and),value(out(n1,and2(h2(v(n1,a)))),n1) -> value(in(n2,and2(h2(v(n1,a)))),n1)
% 117.24/24.00 === Conflict found: 135:4:4:[2.3,1.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x0,x3) -> value(x3,x2) {x0 -> out(n1,a), x1 -> out(s,v(n1,a)), x2 -> n0, x3 -> in(n0,and2(h2(v(n1,a))))}
% 117.24/24.00 === Backtracking. Learning clause 194:6:4:[135.4,8.3]:TopTopTopTop: connection(x0,x1),value(x1,n0),connection(x0,in(x2,x3)),mode(x3,ok),type(x3,and) -> value(out(n1,x3),n0)
% 117.24/24.00 === Backtracking. Learning clause 195:2:0:[2.3,2.2,11.4,61.2,28.2,41.2,1.3,53.1,49.2,52.1,36.2,63.1,188.1]:: type(and2(h2(v(n1,a))),and),value(out(n1,and2(h2(v(n1,a)))),n1) ->
% 117.24/24.00 === Backtracking. Learning clause 196:1:0:[15.4,135.2,61.2,40.2,135.4,106.1,1.3,72.2,48.2,45.2,76.2,39.2,31.2,31.2,82.1,139.1,195.2,52.1,36.2,63.1]:: type(and2(h2(v(n1,a))),and) ->
% 117.24/24.00
% 117.24/24.00 SZS status Unsatisfiable
% 117.24/24.00
% 117.24/24.00 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.24/24.00
% 117.24/24.00 SPASS-SCL-FOL Statistics:
% 117.24/24.00 Number of learned clauses: 116
% 117.24/24.00 Number of propagations: 15337
% 117.24/24.00 Number of decisions: 12279
% 117.24/24.00 Number of resolutions: 190
% 117.24/24.00 Number of condensations: 3
% 117.24/24.00 Number of sub resolutions: 20
% 117.24/24.00 Number of input literals (deduplicated): 60
% 117.24/24.00 Number of grows: 59
% 117.24/24.00 Number of considered ground atoms: 946
% 117.24/24.00
% 117.24/24.00 Needed: 0:0:23.48
% 117.24/24.00
%------------------------------------------------------------------------------