%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SYN445-1 : TPTP v3.4.2. Released v2.1.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art02.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 248.6s
% Output : Assurance 248.6s
% 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/SYN/SYN445-1+noeq.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: nne
% detected subclass: big
%
% strategies selected:
% (hyper 30 #f 1 19)
% (binary-unit 30 #f 1 19)
% (binary-double 18 #f 1 19)
% (binary 90 #t 1 19)
% (binary-order 30 #f 1 19)
% (binary-posweight-order 54 #f)
% (binary-order-sos 30 #t)
% (binary-unit-uniteq 30 #f)
% (binary-weightorder 30 #f)
% (binary-weightorder-sos 30 #f)
% (binary-order 30 #f)
% (hyper-order 30 #f)
% (binary 168 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(180,40,0,360,0,1,264366,5,3002,264367,1,3002,264367,50,3002,264367,40,3002,264547,0,3002,264751,50,3002,264931,0,3002,265135,50,3003,265315,0,3003,265519,50,3004,265699,0,3004,265903,50,3004,266083,0,3004,266287,50,3005,266467,0,3005,266671,50,3006,266851,0,3006,267055,50,3006,267235,0,3006,267439,50,3007,267619,0,3007,267823,50,3007,268003,0,3008,268207,50,3008,268387,0,3008,268591,50,3009,268771,0,3009,268975,50,3010,269155,0,3010,269359,50,3010,269539,0,3011,269743,50,3011,269923,0,3011,270127,50,3012,270307,0,3012,270511,50,3013,270691,0,3013,270895,50,3013,271075,0,3014,271279,50,3014,271459,0,3014,271663,50,3015,271843,0,3015,272047,50,3016,272227,0,3016,272431,50,3016,272431,40,3016,272611,0,3017,299726,3,3918,300863,4,4368,303085,5,4818,303085,1,4818,303085,50,4818,303085,40,4818,303265,0,4818,422948,3,9321,423916,4,11569,425925,5,13820,425926,1,13820,425926,50,13822,425926,40,13822,426106,0,13823,474051,3,15439,474655,4,16074,475848,5,16824,475849,1,16824,475849,50,16825,475849,40,16825,476029,0,16825,531342,3,19528,531992,4,20877,532739,1,22226,532739,50,22228,532739,40,22228,532919,0,22228,580656,3,23924,581201,4,24479,582377,5,25229,582378,1,25229,582378,50,25230,582378,40,25230,582558,0,25230,582750,50,25230,582750,40,25230,582930,0,25230)
%
%
% START OF PROOF
% 582753 [] -ndr1_0(0) | -c3_1(X) | -c1_1(Z) | -c1_1(Y) | -c1_1(X) | c3_1(Z) | c2_1(Y) | c0_1(Y) | c0_1(X) | c0_1(Z).
% 582754 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c1_1(Z) | -c1_1(X) | c3_1(X) | c2_1(Z) | c1_1(Y) | c0_1(Y) | c0_1(Z).
% 582755 [] -ndr1_0(0) | -c3_1(X) | -c2_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c1_1(X) | c0_1(Z) | c0_1(Y).
% 582757 [] -ndr1_0(0) | -c3_1(X) | -c2_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c1_1(Y) | c0_1(Y) | c0_1(X) | c0_1(Z).
% 582758 [] -ndr1_0(0) | -c3_1(X) | -c1_1(X) | c3_1(Y) | c2_1(Z) | c2_1(Y) | c2_1(X) | c1_1(Z) | c1_1(Y) | c0_1(Z).
% 582759 [] -ndr1_0(0) | -c2_1(X) | -c1_1(X) | c3_1(Y) | c2_1(Z) | c2_1(Y) | c1_1(Z) | c0_1(Z) | c0_1(X) | c0_1(Y).
% 582762 [] -ndr1_0(0) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(X).
% 582769 [?] ?
% 582770 [?] ?
% 582771 [?] ?
% 582776 [?] ?
% 582777 [?] ?
% 582781 [?] ?
% 582782 [?] ?
% 582791 [?] ?
% 582794 [?] ?
% 582795 [?] ?
% 582797 [?] ?
% 582800 [?] ?
% 582802 [?] ?
% 582803 [?] ?
% 582804 [] -hskp1(0) | c2_1(a295).
% 582805 [] -hskp1(0) | c0_1(a295).
% 582806 [] -hskp2(0) | c1_1(a297).
% 582807 [] -hskp3(0) | c3_1(a299).
% 582813 [] -hskp8(0) | c2_1(a305).
% 582815 [] -hskp10(0) | c3_1(a308).
% 582816 [] -hskp10(0) | c1_1(a308).
% 582817 [] -hskp11(0) | c3_1(a309).
% 582818 [] -hskp11(0) | c1_1(a309).
% 582819 [] -hskp12(0) | c3_1(a310).
% 582822 [] -hskp14(0) | c2_1(a315).
% 582823 [] -hskp14(0) | c1_1(a315).
% 582825 [] -hskp16(0) | c3_1(a321).
% 582826 [] -hskp16(0) | c2_1(a321).
% 582832 [] -hskp20(0) | c1_1(a333).
% 582833 [] -hskp21(0) | c3_1(a336).
% 582837 [] -hskp26(0) | c0_1(a349).
% 582848 [] hskp11(0) | hskp12(0) | hskp26(0).
% 582869 [] -hskp16(0) | ndr1_0(0).
% 582879 [] -hskp26(0) | ndr1_0(0).
% 582883 [] hskp16(0) | hskp26(0).
% 582884 [] -c2_1(a349) | -hskp26(0).
% 582885 [] -c3_1(a349) | -hskp26(0).
% 582895 [] -c0_1(a336) | -hskp21(0).
% 582896 [] -c1_1(a336) | -hskp21(0).
% 582897 [] -c2_1(a333) | -hskp20(0).
% 582898 [] -c3_1(a333) | -hskp20(0).
% 582903 [] -c1_1(a321) | -hskp16(0).
% 582906 [] -c0_1(a315) | -hskp14(0).
% 582908 [] -c0_1(a310) | -hskp12(0).
% 582909 [] -c2_1(a310) | -hskp12(0).
% 582910 [] -c2_1(a309) | -hskp11(0).
% 582911 [] -c0_1(a308) | -hskp10(0).
% 582914 [] -c0_1(a305) | -hskp8(0).
% 582915 [] -c1_1(a305) | -hskp8(0).
% 582924 [] -c2_1(a299) | -hskp3(0).
% 582925 [] -c0_1(a297) | -hskp2(0).
% 582926 [] -c3_1(a297) | -hskp2(0).
% 582927 [] -c1_1(a295) | -hskp1(0).
% 582928 [] -c0_1(a294) | -hskp0(0).
% 582929 [] -c2_1(a294) | -hskp0(0).
% 582930 [] -c3_1(a294) | -hskp0(0).
% 583082 [binary:582825,582883] c3_1(a321) | hskp26(0).
% 583083 [binary:582826,582883] c2_1(a321) | hskp26(0).
% 583085 [binary:582869,582883,binarycut:582879] ndr1_0(0).
% 583088 [binary:582753,583085] -c3_1(X) | -c1_1(Z) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Y) | c0_1(Z).
% 583089 [binary:582754,583085] -c2_1(X) | -c2_1(Y) | -c1_1(Z) | -c1_1(Y) | c3_1(Y) | c2_1(Z) | c1_1(X) | c0_1(X) | c0_1(Z).
% 583090 [binary:582755,583085] -c3_1(X) | -c2_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c1_1(X) | c0_1(Z) | c0_1(Y).
% 583092 [binary:582757,583085] -c3_1(X) | -c2_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c1_1(Y) | c0_1(X) | c0_1(Z) | c0_1(Y).
% 583093 [binary:582758,583085] -c3_1(X) | -c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c2_1(Z) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 583094 [binary:582759,583085] -c2_1(X) | -c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(Z) | c1_1(Z) | c0_1(X) | c0_1(Y) | c0_1(Z).
% 583097 [binary:582762,583085] -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(X).
% 583108 [input:582769,cut:583085] hskp12(0) | -c2_1(X) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 583112 [binary:582817,582848] c3_1(a309) | hskp12(0) | hskp26(0).
% 583113 [binary:582818,582848] c1_1(a309) | hskp12(0) | hskp26(0).
% 583124 [input:582770,cut:583085] hskp8(0) | -c2_1(X) | -c2_1(Y) | -c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 583125 [binary:582813,583124] c2_1(a305) | -c2_1(X) | -c2_1(Y) | -c1_1(X) | c3_1(X) | c3_1(Y) | c0_1(Y).
% 583131 [input:582771,cut:583085] hskp12(0) | -c3_1(X) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 583132 [binary:582819,583131] c3_1(a310) | -c3_1(X) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 583155 [input:582802,cut:583085] hskp21(0) | -c0_1(X) | c3_1(X) | c2_1(X).
% 583156 [binary:582833,583155] c3_1(a336) | -c0_1(X) | c3_1(X) | c2_1(X).
% 583160 [input:582803,cut:583085] hskp16(0) | -c3_1(X) | c2_1(X) | c1_1(X).
% 583161 [binary:582825,583160] c3_1(a321) | -c3_1(X) | c2_1(X) | c1_1(X).
% 583162 [binary:582826,583160] c2_1(a321) | -c3_1(X) | c2_1(X) | c1_1(X).
% 583163 [binary:582826,583160,factor] -c3_1(a321) | c2_1(a321) | c1_1(a321).
% 583170 [binary:583082,583097,binarycut:583083] -c0_1(a321) | hskp26(0) | -c3_1(X) | -c1_1(X) | c2_1(X).
% 583177 [binary:583161,583097] -c2_1(a321) | -c0_1(a321) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X).
% 583182 [input:582776,cut:583085] hskp0(0) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X).
% 583192 [input:582777,cut:583085] hskp1(0) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 583193 [binary:582804,583192] c2_1(a295) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 583194 [binary:582805,583192] c0_1(a295) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 583233 [input:582791,cut:583085] hskp11(0) | hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 583234 [binary:582817,583233] c3_1(a309) | hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 583235 [binary:582818,583233] c1_1(a309) | hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 583237 [input:582781,cut:583085] hskp3(0) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 583238 [binary:582807,583237] c3_1(a299) | -c1_1(X) | -c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 583252 [input:582782,cut:583085] hskp0(0) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 583261 [input:582794,cut:583085] hskp0(0) | hskp14(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 583262 [input:582795,cut:583085] hskp11(0) | hskp16(0) | -c2_1(X) | c3_1(X) | c1_1(X).
% 583265 [binary:582818,583262] c1_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c1_1(X).
% 583275 [input:582797,cut:583085] hskp10(0) | hskp11(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 583276 [binary:582815,583275] c3_1(a308) | hskp11(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 583277 [binary:582816,583275] c1_1(a308) | hskp11(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 583288 [input:582800,cut:583085] hskp0(0) | hskp2(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 583343 [binary:583161,583088] -c1_1(a321) | c0_1(a321) | -c3_1(X) | -c1_1(Y) | -c1_1(Z) | c3_1(Y) | c2_1(X) | c2_1(Z) | c1_1(X) | c0_1(Y) | c0_1(Z).
% 583384 [binary:583161,583090] -c2_1(a321) | c1_1(a321) | -c3_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c2_1(Y) | c1_1(X) | c0_1(Z) | c0_1(Y).
% 583431 [binary:583156,583092] -c2_1(a336) | c0_1(a336) | -c0_1(X) | c3_1(X) | c3_1(Z) | c3_1(Y) | c2_1(X) | c2_1(Z) | c1_1(Y) | c0_1(Z) | c0_1(Y).
% 583441 [binary:583276,583092] -c2_1(a308) | c0_1(a308) | hskp11(0) | -c3_1(X) | c3_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c1_1(Y) | c0_1(X) | c0_1(Y) | c0_1(Z).
% 583464 [binary:583089,583125,factor:factor:factor:factor:factor] c1_1(a305) | c0_1(a305) | -c2_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 583480 [binary:583088,583132,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] -c1_1(a310) | c0_1(a310) | -c3_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 583489 [binary:583090,583132,factor:factor:factor:factor:factor] -c2_1(a310) | c1_1(a310) | -c3_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 583497 [binary:583112,583093] -c1_1(a309) | c2_1(a309) | hskp12(0) | hskp26(0) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 583508 [binary:583276,583093,factor:factor] -c1_1(a308) | c2_1(a308) | hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 583600 [binary:583090,583238,factor:factor:factor:factor:factor] -c2_1(a299) | c1_1(a299) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 583688 [binary:583162,583177,factor:factor] -c0_1(a321) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X).
% 583731 [binary:582915,583464,binarycut:582914] -hskp8(0) | -c2_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 583735 [binary:583124,583731,factor:factor:factor] -c2_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 583954 [binary:583277,583508,factor:factor] c2_1(a308) | hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 584080 [binary:583113,583497] c2_1(a309) | hskp12(0) | hskp26(0) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 584085 [binary:582910,584080] -hskp11(0) | hskp12(0) | hskp26(0) | c3_1(X) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 584107 [binary:582848,584085] hskp12(0) | hskp26(0) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 584110 [binary:582819,584107] c3_1(a310) | hskp26(0) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 584111 [binary:582819,584107,factor] c3_1(a310) | c2_1(a310) | c1_1(a310) | hskp26(0) | c2_1(X) | c1_1(X) | c0_1(X).
% 584129 [binary:583093,584110,factor:factor:factor:factor:factor:factor] -c1_1(a310) | c2_1(a310) | hskp26(0) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 584400 [binary:583162,583384,factor:factor] c1_1(a321) | -c3_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c2_1(Y) | c1_1(X) | c0_1(Y) | c0_1(Z).
% 584403 [binary:582903,584400] -hskp16(0) | -c3_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(X) | c2_1(Z) | c1_1(X) | c0_1(Z) | c0_1(Y).
% 584431 [binary:583343,584400,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c0_1(a321) | -c3_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(Y).
% 584436 [binary:583688,584431,factor] -c3_1(X) | -c3_1(Y) | -c1_1(Z) | -c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(Z).
% 584450 [binary:583132,584436,factor:factor:factor] c2_1(a310) | c1_1(a310) | -c3_1(X) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 584476 [binary:583489,584450,factor:factor] c1_1(a310) | -c3_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 584488 [binary:583480,584476,factor:factor:factor:factor:factor] c0_1(a310) | -c3_1(X) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 584497 [binary:582908,584488] -hskp12(0) | -c3_1(X) | -c1_1(Y) | -c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 584504 [binary:583131,584497,factor:factor:factor] -c3_1(X) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 584525 [binary:583238,584504,factor:factor:factor:factor:factor:factor:factor] -c1_1(a299) | c2_1(a299) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584570 [binary:583160,584403,factor] -c3_1(X) | -c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(Z) | c0_1(Y).
% 584590 [binary:583238,584570,factor:factor:factor:factor:factor:factor] c2_1(a299) | c1_1(a299) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584603 [binary:583600,584590,factor] c1_1(a299) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584615 [binary:584525,584603,factor:factor] c2_1(a299) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584621 [binary:582924,584615] -hskp3(0) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584630 [binary:583237,584621,factor:factor] -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 584739 [binary:583954,583441,factor:factor:factor:factor:factor] c0_1(a308) | hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 584741 [binary:582911,584739] -hskp10(0) | hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 584747 [binary:583275,584741,factor] hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 584750 [binary:582817,584747] c3_1(a309) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 584752 [binary:582818,584747] c1_1(a309) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 584767 [binary:583093,584750,factor:factor:factor:factor:factor:factor] -c1_1(a309) | c2_1(a309) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 584781 [binary:584752,584767,factor:factor:factor:factor:factor] c2_1(a309) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 584783 [binary:582910,584781] -hskp11(0) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 584826 [binary:584747,584783,factor:factor] -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 584829 [binary:583156,584826] c2_1(a336) | c1_1(a336) | c0_1(a336) | -c0_1(X) | c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c0_1(Y).
% 584834 [binary:584111,584826,factor:factor:factor] c2_1(a310) | c1_1(a310) | c0_1(a310) | hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584839 [binary:582909,584834,binarycut:582908] -hskp12(0) | c1_1(a310) | hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584864 [binary:584107,584839,factor:factor:factor:factor:factor] c1_1(a310) | hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584895 [binary:584129,584864,factor:factor:factor:factor] c2_1(a310) | hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584900 [binary:582909,584895] -hskp12(0) | hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584929 [binary:584107,584900,factor:factor] hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 584931 [binary:582837,584929] c0_1(a349) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 585072 [binary:583431,584829,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c1_1(a336) | c0_1(a336) | -c0_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585075 [binary:582896,585072,binarycut:582895] -hskp21(0) | -c0_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585099 [binary:583155,585075,factor] -c0_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585125 [binary:584931,585099,factor:factor:factor] c3_1(a349) | c2_1(a349) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 585133 [binary:582885,585125,binarycut:582884] -hskp26(0) | c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 585151 [binary:584929,585133,factor] c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 585159 [binary:582930,585151,binarycut:582929,binarycut:582928] -hskp0(0) | c1_1(a294).
% 585160 [binary:583163,585151] c2_1(a321) | c1_1(a321) | c0_1(a321).
% 585169 [binary:583182,585159] c1_1(a294) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X).
% 585171 [binary:583252,585159] c1_1(a294) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585173 [binary:583261,585159] c1_1(a294) | hskp14(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585174 [binary:583288,585159] c1_1(a294) | hskp2(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585184 [binary:584630,585173] c3_1(a294) | c2_1(a294) | c0_1(a294) | hskp14(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585186 [binary:584630,585174] c3_1(a294) | c2_1(a294) | c0_1(a294) | hskp2(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585202 [binary:584630,585169] c3_1(a294) | c2_1(a294) | c0_1(a294) | -c3_1(Y) | -c3_1(X) | -c1_1(X) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585204 [binary:584630,585171] c3_1(a294) | c2_1(a294) | c0_1(a294) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585208 [binary:582930,585184,binarycut:582929,binarycut:582928] -hskp0(0) | hskp14(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585219 [binary:583261,585208,factor] hskp14(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585221 [binary:582822,585219] c2_1(a315) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585222 [binary:582823,585219] c1_1(a315) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 585233 [binary:582930,585186,binarycut:582929,binarycut:582928] -hskp0(0) | hskp2(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585247 [binary:583288,585233,factor] hskp2(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585249 [binary:582806,585247] c1_1(a297) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585257 [binary:584630,585249] c3_1(a297) | c2_1(a297) | c0_1(a297) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585260 [binary:582926,585257,binarycut:582925] -hskp2(0) | c2_1(a297) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585271 [binary:585247,585260,factor] c2_1(a297) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585275 [binary:583094,585271,factor:factor] -c1_1(a297) | c0_1(a297) | -c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 585276 [binary:583735,585271] -c1_1(a297) | c3_1(a297) | c0_1(a297) | -c3_1(X) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 585318 [binary:582930,585202,binarycut:582929,binarycut:582928] -hskp0(0) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X).
% 585326 [binary:583182,585318,factor:factor:factor] -c3_1(Y) | -c3_1(X) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X).
% 585332 [binary:583112,585326] -c1_1(a309) | c2_1(a309) | hskp12(0) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585338 [binary:583234,585326] -c1_1(a309) | c2_1(a309) | hskp20(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585382 [binary:583113,585332] c2_1(a309) | hskp12(0) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585385 [binary:582930,585204,binarycut:582929,binarycut:582928] -hskp0(0) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y).
% 585399 [binary:582910,585382] -hskp11(0) | hskp12(0) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585405 [binary:582848,585399] hskp12(0) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585409 [binary:582819,585405] c3_1(a310) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585421 [binary:585326,585409,factor] -c1_1(a310) | c2_1(a310) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 585426 [binary:583252,585385,factor:factor] -c1_1(X) | -c0_1(X) | c2_1(X) | c2_1(Y) | c1_1(Y) | c0_1(Y).
% 585431 [binary:583265,585426] -c0_1(a309) | c2_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 585464 [binary:585249,585275,factor:factor] c0_1(a297) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(Y) | c0_1(X).
% 585466 [binary:582925,585464] -hskp2(0) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 585469 [binary:585247,585466,factor] -c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 585487 [binary:585151,585469] c3_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 585491 [binary:582898,585487,binarycut:582897] -hskp20(0) | c0_1(a333) | c2_1(X) | c1_1(X) | c0_1(X).
% 585508 [binary:585326,585487,factor:factor] -c3_1(X) | -c1_1(Y) | c2_1(X) | c2_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 585525 [binary:585151,585508] -c1_1(X) | c2_1(Y) | c2_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 585531 [binary:583265,585525] c2_1(a309) | c0_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 585598 [binary:585249,585276,factor:factor] c3_1(a297) | c0_1(a297) | -c3_1(X) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 585601 [binary:582926,585598,binarycut:582925] -hskp2(0) | -c3_1(X) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 585613 [binary:585247,585601,factor] -c3_1(X) | -c1_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 585617 [binary:583156,585613] c1_1(a336) | c0_1(a336) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 585661 [binary:582896,585617,binarycut:582895] -hskp21(0) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 585682 [binary:583155,585661,factor] -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 585851 [binary:583235,585338,factor] c2_1(a309) | hskp20(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585858 [binary:582910,585851] -hskp11(0) | hskp20(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585867 [binary:583233,585858,factor] hskp20(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 585869 [binary:582832,585867] c1_1(a333) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 585874 [binary:585491,585867,factor:factor] c0_1(a333) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585885 [binary:585426,585869,factor:factor] -c0_1(a333) | c2_1(a333) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585893 [binary:585874,585885,factor:factor:factor] c2_1(a333) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585896 [binary:582897,585893] -hskp20(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585900 [binary:585867,585896,factor:factor] -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c2_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 585910 [binary:585151,585900] -c2_1(X) | -c0_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 585917 [binary:583162,585910,factor:factor] -c0_1(a321) | c1_1(a321) | -c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 585922 [binary:583193,585910] -c0_1(a295) | c1_1(a295) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | c2_1(Z) | c1_1(Y) | c1_1(X) | c1_1(Z) | c0_1(Y) | c0_1(Z).
% 586101 [binary:582910,585531] -hskp11(0) | c0_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 586104 [binary:583262,586101,factor] c0_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 586110 [binary:585431,586104,factor:factor:factor:factor] c2_1(a309) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 586113 [binary:582910,586110] -hskp11(0) | hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 586118 [binary:583262,586113,factor] hskp16(0) | -c2_1(X) | c3_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 586125 [binary:582825,586118,factor] -c2_1(a321) | c3_1(a321) | c1_1(a321) | c2_1(X) | c1_1(X) | c0_1(X).
% 586129 [binary:585160,586125] c3_1(a321) | c1_1(a321) | c0_1(a321) | c2_1(X) | c1_1(X) | c0_1(X).
% 588259 [binary:583194,585922,factor:factor:factor:factor:factor:factor:factor] c1_1(a295) | -c3_1(X) | -c2_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 588263 [binary:582927,588259] -hskp1(0) | -c3_1(X) | -c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 588276 [binary:583192,588263,factor:factor] -c3_1(X) | -c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 588297 [binary:586129,588276,factor:factor:factor] -c2_1(a321) | c1_1(a321) | c0_1(a321) | c2_1(X) | c1_1(X) | c0_1(X).
% 588327 [binary:585160,588297] c1_1(a321) | c0_1(a321) | c2_1(X) | c1_1(X) | c0_1(X).
% 588330 [binary:582903,588327] -hskp16(0) | c0_1(a321) | c2_1(X) | c1_1(X) | c0_1(X).
% 588337 [binary:583160,588330,factor] c0_1(a321) | -c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 588347 [binary:585917,588337,factor:factor] c1_1(a321) | -c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 588352 [binary:582903,588347] -hskp16(0) | -c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 588355 [binary:583160,588352,factor] -c3_1(X) | c2_1(X) | c1_1(X) | c0_1(X).
% 588361 [binary:585151,588355] c2_1(X) | c1_1(X) | c0_1(X).
% 588366 [binary:582909,588361,binarycut:582908] -hskp12(0) | c1_1(a310).
% 588396 [binary:583108,588366] c1_1(a310) | -c2_1(X) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 588401 [binary:585405,588366] c1_1(a310) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 588452 [binary:585421,588401,factor] c2_1(a310) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 588454 [binary:582909,588452] -hskp12(0) | hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 588470 [binary:585405,588454,factor] hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 588472 [binary:582837,588470] c0_1(a349) | -c3_1(X) | c1_1(X) | c0_1(X).
% 588780 [binary:585682,588396,factor:factor:factor] c2_1(a310) | c0_1(a310) | -c2_1(X) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589096 [binary:582909,588780,binarycut:582908] -hskp12(0) | -c2_1(X) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589108 [binary:583108,589096,factor:factor] -c2_1(X) | -c1_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589131 [binary:585221,589108] -c1_1(a315) | c0_1(a315) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589294 [binary:585222,589131,factor:factor] c0_1(a315) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589296 [binary:582906,589294] -hskp14(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589301 [binary:585219,589296,factor] -c3_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 589306 [binary:583156,589301,factor] -c2_1(a336) | c0_1(a336) | -c0_1(X) | c3_1(X) | c2_1(X).
% 589342 [binary:588361,589306] c1_1(a336) | c0_1(a336) | -c0_1(X) | c3_1(X) | c2_1(X).
% 589345 [binary:582896,589342,binarycut:582895] -hskp21(0) | -c0_1(X) | c3_1(X) | c2_1(X).
% 589359 [binary:583155,589345,factor] -c0_1(X) | c3_1(X) | c2_1(X).
% 589387 [binary:588472,589359] c3_1(a349) | c2_1(a349) | -c3_1(X) | c1_1(X) | c0_1(X).
% 589434 [binary:582885,589387,binarycut:582884] -hskp26(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 589441 [binary:588470,589434,factor] -c3_1(X) | c1_1(X) | c0_1(X).
% 589443 [binary:583082,589441] c1_1(a321) | c0_1(a321) | hskp26(0).
% 589453 [binary:582903,589443,binarycut:582883] c0_1(a321) | hskp26(0).
% 589455 [binary:583170,589453] hskp26(0) | -c3_1(X) | -c1_1(X) | c2_1(X).
% 589458 [binary:582837,589455] c0_1(a349) | -c3_1(X) | -c1_1(X) | c2_1(X).
% 589464 [binary:589359,589458] c3_1(a349) | c2_1(a349) | -c3_1(X) | -c1_1(X) | c2_1(X).
% 589557 [binary:582885,589464,binarycut:582884] -hskp26(0) | -c3_1(X) | -c1_1(X) | c2_1(X).
% 589562 [binary:589455,589557,factor] -c3_1(X) | -c1_1(X) | c2_1(X).
% 589564 [binary:583112,589562] -c1_1(a309) | c2_1(a309) | hskp12(0) | hskp26(0).
% 589581 [binary:583113,589564] c2_1(a309) | hskp12(0) | hskp26(0).
% 589583 [binary:582910,589581] -hskp11(0) | hskp12(0) | hskp26(0).
% 589586 [binary:582848,589583] hskp12(0) | hskp26(0).
% 589588 [binary:582819,589586] c3_1(a310) | hskp26(0).
% 589589 [binary:588366,589586] c1_1(a310) | hskp26(0).
% 589595 [binary:589562,589588,binarycut:589589] c2_1(a310) | hskp26(0).
% 589599 [binary:582909,589595,binarycut:589586] hskp26(0).
% 589600 [binary:582837,589599] c0_1(a349).
% 589601 [binary:589359,589600] c3_1(a349) | c2_1(a349).
% 589603 [binary:582885,589601,cut:589599] c2_1(a349).
% 589604 [binary:582884,589603,cut:589599] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using weight-order strategy
% not using sos strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 20364
% derived clauses: 1147409
% kept clauses: 226698
% kept size sum: 788932
% kept mid-nuclei: 261760
% kept new demods: 0
% forw unit-subs: 135
% forw double-subs: 112913
% forw overdouble-subs: 410030
% backward subs: 6389
% fast unit cutoff: 6106
% full unit cutoff: 0
% dbl unit cutoff: 20536
% real runtime: 256.32
% process. runtime: 254.61
% specific non-discr-tree subsumption statistics:
% tried: 112101111
% length fails: 1225560
% strength fails: 37311346
% predlist fails: 55524972
% aux str. fails: 1541673
% by-lit fails: 12229940
% full subs tried: 2417559
% full subs fail: 2354515
%
% ; 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/SYN/SYN445-1+noeq.in")
%
%------------------------------------------------------------------------------