%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SYN500-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 : art01.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 259.2s
% Output : Assurance 259.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/SYN500-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(200,40,1,400,0,1,150117,4,2275,172900,5,3002,172900,1,3002,172900,50,3002,172900,40,3002,173100,0,3002,173328,50,3003,173528,0,3005,173756,50,3006,173956,0,3006,174184,50,3006,174384,0,3008,174612,50,3009,174812,0,3010,175040,50,3011,175240,0,3011,175468,50,3012,175668,0,3013,175896,50,3014,176096,0,3015,176324,50,3016,176524,0,3016,176752,50,3017,176952,0,3018,177180,50,3019,177380,0,3021,177608,50,3021,177808,0,3021,178036,50,3022,178236,0,3024,178464,50,3024,178664,0,3026,178892,50,3027,179092,0,3027,179320,50,3027,179520,0,3029,179748,50,3030,179948,0,3031,180176,50,3032,180376,0,3032,180604,50,3033,180804,0,3034,181032,50,3035,181232,0,3037,181460,50,3037,181660,0,3038,181888,50,3038,181888,40,3038,182088,0,3040,200165,3,3941,201255,4,4391,203049,1,4841,203049,50,4841,203049,40,4841,203249,0,4841,298418,3,9343,299318,4,11592,302535,1,13842,302535,50,13845,302535,40,13845,302735,0,13845,362137,3,15872,362314,4,16096,363417,5,16846,363418,1,16846,363418,50,16848,363418,40,16848,363618,0,16848,434319,3,19565,435000,4,20899,435760,1,22249,435760,50,22251,435760,40,22251,435960,0,22251,495523,3,24317,495664,4,24502,496776,5,25252,496777,1,25252,496777,50,25254,496777,40,25254,496977,0,25254,497191,50,25255,497191,40,25255,497391,0,25260)
%
%
% START OF PROOF
% 497192 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Z) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | -c0_1(X) | c1_1(Y) | c1_1(Z).
% 497193 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Z) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c2_1(X).
% 497194 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Y).
% 497195 [] -ndr1_0(0) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c2_1(Z).
% 497196 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Y) | -c3_1(Z) | -c2_1(Z) | -c2_1(X) | c1_1(Z) | c3_1(X) | c0_1(Y).
% 497200 [] -ndr1_0(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c2_1(Z) | c2_1(X).
% 497201 [] -ndr1_0(0) | -c1_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | -c0_1(X) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Y).
% 497202 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(Z) | c2_1(X) | c0_1(Z) | c0_1(Y).
% 497205 [] -ndr1_0(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c2_1(Z) | c1_1(X) | c1_1(Z) | c3_1(Z) | c0_1(X) | c0_1(Y).
% 497206 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Y) | c1_1(Z) | c1_1(Y) | c2_1(X) | c0_1(Z) | c0_1(X).
% 497207 [] -ndr1_0(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(Y) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 497209 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c0_1(Z) | c1_1(Z) | c3_1(Y) | c3_1(Z) | c3_1(X) | c2_1(X) | c0_1(Y).
% 497210 [?] ?
% 497211 [?] ?
% 497212 [?] ?
% 497214 [?] ?
% 497215 [?] ?
% 497217 [?] ?
% 497223 [?] ?
% 497224 [?] ?
% 497226 [?] ?
% 497228 [?] ?
% 497229 [?] ?
% 497230 [?] ?
% 497232 [?] ?
% 497234 [?] ?
% 497235 [?] ?
% 497238 [?] ?
% 497239 [?] ?
% 497243 [?] ?
% 497244 [?] ?
% 497246 [?] ?
% 497247 [?] ?
% 497249 [?] ?
% 497253 [?] ?
% 497256 [?] ?
% 497259 [?] ?
% 497260 [?] ?
% 497262 [?] ?
% 497263 [?] ?
% 497264 [] -hskp0(0) | c3_1(a1).
% 497265 [] -hskp0(0) | c1_1(a1).
% 497266 [] -hskp1(0) | c0_1(a2).
% 497268 [] -hskp3(0) | c2_1(a5).
% 497269 [] -hskp5(0) | c1_1(a8).
% 497274 [] -hskp11(0) | c2_1(a19).
% 497275 [] -hskp11(0) | c1_1(a19).
% 497276 [] -hskp13(0) | c3_1(a22).
% 497277 [] -hskp14(0) | c1_1(a25).
% 497278 [] -hskp14(0) | c0_1(a25).
% 497279 [] -hskp15(0) | c3_1(a28).
% 497280 [] -hskp15(0) | c2_1(a28).
% 497283 [] -hskp17(0) | c0_1(a33).
% 497284 [] -hskp18(0) | c3_1(a39).
% 497285 [] -hskp18(0) | c0_1(a39).
% 497286 [] -hskp19(0) | c2_1(a40).
% 497287 [] -hskp20(0) | c1_1(a43).
% 497288 [] -hskp20(0) | c0_1(a43).
% 497289 [] -hskp21(0) | c3_1(a47).
% 497290 [] -hskp21(0) | c2_1(a47).
% 497291 [] -hskp22(0) | c1_1(a48).
% 497293 [] -hskp24(0) | c3_1(a64).
% 497294 [] -hskp24(0) | c1_1(a64).
% 497295 [] -hskp25(0) | c2_1(a73).
% 497296 [] -hskp25(0) | c0_1(a73).
% 497297 [] -hskp26(0) | c3_1(a4).
% 497298 [] -hskp26(0) | c1_1(a4).
% 497299 [] -hskp26(0) | c0_1(a4).
% 497300 [] -hskp27(0) | c3_1(a13).
% 497301 [] -hskp27(0) | c2_1(a13).
% 497302 [] -hskp27(0) | c1_1(a13).
% 497303 [] -hskp28(0) | c2_1(a23).
% 497304 [] -hskp28(0) | c1_1(a23).
% 497305 [] -hskp28(0) | c0_1(a23).
% 497309 [] hskp11(0) | hskp12(0) | hskp21(0).
% 497310 [] hskp0(0) | hskp11(0) | hskp22(0).
% 497311 [] hskp17(0) | hskp19(0) | hskp22(0).
% 497315 [] hskp12(0) | hskp14(0) | hskp20(0).
% 497325 [] -hskp9(0) | ndr1_0(0).
% 497343 [] -hskp27(0) | ndr1_0(0).
% 497346 [] hskp9(0) | hskp27(0).
% 497347 [] -c3_1(a73) | -hskp25(0).
% 497348 [] -c0_1(a64) | -hskp24(0).
% 497351 [] -c0_1(a48) | -hskp22(0).
% 497352 [] -c3_1(a48) | -hskp22(0).
% 497353 [] -c0_1(a47) | -hskp21(0).
% 497354 [] -c3_1(a43) | -hskp20(0).
% 497355 [] -c0_1(a40) | -hskp19(0).
% 497356 [] -c3_1(a40) | -hskp19(0).
% 497357 [] -c1_1(a39) | -hskp18(0).
% 497358 [] -c1_1(a33) | -hskp17(0).
% 497359 [] -c3_1(a33) | -hskp17(0).
% 497361 [] -c1_1(a28) | -hskp15(0).
% 497362 [] -c2_1(a25) | -hskp14(0).
% 497363 [] -c0_1(a22) | -hskp13(0).
% 497364 [] -c1_1(a22) | -hskp13(0).
% 497365 [] -c0_1(a20) | -hskp12(0).
% 497366 [] -c2_1(a20) | -hskp12(0).
% 497367 [] -c3_1(a20) | -hskp12(0).
% 497368 [] -c0_1(a19) | -hskp11(0).
% 497369 [] -c1_1(a18) | -hskp10(0).
% 497370 [] -c2_1(a18) | -hskp10(0).
% 497371 [] -c3_1(a18) | -hskp10(0).
% 497372 [] -c0_1(a15) | -hskp9(0).
% 497373 [] -c1_1(a15) | -hskp9(0).
% 497374 [] -c2_1(a15) | -hskp9(0).
% 497380 [] -c2_1(a8) | -hskp5(0).
% 497381 [] -c3_1(a8) | -hskp5(0).
% 497382 [] -c0_1(a7) | -hskp4(0).
% 497383 [] -c1_1(a7) | -hskp4(0).
% 497384 [] -c3_1(a7) | -hskp4(0).
% 497385 [] -c0_1(a5) | -hskp3(0).
% 497386 [] -c1_1(a5) | -hskp3(0).
% 497389 [] -c1_1(a2) | -hskp1(0).
% 497390 [] -c2_1(a2) | -hskp1(0).
% 497391 [] -c2_1(a1) | -hskp0(0).
% 497546 [binary:497325,497346,binarycut:497343] ndr1_0(0).
% 497547 [binary:497192,497546] -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Z) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Y) | c1_1(Z).
% 497548 [binary:497193,497546] -c1_1(X) | -c3_1(Y) | -c2_1(Z) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c2_1(X).
% 497549 [binary:497194,497546] -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c2_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Y).
% 497550 [binary:497195,497546] -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Y) | c1_1(Z) | c2_1(Z).
% 497551 [binary:497196,497546] -c1_1(X) | -c1_1(Y) | -c3_1(X) | -c3_1(Z) | -c2_1(Z) | -c2_1(Y) | c1_1(Z) | c3_1(Y) | c0_1(X).
% 497555 [binary:497200,497546] -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c2_1(Z) | c2_1(X).
% 497556 [binary:497201,497546] -c1_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(Y).
% 497557 [binary:497202,497546] -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Z) | -c0_1(X) | c1_1(Y) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 497560 [binary:497205,497546] -c3_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Z) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c0_1(Y) | c0_1(X).
% 497561 [binary:497206,497546] -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Z) | c1_1(Y) | c1_1(Z) | c2_1(X) | c0_1(Y) | c0_1(X).
% 497562 [binary:497207,497546] -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Z) | c1_1(Y) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 497564 [binary:497209,497546] -c1_1(X) | -c1_1(Y) | -c0_1(Z) | c1_1(Z) | c3_1(Y) | c3_1(X) | c3_1(Z) | c2_1(Y) | c0_1(X).
% 497566 [binary:497274,497309] c2_1(a19) | hskp12(0) | hskp21(0).
% 497567 [binary:497275,497309] c1_1(a19) | hskp12(0) | hskp21(0).
% 497569 [binary:497264,497310] c3_1(a1) | hskp11(0) | hskp22(0).
% 497570 [binary:497265,497310] c1_1(a1) | hskp11(0) | hskp22(0).
% 497572 [binary:497283,497311] c0_1(a33) | hskp19(0) | hskp22(0).
% 497573 [input:497210,cut:497546] -c1_1(X) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(Z).
% 497582 [input:497211,cut:497546] -c3_1(X) | -c2_1(Y) | -c0_1(Z) | c1_1(Y) | c1_1(X) | c3_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(X).
% 497589 [input:497212,cut:497546] -c2_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c3_1(Y) | c2_1(Y) | c0_1(Z) | c0_1(X).
% 497596 [input:497239,cut:497546] hskp25(0) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 497597 [binary:497295,497596] c2_1(a73) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 497598 [binary:497296,497596] c0_1(a73) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 497600 [input:497214,cut:497546] -c1_1(X) | c1_1(Y) | c1_1(Z) | c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c2_1(Z) | c0_1(Z).
% 497603 [input:497259,cut:497546] hskp19(0) | -c1_1(X) | c3_1(X) | c2_1(X).
% 497604 [binary:497286,497603] c2_1(a40) | -c1_1(X) | c3_1(X) | c2_1(X).
% 497613 [input:497215,cut:497546] hskp13(0) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c3_1(Y) | c2_1(Y).
% 497614 [binary:497276,497613] c3_1(a22) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y).
% 497634 [input:497243,cut:497546] hskp11(0) | hskp21(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497635 [binary:497274,497634] c2_1(a19) | hskp21(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497636 [binary:497275,497634] c1_1(a19) | hskp21(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497638 [input:497217,cut:497546] hskp12(0) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(X).
% 497645 [input:497244,cut:497546] hskp18(0) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497646 [binary:497284,497645] c3_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497647 [binary:497285,497645] c0_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497659 [input:497246,cut:497546] hskp10(0) | hskp13(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 497660 [input:497247,cut:497546] hskp5(0) | hskp17(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 497661 [binary:497269,497660] c1_1(a8) | hskp17(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 497670 [binary:497600,497661] c3_1(a8) | c2_1(a8) | hskp17(0) | -c1_1(X) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(Y) | c0_1(X).
% 497684 [input:497249,cut:497546] hskp22(0) | hskp24(0) | -c0_1(X) | c3_1(X) | c2_1(X).
% 497685 [binary:497291,497684] c1_1(a48) | hskp24(0) | -c0_1(X) | c3_1(X) | c2_1(X).
% 497713 [input:497223,cut:497546] hskp20(0) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 497714 [binary:497287,497713] c1_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 497715 [binary:497288,497713] c0_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 497719 [input:497253,cut:497546] hskp13(0) | hskp15(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 497720 [binary:497276,497719] c3_1(a22) | hskp15(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 497721 [binary:497276,497719,factor] -c2_1(a22) | c3_1(a22) | c0_1(a22) | hskp15(0).
% 497728 [input:497224,cut:497546] hskp22(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 497729 [binary:497291,497728] c1_1(a48) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 497748 [input:497256,cut:497546] hskp1(0) | hskp10(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 497749 [binary:497266,497748] c0_1(a2) | hskp10(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 497753 [input:497226,cut:497546] hskp15(0) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 497754 [binary:497279,497753] c3_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 497756 [binary:497280,497753] c2_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 497774 [input:497228,cut:497546] hskp14(0) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 497775 [binary:497277,497774] c1_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 497776 [binary:497278,497774] c0_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 497778 [input:497260,cut:497546] hskp11(0) | hskp12(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 497779 [binary:497274,497778] c2_1(a19) | hskp12(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 497781 [binary:497275,497778] c1_1(a19) | hskp12(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 497783 [input:497229,cut:497546] hskp3(0) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 497784 [binary:497268,497783] c2_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 497798 [input:497230,cut:497546] hskp28(0) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 497799 [binary:497303,497798] c2_1(a23) | -c3_1(X) | -c3_1(Y) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 497801 [binary:497304,497798] c1_1(a23) | -c3_1(X) | -c3_1(Y) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 497802 [binary:497305,497798] c0_1(a23) | -c3_1(X) | -c3_1(Y) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 497810 [input:497262,cut:497546] hskp1(0) | hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 497811 [binary:497266,497810] c0_1(a2) | hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 497818 [input:497263,cut:497546] hskp3(0) | hskp26(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 497819 [binary:497268,497818] c2_1(a5) | hskp26(0) | c1_1(X) | c3_1(X) | c0_1(X).
% 497823 [binary:497589,497819,factor:factor:factor] c1_1(a5) | c0_1(a5) | hskp26(0) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 497828 [input:497232,cut:497546] hskp5(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 497829 [binary:497269,497828] c1_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 497843 [input:497234,cut:497546] hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y).
% 497844 [binary:497287,497843] c1_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 497846 [binary:497287,497843,factor:factor] c1_1(a43) | c3_1(a43) | c2_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 497847 [binary:497288,497843] c0_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 497854 [input:497235,cut:497546] hskp4(0) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 497868 [binary:497582,497614,factor] c1_1(a22) | c0_1(a22) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Y) | c3_1(Z) | c3_1(Y) | c2_1(Z).
% 497890 [input:497238,cut:497546] hskp0(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 497891 [binary:497264,497890] c3_1(a1) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 497893 [binary:497265,497890] c1_1(a1) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 498034 [binary:497775,497549] -c3_1(a25) | -c0_1(a25) | -c1_1(X) | -c3_1(Y) | -c2_1(U) | -c2_1(Z) | -c0_1(U) | -c0_1(Y) | c1_1(Z) | c3_1(X) | c3_1(U) | c3_1(Z) | c2_1(Y) | c0_1(X).
% 498061 [binary:497646,497550,factor:factor:factor:factor] -c2_1(a39) | -c0_1(a39) | c1_1(a39) | hskp19(0) | -c0_1(X) | c1_1(X) | c2_1(X).
% 498110 [binary:497600,497829,factor] c3_1(a8) | c2_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 498123 [binary:497573,497844,factor:factor:factor:factor:factor:factor:factor:factor] -c2_1(a43) | c3_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 498129 [binary:497547,497844,factor:factor:factor:factor:factor] -c2_1(a43) | -c0_1(a43) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y).
% 498136 [binary:497548,497844,factor:factor:factor:factor:factor:factor:factor] -c0_1(a43) | c2_1(a43) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y).
% 498143 [binary:497570,497551] -c3_1(a1) | c0_1(a1) | hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X).
% 498356 [binary:497646,497555,factor:factor] -c0_1(a39) | c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c2_1(Y).
% 498427 [binary:497714,497556,factor:factor:factor:factor:factor:factor:factor] -c2_1(a43) | -c0_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 498447 [binary:497570,497557] -c0_1(a1) | c2_1(a1) | hskp11(0) | hskp22(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 498472 [binary:497829,497557,factor:factor] -c0_1(a8) | c2_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 498646 [binary:497570,497561] c2_1(a1) | c0_1(a1) | hskp11(0) | hskp22(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 498662 [binary:497729,497561,factor:factor:factor] c2_1(a48) | c0_1(a48) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 498666 [binary:497829,497561,factor:factor:factor:factor:factor] c2_1(a8) | c0_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 498688 [binary:497570,497562] -c3_1(a1) | c2_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c2_1(Y) | c0_1(Y).
% 498711 [binary:497893,497562,factor:factor:factor] -c3_1(a1) | c2_1(a1) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(X) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 498823 [binary:497847,498136,factor:factor:factor:factor] c2_1(a43) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y).
% 498829 [binary:498129,498823,factor:factor:factor:factor:factor] -c0_1(a43) | -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 498836 [binary:497847,498829,factor:factor:factor] -c3_1(X) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 498858 [binary:497754,498836,factor:factor] -c2_1(a28) | -c0_1(a28) | c1_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 498950 [binary:497380,498666] -hskp5(0) | c0_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 498975 [binary:497828,498950,factor:factor:factor:factor:factor] c0_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 498983 [binary:498472,498975,factor:factor] c2_1(a8) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 498987 [binary:497380,498983] -hskp5(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 498993 [binary:497828,498987,factor:factor] -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 498996 [binary:497570,498993] -c2_1(a1) | c0_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 499007 [binary:497729,498993,factor:factor] -c2_1(a48) | c0_1(a48) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 499072 [binary:498662,499007,factor:factor:factor:factor] c0_1(a48) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 499075 [binary:497351,499072] -hskp22(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 499089 [binary:497728,499075,factor:factor] -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 499109 [binary:497754,499089,factor:factor] -c2_1(a28) | c1_1(a28) | c0_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 499145 [binary:497386,497823,binarycut:497385] -hskp3(0) | hskp26(0) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 499161 [binary:497818,499145,factor] hskp26(0) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 499163 [binary:497297,499161] c3_1(a4) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 499166 [binary:497298,499161] c1_1(a4) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 499168 [binary:497299,499161] c0_1(a4) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 499172 [binary:497381,497670,binarycut:497380] -hskp5(0) | hskp17(0) | -c1_1(X) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Y).
% 499273 [binary:497647,498356,factor] c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c2_1(Y).
% 499280 [binary:498061,499273,factor:factor:factor:factor:factor:factor:factor:factor] -c0_1(a39) | c1_1(a39) | c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 499298 [binary:497647,499280,factor:factor] c1_1(a39) | c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 499300 [binary:497357,499298] -hskp18(0) | c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 499318 [binary:497645,499300,factor] c2_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 499738 [binary:497364,497868,binarycut:497363] -hskp13(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(Z) | c2_1(Z).
% 499748 [binary:497613,499738,factor:factor] -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Y) | c3_1(Z) | c3_1(Y) | c2_1(Z).
% 499792 [binary:499166,499748,factor:factor:factor:factor] -c3_1(a4) | -c0_1(a4) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 499798 [binary:499163,499792,factor:factor:factor:factor] -c0_1(a4) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 499803 [binary:499168,499798,factor:factor] -c2_1(X) | -c0_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 499806 [binary:497604,499803] c1_1(a40) | c3_1(a40) | c0_1(a40) | -c1_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 499807 [binary:497604,499803,factor:factor] c1_1(a40) | c3_1(a40) | c0_1(a40) | -c1_1(X) | -c0_1(X) | c3_1(X) | c2_1(X).
% 499812 [binary:497784,499803,factor:factor] c1_1(a5) | c3_1(a5) | c0_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 499848 [binary:497564,499807,factor:factor] c3_1(a40) | c0_1(a40) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X).
% 499858 [binary:497356,499848,binarycut:497355] -hskp19(0) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X).
% 499870 [binary:497603,499858,factor] -c1_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X).
% 499903 [binary:497846,499870,factor:factor:factor] -c0_1(a43) | c3_1(a43) | c2_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 499912 [binary:497775,499870,factor:factor:factor:factor] -c0_1(a25) | c3_1(a25) | c2_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 499919 [binary:497847,499903,factor:factor:factor] c3_1(a43) | c2_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 499925 [binary:497354,499919] -hskp20(0) | c2_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y).
% 499940 [binary:497843,499925,factor:factor:factor:factor] c2_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y).
% 499952 [binary:498123,499940,factor:factor:factor:factor:factor:factor:factor] c3_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 499961 [binary:497354,499952] -hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 499997 [binary:497843,499961,factor:factor:factor] -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 500032 [binary:497564,499806,factor:factor:factor:factor:factor:factor] c3_1(a40) | c0_1(a40) | -c1_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X).
% 500038 [binary:497356,500032,binarycut:497355] -hskp19(0) | -c1_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y).
% 500048 [binary:497603,500038,factor] -c1_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y).
% 500054 [binary:497685,500048,factor:factor:factor] c3_1(a48) | c2_1(a48) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500061 [binary:497714,500048,factor:factor:factor:factor] c3_1(a43) | c2_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y).
% 500071 [binary:497352,500054] -hskp22(0) | c2_1(a48) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500084 [binary:497684,500071,factor:factor] c2_1(a48) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500147 [binary:497354,500061] -hskp20(0) | c2_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 500180 [binary:497713,500147,factor:factor:factor:factor] c2_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y).
% 500190 [binary:498427,500180,factor:factor:factor:factor] -c0_1(a43) | -c1_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X).
% 500196 [binary:497715,500190,factor:factor] -c1_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500204 [binary:497685,500196,factor:factor] -c2_1(a48) | c3_1(a48) | c0_1(a48) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500238 [binary:500084,500204,factor:factor] c3_1(a48) | c0_1(a48) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500247 [binary:497352,500238,binarycut:497351] -hskp22(0) | hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500252 [binary:497684,500247,factor] hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500254 [binary:497293,500252] c3_1(a64) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500256 [binary:497294,500252] c1_1(a64) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 500314 [binary:497660,499172,factor] hskp17(0) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Y).
% 500393 [binary:497283,500314] c0_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Y) | c2_1(Z) | c2_1(Y) | c0_1(Z) | c0_1(X).
% 500799 [binary:497756,498858,factor:factor:factor:factor] -c0_1(a28) | c1_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500957 [binary:497756,499109,factor:factor:factor] c1_1(a28) | c0_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500959 [binary:497361,500957] -hskp15(0) | c0_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500966 [binary:497753,500959,factor:factor:factor] c0_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500972 [binary:500799,500966,factor:factor:factor:factor] c1_1(a28) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500974 [binary:497361,500972] -hskp15(0) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 500987 [binary:497753,500974,factor:factor] -c1_1(X) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 501030 [binary:500256,500987,factor] -c3_1(a64) | c0_1(a64) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 501041 [binary:500254,501030,factor] c0_1(a64) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 501052 [binary:497348,501041] -hskp24(0) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 501061 [binary:500252,501052,factor] -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 501063 [binary:497572,501061] c1_1(a33) | c3_1(a33) | c2_1(a33) | hskp19(0) | hskp22(0).
% 501067 [binary:497749,501061] c1_1(a2) | c3_1(a2) | c2_1(a2) | hskp10(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 501068 [binary:497811,501061] c1_1(a2) | c3_1(a2) | c2_1(a2) | hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 501076 [binary:500393,501061,factor:factor] c1_1(a33) | c3_1(a33) | c2_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 501080 [binary:497358,501063,binarycut:497359] -hskp17(0) | c2_1(a33) | hskp19(0) | hskp22(0).
% 501088 [binary:497311,501080] c2_1(a33) | hskp19(0) | hskp22(0).
% 501194 [binary:497389,501067,binarycut:497390] -hskp1(0) | c3_1(a2) | hskp10(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 501205 [binary:497748,501194,factor] c3_1(a2) | hskp10(0) | -c1_1(X) | c2_1(X) | c0_1(X).
% 501212 [binary:497389,501068,binarycut:497390] -hskp1(0) | c3_1(a2) | hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 501227 [binary:497810,501212,factor:factor] c3_1(a2) | hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 501372 [binary:497358,501076,binarycut:497359] -hskp17(0) | c2_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 501395 [binary:500314,501372,factor:factor:factor:factor:factor:factor] c2_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 501409 [binary:499997,501395,factor:factor:factor:factor:factor:factor:factor] -c0_1(a33) | c1_1(a33) | c3_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 501603 [binary:497386,499812,binarycut:497385] -hskp3(0) | c3_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 501609 [binary:497783,501603,factor:factor] c3_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 501626 [binary:497776,499912,factor:factor:factor:factor:factor] c3_1(a25) | c2_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 501646 [binary:501626,498034,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] -c3_1(a25) | -c0_1(a25) | c2_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c0_1(X).
% 501833 [binary:500393,501409,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c1_1(a33) | c3_1(a33) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 501837 [binary:497358,501833,binarycut:497359] -hskp17(0) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 501853 [binary:500314,501837,factor:factor:factor] -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 502042 [binary:501626,501646,factor:factor:factor:factor] -c0_1(a25) | c2_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 502046 [binary:497776,502042,factor:factor] c2_1(a25) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 502048 [binary:497362,502046] -hskp14(0) | -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 502074 [binary:497774,502048,factor:factor] -c1_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 502079 [binary:497636,502074,factor] c3_1(a19) | c0_1(a19) | hskp21(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502090 [binary:497729,502074,factor:factor:factor] c3_1(a48) | c0_1(a48) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 502108 [binary:497560,502079,factor:factor] -c2_1(a19) | c0_1(a19) | hskp21(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 502146 [binary:497352,502090,binarycut:497351] -hskp22(0) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y).
% 502157 [binary:497728,502146,factor:factor] -c3_1(X) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y).
% 502168 [binary:497646,502157,factor:factor:factor] -c2_1(a39) | c1_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502251 [binary:499318,502168,factor:factor] c1_1(a39) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502253 [binary:497357,502251] -hskp18(0) | hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502264 [binary:497645,502253,factor] hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502266 [binary:497286,502264] c2_1(a40) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 502434 [binary:497381,498110,binarycut:497380] -hskp5(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 502503 [binary:497828,502434,factor:factor] -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 502518 [binary:497781,502503,factor:factor] -c2_1(a19) | c0_1(a19) | hskp12(0) | -c3_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 503002 [binary:497569,498143] c0_1(a1) | hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X).
% 503023 [binary:497635,502108,factor] c0_1(a19) | hskp21(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 503025 [binary:497368,503023] -hskp11(0) | hskp21(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 503030 [binary:497634,503025,factor] hskp21(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 503032 [binary:497289,503030] c3_1(a47) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 503034 [binary:497290,503030] c2_1(a47) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 503045 [binary:497560,503032,factor:factor:factor:factor:factor:factor] -c2_1(a47) | c0_1(a47) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 503063 [binary:503034,503045,factor:factor:factor] c0_1(a47) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 503065 [binary:497353,503063] -hskp21(0) | -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c0_1(X).
% 503071 [binary:503030,503065,factor:factor] -c3_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c0_1(X).
% 503076 [binary:497720,503071] c1_1(a22) | c0_1(a22) | hskp15(0) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c3_1(Y) | c0_1(X).
% 503201 [binary:497779,502518,factor] c0_1(a19) | hskp12(0) | -c3_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 503203 [binary:497368,503201] -hskp11(0) | hskp12(0) | -c3_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 503210 [binary:497778,503203,factor] hskp12(0) | -c3_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 503299 [binary:497364,503076,binarycut:497363] -hskp13(0) | hskp15(0) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c3_1(X) | c3_1(Y) | c0_1(Y).
% 503307 [binary:497719,503299,factor:factor] hskp15(0) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 503310 [binary:497279,503307] c3_1(a28) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 503313 [binary:497280,503307] c2_1(a28) | -c2_1(Y) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c0_1(X).
% 503330 [binary:502157,503310,factor:factor:factor:factor:factor] -c2_1(a28) | c1_1(a28) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c0_1(Y).
% 503347 [binary:503313,503330,factor:factor:factor:factor:factor:factor] c1_1(a28) | -c2_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X) | c3_1(Y) | c0_1(Y).
% 503350 [binary:497361,503347] -hskp15(0) | -c2_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X) | c3_1(Y) | c0_1(Y).
% 503359 [binary:503307,503350,factor:factor:factor:factor] -c2_1(Y) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X) | c3_1(Y) | c0_1(Y).
% 503379 [binary:502266,503359,factor:factor] c3_1(a40) | c0_1(a40) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 503393 [binary:497356,503379,binarycut:497355] -hskp19(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 503408 [binary:502264,503393,factor] -c2_1(X) | -c0_1(X) | c1_1(X) | c3_1(X).
% 503411 [binary:497597,503408] -c0_1(a73) | c1_1(a73) | c3_1(a73) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 503425 [binary:501088,503408] -c0_1(a33) | c1_1(a33) | c3_1(a33) | hskp19(0) | hskp22(0).
% 503429 [binary:497572,503425] c1_1(a33) | c3_1(a33) | hskp19(0) | hskp22(0).
% 503435 [binary:497358,503429,binarycut:497359] -hskp17(0) | hskp19(0) | hskp22(0).
% 503440 [binary:497311,503435] hskp19(0) | hskp22(0).
% 503442 [binary:497286,503440] c2_1(a40) | hskp22(0).
% 503450 [binary:497598,503411,factor] c1_1(a73) | c3_1(a73) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 503455 [binary:497573,503450] -c2_1(a73) | c3_1(a73) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 503564 [binary:503002,498447,factor:factor:factor] c2_1(a1) | hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503566 [binary:497391,503564] -hskp0(0) | hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503573 [binary:497310,503566] hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503575 [binary:497274,503573] c2_1(a19) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503576 [binary:497275,503573] c1_1(a19) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503610 [binary:498993,503576,factor:factor:factor:factor] -c2_1(a19) | c0_1(a19) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503628 [binary:503575,503610,factor:factor:factor:factor] c0_1(a19) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503631 [binary:497368,503628] -hskp11(0) | hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503637 [binary:503573,503631,factor:factor] hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503639 [binary:497291,503637] c1_1(a48) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503679 [binary:497561,503639,factor:factor:factor:factor] c2_1(a48) | c0_1(a48) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503684 [binary:498993,503639,factor:factor:factor:factor] -c2_1(a48) | c0_1(a48) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503707 [binary:503679,503684,factor:factor:factor:factor] c0_1(a48) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503712 [binary:497351,503707] -hskp22(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | -c2_1(Y) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503736 [binary:503637,503712,factor:factor] -c1_1(X) | -c3_1(Y) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c0_1(Y).
% 503743 [binary:497801,503736,factor:factor:factor] -c2_1(a23) | c3_1(a23) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | c1_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 503745 [binary:503450,503736] -c2_1(a73) | c3_1(a73) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c0_1(Y).
% 503758 [binary:497799,503743,factor:factor:factor] c3_1(a23) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 503763 [binary:497597,503745,factor] c3_1(a73) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c0_1(Y).
% 503771 [binary:497347,503763] -hskp25(0) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c0_1(Y).
% 503774 [binary:497596,503771,factor] -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c0_1(Y).
% 503776 [binary:497570,503774] -c3_1(a1) | -c0_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 503783 [binary:497801,503774,factor:factor:factor:factor] -c3_1(a23) | -c0_1(a23) | -c3_1(X) | -c3_1(Y) | -c2_1(Y) | c1_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 503787 [binary:497569,503776] -c0_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 503794 [binary:503758,503783,factor:factor:factor] -c0_1(a23) | -c3_1(Y) | -c3_1(X) | -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 503799 [binary:497802,503794,factor:factor:factor] -c3_1(Y) | -c3_1(X) | -c2_1(Y) | c1_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 503825 [binary:501609,503799,factor:factor] -c2_1(a5) | c1_1(a5) | c0_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 503895 [binary:497784,503825,factor:factor:factor:factor] c1_1(a5) | c0_1(a5) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 503907 [binary:497386,503895,binarycut:497385] -hskp3(0) | -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 503923 [binary:497783,503907,factor:factor] -c1_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 504311 [binary:498996,498646,factor:factor:factor:factor] c0_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504343 [binary:503787,504311,factor] hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504345 [binary:497274,504343] c2_1(a19) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504346 [binary:497275,504343] c1_1(a19) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504367 [binary:498993,504346,factor:factor:factor] -c2_1(a19) | c0_1(a19) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504383 [binary:504345,504367,factor:factor] c0_1(a19) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504385 [binary:497368,504383] -hskp11(0) | hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504388 [binary:504343,504385,factor] hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504391 [binary:497291,504388] c1_1(a48) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504416 [binary:497561,504391,factor:factor:factor:factor] c2_1(a48) | c0_1(a48) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504422 [binary:498993,504391,factor:factor:factor] -c2_1(a48) | c0_1(a48) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504437 [binary:504416,504422,factor:factor] c0_1(a48) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504440 [binary:497351,504437] -hskp22(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504469 [binary:504388,504440,factor] -c3_1(X) | -c2_1(X) | c1_1(X) | c0_1(X).
% 504669 [binary:497569,498688] c2_1(a1) | hskp11(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 504671 [binary:497391,504669] -hskp0(0) | hskp11(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 504712 [binary:497310,504671] hskp11(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y).
% 504714 [binary:497274,504712] c2_1(a19) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c2_1(Y) | c0_1(Y).
% 504716 [binary:497275,504712] c1_1(a19) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c2_1(Y) | c0_1(Y).
% 504786 [binary:501853,504716,factor:factor:factor] -c2_1(a19) | c0_1(a19) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504829 [binary:504714,504786,factor:factor:factor:factor:factor] c0_1(a19) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504832 [binary:497368,504829] -hskp11(0) | hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504838 [binary:504712,504832,factor:factor] hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504840 [binary:497291,504838] c1_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504859 [binary:497600,504840,factor:factor:factor:factor:factor:factor:factor:factor] c3_1(a48) | c2_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504890 [binary:497562,504840,factor:factor:factor:factor:factor:factor] -c3_1(a48) | c2_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504897 [binary:501853,504840,factor:factor] -c2_1(a48) | c0_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504917 [binary:504859,504890,factor:factor:factor:factor] c2_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504931 [binary:504917,504897,factor:factor:factor:factor] c0_1(a48) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504933 [binary:497351,504931] -hskp22(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504944 [binary:504838,504933,factor:factor] -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 504972 [binary:501227,504944,factor] -c0_1(a2) | c1_1(a2) | hskp27(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 504985 [binary:497811,504972,factor] c1_1(a2) | hskp27(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 504987 [binary:497389,504985] -hskp1(0) | hskp27(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 504997 [binary:497810,504987,factor] hskp27(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 505000 [binary:497300,504997] c3_1(a13) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 505002 [binary:497301,504997] c2_1(a13) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 505004 [binary:497302,504997] c1_1(a13) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 505023 [binary:501853,505004,factor:factor] -c2_1(a13) | c0_1(a13) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 505027 [binary:505002,505023,factor:factor] c0_1(a13) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 506390 [binary:497891,498711,factor:factor:factor:factor:factor] c2_1(a1) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(X) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 506396 [binary:497391,506390] -hskp0(0) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c3_1(X) | c2_1(X) | c2_1(Z) | c0_1(Z).
% 506525 [binary:497890,506396,factor:factor:factor] -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Z) | c1_1(Y) | c3_1(X) | c2_1(Z) | c2_1(X) | c0_1(Z).
% 508497 [binary:497597,503455,factor] c3_1(a73) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 508499 [binary:497347,508497] -hskp25(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 508515 [binary:497596,508499,factor] -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c3_1(Z) | c2_1(Z) | c0_1(Z).
% 508558 [binary:505004,508515,factor:factor:factor] -c3_1(a13) | -c0_1(a13) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 508574 [binary:505000,508558,factor] -c0_1(a13) | -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 508577 [binary:505027,508574,factor:factor] -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 508587 [binary:503442,508577] c1_1(a40) | c3_1(a40) | hskp22(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508596 [binary:501853,508587,binarycut:503442,factor:factor:factor] c3_1(a40) | c0_1(a40) | hskp22(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508609 [binary:497356,508596,binarycut:503440] c0_1(a40) | hskp22(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508612 [binary:497355,508609,binarycut:503440] hskp22(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508614 [binary:497291,508612] c1_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508634 [binary:497600,508614,factor:factor:factor:factor:factor:factor] c3_1(a48) | c2_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508639 [binary:501853,508614,factor:factor] -c2_1(a48) | c0_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508641 [binary:497352,508634] -hskp22(0) | c2_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508646 [binary:508612,508641,factor:factor] c2_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508677 [binary:508639,508646,factor:factor] c0_1(a48) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508680 [binary:497351,508677] -hskp22(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508683 [binary:508612,508680,factor] c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 508686 [binary:497369,508683,binarycut:497371,binarycut:497370] -hskp10(0) | c0_1(a18).
% 508690 [binary:497383,508683,binarycut:497384,binarycut:497382] -hskp4(0) | c2_1(a7).
% 508702 [binary:497564,508683,factor] -c1_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(X).
% 508703 [binary:506525,508683] -c3_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(Y) | c0_1(Z).
% 508707 [binary:497659,508686] c0_1(a18) | hskp13(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 508712 [binary:497854,508690] c2_1(a7) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 508736 [binary:501061,508707] c1_1(a18) | c3_1(a18) | c2_1(a18) | hskp13(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 508776 [binary:508683,508702] -c0_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 508785 [binary:497369,508736,binarycut:497371,binarycut:497370] -hskp10(0) | hskp13(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 508797 [binary:497659,508785,factor] hskp13(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 508799 [binary:497276,508797] c3_1(a22) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 508808 [binary:504469,508799] -c2_1(a22) | c1_1(a22) | c0_1(a22) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 509050 [binary:501205,508703,factor] -c0_1(a2) | c1_1(a2) | hskp10(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 509475 [binary:497749,509050,factor] c1_1(a2) | hskp10(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 509477 [binary:497389,509475] -hskp1(0) | hskp10(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509494 [binary:497748,509477,factor] hskp10(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 509496 [binary:508686,509494] c0_1(a18) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 509520 [binary:508776,509496,factor:factor:factor] c1_1(a18) | c3_1(a18) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 509530 [binary:497369,509520,binarycut:497371] -hskp10(0) | -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 509545 [binary:509494,509530,factor:factor] -c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509566 [binary:508683,509545] c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(X).
% 509570 [binary:497364,509566,binarycut:497363] -hskp13(0) | c2_1(a22) | c3_1(X) | c2_1(X) | c0_1(X).
% 509572 [binary:497373,509566,binarycut:497374,binarycut:497372] -hskp9(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 509587 [binary:497346,509572] hskp27(0) | c3_1(X) | c2_1(X) | c0_1(X).
% 509589 [binary:497300,509587] c3_1(a13) | c3_1(X) | c2_1(X) | c0_1(X).
% 509591 [binary:497301,509587] c2_1(a13) | c3_1(X) | c2_1(X) | c0_1(X).
% 509593 [binary:497302,509587] c1_1(a13) | c3_1(X) | c2_1(X) | c0_1(X).
% 509604 [binary:508515,509593,factor] -c3_1(a13) | -c0_1(a13) | -c2_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 509621 [binary:508797,509570] c2_1(a22) | -c1_1(X) | -c2_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509695 [binary:508808,509621,factor:factor:factor] c1_1(a22) | c0_1(a22) | -c1_1(X) | -c2_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 509730 [binary:509589,509604,factor] -c0_1(a13) | -c2_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 509801 [binary:497364,509695,binarycut:497363] -hskp13(0) | -c1_1(X) | -c2_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509815 [binary:508797,509801,factor] -c1_1(X) | -c2_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 509879 [binary:509593,509815,factor:factor] -c2_1(a13) | c0_1(a13) | c3_1(X) | c2_1(X) | c0_1(X).
% 509885 [binary:509591,509879,factor:factor] c0_1(a13) | c3_1(X) | c2_1(X) | c0_1(X).
% 509891 [binary:509730,509885,factor:factor] -c2_1(X) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 509919 [binary:508712,509891,factor:factor:factor:factor:factor] c1_1(a7) | c3_1(a7) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 509962 [binary:497383,509919,binarycut:497384] -hskp4(0) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 509974 [binary:497854,509962,factor:factor] -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 509984 [binary:508683,509974] c3_1(X) | c2_1(X) | c0_1(X).
% 509989 [binary:497367,509984,binarycut:497366,binarycut:497365] -hskp12(0).
% 509991 [binary:497381,509984,binarycut:497380] -hskp5(0) | c0_1(a8).
% 510037 [binary:497315,509989] hskp14(0) | hskp20(0).
% 510038 [binary:497638,509989] -c1_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(X).
% 510040 [binary:503210,509989] -c3_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 510048 [binary:497660,509991] c0_1(a8) | hskp17(0) | -c1_1(X) | -c2_1(X) | c0_1(X).
% 510054 [binary:497277,510037] c1_1(a25) | hskp20(0).
% 510055 [binary:497278,510037] c0_1(a25) | hskp20(0).
% 510174 [binary:503450,510038] -c0_1(a73) | c3_1(a73) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Y).
% 510191 [binary:510054,510038,binarycut:510055] c3_1(a25) | hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 510353 [binary:509984,510040] c1_1(Y) | c1_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 510357 [binary:497364,510353,binarycut:497363] -hskp13(0) | c2_1(a22) | c1_1(X) | c3_1(X) | c2_1(X).
% 510410 [binary:508797,510357] c2_1(a22) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 510501 [binary:508808,510410,factor:factor:factor] c1_1(a22) | c0_1(a22) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 511141 [binary:497598,510174,factor] c3_1(a73) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Y).
% 511144 [binary:497347,511141] -hskp25(0) | -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Y).
% 511170 [binary:497596,511144,factor] -c1_1(X) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Y) | c1_1(Y).
% 511198 [binary:510054,511170,binarycut:510055] -c3_1(a25) | hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511213 [binary:510191,511198,factor] hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511215 [binary:497287,511213] c1_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511217 [binary:497288,511213] c0_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511238 [binary:510038,511215,factor:factor] -c0_1(a43) | c3_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511256 [binary:511217,511238,factor] c3_1(a43) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511258 [binary:497354,511256] -hskp20(0) | -c2_1(X) | -c0_1(X) | c1_1(X).
% 511280 [binary:511213,511258,factor] -c2_1(X) | -c0_1(X) | c1_1(X).
% 511401 [binary:497364,510501,binarycut:497363] -hskp13(0) | -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 511421 [binary:508797,511401,factor] -c1_1(X) | -c2_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 511435 [binary:497781,511421,cut:509989,factor] -c2_1(a19) | c0_1(a19) | c1_1(X) | c3_1(X) | c2_1(X).
% 511488 [binary:497779,511435,cut:509989,factor] c0_1(a19) | c1_1(X) | c3_1(X) | c2_1(X).
% 511490 [binary:497368,511488] -hskp11(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 511542 [binary:497778,511490,cut:509989,factor] c1_1(X) | c3_1(X) | c2_1(X).
% 511545 [binary:497358,511542,binarycut:497359] -hskp17(0) | c2_1(a33).
% 511557 [binary:503923,511542] -c3_1(X) | -c0_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 511595 [binary:509984,511557] -c0_1(X) | c3_1(X) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 511601 [binary:510048,511595] c3_1(a8) | c2_1(a8) | hskp17(0) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 511803 [binary:497381,511601,binarycut:497380] -hskp5(0) | hskp17(0) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 511816 [binary:497660,511803,factor] hskp17(0) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 511818 [binary:497283,511816] c0_1(a33) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 511821 [binary:511545,511816] c2_1(a33) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 511829 [binary:511280,511821] -c0_1(a33) | c1_1(a33) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 511833 [binary:511818,511829,factor:factor] c1_1(a33) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 511835 [binary:497358,511833] -hskp17(0) | -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 511848 [binary:511816,511835,factor:factor] -c1_1(X) | -c2_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 511850 [binary:497567,511848,cut:509989] -c2_1(a19) | c0_1(a19) | hskp21(0) | c2_1(X) | c0_1(X).
% 511948 [binary:497566,511850,cut:509989] c0_1(a19) | hskp21(0) | c2_1(X) | c0_1(X).
% 511950 [binary:497368,511948] -hskp11(0) | hskp21(0) | c2_1(X) | c0_1(X).
% 511959 [binary:497309,511950,cut:509989] hskp21(0) | c2_1(X) | c0_1(X).
% 511961 [binary:497289,511959] c3_1(a47) | c2_1(X) | c0_1(X).
% 511963 [binary:497290,511959,factor] c2_1(a47) | c0_1(a47).
% 511973 [binary:504469,511961,binarycut:511963] c1_1(a47) | c0_1(a47) | c2_1(X) | c0_1(X).
% 512008 [binary:511848,511973,binarycut:511963,factor:factor] c0_1(a47) | c2_1(X) | c0_1(X).
% 512011 [binary:497353,512008] -hskp21(0) | c2_1(X) | c0_1(X).
% 512018 [binary:511959,512011,factor] c2_1(X) | c0_1(X).
% 512029 [binary:497721,512018] c3_1(a22) | c0_1(a22) | hskp15(0).
% 512104 [binary:504469,512029,binarycut:512018] c1_1(a22) | c0_1(a22) | hskp15(0).
% 512115 [binary:497364,512104,binarycut:497363] -hskp13(0) | hskp15(0).
% 512126 [binary:497719,512115,binarycut:512018] hskp15(0) | c3_1(X) | c0_1(X).
% 512128 [binary:508797,512115,binarycut:512018] hskp15(0) | -c1_1(X) | c0_1(X).
% 512131 [binary:497279,512126,factor] c3_1(a28) | c0_1(a28).
% 512132 [binary:497280,512126] c2_1(a28) | c3_1(X) | c0_1(X).
% 512137 [binary:504469,512131,binarycut:512018] c1_1(a28) | c0_1(a28).
% 512139 [binary:497361,512137] -hskp15(0) | c0_1(a28).
% 512156 [binary:512139,512128,factor:binarycut:512137] c0_1(a28).
% 512162 [binary:511280,512132,cut:512156] c1_1(a28) | c3_1(X) | c0_1(X).
% 512168 [binary:497361,512162] -hskp15(0) | c3_1(X) | c0_1(X).
% 512188 [binary:512126,512168,factor] c3_1(X) | c0_1(X).
% 512192 [binary:497352,512188,binarycut:497351] -hskp22(0).
% 512194 [binary:497356,512188,binarycut:497355] -hskp19(0).
% 512229 [binary:503440,512194,cut:512192] 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: 21804
% derived clauses: 1279200
% kept clauses: 277061
% kept size sum: 980068
% kept mid-nuclei: 147474
% kept new demods: 0
% forw unit-subs: 25
% forw double-subs: 100914
% forw overdouble-subs: 553057
% backward subs: 6499
% fast unit cutoff: 15881
% full unit cutoff: 0
% dbl unit cutoff: 18346
% real runtime: 263.71
% process. runtime: 262.64
% specific non-discr-tree subsumption statistics:
% tried: 149917522
% length fails: 906762
% strength fails: 63977484
% predlist fails: 69301126
% aux str. fails: 1958923
% by-lit fails: 9242656
% full subs tried: 2590118
% full subs fail: 2491685
%
% ; 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/SYN500-1+noeq.in")
%
%------------------------------------------------------------------------------