WATCH: 0.00 CPU 0.01 WC ----- Otter 3.3f, August 2004 ----- The process was started by sutcliff on cl5-019, Wed Aug 3 11:39:06 2011 The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter". The process ID is 4703. set(prolog_style_variables). set(tptp_eq). set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). formula_list(usable). -(-((c1_1(a584)& -c0_1(a584)& -c2_1(a584)&ndr1_0| -hskp0)& (-hskp1|c2_1(a585)& -c0_1(a585)&c1_1(a585)&ndr1_0)& (-hskp3|c2_1(a587)& -c1_1(a587)&c0_1(a587)&ndr1_0)& (ndr1_0& -c1_1(a599)&c3_1(a599)&c2_1(a599)| -hskp11)& (-hskp12|c0_1(a600)& -c3_1(a600)&c2_1(a600)&ndr1_0)& (ndr1_0&c0_1(a603)& -c3_1(a603)& -c1_1(a603)| -hskp14)& (c1_1(a604)& -c0_1(a604)&c3_1(a604)&ndr1_0| -hskp15)& (ndr1_0&c3_1(a607)& -c2_1(a607)& -c1_1(a607)| -hskp17)& (c3_1(a610)& -c0_1(a610)& -c2_1(a610)&ndr1_0| -hskp18)& (-hskp19| -c1_1(a617)& -c0_1(a617)&c2_1(a617)&ndr1_0)& (-hskp21| -c2_1(a629)& -c3_1(a629)&c0_1(a629)&ndr1_0)& (-c3_1(a633)& -c0_1(a633)&c1_1(a633)&ndr1_0| -hskp22)& (ndr1_0& -c1_1(a636)& -c0_1(a636)&c3_1(a636)| -hskp23)& (-hskp25| -c1_1(a651)& -c3_1(a651)&c2_1(a651)&ndr1_0)& (-hskp26|c0_1(a583)&c2_1(a583)&c1_1(a583)&ndr1_0)& (c0_1(a678)&c2_1(a678)&c3_1(a678)&ndr1_0| -hskp29)& (hskp1| (all Z (ndr1_0-> -c3_1(Z)| -c1_1(Z)|c0_1(Z)))| (all Y (ndr1_0->c0_1(Y)|c3_1(Y)|c1_1(Y))))& ((all X2 (ndr1_0->c1_1(X2)| -c2_1(X2)|c3_1(X2)))|hskp2| (all X1 (ndr1_0->c0_1(X1)|c3_1(X1)|c1_1(X1))))& ((all X4 (ndr1_0->c0_1(X4)|c1_1(X4)| -c2_1(X4)))| (all X5 (ndr1_0->c0_1(X5)| -c2_1(X5)| -c3_1(X5)))| (all X6 (ndr1_0-> -c1_1(X6)| -c3_1(X6)| -c0_1(X6))))& ((all X15 (ndr1_0-> -c3_1(X15)|c1_1(X15)|c0_1(X15)))|hskp6|hskp8)& ((all X18 (ndr1_0-> -c0_1(X18)|c2_1(X18)|c1_1(X18)))| (all X17 (ndr1_0-> -c3_1(X17)| -c1_1(X17)|c0_1(X17)))| (all X16 (ndr1_0->c3_1(X16)|c2_1(X16)|c0_1(X16))))& ((all X20 (ndr1_0->c0_1(X20)| -c3_1(X20)| -c2_1(X20)))| (all X21 (ndr1_0->c1_1(X21)| -c3_1(X21)| -c2_1(X21)))| (all X19 (ndr1_0->c3_1(X19)|c2_1(X19)|c0_1(X19))))& ((all X23 (ndr1_0->c1_1(X23)| -c0_1(X23)|c2_1(X23)))|hskp10| (all X22 (ndr1_0->c3_1(X22)|c2_1(X22)|c0_1(X22))))& ((all X24 (ndr1_0->c3_1(X24)|c2_1(X24)|c0_1(X24)))| (all X25 (ndr1_0-> -c0_1(X25)| -c2_1(X25)| -c3_1(X25)))|hskp11)& ((all X26 (ndr1_0->c0_1(X26)|c3_1(X26)|c2_1(X26)))|hskp12|hskp13)& (hskp16| (all X30 (ndr1_0->c1_1(X30)| -c2_1(X30)|c3_1(X30)))| (all X29 (ndr1_0->c0_1(X29)|c2_1(X29)| -c1_1(X29))))& ((all X31 (ndr1_0->c0_1(X31)|c2_1(X31)| -c1_1(X31)))|hskp17| (all X32 (ndr1_0->c1_1(X32)| -c2_1(X32)| -c0_1(X32))))& ((all X34 (ndr1_0-> -c3_1(X34)|c2_1(X34)|c0_1(X34)))|hskp18| (all X35 (ndr1_0->c1_1(X35)|c3_1(X35)| -c0_1(X35))))& ((all X36 (ndr1_0->c0_1(X36)| -c3_1(X36)|c2_1(X36)))| (all X37 (ndr1_0-> -c0_1(X37)| -c1_1(X37)|c2_1(X37)))|hskp27)& ((all X38 (ndr1_0->c0_1(X38)|c2_1(X38)| -c3_1(X38)))|hskp28| (all X39 (ndr1_0->c3_1(X39)| -c0_1(X39)| -c2_1(X39))))& ((all X40 (ndr1_0-> -c1_1(X40)|c3_1(X40)|c0_1(X40)))| (all X42 (ndr1_0->c3_1(X42)| -c0_1(X42)| -c2_1(X42)))| (all X41 (ndr1_0-> -c2_1(X41)| -c3_1(X41)|c1_1(X41))))& ((all X43 (ndr1_0-> -c2_1(X43)|c3_1(X43)|c0_1(X43)))| (all X44 (ndr1_0->c1_1(X44)| -c0_1(X44)|c2_1(X44)))|hskp14)& ((all X45 (ndr1_0-> -c2_1(X45)|c3_1(X45)|c0_1(X45)))|hskp8|hskp18)& ((all X46 (ndr1_0-> -c2_1(X46)| -c1_1(X46)|c0_1(X46)))| (all X47 (ndr1_0-> -c3_1(X47)|c2_1(X47)|c1_1(X47)))| (all X48 (ndr1_0-> -c0_1(X48)| -c3_1(X48)| -c2_1(X48))))& ((all X49 (ndr1_0->c0_1(X49)| -c1_1(X49)| -c2_1(X49)))|hskp12| (all X50 (ndr1_0-> -c2_1(X50)| -c1_1(X50)| -c0_1(X50))))& ((all X54 (ndr1_0-> -c1_1(X54)| -c3_1(X54)|c0_1(X54)))|hskp16| (all X55 (ndr1_0-> -c1_1(X55)| -c0_1(X55)|c3_1(X55))))& ((all X56 (ndr1_0->c0_1(X56)| -c1_1(X56)| -c3_1(X56)))|hskp15| (all X57 (ndr1_0->c3_1(X57)| -c1_1(X57)| -c2_1(X57))))& ((all X58 (ndr1_0-> -c3_1(X58)| -c1_1(X58)|c0_1(X58)))|hskp7|hskp20)& (hskp16| (all X60 (ndr1_0->c2_1(X60)| -c0_1(X60)|c3_1(X60)))| (all X59 (ndr1_0->c0_1(X59)| -c3_1(X59)| -c2_1(X59))))& (hskp26| (all X63 (ndr1_0->c1_1(X63)| -c2_1(X63)| -c0_1(X63)))| (all X62 (ndr1_0->c1_1(X62)|c3_1(X62)|c2_1(X62))))& ((all X64 (ndr1_0-> -c0_1(X64)|c2_1(X64)|c1_1(X64)))|hskp1| (all X65 (ndr1_0-> -c0_1(X65)| -c2_1(X65)|c3_1(X65))))& ((all X69 (ndr1_0->c1_1(X69)| -c3_1(X69)|c2_1(X69)))|hskp3| (all X70 (ndr1_0->c3_1(X70)| -c0_1(X70)|c1_1(X70))))& ((all X71 (ndr1_0-> -c3_1(X71)|c2_1(X71)|c1_1(X71)))| (all X72 (ndr1_0->c2_1(X72)| -c1_1(X72)| -c0_1(X72)))| (all X73 (ndr1_0-> -c0_1(X73)| -c2_1(X73)| -c3_1(X73))))& ((all X74 (ndr1_0->c2_1(X74)| -c3_1(X74)|c1_1(X74)))|hskp23| (all X75 (ndr1_0->c2_1(X75)| -c3_1(X75)| -c0_1(X75))))& (hskp28| (all X81 (ndr1_0->c3_1(X81)| -c2_1(X81)| -c1_1(X81)))| (all X80 (ndr1_0->c1_1(X80)| -c3_1(X80)| -c2_1(X80))))& (hskp23|hskp14| (all X82 (ndr1_0-> -c2_1(X82)| -c3_1(X82)|c1_1(X82))))& ((all X84 (ndr1_0->c3_1(X84)| -c2_1(X84)| -c0_1(X84)))|hskp8| (all X83 (ndr1_0->c2_1(X83)| -c0_1(X83)|c3_1(X83))))& ((all X85 (ndr1_0->c2_1(X85)| -c0_1(X85)|c3_1(X85)))|hskp16|hskp3)& (hskp6|hskp8| (all X88 (ndr1_0->c2_1(X88)|c3_1(X88)| -c1_1(X88))))& ((all X92 (ndr1_0->c2_1(X92)| -c0_1(X92)| -c3_1(X92)))|hskp26|hskp28)& ((all X95 (ndr1_0-> -c3_1(X95)| -c0_1(X95)|c2_1(X95)))|hskp15|hskp11)& ((all X98 (ndr1_0-> -c1_1(X98)| -c3_1(X98)|c2_1(X98)))|hskp3|hskp17)& ((all X99 (ndr1_0->c3_1(X99)| -c1_1(X99)| -c0_1(X99)))|hskp3|hskp17)& ((all X101 (ndr1_0->c3_1(X101)| -c2_1(X101)| -c0_1(X101)))|hskp8|hskp27)& (hskp26|hskp12|hskp8)& (hskp11|hskp26)& (hskp14|hskp0|hskp21)& (hskp17|hskp7|hskp29)& (hskp17|hskp22|hskp29)& ((all X111 (ndr1_0-> -c1_1(X111)| -c2_1(X111)| -c3_1(X111)))|hskp1|hskp10)& ((all X110 (ndr1_0-> -c0_1(X110)| -c2_1(X110)| -c3_1(X110)))|hskp12|hskp10)& ((all X109 (ndr1_0-> -c0_1(X109)| -c1_1(X109)| -c3_1(X109)))|hskp19|hskp20)& ((all X108 (ndr1_0-> -c1_1(X108)| -c3_1(X108)| -c0_1(X108)))|hskp29|hskp14)& ((all X106 (ndr1_0-> -c2_1(X106)| -c1_1(X106)| -c0_1(X106)))| (all X107 (ndr1_0-> -c2_1(X107)| -c3_1(X107)| -c1_1(X107)))|hskp10)& ((all X105 (ndr1_0->c3_1(X105)| -c2_1(X105)| -c1_1(X105)))|hskp18|hskp29)& ((all X104 (ndr1_0->c3_1(X104)| -c1_1(X104)| -c2_1(X104)))|hskp15|hskp29)& (hskp7|hskp20| (all X103 (ndr1_0-> -c0_1(X103)| -c2_1(X103)|c3_1(X103))))& ((all X102 (ndr1_0-> -c0_1(X102)| -c2_1(X102)|c3_1(X102)))|hskp14|hskp22)& (hskp4|hskp17| (all X100 (ndr1_0-> -c0_1(X100)| -c1_1(X100)|c3_1(X100))))& ((all X97 (ndr1_0-> -c3_1(X97)| -c2_1(X97)| -c0_1(X97)))|hskp14| (all X96 (ndr1_0->c2_1(X96)| -c1_1(X96)| -c3_1(X96))))& ((all X94 (ndr1_0-> -c0_1(X94)| -c3_1(X94)|c2_1(X94)))|hskp21|hskp8)& (hskp24|hskp5| (all X93 (ndr1_0-> -c3_1(X93)| -c0_1(X93)|c2_1(X93))))& ((all X91 (ndr1_0-> -c0_1(X91)| -c1_1(X91)|c2_1(X91)))|hskp11|hskp0)& (hskp25|hskp15| (all X90 (ndr1_0->c2_1(X90)| -c0_1(X90)| -c1_1(X90))))& (hskp25|hskp9| (all X89 (ndr1_0->c2_1(X89)| -c1_1(X89)|c3_1(X89))))& ((all X86 (ndr1_0-> -c1_1(X86)|c3_1(X86)|c2_1(X86)))| (all X87 (ndr1_0->c2_1(X87)| -c1_1(X87)| -c0_1(X87)))|hskp24)& ((all X79 (ndr1_0->c1_1(X79)| -c3_1(X79)| -c0_1(X79)))|hskp11|hskp23)& ((all X78 (ndr1_0-> -c0_1(X78)| -c1_1(X78)| -c3_1(X78)))|hskp15| (all X77 (ndr1_0-> -c3_1(X77)| -c0_1(X77)|c1_1(X77))))& ((all X76 (ndr1_0-> -c2_1(X76)|c3_1(X76)|c1_1(X76)))|hskp3|hskp4)& ((all X68 (ndr1_0->c2_1(X68)| -c0_1(X68)|c1_1(X68)))|hskp22|hskp6)& ((all X67 (ndr1_0->c1_1(X67)|c2_1(X67)| -c0_1(X67)))|hskp28|hskp8)& (hskp21|hskp11| (all X66 (ndr1_0->c2_1(X66)| -c0_1(X66)|c1_1(X66))))& (hskp4|hskp10| (all X61 (ndr1_0-> -c2_1(X61)| -c3_1(X61)|c0_1(X61))))& (hskp8| (all X53 (ndr1_0->c2_1(X53)| -c3_1(X53)| -c0_1(X53)))| (all X52 (ndr1_0-> -c3_1(X52)| -c1_1(X52)|c0_1(X52))))& ((all X51 (ndr1_0-> -c1_1(X51)| -c2_1(X51)|c0_1(X51)))|hskp13|hskp19)& (hskp10|hskp7| (all X33 (ndr1_0-> -c1_1(X33)|c2_1(X33)|c0_1(X33))))& (hskp13|hskp15| (all X28 (ndr1_0->c3_1(X28)|c2_1(X28)|c0_1(X28))))& ((all X27 (ndr1_0->c3_1(X27)|c2_1(X27)|c0_1(X27)))|hskp14|hskp4)& ((all X14 (ndr1_0-> -c2_1(X14)| -c1_1(X14)| -c0_1(X14)))|hskp9| (all X13 (ndr1_0->c1_1(X13)| -c3_1(X13)|c0_1(X13))))& ((all X11 (ndr1_0-> -c3_1(X11)|c1_1(X11)|c0_1(X11)))| (all X12 (ndr1_0->c1_1(X12)|c2_1(X12)|c3_1(X12)))|hskp26)& ((all X9 (ndr1_0->c0_1(X9)| -c3_1(X9)|c1_1(X9)))|hskp8| (all X10 (ndr1_0->c0_1(X10)| -c1_1(X10)| -c2_1(X10))))& ((all X8 (ndr1_0->c0_1(X8)| -c2_1(X8)|c1_1(X8)))|hskp2|hskp7)& (hskp5|hskp6| (all X7 (ndr1_0-> -c2_1(X7)|c1_1(X7)|c0_1(X7))))& ((all X3 (ndr1_0->c1_1(X3)|c3_1(X3)|c0_1(X3)))|hskp4|hskp3)& ((all V (ndr1_0->c0_1(V)|c3_1(V)|c1_1(V)))| (all X (ndr1_0-> -c0_1(X)|c3_1(X)|c2_1(X)))| (all W (ndr1_0->c0_1(W)| -c1_1(W)|c2_1(W))))& (hskp26|hskp0| (all U (ndr1_0->c0_1(U)|c2_1(U)|c1_1(U))))& (c1_1(a612)&c2_1(a612)&c3_1(a612)&ndr1_0| -hskp28)& (-hskp27|ndr1_0&c0_1(a611)&c1_1(a611)&c3_1(a611))& (-hskp24|ndr1_0&c0_1(a648)& -c3_1(a648)&c1_1(a648))& (ndr1_0& -c1_1(a623)& -c2_1(a623)& -c3_1(a623)| -hskp20)& (c1_1(a606)& -c2_1(a606)& -c3_1(a606)&ndr1_0| -hskp16)& (-hskp13| -c0_1(a601)& -c2_1(a601)& -c1_1(a601)&ndr1_0)& (-hskp10|c0_1(a598)&c3_1(a598)& -c1_1(a598)&ndr1_0)& (ndr1_0& -c0_1(a595)& -c3_1(a595)& -c1_1(a595)| -hskp9)& (-hskp8|c3_1(a593)& -c2_1(a593)&c1_1(a593)&ndr1_0)& (-hskp7|ndr1_0& -c0_1(a592)& -c3_1(a592)&c2_1(a592))& (-hskp6| -c0_1(a590)&c3_1(a590)&c2_1(a590)&ndr1_0)& (-hskp5|c0_1(a589)& -c2_1(a589)&c1_1(a589)&ndr1_0)& (ndr1_0&c0_1(a588)& -c1_1(a588)& -c2_1(a588)| -hskp4)& (-hskp2|c2_1(a586)& -c3_1(a586)&c1_1(a586)&ndr1_0))). end_of_list. -------> usable clausifies to: list(usable). 0 [] c1_1(a584)| -hskp0. 0 [] -c0_1(a584)| -hskp0. 0 [] -c2_1(a584)| -hskp0. 0 [] ndr1_0| -hskp0. 0 [] -hskp1|c2_1(a585). 0 [] -hskp1| -c0_1(a585). 0 [] -hskp1|c1_1(a585). 0 [] -hskp1|ndr1_0. 0 [] -hskp3|c2_1(a587). 0 [] -hskp3| -c1_1(a587). 0 [] -hskp3|c0_1(a587). 0 [] -hskp3|ndr1_0. 0 [] ndr1_0| -hskp11. 0 [] -c1_1(a599)| -hskp11. 0 [] c3_1(a599)| -hskp11. 0 [] c2_1(a599)| -hskp11. 0 [] -hskp12|c0_1(a600). 0 [] -hskp12| -c3_1(a600). 0 [] -hskp12|c2_1(a600). 0 [] -hskp12|ndr1_0. 0 [] ndr1_0| -hskp14. 0 [] c0_1(a603)| -hskp14. 0 [] -c3_1(a603)| -hskp14. 0 [] -c1_1(a603)| -hskp14. 0 [] c1_1(a604)| -hskp15. 0 [] -c0_1(a604)| -hskp15. 0 [] c3_1(a604)| -hskp15. 0 [] ndr1_0| -hskp15. 0 [] ndr1_0| -hskp17. 0 [] c3_1(a607)| -hskp17. 0 [] -c2_1(a607)| -hskp17. 0 [] -c1_1(a607)| -hskp17. 0 [] c3_1(a610)| -hskp18. 0 [] -c0_1(a610)| -hskp18. 0 [] -c2_1(a610)| -hskp18. 0 [] ndr1_0| -hskp18. 0 [] -hskp19| -c1_1(a617). 0 [] -hskp19| -c0_1(a617). 0 [] -hskp19|c2_1(a617). 0 [] -hskp19|ndr1_0. 0 [] -hskp21| -c2_1(a629). 0 [] -hskp21| -c3_1(a629). 0 [] -hskp21|c0_1(a629). 0 [] -hskp21|ndr1_0. 0 [] -c3_1(a633)| -hskp22. 0 [] -c0_1(a633)| -hskp22. 0 [] c1_1(a633)| -hskp22. 0 [] ndr1_0| -hskp22. 0 [] ndr1_0| -hskp23. 0 [] -c1_1(a636)| -hskp23. 0 [] -c0_1(a636)| -hskp23. 0 [] c3_1(a636)| -hskp23. 0 [] -hskp25| -c1_1(a651). 0 [] -hskp25| -c3_1(a651). 0 [] -hskp25|c2_1(a651). 0 [] -hskp25|ndr1_0. 0 [] -hskp26|c0_1(a583). 0 [] -hskp26|c2_1(a583). 0 [] -hskp26|c1_1(a583). 0 [] -hskp26|ndr1_0. 0 [] c0_1(a678)| -hskp29. 0 [] c2_1(a678)| -hskp29. 0 [] c3_1(a678)| -hskp29. 0 [] ndr1_0| -hskp29. 0 [] hskp1| -ndr1_0| -c3_1(Z)| -c1_1(Z)|c0_1(Z)|c0_1(Y)|c3_1(Y)|c1_1(Y). 0 [] -ndr1_0|c1_1(X2)| -c2_1(X2)|c3_1(X2)|hskp2|c0_1(X1)|c3_1(X1)|c1_1(X1). 0 [] -ndr1_0|c0_1(X4)|c1_1(X4)| -c2_1(X4)|c0_1(X5)| -c2_1(X5)| -c3_1(X5)| -c1_1(X6)| -c3_1(X6)| -c0_1(X6). 0 [] -ndr1_0| -c3_1(X15)|c1_1(X15)|c0_1(X15)|hskp6|hskp8. 0 [] -ndr1_0| -c0_1(X18)|c2_1(X18)|c1_1(X18)| -c3_1(X17)| -c1_1(X17)|c0_1(X17)|c3_1(X16)|c2_1(X16)|c0_1(X16). 0 [] -ndr1_0|c0_1(X20)| -c3_1(X20)| -c2_1(X20)|c1_1(X21)| -c3_1(X21)| -c2_1(X21)|c3_1(X19)|c2_1(X19)|c0_1(X19). 0 [] -ndr1_0|c1_1(X23)| -c0_1(X23)|c2_1(X23)|hskp10|c3_1(X22)|c2_1(X22)|c0_1(X22). 0 [] -ndr1_0|c3_1(X24)|c2_1(X24)|c0_1(X24)| -c0_1(X25)| -c2_1(X25)| -c3_1(X25)|hskp11. 0 [] -ndr1_0|c0_1(X26)|c3_1(X26)|c2_1(X26)|hskp12|hskp13. 0 [] hskp16| -ndr1_0|c1_1(X30)| -c2_1(X30)|c3_1(X30)|c0_1(X29)|c2_1(X29)| -c1_1(X29). 0 [] -ndr1_0|c0_1(X31)|c2_1(X31)| -c1_1(X31)|hskp17|c1_1(X32)| -c2_1(X32)| -c0_1(X32). 0 [] -ndr1_0| -c3_1(X34)|c2_1(X34)|c0_1(X34)|hskp18|c1_1(X35)|c3_1(X35)| -c0_1(X35). 0 [] -ndr1_0|c0_1(X36)| -c3_1(X36)|c2_1(X36)| -c0_1(X37)| -c1_1(X37)|c2_1(X37)|hskp27. 0 [] -ndr1_0|c0_1(X38)|c2_1(X38)| -c3_1(X38)|hskp28|c3_1(X39)| -c0_1(X39)| -c2_1(X39). 0 [] -ndr1_0| -c1_1(X40)|c3_1(X40)|c0_1(X40)|c3_1(X42)| -c0_1(X42)| -c2_1(X42)| -c2_1(X41)| -c3_1(X41)|c1_1(X41). 0 [] -ndr1_0| -c2_1(X43)|c3_1(X43)|c0_1(X43)|c1_1(X44)| -c0_1(X44)|c2_1(X44)|hskp14. 0 [] -ndr1_0| -c2_1(X45)|c3_1(X45)|c0_1(X45)|hskp8|hskp18. 0 [] -ndr1_0| -c2_1(X46)| -c1_1(X46)|c0_1(X46)| -c3_1(X47)|c2_1(X47)|c1_1(X47)| -c0_1(X48)| -c3_1(X48)| -c2_1(X48). 0 [] -ndr1_0|c0_1(X49)| -c1_1(X49)| -c2_1(X49)|hskp12| -c2_1(X50)| -c1_1(X50)| -c0_1(X50). 0 [] -ndr1_0| -c1_1(X54)| -c3_1(X54)|c0_1(X54)|hskp16| -c1_1(X55)| -c0_1(X55)|c3_1(X55). 0 [] -ndr1_0|c0_1(X56)| -c1_1(X56)| -c3_1(X56)|hskp15|c3_1(X57)| -c1_1(X57)| -c2_1(X57). 0 [] -ndr1_0| -c3_1(X58)| -c1_1(X58)|c0_1(X58)|hskp7|hskp20. 0 [] hskp16| -ndr1_0|c2_1(X60)| -c0_1(X60)|c3_1(X60)|c0_1(X59)| -c3_1(X59)| -c2_1(X59). 0 [] hskp26| -ndr1_0|c1_1(X63)| -c2_1(X63)| -c0_1(X63)|c1_1(X62)|c3_1(X62)|c2_1(X62). 0 [] -ndr1_0| -c0_1(X64)|c2_1(X64)|c1_1(X64)|hskp1| -c0_1(X65)| -c2_1(X65)|c3_1(X65). 0 [] -ndr1_0|c1_1(X69)| -c3_1(X69)|c2_1(X69)|hskp3|c3_1(X70)| -c0_1(X70)|c1_1(X70). 0 [] -ndr1_0| -c3_1(X71)|c2_1(X71)|c1_1(X71)|c2_1(X72)| -c1_1(X72)| -c0_1(X72)| -c0_1(X73)| -c2_1(X73)| -c3_1(X73). 0 [] -ndr1_0|c2_1(X74)| -c3_1(X74)|c1_1(X74)|hskp23|c2_1(X75)| -c3_1(X75)| -c0_1(X75). 0 [] hskp28| -ndr1_0|c3_1(X81)| -c2_1(X81)| -c1_1(X81)|c1_1(X80)| -c3_1(X80)| -c2_1(X80). 0 [] hskp23|hskp14| -ndr1_0| -c2_1(X82)| -c3_1(X82)|c1_1(X82). 0 [] -ndr1_0|c3_1(X84)| -c2_1(X84)| -c0_1(X84)|hskp8|c2_1(X83)| -c0_1(X83)|c3_1(X83). 0 [] -ndr1_0|c2_1(X85)| -c0_1(X85)|c3_1(X85)|hskp16|hskp3. 0 [] hskp6|hskp8| -ndr1_0|c2_1(X88)|c3_1(X88)| -c1_1(X88). 0 [] -ndr1_0|c2_1(X92)| -c0_1(X92)| -c3_1(X92)|hskp26|hskp28. 0 [] -ndr1_0| -c3_1(X95)| -c0_1(X95)|c2_1(X95)|hskp15|hskp11. 0 [] -ndr1_0| -c1_1(X98)| -c3_1(X98)|c2_1(X98)|hskp3|hskp17. 0 [] -ndr1_0|c3_1(X99)| -c1_1(X99)| -c0_1(X99)|hskp3|hskp17. 0 [] -ndr1_0|c3_1(X101)| -c2_1(X101)| -c0_1(X101)|hskp8|hskp27. 0 [] hskp26|hskp12|hskp8. 0 [] hskp11|hskp26. 0 [] hskp14|hskp0|hskp21. 0 [] hskp17|hskp7|hskp29. 0 [] hskp17|hskp22|hskp29. 0 [] -ndr1_0| -c1_1(X111)| -c2_1(X111)| -c3_1(X111)|hskp1|hskp10. 0 [] -ndr1_0| -c0_1(X110)| -c2_1(X110)| -c3_1(X110)|hskp12|hskp10. 0 [] -ndr1_0| -c0_1(X109)| -c1_1(X109)| -c3_1(X109)|hskp19|hskp20. 0 [] -ndr1_0| -c1_1(X108)| -c3_1(X108)| -c0_1(X108)|hskp29|hskp14. 0 [] -ndr1_0| -c2_1(X106)| -c1_1(X106)| -c0_1(X106)| -c2_1(X107)| -c3_1(X107)| -c1_1(X107)|hskp10. 0 [] -ndr1_0|c3_1(X105)| -c2_1(X105)| -c1_1(X105)|hskp18|hskp29. 0 [] -ndr1_0|c3_1(X104)| -c1_1(X104)| -c2_1(X104)|hskp15|hskp29. 0 [] hskp7|hskp20| -ndr1_0| -c0_1(X103)| -c2_1(X103)|c3_1(X103). 0 [] -ndr1_0| -c0_1(X102)| -c2_1(X102)|c3_1(X102)|hskp14|hskp22. 0 [] hskp4|hskp17| -ndr1_0| -c0_1(X100)| -c1_1(X100)|c3_1(X100). 0 [] -ndr1_0| -c3_1(X97)| -c2_1(X97)| -c0_1(X97)|hskp14|c2_1(X96)| -c1_1(X96)| -c3_1(X96). 0 [] -ndr1_0| -c0_1(X94)| -c3_1(X94)|c2_1(X94)|hskp21|hskp8. 0 [] hskp24|hskp5| -ndr1_0| -c3_1(X93)| -c0_1(X93)|c2_1(X93). 0 [] -ndr1_0| -c0_1(X91)| -c1_1(X91)|c2_1(X91)|hskp11|hskp0. 0 [] hskp25|hskp15| -ndr1_0|c2_1(X90)| -c0_1(X90)| -c1_1(X90). 0 [] hskp25|hskp9| -ndr1_0|c2_1(X89)| -c1_1(X89)|c3_1(X89). 0 [] -ndr1_0| -c1_1(X86)|c3_1(X86)|c2_1(X86)|c2_1(X87)| -c1_1(X87)| -c0_1(X87)|hskp24. 0 [] -ndr1_0|c1_1(X79)| -c3_1(X79)| -c0_1(X79)|hskp11|hskp23. 0 [] -ndr1_0| -c0_1(X78)| -c1_1(X78)| -c3_1(X78)|hskp15| -c3_1(X77)| -c0_1(X77)|c1_1(X77). 0 [] -ndr1_0| -c2_1(X76)|c3_1(X76)|c1_1(X76)|hskp3|hskp4. 0 [] -ndr1_0|c2_1(X68)| -c0_1(X68)|c1_1(X68)|hskp22|hskp6. 0 [] -ndr1_0|c1_1(X67)|c2_1(X67)| -c0_1(X67)|hskp28|hskp8. 0 [] hskp21|hskp11| -ndr1_0|c2_1(X66)| -c0_1(X66)|c1_1(X66). 0 [] hskp4|hskp10| -ndr1_0| -c2_1(X61)| -c3_1(X61)|c0_1(X61). 0 [] hskp8| -ndr1_0|c2_1(X53)| -c3_1(X53)| -c0_1(X53)| -c3_1(X52)| -c1_1(X52)|c0_1(X52). 0 [] -ndr1_0| -c1_1(X51)| -c2_1(X51)|c0_1(X51)|hskp13|hskp19. 0 [] hskp10|hskp7| -ndr1_0| -c1_1(X33)|c2_1(X33)|c0_1(X33). 0 [] hskp13|hskp15| -ndr1_0|c3_1(X28)|c2_1(X28)|c0_1(X28). 0 [] -ndr1_0|c3_1(X27)|c2_1(X27)|c0_1(X27)|hskp14|hskp4. 0 [] -ndr1_0| -c2_1(X14)| -c1_1(X14)| -c0_1(X14)|hskp9|c1_1(X13)| -c3_1(X13)|c0_1(X13). 0 [] -ndr1_0| -c3_1(X11)|c1_1(X11)|c0_1(X11)|c1_1(X12)|c2_1(X12)|c3_1(X12)|hskp26. 0 [] -ndr1_0|c0_1(X9)| -c3_1(X9)|c1_1(X9)|hskp8|c0_1(X10)| -c1_1(X10)| -c2_1(X10). 0 [] -ndr1_0|c0_1(X8)| -c2_1(X8)|c1_1(X8)|hskp2|hskp7. 0 [] hskp5|hskp6| -ndr1_0| -c2_1(X7)|c1_1(X7)|c0_1(X7). 0 [] -ndr1_0|c1_1(X3)|c3_1(X3)|c0_1(X3)|hskp4|hskp3. 0 [] -ndr1_0|c0_1(V)|c3_1(V)|c1_1(V)| -c0_1(X)|c3_1(X)|c2_1(X)|c0_1(W)| -c1_1(W)|c2_1(W). 0 [] hskp26|hskp0| -ndr1_0|c0_1(U)|c2_1(U)|c1_1(U). 0 [] c1_1(a612)| -hskp28. 0 [] c2_1(a612)| -hskp28. 0 [] c3_1(a612)| -hskp28. 0 [] ndr1_0| -hskp28. 0 [] -hskp27|ndr1_0. 0 [] -hskp27|c0_1(a611). 0 [] -hskp27|c1_1(a611). 0 [] -hskp27|c3_1(a611). 0 [] -hskp24|ndr1_0. 0 [] -hskp24|c0_1(a648). 0 [] -hskp24| -c3_1(a648). 0 [] -hskp24|c1_1(a648). 0 [] ndr1_0| -hskp20. 0 [] -c1_1(a623)| -hskp20. 0 [] -c2_1(a623)| -hskp20. 0 [] -c3_1(a623)| -hskp20. 0 [] c1_1(a606)| -hskp16. 0 [] -c2_1(a606)| -hskp16. 0 [] -c3_1(a606)| -hskp16. 0 [] ndr1_0| -hskp16. 0 [] -hskp13| -c0_1(a601). 0 [] -hskp13| -c2_1(a601). 0 [] -hskp13| -c1_1(a601). 0 [] -hskp13|ndr1_0. 0 [] -hskp10|c0_1(a598). 0 [] -hskp10|c3_1(a598). 0 [] -hskp10| -c1_1(a598). 0 [] -hskp10|ndr1_0. 0 [] ndr1_0| -hskp9. 0 [] -c0_1(a595)| -hskp9. 0 [] -c3_1(a595)| -hskp9. 0 [] -c1_1(a595)| -hskp9. 0 [] -hskp8|c3_1(a593). 0 [] -hskp8| -c2_1(a593). 0 [] -hskp8|c1_1(a593). 0 [] -hskp8|ndr1_0. 0 [] -hskp7|ndr1_0. 0 [] -hskp7| -c0_1(a592). 0 [] -hskp7| -c3_1(a592). 0 [] -hskp7|c2_1(a592). 0 [] -hskp6| -c0_1(a590). 0 [] -hskp6|c3_1(a590). 0 [] -hskp6|c2_1(a590). 0 [] -hskp6|ndr1_0. 0 [] -hskp5|c0_1(a589). 0 [] -hskp5| -c2_1(a589). 0 [] -hskp5|c1_1(a589). 0 [] -hskp5|ndr1_0. 0 [] ndr1_0| -hskp4. 0 [] c0_1(a588)| -hskp4. 0 [] -c1_1(a588)| -hskp4. 0 [] -c2_1(a588)| -hskp4. 0 [] -hskp2|c2_1(a586). 0 [] -hskp2| -c3_1(a586). 0 [] -hskp2|c1_1(a586). 0 [] -hskp2|ndr1_0. end_of_list. SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=10. This is a non-Horn set without equality. The strategy will be ordered hyper_res, unit deletion, and factoring, with satellites in sos and with nuclei in usable. dependent: set(hyper_res). dependent: set(factor). dependent: set(unit_deletion). ------------> process usable: ** KEPT (pick-wt=3): 1 [] c1_1(a584)| -hskp0. ** KEPT (pick-wt=3): 2 [] -c0_1(a584)| -hskp0. ** KEPT (pick-wt=3): 3 [] -c2_1(a584)| -hskp0. ** KEPT (pick-wt=2): 4 [] ndr1_0| -hskp0. ** KEPT (pick-wt=3): 5 [] -hskp1|c2_1(a585). ** KEPT (pick-wt=3): 6 [] -hskp1| -c0_1(a585). ** KEPT (pick-wt=3): 7 [] -hskp1|c1_1(a585). ** KEPT (pick-wt=2): 8 [] -hskp1|ndr1_0. ** KEPT (pick-wt=3): 9 [] -hskp3|c2_1(a587). ** KEPT (pick-wt=3): 10 [] -hskp3| -c1_1(a587). ** KEPT (pick-wt=3): 11 [] -hskp3|c0_1(a587). ** KEPT (pick-wt=2): 12 [] -hskp3|ndr1_0. ** KEPT (pick-wt=2): 13 [] ndr1_0| -hskp11. ** KEPT (pick-wt=3): 14 [] -c1_1(a599)| -hskp11. ** KEPT (pick-wt=3): 15 [] c3_1(a599)| -hskp11. ** KEPT (pick-wt=3): 16 [] c2_1(a599)| -hskp11. ** KEPT (pick-wt=3): 17 [] -hskp12|c0_1(a600). ** KEPT (pick-wt=3): 18 [] -hskp12| -c3_1(a600). ** KEPT (pick-wt=3): 19 [] -hskp12|c2_1(a600). ** KEPT (pick-wt=2): 20 [] -hskp12|ndr1_0. ** KEPT (pick-wt=2): 21 [] ndr1_0| -hskp14. ** KEPT (pick-wt=3): 22 [] c0_1(a603)| -hskp14. ** KEPT (pick-wt=3): 23 [] -c3_1(a603)| -hskp14. ** KEPT (pick-wt=3): 24 [] -c1_1(a603)| -hskp14. ** KEPT (pick-wt=3): 25 [] c1_1(a604)| -hskp15. ** KEPT (pick-wt=3): 26 [] -c0_1(a604)| -hskp15. ** KEPT (pick-wt=3): 27 [] c3_1(a604)| -hskp15. ** KEPT (pick-wt=2): 28 [] ndr1_0| -hskp15. ** KEPT (pick-wt=2): 29 [] ndr1_0| -hskp17. ** KEPT (pick-wt=3): 30 [] c3_1(a607)| -hskp17. ** KEPT (pick-wt=3): 31 [] -c2_1(a607)| -hskp17. ** KEPT (pick-wt=3): 32 [] -c1_1(a607)| -hskp17. ** KEPT (pick-wt=3): 33 [] c3_1(a610)| -hskp18. ** KEPT (pick-wt=3): 34 [] -c0_1(a610)| -hskp18. ** KEPT (pick-wt=3): 35 [] -c2_1(a610)| -hskp18. ** KEPT (pick-wt=2): 36 [] ndr1_0| -hskp18. ** KEPT (pick-wt=3): 37 [] -hskp19| -c1_1(a617). ** KEPT (pick-wt=3): 38 [] -hskp19| -c0_1(a617). ** KEPT (pick-wt=3): 39 [] -hskp19|c2_1(a617). ** KEPT (pick-wt=2): 40 [] -hskp19|ndr1_0. ** KEPT (pick-wt=3): 41 [] -hskp21| -c2_1(a629). ** KEPT (pick-wt=3): 42 [] -hskp21| -c3_1(a629). ** KEPT (pick-wt=3): 43 [] -hskp21|c0_1(a629). ** KEPT (pick-wt=2): 44 [] -hskp21|ndr1_0. ** KEPT (pick-wt=3): 45 [] -c3_1(a633)| -hskp22. ** KEPT (pick-wt=3): 46 [] -c0_1(a633)| -hskp22. ** KEPT (pick-wt=3): 47 [] c1_1(a633)| -hskp22. ** KEPT (pick-wt=2): 48 [] ndr1_0| -hskp22. ** KEPT (pick-wt=2): 49 [] ndr1_0| -hskp23. ** KEPT (pick-wt=3): 50 [] -c1_1(a636)| -hskp23. ** KEPT (pick-wt=3): 51 [] -c0_1(a636)| -hskp23. ** KEPT (pick-wt=3): 52 [] c3_1(a636)| -hskp23. ** KEPT (pick-wt=3): 53 [] -hskp25| -c1_1(a651). ** KEPT (pick-wt=3): 54 [] -hskp25| -c3_1(a651). ** KEPT (pick-wt=3): 55 [] -hskp25|c2_1(a651). ** KEPT (pick-wt=2): 56 [] -hskp25|ndr1_0. ** KEPT (pick-wt=3): 57 [] -hskp26|c0_1(a583). ** KEPT (pick-wt=3): 58 [] -hskp26|c2_1(a583). ** KEPT (pick-wt=3): 59 [] -hskp26|c1_1(a583). ** KEPT (pick-wt=2): 60 [] -hskp26|ndr1_0. ** KEPT (pick-wt=3): 61 [] c0_1(a678)| -hskp29. ** KEPT (pick-wt=3): 62 [] c2_1(a678)| -hskp29. ** KEPT (pick-wt=3): 63 [] c3_1(a678)| -hskp29. ** KEPT (pick-wt=2): 64 [] ndr1_0| -hskp29. ** KEPT (pick-wt=14): 65 [] hskp1| -ndr1_0| -c3_1(A)| -c1_1(A)|c0_1(A)|c0_1(B)|c3_1(B)|c1_1(B). ** KEPT (pick-wt=14): 66 [] -ndr1_0|c1_1(A)| -c2_1(A)|c3_1(A)|hskp2|c0_1(B)|c3_1(B)|c1_1(B). ** KEPT (pick-wt=19): 67 [] -ndr1_0|c0_1(A)|c1_1(A)| -c2_1(A)|c0_1(B)| -c2_1(B)| -c3_1(B)| -c1_1(C)| -c3_1(C)| -c0_1(C). ** KEPT (pick-wt=9): 68 [] -ndr1_0| -c3_1(A)|c1_1(A)|c0_1(A)|hskp6|hskp8. ** KEPT (pick-wt=19): 69 [] -ndr1_0| -c0_1(A)|c2_1(A)|c1_1(A)| -c3_1(B)| -c1_1(B)|c0_1(B)|c3_1(C)|c2_1(C)|c0_1(C). ** KEPT (pick-wt=19): 70 [] -ndr1_0|c0_1(A)| -c3_1(A)| -c2_1(A)|c1_1(B)| -c3_1(B)| -c2_1(B)|c3_1(C)|c2_1(C)|c0_1(C). ** KEPT (pick-wt=14): 71 [] -ndr1_0|c1_1(A)| -c0_1(A)|c2_1(A)|hskp10|c3_1(B)|c2_1(B)|c0_1(B). ** KEPT (pick-wt=14): 72 [] -ndr1_0|c3_1(A)|c2_1(A)|c0_1(A)| -c0_1(B)| -c2_1(B)| -c3_1(B)|hskp11. ** KEPT (pick-wt=9): 73 [] -ndr1_0|c0_1(A)|c3_1(A)|c2_1(A)|hskp12|hskp13. ** KEPT (pick-wt=14): 74 [] hskp16| -ndr1_0|c1_1(A)| -c2_1(A)|c3_1(A)|c0_1(B)|c2_1(B)| -c1_1(B). ** KEPT (pick-wt=14): 75 [] -ndr1_0|c0_1(A)|c2_1(A)| -c1_1(A)|hskp17|c1_1(B)| -c2_1(B)| -c0_1(B). ** KEPT (pick-wt=14): 76 [] -ndr1_0| -c3_1(A)|c2_1(A)|c0_1(A)|hskp18|c1_1(B)|c3_1(B)| -c0_1(B). ** KEPT (pick-wt=14): 77 [] -ndr1_0|c0_1(A)| -c3_1(A)|c2_1(A)| -c0_1(B)| -c1_1(B)|c2_1(B)|hskp27. ** KEPT (pick-wt=14): 78 [] -ndr1_0|c0_1(A)|c2_1(A)| -c3_1(A)|hskp28|c3_1(B)| -c0_1(B)| -c2_1(B). ** KEPT (pick-wt=19): 79 [] -ndr1_0| -c1_1(A)|c3_1(A)|c0_1(A)|c3_1(B)| -c0_1(B)| -c2_1(B)| -c2_1(C)| -c3_1(C)|c1_1(C). ** KEPT (pick-wt=14): 80 [] -ndr1_0| -c2_1(A)|c3_1(A)|c0_1(A)|c1_1(B)| -c0_1(B)|c2_1(B)|hskp14. ** KEPT (pick-wt=9): 81 [] -ndr1_0| -c2_1(A)|c3_1(A)|c0_1(A)|hskp8|hskp18. ** KEPT (pick-wt=19): 82 [] -ndr1_0| -c2_1(A)| -c1_1(A)|c0_1(A)| -c3_1(B)|c2_1(B)|c1_1(B)| -c0_1(C)| -c3_1(C)| -c2_1(C). ** KEPT (pick-wt=14): 83 [] -ndr1_0|c0_1(A)| -c1_1(A)| -c2_1(A)|hskp12| -c2_1(B)| -c1_1(B)| -c0_1(B). ** KEPT (pick-wt=14): 84 [] -ndr1_0| -c1_1(A)| -c3_1(A)|c0_1(A)|hskp16| -c1_1(B)| -c0_1(B)|c3_1(B). ** KEPT (pick-wt=14): 85 [] -ndr1_0|c0_1(A)| -c1_1(A)| -c3_1(A)|hskp15|c3_1(B)| -c1_1(B)| -c2_1(B). ** KEPT (pick-wt=9): 86 [] -ndr1_0| -c3_1(A)| -c1_1(A)|c0_1(A)|hskp7|hskp20. ** KEPT (pick-wt=14): 87 [] hskp16| -ndr1_0|c2_1(A)| -c0_1(A)|c3_1(A)|c0_1(B)| -c3_1(B)| -c2_1(B). ** KEPT (pick-wt=14): 88 [] hskp26| -ndr1_0|c1_1(A)| -c2_1(A)| -c0_1(A)|c1_1(B)|c3_1(B)|c2_1(B). ** KEPT (pick-wt=14): 89 [] -ndr1_0| -c0_1(A)|c2_1(A)|c1_1(A)|hskp1| -c0_1(B)| -c2_1(B)|c3_1(B). ** KEPT (pick-wt=14): 90 [] -ndr1_0|c1_1(A)| -c3_1(A)|c2_1(A)|hskp3|c3_1(B)| -c0_1(B)|c1_1(B). ** KEPT (pick-wt=19): 91 [] -ndr1_0| -c3_1(A)|c2_1(A)|c1_1(A)|c2_1(B)| -c1_1(B)| -c0_1(B)| -c0_1(C)| -c2_1(C)| -c3_1(C). ** KEPT (pick-wt=14): 92 [] -ndr1_0|c2_1(A)| -c3_1(A)|c1_1(A)|hskp23|c2_1(B)| -c3_1(B)| -c0_1(B). ** KEPT (pick-wt=14): 93 [] hskp28| -ndr1_0|c3_1(A)| -c2_1(A)| -c1_1(A)|c1_1(B)| -c3_1(B)| -c2_1(B). ** KEPT (pick-wt=9): 94 [] hskp23|hskp14| -ndr1_0| -c2_1(A)| -c3_1(A)|c1_1(A). ** KEPT (pick-wt=14): 95 [] -ndr1_0|c3_1(A)| -c2_1(A)| -c0_1(A)|hskp8|c2_1(B)| -c0_1(B)|c3_1(B). ** KEPT (pick-wt=9): 96 [] -ndr1_0|c2_1(A)| -c0_1(A)|c3_1(A)|hskp16|hskp3. ** KEPT (pick-wt=9): 97 [] hskp6|hskp8| -ndr1_0|c2_1(A)|c3_1(A)| -c1_1(A). ** KEPT (pick-wt=9): 98 [] -ndr1_0|c2_1(A)| -c0_1(A)| -c3_1(A)|hskp26|hskp28. ** KEPT (pick-wt=9): 99 [] -ndr1_0| -c3_1(A)| -c0_1(A)|c2_1(A)|hskp15|hskp11. ** KEPT (pick-wt=9): 100 [] -ndr1_0| -c1_1(A)| -c3_1(A)|c2_1(A)|hskp3|hskp17. ** KEPT (pick-wt=9): 101 [] -ndr1_0|c3_1(A)| -c1_1(A)| -c0_1(A)|hskp3|hskp17. ** KEPT (pick-wt=9): 102 [] -ndr1_0|c3_1(A)| -c2_1(A)| -c0_1(A)|hskp8|hskp27. ** KEPT (pick-wt=9): 103 [] -ndr1_0| -c1_1(A)| -c2_1(A)| -c3_1(A)|hskp1|hskp10. ** KEPT (pick-wt=9): 104 [] -ndr1_0| -c0_1(A)| -c2_1(A)| -c3_1(A)|hskp12|hskp10. ** KEPT (pick-wt=9): 105 [] -ndr1_0| -c0_1(A)| -c1_1(A)| -c3_1(A)|hskp19|hskp20. ** KEPT (pick-wt=9): 106 [] -ndr1_0| -c1_1(A)| -c3_1(A)| -c0_1(A)|hskp29|hskp14. ** KEPT (pick-wt=14): 107 [] -ndr1_0| -c2_1(A)| -c1_1(A)| -c0_1(A)| -c2_1(B)| -c3_1(B)| -c1_1(B)|hskp10. ** KEPT (pick-wt=9): 108 [] -ndr1_0|c3_1(A)| -c2_1(A)| -c1_1(A)|hskp18|hskp29. ** KEPT (pick-wt=9): 109 [] -ndr1_0|c3_1(A)| -c1_1(A)| -c2_1(A)|hskp15|hskp29. ** KEPT (pick-wt=9): 110 [] hskp7|hskp20| -ndr1_0| -c0_1(A)| -c2_1(A)|c3_1(A). ** KEPT (pick-wt=9): 111 [] -ndr1_0| -c0_1(A)| -c2_1(A)|c3_1(A)|hskp14|hskp22. ** KEPT (pick-wt=9): 112 [] hskp4|hskp17| -ndr1_0| -c0_1(A)| -c1_1(A)|c3_1(A). ** KEPT (pick-wt=14): 113 [] -ndr1_0| -c3_1(A)| -c2_1(A)| -c0_1(A)|hskp14|c2_1(B)| -c1_1(B)| -c3_1(B). ** KEPT (pick-wt=9): 114 [] -ndr1_0| -c0_1(A)| -c3_1(A)|c2_1(A)|hskp21|hskp8. ** KEPT (pick-wt=9): 115 [] hskp24|hskp5| -ndr1_0| -c3_1(A)| -c0_1(A)|c2_1(A). ** KEPT (pick-wt=9): 116 [] -ndr1_0| -c0_1(A)| -c1_1(A)|c2_1(A)|hskp11|hskp0. ** KEPT (pick-wt=9): 117 [] hskp25|hskp15| -ndr1_0|c2_1(A)| -c0_1(A)| -c1_1(A). ** KEPT (pick-wt=9): 118 [] hskp25|hskp9| -ndr1_0|c2_1(A)| -c1_1(A)|c3_1(A). ** KEPT (pick-wt=14): 119 [] -ndr1_0| -c1_1(A)|c3_1(A)|c2_1(A)|c2_1(B)| -c1_1(B)| -c0_1(B)|hskp24. ** KEPT (pick-wt=9): 120 [] -ndr1_0|c1_1(A)| -c3_1(A)| -c0_1(A)|hskp11|hskp23. ** KEPT (pick-wt=14): 121 [] -ndr1_0| -c0_1(A)| -c1_1(A)| -c3_1(A)|hskp15| -c3_1(B)| -c0_1(B)|c1_1(B). ** KEPT (pick-wt=9): 122 [] -ndr1_0| -c2_1(A)|c3_1(A)|c1_1(A)|hskp3|hskp4. ** KEPT (pick-wt=9): 123 [] -ndr1_0|c2_1(A)| -c0_1(A)|c1_1(A)|hskp22|hskp6. ** KEPT (pick-wt=9): 124 [] -ndr1_0|c1_1(A)|c2_1(A)| -c0_1(A)|hskp28|hskp8. ** KEPT (pick-wt=9): 125 [] hskp21|hskp11| -ndr1_0|c2_1(A)| -c0_1(A)|c1_1(A). ** KEPT (pick-wt=9): 126 [] hskp4|hskp10| -ndr1_0| -c2_1(A)| -c3_1(A)|c0_1(A). ** KEPT (pick-wt=14): 127 [] hskp8| -ndr1_0|c2_1(A)| -c3_1(A)| -c0_1(A)| -c3_1(B)| -c1_1(B)|c0_1(B). ** KEPT (pick-wt=9): 128 [] -ndr1_0| -c1_1(A)| -c2_1(A)|c0_1(A)|hskp13|hskp19. ** KEPT (pick-wt=9): 129 [] hskp10|hskp7| -ndr1_0| -c1_1(A)|c2_1(A)|c0_1(A). ** KEPT (pick-wt=9): 130 [] hskp13|hskp15| -ndr1_0|c3_1(A)|c2_1(A)|c0_1(A). ** KEPT (pick-wt=9): 131 [] -ndr1_0|c3_1(A)|c2_1(A)|c0_1(A)|hskp14|hskp4. ** KEPT (pick-wt=14): 132 [] -ndr1_0| -c2_1(A)| -c1_1(A)| -c0_1(A)|hskp9|c1_1(B)| -c3_1(B)|c0_1(B). ** KEPT (pick-wt=14): 133 [] -ndr1_0| -c3_1(A)|c1_1(A)|c0_1(A)|c1_1(B)|c2_1(B)|c3_1(B)|hskp26. ** KEPT (pick-wt=14): 134 [] -ndr1_0|c0_1(A)| -c3_1(A)|c1_1(A)|hskp8|c0_1(B)| -c1_1(B)| -c2_1(B). ** KEPT (pick-wt=9): 135 [] -ndr1_0|c0_1(A)| -c2_1(A)|c1_1(A)|hskp2|hskp7. ** KEPT (pick-wt=9): 136 [] hskp5|hskp6| -ndr1_0| -c2_1(A)|c1_1(A)|c0_1(A). ** KEPT (pick-wt=9): 137 [] -ndr1_0|c1_1(A)|c3_1(A)|c0_1(A)|hskp4|hskp3. ** KEPT (pick-wt=19): 138 [] -ndr1_0|c0_1(A)|c3_1(A)|c1_1(A)| -c0_1(B)|c3_1(B)|c2_1(B)|c0_1(C)| -c1_1(C)|c2_1(C). ** KEPT (pick-wt=9): 139 [] hskp26|hskp0| -ndr1_0|c0_1(A)|c2_1(A)|c1_1(A). ** KEPT (pick-wt=3): 140 [] c1_1(a612)| -hskp28. ** KEPT (pick-wt=3): 141 [] c2_1(a612)| -hskp28. ** KEPT (pick-wt=3): 142 [] c3_1(a612)| -hskp28. ** KEPT (pick-wt=2): 143 [] ndr1_0| -hskp28. ** KEPT (pick-wt=2): 144 [] -hskp27|ndr1_0. ** KEPT (pick-wt=3): 145 [] -hskp27|c0_1(a611). ** KEPT (pick-wt=3): 146 [] -hskp27|c1_1(a611). ** KEPT (pick-wt=3): 147 [] -hskp27|c3_1(a611). ** KEPT (pick-wt=2): 148 [] -hskp24|ndr1_0. ** KEPT (pick-wt=3): 149 [] -hskp24|c0_1(a648). ** KEPT (pick-wt=3): 150 [] -hskp24| -c3_1(a648). ** KEPT (pick-wt=3): 151 [] -hskp24|c1_1(a648). ** KEPT (pick-wt=2): 152 [] ndr1_0| -hskp20. ** KEPT (pick-wt=3): 153 [] -c1_1(a623)| -hskp20. ** KEPT (pick-wt=3): 154 [] -c2_1(a623)| -hskp20. ** KEPT (pick-wt=3): 155 [] -c3_1(a623)| -hskp20. ** KEPT (pick-wt=3): 156 [] c1_1(a606)| -hskp16. ** KEPT (pick-wt=3): 157 [] -c2_1(a606)| -hskp16. ** KEPT (pick-wt=3): 158 [] -c3_1(a606)| -hskp16. ** KEPT (pick-wt=2): 159 [] ndr1_0| -hskp16. ** KEPT (pick-wt=3): 160 [] -hskp13| -c0_1(a601). ** KEPT (pick-wt=3): 161 [] -hskp13| -c2_1(a601). ** KEPT (pick-wt=3): 162 [] -hskp13| -c1_1(a601). ** KEPT (pick-wt=2): 163 [] -hskp13|ndr1_0. ** KEPT (pick-wt=3): 164 [] -hskp10|c0_1(a598). ** KEPT (pick-wt=3): 165 [] -hskp10|c3_1(a598). ** KEPT (pick-wt=3): 166 [] -hskp10| -c1_1(a598). ** KEPT (pick-wt=2): 167 [] -hskp10|ndr1_0. ** KEPT (pick-wt=2): 168 [] ndr1_0| -hskp9. ** KEPT (pick-wt=3): 169 [] -c0_1(a595)| -hskp9. ** KEPT (pick-wt=3): 170 [] -c3_1(a595)| -hskp9. ** KEPT (pick-wt=3): 171 [] -c1_1(a595)| -hskp9. ** KEPT (pick-wt=3): 172 [] -hskp8|c3_1(a593). ** KEPT (pick-wt=3): 173 [] -hskp8| -c2_1(a593). ** KEPT (pick-wt=3): 174 [] -hskp8|c1_1(a593). ** KEPT (pick-wt=2): 175 [] -hskp8|ndr1_0. ** KEPT (pick-wt=2): 176 [] -hskp7|ndr1_0. ** KEPT (pick-wt=3): 177 [] -hskp7| -c0_1(a592). ** KEPT (pick-wt=3): 178 [] -hskp7| -c3_1(a592). ** KEPT (pick-wt=3): 179 [] -hskp7|c2_1(a592). ** KEPT (pick-wt=3): 180 [] -hskp6| -c0_1(a590). ** KEPT (pick-wt=3): 181 [] -hskp6|c3_1(a590). ** KEPT (pick-wt=3): 182 [] -hskp6|c2_1(a590). ** KEPT (pick-wt=2): 183 [] -hskp6|ndr1_0. ** KEPT (pick-wt=3): 184 [] -hskp5|c0_1(a589). ** KEPT (pick-wt=3): 185 [] -hskp5| -c2_1(a589). ** KEPT (pick-wt=3): 186 [] -hskp5|c1_1(a589). ** KEPT (pick-wt=2): 187 [] -hskp5|ndr1_0. ** KEPT (pick-wt=2): 188 [] ndr1_0| -hskp4. ** KEPT (pick-wt=3): 189 [] c0_1(a588)| -hskp4. ** KEPT (pick-wt=3): 190 [] -c1_1(a588)| -hskp4. ** KEPT (pick-wt=3): 191 [] -c2_1(a588)| -hskp4. ** KEPT (pick-wt=3): 192 [] -hskp2|c2_1(a586). ** KEPT (pick-wt=3): 193 [] -hskp2| -c3_1(a586). ** KEPT (pick-wt=3): 194 [] -hskp2|c1_1(a586). ** KEPT (pick-wt=2): 195 [] -hskp2|ndr1_0. ------------> process sos: ** KEPT (pick-wt=3): 202 [] hskp26|hskp12|hskp8. ** KEPT (pick-wt=2): 203 [] hskp11|hskp26. ** KEPT (pick-wt=3): 204 [] hskp14|hskp0|hskp21. ** KEPT (pick-wt=3): 205 [] hskp17|hskp7|hskp29. ** KEPT (pick-wt=3): 206 [] hskp17|hskp22|hskp29. ======= end of input processing ======= =========== start of search =========== WATCH: 2.89 CPU 3.02 WC WATCH: 5.90 CPU 6.03 WC WATCH: 8.90 CPU 9.04 WC WATCH: 11.90 CPU 12.05 WC WATCH: 14.91 CPU 15.06 WC WATCH: 17.91 CPU 18.07 WC WATCH: 20.92 CPU 21.08 WC WATCH: 23.92 CPU 24.09 WC WATCH: 26.92 CPU 27.10 WC WATCH: 29.93 CPU 30.11 WC WATCH: 32.93 CPU 33.12 WC WATCH: 35.93 CPU 36.13 WC WATCH: 38.94 CPU 39.14 WC WATCH: 41.94 CPU 42.15 WC WATCH: 44.95 CPU 45.15 WC WATCH: 47.95 CPU 48.16 WC WATCH: 50.96 CPU 51.17 WC WATCH: 53.96 CPU 54.18 WC WATCH: 56.96 CPU 57.19 WC WATCH: 59.97 CPU 60.20 WC WATCH: 62.97 CPU 63.21 WC WATCH: 65.98 CPU 66.22 WC WATCH: 68.98 CPU 69.23 WC WATCH: 71.99 CPU 72.24 WC WATCH: 74.99 CPU 75.25 WC WATCH: 78.00 CPU 78.26 WC WATCH: 81.00 CPU 81.27 WC WATCH: 84.01 CPU 84.28 WC WATCH: 87.01 CPU 87.29 WC WATCH: 90.02 CPU 90.30 WC WATCH: 93.02 CPU 93.31 WC WATCH: 96.03 CPU 96.32 WC WATCH: 99.03 CPU 99.33 WC WATCH: 102.04 CPU 102.34 WC WATCH: 105.04 CPU 105.35 WC WATCH: 108.04 CPU 108.36 WC WATCH: 111.05 CPU 111.37 WC WATCH: 114.05 CPU 114.38 WC WATCH: 117.06 CPU 117.39 WC WATCH: 120.06 CPU 120.40 WC WATCH: 123.07 CPU 123.41 WC WATCH: 126.07 CPU 126.42 WC WATCH: 129.08 CPU 129.44 WC WATCH: 132.09 CPU 132.45 WC WATCH: 135.10 CPU 135.46 WC WATCH: 138.10 CPU 138.47 WC WATCH: 141.11 CPU 141.49 WC WATCH: 144.12 CPU 144.50 WC WATCH: 147.13 CPU 147.52 WC WATCH: 150.14 CPU 150.53 WC WATCH: 153.15 CPU 153.54 WC WATCH: 156.15 CPU 156.55 WC WATCH: 159.16 CPU 159.57 WC WATCH: 162.17 CPU 162.58 WC WATCH: 165.17 CPU 165.59 WC WATCH: 168.18 CPU 168.61 WC WATCH: 171.19 CPU 171.62 WC WATCH: 174.20 CPU 174.63 WC WATCH: 177.21 CPU 177.65 WC WATCH: 180.21 CPU 180.66 WC WATCH: 183.22 CPU 183.67 WC WATCH: 186.23 CPU 186.68 WC WATCH: 189.24 CPU 189.70 WC WATCH: 192.25 CPU 192.71 WC WATCH: 195.25 CPU 195.72 WC WATCH: 198.26 CPU 198.74 WC WATCH: 201.27 CPU 201.75 WC WATCH: 204.28 CPU 204.76 WC WATCH: 207.28 CPU 207.78 WC WATCH: 210.29 CPU 210.79 WC WATCH: 213.30 CPU 213.80 WC WATCH: 216.31 CPU 216.82 WC WATCH: 219.32 CPU 219.83 WC WATCH: 222.32 CPU 222.84 WC WATCH: 225.33 CPU 225.86 WC WATCH: 228.34 CPU 228.87 WC WATCH: 231.35 CPU 231.88 WC WATCH: 234.36 CPU 234.89 WC WATCH: 237.36 CPU 237.91 WC WATCH: 240.37 CPU 240.92 WC WATCH: 243.38 CPU 243.93 WC WATCH: 246.39 CPU 246.95 WC WATCH: 249.40 CPU 249.96 WC WATCH: 252.40 CPU 252.97 WC WATCH: 255.41 CPU 255.99 WC WATCH: 258.42 CPU 259.00 WC WATCH: 261.43 CPU 262.01 WC WATCH: 264.43 CPU 265.03 WC WATCH: 267.44 CPU 268.04 WC WATCH: 270.45 CPU 271.05 WC WATCH: 273.46 CPU 274.06 WC WATCH: 276.47 CPU 277.08 WC WATCH: 279.47 CPU 280.09 WC WATCH: 282.48 CPU 283.10 WC WATCH: 285.49 CPU 286.12 WC WATCH: 288.50 CPU 289.13 WC WATCH: 291.51 CPU 292.14 WC WATCH: 294.51 CPU 295.16 WC WATCH: 297.52 CPU 298.17 WC WATCH: 300.53 CPU 301.18 WC FINAL WATCH: 300.53 CPU 301.29 WC