↑ Up

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

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Gandalf---c-2.6
% Problem  : SYN502-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 : art09.cs.miami.edu
% Model    : i686 unknown
% CPU      : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory   : 1000MB
% OS       : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s

% Result   : Unsatisfiable 249.1s
% Output   : Assurance 249.1s
% 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/SYN502-1+noeq.in
% Using automatic strategy selection.
% Time limit in seconds: 600
% 
% prove-all-passes started
% 
% detected problem class: nne
% detected subclass: big
% 
% strategies selected: 
% (hyper 30 #f 1 19)
% (binary-unit 30 #f 1 19)
% (binary-double 18 #f 1 19)
% (binary 90 #t 1 19)
% (binary-order 30 #f 1 19)
% (binary-posweight-order 54 #f)
% (binary-order-sos 30 #t)
% (binary-unit-uniteq 30 #f)
% (binary-weightorder 30 #f)
% (binary-weightorder-sos 30 #f)
% (binary-order 30 #f)
% (hyper-order 30 #f)
% (binary 168 #t)
% 
% 
% ********* EMPTY CLAUSE DERIVED *********
% 
% 
% timer checkpoints: c(206,40,1,412,0,1,109329,4,2446,131011,1,3002,131011,50,3002,131011,40,3002,131217,0,3002,131451,50,3003,131657,0,3005,131891,50,3006,132097,0,3006,132331,50,3006,132537,0,3008,132771,50,3008,132977,0,3010,133211,50,3011,133417,0,3011,133651,50,3011,133857,0,3013,134091,50,3013,134297,0,3015,134531,50,3016,134737,0,3016,134971,50,3016,135177,0,3018,135411,50,3018,135617,0,3020,135851,50,3021,136057,0,3021,136291,50,3021,136497,0,3023,136731,50,3023,136937,0,3025,137171,50,3026,137377,0,3026,137611,50,3026,137817,0,3028,138051,50,3029,138257,0,3030,138491,50,3031,138697,0,3031,138931,50,3032,139137,0,3033,139371,50,3034,139577,0,3035,139811,50,3036,140017,0,3036,140251,50,3037,140251,40,3037,140457,0,3038,156817,3,3939,158765,4,4389,161829,5,4839,161830,1,4839,161830,50,4839,161830,40,4839,162036,0,4839,253754,3,9347,254559,4,11591,255350,1,13840,255350,50,13843,255350,40,13843,255556,0,13843,297082,3,15344,297861,4,16094,299090,5,16844,299091,1,16844,299091,50,16845,299091,40,16845,299297,0,16845,362993,3,19546,363892,4,20896,364869,5,22246,364870,1,22246,364870,50,22248,364870,40,22248,365076,0,22248,414333,3,23949,414839,4,24499,415945,5,25249,415946,1,25249,415946,50,25250,415946,40,25250,416152,0,25251,416372,50,25251,416372,40,25251,416578,0,25257)
% 
% 
% START OF PROOF
% 416373 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | -c0_1(X) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 416374 [] -ndr1_0(0) | -c3_1(Y) | -c3_1(X) | -c0_1(Z) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(X).
% 416375 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | -c0_1(X) | c1_1(Z) | c2_1(Z) | c0_1(Z) | c0_1(Y).
% 416376 [] -ndr1_0(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Z) | -c2_1(X) | c1_1(Z) | c3_1(Y) | c3_1(X) | c2_1(Z) | c2_1(Y).
% 416377 [] -ndr1_0(0) | -c1_1(Z) | -c1_1(Y) | -c1_1(X) | -c3_1(X) | c3_1(Z) | c2_1(Y) | c2_1(X) | c0_1(Y) | c0_1(Z).
% 416378 [] -ndr1_0(0) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Z) | c1_1(Y) | c1_1(X) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 416379 [] -ndr1_0(0) | -c3_1(Y) | -c3_1(X) | -c0_1(X) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c2_1(X) | c0_1(Z) | c0_1(Y).
% 416387 [] -ndr1_0(0) | hskp5(0) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c3_1(X) | c3_1(Y).
% 416388 [] -ndr1_0(0) | hskp25(0) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y).
% 416390 [] -ndr1_0(0) | hskp29(0) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X).
% 416391 [?] ?
% 416392 [?] ?
% 416393 [?] ?
% 416394 [?] ?
% 416400 [?] ?
% 416402 [?] ?
% 416404 [?] ?
% 416409 [?] ?
% 416411 [?] ?
% 416412 [?] ?
% 416416 [?] ?
% 416417 [?] ?
% 416419 [?] ?
% 416420 [?] ?
% 416430 [?] ?
% 416433 [?] ?
% 416434 [?] ?
% 416436 [?] ?
% 416438 [?] ?
% 416442 [] -hskp2(0) | c3_1(a236).
% 416443 [] -hskp2(0) | c1_1(a236).
% 416445 [] -hskp4(0) | c3_1(a239).
% 416446 [] -hskp5(0) | c3_1(a241).
% 416447 [] -hskp5(0) | c2_1(a241).
% 416448 [] -hskp6(0) | c2_1(a242).
% 416449 [] -hskp7(0) | c0_1(a244).
% 416451 [] -hskp8(0) | c0_1(a245).
% 416452 [] -hskp9(0) | c3_1(a248).
% 416453 [] -hskp10(0) | c3_1(a249).
% 416454 [] -hskp10(0) | c0_1(a249).
% 416456 [] -hskp12(0) | c0_1(a252).
% 416457 [] -hskp13(0) | c1_1(a253).
% 416458 [] -hskp14(0) | c3_1(a257).
% 416459 [] -hskp14(0) | c2_1(a257).
% 416460 [] -hskp16(0) | c1_1(a259).
% 416461 [] -hskp18(0) | c2_1(a265).
% 416462 [] -hskp18(0) | c1_1(a265).
% 416463 [] -hskp19(0) | c3_1(a269).
% 416464 [] -hskp19(0) | c0_1(a269).
% 416471 [] -hskp23(0) | c3_1(a281).
% 416472 [] -hskp23(0) | c1_1(a281).
% 416473 [] -hskp24(0) | c3_1(a282).
% 416474 [] -hskp25(0) | c2_1(a294).
% 416475 [] -hskp25(0) | c1_1(a294).
% 416477 [] -hskp28(0) | c2_1(a237).
% 416478 [] -hskp28(0) | c1_1(a237).
% 416479 [] -hskp28(0) | c0_1(a237).
% 416480 [] -hskp29(0) | c3_1(a240).
% 416481 [] -hskp29(0) | c2_1(a240).
% 416482 [] -hskp29(0) | c1_1(a240).
% 416486 [] -hskp31(0) | c3_1(a246).
% 416488 [] -hskp31(0) | c0_1(a246).
% 416489 [] hskp5(0) | hskp9(0) | hskp11(0).
% 416490 [] hskp13(0) | hskp23(0) | hskp24(0).
% 416495 [] hskp7(0) | hskp8(0) | hskp15(0).
% 416504 [] -hskp5(0) | ndr1_0(0).
% 416508 [] -hskp9(0) | ndr1_0(0).
% 416510 [] -hskp11(0) | ndr1_0(0).
% 416531 [] -c1_1(a322) | -hskp27(0).
% 416532 [] -c2_1(a322) | -hskp27(0).
% 416533 [] -c3_1(a322) | -hskp27(0).
% 416536 [] -c3_1(a294) | -hskp25(0).
% 416537 [] -c0_1(a282) | -hskp24(0).
% 416538 [] -c2_1(a282) | -hskp24(0).
% 416539 [] -c2_1(a281) | -hskp23(0).
% 416543 [] -c1_1(a269) | -hskp19(0).
% 416544 [] -c0_1(a265) | -hskp18(0).
% 416545 [] -c0_1(a263) | -hskp17(0).
% 416546 [] -c1_1(a263) | -hskp17(0).
% 416547 [] -c3_1(a263) | -hskp17(0).
% 416548 [] -c2_1(a259) | -hskp16(0).
% 416549 [] -c3_1(a259) | -hskp16(0).
% 416550 [] -c0_1(a258) | -hskp15(0).
% 416551 [] -c2_1(a258) | -hskp15(0).
% 416552 [] -c3_1(a258) | -hskp15(0).
% 416553 [] -c1_1(a257) | -hskp14(0).
% 416554 [] -c0_1(a253) | -hskp13(0).
% 416555 [] -c3_1(a253) | -hskp13(0).
% 416556 [] -c1_1(a252) | -hskp12(0).
% 416557 [] -c3_1(a252) | -hskp12(0).
% 416558 [] -c1_1(a251) | -hskp11(0).
% 416559 [] -c3_1(a251) | -hskp11(0).
% 416560 [] -c2_1(a249) | -hskp10(0).
% 416561 [] -c0_1(a248) | -hskp9(0).
% 416563 [] -c1_1(a245) | -hskp8(0).
% 416564 [] -c1_1(a244) | -hskp7(0).
% 416565 [] -c2_1(a244) | -hskp7(0).
% 416566 [] -c0_1(a242) | -hskp6(0).
% 416567 [] -c1_1(a242) | -hskp6(0).
% 416568 [] -c0_1(a241) | -hskp5(0).
% 416569 [] -c1_1(a239) | -hskp4(0).
% 416570 [] -c2_1(a239) | -hskp4(0).
% 416571 [] -c2_1(a238) | -hskp3(0).
% 416572 [] -c3_1(a238) | -hskp3(0).
% 416573 [] -c0_1(a236) | -hskp2(0).
% 416740 [binary:416446,416489] c3_1(a241) | hskp9(0) | hskp11(0).
% 416743 [binary:416504,416489,binarycut:416508,binarycut:416510] ndr1_0(0).
% 416744 [binary:416373,416743] -c1_1(X) | -c1_1(Y) | -c3_1(X) | -c3_1(Y) | -c0_1(Z) | -c0_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(X).
% 416745 [binary:416374,416743] -c3_1(X) | -c3_1(Y) | -c0_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Y).
% 416746 [binary:416375,416743] -c1_1(X) | -c1_1(Y) | -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Z) | c2_1(Z) | c0_1(Z) | c0_1(X).
% 416747 [binary:416376,416743] -c1_1(X) | -c1_1(Y) | -c3_1(Z) | -c2_1(Y) | c1_1(Z) | c3_1(Y) | c3_1(X) | c2_1(Z) | c2_1(X).
% 416748 [binary:416377,416743] -c1_1(Y) | -c1_1(Z) | -c1_1(X) | -c3_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Z).
% 416749 [binary:416378,416743] -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c1_1(Z) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 416750 [binary:416379,416743] -c3_1(X) | -c3_1(Y) | -c0_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c0_1(Z) | c0_1(X).
% 416758 [binary:416387,416743] hskp5(0) | -c2_1(X) | -c2_1(Y) | -c0_1(Y) | c1_1(X) | c3_1(X) | c3_1(Y).
% 416759 [binary:416388,416743] hskp25(0) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 416761 [binary:416390,416743] hskp29(0) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | c1_1(Y) | c2_1(Y) | c2_1(X).
% 416763 [binary:416457,416490] c1_1(a253) | hskp23(0) | hskp24(0).
% 416764 [input:416391,cut:416743] hskp4(0) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 416779 [binary:416449,416495] c0_1(a244) | hskp8(0) | hskp15(0).
% 416780 [input:416392,cut:416743] hskp10(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c0_1(Y) | c0_1(X).
% 416781 [binary:416453,416780] c3_1(a249) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c0_1(X) | c0_1(Y).
% 416783 [binary:416454,416780] c0_1(a249) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c0_1(X) | c0_1(Y).
% 416792 [input:416393,cut:416743] hskp16(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 416793 [binary:416460,416792] c1_1(a259) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 416798 [input:416394,cut:416743] hskp15(0) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c2_1(X) | c0_1(X).
% 416824 [input:416412,cut:416743] hskp4(0) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 416825 [binary:416445,416824] c3_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 416827 [input:416436,cut:416743] hskp29(0) | -c0_1(X) | c1_1(X) | c3_1(X).
% 416828 [binary:416480,416827] c3_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X).
% 416830 [binary:416481,416827] c2_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X).
% 416831 [binary:416482,416827] c1_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X).
% 416844 [input:416438,cut:416743] hskp10(0) | -c2_1(X) | c1_1(X) | c0_1(X).
% 416845 [binary:416453,416844] c3_1(a249) | -c2_1(X) | c1_1(X) | c0_1(X).
% 416846 [binary:416454,416844] c0_1(a249) | -c2_1(X) | c1_1(X) | c0_1(X).
% 416862 [input:416400,cut:416743] hskp18(0) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c2_1(Y) | c2_1(X).
% 416863 [binary:416461,416862] c2_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 416867 [binary:416462,416862] c1_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 416878 [input:416411,cut:416743] hskp24(0) | hskp27(0) | -c1_1(X) | -c3_1(X) | -c2_1(X).
% 416880 [input:416402,cut:416743] hskp14(0) | -c1_1(X) | -c1_1(Y) | c3_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 416881 [binary:416458,416880] c3_1(a257) | -c1_1(X) | -c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 416882 [binary:416458,416880,factor] -c1_1(a257) | c3_1(a257) | c0_1(a257) | -c1_1(X) | c2_1(X) | c0_1(X).
% 416883 [binary:416459,416880] c2_1(a257) | -c1_1(X) | -c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 416905 [input:416404,cut:416743] hskp2(0) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 416906 [binary:416442,416905] c3_1(a236) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 416907 [binary:416443,416905] c1_1(a236) | -c1_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 416910 [input:416416,cut:416743] hskp3(0) | hskp12(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 416913 [input:416417,cut:416743] hskp5(0) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 416914 [binary:416446,416913] c3_1(a241) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 416915 [binary:416447,416913] c2_1(a241) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 416926 [input:416419,cut:416743] hskp23(0) | hskp24(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 416927 [binary:416471,416926] c3_1(a281) | hskp24(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 416928 [binary:416472,416926] c1_1(a281) | hskp24(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 416935 [input:416420,cut:416743] hskp17(0) | hskp19(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 416958 [input:416409,cut:416743] hskp6(0) | c1_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 416959 [binary:416448,416958] c2_1(a242) | c1_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 416993 [input:416430,cut:416743] hskp4(0) | hskp28(0) | -c2_1(X) | c3_1(X) | c0_1(X).
% 416995 [binary:416445,416993,factor] -c2_1(a239) | c3_1(a239) | c0_1(a239) | hskp28(0).
% 417004 [input:416433,cut:416743] hskp14(0) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 417005 [binary:416458,417004] c3_1(a257) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 417007 [binary:416459,417004,factor] -c3_1(a257) | c2_1(a257) | c0_1(a257) | hskp31(0).
% 417010 [input:416434,cut:416743] hskp12(0) | hskp13(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 417011 [binary:416456,417010] c0_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 417051 [binary:416845,416745] -c0_1(a249) | c1_1(a249) | -c3_1(X) | -c2_1(Y) | -c0_1(Z) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Z) | c2_1(X) | c0_1(Y).
% 417120 [binary:416928,416748] -c3_1(a281) | c2_1(a281) | hskp24(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Z) | -c2_1(Z) | c3_1(X) | c2_1(Y) | c0_1(Z) | c0_1(X) | c0_1(Y).
% 417158 [binary:416825,416749] -c0_1(a239) | c1_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y).
% 417159 [binary:416845,416749] -c0_1(a249) | c1_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Z) | c2_1(Y) | c0_1(X).
% 417254 [binary:416446,416758] c3_1(a241) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y).
% 417258 [binary:416447,416758] c2_1(a241) | -c2_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y).
% 417263 [binary:416474,416759] c2_1(a294) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 417264 [binary:416475,416759] c1_1(a294) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y).
% 417275 [binary:416480,416761] c3_1(a240) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 417276 [binary:416481,416761] c2_1(a240) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 417279 [binary:416482,416761] c1_1(a240) | -c1_1(X) | -c3_1(X) | -c3_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 417308 [binary:416747,416793,factor:factor:factor:factor:factor:factor] c3_1(a259) | c2_1(a259) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 417384 [binary:416746,416907,factor:factor:factor:factor:factor:factor] -c3_1(a236) | c0_1(a236) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 417576 [binary:416549,417308,binarycut:416548] -hskp16(0) | -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 417588 [binary:416792,417576,factor:factor] -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 417599 [binary:416867,417588,factor] -c2_1(a265) | c3_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c2_1(X) | c2_1(Y) | c0_1(X).
% 417608 [binary:417264,417588] -c2_1(a294) | c3_1(a294) | -c3_1(Y) | -c3_1(X) | -c2_1(Z) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c2_1(X) | c0_1(X).
% 417631 [binary:416906,417384,factor:factor:factor:factor] c0_1(a236) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 417633 [binary:416573,417631] -hskp2(0) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 417640 [binary:416905,417633,factor:factor] -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 417670 [binary:416846,417051,factor:factor] c1_1(a249) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | -c0_1(Z) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(X) | c0_1(Y).
% 417695 [binary:416863,417599,factor:factor] c3_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c2_1(Y) | c2_1(X) | c0_1(X).
% 417768 [binary:416744,417670,factor:factor:factor:factor:factor:factor:factor:factor:factor] -c1_1(a249) | -c3_1(a249) | -c0_1(a249) | c2_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 418328 [binary:416927,417120,factor] c2_1(a281) | hskp24(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Z) | -c2_1(Z) | c3_1(Y) | c2_1(X) | c0_1(X) | c0_1(Z) | c0_1(Y).
% 418413 [binary:416846,417159,factor:factor] c1_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(X).
% 418430 [binary:417640,418413,factor:factor:factor:factor:factor] -c3_1(a249) | -c0_1(a249) | c1_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 418833 [binary:416539,418328] -hskp23(0) | hskp24(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Z) | -c2_1(Z) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Z) | c0_1(Y).
% 418953 [binary:416926,418833,factor] hskp24(0) | -c1_1(Y) | -c1_1(X) | -c3_1(Z) | -c2_1(Z) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X) | c0_1(Z).
% 418956 [binary:416473,418953,factor] -c1_1(a282) | c3_1(a282) | c0_1(a282) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c2_1(X) | c0_1(X) | c0_1(Y).
% 419062 [binary:417670,417768,factor:factor:factor:factor:factor:factor:factor] -c3_1(a249) | -c0_1(a249) | c2_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419069 [binary:416845,419062,factor] -c0_1(a249) | c2_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419072 [binary:416846,419069,factor] c2_1(a249) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419078 [binary:416560,419072] -hskp10(0) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419083 [binary:416844,419078,factor] -c2_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419483 [binary:416845,418430,factor:factor] -c0_1(a249) | c1_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 419486 [binary:416846,419483,factor:factor] c1_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 419491 [binary:417640,419486,factor:factor:factor] -c3_1(a249) | -c0_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 419496 [binary:416845,419491,factor] -c0_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 419499 [binary:416846,419496,factor] c2_1(a249) | -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 419502 [binary:416560,419499] -hskp10(0) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 419507 [binary:416844,419502,factor] -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 419535 [binary:416959,419507,factor:factor:factor:factor:factor:factor:factor] c1_1(a242) | c0_1(a242) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 419580 [binary:416567,419535,binarycut:416566] -hskp6(0) | c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 419596 [binary:416958,419580,factor:factor] c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 419599 [binary:416531,419596,binarycut:416533,binarycut:416532] -hskp27(0) | c0_1(a322).
% 419601 [binary:416546,419596,binarycut:416547,binarycut:416545] -hskp17(0) | c2_1(a263).
% 419610 [binary:416882,419596,factor] -c1_1(a257) | c3_1(a257) | c2_1(a257) | c0_1(a257).
% 419613 [binary:416747,419596] -c1_1(X) | -c3_1(Y) | -c2_1(X) | c1_1(Y) | c3_1(Z) | c3_1(X) | c2_1(Y) | c2_1(Z) | c0_1(Z).
% 419617 [binary:418956,419596,factor] -c1_1(a282) | c3_1(a282) | c2_1(a282) | c0_1(a282) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 419623 [binary:416935,419601] c2_1(a263) | hskp19(0) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 419652 [binary:419083,419623] c1_1(a263) | c0_1(a263) | hskp19(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419655 [binary:419596,419610] c3_1(a257) | c2_1(a257) | c0_1(a257).
% 419657 [binary:417007,419655] c2_1(a257) | c0_1(a257) | hskp31(0).
% 419688 [binary:419596,419617] c3_1(a282) | c2_1(a282) | c0_1(a282) | -c3_1(X) | -c2_1(X) | c0_1(X).
% 419690 [binary:416750,419688] c2_1(a282) | c0_1(a282) | -c3_1(Y) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c3_1(Z) | c2_1(Y) | c2_1(Z) | c0_1(Z) | c0_1(X).
% 419707 [binary:416867,419613,factor:factor] -c2_1(a265) | c3_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 419816 [binary:416863,419707,factor:factor] c3_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 419836 [binary:416546,419652,binarycut:416545] -hskp17(0) | hskp19(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419845 [binary:416935,419836,factor] hskp19(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419847 [binary:416463,419845] c3_1(a269) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419849 [binary:416464,419845] c0_1(a269) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419865 [binary:416749,419847,factor:factor:factor:factor:factor] -c0_1(a269) | c1_1(a269) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419878 [binary:419849,419865,factor:factor:factor:factor] c1_1(a269) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419881 [binary:416543,419878] -hskp19(0) | -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419905 [binary:419845,419881,factor:factor] -c3_1(X) | -c2_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 419913 [binary:416828,419905,factor] -c2_1(a240) | c0_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 419939 [binary:417695,419905,factor:factor] -c2_1(a265) | c0_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 419960 [binary:416830,419913,factor] c0_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 420208 [binary:416863,419939,factor:factor] c0_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 420210 [binary:416544,420208] -hskp18(0) | -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(X).
% 420214 [binary:416862,420210,factor:factor] -c3_1(X) | -c0_1(Y) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(X).
% 420216 [binary:416825,420214] c1_1(a239) | c2_1(a239) | c0_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421128 [binary:416569,420216,binarycut:416570] -hskp4(0) | c0_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(Y) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421141 [binary:416824,421128,factor] c0_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421164 [binary:417158,421141,factor:factor:factor:factor:factor] c1_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421166 [binary:416569,421164] -hskp4(0) | -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421187 [binary:416824,421166,factor] -c1_1(X) | -c3_1(X) | -c0_1(X) | -c0_1(Y) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 421194 [binary:416831,421187,factor:factor] -c3_1(a240) | -c0_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 421232 [binary:416828,421194,factor:factor] -c0_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 421236 [binary:419960,421232,factor] -c0_1(X) | c1_1(X) | c3_1(X) | c2_1(X).
% 421238 [binary:416779,421236] c1_1(a244) | c3_1(a244) | c2_1(a244) | hskp8(0) | hskp15(0).
% 421242 [binary:417011,421236] c1_1(a252) | c3_1(a252) | c2_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 421263 [binary:416564,421238,binarycut:416565] -hskp7(0) | c3_1(a244) | hskp8(0) | hskp15(0).
% 421266 [binary:416495,421263] c3_1(a244) | hskp8(0) | hskp15(0).
% 421269 [binary:416749,421266] -c0_1(a244) | c1_1(a244) | hskp8(0) | hskp15(0) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 421300 [binary:416556,421242,binarycut:416557] -hskp12(0) | c2_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 421305 [binary:417010,421300,factor] c2_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c0_1(X).
% 421370 [binary:416779,421269] c1_1(a244) | hskp8(0) | hskp15(0) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 421372 [binary:416564,421370] -hskp7(0) | hskp8(0) | hskp15(0) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 421392 [binary:416495,421372] hskp8(0) | hskp15(0) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 421398 [binary:416451,421392] c0_1(a245) | hskp15(0) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 421507 [binary:417263,417608,factor:factor:factor:factor:factor:factor] c3_1(a294) | -c3_1(Y) | -c3_1(X) | -c2_1(Z) | -c0_1(X) | c1_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Z) | c2_1(Y) | c0_1(Y).
% 421602 [binary:416536,421507] -hskp25(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Z) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c2_1(Y) | c0_1(Y).
% 421614 [binary:416759,421602,factor:factor:factor:factor] -c3_1(X) | -c3_1(Y) | -c2_1(Z) | -c0_1(Y) | c1_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Z) | c2_1(X) | c0_1(X).
% 421787 [binary:416538,419690,binarycut:416537] -hskp24(0) | -c3_1(Y) | -c3_1(X) | -c2_1(Y) | -c0_1(X) | c3_1(Z) | c2_1(X) | c2_1(Z) | c0_1(Y) | c0_1(Z).
% 421796 [binary:418953,421787,factor:factor:factor:factor:factor:factor] -c1_1(X) | -c3_1(Z) | -c3_1(Y) | -c2_1(Y) | -c0_1(Z) | c3_1(X) | c2_1(X) | c2_1(Z) | c0_1(X) | c0_1(Y).
% 421828 [binary:419596,421796] -c3_1(X) | -c3_1(Y) | -c2_1(Y) | -c0_1(X) | c3_1(Z) | c2_1(Z) | c2_1(X) | c0_1(Z) | c0_1(Y).
% 421835 [binary:416845,421828,factor] -c0_1(a249) | c2_1(a249) | -c3_1(X) | -c2_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 421860 [binary:416781,421828,factor:factor] -c0_1(a249) | c2_1(a249) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y) | c0_1(X).
% 421905 [binary:416846,421835,factor] c2_1(a249) | -c3_1(X) | -c2_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 421907 [binary:416560,421905] -hskp10(0) | -c3_1(X) | -c2_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 421919 [binary:416844,421907,factor] -c3_1(X) | -c2_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 421948 [binary:416881,421919,factor:factor:factor:factor:factor:factor] -c2_1(a257) | c1_1(a257) | c0_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 421974 [binary:416883,421948,factor:factor:factor:factor:factor] c1_1(a257) | c0_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 421976 [binary:416553,421974] -hskp14(0) | c0_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 421993 [binary:416880,421976,factor:factor:factor:factor:factor] c0_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 422066 [binary:416783,421860,factor:factor] c2_1(a249) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c2_1(X) | c0_1(X) | c0_1(Y).
% 422068 [binary:416560,422066] -hskp10(0) | -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y) | c0_1(X).
% 422072 [binary:416780,422068,factor:factor] -c1_1(X) | -c3_1(Y) | -c2_1(Y) | c3_1(X) | c2_1(X) | c0_1(X) | c0_1(Y).
% 422096 [binary:419596,422072] -c3_1(X) | -c2_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 422108 [binary:416914,422096] -c2_1(a241) | c0_1(a241) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422149 [binary:419816,422096,factor:factor] -c2_1(a265) | c0_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X) | c0_1(Y).
% 422482 [binary:416863,422149,factor:factor] c0_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 422484 [binary:416544,422482] -hskp18(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 422488 [binary:416862,422484,factor:factor] -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y) | c0_1(Y).
% 422697 [binary:416915,422108,factor] c0_1(a241) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422699 [binary:416568,422697] -hskp5(0) | hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422702 [binary:416913,422699,factor] hskp10(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422704 [binary:416453,422702] c3_1(a249) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422706 [binary:416454,422702] c0_1(a249) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 422718 [binary:422488,422704,factor:factor:factor:factor] -c0_1(a249) | c1_1(a249) | c2_1(a249) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 423522 [binary:422706,422718,factor:factor:factor:factor:factor] c1_1(a249) | c2_1(a249) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 423532 [binary:416748,423522,factor:factor:factor:factor:factor:factor] -c3_1(a249) | c2_1(a249) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(X) | c0_1(X).
% 423557 [binary:422704,423532,factor:factor:factor:factor] c2_1(a249) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(X) | c0_1(X).
% 423560 [binary:416560,423557] -hskp10(0) | -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(X) | c0_1(X).
% 423567 [binary:422702,423560,factor:factor] -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c3_1(X) | c2_1(X) | c0_1(X).
% 423588 [binary:419596,423567] -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(Y).
% 423615 [binary:416881,423588,factor:factor:factor] -c0_1(a257) | c1_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 423631 [binary:421993,423615,factor] c1_1(a257) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 423633 [binary:416553,423631] -hskp14(0) | -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 423649 [binary:416880,423633,factor:factor] -c1_1(X) | c3_1(X) | c2_1(X) | c0_1(X).
% 423669 [binary:419596,423649] c3_1(X) | c2_1(X) | c0_1(X).
% 423674 [binary:416552,423669,binarycut:416551,binarycut:416550] -hskp15(0).
% 423676 [binary:416555,423669,binarycut:416554] -hskp13(0) | c2_1(a253).
% 423719 [binary:421614,423669] -c3_1(X) | -c2_1(Y) | -c0_1(X) | c1_1(Y) | c1_1(Z) | c1_1(X) | c3_1(Y) | c2_1(Z) | c0_1(Z).
% 423722 [binary:416798,423674] -c1_1(X) | -c3_1(Y) | -c0_1(Y) | c1_1(Y) | c2_1(X) | c0_1(X).
% 423929 [binary:416845,423719,factor:factor] -c0_1(a249) | c1_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424110 [binary:416846,423929,factor:factor] c1_1(a249) | -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424117 [binary:417640,424110,factor:factor] -c3_1(a249) | -c0_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424452 [binary:416845,424117,factor] -c0_1(a249) | c2_1(a249) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424455 [binary:416846,424452,factor] c2_1(a249) | -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424457 [binary:416560,424455] -hskp10(0) | -c2_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424461 [binary:416844,424457,factor] -c2_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424475 [binary:419623,424461] c1_1(a263) | c3_1(a263) | c0_1(a263) | hskp19(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424771 [binary:416546,424475,binarycut:416547,binarycut:416545] -hskp17(0) | hskp19(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424783 [binary:416935,424771,factor] hskp19(0) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 424785 [binary:416463,424783] c3_1(a269) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424786 [binary:416464,424783] c0_1(a269) | -c3_1(X) | -c2_1(X) | c1_1(Y) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 424801 [binary:423719,424785,factor:factor:factor:factor] -c0_1(a269) | c1_1(a269) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Z).
% 425891 [binary:424786,424801,factor:factor:factor:factor:factor] c1_1(a269) | -c3_1(X) | -c2_1(Y) | -c2_1(X) | c1_1(Z) | c1_1(Y) | c3_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Z).
% 425894 [binary:416543,425891] -hskp19(0) | -c3_1(X) | -c2_1(X) | -c2_1(Y) | c1_1(Z) | c1_1(Y) | c3_1(Y) | c2_1(Z) | c0_1(Z) | c0_1(X).
% 425914 [binary:424783,425894,factor:factor] -c3_1(X) | -c2_1(Y) | -c2_1(X) | c1_1(Y) | c1_1(Z) | c3_1(Y) | c2_1(Z) | c0_1(X) | c0_1(Z).
% 425955 [binary:417254,425914,factor:factor:factor:factor:factor:factor:factor] -c2_1(a241) | c0_1(a241) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 426054 [binary:417258,425955,factor:factor:factor] c0_1(a241) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 426056 [binary:416568,426054] -hskp5(0) | -c2_1(X) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 426123 [binary:416758,426056,factor:factor] -c2_1(X) | -c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(X) | c2_1(Y) | c0_1(Y).
% 426142 [binary:421305,426123,factor:factor] -c0_1(a252) | c1_1(a252) | c3_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426156 [binary:417011,426142,factor:factor] c1_1(a252) | c3_1(a252) | hskp13(0) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426159 [binary:416556,426156,binarycut:416557] -hskp12(0) | hskp13(0) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426164 [binary:417010,426159,factor] hskp13(0) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426166 [binary:416457,426164] c1_1(a253) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426168 [binary:423676,426164] c2_1(a253) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426187 [binary:417588,426166,factor] -c2_1(a253) | c3_1(a253) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426198 [binary:426168,426187,factor] c3_1(a253) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426200 [binary:416555,426198] -hskp13(0) | -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426205 [binary:426164,426200,factor] -c3_1(X) | c1_1(X) | c2_1(X) | c0_1(X).
% 426240 [binary:423669,426205] c1_1(X) | c2_1(X) | c0_1(X).
% 426245 [binary:416569,426240,binarycut:416570] -hskp4(0) | c0_1(a239).
% 426254 [binary:423722,426240] -c3_1(X) | -c0_1(X) | c1_1(X) | c2_1(Y) | c0_1(Y).
% 426259 [binary:416764,426245] c0_1(a239) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 426260 [binary:416824,426245] c0_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X).
% 426279 [binary:416825,426254] -c0_1(a239) | c1_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c2_1(Y) | c0_1(Y).
% 426280 [binary:416845,426254] -c0_1(a249) | c1_1(a249) | -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 426294 [binary:417005,426254,factor] -c0_1(a257) | c1_1(a257) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426442 [binary:426260,426279,factor] c1_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c2_1(Y) | c0_1(Y).
% 426444 [binary:416569,426442] -hskp4(0) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c2_1(Y) | c0_1(Y).
% 426463 [binary:416824,426444,factor] -c1_1(X) | -c3_1(X) | -c0_1(X) | c2_1(Y) | c0_1(Y).
% 426519 [binary:416846,426280,factor:factor] c1_1(a249) | -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 426527 [binary:426463,426519,factor] -c3_1(a249) | -c0_1(a249) | -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 426594 [binary:416845,426527,factor] -c0_1(a249) | -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(Y) | c0_1(X).
% 426597 [binary:416846,426594,factor] -c2_1(X) | c1_1(X) | c2_1(Y) | c0_1(X) | c0_1(Y).
% 426630 [binary:419657,426597] c1_1(a257) | c0_1(a257) | hskp31(0) | c2_1(X) | c0_1(X).
% 426681 [binary:416553,426630] -hskp14(0) | c0_1(a257) | hskp31(0) | c2_1(X) | c0_1(X).
% 426719 [binary:417004,426681,factor:factor] c0_1(a257) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426727 [binary:426294,426719,factor] c1_1(a257) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426747 [binary:416553,426727] -hskp14(0) | hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426752 [binary:417004,426747,factor] hskp31(0) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426754 [binary:416486,426752] c3_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426757 [binary:416488,426752] c0_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426768 [binary:426254,426754,factor] -c0_1(a246) | c1_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426774 [binary:426757,426768,factor] c1_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426777 [binary:426463,426774,factor:factor] -c3_1(a246) | -c0_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426782 [binary:426754,426777,factor] -c0_1(a246) | -c3_1(X) | c2_1(X) | c0_1(X).
% 426786 [binary:426757,426782,factor] -c3_1(X) | c2_1(X) | c0_1(X).
% 426803 [binary:423669,426786] c2_1(X) | c0_1(X).
% 426806 [binary:416538,426803,binarycut:416537] -hskp24(0).
% 426807 [binary:416539,426803] -hskp23(0) | c0_1(a281).
% 426812 [binary:416995,426803] c3_1(a239) | c0_1(a239) | hskp28(0).
% 426819 [binary:416878,426806] hskp27(0) | -c1_1(X) | -c3_1(X) | -c2_1(X).
% 426824 [binary:416926,426807,cut:426806,binarycut:426803] c0_1(a281) | -c3_1(X) | c0_1(X).
% 426836 [binary:419599,426819] c0_1(a322) | -c1_1(X) | -c3_1(X) | -c2_1(X).
% 426838 [binary:421236,426836] c1_1(a322) | c3_1(a322) | c2_1(a322) | -c1_1(X) | -c3_1(X) | -c2_1(X).
% 426862 [binary:416531,426838,binarycut:416533,binarycut:416532] -hskp27(0) | -c1_1(X) | -c3_1(X) | -c2_1(X).
% 426868 [binary:426819,426862,factor] -c1_1(X) | -c3_1(X) | -c2_1(X).
% 426873 [binary:416831,426868] -c3_1(a240) | -c2_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X).
% 426884 [binary:416867,426868] -c3_1(a265) | -c2_1(a265) | -c3_1(X) | -c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 426892 [binary:417279,426868] -c3_1(a240) | -c2_1(a240) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 426986 [binary:416828,426873,factor] -c2_1(a240) | -c0_1(X) | c1_1(X) | c3_1(X).
% 426989 [binary:416830,426986,factor] -c0_1(X) | c1_1(X) | c3_1(X).
% 426992 [binary:416779,426989,cut:423674] c1_1(a244) | c3_1(a244) | hskp8(0).
% 427003 [binary:421398,426989,cut:423674] c1_1(a245) | c3_1(a245) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 427019 [binary:416564,426992] -hskp7(0) | c3_1(a244) | hskp8(0).
% 427023 [binary:416495,427019,cut:423674] c3_1(a244) | hskp8(0).
% 427338 [binary:416563,427003] -hskp8(0) | c3_1(a245) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 427347 [binary:417275,426892,factor:factor:factor] -c2_1(a240) | -c1_1(X) | -c3_1(Y) | -c3_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 427351 [binary:417276,427347,factor:factor] -c1_1(X) | -c3_1(Y) | -c3_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y).
% 427579 [binary:421392,427338,cut:423674,factor:factor:factor:factor] c3_1(a245) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 427589 [binary:416749,427579,factor:factor:factor:factor:factor:factor:factor] -c0_1(a245) | c1_1(a245) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 427703 [binary:421398,427589,cut:423674,factor:factor:factor:factor:factor] c1_1(a245) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 427706 [binary:416563,427703] -hskp8(0) | -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 427719 [binary:421392,427706,cut:423674,factor:factor:factor] -c0_1(X) | c1_1(X) | c1_1(Y) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 427744 [binary:426260,427719] c1_1(a239) | c2_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 427751 [binary:426259,427719,factor:factor:factor] c1_1(a239) | c2_1(a239) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 427880 [binary:416569,427744,binarycut:416570] -hskp4(0) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 427895 [binary:416824,427880,factor] -c1_1(X) | -c3_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 427899 [binary:416928,427895,cut:426806,binarycut:426803] -c3_1(a281) | -c0_1(a281) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 427940 [binary:416927,427899,cut:426806,binarycut:426803,factor] -c0_1(a281) | -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 427943 [binary:426824,427940,factor] -c3_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 427953 [binary:426812,427943] c0_1(a239) | hskp28(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 427965 [binary:427719,427953,factor:factor:factor] c1_1(a239) | c2_1(a239) | hskp28(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 428031 [binary:416569,427965,binarycut:416570] -hskp4(0) | hskp28(0) | c1_1(X) | c3_1(X) | c2_1(X).
% 428040 [binary:416993,428031,binarycut:426803] hskp28(0) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 428043 [binary:416477,428040] c2_1(a237) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 428045 [binary:416478,428040] c1_1(a237) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 428048 [binary:416479,428040,factor] c3_1(a237) | c0_1(a237) | c1_1(X) | c3_1(X) | c2_1(X).
% 428054 [binary:427943,428048,factor] c0_1(a237) | c1_1(X) | c3_1(X) | c2_1(X).
% 428139 [binary:416569,427751,binarycut:416570] -hskp4(0) | -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 428146 [binary:416764,428139,factor:factor] -c1_1(X) | -c2_1(X) | -c0_1(X) | c1_1(Y) | c3_1(Y) | c2_1(Y).
% 428199 [binary:428045,428146,factor] -c2_1(a237) | -c0_1(a237) | c1_1(X) | c3_1(Y) | c3_1(X) | c2_1(X) | c0_1(Y).
% 428226 [binary:428043,428199,factor:factor] -c0_1(a237) | c1_1(X) | c3_1(X) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 428229 [binary:428054,428226,factor] c1_1(X) | c3_1(X) | c3_1(Y) | c2_1(X) | c0_1(Y).
% 428246 [binary:416747,428229,factor:factor:binarycut:426803] -c1_1(X) | -c3_1(Y) | c1_1(Y) | c3_1(Z) | c3_1(X) | c2_1(Z) | c2_1(Y) | c0_1(X).
% 428270 [binary:416763,428246,cut:426806] c3_1(a253) | c0_1(a253) | hskp23(0) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 428276 [binary:416867,428246,factor:factor] c3_1(a265) | c0_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 428432 [binary:426884,428276,binarycut:426803,factor:factor] c0_1(a265) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 428434 [binary:416544,428432] -hskp18(0) | -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 428440 [binary:416862,428434,factor:factor] -c3_1(X) | -c0_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 428447 [binary:416845,428440,binarycut:426803] -c0_1(a249) | c1_1(a249) | c2_1(a249) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 428607 [binary:416846,428447,binarycut:426803,factor:factor] c1_1(a249) | c2_1(a249) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429071 [binary:416555,428270,binarycut:416554] -hskp13(0) | hskp23(0) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429075 [binary:416490,429071,cut:426806] hskp23(0) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 429077 [binary:416471,429075] c3_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429078 [binary:416471,429075,factor] c3_1(a281) | c2_1(a281) | -c3_1(X) | c1_1(X) | c2_1(X).
% 429079 [binary:416472,429075] c1_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429090 [binary:426868,429079] -c3_1(a281) | -c2_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429093 [binary:427351,429079,factor:factor:factor:factor] -c3_1(a281) | c2_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429099 [binary:429077,429090,factor:factor] -c2_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429105 [binary:429078,429093,factor:factor:factor] c2_1(a281) | -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(Y) | c2_1(X).
% 429112 [binary:429099,429105,factor:factor] -c3_1(X) | c1_1(X) | c3_1(Y) | c2_1(X) | c2_1(Y).
% 429114 [binary:416825,429112] c1_1(a239) | c2_1(a239) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c2_1(Y).
% 429159 [binary:416569,429114,binarycut:416570] -hskp4(0) | -c1_1(X) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c2_1(Y).
% 429168 [binary:416824,429159,factor] -c1_1(X) | -c3_1(X) | -c0_1(X) | c3_1(Y) | c2_1(Y).
% 429172 [binary:416928,429168,cut:426806,binarycut:426803] -c3_1(a281) | -c0_1(a281) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429194 [binary:428607,429168,factor:factor] -c3_1(a249) | -c0_1(a249) | c2_1(a249) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429221 [binary:416927,429172,cut:426806,binarycut:426803,factor] -c0_1(a281) | -c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429224 [binary:426824,429221,factor] -c3_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429226 [binary:416740,429224] c0_1(a241) | hskp9(0) | hskp11(0) | c3_1(X) | c2_1(X).
% 429250 [binary:416568,429226] -hskp5(0) | hskp9(0) | hskp11(0) | c3_1(X) | c2_1(X).
% 429261 [binary:416489,429250] hskp9(0) | hskp11(0) | c3_1(X) | c2_1(X).
% 429263 [binary:416452,429261] c3_1(a248) | hskp11(0) | c3_1(X) | c2_1(X).
% 429270 [binary:429224,429263,factor] c0_1(a248) | hskp11(0) | c3_1(X) | c2_1(X).
% 429273 [binary:416561,429270] -hskp9(0) | hskp11(0) | c3_1(X) | c2_1(X).
% 429279 [binary:429261,429273,factor] hskp11(0) | c3_1(X) | c2_1(X).
% 429448 [binary:416845,429194,binarycut:426803,factor] -c0_1(a249) | c2_1(a249) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429452 [binary:416846,429448,binarycut:426803,factor] c2_1(a249) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429454 [binary:416560,429452] -hskp10(0) | c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429458 [binary:416844,429454,binarycut:426803,factor] c1_1(X) | c3_1(Y) | c2_1(Y) | c0_1(X).
% 429463 [binary:416558,429458] -hskp11(0) | c0_1(a251) | c3_1(X) | c2_1(X).
% 429483 [binary:429279,429463,factor] c0_1(a251) | c3_1(X) | c2_1(X).
% 429485 [binary:426989,429483] c1_1(a251) | c3_1(a251) | c3_1(X) | c2_1(X).
% 429489 [binary:416558,429485,binarycut:416559] -hskp11(0) | c3_1(X) | c2_1(X).
% 429495 [binary:429279,429489,factor] c3_1(X) | c2_1(X).
% 429501 [binary:416572,429495,binarycut:416571] -hskp3(0).
% 429513 [binary:416910,429501] hskp12(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 429532 [binary:416456,429513] c0_1(a252) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 429535 [binary:426989,429532] c1_1(a252) | c3_1(a252) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 429543 [binary:416556,429535,binarycut:416557] -hskp12(0) | -c3_1(X) | -c0_1(X) | c1_1(X).
% 429546 [binary:429513,429543,factor] -c3_1(X) | -c0_1(X) | c1_1(X).
% 429578 [binary:427023,429546] -c0_1(a244) | c1_1(a244) | hskp8(0).
% 429640 [binary:416779,429578,cut:423674] c1_1(a244) | hskp8(0).
% 429642 [binary:416564,429640] -hskp7(0) | hskp8(0).
% 429648 [binary:416495,429642,cut:423674] hskp8(0).
% 429650 [binary:416451,429648] c0_1(a245).
% 429651 [binary:426989,429650] c1_1(a245) | c3_1(a245).
% 429653 [binary:416563,429651,cut:429648] c3_1(a245).
% 429654 [binary:429546,429653,cut:429650] c1_1(a245).
% 429655 [binary:416563,429654,cut:429648] 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:    24471
%  derived clauses:   1191316
%  kept clauses:      239542
%  kept size sum:     836502
%  kept mid-nuclei:   106365
%  kept new demods:   0
%  forw unit-subs:    9
%  forw double-subs: 54466
%  forw overdouble-subs: 634669
%  backward subs:     7278
%  fast unit cutoff:  15106
%  full unit cutoff:  0
%  dbl  unit cutoff:  12778
%  real runtime:  260.6
%  process. runtime:  258.85
% specific non-discr-tree subsumption statistics: 
%  tried:           154078757
%  length fails:    872971
%  strength fails:  55470821
%  predlist fails:  78540832
%  aux str. fails:  2241685
%  by-lit fails:    13124069
%  full subs tried: 1533820
%  full subs fail:  1443558
% 
% ; 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/SYN502-1+noeq.in")
% 
%------------------------------------------------------------------------------