%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV006-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.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 128.54s 26.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV006-1 : TPTP v9.2.1. Released v2.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n028.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 12:06:01 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 128.54/26.24 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24 Execution lmodel_grow ended with status: unsatisfiable
% 128.54/26.24 Used heuristic: lmodel_grow
% 128.54/26.24
% 128.54/26.24 Input Clauses:
% 128.54/26.24
% 128.54/26.24 Predicates: connection value equal_value mode type
% 128.54/26.24 Fol Constants: n0 n1 ok abnormal and n2 or not halfadder s c fulladder f
% 128.54/26.24 Fol Functions: in out and1 and2 not1 or1 h1 h2
% 128.54/26.24 Problem Properties:
% 128.54/26.24 This is a full first-order problem without equality.
% 128.54/26.24
% 128.54/26.24 After reduction: Problem Properties:
% 128.54/26.24 This is a full first-order problem without equality.
% 128.54/26.24
% 128.54/26.24
% 128.54/26.24 Reduced Input Clauses:
% 128.54/26.24
% 128.54/26.24 Most General Atoms: connection(x0,x1) value(x0,x1) equal_value(x1,x2) mode(x0,ok) mode(x0,abnormal) type(x0,x1)
% 128.54/26.24
% 128.54/26.24 === Starting SPASS-SCL-FOL A Little Less Naive, considering 58 atoms initially, heuristics mode: lmodel_grow ===
% 128.54/26.24
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 90
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 112
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 125
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 135
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 151
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 157
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 163
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 172
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 183
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 188
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 190
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 198
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 202
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 208
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 216
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 222
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 229
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 234
% 128.54/26.24 === Backtracking. Learning clause 59:3:1:[25.1,35.2,7.1]:Top: type(x0,fulladder) -> mode(or1(h1(x0)),ok),mode(or1(h1(x0)),abnormal)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 253
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 262
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 265
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 271
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 275
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 280
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 282
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 284
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 286
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 287
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 296
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 298
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 301
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 303
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 307
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 309
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 310
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 315
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 319
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 323
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 326
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 329
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 332
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 333
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 334
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 337
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 341
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 342
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 347
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 352
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 358
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 364
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 369
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 373
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 376
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 381
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 384
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 388
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 392
% 128.54/26.24 === Backtracking. Learning clause 60:5:2:[2.2,16.4]:TopTop: connection(x0,in(n1,x1)),mode(x1,ok),type(x1,or),value(out(n1,x1),n0) -> value(x0,n0)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 412
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 420
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 427
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 434
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 439
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 445
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 455
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 461
% 128.54/26.24 === Conflict found: 60:5:2:[2.2,16.4]:TopTop: connection(x0,in(n1,x1)),mode(x1,ok),type(x1,or),value(out(n1,x1),n0) -> value(x0,n0) {x0 -> in(n1,f), x1 -> or1(f)}
% 128.54/26.24 === Backtracking. Learning clause 61:7:2:[60.5,3.1,7.2,54.1,7.3,22.2]:TopTop: connection(x0,in(n1,or1(f))),type(or1(f),or),value(out(n1,or1(f)),n0),value(x0,x1),type(h2(f),halfadder) -> equal_value(n0,x1),mode(and1(h2(f)),ok)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 474
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 486
% 128.54/26.24 === Backtracking. Learning clause 62:5:2:[12.4,2.2]:TopTop: mode(x0,ok),type(x0,and),value(out(n1,x0),n1),connection(x1,in(n2,x0)) -> value(x1,n1)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 494
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 499
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 505
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 513
% 128.54/26.24 === Backtracking. Learning clause 63:4:4:[2.3,2.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x3,x0) -> value(x3,x2)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 522
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 530
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 537
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 543
% 128.54/26.24 === Conflict found: 63:4:4:[2.3,2.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x3,x0) -> value(x3,x2) {x0 -> out(n1,or1(h1(n0))), x1 -> in(n1,and1(h1(n0))), x2 -> n1, x3 -> out(c,h1(n0))}
% 128.54/26.24 === Backtracking. Learning clause 64:4:3:[63.1,32.2]:TopTopTop: value(in(n1,and1(x0)),x1),connection(x2,out(n1,or1(x0))),type(x0,halfadder) -> value(x2,x1)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 554
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 565
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 576
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 585
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 594
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 604
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 616
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 623
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 632
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 641
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 646
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 653
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 662
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 669
% 128.54/26.24 === Conflict found: 63:4:4:[2.3,2.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x3,x0) -> value(x3,x2) {x0 -> out(n1,not1(h1(n0))), x1 -> in(n2,and1(h1(n0))), x2 -> n1, x3 -> n0}
% 128.54/26.24 === Backtracking. Learning clause 65:4:3:[63.1,34.2]:TopTopTop: value(in(n2,and1(x0)),x1),connection(x2,out(n1,not1(x0))),type(x0,halfadder) -> value(x2,x1)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 677
% 128.54/26.24 === Backtracking. Learning clause 66:4:4:[3.2,2.3]:TopTopTopTop: value(x0,x1),connection(x0,x2),value(x2,x3) -> equal_value(x1,x3)
% 128.54/26.24 === Backtracking. Learning clause 67:18:8:[21.1,7.2,62.5,52.2,61.7,63.2,1.2,66.3,7.3,60.2]:TopTopTopTopTopTopTopTop: type(not1(h2(f)),not),type(and1(h2(f)),and),value(out(n1,and1(h2(f))),n1),connection(out(n1,not1(h2(f))),in(n2,and1(h2(f)))),connection(x0,in(n1,or1(f))),value(x0,x1),type(h2(f),halfadder),connection(x2,in(n1,not1(h2(f)))),connection(x3,x2),connection(x3,x4),value(x5,x6),connection(x5,x4),connection(x7,in(n1,or1(f))),type(or1(f),or),value(out(n1,or1(f)),n0) -> equal_value(n0,x1),equal_value(x6,n0),value(x7,n0)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 693
% 128.54/26.24 === Backtracking. Learning clause 68:3:2:[1.1,39.2]:TopTop: value(out(c,h1(x0)),x1),type(x0,fulladder) -> value(in(n2,or1(x0)),x1)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 703
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 714
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 721
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 729
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 734
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 738
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 743
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 746
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 751
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 755
% 128.54/26.24 === Conflict found: 63:4:4:[2.3,2.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x3,x0) -> value(x3,x2) {x0 -> out(n1,and2(h1(f))), x1 -> in(n1,not1(h1(f))), x2 -> n1, x3 -> out(c,h1(n0))}
% 128.54/26.24 === Backtracking. Learning clause 69:4:3:[63.1,33.2]:TopTopTop: value(in(n1,not1(x0)),x1),connection(x2,out(n1,and2(x0))),type(x0,halfadder) -> value(x2,x1)
% 128.54/26.24 === Backtracking. Learning clause 72:26:12:[24.1,70.7,37.1,71.22,1.2,63.4,10.3,2.2,20.3,2.2,10.5,63.2,1.3,17.3,66.3,63.2,1.2,13.3,39.2,33.2,60.5,7.2]:TopTopTopTopTopTopTopTopTopTopTopTop: connection(x0,out(n1,x1)),connection(x2,in(n2,x3)),connection(x0,x2),mode(x1,ok),type(x1,and),connection(out(n1,not1(x4)),in(n2,x1)),mode(not1(x4),ok),connection(out(n1,x5),in(n1,x1)),mode(x3,ok),type(x3,and),connection(out(c,h1(x6)),out(n1,and2(x4))),connection(x7,out(n1,x3)),mode(x5,ok),type(x5,or),value(x8,x9),connection(x8,in(n2,x5)),connection(x10,in(n1,x3)),connection(x11,x10),type(x6,fulladder),type(x4,halfadder),connection(x7,in(n1,or1(x6))),value(out(n1,or1(x6)),n0) -> equal_value(x9,n0),value(x11,n0),value(out(n1,or1(x6)),n1),mode(or1(x6),abnormal)
% 128.54/26.24 === Conflict found: 62:5:2:[12.4,2.2]:TopTop: mode(x0,ok),type(x0,and),value(out(n1,x0),n1),connection(x1,in(n2,x0)) -> value(x1,n1) {x0 -> and1(h2(f)), x1 -> out(n1,not1(h2(f)))}
% 128.54/26.24 === Backtracking. Learning clause 73:9:2:[62.3,1.3,7.2,54.2,21.3,7.2,52.2,69.1]:TopTop: type(and1(h2(f)),and),connection(out(n1,not1(h2(f))),in(n2,and1(h2(f)))),connection(x0,out(n1,and1(h2(f)))),value(x0,n1),type(not1(h2(f)),not),mode(or1(f),abnormal),connection(x1,out(n1,and2(h2(f)))),type(h2(f),halfadder) -> value(x1,n0)
% 128.54/26.24 === Clause set with instances from active satisfied. Growing active. New size: 764
% 128.54/26.24 === Conflict found: 63:4:4:[2.3,2.2]:TopTopTopTop: connection(x0,x1),value(x1,x2),connection(x3,x0) -> value(x3,x2) {x0 -> in(n1,h1(f)), x1 -> in(n1,or1(h1(f))), x2 -> n1, x3 -> in(n2,f)}
% 128.54/26.24
% 128.54/26.24 SZS status Unsatisfiable
% 128.54/26.24
% 128.54/26.24 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.54/26.24
% 128.54/26.24 SPASS-SCL-FOL Statistics:
% 128.54/26.24 Number of learned clauses: 13
% 128.54/26.24 Number of propagations: 2614
% 128.54/26.24 Number of decisions: 2616
% 128.54/26.24 Number of resolutions: 118
% 128.54/26.24 Number of condensations: 4
% 128.54/26.24 Number of sub resolutions: 2
% 128.54/26.24 Number of input literals (deduplicated): 58
% 128.54/26.24 Number of grows: 102
% 128.54/26.24 Number of considered ground atoms: 764
% 128.54/26.24
% 128.54/26.24 Needed: 0:0:25.70
% 128.54/26.24
%------------------------------------------------------------------------------