%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN547+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n128.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 06:42:21 EDT 2016
% Result : CounterSatisfiable 127.03s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN547+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.23 % Computer : n128.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.75MB
% 0.02/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Sat Apr 9 00:16:24 CDT 2016
% 0.02/0.23 % CPUTime:
% 6.31/5.83 > val it = (): unit
% 7.02/6.59 Trying to find a model that refutes: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c4_1 U |
% 7.02/6.59 ((bnd_ndr1_1 U & ~ bnd_c4_2 U bnd_a456) &
% 7.02/6.59 bnd_c6_2 U bnd_a456) &
% 7.02/6.59 bnd_c8_2 U bnd_a456) |
% 7.02/6.59 ((bnd_ndr1_1 U & ~ bnd_c6_2 U bnd_a457) &
% 7.02/6.59 bnd_c7_2 U bnd_a457) &
% 7.02/6.59 bnd_c5_2 U bnd_a457) |
% 7.02/6.59 bnd_c2_0) |
% 7.02/6.59 ~ bnd_c7_0) &
% 7.02/6.59 (bnd_c2_0 | ~ bnd_c1_0)) &
% 7.02/6.59 ((~ bnd_c8_0 |
% 7.02/6.59 ((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a458) &
% 7.02/6.59 bnd_c4_1 bnd_a458) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a458) |
% 7.02/6.59 (ALL V.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c6_1 V | bnd_c2_1 V) |
% 7.02/6.59 (ALL W.
% 7.02/6.59 bnd_ndr1_1 V -->
% 7.02/6.59 bnd_c3_2 V W | ~ bnd_c7_2 V W)))) &
% 7.02/6.59 (((ALL X.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c3_1 X | ~ bnd_c8_1 X) |
% 7.02/6.59 ((bnd_ndr1_1 X & ~ bnd_c6_2 X bnd_a459) &
% 7.02/6.59 ~ bnd_c3_2 X bnd_a459) &
% 7.02/6.59 bnd_c7_2 X bnd_a459) |
% 7.02/6.59 ~ bnd_c6_0) |
% 7.02/6.59 (ALL Y.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((bnd_ndr1_1 Y & bnd_c8_2 Y bnd_a460) &
% 7.02/6.59 bnd_c5_2 Y bnd_a460) &
% 7.02/6.59 bnd_c1_2 Y bnd_a460))) &
% 7.02/6.59 (((ALL Z.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X1.
% 7.02/6.59 bnd_ndr1_1 Z -->
% 7.02/6.59 ~ bnd_c7_2 Z X1 | ~ bnd_c8_2 Z X1) |
% 7.02/6.59 ((bnd_ndr1_1 Z & ~ bnd_c7_2 Z bnd_a461) &
% 7.02/6.59 ~ bnd_c2_2 Z bnd_a461) &
% 7.02/6.59 ~ bnd_c4_2 Z bnd_a461) |
% 7.02/6.59 ~ bnd_c8_1 Z) |
% 7.02/6.59 bnd_c2_0) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 (((ALL X2.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X3.
% 7.02/6.59 bnd_ndr1_1 X2 -->
% 7.02/6.59 (~ bnd_c2_2 X2 X3 | bnd_c6_2 X2 X3) |
% 7.02/6.59 ~ bnd_c4_2 X2 X3) |
% 7.02/6.59 ((bnd_ndr1_1 X2 & ~ bnd_c1_2 X2 bnd_a462) &
% 7.02/6.59 ~ bnd_c7_2 X2 bnd_a462) &
% 7.02/6.59 ~ bnd_c6_2 X2 bnd_a462) |
% 7.02/6.59 ~ bnd_c8_1 X2) |
% 7.02/6.59 ~ bnd_c5_0) |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c7_1 bnd_a463) &
% 7.02/6.59 ~ bnd_c1_1 bnd_a463) &
% 7.02/6.59 ~ bnd_c5_1 bnd_a463)) &
% 7.02/6.59 ((bnd_c6_0 |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c2_1 bnd_a464) & bnd_c8_1 bnd_a464) &
% 7.02/6.59 ~ bnd_c7_1 bnd_a464) |
% 7.02/6.59 ~ bnd_c1_0)) &
% 7.02/6.59 (((ALL X4.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X5.
% 7.02/6.59 bnd_ndr1_1 X4 -->
% 7.02/6.59 (~ bnd_c6_2 X4 X5 | bnd_c5_2 X4 X5) |
% 7.02/6.59 ~ bnd_c7_2 X4 X5) |
% 7.02/6.59 ((bnd_ndr1_1 X4 & ~ bnd_c1_2 X4 bnd_a465) &
% 7.02/6.59 ~ bnd_c5_2 X4 bnd_a465) &
% 7.02/6.59 ~ bnd_c7_2 X4 bnd_a465) |
% 7.02/6.59 bnd_c8_1 X4) |
% 7.02/6.59 (ALL X6.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c8_1 X6 |
% 7.02/6.59 (ALL X7.
% 7.02/6.59 bnd_ndr1_1 X6 -->
% 7.02/6.59 (~ bnd_c6_2 X6 X7 | bnd_c1_2 X6 X7) |
% 7.02/6.59 ~ bnd_c2_2 X6 X7)) |
% 7.02/6.59 ~ bnd_c1_1 X6)) |
% 7.02/6.59 (ALL X8.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c1_1 X8 | bnd_c2_1 X8) |
% 7.02/6.59 (ALL X9.
% 7.02/6.59 bnd_ndr1_1 X8 -->
% 7.02/6.59 (bnd_c1_2 X8 X9 | bnd_c7_2 X8 X9) |
% 7.02/6.59 bnd_c3_2 X8 X9)))) &
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c1_1 bnd_a466) & ~ bnd_c8_1 bnd_a466 |
% 7.02/6.59 ~ bnd_c2_0)) &
% 7.02/6.59 (bnd_c8_0 | ~ bnd_c5_0)) &
% 7.02/6.59 ((ALL X10.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X11.
% 7.02/6.59 bnd_ndr1_1 X10 -->
% 7.02/6.59 (bnd_c8_2 X10 X11 | ~ bnd_c4_2 X10 X11) |
% 7.02/6.59 ~ bnd_c7_2 X10 X11) |
% 7.02/6.59 bnd_c8_1 X10) |
% 7.02/6.59 ~ bnd_c2_1 X10) |
% 7.02/6.59 (ALL X12.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X12 & bnd_c8_2 X12 bnd_a467) &
% 7.02/6.59 bnd_c2_2 X12 bnd_a467) &
% 7.02/6.59 bnd_c3_2 X12 bnd_a467 |
% 7.02/6.59 ~ bnd_c6_1 X12) |
% 7.02/6.59 ~ bnd_c8_1 X12))) &
% 7.02/6.59 (~ bnd_c4_0 |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c6_1 bnd_a468) & ~ bnd_c4_1 bnd_a468) &
% 7.02/6.59 ~ bnd_c3_1 bnd_a468)) &
% 7.02/6.59 (((ALL X13.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X13 & bnd_c2_2 X13 bnd_a469) &
% 7.02/6.59 ~ bnd_c8_2 X13 bnd_a469) &
% 7.02/6.59 ~ bnd_c6_2 X13 bnd_a469 |
% 7.02/6.59 (ALL X14.
% 7.02/6.59 bnd_ndr1_1 X13 -->
% 7.02/6.59 (bnd_c3_2 X13 X14 | ~ bnd_c6_2 X13 X14) |
% 7.02/6.59 ~ bnd_c2_2 X13 X14)) |
% 7.02/6.59 bnd_c8_1 X13) |
% 7.02/6.59 bnd_c6_0) |
% 7.02/6.59 bnd_c2_0)) &
% 7.02/6.59 ((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X15.
% 7.02/6.59 bnd_ndr1_1 bnd_a470 -->
% 7.02/6.59 (~ bnd_c1_2 bnd_a470 X15 | bnd_c7_2 bnd_a470 X15) |
% 7.02/6.59 ~ bnd_c4_2 bnd_a470 X15)) &
% 7.02/6.59 bnd_c7_1 bnd_a470) &
% 7.02/6.59 (ALL X16.
% 7.02/6.59 bnd_ndr1_1 bnd_a470 -->
% 7.02/6.59 ~ bnd_c8_2 bnd_a470 X16 | bnd_c7_2 bnd_a470 X16) |
% 7.02/6.59 bnd_c8_0) |
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a471) & bnd_ndr1_1 bnd_a471) &
% 7.02/6.59 bnd_c7_2 bnd_a471 bnd_a472) &
% 7.02/6.59 ~ bnd_c5_2 bnd_a471 bnd_a472) &
% 7.02/6.59 (ALL X17.
% 7.02/6.59 bnd_ndr1_1 bnd_a471 -->
% 7.02/6.59 (bnd_c3_2 bnd_a471 X17 | bnd_c1_2 bnd_a471 X17) |
% 7.02/6.59 bnd_c6_2 bnd_a471 X17))) &
% 7.02/6.59 bnd_c3_0) &
% 7.02/6.59 ((~ bnd_c7_0 |
% 7.02/6.59 (ALL X18.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((bnd_ndr1_1 X18 & bnd_c8_2 X18 bnd_a473) &
% 7.02/6.59 bnd_c4_2 X18 bnd_a473) &
% 7.02/6.59 ~ bnd_c3_2 X18 bnd_a473 |
% 7.02/6.59 ~ bnd_c3_1 X18)) |
% 7.02/6.59 (ALL X19.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (ALL X20.
% 7.02/6.59 bnd_ndr1_1 X19 -->
% 7.02/6.59 (~ bnd_c8_2 X19 X20 | ~ bnd_c4_2 X19 X20) |
% 7.02/6.59 ~ bnd_c1_2 X19 X20)))) &
% 7.02/6.59 (((ALL X21.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((bnd_ndr1_1 X21 & bnd_c6_2 X21 bnd_a474) &
% 7.02/6.59 bnd_c7_2 X21 bnd_a474) &
% 7.02/6.59 bnd_c1_2 X21 bnd_a474 |
% 7.02/6.59 ~ bnd_c5_1 X21) |
% 7.02/6.59 (ALL X22.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c6_1 X22 | ~ bnd_c7_1 X22) |
% 7.02/6.59 (ALL X23.
% 7.02/6.59 bnd_ndr1_1 X22 -->
% 7.02/6.59 (bnd_c1_2 X22 X23 | bnd_c4_2 X22 X23) |
% 7.02/6.59 ~ bnd_c6_2 X22 X23))) |
% 7.02/6.59 (ALL X24.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X25.
% 7.02/6.59 bnd_ndr1_1 X24 -->
% 7.02/6.59 (bnd_c4_2 X24 X25 | ~ bnd_c6_2 X24 X25) |
% 7.02/6.59 ~ bnd_c3_2 X24 X25) |
% 7.02/6.59 bnd_c8_1 X24) |
% 7.02/6.59 ~ bnd_c3_1 X24))) &
% 7.02/6.59 ((((((((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X26.
% 7.02/6.59 bnd_ndr1_1 bnd_a475 -->
% 7.02/6.59 (~ bnd_c8_2 bnd_a475 X26 | bnd_c4_2 bnd_a475 X26) |
% 7.02/6.59 bnd_c5_2 bnd_a475 X26)) &
% 7.02/6.59 bnd_ndr1_1 bnd_a475) &
% 7.02/6.59 bnd_c5_2 bnd_a475 bnd_a476) &
% 7.02/6.59 ~ bnd_c3_2 bnd_a475 bnd_a476) &
% 7.02/6.59 bnd_c7_2 bnd_a475 bnd_a476) &
% 7.02/6.59 bnd_ndr1_1 bnd_a475) &
% 7.02/6.59 bnd_c4_2 bnd_a475 bnd_a477) &
% 7.02/6.59 bnd_c6_2 bnd_a475 bnd_a477) &
% 7.02/6.59 bnd_c7_2 bnd_a475 bnd_a477 |
% 7.02/6.59 bnd_c7_0) |
% 7.02/6.59 ~ bnd_c2_0)) &
% 7.02/6.59 (((ALL X27.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X27 & ~ bnd_c4_2 X27 bnd_a478) &
% 7.02/6.59 bnd_c7_2 X27 bnd_a478) &
% 7.02/6.59 ~ bnd_c5_2 X27 bnd_a478 |
% 7.02/6.59 ~ bnd_c3_1 X27) |
% 7.02/6.59 (ALL X28.
% 7.02/6.59 bnd_ndr1_1 X27 -->
% 7.02/6.59 ~ bnd_c6_2 X27 X28 | ~ bnd_c1_2 X27 X28)) |
% 7.02/6.59 bnd_c2_0) |
% 7.02/6.59 ~ bnd_c1_0)) &
% 7.02/6.59 ((~ bnd_c6_0 |
% 7.02/6.59 (ALL X29.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X30.
% 7.02/6.59 bnd_ndr1_1 X29 -->
% 7.02/6.59 (bnd_c3_2 X29 X30 | bnd_c1_2 X29 X30) |
% 7.02/6.59 ~ bnd_c8_2 X29 X30) |
% 7.02/6.59 ~ bnd_c8_1 X29) |
% 7.02/6.59 (bnd_ndr1_1 X29 & bnd_c6_2 X29 bnd_a479) &
% 7.02/6.59 ~ bnd_c7_2 X29 bnd_a479)) |
% 7.02/6.59 (ALL X31.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X31 & bnd_c3_2 X31 bnd_a480) &
% 7.02/6.59 bnd_c4_2 X31 bnd_a480) &
% 7.02/6.59 ~ bnd_c6_2 X31 bnd_a480 |
% 7.02/6.59 bnd_c3_1 X31) |
% 7.02/6.59 ~ bnd_c2_1 X31))) &
% 7.02/6.59 ((bnd_c5_0 |
% 7.02/6.59 (ALL X32.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X33.
% 7.02/6.59 bnd_ndr1_1 X32 -->
% 7.02/6.59 (bnd_c4_2 X32 X33 | ~ bnd_c6_2 X32 X33) |
% 7.02/6.59 ~ bnd_c3_2 X32 X33) |
% 7.02/6.59 bnd_c8_1 X32) |
% 7.02/6.59 (bnd_ndr1_1 X32 & bnd_c2_2 X32 bnd_a481) &
% 7.02/6.59 bnd_c8_2 X32 bnd_a481)) |
% 7.02/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a482) &
% 7.02/6.59 bnd_c3_2 bnd_a482 bnd_a483) &
% 7.02/6.59 bnd_c2_2 bnd_a482 bnd_a483) &
% 7.02/6.59 bnd_c8_2 bnd_a482 bnd_a483) &
% 7.02/6.59 (ALL X34.
% 7.02/6.59 bnd_ndr1_1 bnd_a482 -->
% 7.02/6.59 (bnd_c2_2 bnd_a482 X34 | ~ bnd_c6_2 bnd_a482 X34) |
% 7.02/6.59 ~ bnd_c8_2 bnd_a482 X34)) &
% 7.02/6.59 bnd_ndr1_1 bnd_a482) &
% 7.02/6.59 bnd_c5_2 bnd_a482 bnd_a484) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a482 bnd_a484) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a482 bnd_a484)) &
% 7.02/6.59 (((ALL X35.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c8_1 X35 |
% 7.02/6.59 ((bnd_ndr1_1 X35 & ~ bnd_c2_2 X35 bnd_a485) &
% 7.02/6.59 ~ bnd_c3_2 X35 bnd_a485) &
% 7.02/6.59 ~ bnd_c1_2 X35 bnd_a485) |
% 7.02/6.59 ((bnd_ndr1_1 X35 & bnd_c6_2 X35 bnd_a486) &
% 7.02/6.59 bnd_c1_2 X35 bnd_a486) &
% 7.02/6.59 bnd_c5_2 X35 bnd_a486) |
% 7.02/6.59 ~ bnd_c5_0) |
% 7.02/6.59 bnd_c7_0)) &
% 7.02/6.59 (((ALL X36.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c2_1 X36 | bnd_c5_1 X36) |
% 7.02/6.59 (bnd_ndr1_1 X36 & bnd_c1_2 X36 bnd_a487) & bnd_c4_2 X36 bnd_a487) |
% 7.02/6.59 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a488) & bnd_c4_1 bnd_a488) &
% 7.02/6.59 (ALL X37.
% 7.02/6.59 bnd_ndr1_1 bnd_a488 -->
% 7.02/6.59 (~ bnd_c6_2 bnd_a488 X37 | bnd_c2_2 bnd_a488 X37) |
% 7.02/6.59 bnd_c5_2 bnd_a488 X37)) |
% 7.02/6.59 bnd_c1_0)) &
% 7.02/6.59 (((ALL X38.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c4_1 X38 |
% 7.02/6.59 ((bnd_ndr1_1 X38 & bnd_c4_2 X38 bnd_a489) &
% 7.02/6.59 ~ bnd_c8_2 X38 bnd_a489) &
% 7.02/6.59 ~ bnd_c3_2 X38 bnd_a489) |
% 7.02/6.59 (ALL X39.
% 7.02/6.59 bnd_ndr1_1 X38 -->
% 7.02/6.59 (bnd_c1_2 X38 X39 | bnd_c5_2 X38 X39) | ~ bnd_c8_2 X38 X39)) |
% 7.02/6.59 bnd_c8_0) |
% 7.02/6.59 ~ bnd_c7_0)) &
% 7.02/6.59 ((bnd_c5_0 |
% 7.02/6.59 (ALL X40.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c8_1 X40 | ~ bnd_c7_1 X40) |
% 7.02/6.59 ((bnd_ndr1_1 X40 & bnd_c4_2 X40 bnd_a490) & ~ bnd_c6_2 X40 bnd_a490) &
% 7.02/6.59 bnd_c7_2 X40 bnd_a490)) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 ((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a491) &
% 7.02/6.59 (ALL X41.
% 7.02/6.59 bnd_ndr1_1 bnd_a491 -->
% 7.02/6.59 (bnd_c6_2 bnd_a491 X41 | bnd_c4_2 bnd_a491 X41) |
% 7.02/6.59 bnd_c3_2 bnd_a491 X41)) &
% 7.02/6.59 ~ bnd_c5_1 bnd_a491 |
% 7.02/6.59 (ALL X42.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X43.
% 7.02/6.59 bnd_ndr1_1 X42 -->
% 7.02/6.59 (bnd_c3_2 X42 X43 | ~ bnd_c5_2 X42 X43) | ~ bnd_c8_2 X42 X43) |
% 7.02/6.59 ((bnd_ndr1_1 X42 & bnd_c4_2 X42 bnd_a492) & ~ bnd_c6_2 X42 bnd_a492) &
% 7.02/6.59 ~ bnd_c7_2 X42 bnd_a492) |
% 7.02/6.59 ((bnd_ndr1_1 X42 & ~ bnd_c6_2 X42 bnd_a493) & bnd_c1_2 X42 bnd_a493) &
% 7.02/6.59 ~ bnd_c2_2 X42 bnd_a493)) |
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a494) & bnd_ndr1_1 bnd_a494) &
% 7.02/6.59 ~ bnd_c3_2 bnd_a494 bnd_a495) &
% 7.02/6.59 bnd_c8_2 bnd_a494 bnd_a495) &
% 7.02/6.59 bnd_c4_1 bnd_a494)) &
% 7.02/6.59 ((bnd_c7_0 | bnd_c2_0) | bnd_c8_0)) &
% 7.02/6.59 ((~ bnd_c4_0 | ~ bnd_c6_0) |
% 7.02/6.59 (((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X44.
% 7.02/6.59 bnd_ndr1_1 bnd_a496 -->
% 7.02/6.59 (bnd_c3_2 bnd_a496 X44 | ~ bnd_c8_2 bnd_a496 X44) |
% 7.02/6.59 ~ bnd_c2_2 bnd_a496 X44)) &
% 7.02/6.59 bnd_ndr1_1 bnd_a496) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a496 bnd_a497) &
% 7.02/6.59 bnd_c3_2 bnd_a496 bnd_a497) &
% 7.02/6.59 bnd_c6_2 bnd_a496 bnd_a497) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a496)) &
% 7.02/6.59 ((bnd_c2_0 |
% 7.02/6.59 (ALL X45.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c5_1 X45 |
% 7.02/6.59 (ALL X46.
% 7.02/6.59 bnd_ndr1_1 X45 -->
% 7.02/6.59 (~ bnd_c7_2 X45 X46 | bnd_c2_2 X45 X46) | ~ bnd_c1_2 X45 X46)) |
% 7.02/6.59 (ALL X47.
% 7.02/6.59 bnd_ndr1_1 X45 -->
% 7.02/6.59 (bnd_c1_2 X45 X47 | ~ bnd_c5_2 X45 X47) | bnd_c2_2 X45 X47))) |
% 7.02/6.59 (ALL X48.
% 7.02/6.59 bnd_ndr1_0 --> (bnd_c1_1 X48 | bnd_c2_1 X48) | ~ bnd_c4_1 X48))) &
% 7.02/6.59 ((bnd_c1_0 | bnd_c2_0) |
% 7.02/6.59 ((((((((bnd_ndr1_0 &
% 7.02/6.59 bnd_ndr1_1 bnd_a498) &
% 7.02/6.59 bnd_c3_2 bnd_a498 bnd_a499) &
% 7.02/6.59 bnd_c7_2 bnd_a498 bnd_a499) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a498 bnd_a499) &
% 7.02/6.59 bnd_c7_1 bnd_a498) &
% 7.02/6.59 bnd_ndr1_1 bnd_a498) &
% 7.02/6.59 bnd_c8_2 bnd_a498 bnd_a500) &
% 7.02/6.59 bnd_c4_2 bnd_a498 bnd_a500) &
% 7.02/6.59 ~ bnd_c7_2 bnd_a498 bnd_a500)) &
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a501) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a501) &
% 7.02/6.59 ~ bnd_c8_1 bnd_a501 |
% 7.02/6.59 bnd_c7_0) |
% 7.02/6.59 (ALL X49.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X50.
% 7.02/6.59 bnd_ndr1_1 X49 -->
% 7.02/6.59 (bnd_c7_2 X49 X50 | bnd_c6_2 X49 X50) | bnd_c1_2 X49 X50) |
% 7.02/6.59 bnd_c1_1 X49) |
% 7.02/6.59 ~ bnd_c2_1 X49))) &
% 7.02/6.59 (((ALL X51.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X51 &
% 7.02/6.59 ~ bnd_c1_2 X51 bnd_a502) &
% 7.02/6.59 ~ bnd_c7_2 X51 bnd_a502) &
% 7.02/6.59 ~ bnd_c8_2 X51 bnd_a502 |
% 7.02/6.59 ((bnd_ndr1_1 X51 & ~ bnd_c3_2 X51 bnd_a503) & ~ bnd_c4_2 X51 bnd_a503) &
% 7.02/6.59 bnd_c1_2 X51 bnd_a503) |
% 7.02/6.59 ((bnd_ndr1_1 X51 &
% 7.02/6.59 ~ bnd_c5_2 X51 bnd_a504) &
% 7.02/6.59 bnd_c8_2 X51 bnd_a504) &
% 7.02/6.59 ~ bnd_c3_2 X51 bnd_a504) |
% 7.02/6.59 ((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a505) &
% 7.02/6.59 bnd_ndr1_1 bnd_a505) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a505 bnd_a506) &
% 7.02/6.59 bnd_c6_2 bnd_a505 bnd_a506) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a505 bnd_a506) |
% 7.02/6.59 ~ bnd_c4_0)) &
% 7.02/6.59 (((ALL X52.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ~ bnd_c6_1 X52 |
% 7.02/6.59 (bnd_ndr1_1 X52 &
% 7.02/6.59 ~ bnd_c2_2 X52 bnd_a507) &
% 7.02/6.59 bnd_c5_2 X52 bnd_a507) |
% 7.02/6.59 (ALL X53.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c8_1 X53 | ~ bnd_c1_1 X53) |
% 7.02/6.59 ~ bnd_c5_1 X53)) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 ((~ bnd_c6_0 |
% 7.02/6.59 (ALL X54.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ~ bnd_c4_1 X54 |
% 7.02/6.59 (ALL X55.
% 7.02/6.59 bnd_ndr1_1 X54 -->
% 7.02/6.59 (~ bnd_c4_2 X54 X55 | ~ bnd_c3_2 X54 X55) | ~ bnd_c7_2 X54 X55))) |
% 7.02/6.59 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a508) &
% 7.02/6.59 bnd_c1_1 bnd_a508)) &
% 7.02/6.59 ((~ bnd_c4_0 | bnd_c7_0) |
% 7.02/6.59 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a509) &
% 7.02/6.59 bnd_c4_2 bnd_a509 bnd_a510) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a509 bnd_a510) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a509 bnd_a510) &
% 7.02/6.59 bnd_ndr1_1 bnd_a509) &
% 7.02/6.59 ~ bnd_c5_2 bnd_a509 bnd_a511) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a509 bnd_a511) &
% 7.02/6.59 bnd_c3_2 bnd_a509 bnd_a511)) &
% 7.02/6.59 ((~ bnd_c5_0 | ~ bnd_c1_0) | ~ bnd_c8_0)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & bnd_c6_1 bnd_a512) &
% 7.02/6.59 bnd_ndr1_1 bnd_a512) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a512 bnd_a513) &
% 7.02/6.59 ~ bnd_c2_2 bnd_a512 bnd_a513) &
% 7.02/6.59 bnd_c3_2 bnd_a512 bnd_a513 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X56.
% 7.02/6.59 bnd_ndr1_1 bnd_a514 -->
% 7.02/6.59 (bnd_c6_2 bnd_a514 X56 |
% 7.02/6.59 ~ bnd_c4_2 bnd_a514 X56) |
% 7.02/6.59 ~ bnd_c8_2 bnd_a514 X56)) &
% 7.02/6.59 bnd_c5_1 bnd_a514) &
% 7.02/6.59 ~ bnd_c1_1 bnd_a514) |
% 7.02/6.59 (ALL X57.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X57 &
% 7.02/6.59 ~ bnd_c2_2 X57 bnd_a515) &
% 7.02/6.59 bnd_c7_2 X57 bnd_a515) &
% 7.02/6.59 ~ bnd_c3_2 X57 bnd_a515 |
% 7.02/6.59 (bnd_ndr1_1 X57 & ~ bnd_c6_2 X57 bnd_a516) &
% 7.02/6.59 ~ bnd_c2_2 X57 bnd_a516) |
% 7.02/6.59 (ALL X58.
% 7.02/6.59 bnd_ndr1_1 X57 -->
% 7.02/6.59 bnd_c5_2 X57 X58 |
% 7.02/6.59 ~ bnd_c4_2 X57 X58)))) &
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c6_1 bnd_a517) &
% 7.02/6.59 bnd_c4_1 bnd_a517) &
% 7.02/6.59 bnd_c2_1 bnd_a517 |
% 7.02/6.59 bnd_c8_0) |
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a518) &
% 7.02/6.59 bnd_c7_2 bnd_a518 bnd_a519) &
% 7.02/6.59 bnd_c5_2 bnd_a518 bnd_a519) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a518 bnd_a519) &
% 7.02/6.59 bnd_c5_1 bnd_a518)) &
% 7.02/6.59 ((ALL X59.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c1_1 X59 | bnd_c7_1 X59) |
% 7.02/6.59 ~ bnd_c3_1 X59) |
% 7.02/6.59 ~ bnd_c5_0)) &
% 7.02/6.59 ((bnd_c5_0 |
% 7.02/6.59 (((((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a520) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a520) &
% 7.02/6.59 bnd_ndr1_1 bnd_a520) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a520 bnd_a521) &
% 7.02/6.59 bnd_c2_2 bnd_a520 bnd_a521) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a520 bnd_a521) |
% 7.02/6.59 bnd_c1_0)) &
% 7.02/6.59 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a522) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a522 bnd_a523) &
% 7.02/6.59 bnd_c4_2 bnd_a522 bnd_a523) &
% 7.02/6.59 bnd_c1_2 bnd_a522 bnd_a523) &
% 7.02/6.59 bnd_ndr1_1 bnd_a522) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a522 bnd_a524) &
% 7.02/6.59 bnd_c6_2 bnd_a522 bnd_a524) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a522 bnd_a524) &
% 7.02/6.59 bnd_c6_1 bnd_a522 |
% 7.02/6.59 ~ bnd_c5_0) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 (((ALL X60.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c8_1 X60 | ~ bnd_c4_1 X60) |
% 7.02/6.59 (ALL X61.
% 7.02/6.59 bnd_ndr1_1 X60 -->
% 7.02/6.59 (bnd_c3_2 X60 X61 | ~ bnd_c6_2 X60 X61) |
% 7.02/6.59 ~ bnd_c4_2 X60 X61)) |
% 7.02/6.59 ~ bnd_c2_0) |
% 7.02/6.59 (ALL X62.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c3_1 X62 |
% 7.02/6.59 ((bnd_ndr1_1 X62 & bnd_c7_2 X62 bnd_a525) &
% 7.02/6.59 ~ bnd_c6_2 X62 bnd_a525) &
% 7.02/6.59 ~ bnd_c2_2 X62 bnd_a525) |
% 7.02/6.59 bnd_c6_1 X62))) &
% 7.02/6.59 (((ALL X63.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X63 & bnd_c7_2 X63 bnd_a526) &
% 7.02/6.59 ~ bnd_c3_2 X63 bnd_a526) &
% 7.02/6.59 bnd_c8_2 X63 bnd_a526 |
% 7.02/6.59 ((bnd_ndr1_1 X63 & ~ bnd_c2_2 X63 bnd_a527) &
% 7.02/6.59 ~ bnd_c1_2 X63 bnd_a527) &
% 7.02/6.59 bnd_c4_2 X63 bnd_a527) |
% 7.02/6.59 (ALL X64.
% 7.02/6.59 bnd_ndr1_1 X63 -->
% 7.02/6.59 (~ bnd_c1_2 X63 X64 | bnd_c3_2 X63 X64) |
% 7.02/6.59 bnd_c2_2 X63 X64)) |
% 7.02/6.59 ~ bnd_c4_0) |
% 7.02/6.59 (ALL X65.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X66.
% 7.02/6.59 bnd_ndr1_1 X65 -->
% 7.02/6.59 (bnd_c3_2 X65 X66 | ~ bnd_c7_2 X65 X66) |
% 7.02/6.59 bnd_c8_2 X65 X66) |
% 7.02/6.59 ((bnd_ndr1_1 X65 & bnd_c6_2 X65 bnd_a528) &
% 7.02/6.59 bnd_c2_2 X65 bnd_a528) &
% 7.02/6.59 ~ bnd_c5_2 X65 bnd_a528) |
% 7.02/6.59 bnd_c2_1 X65))) &
% 7.02/6.59 ((bnd_c2_0 |
% 7.02/6.59 (ALL X67.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c8_1 X67 |
% 7.02/6.59 ((bnd_ndr1_1 X67 & ~ bnd_c8_2 X67 bnd_a529) &
% 7.02/6.59 ~ bnd_c1_2 X67 bnd_a529) &
% 7.02/6.59 ~ bnd_c5_2 X67 bnd_a529) |
% 7.02/6.59 (ALL X68.
% 7.02/6.59 bnd_ndr1_1 X67 -->
% 7.02/6.59 bnd_c7_2 X67 X68 | bnd_c5_2 X67 X68))) |
% 7.02/6.59 ~ bnd_c5_0)) &
% 7.02/6.59 ((~ bnd_c2_0 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X69.
% 7.02/6.59 bnd_ndr1_1 bnd_a530 -->
% 7.02/6.59 (~ bnd_c6_2 bnd_a530 X69 |
% 7.02/6.59 bnd_c7_2 bnd_a530 X69) |
% 7.02/6.59 ~ bnd_c4_2 bnd_a530 X69)) &
% 7.02/6.59 (ALL X70.
% 7.02/6.59 bnd_ndr1_1 bnd_a530 -->
% 7.02/6.59 (~ bnd_c6_2 bnd_a530 X70 |
% 7.02/6.59 ~ bnd_c8_2 bnd_a530 X70) |
% 7.02/6.59 ~ bnd_c3_2 bnd_a530 X70)) &
% 7.02/6.59 (ALL X71.
% 7.02/6.59 bnd_ndr1_1 bnd_a530 -->
% 7.02/6.59 (bnd_c8_2 bnd_a530 X71 | bnd_c4_2 bnd_a530 X71) |
% 7.02/6.59 bnd_c7_2 bnd_a530 X71)) |
% 7.02/6.59 (ALL X72.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c8_1 X72 | ~ bnd_c6_1 X72) | bnd_c1_1 X72))) &
% 7.02/6.59 (((bnd_ndr1_0 & bnd_c4_1 bnd_a531) & ~ bnd_c5_1 bnd_a531) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a531 |
% 7.02/6.59 (ALL X73.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X74.
% 7.02/6.59 bnd_ndr1_1 X73 -->
% 7.02/6.59 (bnd_c3_2 X73 X74 | ~ bnd_c8_2 X73 X74) |
% 7.02/6.59 ~ bnd_c1_2 X73 X74) |
% 7.02/6.59 bnd_c5_1 X73) |
% 7.02/6.59 (ALL X75.
% 7.02/6.59 bnd_ndr1_1 X73 -->
% 7.02/6.59 (bnd_c3_2 X73 X75 | bnd_c6_2 X73 X75) |
% 7.02/6.59 ~ bnd_c7_2 X73 X75)))) &
% 7.02/6.59 (((ALL X76.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c2_1 X76 |
% 7.02/6.59 (ALL X77.
% 7.02/6.59 bnd_ndr1_1 X76 -->
% 7.02/6.59 (~ bnd_c6_2 X76 X77 | bnd_c7_2 X76 X77) |
% 7.02/6.59 ~ bnd_c2_2 X76 X77)) |
% 7.02/6.59 bnd_c4_1 X76) |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X78.
% 7.02/6.59 bnd_ndr1_1 bnd_a532 -->
% 7.02/6.59 (bnd_c7_2 bnd_a532 X78 | ~ bnd_c4_2 bnd_a532 X78) |
% 7.02/6.59 ~ bnd_c8_2 bnd_a532 X78)) &
% 7.02/6.59 bnd_c3_1 bnd_a532) &
% 7.02/6.59 bnd_c1_1 bnd_a532) |
% 7.02/6.59 bnd_ndr1_0 & ~ bnd_c3_1 bnd_a533)) &
% 7.02/6.59 (((((((bnd_ndr1_0 & bnd_c8_1 bnd_a534) &
% 7.02/6.59 bnd_ndr1_1 bnd_a534) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a534 bnd_a535) &
% 7.02/6.59 bnd_c4_2 bnd_a534 bnd_a535) &
% 7.02/6.59 bnd_c8_2 bnd_a534 bnd_a535) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a534 |
% 7.02/6.59 (ALL X79.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X80.
% 7.02/6.59 bnd_ndr1_1 X79 -->
% 7.02/6.59 (~ bnd_c1_2 X79 X80 | ~ bnd_c3_2 X79 X80) |
% 7.02/6.59 ~ bnd_c6_2 X79 X80) |
% 7.02/6.59 (ALL X81.
% 7.02/6.59 bnd_ndr1_1 X79 -->
% 7.02/6.59 (bnd_c1_2 X79 X81 | bnd_c7_2 X79 X81) |
% 7.02/6.59 ~ bnd_c2_2 X79 X81)) |
% 7.02/6.59 bnd_c6_1 X79)) |
% 7.02/6.59 ~ bnd_c8_0)) &
% 7.02/6.59 ((bnd_c1_0 | ~ bnd_c2_0) | bnd_c8_0)) &
% 7.02/6.59 ((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X82.
% 7.02/6.59 bnd_ndr1_1 bnd_a536 -->
% 7.02/6.59 (bnd_c3_2 bnd_a536 X82 | bnd_c5_2 bnd_a536 X82) |
% 7.02/6.59 ~ bnd_c7_2 bnd_a536 X82)) &
% 7.02/6.59 ~ bnd_c7_1 bnd_a536) &
% 7.02/6.59 bnd_c5_1 bnd_a536 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X83.
% 7.02/6.59 bnd_ndr1_1 bnd_a537 -->
% 7.02/6.59 (~ bnd_c3_2 bnd_a537 X83 | ~ bnd_c7_2 bnd_a537 X83) |
% 7.02/6.59 ~ bnd_c2_2 bnd_a537 X83)) &
% 7.02/6.59 ~ bnd_c5_1 bnd_a537) &
% 7.02/6.59 bnd_c4_1 bnd_a537) |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X84.
% 7.02/6.59 bnd_ndr1_1 bnd_a538 -->
% 7.02/6.59 (~ bnd_c7_2 bnd_a538 X84 | bnd_c2_2 bnd_a538 X84) |
% 7.02/6.59 bnd_c3_2 bnd_a538 X84)) &
% 7.02/6.59 (ALL X85.
% 7.02/6.59 bnd_ndr1_1 bnd_a538 -->
% 7.02/6.59 (bnd_c8_2 bnd_a538 X85 | bnd_c7_2 bnd_a538 X85) |
% 7.02/6.59 ~ bnd_c1_2 bnd_a538 X85)) &
% 7.02/6.59 bnd_c1_1 bnd_a538)) &
% 7.02/6.59 ((~ bnd_c7_0 |
% 7.02/6.59 (ALL X86.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c1_1 X86 | bnd_c6_1 X86) | bnd_c5_1 X86)) |
% 7.02/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a539) &
% 7.02/6.59 bnd_c8_2 bnd_a539 bnd_a540) &
% 7.02/6.59 ~ bnd_c5_2 bnd_a539 bnd_a540) &
% 7.02/6.59 bnd_c3_2 bnd_a539 bnd_a540) &
% 7.02/6.59 bnd_c6_1 bnd_a539) &
% 7.02/6.59 bnd_ndr1_1 bnd_a539) &
% 7.02/6.59 ~ bnd_c2_2 bnd_a539 bnd_a541) &
% 7.02/6.59 ~ bnd_c5_2 bnd_a539 bnd_a541) &
% 7.02/6.59 bnd_c8_2 bnd_a539 bnd_a541)) &
% 7.02/6.59 ((~ bnd_c5_0 | ~ bnd_c7_0) |
% 7.02/6.59 (ALL X87.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c5_1 X87 | ~ bnd_c2_1 X87) | bnd_c7_1 X87))) &
% 7.02/6.59 (((ALL X88. bnd_ndr1_0 --> ~ bnd_c8_1 X88 | ~ bnd_c2_1 X88) |
% 7.02/6.59 ((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X89.
% 7.02/6.59 bnd_ndr1_1 bnd_a542 -->
% 7.02/6.59 bnd_c7_2 bnd_a542 X89 | ~ bnd_c4_2 bnd_a542 X89)) &
% 7.02/6.59 bnd_c2_1 bnd_a542) &
% 7.02/6.59 bnd_ndr1_1 bnd_a542) &
% 7.02/6.59 bnd_c8_2 bnd_a542 bnd_a543) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a542 bnd_a543) |
% 7.02/6.59 ((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X90.
% 7.02/6.59 bnd_ndr1_1 bnd_a544 -->
% 7.02/6.59 bnd_c1_2 bnd_a544 X90 | bnd_c4_2 bnd_a544 X90)) &
% 7.02/6.59 bnd_ndr1_1 bnd_a544) &
% 7.02/6.59 ~ bnd_c7_2 bnd_a544 bnd_a545) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a544 bnd_a545) &
% 7.02/6.59 ~ bnd_c3_2 bnd_a544 bnd_a545)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a546) &
% 7.02/6.59 (ALL X91.
% 7.02/6.59 bnd_ndr1_1 bnd_a546 -->
% 7.02/6.59 (bnd_c8_2 bnd_a546 X91 | ~ bnd_c1_2 bnd_a546 X91) |
% 7.02/6.59 ~ bnd_c4_2 bnd_a546 X91)) &
% 7.02/6.59 bnd_ndr1_1 bnd_a546) &
% 7.02/6.59 ~ bnd_c2_2 bnd_a546 bnd_a547) &
% 7.02/6.59 bnd_c7_2 bnd_a546 bnd_a547) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a546 bnd_a547 |
% 7.02/6.59 (ALL X92.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X93.
% 7.02/6.59 bnd_ndr1_1 X92 -->
% 7.02/6.59 (~ bnd_c6_2 X92 X93 | ~ bnd_c8_2 X92 X93) |
% 7.02/6.59 bnd_c3_2 X92 X93) |
% 7.02/6.59 ((bnd_ndr1_1 X92 & bnd_c2_2 X92 bnd_a548) &
% 7.02/6.59 ~ bnd_c4_2 X92 bnd_a548) &
% 7.02/6.59 ~ bnd_c7_2 X92 bnd_a548) |
% 7.02/6.59 ~ bnd_c1_1 X92))) &
% 7.02/6.59 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a549) &
% 7.02/6.59 bnd_c4_2 bnd_a549 bnd_a550) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a549 bnd_a550) &
% 7.02/6.59 bnd_c6_2 bnd_a549 bnd_a550) &
% 7.02/6.59 bnd_ndr1_1 bnd_a549) &
% 7.02/6.59 bnd_c2_2 bnd_a549 bnd_a551) &
% 7.02/6.59 bnd_c8_2 bnd_a549 bnd_a551) &
% 7.02/6.59 bnd_c5_2 bnd_a549 bnd_a551) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a549 |
% 7.02/6.59 ~ bnd_c4_0) |
% 7.02/6.59 ~ bnd_c8_0)) &
% 7.02/6.59 ((bnd_c7_0 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X94.
% 7.02/6.59 bnd_ndr1_1 bnd_a552 -->
% 7.02/6.59 (bnd_c6_2 bnd_a552 X94 | bnd_c8_2 bnd_a552 X94) |
% 7.02/6.59 bnd_c2_2 bnd_a552 X94)) &
% 7.02/6.59 ~ bnd_c8_1 bnd_a552) &
% 7.02/6.59 bnd_c6_1 bnd_a552) |
% 7.02/6.59 (ALL X95.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c4_1 X95 | ~ bnd_c5_1 X95) |
% 7.02/6.59 ((bnd_ndr1_1 X95 & ~ bnd_c2_2 X95 bnd_a553) &
% 7.02/6.59 bnd_c7_2 X95 bnd_a553) &
% 7.02/6.59 ~ bnd_c3_2 X95 bnd_a553))) &
% 7.02/6.59 (~ bnd_c8_0 | ~ bnd_c5_0)) &
% 7.02/6.59 (~ bnd_c5_0 |
% 7.02/6.59 (ALL X96.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c5_1 X96 |
% 7.02/6.59 (bnd_ndr1_1 X96 & ~ bnd_c6_2 X96 bnd_a554) &
% 7.02/6.59 ~ bnd_c3_2 X96 bnd_a554) |
% 7.02/6.59 ((bnd_ndr1_1 X96 & bnd_c5_2 X96 bnd_a555) &
% 7.02/6.59 bnd_c1_2 X96 bnd_a555) &
% 7.02/6.59 ~ bnd_c4_2 X96 bnd_a555))) &
% 7.02/6.59 ((bnd_c8_0 |
% 7.02/6.59 (ALL X97.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (ALL X98.
% 7.02/6.59 bnd_ndr1_1 X97 --> bnd_c2_2 X97 X98 | bnd_c7_2 X97 X98) |
% 7.02/6.59 bnd_c6_1 X97)) |
% 7.02/6.59 ~ bnd_c2_0)) &
% 7.02/6.59 ((bnd_c5_0 | ~ bnd_c2_0) | bnd_c8_0)) &
% 7.02/6.59 (((ALL X99.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c7_1 X99 | ~ bnd_c6_1 X99) |
% 7.02/6.59 ((bnd_ndr1_1 X99 & ~ bnd_c4_2 X99 bnd_a556) &
% 7.02/6.59 bnd_c8_2 X99 bnd_a556) &
% 7.02/6.59 bnd_c7_2 X99 bnd_a556) |
% 7.02/6.59 ~ bnd_c7_0) |
% 7.02/6.59 bnd_c8_0)) &
% 7.02/6.59 (((ALL X100.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X100 & ~ bnd_c6_2 X100 bnd_a557) &
% 7.02/6.59 ~ bnd_c2_2 X100 bnd_a557) &
% 7.02/6.59 bnd_c1_2 X100 bnd_a557 |
% 7.02/6.59 (ALL X101.
% 7.02/6.59 bnd_ndr1_1 X100 --> bnd_c8_2 X100 X101 | bnd_c2_2 X100 X101)) |
% 7.02/6.59 bnd_c7_1 X100) |
% 7.02/6.59 (ALL X102.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c6_1 X102 | ~ bnd_c3_1 X102) | bnd_c5_1 X102)) |
% 7.02/6.59 bnd_c5_0)) &
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c1_1 bnd_a558) & bnd_c6_1 bnd_a558 | ~ bnd_c7_0)) &
% 7.02/6.59 ((bnd_c8_0 | ~ bnd_c1_0) | bnd_c7_0)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & bnd_c7_1 bnd_a559) &
% 7.02/6.59 bnd_ndr1_1 bnd_a559) &
% 7.02/6.59 bnd_c4_2 bnd_a559 bnd_a560) &
% 7.02/6.59 bnd_c7_2 bnd_a559 bnd_a560) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a559 |
% 7.02/6.59 ~ bnd_c8_0) |
% 7.02/6.59 (ALL X103.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c8_1 X103 |
% 7.02/6.59 (ALL X104.
% 7.02/6.59 bnd_ndr1_1 X103 -->
% 7.02/6.59 (bnd_c7_2 X103 X104 | bnd_c2_2 X103 X104) | bnd_c8_2 X103 X104)) |
% 7.02/6.59 (ALL X105.
% 7.02/6.59 bnd_ndr1_1 X103 -->
% 7.02/6.59 (bnd_c3_2 X103 X105 | ~ bnd_c6_2 X103 X105) |
% 7.02/6.59 ~ bnd_c2_2 X103 X105)))) &
% 7.02/6.59 (bnd_c5_0 | ~ bnd_c1_0)) &
% 7.02/6.59 (~ bnd_c4_0 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X106.
% 7.02/6.59 bnd_ndr1_1 bnd_a561 -->
% 7.02/6.59 bnd_c8_2 bnd_a561 X106 | bnd_c4_2 bnd_a561 X106)) &
% 7.02/6.59 ~ bnd_c5_1 bnd_a561) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a561)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a562) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a562 bnd_a563) &
% 7.02/6.59 bnd_c8_2 bnd_a562 bnd_a563) &
% 7.02/6.59 bnd_c2_2 bnd_a562 bnd_a563) &
% 7.02/6.59 ~ bnd_c7_1 bnd_a562 |
% 7.02/6.59 ~ bnd_c2_0) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c7_1 bnd_a564) &
% 7.02/6.59 (ALL X107.
% 7.02/6.59 bnd_ndr1_1 bnd_a564 -->
% 7.02/6.59 (bnd_c3_2 bnd_a564 X107 | bnd_c8_2 bnd_a564 X107) |
% 7.02/6.59 ~ bnd_c1_2 bnd_a564 X107)) &
% 7.02/6.59 bnd_c5_1 bnd_a564 |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c6_1 bnd_a565) &
% 7.02/6.59 bnd_c3_1 bnd_a565) &
% 7.02/6.59 bnd_c2_1 bnd_a565) |
% 7.02/6.59 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a566) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a566 bnd_a567) &
% 7.02/6.59 bnd_c6_2 bnd_a566 bnd_a567) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a566 bnd_a567) &
% 7.02/6.59 bnd_c1_1 bnd_a566) &
% 7.02/6.59 (ALL X108.
% 7.02/6.59 bnd_ndr1_1 bnd_a566 -->
% 7.02/6.59 (~ bnd_c2_2 bnd_a566 X108 |
% 7.02/6.59 bnd_c5_2 bnd_a566 X108) |
% 7.02/6.59 ~ bnd_c1_2 bnd_a566 X108))) &
% 7.02/6.59 ((~ bnd_c7_0 |
% 7.02/6.59 (bnd_ndr1_0 &
% 7.02/6.59 (ALL X109.
% 7.02/6.59 bnd_ndr1_1 bnd_a568 --> bnd_c6_2 bnd_a568 X109 | bnd_c4_2 bnd_a568 X109)) &
% 7.02/6.59 ~ bnd_c4_1 bnd_a568) |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c4_1 bnd_a569) &
% 7.02/6.59 (ALL X110.
% 7.02/6.59 bnd_ndr1_1 bnd_a569 -->
% 7.02/6.59 (bnd_c6_2 bnd_a569 X110 |
% 7.02/6.59 bnd_c3_2 bnd_a569 X110) |
% 7.02/6.59 ~ bnd_c4_2 bnd_a569 X110)) &
% 7.02/6.59 bnd_c3_1 bnd_a569)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & bnd_c4_1 bnd_a570) &
% 7.02/6.59 bnd_c5_1 bnd_a570) &
% 7.02/6.59 bnd_ndr1_1 bnd_a570) &
% 7.02/6.59 bnd_c2_2 bnd_a570 bnd_a571) &
% 7.02/6.59 bnd_c1_2 bnd_a570 bnd_a571) &
% 7.02/6.59 bnd_c3_2 bnd_a570 bnd_a571 |
% 7.02/6.59 bnd_c5_0)) &
% 7.02/6.59 ((bnd_c1_0 | bnd_c5_0) |
% 7.02/6.59 (ALL X111.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X112.
% 7.02/6.59 bnd_ndr1_1 X111 --> bnd_c2_2 X111 X112 | bnd_c5_2 X111 X112) |
% 7.02/6.59 ((bnd_ndr1_1 X111 &
% 7.02/6.59 ~ bnd_c6_2 X111 bnd_a572) &
% 7.02/6.59 ~ bnd_c5_2 X111 bnd_a572) &
% 7.02/6.59 bnd_c2_2 X111 bnd_a572) |
% 7.02/6.59 ~ bnd_c4_1 X111))) &
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a573) &
% 7.02/6.59 bnd_c3_1 bnd_a573) &
% 7.02/6.59 (ALL X113.
% 7.02/6.59 bnd_ndr1_1 bnd_a573 -->
% 7.02/6.59 (~ bnd_c6_2 bnd_a573 X113 |
% 7.02/6.59 ~ bnd_c2_2 bnd_a573 X113) |
% 7.02/6.59 bnd_c5_2 bnd_a573 X113) |
% 7.02/6.59 (ALL X114.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c8_1 X114 |
% 7.02/6.59 (ALL X115.
% 7.02/6.59 bnd_ndr1_1 X114 -->
% 7.02/6.59 (bnd_c5_2 X114 X115 | bnd_c4_2 X114 X115) | ~ bnd_c7_2 X114 X115)) |
% 7.02/6.59 (ALL X116.
% 7.02/6.59 bnd_ndr1_1 X114 -->
% 7.02/6.59 (bnd_c2_2 X114 X116 | ~ bnd_c3_2 X114 X116) | bnd_c1_2 X114 X116))) |
% 7.02/6.59 bnd_c1_0)) &
% 7.02/6.59 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a574) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a574 bnd_a575) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a574 bnd_a575) &
% 7.02/6.59 bnd_c4_2 bnd_a574 bnd_a575) &
% 7.02/6.59 (ALL X117.
% 7.02/6.59 bnd_ndr1_1 bnd_a574 -->
% 7.02/6.59 (~ bnd_c4_2 bnd_a574 X117 |
% 7.02/6.59 ~ bnd_c2_2 bnd_a574 X117) |
% 7.02/6.59 ~ bnd_c3_2 bnd_a574 X117)) &
% 7.02/6.59 ~ bnd_c3_1 bnd_a574 |
% 7.02/6.59 ~ bnd_c2_0) |
% 7.02/6.59 (ALL X118.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c6_1 X118 | bnd_c5_1 X118) |
% 7.02/6.59 (ALL X119.
% 7.02/6.59 bnd_ndr1_1 X118 -->
% 7.02/6.59 (bnd_c8_2 X118 X119 |
% 7.02/6.59 bnd_c7_2 X118 X119) |
% 7.02/6.59 bnd_c6_2 X118 X119)))) &
% 7.02/6.59 (((ALL X120.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X121.
% 7.02/6.59 bnd_ndr1_1 X120 -->
% 7.02/6.59 (bnd_c3_2 X120 X121 |
% 7.02/6.59 ~ bnd_c2_2 X120 X121) |
% 7.02/6.59 bnd_c8_2 X120 X121) |
% 7.02/6.59 (ALL X122.
% 7.02/6.59 bnd_ndr1_1 X120 -->
% 7.02/6.59 (~ bnd_c1_2 X120 X122 |
% 7.02/6.59 bnd_c5_2 X120 X122) |
% 7.02/6.59 bnd_c3_2 X120 X122)) |
% 7.02/6.59 (ALL X123.
% 7.02/6.59 bnd_ndr1_1 X120 -->
% 7.02/6.59 bnd_c6_2 X120 X123 |
% 7.02/6.59 bnd_c2_2 X120 X123)) |
% 7.02/6.59 (ALL X124.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c7_1 X124 | ~ bnd_c1_1 X124) |
% 7.02/6.59 (bnd_ndr1_1 X124 & bnd_c4_2 X124 bnd_a576) &
% 7.02/6.59 ~ bnd_c8_2 X124 bnd_a576)) |
% 7.02/6.59 (((((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a577) &
% 7.02/6.59 bnd_ndr1_1 bnd_a577) &
% 7.02/6.59 bnd_c8_2 bnd_a577 bnd_a578) &
% 7.02/6.59 bnd_c1_2 bnd_a577 bnd_a578) &
% 7.02/6.59 bnd_c6_2 bnd_a577 bnd_a578) &
% 7.02/6.59 bnd_ndr1_1 bnd_a577) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a577 bnd_a579) &
% 7.02/6.59 ~ bnd_c8_2 bnd_a577 bnd_a579)) &
% 7.02/6.59 (((ALL X125.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X125 &
% 7.02/6.59 bnd_c7_2 X125 bnd_a580) &
% 7.02/6.59 ~ bnd_c5_2 X125 bnd_a580) &
% 7.02/6.59 ~ bnd_c2_2 X125 bnd_a580 |
% 7.02/6.59 bnd_c4_1 X125) |
% 7.02/6.59 bnd_c8_1 X125) |
% 7.02/6.59 bnd_c8_0) |
% 7.02/6.59 (ALL X126.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c5_1 X126 | bnd_c6_1 X126) |
% 7.02/6.59 (ALL X127.
% 7.02/6.59 bnd_ndr1_1 X126 -->
% 7.02/6.59 (bnd_c4_2 X126 X127 |
% 7.02/6.59 bnd_c7_2 X126 X127) |
% 7.02/6.59 bnd_c8_2 X126 X127)))) &
% 7.02/6.59 (~ bnd_c2_0 |
% 7.02/6.59 ((bnd_ndr1_0 &
% 7.02/6.59 (ALL X128.
% 7.02/6.59 bnd_ndr1_1 bnd_a581 -->
% 7.02/6.59 (bnd_c7_2 bnd_a581 X128 |
% 7.02/6.59 bnd_c8_2 bnd_a581 X128) |
% 7.02/6.59 bnd_c2_2 bnd_a581 X128)) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a581) &
% 7.02/6.59 bnd_c8_1 bnd_a581)) &
% 7.02/6.59 (((ALL X129.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c3_1 X129 | bnd_c1_1 X129) |
% 7.02/6.59 ((bnd_ndr1_1 X129 & ~ bnd_c5_2 X129 bnd_a582) &
% 7.02/6.59 bnd_c3_2 X129 bnd_a582) &
% 7.02/6.59 bnd_c2_2 X129 bnd_a582) |
% 7.02/6.59 ~ bnd_c4_0) |
% 7.02/6.59 ~ bnd_c8_0)) &
% 7.02/6.59 (~ bnd_c7_0 | ~ bnd_c4_0)) &
% 7.02/6.59 ((ALL X130.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c4_1 X130 |
% 7.02/6.59 (ALL X131.
% 7.02/6.59 bnd_ndr1_1 X130 -->
% 7.02/6.59 (bnd_c7_2 X130 X131 | ~ bnd_c2_2 X130 X131) |
% 7.02/6.59 ~ bnd_c6_2 X130 X131)) |
% 7.02/6.59 bnd_c7_1 X130) |
% 7.02/6.59 (ALL X132.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (((bnd_ndr1_1 X132 & bnd_c7_2 X132 bnd_a583) &
% 7.02/6.59 ~ bnd_c4_2 X132 bnd_a583) &
% 7.02/6.59 bnd_c2_2 X132 bnd_a583 |
% 7.02/6.59 bnd_c5_1 X132) |
% 7.02/6.59 bnd_c7_1 X132))) &
% 7.02/6.59 (((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a584) &
% 7.02/6.59 ~ bnd_c2_1 bnd_a584) &
% 7.02/6.59 bnd_c3_1 bnd_a584 |
% 7.02/6.59 bnd_c8_0)) &
% 7.02/6.59 (((ALL X133.
% 7.02/6.59 bnd_ndr1_0 --> ~ bnd_c5_1 X133 | ~ bnd_c6_1 X133) |
% 7.02/6.59 (((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X134.
% 7.02/6.59 bnd_ndr1_1 bnd_a585 -->
% 7.02/6.59 ~ bnd_c4_2 bnd_a585 X134 |
% 7.02/6.59 bnd_c3_2 bnd_a585 X134)) &
% 7.02/6.59 ~ bnd_c8_1 bnd_a585) &
% 7.02/6.59 bnd_ndr1_1 bnd_a585) &
% 7.02/6.59 bnd_c2_2 bnd_a585 bnd_a586) &
% 7.02/6.59 ~ bnd_c3_2 bnd_a585 bnd_a586) &
% 7.02/6.59 bnd_c1_2 bnd_a585 bnd_a586) |
% 7.02/6.59 ~ bnd_c5_0)) &
% 7.02/6.59 (((bnd_ndr1_0 & bnd_c3_1 bnd_a587) &
% 7.02/6.59 (ALL X135.
% 7.02/6.59 bnd_ndr1_1 bnd_a587 -->
% 7.02/6.59 (~ bnd_c5_2 bnd_a587 X135 |
% 7.02/6.59 ~ bnd_c8_2 bnd_a587 X135) |
% 7.02/6.59 bnd_c1_2 bnd_a587 X135) |
% 7.02/6.59 (ALL X136.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X137.
% 7.02/6.59 bnd_ndr1_1 X136 -->
% 7.02/6.59 ~ bnd_c2_2 X136 X137 | bnd_c5_2 X136 X137) |
% 7.02/6.59 (bnd_ndr1_1 X136 & ~ bnd_c1_2 X136 bnd_a588) &
% 7.02/6.59 bnd_c5_2 X136 bnd_a588) |
% 7.02/6.59 ((bnd_ndr1_1 X136 & bnd_c8_2 X136 bnd_a589) &
% 7.02/6.59 ~ bnd_c7_2 X136 bnd_a589) &
% 7.02/6.59 ~ bnd_c5_2 X136 bnd_a589)) |
% 7.02/6.59 (ALL X138.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X139.
% 7.02/6.59 bnd_ndr1_1 X138 -->
% 7.02/6.59 (~ bnd_c4_2 X138 X139 | bnd_c8_2 X138 X139) |
% 7.02/6.59 ~ bnd_c2_2 X138 X139) |
% 7.02/6.59 bnd_c6_1 X138) |
% 7.02/6.59 (ALL X140.
% 7.02/6.59 bnd_ndr1_1 X138 -->
% 7.02/6.59 (bnd_c2_2 X138 X140 | bnd_c6_2 X138 X140) |
% 7.02/6.59 ~ bnd_c8_2 X138 X140)))) &
% 7.02/6.59 ((~ bnd_c5_0 | ~ bnd_c4_0) | ~ bnd_c6_0)) &
% 7.02/6.59 ((bnd_c5_0 | bnd_c6_0) |
% 7.02/6.59 ((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a590) &
% 7.02/6.59 bnd_c7_1 bnd_a590) &
% 7.02/6.59 bnd_ndr1_1 bnd_a590) &
% 7.02/6.59 ~ bnd_c3_2 bnd_a590 bnd_a591) &
% 7.02/6.59 ~ bnd_c2_2 bnd_a590 bnd_a591)) &
% 7.02/6.59 ((((bnd_ndr1_0 &
% 7.02/6.59 (ALL X141.
% 7.02/6.59 bnd_ndr1_1 bnd_a592 -->
% 7.02/6.59 (bnd_c5_2 bnd_a592 X141 | bnd_c6_2 bnd_a592 X141) |
% 7.02/6.59 ~ bnd_c1_2 bnd_a592 X141)) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a592) &
% 7.02/6.59 (ALL X142.
% 7.02/6.59 bnd_ndr1_1 bnd_a592 -->
% 7.02/6.59 bnd_c3_2 bnd_a592 X142 | ~ bnd_c5_2 bnd_a592 X142) |
% 7.02/6.59 (ALL X143.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X144.
% 7.02/6.59 bnd_ndr1_1 X143 -->
% 7.02/6.59 (~ bnd_c7_2 X143 X144 | bnd_c6_2 X143 X144) |
% 7.02/6.59 bnd_c2_2 X143 X144) |
% 7.02/6.59 ~ bnd_c6_1 X143) |
% 7.02/6.59 ((bnd_ndr1_1 X143 & bnd_c8_2 X143 bnd_a593) &
% 7.02/6.59 ~ bnd_c7_2 X143 bnd_a593) &
% 7.02/6.59 ~ bnd_c4_2 X143 bnd_a593)) |
% 7.02/6.59 bnd_c7_0)) &
% 7.02/6.59 ((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a594) &
% 7.02/6.59 ~ bnd_c6_1 bnd_a594) &
% 7.02/6.59 bnd_ndr1_1 bnd_a594) &
% 7.02/6.59 bnd_c1_2 bnd_a594 bnd_a595) &
% 7.02/6.59 ~ bnd_c6_2 bnd_a594 bnd_a595) &
% 7.02/6.59 ~ bnd_c4_2 bnd_a594 bnd_a595 |
% 7.02/6.59 ~ bnd_c1_0)) &
% 7.02/6.59 ((~ bnd_c7_0 | bnd_c2_0) |
% 7.02/6.59 (ALL X145.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X146.
% 7.02/6.59 bnd_ndr1_1 X145 -->
% 7.02/6.59 (bnd_c1_2 X145 X146 | bnd_c7_2 X145 X146) |
% 7.02/6.59 bnd_c4_2 X145 X146) |
% 7.02/6.59 bnd_c3_1 X145) |
% 7.02/6.59 bnd_c6_1 X145))) &
% 7.02/6.59 ((((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a596) & bnd_c7_1 bnd_a596) &
% 7.02/6.59 (ALL X147.
% 7.02/6.59 bnd_ndr1_1 bnd_a596 -->
% 7.02/6.59 ~ bnd_c4_2 bnd_a596 X147 | ~ bnd_c1_2 bnd_a596 X147) |
% 7.02/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a597) &
% 7.02/6.59 bnd_c4_2 bnd_a597 bnd_a598) &
% 7.02/6.59 bnd_c3_2 bnd_a597 bnd_a598) &
% 7.02/6.59 bnd_c7_2 bnd_a597 bnd_a598) &
% 7.02/6.59 ~ bnd_c1_1 bnd_a597) &
% 7.02/6.59 bnd_ndr1_1 bnd_a597) &
% 7.02/6.59 bnd_c3_2 bnd_a597 bnd_a599) &
% 7.02/6.59 bnd_c5_2 bnd_a597 bnd_a599) &
% 7.02/6.59 ~ bnd_c1_2 bnd_a597 bnd_a599) |
% 7.02/6.59 bnd_c6_0)) &
% 7.02/6.59 (bnd_c1_0 | bnd_c6_0)) &
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c3_1 bnd_a600) &
% 7.02/6.59 (ALL X148.
% 7.02/6.59 bnd_ndr1_1 bnd_a600 -->
% 7.02/6.59 ~ bnd_c1_2 bnd_a600 X148 | bnd_c7_2 bnd_a600 X148) |
% 7.02/6.59 ((bnd_ndr1_0 & bnd_c7_1 bnd_a601) & ~ bnd_c1_1 bnd_a601) &
% 7.02/6.59 bnd_c5_1 bnd_a601)) &
% 7.02/6.59 ((~ bnd_c1_0 | bnd_c5_0) | ~ bnd_c8_0)) &
% 7.02/6.59 (((ALL X149.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 ((ALL X150.
% 7.02/6.59 bnd_ndr1_1 X149 -->
% 7.02/6.59 (~ bnd_c8_2 X149 X150 | bnd_c1_2 X149 X150) |
% 7.02/6.59 bnd_c3_2 X149 X150) |
% 7.02/6.59 bnd_c8_1 X149) |
% 7.02/6.59 bnd_c4_1 X149) |
% 7.02/6.59 bnd_c1_0) |
% 7.02/6.59 (ALL X151.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c3_1 X151 | ~ bnd_c1_1 X151) | bnd_c8_1 X151))) &
% 7.02/6.59 (((ALL X152.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (~ bnd_c3_1 X152 | bnd_c1_1 X152) | bnd_c6_1 X152) |
% 7.02/6.59 ~ bnd_c1_0) |
% 7.02/6.59 bnd_c5_0)) &
% 7.02/6.59 ((bnd_c2_0 | ~ bnd_c7_0) | ~ bnd_c8_0)) &
% 7.02/6.59 ((bnd_c1_0 |
% 7.02/6.59 (ALL X153.
% 7.02/6.59 bnd_ndr1_0 -->
% 7.02/6.59 (bnd_c2_1 X153 |
% 7.02/6.59 ((bnd_ndr1_1 X153 & bnd_c3_2 X153 bnd_a602) &
% 7.02/6.59 bnd_c4_2 X153 bnd_a602) &
% 7.02/6.59 ~ bnd_c7_2 X153 bnd_a602) |
% 7.02/6.59 bnd_c7_1 X153)) |
% 7.02/6.59 ~ bnd_c7_0)) &
% 7.02/6.59 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a603) &
% 7.02/6.59 (ALL X154.
% 7.02/6.59 bnd_ndr1_1 bnd_a603 -->
% 7.02/6.59 (~ bnd_c3_2 bnd_a603 X154 | bnd_c7_2 bnd_a603 X154) |
% 7.02/6.59 ~ bnd_c5_2 bnd_a603 X154)) &
% 7.02/6.59 ~ bnd_c4_1 bnd_a603 |
% 7.02/6.59 ~ bnd_c5_0) |
% 7.02/6.59 ~ bnd_c8_0)) &
% 7.02/6.59 ((bnd_c8_0 | ~ bnd_c7_0) | bnd_c5_0))
% 15.33/14.81 Unfolded term: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c4_1 U |
% 15.33/14.81 ((bnd_ndr1_1 U & ~ bnd_c4_2 U bnd_a456) &
% 15.33/14.81 bnd_c6_2 U bnd_a456) &
% 15.33/14.81 bnd_c8_2 U bnd_a456) |
% 15.33/14.81 ((bnd_ndr1_1 U & ~ bnd_c6_2 U bnd_a457) &
% 15.33/14.81 bnd_c7_2 U bnd_a457) &
% 15.33/14.81 bnd_c5_2 U bnd_a457) |
% 15.33/14.81 bnd_c2_0) |
% 15.33/14.81 ~ bnd_c7_0) &
% 15.33/14.81 (bnd_c2_0 | ~ bnd_c1_0)) &
% 15.33/14.81 ((~ bnd_c8_0 |
% 15.33/14.81 ((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a458) &
% 15.33/14.81 bnd_c4_1 bnd_a458) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a458) |
% 15.33/14.81 (ALL V.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c6_1 V | bnd_c2_1 V) |
% 15.33/14.81 (ALL W.
% 15.33/14.81 bnd_ndr1_1 V -->
% 15.33/14.81 bnd_c3_2 V W | ~ bnd_c7_2 V W)))) &
% 15.33/14.81 (((ALL X.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c3_1 X | ~ bnd_c8_1 X) |
% 15.33/14.81 ((bnd_ndr1_1 X & ~ bnd_c6_2 X bnd_a459) &
% 15.33/14.81 ~ bnd_c3_2 X bnd_a459) &
% 15.33/14.81 bnd_c7_2 X bnd_a459) |
% 15.33/14.81 ~ bnd_c6_0) |
% 15.33/14.81 (ALL Y.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((bnd_ndr1_1 Y & bnd_c8_2 Y bnd_a460) &
% 15.33/14.81 bnd_c5_2 Y bnd_a460) &
% 15.33/14.81 bnd_c1_2 Y bnd_a460))) &
% 15.33/14.81 (((ALL Z.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X1.
% 15.33/14.81 bnd_ndr1_1 Z -->
% 15.33/14.81 ~ bnd_c7_2 Z X1 | ~ bnd_c8_2 Z X1) |
% 15.33/14.81 ((bnd_ndr1_1 Z & ~ bnd_c7_2 Z bnd_a461) &
% 15.33/14.81 ~ bnd_c2_2 Z bnd_a461) &
% 15.33/14.81 ~ bnd_c4_2 Z bnd_a461) |
% 15.33/14.81 ~ bnd_c8_1 Z) |
% 15.33/14.81 bnd_c2_0) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 (((ALL X2.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X3.
% 15.33/14.81 bnd_ndr1_1 X2 -->
% 15.33/14.81 (~ bnd_c2_2 X2 X3 | bnd_c6_2 X2 X3) |
% 15.33/14.81 ~ bnd_c4_2 X2 X3) |
% 15.33/14.81 ((bnd_ndr1_1 X2 & ~ bnd_c1_2 X2 bnd_a462) &
% 15.33/14.81 ~ bnd_c7_2 X2 bnd_a462) &
% 15.33/14.81 ~ bnd_c6_2 X2 bnd_a462) |
% 15.33/14.81 ~ bnd_c8_1 X2) |
% 15.33/14.81 ~ bnd_c5_0) |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c7_1 bnd_a463) &
% 15.33/14.81 ~ bnd_c1_1 bnd_a463) &
% 15.33/14.81 ~ bnd_c5_1 bnd_a463)) &
% 15.33/14.81 ((bnd_c6_0 |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c2_1 bnd_a464) & bnd_c8_1 bnd_a464) &
% 15.33/14.81 ~ bnd_c7_1 bnd_a464) |
% 15.33/14.81 ~ bnd_c1_0)) &
% 15.33/14.81 (((ALL X4.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X5.
% 15.33/14.81 bnd_ndr1_1 X4 -->
% 15.33/14.81 (~ bnd_c6_2 X4 X5 | bnd_c5_2 X4 X5) |
% 15.33/14.81 ~ bnd_c7_2 X4 X5) |
% 15.33/14.81 ((bnd_ndr1_1 X4 & ~ bnd_c1_2 X4 bnd_a465) &
% 15.33/14.81 ~ bnd_c5_2 X4 bnd_a465) &
% 15.33/14.81 ~ bnd_c7_2 X4 bnd_a465) |
% 15.33/14.81 bnd_c8_1 X4) |
% 15.33/14.81 (ALL X6.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c8_1 X6 |
% 15.33/14.81 (ALL X7.
% 15.33/14.81 bnd_ndr1_1 X6 -->
% 15.33/14.81 (~ bnd_c6_2 X6 X7 | bnd_c1_2 X6 X7) |
% 15.33/14.81 ~ bnd_c2_2 X6 X7)) |
% 15.33/14.81 ~ bnd_c1_1 X6)) |
% 15.33/14.81 (ALL X8.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c1_1 X8 | bnd_c2_1 X8) |
% 15.33/14.81 (ALL X9.
% 15.33/14.81 bnd_ndr1_1 X8 -->
% 15.33/14.81 (bnd_c1_2 X8 X9 | bnd_c7_2 X8 X9) |
% 15.33/14.81 bnd_c3_2 X8 X9)))) &
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c1_1 bnd_a466) & ~ bnd_c8_1 bnd_a466 |
% 15.33/14.81 ~ bnd_c2_0)) &
% 15.33/14.81 (bnd_c8_0 | ~ bnd_c5_0)) &
% 15.33/14.81 ((ALL X10.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X11.
% 15.33/14.81 bnd_ndr1_1 X10 -->
% 15.33/14.81 (bnd_c8_2 X10 X11 | ~ bnd_c4_2 X10 X11) |
% 15.33/14.81 ~ bnd_c7_2 X10 X11) |
% 15.33/14.81 bnd_c8_1 X10) |
% 15.33/14.81 ~ bnd_c2_1 X10) |
% 15.33/14.81 (ALL X12.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X12 & bnd_c8_2 X12 bnd_a467) &
% 15.33/14.81 bnd_c2_2 X12 bnd_a467) &
% 15.33/14.81 bnd_c3_2 X12 bnd_a467 |
% 15.33/14.81 ~ bnd_c6_1 X12) |
% 15.33/14.81 ~ bnd_c8_1 X12))) &
% 15.33/14.81 (~ bnd_c4_0 |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c6_1 bnd_a468) & ~ bnd_c4_1 bnd_a468) &
% 15.33/14.81 ~ bnd_c3_1 bnd_a468)) &
% 15.33/14.81 (((ALL X13.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X13 & bnd_c2_2 X13 bnd_a469) &
% 15.33/14.81 ~ bnd_c8_2 X13 bnd_a469) &
% 15.33/14.81 ~ bnd_c6_2 X13 bnd_a469 |
% 15.33/14.81 (ALL X14.
% 15.33/14.81 bnd_ndr1_1 X13 -->
% 15.33/14.81 (bnd_c3_2 X13 X14 | ~ bnd_c6_2 X13 X14) |
% 15.33/14.81 ~ bnd_c2_2 X13 X14)) |
% 15.33/14.81 bnd_c8_1 X13) |
% 15.33/14.81 bnd_c6_0) |
% 15.33/14.81 bnd_c2_0)) &
% 15.33/14.81 ((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X15.
% 15.33/14.81 bnd_ndr1_1 bnd_a470 -->
% 15.33/14.81 (~ bnd_c1_2 bnd_a470 X15 | bnd_c7_2 bnd_a470 X15) |
% 15.33/14.81 ~ bnd_c4_2 bnd_a470 X15)) &
% 15.33/14.81 bnd_c7_1 bnd_a470) &
% 15.33/14.81 (ALL X16.
% 15.33/14.81 bnd_ndr1_1 bnd_a470 -->
% 15.33/14.81 ~ bnd_c8_2 bnd_a470 X16 | bnd_c7_2 bnd_a470 X16) |
% 15.33/14.81 bnd_c8_0) |
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a471) & bnd_ndr1_1 bnd_a471) &
% 15.33/14.81 bnd_c7_2 bnd_a471 bnd_a472) &
% 15.33/14.81 ~ bnd_c5_2 bnd_a471 bnd_a472) &
% 15.33/14.81 (ALL X17.
% 15.33/14.81 bnd_ndr1_1 bnd_a471 -->
% 15.33/14.81 (bnd_c3_2 bnd_a471 X17 | bnd_c1_2 bnd_a471 X17) |
% 15.33/14.81 bnd_c6_2 bnd_a471 X17))) &
% 15.33/14.81 bnd_c3_0) &
% 15.33/14.81 ((~ bnd_c7_0 |
% 15.33/14.81 (ALL X18.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((bnd_ndr1_1 X18 & bnd_c8_2 X18 bnd_a473) &
% 15.33/14.81 bnd_c4_2 X18 bnd_a473) &
% 15.33/14.81 ~ bnd_c3_2 X18 bnd_a473 |
% 15.33/14.81 ~ bnd_c3_1 X18)) |
% 15.33/14.81 (ALL X19.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (ALL X20.
% 15.33/14.81 bnd_ndr1_1 X19 -->
% 15.33/14.81 (~ bnd_c8_2 X19 X20 | ~ bnd_c4_2 X19 X20) |
% 15.33/14.81 ~ bnd_c1_2 X19 X20)))) &
% 15.33/14.81 (((ALL X21.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((bnd_ndr1_1 X21 & bnd_c6_2 X21 bnd_a474) &
% 15.33/14.81 bnd_c7_2 X21 bnd_a474) &
% 15.33/14.81 bnd_c1_2 X21 bnd_a474 |
% 15.33/14.81 ~ bnd_c5_1 X21) |
% 15.33/14.81 (ALL X22.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c6_1 X22 | ~ bnd_c7_1 X22) |
% 15.33/14.81 (ALL X23.
% 15.33/14.81 bnd_ndr1_1 X22 -->
% 15.33/14.81 (bnd_c1_2 X22 X23 | bnd_c4_2 X22 X23) |
% 15.33/14.81 ~ bnd_c6_2 X22 X23))) |
% 15.33/14.81 (ALL X24.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X25.
% 15.33/14.81 bnd_ndr1_1 X24 -->
% 15.33/14.81 (bnd_c4_2 X24 X25 | ~ bnd_c6_2 X24 X25) |
% 15.33/14.81 ~ bnd_c3_2 X24 X25) |
% 15.33/14.81 bnd_c8_1 X24) |
% 15.33/14.81 ~ bnd_c3_1 X24))) &
% 15.33/14.81 ((((((((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X26.
% 15.33/14.81 bnd_ndr1_1 bnd_a475 -->
% 15.33/14.81 (~ bnd_c8_2 bnd_a475 X26 | bnd_c4_2 bnd_a475 X26) |
% 15.33/14.81 bnd_c5_2 bnd_a475 X26)) &
% 15.33/14.81 bnd_ndr1_1 bnd_a475) &
% 15.33/14.81 bnd_c5_2 bnd_a475 bnd_a476) &
% 15.33/14.81 ~ bnd_c3_2 bnd_a475 bnd_a476) &
% 15.33/14.81 bnd_c7_2 bnd_a475 bnd_a476) &
% 15.33/14.81 bnd_ndr1_1 bnd_a475) &
% 15.33/14.81 bnd_c4_2 bnd_a475 bnd_a477) &
% 15.33/14.81 bnd_c6_2 bnd_a475 bnd_a477) &
% 15.33/14.81 bnd_c7_2 bnd_a475 bnd_a477 |
% 15.33/14.81 bnd_c7_0) |
% 15.33/14.81 ~ bnd_c2_0)) &
% 15.33/14.81 (((ALL X27.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X27 & ~ bnd_c4_2 X27 bnd_a478) &
% 15.33/14.81 bnd_c7_2 X27 bnd_a478) &
% 15.33/14.81 ~ bnd_c5_2 X27 bnd_a478 |
% 15.33/14.81 ~ bnd_c3_1 X27) |
% 15.33/14.81 (ALL X28.
% 15.33/14.81 bnd_ndr1_1 X27 -->
% 15.33/14.81 ~ bnd_c6_2 X27 X28 | ~ bnd_c1_2 X27 X28)) |
% 15.33/14.81 bnd_c2_0) |
% 15.33/14.81 ~ bnd_c1_0)) &
% 15.33/14.81 ((~ bnd_c6_0 |
% 15.33/14.81 (ALL X29.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X30.
% 15.33/14.81 bnd_ndr1_1 X29 -->
% 15.33/14.81 (bnd_c3_2 X29 X30 | bnd_c1_2 X29 X30) |
% 15.33/14.81 ~ bnd_c8_2 X29 X30) |
% 15.33/14.81 ~ bnd_c8_1 X29) |
% 15.33/14.81 (bnd_ndr1_1 X29 & bnd_c6_2 X29 bnd_a479) &
% 15.33/14.81 ~ bnd_c7_2 X29 bnd_a479)) |
% 15.33/14.81 (ALL X31.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X31 & bnd_c3_2 X31 bnd_a480) &
% 15.33/14.81 bnd_c4_2 X31 bnd_a480) &
% 15.33/14.81 ~ bnd_c6_2 X31 bnd_a480 |
% 15.33/14.81 bnd_c3_1 X31) |
% 15.33/14.81 ~ bnd_c2_1 X31))) &
% 15.33/14.81 ((bnd_c5_0 |
% 15.33/14.81 (ALL X32.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X33.
% 15.33/14.81 bnd_ndr1_1 X32 -->
% 15.33/14.81 (bnd_c4_2 X32 X33 | ~ bnd_c6_2 X32 X33) |
% 15.33/14.81 ~ bnd_c3_2 X32 X33) |
% 15.33/14.81 bnd_c8_1 X32) |
% 15.33/14.81 (bnd_ndr1_1 X32 & bnd_c2_2 X32 bnd_a481) &
% 15.33/14.81 bnd_c8_2 X32 bnd_a481)) |
% 15.33/14.81 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a482) &
% 15.33/14.81 bnd_c3_2 bnd_a482 bnd_a483) &
% 15.33/14.81 bnd_c2_2 bnd_a482 bnd_a483) &
% 15.33/14.81 bnd_c8_2 bnd_a482 bnd_a483) &
% 15.33/14.81 (ALL X34.
% 15.33/14.81 bnd_ndr1_1 bnd_a482 -->
% 15.33/14.81 (bnd_c2_2 bnd_a482 X34 | ~ bnd_c6_2 bnd_a482 X34) |
% 15.33/14.81 ~ bnd_c8_2 bnd_a482 X34)) &
% 15.33/14.81 bnd_ndr1_1 bnd_a482) &
% 15.33/14.81 bnd_c5_2 bnd_a482 bnd_a484) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a482 bnd_a484) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a482 bnd_a484)) &
% 15.33/14.81 (((ALL X35.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c8_1 X35 |
% 15.33/14.81 ((bnd_ndr1_1 X35 & ~ bnd_c2_2 X35 bnd_a485) &
% 15.33/14.81 ~ bnd_c3_2 X35 bnd_a485) &
% 15.33/14.81 ~ bnd_c1_2 X35 bnd_a485) |
% 15.33/14.81 ((bnd_ndr1_1 X35 & bnd_c6_2 X35 bnd_a486) &
% 15.33/14.81 bnd_c1_2 X35 bnd_a486) &
% 15.33/14.81 bnd_c5_2 X35 bnd_a486) |
% 15.33/14.81 ~ bnd_c5_0) |
% 15.33/14.81 bnd_c7_0)) &
% 15.33/14.81 (((ALL X36.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c2_1 X36 | bnd_c5_1 X36) |
% 15.33/14.81 (bnd_ndr1_1 X36 & bnd_c1_2 X36 bnd_a487) & bnd_c4_2 X36 bnd_a487) |
% 15.33/14.81 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a488) & bnd_c4_1 bnd_a488) &
% 15.33/14.81 (ALL X37.
% 15.33/14.81 bnd_ndr1_1 bnd_a488 -->
% 15.33/14.81 (~ bnd_c6_2 bnd_a488 X37 | bnd_c2_2 bnd_a488 X37) |
% 15.33/14.81 bnd_c5_2 bnd_a488 X37)) |
% 15.33/14.81 bnd_c1_0)) &
% 15.33/14.81 (((ALL X38.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c4_1 X38 |
% 15.33/14.81 ((bnd_ndr1_1 X38 & bnd_c4_2 X38 bnd_a489) &
% 15.33/14.81 ~ bnd_c8_2 X38 bnd_a489) &
% 15.33/14.81 ~ bnd_c3_2 X38 bnd_a489) |
% 15.33/14.81 (ALL X39.
% 15.33/14.81 bnd_ndr1_1 X38 -->
% 15.33/14.81 (bnd_c1_2 X38 X39 | bnd_c5_2 X38 X39) | ~ bnd_c8_2 X38 X39)) |
% 15.33/14.81 bnd_c8_0) |
% 15.33/14.81 ~ bnd_c7_0)) &
% 15.33/14.81 ((bnd_c5_0 |
% 15.33/14.81 (ALL X40.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c8_1 X40 | ~ bnd_c7_1 X40) |
% 15.33/14.81 ((bnd_ndr1_1 X40 & bnd_c4_2 X40 bnd_a490) & ~ bnd_c6_2 X40 bnd_a490) &
% 15.33/14.81 bnd_c7_2 X40 bnd_a490)) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 ((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a491) &
% 15.33/14.81 (ALL X41.
% 15.33/14.81 bnd_ndr1_1 bnd_a491 -->
% 15.33/14.81 (bnd_c6_2 bnd_a491 X41 | bnd_c4_2 bnd_a491 X41) |
% 15.33/14.81 bnd_c3_2 bnd_a491 X41)) &
% 15.33/14.81 ~ bnd_c5_1 bnd_a491 |
% 15.33/14.81 (ALL X42.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X43.
% 15.33/14.81 bnd_ndr1_1 X42 -->
% 15.33/14.81 (bnd_c3_2 X42 X43 | ~ bnd_c5_2 X42 X43) | ~ bnd_c8_2 X42 X43) |
% 15.33/14.81 ((bnd_ndr1_1 X42 & bnd_c4_2 X42 bnd_a492) & ~ bnd_c6_2 X42 bnd_a492) &
% 15.33/14.81 ~ bnd_c7_2 X42 bnd_a492) |
% 15.33/14.81 ((bnd_ndr1_1 X42 & ~ bnd_c6_2 X42 bnd_a493) & bnd_c1_2 X42 bnd_a493) &
% 15.33/14.81 ~ bnd_c2_2 X42 bnd_a493)) |
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a494) & bnd_ndr1_1 bnd_a494) &
% 15.33/14.81 ~ bnd_c3_2 bnd_a494 bnd_a495) &
% 15.33/14.81 bnd_c8_2 bnd_a494 bnd_a495) &
% 15.33/14.81 bnd_c4_1 bnd_a494)) &
% 15.33/14.81 ((bnd_c7_0 | bnd_c2_0) | bnd_c8_0)) &
% 15.33/14.81 ((~ bnd_c4_0 | ~ bnd_c6_0) |
% 15.33/14.81 (((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X44.
% 15.33/14.81 bnd_ndr1_1 bnd_a496 -->
% 15.33/14.81 (bnd_c3_2 bnd_a496 X44 | ~ bnd_c8_2 bnd_a496 X44) |
% 15.33/14.81 ~ bnd_c2_2 bnd_a496 X44)) &
% 15.33/14.81 bnd_ndr1_1 bnd_a496) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a496 bnd_a497) &
% 15.33/14.81 bnd_c3_2 bnd_a496 bnd_a497) &
% 15.33/14.81 bnd_c6_2 bnd_a496 bnd_a497) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a496)) &
% 15.33/14.81 ((bnd_c2_0 |
% 15.33/14.81 (ALL X45.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c5_1 X45 |
% 15.33/14.81 (ALL X46.
% 15.33/14.81 bnd_ndr1_1 X45 -->
% 15.33/14.81 (~ bnd_c7_2 X45 X46 | bnd_c2_2 X45 X46) | ~ bnd_c1_2 X45 X46)) |
% 15.33/14.81 (ALL X47.
% 15.33/14.81 bnd_ndr1_1 X45 -->
% 15.33/14.81 (bnd_c1_2 X45 X47 | ~ bnd_c5_2 X45 X47) | bnd_c2_2 X45 X47))) |
% 15.33/14.81 (ALL X48.
% 15.33/14.81 bnd_ndr1_0 --> (bnd_c1_1 X48 | bnd_c2_1 X48) | ~ bnd_c4_1 X48))) &
% 15.33/14.81 ((bnd_c1_0 | bnd_c2_0) |
% 15.33/14.81 ((((((((bnd_ndr1_0 &
% 15.33/14.81 bnd_ndr1_1 bnd_a498) &
% 15.33/14.81 bnd_c3_2 bnd_a498 bnd_a499) &
% 15.33/14.81 bnd_c7_2 bnd_a498 bnd_a499) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a498 bnd_a499) &
% 15.33/14.81 bnd_c7_1 bnd_a498) &
% 15.33/14.81 bnd_ndr1_1 bnd_a498) &
% 15.33/14.81 bnd_c8_2 bnd_a498 bnd_a500) &
% 15.33/14.81 bnd_c4_2 bnd_a498 bnd_a500) &
% 15.33/14.81 ~ bnd_c7_2 bnd_a498 bnd_a500)) &
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a501) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a501) &
% 15.33/14.81 ~ bnd_c8_1 bnd_a501 |
% 15.33/14.81 bnd_c7_0) |
% 15.33/14.81 (ALL X49.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X50.
% 15.33/14.81 bnd_ndr1_1 X49 -->
% 15.33/14.81 (bnd_c7_2 X49 X50 | bnd_c6_2 X49 X50) | bnd_c1_2 X49 X50) |
% 15.33/14.81 bnd_c1_1 X49) |
% 15.33/14.81 ~ bnd_c2_1 X49))) &
% 15.33/14.81 (((ALL X51.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X51 &
% 15.33/14.81 ~ bnd_c1_2 X51 bnd_a502) &
% 15.33/14.81 ~ bnd_c7_2 X51 bnd_a502) &
% 15.33/14.81 ~ bnd_c8_2 X51 bnd_a502 |
% 15.33/14.81 ((bnd_ndr1_1 X51 & ~ bnd_c3_2 X51 bnd_a503) & ~ bnd_c4_2 X51 bnd_a503) &
% 15.33/14.81 bnd_c1_2 X51 bnd_a503) |
% 15.33/14.81 ((bnd_ndr1_1 X51 &
% 15.33/14.81 ~ bnd_c5_2 X51 bnd_a504) &
% 15.33/14.81 bnd_c8_2 X51 bnd_a504) &
% 15.33/14.81 ~ bnd_c3_2 X51 bnd_a504) |
% 15.33/14.81 ((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a505) &
% 15.33/14.81 bnd_ndr1_1 bnd_a505) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a505 bnd_a506) &
% 15.33/14.81 bnd_c6_2 bnd_a505 bnd_a506) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a505 bnd_a506) |
% 15.33/14.81 ~ bnd_c4_0)) &
% 15.33/14.81 (((ALL X52.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ~ bnd_c6_1 X52 |
% 15.33/14.81 (bnd_ndr1_1 X52 &
% 15.33/14.81 ~ bnd_c2_2 X52 bnd_a507) &
% 15.33/14.81 bnd_c5_2 X52 bnd_a507) |
% 15.33/14.81 (ALL X53.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c8_1 X53 | ~ bnd_c1_1 X53) |
% 15.33/14.81 ~ bnd_c5_1 X53)) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 ((~ bnd_c6_0 |
% 15.33/14.81 (ALL X54.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ~ bnd_c4_1 X54 |
% 15.33/14.81 (ALL X55.
% 15.33/14.81 bnd_ndr1_1 X54 -->
% 15.33/14.81 (~ bnd_c4_2 X54 X55 | ~ bnd_c3_2 X54 X55) | ~ bnd_c7_2 X54 X55))) |
% 15.33/14.81 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a508) &
% 15.33/14.81 bnd_c1_1 bnd_a508)) &
% 15.33/14.81 ((~ bnd_c4_0 | bnd_c7_0) |
% 15.33/14.81 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a509) &
% 15.33/14.81 bnd_c4_2 bnd_a509 bnd_a510) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a509 bnd_a510) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a509 bnd_a510) &
% 15.33/14.81 bnd_ndr1_1 bnd_a509) &
% 15.33/14.81 ~ bnd_c5_2 bnd_a509 bnd_a511) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a509 bnd_a511) &
% 15.33/14.81 bnd_c3_2 bnd_a509 bnd_a511)) &
% 15.33/14.81 ((~ bnd_c5_0 | ~ bnd_c1_0) | ~ bnd_c8_0)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & bnd_c6_1 bnd_a512) &
% 15.33/14.81 bnd_ndr1_1 bnd_a512) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a512 bnd_a513) &
% 15.33/14.81 ~ bnd_c2_2 bnd_a512 bnd_a513) &
% 15.33/14.81 bnd_c3_2 bnd_a512 bnd_a513 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X56.
% 15.33/14.81 bnd_ndr1_1 bnd_a514 -->
% 15.33/14.81 (bnd_c6_2 bnd_a514 X56 |
% 15.33/14.81 ~ bnd_c4_2 bnd_a514 X56) |
% 15.33/14.81 ~ bnd_c8_2 bnd_a514 X56)) &
% 15.33/14.81 bnd_c5_1 bnd_a514) &
% 15.33/14.81 ~ bnd_c1_1 bnd_a514) |
% 15.33/14.81 (ALL X57.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X57 &
% 15.33/14.81 ~ bnd_c2_2 X57 bnd_a515) &
% 15.33/14.81 bnd_c7_2 X57 bnd_a515) &
% 15.33/14.81 ~ bnd_c3_2 X57 bnd_a515 |
% 15.33/14.81 (bnd_ndr1_1 X57 & ~ bnd_c6_2 X57 bnd_a516) &
% 15.33/14.81 ~ bnd_c2_2 X57 bnd_a516) |
% 15.33/14.81 (ALL X58.
% 15.33/14.81 bnd_ndr1_1 X57 -->
% 15.33/14.81 bnd_c5_2 X57 X58 |
% 15.33/14.81 ~ bnd_c4_2 X57 X58)))) &
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c6_1 bnd_a517) &
% 15.33/14.81 bnd_c4_1 bnd_a517) &
% 15.33/14.81 bnd_c2_1 bnd_a517 |
% 15.33/14.81 bnd_c8_0) |
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a518) &
% 15.33/14.81 bnd_c7_2 bnd_a518 bnd_a519) &
% 15.33/14.81 bnd_c5_2 bnd_a518 bnd_a519) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a518 bnd_a519) &
% 15.33/14.81 bnd_c5_1 bnd_a518)) &
% 15.33/14.81 ((ALL X59.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c1_1 X59 | bnd_c7_1 X59) |
% 15.33/14.81 ~ bnd_c3_1 X59) |
% 15.33/14.81 ~ bnd_c5_0)) &
% 15.33/14.81 ((bnd_c5_0 |
% 15.33/14.81 (((((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a520) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a520) &
% 15.33/14.81 bnd_ndr1_1 bnd_a520) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a520 bnd_a521) &
% 15.33/14.81 bnd_c2_2 bnd_a520 bnd_a521) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a520 bnd_a521) |
% 15.33/14.81 bnd_c1_0)) &
% 15.33/14.81 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a522) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a522 bnd_a523) &
% 15.33/14.81 bnd_c4_2 bnd_a522 bnd_a523) &
% 15.33/14.81 bnd_c1_2 bnd_a522 bnd_a523) &
% 15.33/14.81 bnd_ndr1_1 bnd_a522) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a522 bnd_a524) &
% 15.33/14.81 bnd_c6_2 bnd_a522 bnd_a524) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a522 bnd_a524) &
% 15.33/14.81 bnd_c6_1 bnd_a522 |
% 15.33/14.81 ~ bnd_c5_0) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 (((ALL X60.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c8_1 X60 | ~ bnd_c4_1 X60) |
% 15.33/14.81 (ALL X61.
% 15.33/14.81 bnd_ndr1_1 X60 -->
% 15.33/14.81 (bnd_c3_2 X60 X61 | ~ bnd_c6_2 X60 X61) |
% 15.33/14.81 ~ bnd_c4_2 X60 X61)) |
% 15.33/14.81 ~ bnd_c2_0) |
% 15.33/14.81 (ALL X62.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c3_1 X62 |
% 15.33/14.81 ((bnd_ndr1_1 X62 & bnd_c7_2 X62 bnd_a525) &
% 15.33/14.81 ~ bnd_c6_2 X62 bnd_a525) &
% 15.33/14.81 ~ bnd_c2_2 X62 bnd_a525) |
% 15.33/14.81 bnd_c6_1 X62))) &
% 15.33/14.81 (((ALL X63.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X63 & bnd_c7_2 X63 bnd_a526) &
% 15.33/14.81 ~ bnd_c3_2 X63 bnd_a526) &
% 15.33/14.81 bnd_c8_2 X63 bnd_a526 |
% 15.33/14.81 ((bnd_ndr1_1 X63 & ~ bnd_c2_2 X63 bnd_a527) &
% 15.33/14.81 ~ bnd_c1_2 X63 bnd_a527) &
% 15.33/14.81 bnd_c4_2 X63 bnd_a527) |
% 15.33/14.81 (ALL X64.
% 15.33/14.81 bnd_ndr1_1 X63 -->
% 15.33/14.81 (~ bnd_c1_2 X63 X64 | bnd_c3_2 X63 X64) |
% 15.33/14.81 bnd_c2_2 X63 X64)) |
% 15.33/14.81 ~ bnd_c4_0) |
% 15.33/14.81 (ALL X65.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X66.
% 15.33/14.81 bnd_ndr1_1 X65 -->
% 15.33/14.81 (bnd_c3_2 X65 X66 | ~ bnd_c7_2 X65 X66) |
% 15.33/14.81 bnd_c8_2 X65 X66) |
% 15.33/14.81 ((bnd_ndr1_1 X65 & bnd_c6_2 X65 bnd_a528) &
% 15.33/14.81 bnd_c2_2 X65 bnd_a528) &
% 15.33/14.81 ~ bnd_c5_2 X65 bnd_a528) |
% 15.33/14.81 bnd_c2_1 X65))) &
% 15.33/14.81 ((bnd_c2_0 |
% 15.33/14.81 (ALL X67.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c8_1 X67 |
% 15.33/14.81 ((bnd_ndr1_1 X67 & ~ bnd_c8_2 X67 bnd_a529) &
% 15.33/14.81 ~ bnd_c1_2 X67 bnd_a529) &
% 15.33/14.81 ~ bnd_c5_2 X67 bnd_a529) |
% 15.33/14.81 (ALL X68.
% 15.33/14.81 bnd_ndr1_1 X67 -->
% 15.33/14.81 bnd_c7_2 X67 X68 | bnd_c5_2 X67 X68))) |
% 15.33/14.81 ~ bnd_c5_0)) &
% 15.33/14.81 ((~ bnd_c2_0 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X69.
% 15.33/14.81 bnd_ndr1_1 bnd_a530 -->
% 15.33/14.81 (~ bnd_c6_2 bnd_a530 X69 |
% 15.33/14.81 bnd_c7_2 bnd_a530 X69) |
% 15.33/14.81 ~ bnd_c4_2 bnd_a530 X69)) &
% 15.33/14.81 (ALL X70.
% 15.33/14.81 bnd_ndr1_1 bnd_a530 -->
% 15.33/14.81 (~ bnd_c6_2 bnd_a530 X70 |
% 15.33/14.81 ~ bnd_c8_2 bnd_a530 X70) |
% 15.33/14.81 ~ bnd_c3_2 bnd_a530 X70)) &
% 15.33/14.81 (ALL X71.
% 15.33/14.81 bnd_ndr1_1 bnd_a530 -->
% 15.33/14.81 (bnd_c8_2 bnd_a530 X71 | bnd_c4_2 bnd_a530 X71) |
% 15.33/14.81 bnd_c7_2 bnd_a530 X71)) |
% 15.33/14.81 (ALL X72.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c8_1 X72 | ~ bnd_c6_1 X72) | bnd_c1_1 X72))) &
% 15.33/14.81 (((bnd_ndr1_0 & bnd_c4_1 bnd_a531) & ~ bnd_c5_1 bnd_a531) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a531 |
% 15.33/14.81 (ALL X73.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X74.
% 15.33/14.81 bnd_ndr1_1 X73 -->
% 15.33/14.81 (bnd_c3_2 X73 X74 | ~ bnd_c8_2 X73 X74) |
% 15.33/14.81 ~ bnd_c1_2 X73 X74) |
% 15.33/14.81 bnd_c5_1 X73) |
% 15.33/14.81 (ALL X75.
% 15.33/14.81 bnd_ndr1_1 X73 -->
% 15.33/14.81 (bnd_c3_2 X73 X75 | bnd_c6_2 X73 X75) |
% 15.33/14.81 ~ bnd_c7_2 X73 X75)))) &
% 15.33/14.81 (((ALL X76.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c2_1 X76 |
% 15.33/14.81 (ALL X77.
% 15.33/14.81 bnd_ndr1_1 X76 -->
% 15.33/14.81 (~ bnd_c6_2 X76 X77 | bnd_c7_2 X76 X77) |
% 15.33/14.81 ~ bnd_c2_2 X76 X77)) |
% 15.33/14.81 bnd_c4_1 X76) |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X78.
% 15.33/14.81 bnd_ndr1_1 bnd_a532 -->
% 15.33/14.81 (bnd_c7_2 bnd_a532 X78 | ~ bnd_c4_2 bnd_a532 X78) |
% 15.33/14.81 ~ bnd_c8_2 bnd_a532 X78)) &
% 15.33/14.81 bnd_c3_1 bnd_a532) &
% 15.33/14.81 bnd_c1_1 bnd_a532) |
% 15.33/14.81 bnd_ndr1_0 & ~ bnd_c3_1 bnd_a533)) &
% 15.33/14.81 (((((((bnd_ndr1_0 & bnd_c8_1 bnd_a534) &
% 15.33/14.81 bnd_ndr1_1 bnd_a534) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a534 bnd_a535) &
% 15.33/14.81 bnd_c4_2 bnd_a534 bnd_a535) &
% 15.33/14.81 bnd_c8_2 bnd_a534 bnd_a535) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a534 |
% 15.33/14.81 (ALL X79.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X80.
% 15.33/14.81 bnd_ndr1_1 X79 -->
% 15.33/14.81 (~ bnd_c1_2 X79 X80 | ~ bnd_c3_2 X79 X80) |
% 15.33/14.81 ~ bnd_c6_2 X79 X80) |
% 15.33/14.81 (ALL X81.
% 15.33/14.81 bnd_ndr1_1 X79 -->
% 15.33/14.81 (bnd_c1_2 X79 X81 | bnd_c7_2 X79 X81) |
% 15.33/14.81 ~ bnd_c2_2 X79 X81)) |
% 15.33/14.81 bnd_c6_1 X79)) |
% 15.33/14.81 ~ bnd_c8_0)) &
% 15.33/14.81 ((bnd_c1_0 | ~ bnd_c2_0) | bnd_c8_0)) &
% 15.33/14.81 ((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X82.
% 15.33/14.81 bnd_ndr1_1 bnd_a536 -->
% 15.33/14.81 (bnd_c3_2 bnd_a536 X82 | bnd_c5_2 bnd_a536 X82) |
% 15.33/14.81 ~ bnd_c7_2 bnd_a536 X82)) &
% 15.33/14.81 ~ bnd_c7_1 bnd_a536) &
% 15.33/14.81 bnd_c5_1 bnd_a536 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X83.
% 15.33/14.81 bnd_ndr1_1 bnd_a537 -->
% 15.33/14.81 (~ bnd_c3_2 bnd_a537 X83 | ~ bnd_c7_2 bnd_a537 X83) |
% 15.33/14.81 ~ bnd_c2_2 bnd_a537 X83)) &
% 15.33/14.81 ~ bnd_c5_1 bnd_a537) &
% 15.33/14.81 bnd_c4_1 bnd_a537) |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X84.
% 15.33/14.81 bnd_ndr1_1 bnd_a538 -->
% 15.33/14.81 (~ bnd_c7_2 bnd_a538 X84 | bnd_c2_2 bnd_a538 X84) |
% 15.33/14.81 bnd_c3_2 bnd_a538 X84)) &
% 15.33/14.81 (ALL X85.
% 15.33/14.81 bnd_ndr1_1 bnd_a538 -->
% 15.33/14.81 (bnd_c8_2 bnd_a538 X85 | bnd_c7_2 bnd_a538 X85) |
% 15.33/14.81 ~ bnd_c1_2 bnd_a538 X85)) &
% 15.33/14.81 bnd_c1_1 bnd_a538)) &
% 15.33/14.81 ((~ bnd_c7_0 |
% 15.33/14.81 (ALL X86.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c1_1 X86 | bnd_c6_1 X86) | bnd_c5_1 X86)) |
% 15.33/14.81 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a539) &
% 15.33/14.81 bnd_c8_2 bnd_a539 bnd_a540) &
% 15.33/14.81 ~ bnd_c5_2 bnd_a539 bnd_a540) &
% 15.33/14.81 bnd_c3_2 bnd_a539 bnd_a540) &
% 15.33/14.81 bnd_c6_1 bnd_a539) &
% 15.33/14.81 bnd_ndr1_1 bnd_a539) &
% 15.33/14.81 ~ bnd_c2_2 bnd_a539 bnd_a541) &
% 15.33/14.81 ~ bnd_c5_2 bnd_a539 bnd_a541) &
% 15.33/14.81 bnd_c8_2 bnd_a539 bnd_a541)) &
% 15.33/14.81 ((~ bnd_c5_0 | ~ bnd_c7_0) |
% 15.33/14.81 (ALL X87.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c5_1 X87 | ~ bnd_c2_1 X87) | bnd_c7_1 X87))) &
% 15.33/14.81 (((ALL X88. bnd_ndr1_0 --> ~ bnd_c8_1 X88 | ~ bnd_c2_1 X88) |
% 15.33/14.81 ((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X89.
% 15.33/14.81 bnd_ndr1_1 bnd_a542 -->
% 15.33/14.81 bnd_c7_2 bnd_a542 X89 | ~ bnd_c4_2 bnd_a542 X89)) &
% 15.33/14.81 bnd_c2_1 bnd_a542) &
% 15.33/14.81 bnd_ndr1_1 bnd_a542) &
% 15.33/14.81 bnd_c8_2 bnd_a542 bnd_a543) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a542 bnd_a543) |
% 15.33/14.81 ((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X90.
% 15.33/14.81 bnd_ndr1_1 bnd_a544 -->
% 15.33/14.81 bnd_c1_2 bnd_a544 X90 | bnd_c4_2 bnd_a544 X90)) &
% 15.33/14.81 bnd_ndr1_1 bnd_a544) &
% 15.33/14.81 ~ bnd_c7_2 bnd_a544 bnd_a545) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a544 bnd_a545) &
% 15.33/14.81 ~ bnd_c3_2 bnd_a544 bnd_a545)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a546) &
% 15.33/14.81 (ALL X91.
% 15.33/14.81 bnd_ndr1_1 bnd_a546 -->
% 15.33/14.81 (bnd_c8_2 bnd_a546 X91 | ~ bnd_c1_2 bnd_a546 X91) |
% 15.33/14.81 ~ bnd_c4_2 bnd_a546 X91)) &
% 15.33/14.81 bnd_ndr1_1 bnd_a546) &
% 15.33/14.81 ~ bnd_c2_2 bnd_a546 bnd_a547) &
% 15.33/14.81 bnd_c7_2 bnd_a546 bnd_a547) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a546 bnd_a547 |
% 15.33/14.81 (ALL X92.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X93.
% 15.33/14.81 bnd_ndr1_1 X92 -->
% 15.33/14.81 (~ bnd_c6_2 X92 X93 | ~ bnd_c8_2 X92 X93) |
% 15.33/14.81 bnd_c3_2 X92 X93) |
% 15.33/14.81 ((bnd_ndr1_1 X92 & bnd_c2_2 X92 bnd_a548) &
% 15.33/14.81 ~ bnd_c4_2 X92 bnd_a548) &
% 15.33/14.81 ~ bnd_c7_2 X92 bnd_a548) |
% 15.33/14.81 ~ bnd_c1_1 X92))) &
% 15.33/14.81 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a549) &
% 15.33/14.81 bnd_c4_2 bnd_a549 bnd_a550) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a549 bnd_a550) &
% 15.33/14.81 bnd_c6_2 bnd_a549 bnd_a550) &
% 15.33/14.81 bnd_ndr1_1 bnd_a549) &
% 15.33/14.81 bnd_c2_2 bnd_a549 bnd_a551) &
% 15.33/14.81 bnd_c8_2 bnd_a549 bnd_a551) &
% 15.33/14.81 bnd_c5_2 bnd_a549 bnd_a551) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a549 |
% 15.33/14.81 ~ bnd_c4_0) |
% 15.33/14.81 ~ bnd_c8_0)) &
% 15.33/14.81 ((bnd_c7_0 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X94.
% 15.33/14.81 bnd_ndr1_1 bnd_a552 -->
% 15.33/14.81 (bnd_c6_2 bnd_a552 X94 | bnd_c8_2 bnd_a552 X94) |
% 15.33/14.81 bnd_c2_2 bnd_a552 X94)) &
% 15.33/14.81 ~ bnd_c8_1 bnd_a552) &
% 15.33/14.81 bnd_c6_1 bnd_a552) |
% 15.33/14.81 (ALL X95.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c4_1 X95 | ~ bnd_c5_1 X95) |
% 15.33/14.81 ((bnd_ndr1_1 X95 & ~ bnd_c2_2 X95 bnd_a553) &
% 15.33/14.81 bnd_c7_2 X95 bnd_a553) &
% 15.33/14.81 ~ bnd_c3_2 X95 bnd_a553))) &
% 15.33/14.81 (~ bnd_c8_0 | ~ bnd_c5_0)) &
% 15.33/14.81 (~ bnd_c5_0 |
% 15.33/14.81 (ALL X96.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c5_1 X96 |
% 15.33/14.81 (bnd_ndr1_1 X96 & ~ bnd_c6_2 X96 bnd_a554) &
% 15.33/14.81 ~ bnd_c3_2 X96 bnd_a554) |
% 15.33/14.81 ((bnd_ndr1_1 X96 & bnd_c5_2 X96 bnd_a555) &
% 15.33/14.81 bnd_c1_2 X96 bnd_a555) &
% 15.33/14.81 ~ bnd_c4_2 X96 bnd_a555))) &
% 15.33/14.81 ((bnd_c8_0 |
% 15.33/14.81 (ALL X97.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (ALL X98.
% 15.33/14.81 bnd_ndr1_1 X97 --> bnd_c2_2 X97 X98 | bnd_c7_2 X97 X98) |
% 15.33/14.81 bnd_c6_1 X97)) |
% 15.33/14.81 ~ bnd_c2_0)) &
% 15.33/14.81 ((bnd_c5_0 | ~ bnd_c2_0) | bnd_c8_0)) &
% 15.33/14.81 (((ALL X99.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c7_1 X99 | ~ bnd_c6_1 X99) |
% 15.33/14.81 ((bnd_ndr1_1 X99 & ~ bnd_c4_2 X99 bnd_a556) &
% 15.33/14.81 bnd_c8_2 X99 bnd_a556) &
% 15.33/14.81 bnd_c7_2 X99 bnd_a556) |
% 15.33/14.81 ~ bnd_c7_0) |
% 15.33/14.81 bnd_c8_0)) &
% 15.33/14.81 (((ALL X100.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X100 & ~ bnd_c6_2 X100 bnd_a557) &
% 15.33/14.81 ~ bnd_c2_2 X100 bnd_a557) &
% 15.33/14.81 bnd_c1_2 X100 bnd_a557 |
% 15.33/14.81 (ALL X101.
% 15.33/14.81 bnd_ndr1_1 X100 --> bnd_c8_2 X100 X101 | bnd_c2_2 X100 X101)) |
% 15.33/14.81 bnd_c7_1 X100) |
% 15.33/14.81 (ALL X102.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c6_1 X102 | ~ bnd_c3_1 X102) | bnd_c5_1 X102)) |
% 15.33/14.81 bnd_c5_0)) &
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c1_1 bnd_a558) & bnd_c6_1 bnd_a558 | ~ bnd_c7_0)) &
% 15.33/14.81 ((bnd_c8_0 | ~ bnd_c1_0) | bnd_c7_0)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & bnd_c7_1 bnd_a559) &
% 15.33/14.81 bnd_ndr1_1 bnd_a559) &
% 15.33/14.81 bnd_c4_2 bnd_a559 bnd_a560) &
% 15.33/14.81 bnd_c7_2 bnd_a559 bnd_a560) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a559 |
% 15.33/14.81 ~ bnd_c8_0) |
% 15.33/14.81 (ALL X103.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c8_1 X103 |
% 15.33/14.81 (ALL X104.
% 15.33/14.81 bnd_ndr1_1 X103 -->
% 15.33/14.81 (bnd_c7_2 X103 X104 | bnd_c2_2 X103 X104) | bnd_c8_2 X103 X104)) |
% 15.33/14.81 (ALL X105.
% 15.33/14.81 bnd_ndr1_1 X103 -->
% 15.33/14.81 (bnd_c3_2 X103 X105 | ~ bnd_c6_2 X103 X105) |
% 15.33/14.81 ~ bnd_c2_2 X103 X105)))) &
% 15.33/14.81 (bnd_c5_0 | ~ bnd_c1_0)) &
% 15.33/14.81 (~ bnd_c4_0 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X106.
% 15.33/14.81 bnd_ndr1_1 bnd_a561 -->
% 15.33/14.81 bnd_c8_2 bnd_a561 X106 | bnd_c4_2 bnd_a561 X106)) &
% 15.33/14.81 ~ bnd_c5_1 bnd_a561) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a561)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a562) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a562 bnd_a563) &
% 15.33/14.81 bnd_c8_2 bnd_a562 bnd_a563) &
% 15.33/14.81 bnd_c2_2 bnd_a562 bnd_a563) &
% 15.33/14.81 ~ bnd_c7_1 bnd_a562 |
% 15.33/14.81 ~ bnd_c2_0) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c7_1 bnd_a564) &
% 15.33/14.81 (ALL X107.
% 15.33/14.81 bnd_ndr1_1 bnd_a564 -->
% 15.33/14.81 (bnd_c3_2 bnd_a564 X107 | bnd_c8_2 bnd_a564 X107) |
% 15.33/14.81 ~ bnd_c1_2 bnd_a564 X107)) &
% 15.33/14.81 bnd_c5_1 bnd_a564 |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c6_1 bnd_a565) &
% 15.33/14.81 bnd_c3_1 bnd_a565) &
% 15.33/14.81 bnd_c2_1 bnd_a565) |
% 15.33/14.81 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a566) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a566 bnd_a567) &
% 15.33/14.81 bnd_c6_2 bnd_a566 bnd_a567) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a566 bnd_a567) &
% 15.33/14.81 bnd_c1_1 bnd_a566) &
% 15.33/14.81 (ALL X108.
% 15.33/14.81 bnd_ndr1_1 bnd_a566 -->
% 15.33/14.81 (~ bnd_c2_2 bnd_a566 X108 |
% 15.33/14.81 bnd_c5_2 bnd_a566 X108) |
% 15.33/14.81 ~ bnd_c1_2 bnd_a566 X108))) &
% 15.33/14.81 ((~ bnd_c7_0 |
% 15.33/14.81 (bnd_ndr1_0 &
% 15.33/14.81 (ALL X109.
% 15.33/14.81 bnd_ndr1_1 bnd_a568 --> bnd_c6_2 bnd_a568 X109 | bnd_c4_2 bnd_a568 X109)) &
% 15.33/14.81 ~ bnd_c4_1 bnd_a568) |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c4_1 bnd_a569) &
% 15.33/14.81 (ALL X110.
% 15.33/14.81 bnd_ndr1_1 bnd_a569 -->
% 15.33/14.81 (bnd_c6_2 bnd_a569 X110 |
% 15.33/14.81 bnd_c3_2 bnd_a569 X110) |
% 15.33/14.81 ~ bnd_c4_2 bnd_a569 X110)) &
% 15.33/14.81 bnd_c3_1 bnd_a569)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & bnd_c4_1 bnd_a570) &
% 15.33/14.81 bnd_c5_1 bnd_a570) &
% 15.33/14.81 bnd_ndr1_1 bnd_a570) &
% 15.33/14.81 bnd_c2_2 bnd_a570 bnd_a571) &
% 15.33/14.81 bnd_c1_2 bnd_a570 bnd_a571) &
% 15.33/14.81 bnd_c3_2 bnd_a570 bnd_a571 |
% 15.33/14.81 bnd_c5_0)) &
% 15.33/14.81 ((bnd_c1_0 | bnd_c5_0) |
% 15.33/14.81 (ALL X111.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X112.
% 15.33/14.81 bnd_ndr1_1 X111 --> bnd_c2_2 X111 X112 | bnd_c5_2 X111 X112) |
% 15.33/14.81 ((bnd_ndr1_1 X111 &
% 15.33/14.81 ~ bnd_c6_2 X111 bnd_a572) &
% 15.33/14.81 ~ bnd_c5_2 X111 bnd_a572) &
% 15.33/14.81 bnd_c2_2 X111 bnd_a572) |
% 15.33/14.81 ~ bnd_c4_1 X111))) &
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a573) &
% 15.33/14.81 bnd_c3_1 bnd_a573) &
% 15.33/14.81 (ALL X113.
% 15.33/14.81 bnd_ndr1_1 bnd_a573 -->
% 15.33/14.81 (~ bnd_c6_2 bnd_a573 X113 |
% 15.33/14.81 ~ bnd_c2_2 bnd_a573 X113) |
% 15.33/14.81 bnd_c5_2 bnd_a573 X113) |
% 15.33/14.81 (ALL X114.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c8_1 X114 |
% 15.33/14.81 (ALL X115.
% 15.33/14.81 bnd_ndr1_1 X114 -->
% 15.33/14.81 (bnd_c5_2 X114 X115 | bnd_c4_2 X114 X115) | ~ bnd_c7_2 X114 X115)) |
% 15.33/14.81 (ALL X116.
% 15.33/14.81 bnd_ndr1_1 X114 -->
% 15.33/14.81 (bnd_c2_2 X114 X116 | ~ bnd_c3_2 X114 X116) | bnd_c1_2 X114 X116))) |
% 15.33/14.81 bnd_c1_0)) &
% 15.33/14.81 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a574) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a574 bnd_a575) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a574 bnd_a575) &
% 15.33/14.81 bnd_c4_2 bnd_a574 bnd_a575) &
% 15.33/14.81 (ALL X117.
% 15.33/14.81 bnd_ndr1_1 bnd_a574 -->
% 15.33/14.81 (~ bnd_c4_2 bnd_a574 X117 |
% 15.33/14.81 ~ bnd_c2_2 bnd_a574 X117) |
% 15.33/14.81 ~ bnd_c3_2 bnd_a574 X117)) &
% 15.33/14.81 ~ bnd_c3_1 bnd_a574 |
% 15.33/14.81 ~ bnd_c2_0) |
% 15.33/14.81 (ALL X118.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c6_1 X118 | bnd_c5_1 X118) |
% 15.33/14.81 (ALL X119.
% 15.33/14.81 bnd_ndr1_1 X118 -->
% 15.33/14.81 (bnd_c8_2 X118 X119 |
% 15.33/14.81 bnd_c7_2 X118 X119) |
% 15.33/14.81 bnd_c6_2 X118 X119)))) &
% 15.33/14.81 (((ALL X120.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X121.
% 15.33/14.81 bnd_ndr1_1 X120 -->
% 15.33/14.81 (bnd_c3_2 X120 X121 |
% 15.33/14.81 ~ bnd_c2_2 X120 X121) |
% 15.33/14.81 bnd_c8_2 X120 X121) |
% 15.33/14.81 (ALL X122.
% 15.33/14.81 bnd_ndr1_1 X120 -->
% 15.33/14.81 (~ bnd_c1_2 X120 X122 |
% 15.33/14.81 bnd_c5_2 X120 X122) |
% 15.33/14.81 bnd_c3_2 X120 X122)) |
% 15.33/14.81 (ALL X123.
% 15.33/14.81 bnd_ndr1_1 X120 -->
% 15.33/14.81 bnd_c6_2 X120 X123 |
% 15.33/14.81 bnd_c2_2 X120 X123)) |
% 15.33/14.81 (ALL X124.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c7_1 X124 | ~ bnd_c1_1 X124) |
% 15.33/14.81 (bnd_ndr1_1 X124 & bnd_c4_2 X124 bnd_a576) &
% 15.33/14.81 ~ bnd_c8_2 X124 bnd_a576)) |
% 15.33/14.81 (((((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a577) &
% 15.33/14.81 bnd_ndr1_1 bnd_a577) &
% 15.33/14.81 bnd_c8_2 bnd_a577 bnd_a578) &
% 15.33/14.81 bnd_c1_2 bnd_a577 bnd_a578) &
% 15.33/14.81 bnd_c6_2 bnd_a577 bnd_a578) &
% 15.33/14.81 bnd_ndr1_1 bnd_a577) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a577 bnd_a579) &
% 15.33/14.81 ~ bnd_c8_2 bnd_a577 bnd_a579)) &
% 15.33/14.81 (((ALL X125.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X125 &
% 15.33/14.81 bnd_c7_2 X125 bnd_a580) &
% 15.33/14.81 ~ bnd_c5_2 X125 bnd_a580) &
% 15.33/14.81 ~ bnd_c2_2 X125 bnd_a580 |
% 15.33/14.81 bnd_c4_1 X125) |
% 15.33/14.81 bnd_c8_1 X125) |
% 15.33/14.81 bnd_c8_0) |
% 15.33/14.81 (ALL X126.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c5_1 X126 | bnd_c6_1 X126) |
% 15.33/14.81 (ALL X127.
% 15.33/14.81 bnd_ndr1_1 X126 -->
% 15.33/14.81 (bnd_c4_2 X126 X127 |
% 15.33/14.81 bnd_c7_2 X126 X127) |
% 15.33/14.81 bnd_c8_2 X126 X127)))) &
% 15.33/14.81 (~ bnd_c2_0 |
% 15.33/14.81 ((bnd_ndr1_0 &
% 15.33/14.81 (ALL X128.
% 15.33/14.81 bnd_ndr1_1 bnd_a581 -->
% 15.33/14.81 (bnd_c7_2 bnd_a581 X128 |
% 15.33/14.81 bnd_c8_2 bnd_a581 X128) |
% 15.33/14.81 bnd_c2_2 bnd_a581 X128)) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a581) &
% 15.33/14.81 bnd_c8_1 bnd_a581)) &
% 15.33/14.81 (((ALL X129.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c3_1 X129 | bnd_c1_1 X129) |
% 15.33/14.81 ((bnd_ndr1_1 X129 & ~ bnd_c5_2 X129 bnd_a582) &
% 15.33/14.81 bnd_c3_2 X129 bnd_a582) &
% 15.33/14.81 bnd_c2_2 X129 bnd_a582) |
% 15.33/14.81 ~ bnd_c4_0) |
% 15.33/14.81 ~ bnd_c8_0)) &
% 15.33/14.81 (~ bnd_c7_0 | ~ bnd_c4_0)) &
% 15.33/14.81 ((ALL X130.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c4_1 X130 |
% 15.33/14.81 (ALL X131.
% 15.33/14.81 bnd_ndr1_1 X130 -->
% 15.33/14.81 (bnd_c7_2 X130 X131 | ~ bnd_c2_2 X130 X131) |
% 15.33/14.81 ~ bnd_c6_2 X130 X131)) |
% 15.33/14.81 bnd_c7_1 X130) |
% 15.33/14.81 (ALL X132.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (((bnd_ndr1_1 X132 & bnd_c7_2 X132 bnd_a583) &
% 15.33/14.81 ~ bnd_c4_2 X132 bnd_a583) &
% 15.33/14.81 bnd_c2_2 X132 bnd_a583 |
% 15.33/14.81 bnd_c5_1 X132) |
% 15.33/14.81 bnd_c7_1 X132))) &
% 15.33/14.81 (((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a584) &
% 15.33/14.81 ~ bnd_c2_1 bnd_a584) &
% 15.33/14.81 bnd_c3_1 bnd_a584 |
% 15.33/14.81 bnd_c8_0)) &
% 15.33/14.81 (((ALL X133.
% 15.33/14.81 bnd_ndr1_0 --> ~ bnd_c5_1 X133 | ~ bnd_c6_1 X133) |
% 15.33/14.81 (((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X134.
% 15.33/14.81 bnd_ndr1_1 bnd_a585 -->
% 15.33/14.81 ~ bnd_c4_2 bnd_a585 X134 |
% 15.33/14.81 bnd_c3_2 bnd_a585 X134)) &
% 15.33/14.81 ~ bnd_c8_1 bnd_a585) &
% 15.33/14.81 bnd_ndr1_1 bnd_a585) &
% 15.33/14.81 bnd_c2_2 bnd_a585 bnd_a586) &
% 15.33/14.81 ~ bnd_c3_2 bnd_a585 bnd_a586) &
% 15.33/14.81 bnd_c1_2 bnd_a585 bnd_a586) |
% 15.33/14.81 ~ bnd_c5_0)) &
% 15.33/14.81 (((bnd_ndr1_0 & bnd_c3_1 bnd_a587) &
% 15.33/14.81 (ALL X135.
% 15.33/14.81 bnd_ndr1_1 bnd_a587 -->
% 15.33/14.81 (~ bnd_c5_2 bnd_a587 X135 |
% 15.33/14.81 ~ bnd_c8_2 bnd_a587 X135) |
% 15.33/14.81 bnd_c1_2 bnd_a587 X135) |
% 15.33/14.81 (ALL X136.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X137.
% 15.33/14.81 bnd_ndr1_1 X136 -->
% 15.33/14.81 ~ bnd_c2_2 X136 X137 | bnd_c5_2 X136 X137) |
% 15.33/14.81 (bnd_ndr1_1 X136 & ~ bnd_c1_2 X136 bnd_a588) &
% 15.33/14.81 bnd_c5_2 X136 bnd_a588) |
% 15.33/14.81 ((bnd_ndr1_1 X136 & bnd_c8_2 X136 bnd_a589) &
% 15.33/14.81 ~ bnd_c7_2 X136 bnd_a589) &
% 15.33/14.81 ~ bnd_c5_2 X136 bnd_a589)) |
% 15.33/14.81 (ALL X138.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X139.
% 15.33/14.81 bnd_ndr1_1 X138 -->
% 15.33/14.81 (~ bnd_c4_2 X138 X139 | bnd_c8_2 X138 X139) |
% 15.33/14.81 ~ bnd_c2_2 X138 X139) |
% 15.33/14.81 bnd_c6_1 X138) |
% 15.33/14.81 (ALL X140.
% 15.33/14.81 bnd_ndr1_1 X138 -->
% 15.33/14.81 (bnd_c2_2 X138 X140 | bnd_c6_2 X138 X140) |
% 15.33/14.81 ~ bnd_c8_2 X138 X140)))) &
% 15.33/14.81 ((~ bnd_c5_0 | ~ bnd_c4_0) | ~ bnd_c6_0)) &
% 15.33/14.81 ((bnd_c5_0 | bnd_c6_0) |
% 15.33/14.81 ((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a590) &
% 15.33/14.81 bnd_c7_1 bnd_a590) &
% 15.33/14.81 bnd_ndr1_1 bnd_a590) &
% 15.33/14.81 ~ bnd_c3_2 bnd_a590 bnd_a591) &
% 15.33/14.81 ~ bnd_c2_2 bnd_a590 bnd_a591)) &
% 15.33/14.81 ((((bnd_ndr1_0 &
% 15.33/14.81 (ALL X141.
% 15.33/14.81 bnd_ndr1_1 bnd_a592 -->
% 15.33/14.81 (bnd_c5_2 bnd_a592 X141 | bnd_c6_2 bnd_a592 X141) |
% 15.33/14.81 ~ bnd_c1_2 bnd_a592 X141)) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a592) &
% 15.33/14.81 (ALL X142.
% 15.33/14.81 bnd_ndr1_1 bnd_a592 -->
% 15.33/14.81 bnd_c3_2 bnd_a592 X142 | ~ bnd_c5_2 bnd_a592 X142) |
% 15.33/14.81 (ALL X143.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X144.
% 15.33/14.81 bnd_ndr1_1 X143 -->
% 15.33/14.81 (~ bnd_c7_2 X143 X144 | bnd_c6_2 X143 X144) |
% 15.33/14.81 bnd_c2_2 X143 X144) |
% 15.33/14.81 ~ bnd_c6_1 X143) |
% 15.33/14.81 ((bnd_ndr1_1 X143 & bnd_c8_2 X143 bnd_a593) &
% 15.33/14.81 ~ bnd_c7_2 X143 bnd_a593) &
% 15.33/14.81 ~ bnd_c4_2 X143 bnd_a593)) |
% 15.33/14.81 bnd_c7_0)) &
% 15.33/14.81 ((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a594) &
% 15.33/14.81 ~ bnd_c6_1 bnd_a594) &
% 15.33/14.81 bnd_ndr1_1 bnd_a594) &
% 15.33/14.81 bnd_c1_2 bnd_a594 bnd_a595) &
% 15.33/14.81 ~ bnd_c6_2 bnd_a594 bnd_a595) &
% 15.33/14.81 ~ bnd_c4_2 bnd_a594 bnd_a595 |
% 15.33/14.81 ~ bnd_c1_0)) &
% 15.33/14.81 ((~ bnd_c7_0 | bnd_c2_0) |
% 15.33/14.81 (ALL X145.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X146.
% 15.33/14.81 bnd_ndr1_1 X145 -->
% 15.33/14.81 (bnd_c1_2 X145 X146 | bnd_c7_2 X145 X146) |
% 15.33/14.81 bnd_c4_2 X145 X146) |
% 15.33/14.81 bnd_c3_1 X145) |
% 15.33/14.81 bnd_c6_1 X145))) &
% 15.33/14.81 ((((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a596) & bnd_c7_1 bnd_a596) &
% 15.33/14.81 (ALL X147.
% 15.33/14.81 bnd_ndr1_1 bnd_a596 -->
% 15.33/14.81 ~ bnd_c4_2 bnd_a596 X147 | ~ bnd_c1_2 bnd_a596 X147) |
% 15.33/14.81 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a597) &
% 15.33/14.81 bnd_c4_2 bnd_a597 bnd_a598) &
% 15.33/14.81 bnd_c3_2 bnd_a597 bnd_a598) &
% 15.33/14.81 bnd_c7_2 bnd_a597 bnd_a598) &
% 15.33/14.81 ~ bnd_c1_1 bnd_a597) &
% 15.33/14.81 bnd_ndr1_1 bnd_a597) &
% 15.33/14.81 bnd_c3_2 bnd_a597 bnd_a599) &
% 15.33/14.81 bnd_c5_2 bnd_a597 bnd_a599) &
% 15.33/14.81 ~ bnd_c1_2 bnd_a597 bnd_a599) |
% 15.33/14.81 bnd_c6_0)) &
% 15.33/14.81 (bnd_c1_0 | bnd_c6_0)) &
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c3_1 bnd_a600) &
% 15.33/14.81 (ALL X148.
% 15.33/14.81 bnd_ndr1_1 bnd_a600 -->
% 15.33/14.81 ~ bnd_c1_2 bnd_a600 X148 | bnd_c7_2 bnd_a600 X148) |
% 15.33/14.81 ((bnd_ndr1_0 & bnd_c7_1 bnd_a601) & ~ bnd_c1_1 bnd_a601) &
% 15.33/14.81 bnd_c5_1 bnd_a601)) &
% 15.33/14.81 ((~ bnd_c1_0 | bnd_c5_0) | ~ bnd_c8_0)) &
% 15.33/14.81 (((ALL X149.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 ((ALL X150.
% 15.33/14.81 bnd_ndr1_1 X149 -->
% 15.33/14.81 (~ bnd_c8_2 X149 X150 | bnd_c1_2 X149 X150) |
% 15.33/14.81 bnd_c3_2 X149 X150) |
% 15.33/14.81 bnd_c8_1 X149) |
% 15.33/14.81 bnd_c4_1 X149) |
% 15.33/14.81 bnd_c1_0) |
% 15.33/14.81 (ALL X151.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c3_1 X151 | ~ bnd_c1_1 X151) | bnd_c8_1 X151))) &
% 15.33/14.81 (((ALL X152.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (~ bnd_c3_1 X152 | bnd_c1_1 X152) | bnd_c6_1 X152) |
% 15.33/14.81 ~ bnd_c1_0) |
% 15.33/14.81 bnd_c5_0)) &
% 15.33/14.81 ((bnd_c2_0 | ~ bnd_c7_0) | ~ bnd_c8_0)) &
% 15.33/14.81 ((bnd_c1_0 |
% 15.33/14.81 (ALL X153.
% 15.33/14.81 bnd_ndr1_0 -->
% 15.33/14.81 (bnd_c2_1 X153 |
% 15.33/14.81 ((bnd_ndr1_1 X153 & bnd_c3_2 X153 bnd_a602) &
% 15.33/14.81 bnd_c4_2 X153 bnd_a602) &
% 15.33/14.81 ~ bnd_c7_2 X153 bnd_a602) |
% 15.33/14.81 bnd_c7_1 X153)) |
% 15.33/14.81 ~ bnd_c7_0)) &
% 15.33/14.81 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a603) &
% 15.33/14.81 (ALL X154.
% 15.33/14.81 bnd_ndr1_1 bnd_a603 -->
% 15.33/14.81 (~ bnd_c3_2 bnd_a603 X154 | bnd_c7_2 bnd_a603 X154) |
% 15.33/14.81 ~ bnd_c5_2 bnd_a603 X154)) &
% 15.33/14.81 ~ bnd_c4_1 bnd_a603 |
% 15.33/14.81 ~ bnd_c5_0) |
% 15.33/14.81 ~ bnd_c8_0)) &
% 15.33/14.81 ((bnd_c8_0 | ~ bnd_c7_0) | bnd_c5_0))
% 15.33/14.81 Adding axioms...
% 15.33/14.82 Typedef.type_definition_def
% 41.56/41.05 ...done.
% 41.56/41.08 Ground types: ?'b, TPTP_Interpret.ind
% 41.56/41.08 Translating term (sizes: 1, 1) ...
% 63.22/62.62 Invoking SAT solver...
% 63.22/62.62 No model exists.
% 63.22/62.62 Translating term (sizes: 2, 1) ...
% 85.57/84.93 Invoking SAT solver...
% 85.57/84.93 No model exists.
% 85.57/84.93 Translating term (sizes: 1, 2) ...
% 126.52/125.79 Invoking SAT solver...
% 127.03/126.22 Model found:
% 127.03/126.22 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 127.03/126.22 bnd_a603: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a602: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a601: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a600: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a599: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a598: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a597: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a596: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a595: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a594: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a593: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a592: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a591: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a590: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a589: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a588: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a587: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a586: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a585: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a584: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a583: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a582: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a581: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a580: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a579: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a578: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a577: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a576: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a575: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a574: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a573: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a572: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a571: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a570: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a569: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a568: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a567: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a566: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a565: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a564: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a563: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a562: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a561: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a560: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a559: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a558: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a557: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a556: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a555: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a554: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a553: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a552: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a551: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a550: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a549: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a548: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a547: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a546: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a545: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a544: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a543: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a542: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a541: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a540: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a539: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a538: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a537: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a536: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a535: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a534: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a533: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a532: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a531: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a530: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a529: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a528: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a527: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a526: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a525: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a524: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a523: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a522: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a521: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a520: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a519: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a518: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a517: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a516: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a515: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a514: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a513: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a512: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a511: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a510: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a509: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a508: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a507: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a506: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a505: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a504: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a503: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a502: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a501: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a500: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a499: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a498: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a497: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a496: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a495: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a494: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a493: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a492: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a491: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a490: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a489: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a488: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a487: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a486: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a485: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a484: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a483: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a482: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a481: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a480: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a479: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a478: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a477: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a476: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a475: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a474: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a473: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c3_0: True
% 127.03/126.22 bnd_a472: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a471: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a470: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a469: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a468: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c4_0: False
% 127.03/126.22 bnd_a467: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a466: ??.TPTP_Interpret.ind1
% 127.03/126.22 bnd_a465: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_a464: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c5_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_c1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_a463: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c7_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_c5_0: False
% 127.03/126.22 bnd_a462: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c2_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_a461: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c1_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_a460: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c6_0: True
% 127.03/126.22 bnd_a459: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c8_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 127.03/126.22 bnd_c3_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_c3_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_c2_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}
% 127.03/126.22 bnd_a458: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c6_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_c8_0: True
% 127.03/126.22 bnd_c1_0: False
% 127.03/126.22 bnd_c7_0: True
% 127.03/126.22 bnd_c2_0: True
% 127.03/126.22 bnd_c5_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_c7_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_a457: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c8_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 127.03/126.22 bnd_c6_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 127.03/126.22 bnd_a456: ??.TPTP_Interpret.ind0
% 127.03/126.22 bnd_c4_2: {(??.TPTP_Interpret.ind0,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 127.03/126.22 (??.TPTP_Interpret.ind1,
% 127.03/126.22 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 127.03/126.22 bnd_ndr1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_c4_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 127.03/126.22 bnd_ndr1_0: True
% 127.03/126.22
% 127.03/126.22 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------