%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : HWV007-2 : 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/HWV007-2+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 3 7)
% (binary-unit 10 #f 3 7)
% (binary-double 16 #f 3 7)
% (binary 54 #t 3 7)
% (binary-order 27 #f 3 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(62,40,0,124,0,0,701,50,2,763,0,2)
%
%
% START OF PROOF
% 702 [] -connection(X,Y) | -zero(X) | zero(Y).
% 703 [] -connection(X,Y) | -one(X) | one(Y).
% 704 [] -connection(X,Y) | -zero(Y) | zero(X).
% 705 [] -connection(X,Y) | -one(Y) | one(X).
% 706 [] -one(X) | -zero(X).
% 708 [] -zero(in2(X)) | zero(out1(X)) | -and_ok(X).
% 709 [] -one(in2(X)) | -one(in1(X)) | one(out1(X)) | -and_ok(X).
% 711 [] -one(out1(X)) | one(in1(X)) | -and_ok(X).
% 714 [] -logic_and(X) | abnormal(X) | and_ok(X).
% 717 [] -zero(in2(X)) | -zero(in1(X)) | zero(out1(X)) | -or_ok(X).
% 720 [] -zero(out1(X)) | zero(in2(X)) | -or_ok(X).
% 722 [] -logic_or(X) | or_ok(X) | abnormal(X).
% 724 [] -one(in1(X)) | zero(out1(X)) | -not_ok(X).
% 728 [] -logic_not(X) | not_ok(X) | abnormal(X).
% 729 [] logic_and(and1(X)) | -halfadder(X).
% 730 [] logic_and(and2(X)) | -halfadder(X).
% 731 [] logic_not(not1(X)) | -halfadder(X).
% 732 [] logic_or(or1(X)) | -halfadder(X).
% 733 [] connection(in1(X),in1(or1(X))) | -halfadder(X).
% 734 [] connection(in2(X),in2(or1(X))) | -halfadder(X).
% 735 [] connection(in1(X),in1(and2(X))) | -halfadder(X).
% 736 [] connection(in2(X),in2(and2(X))) | -halfadder(X).
% 737 [] connection(outs(X),out1(and1(X))) | -halfadder(X).
% 738 [] connection(outc(X),out1(and2(X))) | -halfadder(X).
% 739 [] connection(out1(or1(X)),in1(and1(X))) | -halfadder(X).
% 740 [] connection(out1(and2(X)),in1(not1(X))) | -halfadder(X).
% 741 [] connection(out1(not1(X)),in2(and1(X))) | -halfadder(X).
% 742 [] halfadder(h1(X)) | -fulladder(X).
% 743 [] halfadder(h2(X)) | -fulladder(X).
% 744 [] logic_or(or1(X)) | -fulladder(X).
% 745 [] connection(outs(h1(X)),in2(h2(X))) | -fulladder(X).
% 746 [] connection(outc(h1(X)),in2(or1(X))) | -fulladder(X).
% 748 [] connection(in1(X),in1(h2(X))) | -fulladder(X).
% 749 [] connection(in2(X),in1(h1(X))) | -fulladder(X).
% 750 [] connection(inc(X),in2(h1(X))) | -fulladder(X).
% 751 [] connection(outs(X),outs(h2(X))) | -fulladder(X).
% 752 [] connection(outc(X),out1(or1(X))) | -fulladder(X).
% 753 [] fulladder(f).
% 754 [] zero(in1(f)).
% 755 [] one(in2(f)).
% 756 [] one(inc(f)).
% 757 [] one(outs(f)).
% 758 [] zero(outc(f)).
% 759 [] -abnormal(and2(h1(f))).
% 760 [] -abnormal(and1(h1(f))) | -abnormal(or1(f)).
% 761 [] -abnormal(not1(h1(f))) | -abnormal(or1(f)).
% 762 [] -abnormal(and1(h2(f))) | -abnormal(or1(f)).
% 763 [] -abnormal(or1(h2(f))) | -abnormal(or1(f)).
% 764 [hyper:742,753] halfadder(h1(f)).
% 765 [hyper:743,753] halfadder(h2(f)).
% 766 [hyper:744,753] logic_or(or1(f)).
% 767 [hyper:745,753] connection(outs(h1(f)),in2(h2(f))).
% 768 [hyper:746,753] connection(outc(h1(f)),in2(or1(f))).
% 770 [hyper:748,753] connection(in1(f),in1(h2(f))).
% 771 [hyper:749,753] connection(in2(f),in1(h1(f))).
% 772 [hyper:750,753] connection(inc(f),in2(h1(f))).
% 773 [hyper:751,753] connection(outs(f),outs(h2(f))).
% 774 [hyper:752,753] connection(outc(f),out1(or1(f))).
% 795 [hyper:729,764] logic_and(and1(h1(f))).
% 796 [hyper:730,764] logic_and(and2(h1(f))).
% 797 [hyper:731,764] logic_not(not1(h1(f))).
% 801 [hyper:735,764] connection(in1(h1(f)),in1(and2(h1(f)))).
% 802 [hyper:736,764] connection(in2(h1(f)),in2(and2(h1(f)))).
% 803 [hyper:737,764] connection(outs(h1(f)),out1(and1(h1(f)))).
% 804 [hyper:738,764] connection(outc(h1(f)),out1(and2(h1(f)))).
% 806 [hyper:740,764] connection(out1(and2(h1(f))),in1(not1(h1(f)))).
% 807 [hyper:741,764] connection(out1(not1(h1(f))),in2(and1(h1(f)))).
% 808 [hyper:729,765] logic_and(and1(h2(f))).
% 811 [hyper:732,765] logic_or(or1(h2(f))).
% 812 [hyper:733,765] connection(in1(h2(f)),in1(or1(h2(f)))).
% 813 [hyper:734,765] connection(in2(h2(f)),in2(or1(h2(f)))).
% 816 [hyper:737,765] connection(outs(h2(f)),out1(and1(h2(f)))).
% 818 [hyper:739,765] connection(out1(or1(h2(f))),in1(and1(h2(f)))).
% 821 [hyper:722,766] or_ok(or1(f)) | abnormal(or1(f)).
% 832 [hyper:714,795] abnormal(and1(h1(f))) | and_ok(and1(h1(f))).
% 833 [hyper:714,796,cut:759] and_ok(and2(h1(f))).
% 835 [hyper:728,797] not_ok(not1(h1(f))) | abnormal(not1(h1(f))).
% 837 [hyper:714,808] abnormal(and1(h2(f))) | and_ok(and1(h2(f))).
% 841 [hyper:722,811] or_ok(or1(h2(f))) | abnormal(or1(h2(f))).
% 854 [hyper:702,770,cut:754] zero(in1(h2(f))).
% 875 [hyper:703,771,cut:755] one(in1(h1(f))).
% 888 [hyper:703,772,cut:756] one(in2(h1(f))).
% 900 [hyper:703,773,cut:757] one(outs(h2(f))).
% 913 [hyper:702,774,cut:758] zero(out1(or1(f))).
% 938 [hyper:720,821,cut:913] zero(in2(or1(f))) | abnormal(or1(f)).
% 1004 [hyper:704,938,768] zero(outc(h1(f))) | abnormal(or1(f)).
% 1134 [hyper:703,801,cut:875] one(in1(and2(h1(f)))).
% 1156 [hyper:703,802,cut:888] one(in2(and2(h1(f)))).
% 1163 [hyper:709,1156,cut:1134,cut:833] one(out1(and2(h1(f)))).
% 1187 [hyper:705,804,cut:1163] one(outc(h1(f))).
% 1194 [hyper:706,1187,1004] abnormal(or1(f)).
% 1223 [hyper:702,812,cut:854] zero(in1(or1(h2(f)))).
% 1275 [hyper:703,816,cut:900] one(out1(and1(h2(f)))).
% 1303 [hyper:760,832,cut:1194] and_ok(and1(h1(f))).
% 1331 [hyper:761,835,cut:1194] not_ok(not1(h1(f))).
% 1364 [hyper:762,837,cut:1194] and_ok(and1(h2(f))).
% 1376 [hyper:711,1364,cut:1275] one(in1(and1(h2(f)))).
% 1431 [hyper:763,841,cut:1194] or_ok(or1(h2(f))).
% 1455 [hyper:703,806,cut:1163] one(in1(not1(h1(f)))).
% 1464 [hyper:724,1455,cut:1331] zero(out1(not1(h1(f)))).
% 1470 [hyper:702,807,cut:1464] zero(in2(and1(h1(f)))).
% 1490 [hyper:708,1470,cut:1303] zero(out1(and1(h1(f)))).
% 1496 [hyper:704,1490,803] zero(outs(h1(f))).
% 1506 [hyper:702,1496,767] zero(in2(h2(f))).
% 1513 [hyper:702,1506,813] zero(in2(or1(h2(f)))).
% 1526 [hyper:705,818,cut:1376] one(out1(or1(h2(f)))).
% 1533 [hyper:717,1513,cut:1223,cut:1431] zero(out1(or1(h2(f)))).
% 1549 [hyper:706,1526,cut:1533] 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 4
% seconds given: 27
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 260
% derived clauses: 2275
% kept clauses: 144
% kept size sum: 887
% kept mid-nuclei: 1064
% kept new demods: 0
% forw unit-subs: 294
% forw double-subs: 213
% forw overdouble-subs: 0
% backward subs: 9
% fast unit cutoff: 87
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 0.6
% process. runtime: 0.4
% specific non-discr-tree subsumption statistics:
% tried: 209
% length fails: 0
% strength fails: 4
% predlist fails: 205
% 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/HWV007-2+noeq.in")
%
%------------------------------------------------------------------------------