%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : HWV008-2.002 : 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 : art06.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.002+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(74,40,0,148,0,0,757,50,2,831,0,2)
%
%
% START OF PROOF
% 758 [] -connection(X,Y) | -zero(X) | zero(Y).
% 759 [] -connection(X,Y) | -one(X) | one(Y).
% 760 [] -connection(X,Y) | -zero(Y) | zero(X).
% 762 [] -one(X) | -zero(X).
% 763 [] -zero(in1(X)) | zero(out1(X)) | -and_ok(X).
% 770 [] -logic_and(X) | abnormal(X) | and_ok(X).
% 773 [] -zero(in2(X)) | -zero(in1(X)) | zero(out1(X)) | -or_ok(X).
% 778 [] -logic_or(X) | or_ok(X) | abnormal(X).
% 786 [] logic_and(and2(X)) | -halfadder(X).
% 791 [] connection(in1(X),in1(and2(X))) | -halfadder(X).
% 794 [] connection(outc(X),out1(and2(X))) | -halfadder(X).
% 798 [] halfadder(h1(X)) | -fulladder(X).
% 799 [] halfadder(h2(X)) | -fulladder(X).
% 800 [] logic_or(or1(X)) | -fulladder(X).
% 802 [] connection(outc(h1(X)),in2(or1(X))) | -fulladder(X).
% 803 [] connection(outc(h2(X)),in1(or1(X))) | -fulladder(X).
% 804 [] connection(in1(X),in1(h2(X))) | -fulladder(X).
% 805 [] connection(in2(X),in1(h1(X))) | -fulladder(X).
% 808 [] connection(outc(X),out1(or1(X))) | -fulladder(X).
% 810 [] fulladder(f2(X)) | -nbit_adder2(X).
% 813 [] connection(outc(X),outc(f2(X))) | -nbit_adder2(X).
% 816 [] connection(ina2(X),in1(f2(X))) | -nbit_adder2(X).
% 817 [] connection(inb2(X),in2(f2(X))) | -nbit_adder2(X).
% 820 [] nbit_adder2(a).
% 822 [] zero(ina2(a)).
% 824 [] zero(inb2(a)).
% 828 [] one(outc(a)).
% 829 [] -abnormal(or1(f2(a))).
% 830 [] -abnormal(and2(h1(f2(a)))).
% 831 [] -abnormal(and2(h2(f2(a)))).
% 833 [hyper:810,820] fulladder(f2(a)).
% 836 [hyper:813,820] connection(outc(a),outc(f2(a))).
% 839 [hyper:816,820] connection(ina2(a),in1(f2(a))).
% 840 [hyper:817,820] connection(inb2(a),in2(f2(a))).
% 882 [hyper:798,833] halfadder(h1(f2(a))).
% 883 [hyper:799,833] halfadder(h2(f2(a))).
% 884 [hyper:800,833] logic_or(or1(f2(a))).
% 886 [hyper:802,833] connection(outc(h1(f2(a))),in2(or1(f2(a)))).
% 887 [hyper:803,833] connection(outc(h2(f2(a))),in1(or1(f2(a)))).
% 888 [hyper:804,833] connection(in1(f2(a)),in1(h2(f2(a)))).
% 889 [hyper:805,833] connection(in2(f2(a)),in1(h1(f2(a)))).
% 892 [hyper:808,833] connection(outc(f2(a)),out1(or1(f2(a)))).
% 927 [hyper:786,882] logic_and(and2(h1(f2(a)))).
% 932 [hyper:791,882] connection(in1(h1(f2(a))),in1(and2(h1(f2(a))))).
% 935 [hyper:794,882] connection(outc(h1(f2(a))),out1(and2(h1(f2(a))))).
% 940 [hyper:786,883] logic_and(and2(h2(f2(a)))).
% 945 [hyper:791,883] connection(in1(h2(f2(a))),in1(and2(h2(f2(a))))).
% 948 [hyper:794,883] connection(outc(h2(f2(a))),out1(and2(h2(f2(a))))).
% 952 [hyper:778,884,cut:829] or_ok(or1(f2(a))).
% 982 [hyper:770,927,cut:830] and_ok(and2(h1(f2(a)))).
% 986 [hyper:770,940,cut:831] and_ok(and2(h2(f2(a)))).
% 1047 [hyper:759,836,cut:828] one(outc(f2(a))).
% 1081 [hyper:758,839,cut:822] zero(in1(f2(a))).
% 1093 [hyper:758,840,cut:824] zero(in2(f2(a))).
% 1246 [hyper:758,888,cut:1081] zero(in1(h2(f2(a)))).
% 1264 [hyper:758,889,cut:1093] zero(in1(h1(f2(a)))).
% 1298 [hyper:759,892,cut:1047] one(out1(or1(f2(a)))).
% 1561 [hyper:758,932,cut:1264] zero(in1(and2(h1(f2(a))))).
% 1569 [hyper:763,1561,cut:982] zero(out1(and2(h1(f2(a))))).
% 1610 [hyper:760,935,cut:1569] zero(outc(h1(f2(a)))).
% 1615 [hyper:758,1610,886] zero(in2(or1(f2(a)))).
% 1664 [hyper:758,945,cut:1246] zero(in1(and2(h2(f2(a))))).
% 1680 [hyper:763,1664,cut:986] zero(out1(and2(h2(f2(a))))).
% 1713 [hyper:760,948,cut:1680] zero(outc(h2(f2(a)))).
% 1726 [hyper:758,1713,887] zero(in1(or1(f2(a)))).
% 1736 [hyper:773,1726,cut:1615,cut:952] zero(out1(or1(f2(a)))).
% 1743 [hyper:762,1736,cut:1298] 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: 348
% derived clauses: 2300
% kept clauses: 221
% kept size sum: 1569
% kept mid-nuclei: 1155
% kept new demods: 0
% forw unit-subs: 424
% forw double-subs: 45
% forw overdouble-subs: 0
% backward subs: 0
% fast unit cutoff: 66
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 0.6
% process. runtime: 0.5
% specific non-discr-tree subsumption statistics:
% tried: 118
% length fails: 0
% strength fails: 4
% predlist fails: 114
% 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.002+noeq.in")
%
%------------------------------------------------------------------------------