%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SYN460-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 : art07.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 258.5s
% Output : Assurance 258.5s
% 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/SYN460-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(296,40,1,592,0,1,94370,4,2362,120922,5,3002,120923,5,3002,120923,1,3002,120923,50,3003,120923,40,3003,121219,0,3003,121544,50,3004,121840,0,3006,122165,50,3007,122461,0,3007,122786,50,3008,123082,0,3010,123407,50,3010,123703,0,3012,124028,50,3013,124324,0,3013,124649,50,3014,124945,0,3016,125270,50,3016,125566,0,3018,125891,50,3019,126187,0,3019,126512,50,3020,126808,0,3022,127133,50,3023,127429,0,3025,127754,50,3026,128050,0,3026,128375,50,3027,128671,0,3028,128996,50,3029,129292,0,3031,129617,50,3032,129913,0,3032,130238,50,3033,130534,0,3035,130859,50,3036,131155,0,3038,131480,50,3039,131776,0,3039,132101,50,3040,132397,0,3042,132722,50,3043,133018,0,3045,133343,50,3046,133639,0,3046,133964,50,3047,133964,40,3047,134260,0,3049,155123,3,3950,157388,4,4400,158538,5,4850,158538,1,4850,158538,50,4850,158538,40,4850,158834,0,4850,274687,3,9364,275291,4,11601,276216,5,13851,276217,1,13851,276217,50,13853,276217,40,13853,276513,0,13853,333009,3,15363,333559,4,16104,336007,1,16854,336007,50,16856,336007,40,16856,336303,0,16856,407109,3,19561,408039,4,20907,408851,5,22257,408852,1,22257,408852,50,22259,408852,40,22259,409148,0,22259,463486,3,23767,464061,4,24510,466537,1,25260,466537,50,25261,466537,40,25261,466833,0,25261,467144,50,25262,467144,40,25262,467440,0,25268)
%
%
% START OF PROOF
% 467145 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c3_1(Y) | -c3_1(Z) | -c1_1(Z) | -c0_1(Y) | c3_1(X) | c0_1(X) | c0_1(Z).
% 467147 [] -ndr1_0(0) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | -c1_1(Z) | -c0_1(Z) | c3_1(X) | c3_1(Z) | c0_1(X) | c0_1(Y).
% 467148 [] -ndr1_0(0) | -c3_1(X) | -c1_1(Z) | -c1_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(Z) | c2_1(Y) | c2_1(X) | c0_1(Z).
% 467149 [] -ndr1_0(0) | -c2_1(X) | -c3_1(Y) | -c1_1(X) | -c0_1(X) | -c0_1(Z) | c2_1(Y) | c2_1(Z) | c3_1(Z) | c1_1(Y).
% 467150 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | -c0_1(X) | c2_1(Z) | c3_1(Z) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 467151 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c3_1(Y) | -c0_1(Z) | c2_1(Z) | c1_1(X) | c1_1(Y) | c1_1(Z) | c0_1(X).
% 467152 [] -ndr1_0(0) | -c2_1(Z) | -c2_1(Y) | -c2_1(X) | -c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Z) | c0_1(Y) | c0_1(Z).
% 467153 [] -ndr1_0(0) | -c2_1(Y) | -c2_1(X) | -c0_1(Z) | -c0_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(X) | c0_1(X).
% 467155 [] -ndr1_0(0) | -c3_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 467156 [] -ndr1_0(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c2_1(Z) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c1_1(Y) | c0_1(Z).
% 467159 [] -ndr1_0(0) | hskp40(0) | -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c0_1(X).
% 467160 [] -ndr1_0(0) | hskp10(0) | -c3_1(X) | -c3_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y).
% 467163 [] -ndr1_0(0) | hskp44(0) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c1_1(Y).
% 467165 [] -ndr1_0(0) | hskp56(0) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 467166 [] -ndr1_0(0) | hskp10(0) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y).
% 467168 [] -ndr1_0(0) | hskp3(0) | -c2_1(X) | -c2_1(Y) | -c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 467169 [] -ndr1_0(0) | hskp26(0) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 467171 [] -ndr1_0(0) | hskp32(0) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y).
% 467173 [] -ndr1_0(0) | hskp13(0) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 467174 [] -ndr1_0(0) | hskp40(0) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 467175 [] -ndr1_0(0) | hskp38(0) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 467176 [] -ndr1_0(0) | hskp53(0) | -c0_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 467177 [] -ndr1_0(0) | hskp47(0) | -c3_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 467178 [] -ndr1_0(0) | hskp1(0) | -c1_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 467180 [?] ?
% 467182 [?] ?
% 467185 [?] ?
% 467186 [?] ?
% 467187 [?] ?
% 467188 [?] ?
% 467190 [?] ?
% 467191 [?] ?
% 467192 [?] ?
% 467193 [?] ?
% 467194 [?] ?
% 467195 [?] ?
% 467196 [?] ?
% 467197 [?] ?
% 467198 [?] ?
% 467200 [] -hskp1(0) | c3_1(a2182).
% 467202 [] -hskp2(0) | c3_1(a2187).
% 467203 [] -hskp3(0) | c2_1(a2190).
% 467204 [] -hskp4(0) | c3_1(a2191).
% 467206 [] -hskp7(0) | c0_1(a2198).
% 467207 [] -hskp7(0) | c2_1(a2198).
% 467208 [] -hskp9(0) | c0_1(a2203).
% 467209 [] -hskp11(0) | c0_1(a2209).
% 467210 [] -hskp12(0) | c2_1(a2211).
% 467211 [] -hskp13(0) | c2_1(a2212).
% 467212 [] -hskp13(0) | c0_1(a2212).
% 467213 [] -hskp14(0) | c2_1(a2213).
% 467215 [] -hskp17(0) | c2_1(a2221).
% 467216 [] -hskp18(0) | c3_1(a2222).
% 467217 [] -hskp18(0) | c0_1(a2222).
% 467221 [] -hskp22(0) | c0_1(a2244).
% 467227 [] -hskp26(0) | c2_1(a2178).
% 467228 [] -hskp26(0) | c0_1(a2178).
% 467238 [] -hskp32(0) | c0_1(a2186).
% 467240 [] -hskp34(0) | c3_1(a2189).
% 467241 [] -hskp34(0) | c1_1(a2189).
% 467246 [] -hskp37(0) | c2_1(a2196).
% 467247 [] -hskp37(0) | c1_1(a2196).
% 467248 [] -hskp38(0) | c1_1(a2200).
% 467250 [] -hskp40(0) | c3_1(a2204).
% 467251 [] -hskp40(0) | c2_1(a2204).
% 467252 [] -hskp41(0) | c1_1(a2205).
% 467254 [] -hskp42(0) | c0_1(a2207).
% 467255 [] -hskp42(0) | c1_1(a2207).
% 467256 [] -hskp43(0) | c0_1(a2208).
% 467257 [] -hskp43(0) | c3_1(a2208).
% 467259 [] -hskp44(0) | c2_1(a2215).
% 467263 [] -hskp46(0) | c2_1(a2218).
% 467264 [] -hskp46(0) | c0_1(a2218).
% 467265 [] -hskp47(0) | c0_1(a2226).
% 467266 [] -hskp47(0) | c2_1(a2226).
% 467271 [] -hskp50(0) | c1_1(a2231).
% 467272 [] -hskp50(0) | c2_1(a2231).
% 467273 [] -hskp51(0) | c2_1(a2232).
% 467274 [] -hskp51(0) | c3_1(a2232).
% 467275 [] -hskp51(0) | c0_1(a2232).
% 467276 [] -hskp52(0) | c2_1(a2234).
% 467277 [] -hskp52(0) | c3_1(a2234).
% 467279 [] -hskp53(0) | c3_1(a2235).
% 467280 [] -hskp53(0) | c2_1(a2235).
% 467281 [] -hskp53(0) | c0_1(a2235).
% 467282 [] -hskp54(0) | c0_1(a2240).
% 467284 [] -hskp54(0) | c1_1(a2240).
% 467285 [] -hskp55(0) | c2_1(a2241).
% 467286 [] -hskp55(0) | c0_1(a2241).
% 467287 [] -hskp55(0) | c1_1(a2241).
% 467288 [] -hskp56(0) | c2_1(a2242).
% 467289 [] -hskp57(0) | c3_1(a2243).
% 467290 [] -hskp57(0) | c0_1(a2243).
% 467291 [] -hskp57(0) | c1_1(a2243).
% 467292 [] -hskp58(0) | c0_1(a2252).
% 467293 [] hskp21(0) | hskp54(0) | hskp55(0).
% 467294 [] hskp3(0) | hskp11(0) | hskp12(0).
% 467295 [] hskp6(0) | hskp34(0) | hskp37(0).
% 467319 [] -hskp21(0) | ndr1_0(0).
% 467352 [] -hskp54(0) | ndr1_0(0).
% 467353 [] -hskp55(0) | ndr1_0(0).
% 467357 [] -c2_1(a2252) | -hskp58(0).
% 467358 [] -c1_1(a2252) | -hskp58(0).
% 467359 [] -c1_1(a2242) | -hskp56(0).
% 467360 [] -c3_1(a2242) | -hskp56(0).
% 467361 [] -c3_1(a2231) | -hskp50(0).
% 467364 [] -c1_1(a2226) | -hskp47(0).
% 467365 [] -c3_1(a2218) | -hskp46(0).
% 467366 [] -c0_1(a2215) | -hskp44(0).
% 467367 [] -c2_1(a2208) | -hskp43(0).
% 467368 [] -c3_1(a2207) | -hskp42(0).
% 467369 [] -c0_1(a2205) | -hskp41(0).
% 467370 [] -c1_1(a2204) | -hskp40(0).
% 467373 [] -c0_1(a2200) | -hskp38(0).
% 467374 [] -c2_1(a2200) | -hskp38(0).
% 467375 [] -c0_1(a2196) | -hskp37(0).
% 467378 [] -c0_1(a2189) | -hskp34(0).
% 467381 [] -c3_1(a2186) | -hskp32(0).
% 467382 [] -c2_1(a2186) | -hskp32(0).
% 467389 [] -c3_1(a2178) | -hskp26(0).
% 467394 [] -c2_1(a2244) | -hskp22(0).
% 467395 [] -c1_1(a2244) | -hskp22(0).
% 467396 [] -c0_1(a2239) | -hskp21(0).
% 467397 [] -c3_1(a2239) | -hskp21(0).
% 467399 [] -c0_1(a2233) | -hskp19(0).
% 467400 [] -c1_1(a2233) | -hskp19(0).
% 467401 [] -c3_1(a2233) | -hskp19(0).
% 467402 [] -c2_1(a2222) | -hskp18(0).
% 467403 [] -c0_1(a2221) | -hskp17(0).
% 467404 [] -c3_1(a2221) | -hskp17(0).
% 467405 [] -c2_1(a2220) | -hskp16(0).
% 467406 [] -c1_1(a2220) | -hskp16(0).
% 467407 [] -c3_1(a2220) | -hskp16(0).
% 467410 [] -c1_1(a2213) | -hskp14(0).
% 467411 [] -c0_1(a2213) | -hskp14(0).
% 467412 [] -c3_1(a2212) | -hskp13(0).
% 467413 [] -c1_1(a2211) | -hskp12(0).
% 467414 [] -c3_1(a2211) | -hskp12(0).
% 467415 [] -c1_1(a2209) | -hskp11(0).
% 467416 [] -c2_1(a2209) | -hskp11(0).
% 467417 [] -c2_1(a2206) | -hskp10(0).
% 467418 [] -c0_1(a2206) | -hskp10(0).
% 467419 [] -c3_1(a2206) | -hskp10(0).
% 467420 [] -c1_1(a2203) | -hskp9(0).
% 467421 [] -c3_1(a2203) | -hskp9(0).
% 467422 [] -c2_1(a2202) | -hskp8(0).
% 467423 [] -c1_1(a2202) | -hskp8(0).
% 467424 [] -c0_1(a2202) | -hskp8(0).
% 467425 [] -c3_1(a2198) | -hskp7(0).
% 467426 [] -c0_1(a2197) | -hskp6(0).
% 467427 [] -c3_1(a2197) | -hskp6(0).
% 467428 [] -c1_1(a2197) | -hskp6(0).
% 467431 [] -c2_1(a2191) | -hskp4(0).
% 467432 [] -c1_1(a2191) | -hskp4(0).
% 467433 [] -c1_1(a2190) | -hskp3(0).
% 467434 [] -c0_1(a2190) | -hskp3(0).
% 467435 [] -c2_1(a2187) | -hskp2(0).
% 467436 [] -c0_1(a2182) | -hskp1(0).
% 467437 [] -c2_1(a2182) | -hskp1(0).
% 467438 [] -c0_1(a2181) | -hskp0(0).
% 467439 [] -c1_1(a2181) | -hskp0(0).
% 467440 [] -c2_1(a2181) | -hskp0(0).
% 467730 [binary:467319,467293,binarycut:467352,binarycut:467353] ndr1_0(0).
% 467731 [binary:467145,467730] -c2_1(X) | -c2_1(Y) | -c3_1(X) | -c3_1(Z) | -c1_1(Z) | -c0_1(X) | c3_1(Y) | c0_1(Y) | c0_1(Z).
% 467733 [binary:467147,467730] -c2_1(X) | -c3_1(Y) | -c1_1(Y) | -c1_1(Z) | -c0_1(Z) | c3_1(Z) | c3_1(X) | c0_1(X) | c0_1(Y).
% 467734 [binary:467148,467730] -c3_1(X) | -c1_1(Z) | -c1_1(X) | -c1_1(Y) | -c0_1(Z) | c2_1(X) | c2_1(Z) | c2_1(Y) | c0_1(Y).
% 467735 [binary:467149,467730] -c2_1(X) | -c3_1(Y) | -c1_1(X) | -c0_1(Z) | -c0_1(X) | c2_1(Z) | c2_1(Y) | c3_1(Z) | c1_1(Y).
% 467736 [binary:467150,467730] -c2_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(Y) | c2_1(Z) | c3_1(Y) | c3_1(Z) | c1_1(X) | c0_1(X).
% 467737 [binary:467151,467730] -c2_1(X) | -c2_1(Y) | -c3_1(X) | -c0_1(Z) | c2_1(Z) | c1_1(Z) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 467738 [binary:467152,467730] -c2_1(Y) | -c2_1(Z) | -c2_1(X) | -c3_1(Y) | c3_1(X) | c1_1(Z) | c1_1(Y) | c0_1(X) | c0_1(Z).
% 467739 [binary:467153,467730] -c2_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c3_1(Z) | c3_1(X) | c1_1(Y) | c1_1(Z) | c0_1(Y).
% 467741 [binary:467155,467730] -c3_1(X) | -c0_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c1_1(Y) | c0_1(Z).
% 467742 [binary:467156,467730] -c3_1(X) | -c0_1(X) | c2_1(Z) | c2_1(X) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c0_1(Y).
% 467745 [binary:467159,467730] hskp40(0) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c0_1(X).
% 467746 [binary:467160,467730] hskp10(0) | -c3_1(X) | -c3_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y).
% 467749 [binary:467163,467730] hskp44(0) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c1_1(Y).
% 467751 [binary:467165,467730] hskp56(0) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 467752 [binary:467166,467730] hskp10(0) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y).
% 467754 [binary:467168,467730] hskp3(0) | -c2_1(X) | -c2_1(Y) | -c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 467755 [binary:467169,467730] hskp26(0) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c1_1(X) | c0_1(Y) | c0_1(X).
% 467757 [binary:467171,467730] hskp32(0) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c1_1(X) | c1_1(Y).
% 467759 [binary:467173,467730] hskp13(0) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 467760 [binary:467174,467730] hskp40(0) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 467761 [binary:467175,467730] hskp38(0) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 467762 [binary:467176,467730] hskp53(0) | -c0_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 467763 [binary:467177,467730] hskp47(0) | -c3_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 467764 [binary:467178,467730] hskp1(0) | -c1_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 467767 [binary:467203,467294] c2_1(a2190) | hskp11(0) | hskp12(0).
% 467769 [input:467180,cut:467730] hskp50(0) | hskp51(0) | -c2_1(X) | -c1_1(X) | c0_1(X).
% 467770 [binary:467271,467769] c1_1(a2231) | hskp51(0) | -c2_1(X) | -c1_1(X) | c0_1(X).
% 467771 [binary:467272,467769] c2_1(a2231) | hskp51(0) | -c2_1(X) | -c1_1(X) | c0_1(X).
% 467783 [input:467182,cut:467730] hskp34(0) | hskp46(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 467784 [binary:467240,467783] c3_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 467785 [binary:467241,467783] c1_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 467796 [input:467185,cut:467730] hskp0(0) | -c2_1(X) | -c1_1(X) | -c0_1(X).
% 467797 [input:467186,cut:467730] hskp17(0) | -c2_1(X) | -c1_1(X) | c3_1(X).
% 467798 [binary:467215,467797] c2_1(a2221) | -c2_1(X) | -c1_1(X) | c3_1(X).
% 467800 [input:467195,cut:467730] hskp58(0) | -c3_1(X) | c2_1(X) | c1_1(X).
% 467801 [binary:467292,467800] c0_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 467807 [input:467196,cut:467730] hskp18(0) | -c1_1(X) | c2_1(X) | c3_1(X).
% 467808 [binary:467216,467807] c3_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 467810 [binary:467217,467807] c0_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 467813 [input:467187,cut:467730] hskp22(0) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 467814 [binary:467221,467813] c0_1(a2244) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 467823 [input:467188,cut:467730] hskp19(0) | hskp52(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 467837 [input:467190,cut:467730] hskp16(0) | hskp17(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 467838 [input:467191,cut:467730] hskp4(0) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 467839 [binary:467204,467838] c3_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 467846 [input:467192,cut:467730] hskp10(0) | hskp41(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 467847 [input:467193,cut:467730] hskp8(0) | hskp9(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 467848 [input:467194,cut:467730] hskp7(0) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 467849 [binary:467206,467848] c0_1(a2198) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 467850 [binary:467207,467848] c2_1(a2198) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 467855 [input:467197,cut:467730] hskp42(0) | hskp43(0) | c3_1(X) | c1_1(X) | c0_1(X).
% 467856 [binary:467254,467855] c0_1(a2207) | hskp43(0) | c3_1(X) | c1_1(X) | c0_1(X).
% 467858 [binary:467255,467855] c1_1(a2207) | hskp43(0) | c3_1(X) | c1_1(X) | c0_1(X).
% 467863 [input:467198,cut:467730] hskp2(0) | hskp32(0) | c3_1(X) | c1_1(X) | c0_1(X).
% 467866 [binary:467202,467863] c3_1(a2187) | hskp32(0) | c3_1(X) | c1_1(X) | c0_1(X).
% 467889 [binary:467250,467745] c3_1(a2204) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c0_1(X).
% 467890 [binary:467251,467745] c2_1(a2204) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c0_1(X).
% 467912 [binary:467259,467749] c2_1(a2215) | -c3_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(X).
% 467923 [binary:467798,467733,factor:factor] c3_1(a2221) | c0_1(a2221) | -c2_1(X) | -c3_1(Y) | -c1_1(X) | -c1_1(Y) | -c0_1(X) | c3_1(X) | c0_1(Y).
% 467928 [binary:467288,467751] c2_1(a2242) | -c2_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c1_1(X).
% 467934 [binary:467808,467734,factor:factor:factor] -c1_1(a2222) | c2_1(a2222) | -c1_1(X) | -c1_1(Y) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(X) | c0_1(X).
% 467963 [binary:467203,467754] c2_1(a2190) | -c2_1(X) | -c2_1(Y) | -c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y).
% 467965 [binary:467227,467755] c2_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 467966 [binary:467228,467755] c0_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 467987 [binary:467238,467757] c0_1(a2186) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X).
% 467994 [binary:467767,467737] -c3_1(a2190) | c1_1(a2190) | hskp11(0) | hskp12(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 468000 [binary:467211,467759] c2_1(a2212) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468001 [binary:467212,467759] c0_1(a2212) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468005 [binary:467250,467760] c3_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468007 [binary:467251,467760] c2_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468019 [binary:467248,467761] c1_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 468032 [binary:467279,467762] c3_1(a2235) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 468036 [binary:467280,467762] c2_1(a2235) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 468038 [binary:467281,467762] c0_1(a2235) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 468061 [binary:467265,467763] c0_1(a2226) | -c3_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 468063 [binary:467266,467763] c2_1(a2226) | -c3_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 468064 [binary:467266,467763,factor] c2_1(a2226) | c3_1(a2226) | c1_1(a2226) | -c3_1(X) | c2_1(X) | c0_1(X).
% 468072 [binary:467739,468064,factor] -c0_1(a2226) | c3_1(a2226) | c1_1(a2226) | -c2_1(X) | -c3_1(Y) | c2_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 468085 [binary:467200,467764] c3_1(a2182) | -c1_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 468097 [binary:467808,467741] -c0_1(a2222) | c2_1(a2222) | -c1_1(X) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 468110 [binary:467866,467741,factor] -c0_1(a2187) | c2_1(a2187) | hskp32(0) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 468117 [binary:467808,467742,factor:factor] -c0_1(a2222) | c2_1(a2222) | -c1_1(X) | c2_1(Y) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 468153 [binary:467737,467890,factor:factor:factor:factor:factor:factor:factor:factor] -c2_1(a2204) | -c3_1(a2204) | c1_1(a2204) | c0_1(a2204) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 468301 [binary:467738,467965,factor:factor:factor:factor:factor:factor:factor:factor] -c3_1(a2178) | c1_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(Y) | c0_1(X).
% 468355 [binary:467739,468000,factor:factor:factor:factor:factor] -c0_1(a2212) | c3_1(a2212) | -c2_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468400 [binary:467737,468036,factor:factor:factor:factor:factor:factor:factor] -c3_1(a2235) | c1_1(a2235) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 468420 [binary:467738,468063] -c3_1(a2226) | c1_1(a2226) | -c2_1(Y) | -c2_1(X) | -c3_1(Z) | c2_1(U) | c2_1(Z) | c3_1(Y) | c3_1(U) | c1_1(X) | c1_1(U) | c0_1(Y) | c0_1(X) | c0_1(Z).
% 468445 [binary:467890,468153,factor:factor:factor:factor] -c3_1(a2204) | c1_1(a2204) | c0_1(a2204) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 468453 [binary:467404,467923,binarycut:467403] -hskp17(0) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | -c1_1(X) | -c0_1(X) | c3_1(X) | c0_1(Y).
% 468457 [binary:467797,468453,factor] -c2_1(X) | -c3_1(Y) | -c1_1(Y) | -c1_1(X) | -c0_1(X) | c3_1(X) | c0_1(Y).
% 468471 [binary:467965,468457,factor:factor] -c1_1(a2178) | -c0_1(a2178) | c3_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c1_1(X) | c0_1(X) | c0_1(Y).
% 468496 [binary:467810,468117,factor:factor] c2_1(a2222) | -c1_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X).
% 468499 [binary:467402,468496] -hskp18(0) | -c1_1(X) | c2_1(Y) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 468514 [binary:467807,468499,factor] -c1_1(X) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X).
% 468526 [binary:468019,468514,factor:factor:factor:factor] c2_1(a2200) | c3_1(a2200) | c0_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 468565 [binary:468001,468355,factor:factor:factor:factor] c3_1(a2212) | -c2_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468568 [binary:467412,468565] -hskp13(0) | -c2_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468572 [binary:467759,468568,factor:factor] -c2_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468589 [binary:467963,468572,factor:factor:factor:factor] -c3_1(a2190) | c1_1(a2190) | c0_1(a2190) | -c2_1(X) | -c2_1(Y) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468595 [binary:468007,468572,factor:factor:factor:factor] -c3_1(a2204) | c1_1(a2204) | c0_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468643 [binary:468032,468400,factor:factor:factor:factor:factor] c1_1(a2235) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 468661 [binary:468061,468072,factor:factor:factor] c3_1(a2226) | c1_1(a2226) | -c2_1(X) | -c3_1(Y) | c2_1(Y) | c2_1(Z) | c3_1(Z) | c1_1(X) | c1_1(Z) | c0_1(Y) | c0_1(X).
% 468754 [binary:468005,468595,factor:factor:factor:factor:factor] c1_1(a2204) | c0_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468756 [binary:467370,468754] -hskp40(0) | c0_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 468764 [binary:467760,468756,factor:factor] c0_1(a2204) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 468888 [binary:467889,468445,factor:factor:factor:factor] c1_1(a2204) | c0_1(a2204) | -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 468890 [binary:467370,468888] -hskp40(0) | c0_1(a2204) | -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 468895 [binary:467745,468890,factor:factor:factor:factor] c0_1(a2204) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 468924 [binary:467374,468526,binarycut:467373] -hskp38(0) | c3_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 468933 [binary:467761,468924,factor:factor:factor] c3_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 469081 [binary:467810,468097,factor:factor] c2_1(a2222) | -c1_1(X) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c1_1(Y) | c0_1(Z).
% 469083 [binary:467402,469081] -hskp18(0) | -c1_1(X) | c2_1(Y) | c2_1(X) | c3_1(Z) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 469111 [binary:467807,469083,factor] -c1_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c3_1(X) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 469118 [binary:467858,469111,factor:factor] c2_1(a2207) | c3_1(a2207) | hskp43(0) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 469120 [binary:467858,469111,factor:factor:factor:factor] c2_1(a2207) | c3_1(a2207) | hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 469147 [binary:468457,469120] -c1_1(a2207) | -c0_1(a2207) | c3_1(a2207) | hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 469158 [binary:467739,469118,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] -c0_1(a2207) | c3_1(a2207) | hskp43(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470107 [binary:467856,469158,factor:factor:factor] c3_1(a2207) | hskp43(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470110 [binary:467368,470107] -hskp42(0) | hskp43(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 470120 [binary:467855,470110,factor] hskp43(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 470122 [binary:467256,470120] c0_1(a2208) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470124 [binary:467257,470120] c3_1(a2208) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470143 [binary:467741,470124,factor:factor:factor:factor:factor:factor] -c0_1(a2208) | c2_1(a2208) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470150 [binary:470122,470143,factor:factor:factor:factor] c2_1(a2208) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 470152 [binary:467367,470150] -hskp43(0) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 470160 [binary:470120,470152,factor:factor] -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(X).
% 470349 [binary:467858,469147,factor:factor] -c0_1(a2207) | c3_1(a2207) | hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470353 [binary:467856,470349,factor:factor] c3_1(a2207) | hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 470356 [binary:467368,470353] -hskp42(0) | hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470365 [binary:467855,470356,factor] hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 470367 [binary:467256,470365] c0_1(a2208) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470370 [binary:467257,470365] c3_1(a2208) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470391 [binary:467741,470370,factor:factor:factor] -c0_1(a2208) | c2_1(a2208) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470397 [binary:470367,470391,factor:factor:factor:factor] c2_1(a2208) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470399 [binary:467367,470397] -hskp43(0) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 470424 [binary:470365,470399,factor:factor] -c3_1(X) | -c1_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 470448 [binary:468933,470424,factor:factor:factor] -c1_1(a2200) | c0_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 470509 [binary:468019,470448,factor:factor:factor:factor] c0_1(a2200) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 470511 [binary:467373,470509] -hskp38(0) | -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 470521 [binary:467761,470511,factor:factor] -c1_1(X) | -c0_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 470529 [binary:467858,470521,factor:factor] -c0_1(a2207) | c3_1(a2207) | hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470544 [binary:467856,470529,factor:factor] c3_1(a2207) | hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470547 [binary:467368,470544] -hskp42(0) | hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470554 [binary:467855,470547,factor] hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470556 [binary:467256,470554] c0_1(a2208) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470558 [binary:467257,470554] c3_1(a2208) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470572 [binary:467741,470558,factor:factor:factor] -c0_1(a2208) | c2_1(a2208) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470576 [binary:470556,470572,factor:factor] c2_1(a2208) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470579 [binary:467367,470576] -hskp43(0) | c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470588 [binary:470554,470579,factor] c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 470591 [binary:467405,470588,binarycut:467407,binarycut:467406] -hskp16(0) | c0_1(a2220).
% 470593 [binary:467417,470588,binarycut:467419,binarycut:467418] -hskp10(0) | c1_1(a2206).
% 470595 [binary:467422,470588,binarycut:467423,binarycut:467424] -hskp8(0) | c3_1(a2202).
% 470597 [binary:467440,470588,binarycut:467439,binarycut:467438] -hskp0(0) | c3_1(a2181).
% 470600 [binary:467736,470588] -c2_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c3_1(Z) | c1_1(Z) | c0_1(Z).
% 470608 [binary:470160,470588] -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 470610 [binary:467837,470591] c0_1(a2220) | hskp17(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 470613 [binary:467846,470593] c1_1(a2206) | hskp41(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 470615 [binary:467752,470593] c1_1(a2206) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y).
% 470618 [binary:467847,470595] c3_1(a2202) | hskp9(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 470621 [binary:467796,470597] c3_1(a2181) | -c2_1(X) | -c1_1(X) | -c0_1(X).
% 470649 [binary:467801,470608] c2_1(a2252) | c3_1(a2252) | c1_1(a2252) | -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 470665 [binary:468514,470615] c2_1(a2206) | c3_1(a2206) | c0_1(a2206) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Z) | c2_1(Y) | c3_1(Z) | c3_1(X) | c1_1(Z) | c1_1(Y).
% 470774 [binary:467850,470600,factor:factor:factor] -c0_1(a2198) | c3_1(a2198) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 470973 [binary:467357,470649,binarycut:467358] -hskp58(0) | c3_1(a2252) | -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 470981 [binary:467800,470973,factor] c3_1(a2252) | -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 471062 [binary:467849,470774,factor:factor] c3_1(a2198) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 471064 [binary:467425,471062] -hskp7(0) | hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 471091 [binary:467848,471064,factor] hskp37(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 471093 [binary:467246,471091] c2_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 471095 [binary:467247,471091] c1_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 471826 [binary:467417,470665,binarycut:467419,binarycut:467418] -hskp10(0) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c2_1(Z) | c3_1(Z) | c3_1(X) | c1_1(Y) | c1_1(Z).
% 471839 [binary:467752,471826,factor:factor] -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c2_1(Z) | c3_1(X) | c3_1(Z) | c1_1(Z) | c1_1(Y).
% 471874 [binary:468000,471839,factor:factor:factor:factor:factor:factor:factor] -c0_1(a2212) | c3_1(a2212) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 471928 [binary:468001,471874,factor:factor:factor:factor] c3_1(a2212) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 471931 [binary:467412,471928] -hskp13(0) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(X).
% 471947 [binary:467759,471931,factor:factor] -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 471951 [binary:467839,471947,factor:factor] c2_1(a2191) | c1_1(a2191) | c0_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 471963 [binary:470621,471947] c2_1(a2181) | c1_1(a2181) | c0_1(a2181) | -c2_1(X) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c1_1(Y).
% 472025 [binary:467440,471963,binarycut:467439,binarycut:467438] -hskp0(0) | -c2_1(X) | -c1_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y).
% 472060 [binary:467796,472025,factor] -c2_1(X) | -c1_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c1_1(Y).
% 472085 [binary:468036,472060,factor:factor:factor:factor] -c1_1(a2235) | -c0_1(a2235) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 472107 [binary:468643,472085,factor:factor] -c0_1(a2235) | -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 472117 [binary:468038,472107,factor:factor] -c2_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 472129 [binary:467431,471951,binarycut:467432] -hskp4(0) | c0_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 472143 [binary:467838,472129,factor] c0_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 472818 [binary:468661,468420,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c1_1(a2226) | -c2_1(X) | -c3_1(Y) | c2_1(Z) | c2_1(Y) | c3_1(Z) | c3_1(X) | c1_1(X) | c1_1(Z) | c0_1(Y) | c0_1(X).
% 473577 [binary:467364,472818] -hskp47(0) | -c2_1(X) | -c3_1(Y) | c2_1(Y) | c2_1(Z) | c3_1(X) | c3_1(Z) | c1_1(X) | c1_1(Z) | c0_1(X) | c0_1(Y).
% 473608 [binary:467763,473577,factor:factor] -c2_1(X) | -c3_1(Y) | c2_1(Y) | c2_1(Z) | c3_1(Z) | c3_1(X) | c1_1(Z) | c1_1(X) | c0_1(X) | c0_1(Y).
% 473623 [binary:470588,473608] -c3_1(X) | c2_1(Y) | c2_1(X) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(Y) | c0_1(Z) | c0_1(X).
% 473634 [binary:467866,473623,factor:factor:factor] c2_1(a2187) | c0_1(a2187) | hskp32(0) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 473673 [binary:467435,473634] -hskp2(0) | c0_1(a2187) | hskp32(0) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473677 [binary:467863,473673,factor:factor] c0_1(a2187) | hskp32(0) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473683 [binary:468110,473677,factor:factor:factor] c2_1(a2187) | hskp32(0) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473685 [binary:467435,473683] -hskp2(0) | hskp32(0) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473698 [binary:467863,473685,factor] hskp32(0) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 473701 [binary:467238,473698] c0_1(a2186) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 473715 [binary:470608,473701,factor:factor:factor:factor] c2_1(a2186) | c3_1(a2186) | c1_1(a2186) | c3_1(X) | c1_1(X) | c0_1(X).
% 473718 [binary:467382,473715,binarycut:467381] -hskp32(0) | c1_1(a2186) | c3_1(X) | c1_1(X) | c0_1(X).
% 473739 [binary:473698,473718,factor:factor:factor:factor] c1_1(a2186) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473750 [binary:469111,473739,factor:factor:factor:factor:factor:factor:factor:factor] c2_1(a2186) | c3_1(a2186) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473770 [binary:467382,473750,binarycut:467381] -hskp32(0) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473806 [binary:473698,473770,factor:factor] c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 473822 [binary:467739,473806,factor:factor:factor:factor:factor:factor] -c2_1(X) | -c0_1(Y) | c3_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(X).
% 473881 [binary:470588,473822] -c0_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 473885 [binary:467966,473881,factor:factor] c3_1(a2178) | c1_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(Y) | c0_1(X).
% 473908 [binary:468301,473885,factor:factor:factor:factor] c1_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 473913 [binary:468471,473908,factor:factor:factor:factor] -c0_1(a2178) | c3_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 473926 [binary:467966,473913,factor:factor] c3_1(a2178) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 473928 [binary:467389,473926] -hskp26(0) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(Y) | c0_1(X).
% 473935 [binary:467755,473928,factor:factor] -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c1_1(X) | c0_1(X) | c0_1(Y).
% 473968 [binary:470588,473935] -c3_1(X) | -c1_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 473971 [binary:467784,473968] -c1_1(a2189) | c0_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 473988 [binary:468085,473968,factor:factor:factor:factor] -c1_1(a2182) | c0_1(a2182) | -c1_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 474121 [binary:467785,473971,factor] c0_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 474123 [binary:467378,474121] -hskp34(0) | hskp46(0) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 474126 [binary:467783,474123,factor] hskp46(0) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 474128 [binary:467263,474126] c2_1(a2218) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 474129 [binary:467264,474126] c0_1(a2218) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 474158 [binary:470600,474128,factor:factor:factor:factor] -c0_1(a2218) | c3_1(a2218) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(X) | c1_1(Z) | c0_1(Z).
% 475070 [binary:474129,474158,factor:factor:factor:factor] c3_1(a2218) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(X) | c0_1(Z).
% 475072 [binary:467365,475070] -hskp46(0) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c1_1(X) | c1_1(Z) | c0_1(Z).
% 475076 [binary:474126,475072,factor:factor:factor] -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c1_1(X) | c0_1(Z).
% 475110 [binary:470981,475076,factor:factor:factor:factor:factor] -c0_1(a2252) | c1_1(a2252) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(X) | c0_1(Z).
% 475263 [binary:467801,475110,factor:factor] c1_1(a2252) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c1_1(X) | c1_1(Z) | c0_1(Z).
% 475265 [binary:467358,475263] -hskp58(0) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(X) | c0_1(Z).
% 475268 [binary:467800,475265,factor] -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c1_1(X) | c0_1(Z).
% 475282 [binary:468085,475268,factor:factor:factor:factor] c2_1(a2182) | c1_1(a2182) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c3_1(X) | c1_1(Z) | c0_1(X) | c0_1(Z).
% 475286 [binary:470621,475268] c2_1(a2181) | c1_1(a2181) | -c2_1(X) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c0_1(Z).
% 475387 [binary:467440,475286,binarycut:467439] -hskp0(0) | -c2_1(X) | -c1_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c0_1(Z).
% 475402 [binary:467796,475387,factor] -c2_1(X) | -c1_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c0_1(Z).
% 475427 [binary:471093,475402,factor:factor:factor:factor] -c1_1(a2196) | -c0_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 475440 [binary:471095,475427,factor:factor:factor:factor] -c0_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 475456 [binary:467437,475282] -hskp1(0) | c1_1(a2182) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c0_1(Z) | c0_1(X).
% 475479 [binary:467764,475456,factor:factor:factor:factor:factor:factor] c1_1(a2182) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Z) | c3_1(Y) | c1_1(Z) | c0_1(X) | c0_1(Z).
% 475499 [binary:473988,475479,factor:factor:factor:factor:factor:factor:factor:factor] c0_1(a2182) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(Z) | c3_1(X) | c1_1(Z) | c0_1(X) | c0_1(Z).
% 475502 [binary:467436,475499] -hskp1(0) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c3_1(Z) | c1_1(Z) | c0_1(Z) | c0_1(X).
% 475506 [binary:467764,475502,factor:factor:factor] -c1_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Z) | c3_1(X) | c3_1(Y) | c1_1(Z) | c0_1(X) | c0_1(Z).
% 475530 [binary:471095,475506,factor:factor:factor:factor:factor:factor:factor] c3_1(a2196) | c0_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 475541 [binary:473968,475530,factor:factor:factor] -c1_1(a2196) | c0_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 475547 [binary:471095,475541,factor:factor:factor:factor] c0_1(a2196) | -c0_1(X) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y).
% 475552 [binary:475440,475547,factor:factor] -c0_1(X) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y).
% 475558 [binary:467987,475552] c2_1(a2186) | c3_1(a2186) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Z) | c1_1(Y) | c1_1(X) | c1_1(Z) | c0_1(Z).
% 475574 [binary:467382,475558,binarycut:467381] -hskp32(0) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Z) | c1_1(Z) | c1_1(Y) | c1_1(X) | c0_1(Z).
% 475583 [binary:467757,475574,factor:factor] -c3_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Z) | c1_1(X) | c1_1(Y) | c1_1(Z) | c0_1(Z).
% 475621 [binary:470618,475583,factor:factor:factor] c2_1(a2202) | c1_1(a2202) | hskp9(0) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475664 [binary:467422,475621,binarycut:467423] -hskp8(0) | hskp9(0) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 475679 [binary:467847,475664,factor] hskp9(0) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475681 [binary:467208,475679] c0_1(a2203) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475690 [binary:473881,475681,factor:factor:factor:factor] c3_1(a2203) | c1_1(a2203) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 475700 [binary:467421,475690,binarycut:467420] -hskp9(0) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X) | c0_1(Y).
% 475717 [binary:475679,475700,factor:factor] -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475719 [binary:467801,475717] c2_1(a2252) | c1_1(a2252) | -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475730 [binary:467357,475719,binarycut:467358] -hskp58(0) | -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475743 [binary:467800,475730,factor] -c3_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y) | c0_1(Y).
% 475751 [binary:468085,475743,factor:factor] c2_1(a2182) | c1_1(a2182) | -c1_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 475885 [binary:467437,475751] -hskp1(0) | c1_1(a2182) | -c1_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 475926 [binary:467764,475885,factor:factor:factor:factor] c1_1(a2182) | -c1_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 475938 [binary:473988,475926,factor:factor:factor:factor:factor:factor:factor] c0_1(a2182) | -c1_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 475941 [binary:467436,475938] -hskp1(0) | -c1_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 475945 [binary:467764,475941,factor:factor] -c1_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 475957 [binary:470613,475945] c3_1(a2206) | c0_1(a2206) | hskp41(0) | -c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 475995 [binary:467419,475957,binarycut:467418] -hskp10(0) | hskp41(0) | -c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 476047 [binary:467846,475995,factor] hskp41(0) | -c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 476060 [binary:467252,476047] c1_1(a2205) | -c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 476073 [binary:475945,476060,factor:factor:factor:factor:factor:factor:factor:factor:factor:factor] c3_1(a2205) | c0_1(a2205) | -c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 476089 [binary:473968,476073,factor:factor] -c1_1(a2205) | c0_1(a2205) | -c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 476096 [binary:476060,476089,factor:factor:factor:factor:factor] c0_1(a2205) | -c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 476098 [binary:467369,476096] -hskp41(0) | -c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 476102 [binary:476047,476098,factor:factor] -c2_1(X) | c3_1(X) | c1_1(X) | c0_1(X).
% 476114 [binary:470588,476102] c3_1(X) | c1_1(X) | c0_1(X).
% 476117 [binary:467360,476114,binarycut:467359] -hskp56(0) | c0_1(a2242).
% 476121 [binary:467401,476114,binarycut:467400,binarycut:467399] -hskp19(0).
% 476125 [binary:467414,476114,binarycut:467413] -hskp12(0) | c0_1(a2211).
% 476127 [binary:467427,476114,binarycut:467428,binarycut:467426] -hskp6(0).
% 476141 [binary:468589,476114] c1_1(a2190) | c0_1(a2190) | -c2_1(X) | -c2_1(Y) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 476147 [binary:467994,476114,factor] -c2_1(a2190) | c1_1(a2190) | c0_1(a2190) | hskp11(0) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 476192 [binary:467823,476121] hskp52(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 476193 [binary:467295,476127] hskp34(0) | hskp37(0).
% 476197 [binary:467751,476117] c0_1(a2242) | -c2_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 476222 [binary:467276,476192] c2_1(a2234) | -c2_1(X) | c3_1(X) | c0_1(X).
% 476223 [binary:467277,476192] c3_1(a2234) | -c2_1(X) | c3_1(X) | c0_1(X).
% 476241 [binary:467731,476222,factor] -c3_1(a2234) | -c0_1(a2234) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c0_1(Y) | c0_1(X).
% 476486 [binary:476223,476241,factor] -c0_1(a2234) | -c2_1(X) | -c3_1(Y) | -c1_1(Y) | c3_1(X) | c0_1(Y) | c0_1(X).
% 476521 [binary:467767,476147] c1_1(a2190) | c0_1(a2190) | hskp11(0) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 476524 [binary:467433,476521,binarycut:467434] -hskp3(0) | hskp11(0) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 476526 [binary:467294,476524] hskp11(0) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 476528 [binary:467209,476526] c0_1(a2209) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 476754 [binary:467433,476141,binarycut:467434] -hskp3(0) | -c2_1(Y) | -c2_1(X) | -c3_1(X) | -c0_1(Y) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 476759 [binary:467754,476754,factor:factor:factor] -c2_1(Y) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c3_1(X) | c1_1(Y) | c1_1(X).
% 476783 [binary:468007,476759,factor:factor:factor:factor] -c3_1(a2204) | c1_1(a2204) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 476901 [binary:468005,476783,factor:factor:factor:factor:factor] c1_1(a2204) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 476904 [binary:467370,476901] -hskp40(0) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(X) | c1_1(Y).
% 476922 [binary:467760,476904,factor:factor] -c2_1(X) | -c3_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y) | c1_1(X).
% 476936 [binary:467928,476922,factor:factor:factor:factor:factor] -c0_1(a2242) | c3_1(a2242) | c1_1(a2242) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 477641 [binary:476197,476936,factor:factor:factor:factor:factor:factor] c3_1(a2242) | c1_1(a2242) | -c2_1(X) | -c3_1(Y) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 477644 [binary:467360,477641,binarycut:467359] -hskp56(0) | -c2_1(X) | -c3_1(Y) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c1_1(Y) | c1_1(X).
% 477696 [binary:467751,477644,factor:factor:factor] -c2_1(X) | -c3_1(Y) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c1_1(X) | c1_1(Y).
% 477708 [binary:467890,477696,factor:factor:factor] -c0_1(a2204) | c1_1(a2204) | -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 477722 [binary:468007,477696,factor:factor:factor:factor] -c0_1(a2204) | c1_1(a2204) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 477744 [binary:468895,477708,factor:factor:factor:factor] c1_1(a2204) | -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 477747 [binary:467370,477744] -hskp40(0) | -c2_1(X) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 477775 [binary:467745,477747,factor:factor] -c2_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 477787 [binary:467912,477775,factor:factor:factor:factor:factor:factor] -c3_1(a2215) | c0_1(a2215) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 477808 [binary:476222,477775] -c3_1(a2234) | c0_1(a2234) | -c2_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X).
% 477838 [binary:476223,477808,factor:factor] c0_1(a2234) | -c2_1(X) | -c3_1(Y) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X).
% 477841 [binary:476486,477838,factor] -c2_1(X) | -c3_1(Z) | -c3_1(Y) | -c1_1(Y) | -c0_1(Z) | c2_1(Z) | c3_1(X) | c1_1(Z) | c0_1(Y) | c0_1(X).
% 477871 [binary:468764,477722,factor:factor:factor:factor:factor] c1_1(a2204) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 477874 [binary:467370,477871] -hskp40(0) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 477916 [binary:467760,477874,factor:factor] -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 477924 [binary:467839,477916,factor:factor:factor] -c0_1(a2191) | c2_1(a2191) | c1_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 477970 [binary:472143,477924,factor:factor:factor] c2_1(a2191) | c1_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 477973 [binary:467431,477970,binarycut:467432] -hskp4(0) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 477976 [binary:467838,477973,factor] hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 477978 [binary:467213,477976] c2_1(a2213) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 478023 [binary:472117,477978,factor:factor] c1_1(a2213) | c0_1(a2213) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 478035 [binary:467410,478023,binarycut:467411] -hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 478038 [binary:477976,478035,factor] -c0_1(X) | c2_1(X) | c3_1(X) | c1_1(X).
% 478067 [binary:467801,478038] c2_1(a2252) | c3_1(a2252) | c1_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 478068 [binary:467814,478038] c2_1(a2244) | c3_1(a2244) | c1_1(a2244) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 478079 [binary:470610,478038] c2_1(a2220) | c3_1(a2220) | c1_1(a2220) | hskp17(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 478082 [binary:476528,478038] c2_1(a2209) | c3_1(a2209) | c1_1(a2209) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 478109 [binary:467357,478067,binarycut:467358] -hskp58(0) | c3_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 478144 [binary:467800,478109,factor] c3_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 478147 [binary:477916,478144] -c0_1(a2252) | c2_1(a2252) | c1_1(a2252) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 478151 [binary:467405,478079,binarycut:467407,binarycut:467406] -hskp16(0) | hskp17(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 478157 [binary:467837,478151,factor] hskp17(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 478159 [binary:467215,478157] c2_1(a2221) | -c2_1(X) | c1_1(X) | c0_1(X).
% 478223 [binary:467416,478082,binarycut:467415] -hskp11(0) | c3_1(a2209) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 478252 [binary:476526,478223,factor] c3_1(a2209) | hskp12(0) | -c0_1(X) | c2_1(X) | c1_1(X).
% 478264 [binary:467394,478068,binarycut:467395] -hskp22(0) | c3_1(a2244) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 478273 [binary:467813,478264,factor:factor] c3_1(a2244) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 478724 [binary:467801,478147,factor:factor:factor] c2_1(a2252) | c1_1(a2252) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(Y) | c1_1(X).
% 478727 [binary:467357,478724,binarycut:467358] -hskp58(0) | -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 478743 [binary:467800,478727,factor] -c3_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 478748 [binary:467839,478743] c2_1(a2191) | c1_1(a2191) | hskp14(0) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X).
% 479221 [binary:467431,478748,binarycut:467432] -hskp4(0) | hskp14(0) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y).
% 479249 [binary:467838,479221,factor] hskp14(0) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y).
% 479252 [binary:467213,479249] c2_1(a2213) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X).
% 479282 [binary:468572,479252,factor:factor:factor] -c3_1(a2213) | c1_1(a2213) | c0_1(a2213) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c3_1(Y) | c3_1(X) | c1_1(X).
% 480272 [binary:476114,479282] c1_1(a2213) | c0_1(a2213) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X) | c1_1(Y).
% 480275 [binary:467410,480272,binarycut:467411] -hskp14(0) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c3_1(X) | c3_1(Y) | c1_1(X).
% 480281 [binary:479249,480275,factor:factor:factor:factor] -c0_1(Y) | -c0_1(X) | c2_1(X) | c3_1(X) | c3_1(Y) | c1_1(Y).
% 480470 [binary:467912,477841,factor:factor:factor:factor:factor] c3_1(a2215) | c0_1(a2215) | -c3_1(X) | -c3_1(Y) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 480497 [binary:477787,480470,factor:factor] c0_1(a2215) | -c3_1(Y) | -c3_1(X) | -c1_1(Y) | -c0_1(X) | c2_1(X) | c1_1(X) | c0_1(Y).
% 480500 [binary:467366,480497] -hskp44(0) | -c3_1(Y) | -c3_1(X) | -c1_1(Y) | -c0_1(X) | c2_1(X) | c1_1(X) | c0_1(Y).
% 480513 [binary:467749,480500,factor:factor:factor:factor] -c3_1(Y) | -c3_1(X) | -c1_1(X) | -c0_1(Y) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 480531 [binary:478144,480513] -c0_1(a2252) | c2_1(a2252) | c1_1(a2252) | -c3_1(Y) | -c3_1(X) | -c1_1(X) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 480629 [binary:467801,480531,factor:factor:factor:factor] c2_1(a2252) | c1_1(a2252) | -c3_1(X) | -c3_1(Y) | -c1_1(Y) | c2_1(X) | c1_1(X) | c0_1(Y).
% 480632 [binary:467357,480629,binarycut:467358] -hskp58(0) | -c3_1(X) | -c3_1(Y) | -c1_1(X) | c2_1(Y) | c1_1(Y) | c0_1(X).
% 480655 [binary:467800,480632,factor:factor] -c3_1(Y) | -c3_1(X) | -c1_1(Y) | c2_1(X) | c1_1(X) | c0_1(Y).
% 480659 [binary:467784,480655,factor] -c1_1(a2189) | c0_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480727 [binary:467785,480659,factor] c0_1(a2189) | hskp46(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480729 [binary:467378,480727] -hskp34(0) | hskp46(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480732 [binary:467783,480729,factor] hskp46(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480734 [binary:467263,480732] c2_1(a2218) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480736 [binary:467264,480732] c0_1(a2218) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480742 [binary:467735,480734,factor:factor] -c1_1(a2218) | -c0_1(a2218) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 480753 [binary:477696,480734,factor:factor:factor] -c0_1(a2218) | c1_1(a2218) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480762 [binary:480736,480753,factor:factor] c1_1(a2218) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 480992 [binary:480762,480742,factor:factor] -c0_1(a2218) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 480995 [binary:480736,480992,factor] -c3_1(X) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 481022 [binary:478252,480995,factor] -c0_1(a2209) | c2_1(a2209) | c1_1(a2209) | hskp12(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 481048 [binary:476528,481022] c2_1(a2209) | c1_1(a2209) | hskp12(0) | -c0_1(Y) | -c0_1(X) | c2_1(Y) | c2_1(X) | c3_1(X) | c1_1(Y).
% 481239 [binary:467416,481048,binarycut:467415] -hskp11(0) | hskp12(0) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 481252 [binary:476526,481239,factor] hskp12(0) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c1_1(X).
% 481259 [binary:476125,481252] c0_1(a2211) | -c0_1(X) | -c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(X) | c1_1(Y).
% 481309 [binary:480281,481259,factor:factor:factor] c3_1(a2211) | c1_1(a2211) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c1_1(Y).
% 481315 [binary:467414,481309,binarycut:467413] -hskp12(0) | -c0_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 481334 [binary:481252,481315,factor:factor:factor] -c0_1(Y) | -c0_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c1_1(X).
% 481351 [binary:467987,481334,factor:factor:factor:factor:factor] c2_1(a2186) | c3_1(a2186) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 481379 [binary:467382,481351,binarycut:467381] -hskp32(0) | -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 481385 [binary:467757,481379,factor:factor] -c3_1(X) | -c0_1(X) | c2_1(X) | c1_1(X).
% 481387 [binary:467808,481385] -c0_1(a2222) | c2_1(a2222) | c1_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 481397 [binary:478144,481385] -c0_1(a2252) | c2_1(a2252) | c1_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 481411 [binary:467810,481387,factor:factor] c2_1(a2222) | c1_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 481413 [binary:467402,481411] -hskp18(0) | c1_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 481421 [binary:467807,481413,factor] c1_1(a2222) | -c1_1(X) | c2_1(X) | c3_1(X).
% 481439 [binary:467801,481397,factor:factor:factor] c2_1(a2252) | c1_1(a2252) | -c3_1(X) | c2_1(X) | c1_1(X).
% 481442 [binary:467357,481439,binarycut:467358] -hskp58(0) | -c3_1(X) | c2_1(X) | c1_1(X).
% 481454 [binary:467800,481442,factor] -c3_1(X) | c2_1(X) | c1_1(X).
% 481459 [binary:467839,481454] c2_1(a2191) | c1_1(a2191) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 481470 [binary:476114,481454] c2_1(X) | c1_1(X) | c0_1(X).
% 481471 [binary:478273,481454] c2_1(a2244) | c1_1(a2244) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481482 [binary:467440,481470,binarycut:467439,binarycut:467438] -hskp0(0).
% 481489 [binary:467738,481470,factor:factor] -c2_1(Y) | -c2_1(X) | -c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(X) | c0_1(Y).
% 481496 [binary:467796,481482] -c2_1(X) | -c1_1(X) | -c0_1(X).
% 481510 [binary:467771,481496] -c1_1(a2231) | -c0_1(a2231) | hskp51(0) | -c2_1(X) | -c1_1(X) | c0_1(X).
% 481764 [binary:467431,481459,binarycut:467432] -hskp4(0) | hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 481770 [binary:467838,481764,factor] hskp14(0) | -c0_1(X) | c2_1(X) | c3_1(X).
% 481790 [binary:467394,481471,binarycut:467395] -hskp22(0) | hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481800 [binary:467813,481790,factor] hskp57(0) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481803 [binary:467770,481510,factor] -c0_1(a2231) | hskp51(0) | -c2_1(X) | -c1_1(X) | c0_1(X).
% 481805 [binary:467289,481800] c3_1(a2243) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481807 [binary:467290,481800] c0_1(a2243) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481809 [binary:467291,481800] c1_1(a2243) | -c1_1(X) | c3_1(X) | c0_1(X).
% 481878 [binary:481470,481489] -c2_1(X) | -c3_1(Y) | c3_1(X) | c1_1(Y) | c0_1(Y) | c0_1(X).
% 481903 [binary:478159,481878,factor:factor] c3_1(a2221) | c0_1(a2221) | -c2_1(X) | -c3_1(X) | c1_1(X) | c0_1(X).
% 481914 [binary:467404,481903,binarycut:467403] -hskp17(0) | -c2_1(X) | -c3_1(X) | c1_1(X) | c0_1(X).
% 481918 [binary:478157,481914,factor] -c2_1(X) | -c3_1(X) | c1_1(X) | c0_1(X).
% 481927 [binary:481470,481918] -c3_1(X) | c1_1(X) | c0_1(X).
% 481934 [binary:476114,481927] c1_1(X) | c0_1(X).
% 481940 [binary:467410,481934,binarycut:467411] -hskp14(0).
% 481942 [binary:467433,481934,binarycut:467434] -hskp3(0).
% 481951 [binary:481770,481940] -c0_1(X) | c2_1(X) | c3_1(X).
% 481952 [binary:467294,481942] hskp11(0) | hskp12(0).
% 481953 [binary:467754,481942] -c2_1(Y) | -c2_1(X) | -c3_1(X) | c3_1(Y) | c1_1(X) | c1_1(Y).
% 481962 [binary:467209,481952] c0_1(a2209) | hskp12(0).
% 481976 [binary:481962,481951] c2_1(a2209) | c3_1(a2209) | hskp12(0).
% 481984 [binary:467416,481976,binarycut:481952] c3_1(a2209) | hskp12(0).
% 481988 [binary:481454,481984] c2_1(a2209) | c1_1(a2209) | hskp12(0).
% 481997 [binary:467416,481988,binarycut:481952] c1_1(a2209) | hskp12(0).
% 482000 [binary:467415,481997,binarycut:481952] hskp12(0).
% 482001 [binary:467210,482000] c2_1(a2211).
% 482002 [binary:476125,482000] c0_1(a2211).
% 482009 [binary:481496,482001,cut:482002] -c1_1(a2211).
% 482055 [binary:482001,481953,cut:482009] c3_1(a2211) | -c2_1(X) | -c3_1(X) | c1_1(X).
% 482058 [binary:467414,482055,cut:482000] -c2_1(X) | -c3_1(X) | c1_1(X).
% 482147 [binary:467934,481421,factor:factor:factor:binarycut:481934] c2_1(a2222) | -c1_1(X) | -c0_1(X) | c2_1(X) | c2_1(Y) | c3_1(Y) | c0_1(Y).
% 482168 [binary:481496,482147,factor] -c1_1(a2222) | -c0_1(a2222) | c2_1(a2222) | c2_1(X) | c3_1(X) | c0_1(X).
% 482174 [binary:481421,482168,factor:factor:binarycut:481934] -c0_1(a2222) | c2_1(a2222) | c2_1(X) | c3_1(X) | c0_1(X).
% 482185 [binary:467810,482174,factor:factor:binarycut:481934] c2_1(a2222) | c2_1(X) | c3_1(X) | c0_1(X).
% 482188 [binary:467402,482185] -hskp18(0) | c2_1(X) | c3_1(X) | c0_1(X).
% 482207 [binary:467807,482188,factor:binarycut:481934] c2_1(X) | c3_1(X) | c0_1(X).
% 482214 [binary:467417,482207,binarycut:467419,binarycut:467418] -hskp10(0).
% 482224 [binary:467746,482214] -c3_1(Y) | -c3_1(X) | -c1_1(X) | -c0_1(Y) | c2_1(X) | c2_1(Y).
% 482292 [binary:481805,482224,binarycut:481934] -c0_1(a2243) | c2_1(a2243) | -c3_1(X) | -c1_1(X) | c2_1(X) | c3_1(Y) | c0_1(Y).
% 482397 [binary:481807,482292,binarycut:481934,factor] c2_1(a2243) | -c3_1(X) | -c1_1(X) | c2_1(X) | c3_1(Y) | c0_1(Y).
% 482415 [binary:481496,482397,factor] -c3_1(a2243) | -c1_1(a2243) | -c0_1(a2243) | c2_1(a2243) | c3_1(X) | c0_1(X).
% 482420 [binary:481805,482415,binarycut:481934,factor] -c1_1(a2243) | -c0_1(a2243) | c2_1(a2243) | c3_1(X) | c0_1(X).
% 482435 [binary:481809,482420,binarycut:481934,factor] -c0_1(a2243) | c2_1(a2243) | c3_1(X) | c0_1(X).
% 482439 [binary:481807,482435,binarycut:481934,factor] c2_1(a2243) | c3_1(X) | c0_1(X).
% 482444 [binary:481496,482439] -c1_1(a2243) | -c0_1(a2243) | c3_1(X) | c0_1(X).
% 482449 [binary:481809,482444,binarycut:481934,factor] -c0_1(a2243) | c3_1(X) | c0_1(X).
% 482453 [binary:481807,482449,binarycut:481934,factor] c3_1(X) | c0_1(X).
% 482455 [binary:467361,482453] -hskp50(0) | c0_1(a2231).
% 482459 [binary:467397,482453,binarycut:467396] -hskp21(0).
% 482474 [binary:467293,482459] hskp54(0) | hskp55(0).
% 482479 [binary:467769,482455,binarycut:481934] c0_1(a2231) | hskp51(0) | -c2_1(X) | c0_1(X).
% 482482 [binary:467282,482474] c0_1(a2240) | hskp55(0).
% 482484 [binary:467284,482474] c1_1(a2240) | hskp55(0).
% 482523 [binary:481803,482479,binarycut:481934,factor] hskp51(0) | -c2_1(X) | c0_1(X).
% 482525 [binary:467273,482523] c2_1(a2232) | -c2_1(X) | c0_1(X).
% 482526 [binary:467274,482523] c3_1(a2232) | -c2_1(X) | c0_1(X).
% 482527 [binary:467275,482523] c0_1(a2232) | -c2_1(X) | c0_1(X).
% 482533 [binary:481496,482525] -c1_1(a2232) | -c0_1(a2232) | -c2_1(X) | c0_1(X).
% 482534 [binary:482058,482525] -c3_1(a2232) | c1_1(a2232) | -c2_1(X) | c0_1(X).
% 482541 [binary:482526,482534,factor] c1_1(a2232) | -c2_1(X) | c0_1(X).
% 482544 [binary:482533,482541,factor] -c0_1(a2232) | -c2_1(X) | c0_1(X).
% 482547 [binary:482527,482544,factor] -c2_1(X) | c0_1(X).
% 482575 [binary:467734,482453,binarycut:481934,binarycut:481934,factor:binarycut:482547] -c1_1(X) | -c0_1(X) | c2_1(X) | c0_1(Y).
% 482588 [binary:482484,482575,binarycut:482482] c2_1(a2240) | hskp55(0) | c0_1(X).
% 482595 [binary:481496,482588,binarycut:482484,binarycut:482482] hskp55(0) | c0_1(X).
% 482597 [binary:467285,482595] c2_1(a2241) | c0_1(X).
% 482599 [binary:467286,482595,factor] c0_1(a2241).
% 482600 [binary:467287,482595] c1_1(a2241) | c0_1(X).
% 482607 [binary:481496,482597,cut:482599,binarycut:482600] c0_1(X).
% 482612 [binary:467375,482607] -hskp37(0).
% 482614 [binary:467378,482607] -hskp34(0).
% 482624 [binary:476193,482614,cut:482612] 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: 25416
% derived clauses: 1239909
% kept clauses: 269525
% kept size sum: 897452
% kept mid-nuclei: 93832
% kept new demods: 0
% forw unit-subs: 16
% forw double-subs: 85073
% forw overdouble-subs: 592547
% backward subs: 7782
% fast unit cutoff: 18190
% full unit cutoff: 0
% dbl unit cutoff: 21509
% real runtime: 264.57
% process. runtime: 262.77
% specific non-discr-tree subsumption statistics:
% tried: 107720366
% length fails: 329493
% strength fails: 41065458
% predlist fails: 47077292
% aux str. fails: 1505243
% by-lit fails: 13393588
% full subs tried: 1804275
% full subs fail: 1721626
%
% ; 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/SYN460-1+noeq.in")
%
%------------------------------------------------------------------------------