%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV007-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 : n013.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 37.83s 9.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV007-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.15/0.34 % Computer : n013.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 12:05:42 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 37.83/9.91 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91 Execution lmodel_grow ended with status: unsatisfiable
% 37.83/9.91 Used heuristic: lmodel_grow
% 37.83/9.91
% 37.83/9.91 Input Clauses:
% 37.83/9.91
% 37.83/9.91 Predicates: connection value equal_value mode type
% 37.83/9.91 Fol Constants: n0 n1 ok abnormal and n2 or not halfadder s c fulladder f
% 37.83/9.91 Fol Functions: in out and1 and2 not1 or1 h1 h2
% 37.83/9.91 Problem Properties:
% 37.83/9.91 This is a full first-order problem without equality.
% 37.83/9.91
% 37.83/9.91 After reduction: Problem Properties:
% 37.83/9.91 This is a full first-order problem without equality.
% 37.83/9.91
% 37.83/9.91
% 37.83/9.91 Reduced Input Clauses:
% 37.83/9.91
% 37.83/9.91 Most General Atoms: connection(x0,x1) value(x0,x1) equal_value(x1,x2) mode(x0,ok) mode(x0,abnormal) type(x0,x1)
% 37.83/9.91
% 37.83/9.91 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: lmodel_grow ===
% 37.83/9.91
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 80
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 98
% 37.83/9.91 === Backtracking. Learning clause 57:3:1:[7.1,25.2]:Top: type(x0,halfadder) -> mode(or1(x0),ok),mode(or1(x0),abnormal)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 124
% 37.83/9.91 === Backtracking. Learning clause 59:6:3:[25.1,58.0,13.3,1.3,7.2,3.2,1.3,27.2]:TopTopTop: value(in(n2,x0),n1),connection(x1,out(n1,or1(x0))),value(x1,x2),type(x0,halfadder) -> mode(or1(x0),abnormal),equal_value(x2,n1)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 145
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 159
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 164
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 173
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 178
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 184
% 37.83/9.91 === Backtracking. Learning clause 60:3:1:[22.1,36.2,7.1]:Top: type(x0,fulladder) -> mode(and1(h2(x0)),ok),mode(and1(h2(x0)),abnormal)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 190
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 197
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 202
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 206
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 209
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 212
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 214
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 220
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 228
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 234
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 240
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 245
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 249
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 256
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 261
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 267
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 269
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 272
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 275
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 278
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 280
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 281
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 286
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 288
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 290
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 292
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 304
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 310
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 315
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 322
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 326
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 334
% 37.83/9.91 === Backtracking. Learning clause 61:4:4:[3.2,1.3]:TopTopTopTop: value(x0,x1),connection(x2,x0),value(x2,x3) -> equal_value(x1,x3)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 343
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 353
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 364
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 372
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 378
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 386
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 389
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 393
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 398
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 402
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 408
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 411
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 415
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 421
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 424
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 428
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 433
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 437
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 440
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 444
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 449
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 452
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 463
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 466
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 469
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 470
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 472
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 473
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 474
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 478
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 481
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 486
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 491
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 497
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 503
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 509
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 518
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 524
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 531
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 535
% 37.83/9.91 === Backtracking. Learning clause 62:5:1:[2.1,27.2,8.3]:Top: value(in(n2,or1(x0)),n0),type(x0,halfadder),mode(x0,ok),type(x0,and) -> value(out(n1,x0),n0)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 540
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 546
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 548
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 550
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 552
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 554
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 555
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 560
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 562
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 563
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 569
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 572
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 575
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 578
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 581
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 586
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 590
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 596
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 600
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 604
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 609
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 613
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 621
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 627
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 633
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 636
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 641
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 646
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 651
% 37.83/9.91 === Backtracking. Learning clause 63:6:5:[1.2,1.3,26.2,61.1]:TopTopTopTopTop: connection(x0,in(n1,x1)),value(x0,x2),type(x1,halfadder),connection(x3,in(n1,or1(x1))),value(x3,x4) -> equal_value(x2,x4)
% 37.83/9.91 === Backtracking. Learning clause 64:4:1:[12.1,7.2]:Top: type(x0,and),value(out(n1,x0),n1) -> value(in(n2,x0),n1),mode(x0,abnormal)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 679
% 37.83/9.91 === Conflict found: 64:4:1:[12.1,7.2]:Top: type(x0,and),value(out(n1,x0),n1) -> value(in(n2,x0),n1),mode(x0,abnormal) {x0 -> and1(h1(f))}
% 37.83/9.91 === Backtracking. Learning clause 65:6:3:[64.3,2.2,1.3]:TopTopTop: type(x0,and),connection(x1,in(n2,x0)),connection(x2,out(n1,x0)),value(x2,n1) -> mode(x0,abnormal),value(x1,n1)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 698
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 716
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 730
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 742
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 748
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 755
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 765
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 772
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 778
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 782
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 786
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 790
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 794
% 37.83/9.91 === Backtracking. Learning clause 67:13:5:[23.1,66.3,1.1,29.2,3.1,10.5,2.3,21.4,65.6]:TopTopTopTopTop: value(in(n2,x0),x1),type(x0,halfadder),mode(and2(x0),ok),connection(out(n1,and2(x0)),in(n1,x2)),mode(x2,ok),type(x2,not),type(x3,and),connection(out(n1,x2),in(n2,x3)),connection(x4,out(n1,x3)),value(x4,n1) -> equal_value(x1,n0),value(in(n1,and2(x0)),n0),mode(x3,abnormal)
% 37.83/9.91 === Clause set with instances from active satisfied. Growing active. New size: 815
% 37.83/9.91 === Backtracking. Learning clause 68:25:9:[15.4,2.2,2.2,2.3,11.4,25.2,32.2,2.2,57.2,67.10,7.2,53.2,56.2,54.2,7.2,55.2,7.3,16.1,2.2,63.5]:TopTopTopTopTopTopTopTopTop: connection(x0,in(n1,or1(h2(f)))),connection(x1,in(n2,or1(h2(f)))),type(and1(h2(f)),and),value(out(n1,and1(h2(f))),n1),connection(x2,x1),type(h2(f),halfadder),value(in(n2,x3),x4),type(x3,halfadder),mode(and2(x3),ok),connection(out(n1,and2(x3)),in(n1,not1(h1(f)))),type(not1(h1(f)),not),type(and1(h1(f)),and),connection(out(n1,not1(h1(f))),in(n2,and1(h1(f)))),connection(x2,out(n1,and1(h1(f)))),type(or1(f),or),value(out(n1,or1(f)),n0),connection(x5,in(n1,or1(f))),connection(x6,in(n1,x7)),value(x6,x8),type(x7,halfadder),connection(x5,in(n1,or1(x7))) -> value(x0,n1),equal_value(x4,n0),value(in(n1,and2(x3)),n0),equal_value(x8,n0)
% 37.83/9.91 === Backtracking. Learning clause 69:10:4:[2.2,9.5,1.2,13.3,7.2,55.1,7.3]:TopTopTopTop: connection(x0,out(n1,x1)),mode(x1,ok),type(x1,and),value(in(n1,x1),n1),value(in(n2,x1),n1),connection(x0,in(x2,or1(f))),type(or1(f),or),type(and1(h2(f)),x3) -> value(out(n1,or1(f)),n1),mode(and1(h2(f)),ok)
% 37.83/9.91 === Backtracking. Learning clause 70:13:4:[7.3,54.2,67.5,53.2,7.3]:TopTopTopTop: value(in(n2,x0),x1),type(x0,halfadder),mode(and2(x0),ok),connection(out(n1,and2(x0)),in(n1,not1(h1(f)))),type(not1(h1(f)),not),type(and1(h1(f)),and),connection(out(n1,not1(h1(f))),in(n2,and1(h1(f)))),connection(x2,out(n1,and1(h1(f)))),value(x2,n1),type(or1(f),x3) -> equal_value(x1,n0),value(in(n1,and2(x0)),n0),mode(or1(f),ok)
% 37.83/9.91 === Backtracking. Learning clause 72:10:4:[23.1,71.3,1.3,69.5,29.2]:TopTopTopTop: value(in(n2,x0),n1),connection(x1,out(n1,and2(x0))),mode(and2(x0),ok),value(in(n1,and2(x0)),n1),connection(x1,in(x2,or1(f))),type(or1(f),or),type(and1(h2(f)),x3),type(x0,halfadder) -> value(out(n1,or1(f)),n1),mode(and1(h2(f)),ok)
% 37.83/9.91 === Backtracking. Learning clause 73:20:5:[2.1,38.2,2.3,15.5,2.3,2.2,7.2,11.4,32.2,56.2,25.2,70.9,7.3]:TopTopTopTopTop: type(x0,fulladder),connection(in(n2,h2(x0)),in(n2,or1(h2(f)))),connection(x1,in(n1,or1(h2(f)))),mode(and1(h2(f)),ok),type(and1(h2(f)),and),value(out(n1,and1(h2(f))),n1),type(h2(f),halfadder),value(in(n2,x2),x3),type(x2,halfadder),mode(and2(x2),ok),connection(out(n1,and2(x2)),in(n1,not1(h1(f)))),type(not1(h1(f)),not),type(and1(h1(f)),and),connection(out(n1,not1(h1(f))),in(n2,and1(h1(f)))),connection(out(s,h1(x0)),out(n1,and1(h1(f)))),type(or1(f),x4) -> value(x1,n1),equal_value(x3,n0),value(in(n1,and2(x2)),n0),mode(or1(f),ok)
% 37.83/9.91
% 37.83/9.91 SZS status Unsatisfiable
% 37.83/9.91
% 37.83/9.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.83/9.91
% 37.83/9.91 SPASS-SCL-FOL Statistics:
% 37.83/9.91 Number of learned clauses: 14
% 37.83/9.91 Number of propagations: 2217
% 37.83/9.91 Number of decisions: 1951
% 37.83/9.91 Number of resolutions: 112
% 37.83/9.91 Number of condensations: 6
% 37.83/9.91 Number of sub resolutions: 3
% 37.83/9.91 Number of input literals (deduplicated): 56
% 37.83/9.91 Number of grows: 125
% 37.83/9.91 Number of considered ground atoms: 815
% 37.83/9.91
% 37.83/9.91 Needed: 0:00:09.34
% 37.83/9.91
%------------------------------------------------------------------------------