%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : HWV008-2.001 : TPTP v3.4.2. Bugfixed v2.7.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art08.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 0.0s
% Output : Assurance 0.0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/HWV/HWV008-2.001+noeq.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: nne
% detected subclass: medium
%
% strategies selected:
% (hyper 27 #f 4 7)
% (binary-unit 10 #f 4 7)
% (binary-double 16 #f 4 7)
% (binary 54 #t 4 7)
% (binary-order 27 #f 4 7)
% (binary-posweight-order 125 #f)
% (binary-order-sos 54 #t)
% (binary-unit-uniteq 27 #f)
% (binary-weightorder 54 #f)
% (binary-order 54 #f)
% (hyper-order 43 #f)
% (binary 109 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(66,40,2,132,0,2,513,50,3,579,0,3)
%
%
% START OF PROOF
% 514 [] -connection(X,Y) | -zero(X) | zero(Y).
% 515 [] -connection(X,Y) | -one(X) | one(Y).
% 516 [] -connection(X,Y) | -zero(Y) | zero(X).
% 518 [] -one(X) | -zero(X).
% 519 [] -zero(in1(X)) | zero(out1(X)) | -and_ok(X).
% 526 [] -logic_and(X) | abnormal(X) | and_ok(X).
% 529 [] -zero(in2(X)) | -zero(in1(X)) | zero(out1(X)) | -or_ok(X).
% 534 [] -logic_or(X) | or_ok(X) | abnormal(X).
% 542 [] logic_and(and2(X)) | -halfadder(X).
% 547 [] connection(in1(X),in1(and2(X))) | -halfadder(X).
% 550 [] connection(outc(X),out1(and2(X))) | -halfadder(X).
% 554 [] halfadder(h1(X)) | -fulladder(X).
% 555 [] halfadder(h2(X)) | -fulladder(X).
% 556 [] logic_or(or1(X)) | -fulladder(X).
% 558 [] connection(outc(h1(X)),in2(or1(X))) | -fulladder(X).
% 559 [] connection(outc(h2(X)),in1(or1(X))) | -fulladder(X).
% 560 [] connection(in1(X),in1(h2(X))) | -fulladder(X).
% 561 [] connection(in2(X),in1(h1(X))) | -fulladder(X).
% 564 [] connection(outc(X),out1(or1(X))) | -fulladder(X).
% 565 [] fulladder(f1(X)) | -nbit_adder1(X).
% 567 [] connection(outc(X),outc(f1(X))) | -nbit_adder1(X).
% 568 [] connection(ina1(X),in1(f1(X))) | -nbit_adder1(X).
% 569 [] connection(inb1(X),in2(f1(X))) | -nbit_adder1(X).
% 571 [] nbit_adder1(a).
% 572 [] zero(ina1(a)).
% 573 [] zero(inb1(a)).
% 576 [] one(outc(a)).
% 577 [] -abnormal(or1(f1(a))).
% 578 [] -abnormal(and2(h1(f1(a)))).
% 579 [] -abnormal(and2(h2(f1(a)))).
% 580 [hyper:565,571] fulladder(f1(a)).
% 582 [hyper:567,571] connection(outc(a),outc(f1(a))).
% 583 [hyper:568,571] connection(ina1(a),in1(f1(a))).
% 584 [hyper:569,571] connection(inb1(a),in2(f1(a))).
% 605 [hyper:554,580] halfadder(h1(f1(a))).
% 606 [hyper:555,580] halfadder(h2(f1(a))).
% 607 [hyper:556,580] logic_or(or1(f1(a))).
% 609 [hyper:558,580] connection(outc(h1(f1(a))),in2(or1(f1(a)))).
% 610 [hyper:559,580] connection(outc(h2(f1(a))),in1(or1(f1(a)))).
% 611 [hyper:560,580] connection(in1(f1(a)),in1(h2(f1(a)))).
% 612 [hyper:561,580] connection(in2(f1(a)),in1(h1(f1(a)))).
% 615 [hyper:564,580] connection(outc(f1(a)),out1(or1(f1(a)))).
% 623 [hyper:542,605] logic_and(and2(h1(f1(a)))).
% 628 [hyper:547,605] connection(in1(h1(f1(a))),in1(and2(h1(f1(a))))).
% 631 [hyper:550,605] connection(outc(h1(f1(a))),out1(and2(h1(f1(a))))).
% 636 [hyper:542,606] logic_and(and2(h2(f1(a)))).
% 641 [hyper:547,606] connection(in1(h2(f1(a))),in1(and2(h2(f1(a))))).
% 644 [hyper:550,606] connection(outc(h2(f1(a))),out1(and2(h2(f1(a))))).
% 648 [hyper:534,607,cut:577] or_ok(or1(f1(a))).
% 665 [hyper:526,623,cut:578] and_ok(and2(h1(f1(a)))).
% 670 [hyper:526,636,cut:579] and_ok(and2(h2(f1(a)))).
% 703 [hyper:515,582,cut:576] one(outc(f1(a))).
% 714 [hyper:514,583,cut:572] zero(in1(f1(a))).
% 729 [hyper:514,584,cut:573] zero(in2(f1(a))).
% 770 [hyper:514,611,cut:714] zero(in1(h2(f1(a)))).
% 800 [hyper:514,612,cut:729] zero(in1(h1(f1(a)))).
% 860 [hyper:515,615,cut:703] one(out1(or1(f1(a)))).
% 925 [hyper:514,628,cut:800] zero(in1(and2(h1(f1(a))))).
% 943 [hyper:519,925,cut:665] zero(out1(and2(h1(f1(a))))).
% 979 [hyper:516,631,cut:943] zero(outc(h1(f1(a)))).
% 984 [hyper:514,979,609] zero(in2(or1(f1(a)))).
% 1050 [hyper:514,641,cut:770] zero(in1(and2(h2(f1(a))))).
% 1058 [hyper:519,1050,cut:670] zero(out1(and2(h2(f1(a))))).
% 1119 [hyper:516,644,cut:1058] zero(outc(h2(f1(a)))).
% 1132 [hyper:514,1119,610] zero(in1(or1(f1(a)))).
% 1142 [hyper:529,1132,cut:984,cut:648] zero(out1(or1(f1(a)))).
% 1149 [hyper:518,1142,cut:860] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 7
% clause depth limited to 5
% seconds given: 27
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 249
% derived clauses: 1400
% kept clauses: 127
% kept size sum: 867
% kept mid-nuclei: 698
% kept new demods: 0
% forw unit-subs: 276
% forw double-subs: 27
% forw overdouble-subs: 0
% backward subs: 0
% fast unit cutoff: 61
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 0.3
% process. runtime: 0.4
% specific non-discr-tree subsumption statistics:
% tried: 88
% length fails: 0
% strength fails: 4
% predlist fails: 84
% aux str. fails: 0
% by-lit fails: 0
% full subs tried: 0
% full subs fail: 0
%
% ; program args: ("/home/graph/tptp/Systems/Gandalf---c-2.6/gandalf" "-time" "600" "/home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/HWV/HWV008-2.001+noeq.in")
%
%------------------------------------------------------------------------------