↑ Up

Gandalf---c-2.6.UNS-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Gandalf---c-2.6
% Problem  : SYN512-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 249.2s
% Output   : Assurance 249.2s
% 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/SYN512-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(206,40,1,412,0,2,133224,4,2528,150931,5,3003,150931,1,3003,150931,50,3003,150931,40,3003,151137,0,3003,151357,50,3004,151563,0,3006,151783,50,3006,151989,0,3006,152209,50,3007,152415,0,3008,152635,50,3009,152841,0,3011,153061,50,3011,153267,0,3011,153487,50,3012,153693,0,3013,153913,50,3014,154119,0,3015,154339,50,3016,154545,0,3016,154765,50,3016,154971,0,3018,155191,50,3018,155397,0,3020,155617,50,3021,155823,0,3021,156043,50,3021,156249,0,3023,156469,50,3023,156675,0,3025,156895,50,3026,157101,0,3026,157321,50,3026,157527,0,3028,157747,50,3028,157953,0,3030,158173,50,3031,158379,0,3031,158599,50,3031,158805,0,3033,159025,50,3033,159231,0,3035,159451,50,3036,159657,0,3036,159877,50,3036,159877,40,3036,160083,0,3038,179294,3,3939,180974,4,4389,181962,5,4839,181963,5,4839,181964,1,4839,181964,50,4839,181964,40,4839,182170,0,4839,305079,3,9343,305986,4,11591,309932,5,13842,309933,1,13842,309933,50,13844,309933,40,13844,310139,0,13845,375442,3,15504,375833,4,16096,376815,5,16846,376816,1,16846,376816,50,16848,376816,40,16848,377022,0,16848,441299,3,19549,442183,4,20899,442929,5,22249,442930,1,22249,442930,50,22251,442930,40,22251,443136,0,22251,507221,3,23927,507608,4,24503,508611,5,25252,508612,1,25252,508612,50,25254,508612,40,25254,508818,0,25254,509031,50,25254,509031,40,25254,509237,0,25258)
% 
% 
% START OF PROOF
% 509032 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(Y).
% 509033 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c0_1(Z) | c0_1(X).
% 509034 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y).
% 509035 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c3_1(X) | c2_1(Z).
% 509037 [] -ndr1_0(0) | hskp25(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y).
% 509043 [] -ndr1_0(0) | hskp5(0) | -c3_1(X) | -c3_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c0_1(X).
% 509044 [] -ndr1_0(0) | hskp11(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c3_1(Y) | c0_1(Y).
% 509046 [] -ndr1_0(0) | hskp17(0) | -c1_1(X) | -c1_1(Y) | -c2_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X).
% 509050 [?] ?
% 509051 [?] ?
% 509054 [?] ?
% 509056 [?] ?
% 509059 [?] ?
% 509061 [?] ?
% 509062 [?] ?
% 509063 [?] ?
% 509064 [?] ?
% 509065 [?] ?
% 509068 [?] ?
% 509070 [?] ?
% 509074 [?] ?
% 509078 [?] ?
% 509080 [?] ?
% 509081 [?] ?
% 509087 [?] ?
% 509090 [?] ?
% 509093 [?] ?
% 509096 [?] ?
% 509097 [?] ?
% 509100 [?] ?
% 509101 [] -hskp0(0) | c2_1(a828).
% 509102 [] -hskp0(0) | c1_1(a828).
% 509103 [] -hskp2(0) | c0_1(a830).
% 509104 [] -hskp3(0) | c3_1(a831).
% 509105 [] -hskp3(0) | c2_1(a831).
% 509106 [] -hskp5(0) | c2_1(a833).
% 509107 [] -hskp5(0) | c0_1(a833).
% 509108 [] -hskp7(0) | c3_1(a836).
% 509109 [] -hskp7(0) | c0_1(a836).
% 509110 [] -hskp8(0) | c1_1(a838).
% 509111 [] -hskp9(0) | c1_1(a841).
% 509112 [] -hskp9(0) | c0_1(a841).
% 509114 [] -hskp11(0) | c3_1(a844).
% 509115 [] -hskp12(0) | c3_1(a845).
% 509116 [] -hskp13(0) | c3_1(a846).
% 509117 [] -hskp14(0) | c2_1(a851).
% 509118 [] -hskp14(0) | c1_1(a851).
% 509119 [] -hskp15(0) | c3_1(a853).
% 509120 [] -hskp15(0) | c1_1(a853).
% 509121 [] -hskp17(0) | c0_1(a859).
% 509124 [] -hskp19(0) | c3_1(a863).
% 509125 [] -hskp19(0) | c0_1(a863).
% 509127 [] -hskp21(0) | c2_1(a865).
% 509128 [] -hskp22(0) | c1_1(a866).
% 509129 [] -hskp22(0) | c0_1(a866).
% 509131 [] -hskp24(0) | c3_1(a884).
% 509132 [] -hskp24(0) | c1_1(a884).
% 509133 [] -hskp25(0) | c2_1(a890).
% 509140 [] -hskp29(0) | c2_1(a849).
% 509141 [] -hskp29(0) | c1_1(a849).
% 509142 [] -hskp29(0) | c0_1(a849).
% 509150 [] hskp2(0) | hskp16(0) | hskp17(0).
% 509169 [] -hskp14(0) | ndr1_0(0).
% 509176 [] -hskp21(0) | ndr1_0(0).
% 509187 [] hskp14(0) | hskp21(0).
% 509193 [] -c0_1(a890) | -hskp25(0).
% 509194 [] -c3_1(a890) | -hskp25(0).
% 509195 [] -c2_1(a884) | -hskp24(0).
% 509198 [] -c3_1(a866) | -hskp22(0).
% 509200 [] -c1_1(a865) | -hskp21(0).
% 509203 [] -c2_1(a863) | -hskp19(0).
% 509205 [] -c1_1(a859) | -hskp17(0).
% 509206 [] -c3_1(a859) | -hskp17(0).
% 509207 [] -c0_1(a858) | -hskp16(0).
% 509208 [] -c1_1(a858) | -hskp16(0).
% 509209 [] -c2_1(a858) | -hskp16(0).
% 509210 [] -c0_1(a853) | -hskp15(0).
% 509211 [] -c3_1(a851) | -hskp14(0).
% 509212 [] -c0_1(a846) | -hskp13(0).
% 509213 [] -c2_1(a846) | -hskp13(0).
% 509214 [] -c0_1(a845) | -hskp12(0).
% 509215 [] -c1_1(a845) | -hskp12(0).
% 509216 [] -c1_1(a844) | -hskp11(0).
% 509217 [] -c2_1(a844) | -hskp11(0).
% 509220 [] -c2_1(a841) | -hskp9(0).
% 509221 [] -c2_1(a838) | -hskp8(0).
% 509222 [] -c3_1(a838) | -hskp8(0).
% 509223 [] -c1_1(a836) | -hskp7(0).
% 509224 [] -c0_1(a835) | -hskp6(0).
% 509225 [] -c2_1(a835) | -hskp6(0).
% 509226 [] -c3_1(a835) | -hskp6(0).
% 509227 [] -c3_1(a833) | -hskp5(0).
% 509228 [] -c1_1(a832) | -hskp4(0).
% 509229 [] -c2_1(a832) | -hskp4(0).
% 509230 [] -c3_1(a832) | -hskp4(0).
% 509231 [] -c1_1(a831) | -hskp3(0).
% 509232 [] -c1_1(a830) | -hskp2(0).
% 509233 [] -c2_1(a830) | -hskp2(0).
% 509237 [] -c0_1(a828) | -hskp0(0).
% 509392 [binary:509117,509187] c2_1(a851) | hskp21(0).
% 509393 [binary:509118,509187] c1_1(a851) | hskp21(0).
% 509395 [binary:509169,509187,binarycut:509176] ndr1_0(0).
% 509396 [binary:509032,509395] -c1_1(X) | -c1_1(Y) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(X).
% 509397 [binary:509033,509395] -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Z) | -c2_1(X) | -c0_1(Z) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 509398 [binary:509034,509395] -c1_1(X) | -c1_1(Y) | -c3_1(X) | -c3_1(Y) | -c0_1(Z) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(X).
% 509399 [binary:509035,509395] -c2_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z).
% 509401 [binary:509037,509395] hskp25(0) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(Y).
% 509407 [binary:509043,509395] hskp5(0) | -c3_1(X) | -c3_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c0_1(X).
% 509408 [binary:509044,509395] hskp11(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c3_1(Y) | c0_1(Y).
% 509410 [binary:509046,509395] hskp17(0) | -c1_1(X) | -c1_1(Y) | -c2_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X).
% 509416 [input:509050,cut:509395] hskp17(0) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(Y).
% 509417 [binary:509121,509416] c0_1(a859) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(Y).
% 509424 [input:509051,cut:509395] hskp3(0) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c2_1(Y) | c2_1(X).
% 509425 [binary:509104,509424] c3_1(a831) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 509426 [binary:509105,509424] c2_1(a831) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 509434 [binary:509103,509150] c0_1(a830) | hskp16(0) | hskp17(0).
% 509453 [input:509054,cut:509395] hskp4(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X).
% 509471 [input:509074,cut:509395] hskp6(0) | hskp16(0) | -c2_1(X) | -c0_1(X) | c3_1(X).
% 509472 [input:509056,cut:509395] hskp15(0) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 509473 [binary:509119,509472] c3_1(a853) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 509474 [binary:509120,509472] c1_1(a853) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 509487 [input:509078,cut:509395] hskp5(0) | hskp16(0) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 509488 [binary:509106,509487] c2_1(a833) | hskp16(0) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 509489 [binary:509107,509487] c0_1(a833) | hskp16(0) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 509496 [input:509080,cut:509395] hskp8(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 509497 [binary:509110,509496] c1_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 509501 [input:509081,cut:509395] hskp2(0) | hskp12(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 509502 [binary:509103,509501] c0_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 509505 [input:509059,cut:509395] hskp5(0) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c0_1(Y).
% 509506 [binary:509106,509505] c2_1(a833) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c0_1(Y).
% 509507 [binary:509107,509505] c0_1(a833) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c0_1(Y).
% 509517 [input:509061,cut:509395] hskp3(0) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 509518 [binary:509104,509517] c3_1(a831) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 509519 [binary:509105,509517] c2_1(a831) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 509529 [input:509062,cut:509395] hskp13(0) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X).
% 509530 [binary:509116,509529] c3_1(a846) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X).
% 509541 [input:509063,cut:509395] hskp24(0) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X).
% 509542 [binary:509131,509541] c3_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X).
% 509544 [binary:509132,509541] c1_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X).
% 509555 [input:509064,cut:509395] hskp29(0) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 509556 [binary:509140,509555] c2_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 509558 [binary:509141,509555] c1_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 509560 [binary:509142,509555] c0_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 509561 [input:509087,cut:509395] hskp11(0) | hskp19(0) | -c0_1(X) | c1_1(X) | c2_1(X).
% 509562 [binary:509114,509561] c3_1(a844) | hskp19(0) | -c0_1(X) | c1_1(X) | c2_1(X).
% 509570 [input:509065,cut:509395] hskp7(0) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 509571 [binary:509108,509570] c3_1(a836) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 509573 [binary:509109,509570] c0_1(a836) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 509587 [input:509090,cut:509395] hskp4(0) | hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 509594 [input:509068,cut:509395] hskp6(0) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 509595 [input:509093,cut:509395] hskp3(0) | hskp29(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 509596 [binary:509104,509595] c3_1(a831) | hskp29(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 509597 [binary:509105,509595] c2_1(a831) | hskp29(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 509615 [input:509070,cut:509395] hskp0(0) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509616 [binary:509101,509615] c2_1(a828) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 509620 [binary:509102,509615] c1_1(a828) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 509625 [input:509096,cut:509395] hskp2(0) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 509626 [binary:509103,509625] c0_1(a830) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 509628 [input:509097,cut:509395] hskp4(0) | hskp11(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 509635 [input:509100,cut:509395] hskp4(0) | hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 509735 [binary:509133,509401] c2_1(a890) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(Y).
% 509763 [binary:509106,509407] c2_1(a833) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c0_1(Y).
% 509764 [binary:509107,509407] c0_1(a833) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c0_1(Y).
% 509768 [binary:509114,509408] c3_1(a844) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c3_1(Y) | c0_1(Y).
% 509776 [binary:509121,509410] c0_1(a859) | -c1_1(X) | -c1_1(Y) | -c2_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 509796 [binary:509399,509426] -c0_1(a831) | c1_1(a831) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(U) | c1_1(Z) | c3_1(U) | c3_1(Y) | c2_1(U) | c2_1(Z) | c2_1(X).
% 509819 [binary:509398,509474,factor:factor:factor] -c3_1(a853) | c0_1(a853) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(X) | -c0_1(Z) | c3_1(Z) | c2_1(Y) | c2_1(X) | c2_1(Z) | c0_1(Y).
% 509848 [binary:509399,509519,factor:factor:factor:factor:factor] -c0_1(a831) | c1_1(a831) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 509859 [binary:509398,509544,factor:factor:factor] -c3_1(a884) | c0_1(a884) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Y) | c2_1(Z).
% 509875 [binary:509396,509620] -c2_1(a828) | c0_1(a828) | -c1_1(X) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(U) | c2_1(Y) | c2_1(Z) | c2_1(U) | c0_1(Z) | c0_1(U).
% 509876 [binary:509397,509620] -c2_1(a828) | c0_1(a828) | -c3_1(Y) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c3_1(U) | c2_1(Z) | c2_1(U) | c0_1(Y) | c0_1(Z) | c0_1(U).
% 509923 [binary:509399,509763] -c0_1(a833) | c1_1(a833) | -c3_1(Y) | -c3_1(X) | -c2_1(Z) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(U) | c1_1(X) | c3_1(U) | c3_1(Z) | c2_1(U) | c0_1(Y).
% 510394 [binary:509473,509819,factor:factor:factor:factor] c0_1(a853) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Z) | -c0_1(X) | c3_1(Z) | c2_1(X) | c2_1(Y) | c2_1(Z) | c0_1(Y).
% 510396 [binary:509210,510394] -hskp15(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | -c0_1(X) | c3_1(Z) | c2_1(Z) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 510412 [binary:509472,510396,factor:factor] -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Z) | c3_1(Z) | c2_1(Y) | c2_1(X) | c2_1(Z) | c0_1(Y).
% 510435 [binary:509544,510412,factor:factor:factor:factor:factor:factor:factor:factor:factor] -c3_1(a884) | -c0_1(a884) | c2_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 510461 [binary:509542,510435,factor:factor:factor:factor:factor] -c0_1(a884) | c2_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 510507 [binary:509542,509859,factor:factor:factor] c0_1(a884) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X).
% 510519 [binary:510461,510507,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] -c1_1(a884) | -c3_1(a884) | c2_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 510525 [binary:509544,510519,factor:factor:factor:factor:factor] -c3_1(a884) | c2_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 510531 [binary:509542,510525,factor:factor:factor] c2_1(a884) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 510533 [binary:509195,510531] -hskp24(0) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 510558 [binary:509541,510533,factor:factor] -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 510569 [binary:509530,510558,factor:factor:factor:factor] c1_1(a846) | c2_1(a846) | c0_1(a846) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 510659 [binary:509398,510569,factor:factor:factor:factor:factor:factor:factor] -c1_1(a846) | -c3_1(a846) | c2_1(a846) | c0_1(a846) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 510706 [binary:509616,509875,factor:factor:factor:factor:factor:factor:factor:factor:factor] c0_1(a828) | -c1_1(X) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(Y) | c2_1(Z) | c0_1(Z).
% 510710 [binary:509237,510706] -hskp0(0) | -c1_1(X) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(Z).
% 510714 [binary:509615,510710,factor:factor:factor] -c1_1(X) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(Z).
% 510747 [binary:509558,510714,factor:factor:factor] -c3_1(a849) | -c2_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 510787 [binary:509616,509876,factor:factor:factor:factor:factor:factor:factor:factor] c0_1(a828) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(X) | c0_1(Z).
% 510795 [binary:509237,510787] -hskp0(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c2_1(Z) | c0_1(Z) | c0_1(X).
% 510804 [binary:509615,510795,factor:factor:factor] -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(X) | c0_1(Z).
% 510830 [binary:509518,510804,factor:factor:factor:factor:factor:factor] c1_1(a831) | c0_1(a831) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 510841 [binary:509231,510830] -hskp3(0) | c0_1(a831) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 510855 [binary:509517,510841,factor:factor:factor:factor] c0_1(a831) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 510873 [binary:509848,510855,factor:factor:factor:factor:factor:factor] c1_1(a831) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(Z).
% 510972 [binary:509231,510873] -hskp3(0) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(Z).
% 510983 [binary:509517,510972,factor:factor] -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 511018 [binary:509571,510983,factor] -c2_1(a836) | -c0_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 511073 [binary:510569,510659,factor:factor:factor:factor:factor:factor:factor:factor] -c3_1(a846) | c2_1(a846) | c0_1(a846) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 511079 [binary:509530,511073,factor:factor:factor] c2_1(a846) | c0_1(a846) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 511083 [binary:509213,511079,binarycut:509212] -hskp13(0) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 511087 [binary:509529,511083,factor:factor] -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 511094 [binary:509562,511087,factor:factor:factor] c1_1(a844) | c2_1(a844) | hskp19(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511104 [binary:509768,511087] c1_1(a844) | c2_1(a844) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Y).
% 511122 [binary:509216,511094,binarycut:509217] -hskp11(0) | hskp19(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511128 [binary:509561,511122,factor] hskp19(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511130 [binary:509124,511128] c3_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511132 [binary:509125,511128] c0_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511138 [binary:511087,511130,factor:factor:factor] c1_1(a863) | c2_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 511246 [binary:509764,509923,factor:factor:factor:factor:factor] c1_1(a833) | -c3_1(X) | -c3_1(Y) | -c2_1(Z) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(U) | c1_1(X) | c3_1(U) | c3_1(Z) | c2_1(U) | c0_1(Y).
% 511491 [binary:509216,511104,binarycut:509217] -hskp11(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Y).
% 511495 [binary:509408,511491,factor:factor] -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Y).
% 511554 [binary:511138,511495,factor:factor:factor] -c3_1(a863) | -c0_1(a863) | c2_1(a863) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 511600 [binary:511130,511554,factor:factor:factor] -c0_1(a863) | c2_1(a863) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 511620 [binary:511132,511600,factor:factor] c2_1(a863) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 511622 [binary:509203,511620] -hskp19(0) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 511643 [binary:511128,511622,factor] -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 511657 [binary:509735,511643] c3_1(a890) | c0_1(a890) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Z) | c3_1(Z) | c2_1(Y) | c2_1(Z).
% 512198 [binary:509194,511657,binarycut:509193] -hskp25(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 512202 [binary:509401,512198,factor:factor] -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 512247 [binary:511138,512202,factor:factor:factor:factor:factor] -c3_1(a863) | -c0_1(a863) | c2_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 512277 [binary:511130,512247,factor:factor:factor] -c0_1(a863) | c2_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 512289 [binary:511132,512277,factor:factor] c2_1(a863) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 512291 [binary:509203,512289] -hskp19(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 512319 [binary:511128,512291,factor] -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 512322 [binary:509502,512319] c1_1(a830) | c3_1(a830) | c2_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 512324 [binary:509626,512319,factor] c1_1(a830) | c3_1(a830) | c2_1(a830) | hskp9(0).
% 512325 [binary:509417,512319] c1_1(a859) | c3_1(a859) | c2_1(a859) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(Y).
% 512330 [binary:509776,512319] c1_1(a859) | c3_1(a859) | c2_1(a859) | -c1_1(Y) | -c1_1(X) | -c2_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y).
% 512334 [binary:509232,512324,binarycut:509233] -hskp2(0) | c3_1(a830) | hskp9(0).
% 512340 [binary:509625,512334] c3_1(a830) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 512364 [binary:509232,512322,binarycut:509233] -hskp2(0) | c3_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 512368 [binary:509501,512364,factor] c3_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 512377 [binary:509205,512325,binarycut:509206] -hskp17(0) | c2_1(a859) | -c1_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y).
% 512386 [binary:509416,512377,factor:factor:factor:factor:factor] c2_1(a859) | -c1_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y).
% 512390 [binary:509399,512386,factor:factor:factor:factor:factor] -c0_1(a859) | c1_1(a859) | -c1_1(X) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(X) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 512429 [binary:509205,512330,binarycut:509206] -hskp17(0) | c2_1(a859) | -c1_1(X) | -c1_1(Y) | -c2_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X).
% 512436 [binary:509410,512429,factor:factor:factor] c2_1(a859) | -c1_1(X) | -c1_1(Y) | -c2_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 512439 [binary:509399,512436,factor] -c0_1(a859) | c1_1(a859) | -c1_1(Y) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(X) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c2_1(X).
% 512573 [binary:509417,512390,factor:factor:factor:factor:factor] c1_1(a859) | -c1_1(X) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c3_1(X) | c2_1(Z) | c2_1(Y).
% 512577 [binary:509205,512573] -hskp17(0) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c3_1(X) | c2_1(Y) | c2_1(Z).
% 512585 [binary:509416,512577,factor:factor:factor] -c1_1(X) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c3_1(X) | c2_1(Z) | c2_1(Y).
% 512700 [binary:509776,512439,factor:factor:factor] c1_1(a859) | -c1_1(Y) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Z) | c3_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z).
% 512702 [binary:509205,512700] -hskp17(0) | -c1_1(Y) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c3_1(X) | c2_1(Z) | c2_1(Y).
% 512709 [binary:509410,512702,factor:factor] -c1_1(X) | -c1_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c3_1(X) | c2_1(Z) | c2_1(Y).
% 512737 [binary:509558,512709,factor:factor:factor:factor:factor:factor:factor:factor] -c2_1(a849) | -c0_1(a849) | c3_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 512775 [binary:509556,512737,factor:factor:factor:factor:factor:factor] -c0_1(a849) | c3_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y).
% 512783 [binary:509560,512775,factor:factor:factor:factor:factor] c3_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 512788 [binary:510747,512783,factor:factor] -c2_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 512792 [binary:509556,512788,factor:factor] -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 513576 [binary:512585,511246,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] -c2_1(a833) | -c0_1(a833) | c3_1(a833) | -c3_1(Y) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(X).
% 514109 [binary:509763,513576,factor:factor:factor:factor:factor] -c0_1(a833) | c3_1(a833) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Y).
% 514118 [binary:509764,514109,factor:factor:factor:factor] c3_1(a833) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Y).
% 514120 [binary:509227,514118] -hskp5(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(X) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y).
% 514143 [binary:509407,514120,factor:factor] -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Y).
% 514167 [binary:509571,514143,factor:factor:factor:factor] -c0_1(a836) | c1_1(a836) | c2_1(a836) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Z) | c0_1(Y).
% 514185 [binary:512340,514143,factor:factor:factor] -c0_1(a830) | c1_1(a830) | c2_1(a830) | hskp9(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514189 [binary:512368,514143,factor] -c0_1(a830) | c1_1(a830) | c2_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514261 [binary:509626,514185,factor:factor:factor] c1_1(a830) | c2_1(a830) | hskp9(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514273 [binary:509232,514261,binarycut:509233] -hskp2(0) | hskp9(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514298 [binary:509625,514273,factor] hskp9(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514300 [binary:509111,514298] c1_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514301 [binary:509111,514298,factor] c1_1(a841) | c3_1(a841) | c2_1(a841) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 514302 [binary:509112,514298] c0_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514306 [binary:512792,514301] -c0_1(a841) | c3_1(a841) | c2_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 514362 [binary:514302,514306,factor:factor:factor:factor:factor:factor] c3_1(a841) | c2_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 514368 [binary:509502,514189,factor] c1_1(a830) | c2_1(a830) | hskp12(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514371 [binary:509232,514368,binarycut:509233] -hskp2(0) | hskp12(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514392 [binary:509501,514371,factor] hskp12(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514394 [binary:509115,514392] c3_1(a845) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 514406 [binary:510804,514394,factor:factor:factor:factor:factor] c1_1(a845) | c0_1(a845) | -c3_1(Y) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(Z) | c0_1(Y).
% 514500 [binary:509215,514406,binarycut:509214] -hskp12(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(Y) | c0_1(Z).
% 514510 [binary:514392,514500,factor:factor:factor] -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c0_1(Y) | c0_1(Z).
% 514537 [binary:509571,514510,factor:factor] -c2_1(a836) | -c0_1(a836) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 514770 [binary:509573,514167,factor:factor:factor:factor:factor] c1_1(a836) | c2_1(a836) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 514772 [binary:509223,514770] -hskp7(0) | c2_1(a836) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z) | c0_1(Y).
% 514786 [binary:509570,514772,factor:factor:factor] c2_1(a836) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Y) | c0_1(Z).
% 514801 [binary:514537,514786,factor:factor:factor] -c0_1(a836) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 514806 [binary:509573,514801,factor:factor] -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 514831 [binary:514300,514806,factor:factor:factor:factor:factor:factor] -c3_1(a841) | c2_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 514849 [binary:514362,514831,factor:factor:factor:factor] c2_1(a841) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 514852 [binary:509220,514849] -hskp9(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 514865 [binary:514298,514852,factor:factor] -c3_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 514870 [binary:509596,514865] -c2_1(a831) | c0_1(a831) | hskp29(0) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 514873 [binary:509425,514865] -c2_1(a831) | c0_1(a831) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(X) | c2_1(Y) | c2_1(Z) | c0_1(Z).
% 514969 [binary:509597,514870,factor:factor] c0_1(a831) | hskp29(0) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 515080 [binary:509426,514873,factor:factor:factor:factor:factor] c0_1(a831) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 515092 [binary:509796,515080,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c1_1(a831) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c3_1(Y) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 515120 [binary:509231,515092] -hskp3(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 515135 [binary:509424,515120,factor:factor:factor] -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 515159 [binary:509571,515135,factor:factor:factor] -c0_1(a836) | c1_1(a836) | c2_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 515163 [binary:512340,515135,factor:factor:factor] -c0_1(a830) | c1_1(a830) | c2_1(a830) | hskp9(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515204 [binary:509626,515163,factor:factor:factor] c1_1(a830) | c2_1(a830) | hskp9(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515217 [binary:509232,515204,binarycut:509233] -hskp2(0) | hskp9(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515225 [binary:509625,515217,factor] hskp9(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515227 [binary:509111,515225] c1_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515229 [binary:509112,515225] c0_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515253 [binary:512792,515227,factor:factor:factor:factor:factor] -c0_1(a841) | c3_1(a841) | c2_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515268 [binary:515229,515253,factor:factor:factor:factor:factor:factor:factor] c3_1(a841) | c2_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515714 [binary:509573,515159,factor:factor:factor:factor:factor] c1_1(a836) | c2_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 515716 [binary:509223,515714] -hskp7(0) | c2_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 515731 [binary:509570,515716,factor:factor:factor] c2_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 515744 [binary:511018,515731,factor:factor:factor:factor:factor] -c0_1(a836) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 515750 [binary:509573,515744,factor:factor] -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 515788 [binary:515227,515750,factor:factor:factor:factor] -c3_1(a841) | c2_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515803 [binary:515268,515788,factor:factor:factor:factor] c2_1(a841) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515805 [binary:509220,515803] -hskp9(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515826 [binary:515225,515805,factor:factor] -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515842 [binary:509506,515826,factor:factor:factor] -c0_1(a833) | c3_1(a833) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515846 [binary:509556,515826,factor:factor:factor:factor] -c0_1(a849) | c3_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 515878 [binary:509507,515842,factor:factor:factor:factor] c3_1(a833) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515880 [binary:509227,515878] -hskp5(0) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515886 [binary:509505,515880,factor:factor] -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515896 [binary:509596,515886] -c2_1(a831) | -c0_1(a831) | hskp29(0) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 515958 [binary:509560,515846,factor:factor:factor:factor:factor] c3_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515974 [binary:515886,515958,factor:factor] -c2_1(a849) | -c0_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515986 [binary:509556,515974,factor:factor:factor] -c0_1(a849) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515992 [binary:509560,515986,factor:factor] -c1_1(X) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 515998 [binary:509497,515992] -c0_1(a838) | c3_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516077 [binary:509597,515896,factor] -c0_1(a831) | hskp29(0) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 516081 [binary:514969,516077,factor:factor] hskp29(0) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 516083 [binary:509140,516081] c2_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 516088 [binary:509142,516081] c0_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 516095 [binary:515826,516083,factor:factor] -c0_1(a849) | c3_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 516105 [binary:516088,516095,factor:factor:factor:factor] c3_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 516111 [binary:515886,516105,factor] -c2_1(a849) | -c0_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 516115 [binary:516083,516111,factor:factor] -c0_1(a849) | -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 516119 [binary:516088,516115,factor:factor] -c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 516124 [binary:509497,516119] c2_1(a838) | c0_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516186 [binary:509221,516124] -hskp8(0) | c0_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516256 [binary:509496,516186,factor] c0_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516291 [binary:515998,516256,factor:factor:factor:factor] c3_1(a838) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516331 [binary:509222,516291] -hskp8(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516342 [binary:509496,516331,factor] hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516344 [binary:509128,516342] c1_1(a866) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516347 [binary:509129,516342] c0_1(a866) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516362 [binary:515992,516344,factor:factor:factor] -c0_1(a866) | c3_1(a866) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516373 [binary:516347,516362,factor:factor:factor:factor] c3_1(a866) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516376 [binary:509198,516373] -hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516380 [binary:516342,516376,factor:factor] -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 516401 [binary:509571,516380,factor:factor] -c0_1(a836) | c1_1(a836) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 516407 [binary:512340,516380,factor:factor] -c0_1(a830) | c1_1(a830) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516439 [binary:509626,516407,factor:factor] c1_1(a830) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516442 [binary:509232,516439] -hskp2(0) | hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516452 [binary:509625,516442,factor] hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516454 [binary:509111,516452] c1_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516456 [binary:509112,516452] c0_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516466 [binary:515992,516454,factor:factor] -c0_1(a841) | c3_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516475 [binary:516456,516466,factor:factor] c3_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516504 [binary:509573,516401,factor:factor:factor:factor] c1_1(a836) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 516507 [binary:509223,516504] -hskp7(0) | -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 516522 [binary:509570,516507,factor:factor] -c1_1(X) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 516542 [binary:516454,516522,factor:factor] -c3_1(a841) | c2_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516550 [binary:516475,516542,factor:factor] c2_1(a841) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516552 [binary:509220,516550] -hskp9(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516558 [binary:516452,516552,factor] c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 516563 [binary:509228,516558,binarycut:509230,binarycut:509229] -hskp4(0) | c0_1(a832).
% 516573 [binary:509453,516563] c0_1(a832) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X).
% 516579 [binary:509587,516563] c0_1(a832) | hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516581 [binary:509628,516563] c0_1(a832) | hskp11(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 516583 [binary:509635,516563] c0_1(a832) | hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 516627 [binary:512319,516579] c1_1(a832) | c3_1(a832) | c2_1(a832) | hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516629 [binary:512319,516581] c1_1(a832) | c3_1(a832) | c2_1(a832) | hskp11(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 516632 [binary:512319,516583] c1_1(a832) | c3_1(a832) | c2_1(a832) | hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 516696 [binary:512319,516573] c1_1(a832) | c3_1(a832) | c2_1(a832) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X).
% 516778 [binary:509228,516627,binarycut:509230,binarycut:509229] -hskp4(0) | hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516784 [binary:509587,516778,factor] hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516786 [binary:509121,516784] c0_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516795 [binary:512319,516786] c1_1(a859) | c3_1(a859) | c2_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516806 [binary:509205,516795,binarycut:509206] -hskp17(0) | c2_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516810 [binary:516784,516806,factor] c2_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 516815 [binary:509228,516629,binarycut:509230,binarycut:509229] -hskp4(0) | hskp11(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 516822 [binary:509628,516815,factor] hskp11(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 516824 [binary:509114,516822] c3_1(a844) | c3_1(X) | c2_1(X) | c0_1(X).
% 516837 [binary:509228,516632,binarycut:509230,binarycut:509229] -hskp4(0) | hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 516846 [binary:509635,516837,factor] hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 516848 [binary:509106,516846] c2_1(a833) | c1_1(X) | c2_1(X) | c0_1(X).
% 516850 [binary:509107,516846] c0_1(a833) | c1_1(X) | c2_1(X) | c0_1(X).
% 516965 [binary:509228,516696,binarycut:509230,binarycut:509229] -hskp4(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X).
% 516971 [binary:509453,516965,factor:factor] -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X).
% 516980 [binary:509530,516971,factor:factor] c2_1(a846) | c0_1(a846) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X).
% 517054 [binary:509213,516980,binarycut:509212] -hskp13(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X).
% 517058 [binary:509529,517054,factor:factor] -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X).
% 517094 [binary:516824,517058] c1_1(a844) | c2_1(a844) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 517230 [binary:509216,517094,binarycut:509217] -hskp11(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 517235 [binary:516822,517230,factor] -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 517265 [binary:516810,517235,factor:factor] -c0_1(a859) | c1_1(a859) | c3_1(a859) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 517275 [binary:516786,517265,factor:factor] c1_1(a859) | c3_1(a859) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 517278 [binary:509205,517275,binarycut:509206] -hskp17(0) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 517288 [binary:516784,517278,factor] -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 517309 [binary:516558,517288] c3_1(X) | c2_1(X) | c0_1(X).
% 517316 [binary:509226,517309,binarycut:509225,binarycut:509224] -hskp6(0).
% 517353 [binary:516971,517309] -c2_1(X) | -c0_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 517355 [binary:509471,517316] hskp16(0) | -c2_1(X) | -c0_1(X) | c3_1(X).
% 517356 [binary:509594,517316] -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 517465 [binary:516848,517353,factor] -c0_1(a833) | c3_1(a833) | c1_1(X) | c2_1(X) | c0_1(X).
% 517496 [binary:516850,517465,factor] c3_1(a833) | c1_1(X) | c2_1(X) | c0_1(X).
% 517498 [binary:509227,517496] -hskp5(0) | c1_1(X) | c2_1(X) | c0_1(X).
% 517505 [binary:516846,517498,factor] c1_1(X) | c2_1(X) | c0_1(X).
% 517509 [binary:509208,517505,binarycut:509209,binarycut:509207] -hskp16(0).
% 517520 [binary:517355,517509] -c2_1(X) | -c0_1(X) | c3_1(X).
% 517531 [binary:509392,517520] -c0_1(a851) | c3_1(a851) | hskp21(0).
% 517536 [binary:509488,517520,cut:517509] -c0_1(a833) | c3_1(a833) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 517567 [binary:516810,517520] -c0_1(a859) | c3_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 517609 [binary:509489,517536,cut:517509,factor] c3_1(a833) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 517611 [binary:509227,517609] -hskp5(0) | -c3_1(X) | -c2_1(X) | c1_1(X).
% 517619 [binary:509487,517611,cut:517509,factor] -c3_1(X) | -c2_1(X) | c1_1(X).
% 517674 [binary:516786,517567,factor:factor] c3_1(a859) | -c1_1(X) | c3_1(X) | c0_1(X).
% 517676 [binary:509206,517674] -hskp17(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 517685 [binary:516784,517676,factor] -c1_1(X) | c3_1(X) | c0_1(X).
% 517687 [binary:509393,517685] c3_1(a851) | c0_1(a851) | hskp21(0).
% 517703 [binary:509211,517687,binarycut:509187] c0_1(a851) | hskp21(0).
% 517705 [binary:517531,517703] c3_1(a851) | hskp21(0).
% 517708 [binary:509211,517705,binarycut:509187] hskp21(0).
% 517709 [binary:509127,517708] c2_1(a865).
% 517710 [binary:517520,517709] -c0_1(a865) | c3_1(a865).
% 517723 [binary:509434,517356,cut:517509] c1_1(a830) | c2_1(a830) | hskp17(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 518036 [binary:509232,517723,binarycut:509233] -hskp2(0) | hskp17(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 518038 [binary:509150,518036,cut:517509] hskp17(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 518040 [binary:509121,518038] c0_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518063 [binary:517356,518040,factor:factor] c1_1(a859) | c2_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518065 [binary:509205,518063] -hskp17(0) | c2_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518068 [binary:518038,518065,factor] c2_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518070 [binary:517520,518068] -c0_1(a859) | c3_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518078 [binary:518040,518070,factor:factor] c3_1(a859) | c1_1(X) | c3_1(X) | c0_1(X).
% 518080 [binary:509206,518078] -hskp17(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 518088 [binary:518038,518080,factor] c1_1(X) | c3_1(X) | c0_1(X).
% 518093 [binary:509200,518088,cut:517708,binarycut:517710] c3_1(a865).
% 518101 [binary:517619,518093,cut:517709] c1_1(a865).
% 518107 [binary:509200,518101,cut:517708] 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
% 
% 
% old unit clauses discarded
% 
% ***GANDALF_FOUND_A_REFUTATION***
% 
% Global statistics over all passes: 
% 
%  given clauses:    23133
%  derived clauses:   1457759
%  kept clauses:      274592
%  kept size sum:     0
%  kept mid-nuclei:   126167
%  kept new demods:   0
%  forw unit-subs:    19
%  forw double-subs: 204604
%  forw overdouble-subs: 685851
%  backward subs:     5094
%  fast unit cutoff:  13564
%  full unit cutoff:  0
%  dbl  unit cutoff:  23897
%  real runtime:  257.90
%  process. runtime:  256.83
% specific non-discr-tree subsumption statistics: 
%  tried:           95846764
%  length fails:    724210
%  strength fails:  32681107
%  predlist fails:  50877629
%  aux str. fails:  939572
%  by-lit fails:    7940368
%  full subs tried: 1176458
%  full subs fail:  1108045
% 
% ; 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/SYN512-1+noeq.in")
% 
%------------------------------------------------------------------------------