%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN544+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n073.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:20 EDT 2016
% Result : CounterSatisfiable 126.36s
% 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 : SYN544+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.23 % Computer : n073.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:15:54 CDT 2016
% 0.02/0.23 % CPUTime:
% 6.27/5.83 > val it = (): unit
% 6.98/6.59 Trying to find a model that refutes: ~ (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c7_1 U | ~ bnd_c5_1 U) | bnd_c2_1 U) |
% 6.98/6.59 (ALL V.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 V & ~ bnd_c4_2 V bnd_a1) &
% 6.98/6.59 ~ bnd_c1_2 V bnd_a1 |
% 6.98/6.59 ((bnd_ndr1_1 V & ~ bnd_c1_2 V bnd_a2) &
% 6.98/6.59 bnd_c7_2 V bnd_a2) &
% 6.98/6.59 bnd_c4_2 V bnd_a2) |
% 6.98/6.59 (bnd_ndr1_1 V & ~ bnd_c7_2 V bnd_a3) &
% 6.98/6.59 bnd_c6_2 V bnd_a3)) |
% 6.98/6.59 ~ bnd_c5_0) &
% 6.98/6.59 (((ALL W.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c1_1 W |
% 6.98/6.59 ((bnd_ndr1_1 W & ~ bnd_c4_2 W bnd_a4) &
% 6.98/6.59 ~ bnd_c3_2 W bnd_a4) &
% 6.98/6.59 ~ bnd_c7_2 W bnd_a4) |
% 6.98/6.59 ((bnd_ndr1_1 W & ~ bnd_c4_2 W bnd_a5) &
% 6.98/6.59 bnd_c3_2 W bnd_a5) &
% 6.98/6.59 ~ bnd_c5_2 W bnd_a5) |
% 6.98/6.59 (ALL X.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL Y.
% 6.98/6.59 bnd_ndr1_1 X -->
% 6.98/6.59 (~ bnd_c2_2 X Y | ~ bnd_c4_2 X Y) |
% 6.98/6.59 ~ bnd_c5_2 X Y) |
% 6.98/6.59 ~ bnd_c1_1 X) |
% 6.98/6.59 bnd_c2_1 X)) |
% 6.98/6.59 ~ bnd_c8_0)) &
% 6.98/6.59 ((bnd_c5_0 |
% 6.98/6.59 (ALL Z.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 Z & bnd_c2_2 Z bnd_a6) &
% 6.98/6.59 ~ bnd_c7_2 Z bnd_a6) &
% 6.98/6.59 bnd_c8_2 Z bnd_a6 |
% 6.98/6.59 ~ bnd_c2_1 Z) |
% 6.98/6.59 ~ bnd_c3_1 Z)) |
% 6.98/6.59 (ALL X1.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X1 & bnd_c1_2 X1 bnd_a7) &
% 6.98/6.59 bnd_c6_2 X1 bnd_a7) &
% 6.98/6.59 bnd_c3_2 X1 bnd_a7 |
% 6.98/6.59 ~ bnd_c8_1 X1) |
% 6.98/6.59 (ALL X2.
% 6.98/6.59 bnd_ndr1_1 X1 -->
% 6.98/6.59 (~ bnd_c2_2 X1 X2 | bnd_c4_2 X1 X2) |
% 6.98/6.59 bnd_c3_2 X1 X2)))) &
% 6.98/6.59 ((~ bnd_c2_0 |
% 6.98/6.59 (ALL X3.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ~ bnd_c5_1 X3 |
% 6.98/6.59 (bnd_ndr1_1 X3 & ~ bnd_c4_2 X3 bnd_a8) &
% 6.98/6.59 bnd_c2_2 X3 bnd_a8)) |
% 6.98/6.59 ((bnd_ndr1_0 & bnd_c4_1 bnd_a9) &
% 6.98/6.59 (ALL X4.
% 6.98/6.59 bnd_ndr1_1 bnd_a9 -->
% 6.98/6.59 (~ bnd_c1_2 bnd_a9 X4 | ~ bnd_c5_2 bnd_a9 X4) |
% 6.98/6.59 ~ bnd_c4_2 bnd_a9 X4)) &
% 6.98/6.59 bnd_c3_1 bnd_a9)) &
% 6.98/6.59 (((ALL X5.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X6.
% 6.98/6.59 bnd_ndr1_1 X5 -->
% 6.98/6.59 ~ bnd_c8_2 X5 X6 | bnd_c7_2 X5 X6) |
% 6.98/6.59 bnd_c7_1 X5) |
% 6.98/6.59 (ALL X7.
% 6.98/6.59 bnd_ndr1_1 X5 -->
% 6.98/6.59 (~ bnd_c8_2 X5 X7 | ~ bnd_c2_2 X5 X7) |
% 6.98/6.59 ~ bnd_c4_2 X5 X7)) |
% 6.98/6.59 bnd_c1_0) |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 (((ALL X8.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c4_1 X8 |
% 6.98/6.59 (ALL X9.
% 6.98/6.59 bnd_ndr1_1 X8 -->
% 6.98/6.59 bnd_c6_2 X8 X9 | ~ bnd_c2_2 X8 X9)) |
% 6.98/6.59 ~ bnd_c5_1 X8) |
% 6.98/6.59 ~ bnd_c8_0) |
% 6.98/6.59 ~ bnd_c4_0)) &
% 6.98/6.59 (((ALL X10.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X10 & ~ bnd_c5_2 X10 bnd_a10) &
% 6.98/6.59 bnd_c7_2 X10 bnd_a10) &
% 6.98/6.59 ~ bnd_c6_2 X10 bnd_a10 |
% 6.98/6.59 (ALL X11.
% 6.98/6.59 bnd_ndr1_1 X10 -->
% 6.98/6.59 (bnd_c3_2 X10 X11 | bnd_c2_2 X10 X11) |
% 6.98/6.59 ~ bnd_c1_2 X10 X11)) |
% 6.98/6.59 ~ bnd_c1_1 X10) |
% 6.98/6.59 ((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a11) &
% 6.98/6.59 bnd_ndr1_1 bnd_a11) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a11 bnd_a12) &
% 6.98/6.59 bnd_c5_2 bnd_a11 bnd_a12) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a11 bnd_a12) |
% 6.98/6.59 bnd_c7_0)) &
% 6.98/6.59 (((ALL X12.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X13.
% 6.98/6.59 bnd_ndr1_1 X12 -->
% 6.98/6.59 bnd_c5_2 X12 X13 | bnd_c1_2 X12 X13) |
% 6.98/6.59 ~ bnd_c1_1 X12) |
% 6.98/6.59 ((bnd_ndr1_1 X12 & ~ bnd_c2_2 X12 bnd_a13) &
% 6.98/6.59 ~ bnd_c8_2 X12 bnd_a13) &
% 6.98/6.59 bnd_c6_2 X12 bnd_a13) |
% 6.98/6.59 (((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a14) &
% 6.98/6.59 bnd_ndr1_1 bnd_a14) &
% 6.98/6.59 bnd_c6_2 bnd_a14 bnd_a15) &
% 6.98/6.59 bnd_c3_2 bnd_a14 bnd_a15) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a14 bnd_a15) &
% 6.98/6.59 ~ bnd_c7_1 bnd_a14) |
% 6.98/6.59 ~ bnd_c3_0)) &
% 6.98/6.59 ((bnd_c2_0 | ~ bnd_c8_0) |
% 6.98/6.59 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a16) & ~ bnd_c8_1 bnd_a16) &
% 6.98/6.59 bnd_c1_1 bnd_a16)) &
% 6.98/6.59 ((bnd_c7_0 | bnd_c2_0) |
% 6.98/6.59 (ALL X14.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X14 & ~ bnd_c6_2 X14 bnd_a17) &
% 6.98/6.59 bnd_c5_2 X14 bnd_a17) &
% 6.98/6.59 bnd_c3_2 X14 bnd_a17 |
% 6.98/6.59 bnd_c8_1 X14) |
% 6.98/6.59 ~ bnd_c5_1 X14))) &
% 6.98/6.59 ((~ bnd_c5_0 |
% 6.98/6.59 (ALL X15.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c1_1 X15 |
% 6.98/6.59 (ALL X16.
% 6.98/6.59 bnd_ndr1_1 X15 -->
% 6.98/6.59 bnd_c7_2 X15 X16 | ~ bnd_c2_2 X15 X16)) |
% 6.98/6.59 (ALL X17.
% 6.98/6.59 bnd_ndr1_1 X15 -->
% 6.98/6.59 (bnd_c5_2 X15 X17 | ~ bnd_c2_2 X15 X17) |
% 6.98/6.59 bnd_c8_2 X15 X17))) |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 ((~ bnd_c6_0 |
% 6.98/6.59 (ALL X18.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X19.
% 6.98/6.59 bnd_ndr1_1 X18 -->
% 6.98/6.59 (~ bnd_c1_2 X18 X19 | ~ bnd_c7_2 X18 X19) |
% 6.98/6.59 bnd_c2_2 X18 X19) |
% 6.98/6.59 bnd_c2_1 X18) |
% 6.98/6.59 bnd_c3_1 X18)) |
% 6.98/6.59 (bnd_ndr1_0 & bnd_c6_1 bnd_a18) & bnd_c1_1 bnd_a18)) &
% 6.98/6.59 ((~ bnd_c1_0 |
% 6.98/6.59 ((((((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X20.
% 6.98/6.59 bnd_ndr1_1 bnd_a19 -->
% 6.98/6.59 (bnd_c6_2 bnd_a19 X20 | bnd_c8_2 bnd_a19 X20) |
% 6.98/6.59 bnd_c3_2 bnd_a19 X20)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a19) &
% 6.98/6.59 bnd_c4_2 bnd_a19 bnd_a20) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a19 bnd_a20) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a19 bnd_a20) &
% 6.98/6.59 bnd_ndr1_1 bnd_a19) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a19 bnd_a21) &
% 6.98/6.59 bnd_c3_2 bnd_a19 bnd_a21) &
% 6.98/6.59 bnd_c7_2 bnd_a19 bnd_a21) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 (((ALL X21.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 X21 & ~ bnd_c7_2 X21 bnd_a22) &
% 6.98/6.59 ~ bnd_c6_2 X21 bnd_a22 |
% 6.98/6.59 ((bnd_ndr1_1 X21 & ~ bnd_c6_2 X21 bnd_a23) &
% 6.98/6.59 ~ bnd_c3_2 X21 bnd_a23) &
% 6.98/6.59 ~ bnd_c2_2 X21 bnd_a23) |
% 6.98/6.59 (ALL X22.
% 6.98/6.59 bnd_ndr1_1 X21 -->
% 6.98/6.59 (~ bnd_c8_2 X21 X22 | bnd_c1_2 X21 X22) |
% 6.98/6.59 ~ bnd_c5_2 X21 X22)) |
% 6.98/6.59 bnd_c5_0) |
% 6.98/6.59 bnd_c8_0)) &
% 6.98/6.59 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a24) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a24 bnd_a25) &
% 6.98/6.59 bnd_c3_2 bnd_a24 bnd_a25) &
% 6.98/6.59 bnd_c1_2 bnd_a24 bnd_a25) &
% 6.98/6.59 ~ bnd_c2_1 bnd_a24) &
% 6.98/6.59 bnd_ndr1_1 bnd_a24) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a24 bnd_a26) &
% 6.98/6.59 bnd_c2_2 bnd_a24 bnd_a26) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a24 bnd_a26 |
% 6.98/6.59 (((((bnd_ndr1_0 & bnd_c8_1 bnd_a27) &
% 6.98/6.59 (ALL X23.
% 6.98/6.59 bnd_ndr1_1 bnd_a27 -->
% 6.98/6.59 (bnd_c5_2 bnd_a27 X23 | bnd_c8_2 bnd_a27 X23) |
% 6.98/6.59 ~ bnd_c7_2 bnd_a27 X23)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a27) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a27 bnd_a28) &
% 6.98/6.59 bnd_c2_2 bnd_a27 bnd_a28) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a27 bnd_a28) |
% 6.98/6.59 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a29) &
% 6.98/6.59 bnd_c7_2 bnd_a29 bnd_a30) &
% 6.98/6.59 bnd_c2_2 bnd_a29 bnd_a30) &
% 6.98/6.59 bnd_c1_2 bnd_a29 bnd_a30) &
% 6.98/6.59 bnd_ndr1_1 bnd_a29) &
% 6.98/6.59 bnd_c5_2 bnd_a29 bnd_a31) &
% 6.98/6.59 bnd_c6_2 bnd_a29 bnd_a31) &
% 6.98/6.59 (ALL X24.
% 6.98/6.59 bnd_ndr1_1 bnd_a29 -->
% 6.98/6.59 (bnd_c1_2 bnd_a29 X24 | ~ bnd_c6_2 bnd_a29 X24) |
% 6.98/6.59 bnd_c5_2 bnd_a29 X24))) &
% 6.98/6.59 ((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X25.
% 6.98/6.59 bnd_ndr1_1 bnd_a32 -->
% 6.98/6.59 bnd_c4_2 bnd_a32 X25 | bnd_c1_2 bnd_a32 X25)) &
% 6.98/6.59 (ALL X26.
% 6.98/6.59 bnd_ndr1_1 bnd_a32 -->
% 6.98/6.59 (bnd_c6_2 bnd_a32 X26 | bnd_c1_2 bnd_a32 X26) |
% 6.98/6.59 ~ bnd_c3_2 bnd_a32 X26)) &
% 6.98/6.59 bnd_c2_1 bnd_a32 |
% 6.98/6.59 (ALL X27.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c1_1 X27 |
% 6.98/6.59 ((bnd_ndr1_1 X27 & bnd_c4_2 X27 bnd_a33) &
% 6.98/6.59 bnd_c1_2 X27 bnd_a33) &
% 6.98/6.59 bnd_c3_2 X27 bnd_a33) |
% 6.98/6.59 ~ bnd_c4_1 X27)) |
% 6.98/6.59 ~ bnd_c1_0)) &
% 6.98/6.59 ((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X28. bnd_ndr1_1 bnd_a34 --> ~ bnd_c7_2 bnd_a34 X28)) &
% 6.98/6.59 (ALL X29.
% 6.98/6.59 bnd_ndr1_1 bnd_a34 -->
% 6.98/6.59 (~ bnd_c1_2 bnd_a34 X29 | bnd_c2_2 bnd_a34 X29) |
% 6.98/6.59 bnd_c7_2 bnd_a34 X29)) &
% 6.98/6.59 (ALL X30.
% 6.98/6.59 bnd_ndr1_1 bnd_a34 -->
% 6.98/6.59 (bnd_c1_2 bnd_a34 X30 | ~ bnd_c8_2 bnd_a34 X30) |
% 6.98/6.59 bnd_c4_2 bnd_a34 X30) |
% 6.98/6.59 bnd_c2_0) |
% 6.98/6.59 bnd_c3_0)) &
% 6.98/6.59 (((((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X31.
% 6.98/6.59 bnd_ndr1_1 bnd_a35 -->
% 6.98/6.59 (bnd_c8_2 bnd_a35 X31 | ~ bnd_c1_2 bnd_a35 X31) |
% 6.98/6.59 ~ bnd_c2_2 bnd_a35 X31)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a35) &
% 6.98/6.59 ~ bnd_c2_2 bnd_a35 bnd_a36) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a35 bnd_a36) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a35 bnd_a36) &
% 6.98/6.59 ~ bnd_c4_1 bnd_a35 |
% 6.98/6.59 (((((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a37) & bnd_ndr1_1 bnd_a37) &
% 6.98/6.59 bnd_c5_2 bnd_a37 bnd_a38) &
% 6.98/6.59 bnd_c4_2 bnd_a37 bnd_a38) &
% 6.98/6.59 bnd_c3_2 bnd_a37 bnd_a38) &
% 6.98/6.59 ~ bnd_c1_1 bnd_a37) |
% 6.98/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a39) &
% 6.98/6.59 bnd_c5_2 bnd_a39 bnd_a40) &
% 6.98/6.59 bnd_c3_2 bnd_a39 bnd_a40) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a39 bnd_a40) &
% 6.98/6.59 (ALL X32.
% 6.98/6.59 bnd_ndr1_1 bnd_a39 -->
% 6.98/6.59 ~ bnd_c8_2 bnd_a39 X32 | bnd_c7_2 bnd_a39 X32)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a39) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a39 bnd_a41) &
% 6.98/6.59 bnd_c6_2 bnd_a39 bnd_a41) &
% 6.98/6.59 ~ bnd_c2_2 bnd_a39 bnd_a41)) &
% 6.98/6.59 ((bnd_c2_0 | bnd_c7_0) | ~ bnd_c4_0)) &
% 6.98/6.59 ((~ bnd_c8_0 |
% 6.98/6.59 (ALL X33.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X34.
% 6.98/6.59 bnd_ndr1_1 X33 -->
% 6.98/6.59 (~ bnd_c2_2 X33 X34 | bnd_c3_2 X33 X34) |
% 6.98/6.59 ~ bnd_c6_2 X33 X34) |
% 6.98/6.59 ~ bnd_c8_1 X33) |
% 6.98/6.59 bnd_c7_1 X33)) |
% 6.98/6.59 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a42) & ~ bnd_c7_2 bnd_a42 bnd_a43) &
% 6.98/6.59 bnd_c8_2 bnd_a42 bnd_a43) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a42 bnd_a43) &
% 6.98/6.59 ~ bnd_c7_1 bnd_a42) &
% 6.98/6.59 (ALL X35.
% 6.98/6.59 bnd_ndr1_1 bnd_a42 -->
% 6.98/6.59 (bnd_c1_2 bnd_a42 X35 | ~ bnd_c7_2 bnd_a42 X35) |
% 6.98/6.59 bnd_c4_2 bnd_a42 X35))) &
% 6.98/6.59 ((((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a44) & bnd_ndr1_1 bnd_a44) &
% 6.98/6.59 bnd_c5_2 bnd_a44 bnd_a45) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a44 bnd_a45) &
% 6.98/6.59 (ALL X36.
% 6.98/6.59 bnd_ndr1_1 bnd_a44 -->
% 6.98/6.59 ~ bnd_c4_2 bnd_a44 X36 | ~ bnd_c5_2 bnd_a44 X36) |
% 6.98/6.59 (ALL X37.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X38.
% 6.98/6.59 bnd_ndr1_1 X37 -->
% 6.98/6.59 (bnd_c4_2 X37 X38 | ~ bnd_c6_2 X37 X38) | bnd_c5_2 X37 X38) |
% 6.98/6.59 (bnd_ndr1_1 X37 & ~ bnd_c8_2 X37 bnd_a46) &
% 6.98/6.59 ~ bnd_c3_2 X37 bnd_a46) |
% 6.98/6.59 ~ bnd_c7_1 X37)) |
% 6.98/6.59 (ALL X39.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c3_1 X39 |
% 6.98/6.59 (ALL X40.
% 6.98/6.59 bnd_ndr1_1 X39 -->
% 6.98/6.59 (bnd_c3_2 X39 X40 | bnd_c6_2 X39 X40) | bnd_c4_2 X39 X40)) |
% 6.98/6.59 (ALL X41.
% 6.98/6.59 bnd_ndr1_1 X39 -->
% 6.98/6.59 (bnd_c5_2 X39 X41 | bnd_c1_2 X39 X41) | bnd_c8_2 X39 X41)))) &
% 6.98/6.59 (bnd_c8_0 |
% 6.98/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a47) & ~ bnd_c2_2 bnd_a47 bnd_a48) &
% 6.98/6.59 bnd_c8_2 bnd_a47 bnd_a48) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a47 bnd_a48) &
% 6.98/6.59 ~ bnd_c6_1 bnd_a47) &
% 6.98/6.59 bnd_ndr1_1 bnd_a47) &
% 6.98/6.59 ~ bnd_c2_2 bnd_a47 bnd_a49) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a47 bnd_a49) &
% 6.98/6.59 bnd_c7_2 bnd_a47 bnd_a49)) &
% 6.98/6.59 (((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a50) & bnd_c1_1 bnd_a50 | bnd_c7_0) |
% 6.98/6.59 bnd_c4_0)) &
% 6.98/6.59 ((~ bnd_c8_0 |
% 6.98/6.59 (ALL X42.
% 6.98/6.59 bnd_ndr1_0 --> (~ bnd_c5_1 X42 | bnd_c6_1 X42) | bnd_c2_1 X42)) |
% 6.98/6.59 ~ bnd_c4_0)) &
% 6.98/6.59 ((bnd_c2_0 | bnd_c3_0) |
% 6.98/6.59 ((bnd_ndr1_0 & bnd_c5_1 bnd_a51) & ~ bnd_c7_1 bnd_a51) &
% 6.98/6.59 (ALL X43.
% 6.98/6.59 bnd_ndr1_1 bnd_a51 -->
% 6.98/6.59 (bnd_c3_2 bnd_a51 X43 | ~ bnd_c5_2 bnd_a51 X43) |
% 6.98/6.59 bnd_c4_2 bnd_a51 X43))) &
% 6.98/6.59 ((ALL X44.
% 6.98/6.59 bnd_ndr1_0 --> (~ bnd_c3_1 X44 | bnd_c2_1 X44) | ~ bnd_c7_1 X44) |
% 6.98/6.59 (ALL X45.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c1_1 X45 |
% 6.98/6.59 (ALL X46.
% 6.98/6.59 bnd_ndr1_1 X45 -->
% 6.98/6.59 (bnd_c4_2 X45 X46 | ~ bnd_c6_2 X45 X46) | ~ bnd_c3_2 X45 X46)) |
% 6.98/6.59 ~ bnd_c6_1 X45))) &
% 6.98/6.59 ((~ bnd_c7_0 | ~ bnd_c6_0) |
% 6.98/6.59 ~ bnd_c3_0)) &
% 6.98/6.59 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a52) &
% 6.98/6.59 (ALL X47.
% 6.98/6.59 bnd_ndr1_1 bnd_a52 -->
% 6.98/6.59 (~ bnd_c5_2 bnd_a52 X47 | ~ bnd_c8_2 bnd_a52 X47) |
% 6.98/6.59 ~ bnd_c7_2 bnd_a52 X47)) &
% 6.98/6.59 bnd_c8_1 bnd_a52 |
% 6.98/6.59 (((((((bnd_ndr1_0 &
% 6.98/6.59 bnd_ndr1_1 bnd_a53) &
% 6.98/6.59 bnd_c4_2 bnd_a53 bnd_a54) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a53 bnd_a54) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a53 bnd_a54) &
% 6.98/6.59 bnd_c1_1 bnd_a53) &
% 6.98/6.59 bnd_ndr1_1 bnd_a53) &
% 6.98/6.59 bnd_c2_2 bnd_a53 bnd_a55) &
% 6.98/6.59 bnd_c6_2 bnd_a53 bnd_a55) |
% 6.98/6.59 ~ bnd_c5_0)) &
% 6.98/6.59 ((bnd_c8_0 |
% 6.98/6.59 (ALL X48.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c5_1 X48 |
% 6.98/6.59 (ALL X49.
% 6.98/6.59 bnd_ndr1_1 X48 -->
% 6.98/6.59 (~ bnd_c4_2 X48 X49 | ~ bnd_c1_2 X48 X49) | ~ bnd_c6_2 X48 X49)) |
% 6.98/6.59 ((bnd_ndr1_1 X48 & bnd_c3_2 X48 bnd_a56) & ~ bnd_c2_2 X48 bnd_a56) &
% 6.98/6.59 bnd_c7_2 X48 bnd_a56)) |
% 6.98/6.59 (ALL X50.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X50 & ~ bnd_c7_2 X50 bnd_a57) & bnd_c2_2 X50 bnd_a57) &
% 6.98/6.59 bnd_c5_2 X50 bnd_a57 |
% 6.98/6.59 ~ bnd_c3_1 X50) |
% 6.98/6.59 ((bnd_ndr1_1 X50 & ~ bnd_c3_2 X50 bnd_a58) & ~ bnd_c5_2 X50 bnd_a58) &
% 6.98/6.59 bnd_c6_2 X50 bnd_a58))) &
% 6.98/6.59 ((bnd_c3_0 | bnd_c2_0) |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X51.
% 6.98/6.59 bnd_ndr1_1 bnd_a59 --> bnd_c7_2 bnd_a59 X51 | bnd_c5_2 bnd_a59 X51)) &
% 6.98/6.59 ~ bnd_c4_1 bnd_a59) &
% 6.98/6.59 bnd_c3_1 bnd_a59)) &
% 6.98/6.59 ((~ bnd_c4_0 | ~ bnd_c2_0) | bnd_c3_0)) &
% 6.98/6.59 (((ALL X52.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 bnd_c1_1 X52 | ~ bnd_c4_1 X52) |
% 6.98/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a60) &
% 6.98/6.59 ~ bnd_c2_2 bnd_a60 bnd_a61) &
% 6.98/6.59 bnd_c8_2 bnd_a60 bnd_a61) &
% 6.98/6.59 bnd_c5_2 bnd_a60 bnd_a61) &
% 6.98/6.59 (ALL X53.
% 6.98/6.59 bnd_ndr1_1 bnd_a60 -->
% 6.98/6.59 (~ bnd_c7_2 bnd_a60 X53 | bnd_c5_2 bnd_a60 X53) |
% 6.98/6.59 ~ bnd_c2_2 bnd_a60 X53)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a60) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a60 bnd_a62) &
% 6.98/6.59 bnd_c2_2 bnd_a60 bnd_a62) &
% 6.98/6.59 bnd_c3_2 bnd_a60 bnd_a62) |
% 6.98/6.59 (ALL X54.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c2_1 X54 | ~ bnd_c3_1 X54) |
% 6.98/6.59 (ALL X55.
% 6.98/6.59 bnd_ndr1_1 X54 -->
% 6.98/6.59 (~ bnd_c3_2 X54 X55 | bnd_c5_2 X54 X55) | bnd_c6_2 X54 X55)))) &
% 6.98/6.59 (((ALL X56.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c7_1 X56 | bnd_c6_1 X56) |
% 6.98/6.59 ((bnd_ndr1_1 X56 &
% 6.98/6.59 ~ bnd_c2_2 X56 bnd_a63) &
% 6.98/6.59 bnd_c4_2 X56 bnd_a63) &
% 6.98/6.59 ~ bnd_c5_2 X56 bnd_a63) |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X57.
% 6.98/6.59 bnd_ndr1_1 bnd_a64 -->
% 6.98/6.59 (bnd_c4_2 bnd_a64 X57 |
% 6.98/6.59 ~ bnd_c2_2 bnd_a64 X57) |
% 6.98/6.59 bnd_c8_2 bnd_a64 X57)) &
% 6.98/6.59 ~ bnd_c1_1 bnd_a64) &
% 6.98/6.59 (ALL X58.
% 6.98/6.59 bnd_ndr1_1 bnd_a64 -->
% 6.98/6.59 (bnd_c1_2 bnd_a64 X58 |
% 6.98/6.59 bnd_c4_2 bnd_a64 X58) |
% 6.98/6.59 bnd_c6_2 bnd_a64 X58)) |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 (((ALL X59.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X59 |
% 6.98/6.59 (ALL X60.
% 6.98/6.59 bnd_ndr1_1 X59 -->
% 6.98/6.59 (~ bnd_c7_2 X59 X60 | bnd_c5_2 X59 X60) | bnd_c8_2 X59 X60)) |
% 6.98/6.59 ~ bnd_c8_1 X59) |
% 6.98/6.59 bnd_c5_0) |
% 6.98/6.59 ~ bnd_c3_0)) &
% 6.98/6.59 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a65) &
% 6.98/6.59 (ALL X61.
% 6.98/6.59 bnd_ndr1_1 bnd_a65 -->
% 6.98/6.59 (bnd_c1_2 bnd_a65 X61 |
% 6.98/6.59 bnd_c4_2 bnd_a65 X61) |
% 6.98/6.59 bnd_c5_2 bnd_a65 X61)) &
% 6.98/6.59 bnd_c6_1 bnd_a65 |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X62.
% 6.98/6.59 bnd_ndr1_1 bnd_a66 -->
% 6.98/6.59 (bnd_c3_2 bnd_a66 X62 |
% 6.98/6.59 ~ bnd_c8_2 bnd_a66 X62) |
% 6.98/6.59 bnd_c5_2 bnd_a66 X62)) &
% 6.98/6.59 (ALL X63.
% 6.98/6.59 bnd_ndr1_1 bnd_a66 -->
% 6.98/6.59 (bnd_c2_2 bnd_a66 X63 |
% 6.98/6.59 ~ bnd_c8_2 bnd_a66 X63) |
% 6.98/6.59 bnd_c3_2 bnd_a66 X63)) &
% 6.98/6.59 ~ bnd_c3_1 bnd_a66) |
% 6.98/6.59 ~ bnd_c1_0)) &
% 6.98/6.59 ((ALL X64.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c2_1 X64 | bnd_c3_1 X64) |
% 6.98/6.59 bnd_c5_1 X64) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 ((~ bnd_c7_0 |
% 6.98/6.59 (ALL X65.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 X65 & ~ bnd_c4_2 X65 bnd_a67) &
% 6.98/6.59 ~ bnd_c7_2 X65 bnd_a67 |
% 6.98/6.59 bnd_c6_1 X65) |
% 6.98/6.59 bnd_c2_1 X65)) |
% 6.98/6.59 ((bnd_ndr1_0 & bnd_c2_1 bnd_a68) &
% 6.98/6.59 (ALL X66.
% 6.98/6.59 bnd_ndr1_1 bnd_a68 -->
% 6.98/6.59 bnd_c7_2 bnd_a68 X66 |
% 6.98/6.59 bnd_c6_2 bnd_a68 X66)) &
% 6.98/6.59 bnd_c5_1 bnd_a68)) &
% 6.98/6.59 ((~ bnd_c7_0 | ~ bnd_c8_0) |
% 6.98/6.59 (ALL X67.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c3_1 X67 |
% 6.98/6.59 ((bnd_ndr1_1 X67 & ~ bnd_c1_2 X67 bnd_a69) &
% 6.98/6.59 ~ bnd_c6_2 X67 bnd_a69) &
% 6.98/6.59 bnd_c5_2 X67 bnd_a69) |
% 6.98/6.59 ((bnd_ndr1_1 X67 & ~ bnd_c6_2 X67 bnd_a70) &
% 6.98/6.59 bnd_c7_2 X67 bnd_a70) &
% 6.98/6.59 bnd_c4_2 X67 bnd_a70))) &
% 6.98/6.59 (((ALL X68.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X68 & ~ bnd_c1_2 X68 bnd_a71) &
% 6.98/6.59 ~ bnd_c3_2 X68 bnd_a71) &
% 6.98/6.59 bnd_c5_2 X68 bnd_a71 |
% 6.98/6.59 ((bnd_ndr1_1 X68 & ~ bnd_c1_2 X68 bnd_a72) &
% 6.98/6.59 bnd_c8_2 X68 bnd_a72) &
% 6.98/6.59 bnd_c7_2 X68 bnd_a72) |
% 6.98/6.59 bnd_c4_1 X68) |
% 6.98/6.59 ~ bnd_c8_0) |
% 6.98/6.59 bnd_c5_0)) &
% 6.98/6.59 ((~ bnd_c3_0 |
% 6.98/6.59 ((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X69.
% 6.98/6.59 bnd_ndr1_1 bnd_a73 -->
% 6.98/6.59 (~ bnd_c1_2 bnd_a73 X69 |
% 6.98/6.59 ~ bnd_c2_2 bnd_a73 X69) |
% 6.98/6.59 ~ bnd_c4_2 bnd_a73 X69)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a73) &
% 6.98/6.59 bnd_c5_2 bnd_a73 bnd_a74) &
% 6.98/6.59 bnd_c4_2 bnd_a73 bnd_a74) &
% 6.98/6.59 bnd_c1_1 bnd_a73) |
% 6.98/6.59 ~ bnd_c7_0)) &
% 6.98/6.59 ((bnd_c8_0 |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X70.
% 6.98/6.59 bnd_ndr1_1 bnd_a75 -->
% 6.98/6.59 (bnd_c6_2 bnd_a75 X70 |
% 6.98/6.59 ~ bnd_c2_2 bnd_a75 X70) |
% 6.98/6.59 ~ bnd_c4_2 bnd_a75 X70)) &
% 6.98/6.59 (ALL X71.
% 6.98/6.59 bnd_ndr1_1 bnd_a75 -->
% 6.98/6.59 (~ bnd_c4_2 bnd_a75 X71 |
% 6.98/6.59 ~ bnd_c6_2 bnd_a75 X71) |
% 6.98/6.59 bnd_c3_2 bnd_a75 X71)) &
% 6.98/6.59 (ALL X72.
% 6.98/6.59 bnd_ndr1_1 bnd_a75 -->
% 6.98/6.59 bnd_c8_2 bnd_a75 X72 | ~ bnd_c1_2 bnd_a75 X72)) |
% 6.98/6.59 bnd_c7_0)) &
% 6.98/6.59 ((bnd_c2_0 | bnd_c5_0) |
% 6.98/6.59 (ALL X73.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c3_1 X73 | ~ bnd_c2_1 X73) | bnd_c7_1 X73))) &
% 6.98/6.59 ((bnd_c7_0 |
% 6.98/6.59 (ALL X74.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c1_1 X74 |
% 6.98/6.59 ((bnd_ndr1_1 X74 & ~ bnd_c6_2 X74 bnd_a76) &
% 6.98/6.59 bnd_c7_2 X74 bnd_a76) &
% 6.98/6.59 bnd_c4_2 X74 bnd_a76) |
% 6.98/6.59 (ALL X75.
% 6.98/6.59 bnd_ndr1_1 X74 -->
% 6.98/6.59 (bnd_c8_2 X74 X75 | bnd_c7_2 X74 X75) |
% 6.98/6.59 ~ bnd_c3_2 X74 X75))) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 (bnd_c8_0 |
% 6.98/6.59 (ALL X76.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c3_1 X76 | bnd_c7_1 X76) |
% 6.98/6.59 (ALL X77.
% 6.98/6.59 bnd_ndr1_1 X76 -->
% 6.98/6.59 (~ bnd_c3_2 X76 X77 | bnd_c7_2 X76 X77) |
% 6.98/6.59 bnd_c1_2 X76 X77)))) &
% 6.98/6.59 (((bnd_ndr1_0 & bnd_c7_1 bnd_a77) &
% 6.98/6.59 (ALL X78.
% 6.98/6.59 bnd_ndr1_1 bnd_a77 -->
% 6.98/6.59 (bnd_c1_2 bnd_a77 X78 | bnd_c7_2 bnd_a77 X78) |
% 6.98/6.59 bnd_c8_2 bnd_a77 X78) |
% 6.98/6.59 ~ bnd_c1_0) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 ((ALL X79. bnd_ndr1_0 --> bnd_c7_1 X79 | ~ bnd_c8_1 X79) |
% 6.98/6.59 bnd_c3_0)) &
% 6.98/6.59 (~ bnd_c3_0 |
% 6.98/6.59 ((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X80.
% 6.98/6.59 bnd_ndr1_1 bnd_a78 -->
% 6.98/6.59 (bnd_c3_2 bnd_a78 X80 | ~ bnd_c7_2 bnd_a78 X80) |
% 6.98/6.59 bnd_c5_2 bnd_a78 X80)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a78) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a78 bnd_a79) &
% 6.98/6.59 bnd_c6_2 bnd_a78 bnd_a79) &
% 6.98/6.59 ~ bnd_c1_1 bnd_a78)) &
% 6.98/6.59 ((bnd_c7_0 | bnd_c6_0) |
% 6.98/6.59 (bnd_ndr1_0 & ~ bnd_c4_1 bnd_a80) & ~ bnd_c2_1 bnd_a80)) &
% 6.98/6.59 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a81) &
% 6.98/6.59 bnd_c4_2 bnd_a81 bnd_a82) &
% 6.98/6.59 bnd_c8_2 bnd_a81 bnd_a82) &
% 6.98/6.59 bnd_c3_2 bnd_a81 bnd_a82) &
% 6.98/6.59 ~ bnd_c6_1 bnd_a81) &
% 6.98/6.59 bnd_c7_1 bnd_a81 |
% 6.98/6.59 ~ bnd_c1_0)) &
% 6.98/6.59 ((bnd_c1_0 |
% 6.98/6.59 (((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a83) & bnd_ndr1_1 bnd_a83) &
% 6.98/6.59 bnd_c5_2 bnd_a83 bnd_a84) &
% 6.98/6.59 ~ bnd_c2_2 bnd_a83 bnd_a84) &
% 6.98/6.59 bnd_c3_2 bnd_a83 bnd_a84) &
% 6.98/6.59 ~ bnd_c7_1 bnd_a83) |
% 6.98/6.59 (((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a85) & bnd_ndr1_1 bnd_a85) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a85 bnd_a86) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a85 bnd_a86) &
% 6.98/6.59 bnd_c7_2 bnd_a85 bnd_a86) &
% 6.98/6.59 bnd_c7_1 bnd_a85)) &
% 6.98/6.59 (((ALL X81.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c7_1 X81 |
% 6.98/6.59 (ALL X82.
% 6.98/6.59 bnd_ndr1_1 X81 -->
% 6.98/6.59 (~ bnd_c4_2 X81 X82 | bnd_c8_2 X81 X82) |
% 6.98/6.59 bnd_c7_2 X81 X82)) |
% 6.98/6.59 ~ bnd_c5_1 X81) |
% 6.98/6.59 (ALL X83.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X83 & bnd_c8_2 X83 bnd_a87) &
% 6.98/6.59 bnd_c5_2 X83 bnd_a87) &
% 6.98/6.59 bnd_c1_2 X83 bnd_a87 |
% 6.98/6.59 ~ bnd_c7_1 X83) |
% 6.98/6.59 (bnd_ndr1_1 X83 & ~ bnd_c7_2 X83 bnd_a88) &
% 6.98/6.59 bnd_c1_2 X83 bnd_a88)) |
% 6.98/6.59 (ALL X84.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c2_1 X84 | bnd_c3_1 X84) |
% 6.98/6.59 (ALL X85.
% 6.98/6.59 bnd_ndr1_1 X84 -->
% 6.98/6.59 (bnd_c4_2 X84 X85 | bnd_c1_2 X84 X85) |
% 6.98/6.59 ~ bnd_c6_2 X84 X85)))) &
% 6.98/6.59 bnd_c6_0) &
% 6.98/6.59 bnd_c4_0) &
% 6.98/6.59 (((ALL X86.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 bnd_c5_1 X86 |
% 6.98/6.59 ((bnd_ndr1_1 X86 & bnd_c2_2 X86 bnd_a89) &
% 6.98/6.59 ~ bnd_c7_2 X86 bnd_a89) &
% 6.98/6.59 bnd_c1_2 X86 bnd_a89) |
% 6.98/6.59 (((((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X87.
% 6.98/6.59 bnd_ndr1_1 bnd_a90 -->
% 6.98/6.59 (~ bnd_c1_2 bnd_a90 X87 | ~ bnd_c2_2 bnd_a90 X87) |
% 6.98/6.59 ~ bnd_c6_2 bnd_a90 X87)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a90) &
% 6.98/6.59 bnd_c1_2 bnd_a90 bnd_a91) &
% 6.98/6.59 bnd_c3_2 bnd_a90 bnd_a91) &
% 6.98/6.59 bnd_ndr1_1 bnd_a90) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a90 bnd_a92) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a90 bnd_a92) &
% 6.98/6.59 bnd_c7_2 bnd_a90 bnd_a92) |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X88.
% 6.98/6.59 bnd_ndr1_1 bnd_a93 -->
% 6.98/6.59 (bnd_c5_2 bnd_a93 X88 | ~ bnd_c6_2 bnd_a93 X88) |
% 6.98/6.59 bnd_c8_2 bnd_a93 X88)) &
% 6.98/6.59 (ALL X89.
% 6.98/6.59 bnd_ndr1_1 bnd_a93 -->
% 6.98/6.59 ~ bnd_c4_2 bnd_a93 X89 | bnd_c6_2 bnd_a93 X89)) &
% 6.98/6.59 (ALL X90.
% 6.98/6.59 bnd_ndr1_1 bnd_a93 -->
% 6.98/6.59 ~ bnd_c6_2 bnd_a93 X90 | ~ bnd_c7_2 bnd_a93 X90))) &
% 6.98/6.59 ((bnd_c5_0 |
% 6.98/6.59 (ALL X91.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c5_1 X91 | bnd_c4_1 X91) | bnd_c1_1 X91)) |
% 6.98/6.59 (ALL X92.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c2_1 X92 |
% 6.98/6.59 ((bnd_ndr1_1 X92 & ~ bnd_c5_2 X92 bnd_a94) &
% 6.98/6.59 bnd_c6_2 X92 bnd_a94) &
% 6.98/6.59 bnd_c2_2 X92 bnd_a94) |
% 6.98/6.59 ((bnd_ndr1_1 X92 & bnd_c5_2 X92 bnd_a95) &
% 6.98/6.59 bnd_c1_2 X92 bnd_a95) &
% 6.98/6.59 bnd_c6_2 X92 bnd_a95))) &
% 6.98/6.59 (((ALL X93.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X94.
% 6.98/6.59 bnd_ndr1_1 X93 -->
% 6.98/6.59 (bnd_c4_2 X93 X94 | ~ bnd_c1_2 X93 X94) |
% 6.98/6.59 bnd_c2_2 X93 X94) |
% 6.98/6.59 bnd_c6_1 X93) |
% 6.98/6.59 bnd_c1_1 X93) |
% 6.98/6.59 bnd_c3_0) |
% 6.98/6.59 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a96) & bnd_c3_1 bnd_a96) &
% 6.98/6.59 bnd_ndr1_1 bnd_a96) &
% 6.98/6.59 bnd_c7_2 bnd_a96 bnd_a97) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a96 bnd_a97) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a96 bnd_a97)) &
% 6.98/6.59 ((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a98) & ~ bnd_c5_1 bnd_a98) &
% 6.98/6.59 (ALL X95.
% 6.98/6.59 bnd_ndr1_1 bnd_a98 -->
% 6.98/6.59 (bnd_c5_2 bnd_a98 X95 | bnd_c4_2 bnd_a98 X95) |
% 6.98/6.59 bnd_c8_2 bnd_a98 X95) |
% 6.98/6.59 ~ bnd_c3_0) |
% 6.98/6.59 ~ bnd_c8_0)) &
% 6.98/6.59 (((ALL X96.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (ALL X97.
% 6.98/6.59 bnd_ndr1_1 X96 -->
% 6.98/6.59 (~ bnd_c2_2 X96 X97 | ~ bnd_c1_2 X96 X97) |
% 6.98/6.59 bnd_c6_2 X96 X97) |
% 6.98/6.59 ((bnd_ndr1_1 X96 & ~ bnd_c6_2 X96 bnd_a99) &
% 6.98/6.59 ~ bnd_c5_2 X96 bnd_a99) &
% 6.98/6.59 bnd_c4_2 X96 bnd_a99) |
% 6.98/6.59 (ALL X98.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X98 | ~ bnd_c2_1 X98) |
% 6.98/6.59 (ALL X99.
% 6.98/6.59 bnd_ndr1_1 X98 -->
% 6.98/6.59 (~ bnd_c1_2 X98 X99 | bnd_c3_2 X98 X99) |
% 6.98/6.59 ~ bnd_c5_2 X98 X99))) |
% 6.98/6.59 ~ bnd_c8_0)) &
% 6.98/6.59 ((~ bnd_c1_0 |
% 6.98/6.59 (ALL X100.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X101.
% 6.98/6.59 bnd_ndr1_1 X100 -->
% 6.98/6.59 (bnd_c6_2 X100 X101 | ~ bnd_c3_2 X100 X101) |
% 6.98/6.59 bnd_c2_2 X100 X101) |
% 6.98/6.59 (ALL X102.
% 6.98/6.59 bnd_ndr1_1 X100 -->
% 6.98/6.59 (bnd_c7_2 X100 X102 | ~ bnd_c5_2 X100 X102) |
% 6.98/6.59 ~ bnd_c8_2 X100 X102)) |
% 6.98/6.59 bnd_c7_1 X100)) |
% 6.98/6.59 (ALL X103.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c3_1 X103 | ~ bnd_c1_1 X103) | bnd_c4_1 X103))) &
% 6.98/6.59 (((ALL X104.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X104 & bnd_c4_2 X104 bnd_a100) &
% 6.98/6.59 bnd_c5_2 X104 bnd_a100) &
% 6.98/6.59 bnd_c2_2 X104 bnd_a100 |
% 6.98/6.59 bnd_c8_1 X104) |
% 6.98/6.59 (ALL X105.
% 6.98/6.59 bnd_ndr1_1 X104 -->
% 6.98/6.59 (bnd_c7_2 X104 X105 | ~ bnd_c2_2 X104 X105) |
% 6.98/6.59 bnd_c4_2 X104 X105)) |
% 6.98/6.59 ~ bnd_c5_0) |
% 6.98/6.59 (ALL X106.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X107.
% 6.98/6.59 bnd_ndr1_1 X106 --> bnd_c2_2 X106 X107 | bnd_c4_2 X106 X107) |
% 6.98/6.59 ((bnd_ndr1_1 X106 & bnd_c7_2 X106 bnd_a101) &
% 6.98/6.59 ~ bnd_c2_2 X106 bnd_a101) &
% 6.98/6.59 bnd_c4_2 X106 bnd_a101) |
% 6.98/6.59 ((bnd_ndr1_1 X106 & bnd_c7_2 X106 bnd_a102) &
% 6.98/6.59 ~ bnd_c1_2 X106 bnd_a102) &
% 6.98/6.59 ~ bnd_c4_2 X106 bnd_a102))) &
% 6.98/6.59 (~ bnd_c1_0 | ~ bnd_c2_0)) &
% 6.98/6.59 ((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X108.
% 6.98/6.59 bnd_ndr1_1 bnd_a103 -->
% 6.98/6.59 (bnd_c5_2 bnd_a103 X108 | bnd_c4_2 bnd_a103 X108) |
% 6.98/6.59 bnd_c1_2 bnd_a103 X108)) &
% 6.98/6.59 bnd_c3_1 bnd_a103) &
% 6.98/6.59 (ALL X109.
% 6.98/6.59 bnd_ndr1_1 bnd_a103 -->
% 6.98/6.59 (~ bnd_c4_2 bnd_a103 X109 | bnd_c8_2 bnd_a103 X109) |
% 6.98/6.59 ~ bnd_c5_2 bnd_a103 X109) |
% 6.98/6.59 bnd_c5_0) |
% 6.98/6.59 ~ bnd_c8_0)) &
% 6.98/6.59 ((~ bnd_c7_0 | bnd_c8_0) |
% 6.98/6.59 (ALL X110.
% 6.98/6.59 bnd_ndr1_0 --> (~ bnd_c8_1 X110 | bnd_c6_1 X110) | bnd_c4_1 X110))) &
% 6.98/6.59 (((ALL X111.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X112.
% 6.98/6.59 bnd_ndr1_1 X111 -->
% 6.98/6.59 (bnd_c6_2 X111 X112 | bnd_c5_2 X111 X112) | ~ bnd_c2_2 X111 X112) |
% 6.98/6.59 ~ bnd_c2_1 X111) |
% 6.98/6.59 ~ bnd_c6_1 X111) |
% 6.98/6.59 bnd_c5_0) |
% 6.98/6.59 (bnd_ndr1_0 & ~ bnd_c5_1 bnd_a104) &
% 6.98/6.59 (ALL X113.
% 6.98/6.59 bnd_ndr1_1 bnd_a104 -->
% 6.98/6.59 ~ bnd_c1_2 bnd_a104 X113 | bnd_c8_2 bnd_a104 X113))) &
% 6.98/6.59 (~ bnd_c2_0 |
% 6.98/6.59 ((((((((bnd_ndr1_0 &
% 6.98/6.59 bnd_ndr1_1 bnd_a105) &
% 6.98/6.59 bnd_c1_2 bnd_a105 bnd_a106) &
% 6.98/6.59 bnd_c7_2 bnd_a105 bnd_a106) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a105 bnd_a106) &
% 6.98/6.59 bnd_ndr1_1 bnd_a105) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a105 bnd_a107) &
% 6.98/6.59 bnd_c4_2 bnd_a105 bnd_a107) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a105 bnd_a107) &
% 6.98/6.59 bnd_c3_1 bnd_a105)) &
% 6.98/6.59 ((ALL X114.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X114 |
% 6.98/6.59 (ALL X115.
% 6.98/6.59 bnd_ndr1_1 X114 --> ~ bnd_c5_2 X114 X115 | ~ bnd_c8_2 X114 X115)) |
% 6.98/6.59 ((bnd_ndr1_1 X114 & bnd_c6_2 X114 bnd_a108) & ~ bnd_c5_2 X114 bnd_a108) &
% 6.98/6.59 ~ bnd_c7_2 X114 bnd_a108) |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 (((ALL X116.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X116 |
% 6.98/6.59 ((bnd_ndr1_1 X116 & bnd_c7_2 X116 bnd_a109) & bnd_c1_2 X116 bnd_a109) &
% 6.98/6.59 ~ bnd_c4_2 X116 bnd_a109) |
% 6.98/6.59 bnd_c6_1 X116) |
% 6.98/6.59 ~ bnd_c2_0) |
% 6.98/6.59 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a110) &
% 6.98/6.59 bnd_c4_2 bnd_a110 bnd_a111) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a110 bnd_a111) &
% 6.98/6.59 bnd_c1_1 bnd_a110) &
% 6.98/6.59 bnd_ndr1_1 bnd_a110) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a110 bnd_a112) &
% 6.98/6.59 bnd_c5_2 bnd_a110 bnd_a112) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a110 bnd_a112)) &
% 6.98/6.59 ((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a113) &
% 6.98/6.59 ~ bnd_c4_1 bnd_a113) &
% 6.98/6.59 (ALL X117.
% 6.98/6.59 bnd_ndr1_1 bnd_a113 -->
% 6.98/6.59 (~ bnd_c4_2 bnd_a113 X117 | bnd_c8_2 bnd_a113 X117) |
% 6.98/6.59 bnd_c7_2 bnd_a113 X117) |
% 6.98/6.59 (ALL X118.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X118 & bnd_c5_2 X118 bnd_a114) & bnd_c1_2 X118 bnd_a114) &
% 6.98/6.59 bnd_c8_2 X118 bnd_a114 |
% 6.98/6.59 bnd_c3_1 X118) |
% 6.98/6.59 ~ bnd_c7_1 X118)) |
% 6.98/6.59 ~ bnd_c1_0)) &
% 6.98/6.59 ((~ bnd_c2_0 |
% 6.98/6.59 (ALL X119.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X120.
% 6.98/6.59 bnd_ndr1_1 X119 -->
% 6.98/6.59 (bnd_c7_2 X119 X120 | bnd_c2_2 X119 X120) | ~ bnd_c1_2 X119 X120) |
% 6.98/6.59 bnd_c6_1 X119) |
% 6.98/6.59 ~ bnd_c4_1 X119)) |
% 6.98/6.59 (ALL X121.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 bnd_c1_1 X121 |
% 6.98/6.59 (ALL X122.
% 6.98/6.59 bnd_ndr1_1 X121 -->
% 6.98/6.59 (bnd_c5_2 X121 X122 | ~ bnd_c6_2 X121 X122) | ~ bnd_c7_2 X121 X122)))) &
% 6.98/6.59 ((~ bnd_c7_0 |
% 6.98/6.59 (ALL X123.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 X123 &
% 6.98/6.59 ~ bnd_c3_2 X123 bnd_a115) &
% 6.98/6.59 ~ bnd_c7_2 X123 bnd_a115) &
% 6.98/6.59 ~ bnd_c8_2 X123 bnd_a115 |
% 6.98/6.59 ~ bnd_c8_1 X123)) |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 ((ALL X124.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c4_1 X124 | bnd_c8_1 X124) |
% 6.98/6.59 ((bnd_ndr1_1 X124 &
% 6.98/6.59 bnd_c2_2 X124 bnd_a116) &
% 6.98/6.59 bnd_c1_2 X124 bnd_a116) &
% 6.98/6.59 ~ bnd_c5_2 X124 bnd_a116) |
% 6.98/6.59 (ALL X125.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X125 | bnd_c4_1 X125) |
% 6.98/6.59 (ALL X126.
% 6.98/6.59 bnd_ndr1_1 X125 -->
% 6.98/6.59 (~ bnd_c4_2 X125 X126 | bnd_c6_2 X125 X126) | bnd_c1_2 X125 X126)))) &
% 6.98/6.59 ((~ bnd_c1_0 |
% 6.98/6.59 (ALL X127.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ~ bnd_c8_1 X127 | ~ bnd_c7_1 X127)) |
% 6.98/6.59 bnd_c7_0)) &
% 6.98/6.59 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a117) &
% 6.98/6.59 bnd_c8_1 bnd_a117 |
% 6.98/6.59 bnd_c3_0)) &
% 6.98/6.59 (((((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X128.
% 6.98/6.59 bnd_ndr1_1 bnd_a118 -->
% 6.98/6.59 (bnd_c8_2 bnd_a118 X128 |
% 6.98/6.59 bnd_c1_2 bnd_a118 X128) |
% 6.98/6.59 ~ bnd_c6_2 bnd_a118 X128)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a118) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a118 bnd_a119) &
% 6.98/6.59 bnd_c2_2 bnd_a118 bnd_a119) &
% 6.98/6.59 bnd_c7_2 bnd_a118 bnd_a119) &
% 6.98/6.59 (ALL X129.
% 6.98/6.59 bnd_ndr1_1 bnd_a118 -->
% 6.98/6.59 (bnd_c2_2 bnd_a118 X129 |
% 6.98/6.59 bnd_c5_2 bnd_a118 X129) |
% 6.98/6.59 ~ bnd_c4_2 bnd_a118 X129) |
% 6.98/6.59 ~ bnd_c2_0) |
% 6.98/6.59 ~ bnd_c7_0)) &
% 6.98/6.59 (((bnd_ndr1_0 &
% 6.98/6.59 (ALL X130.
% 6.98/6.59 bnd_ndr1_1 bnd_a120 -->
% 6.98/6.59 (~ bnd_c8_2 bnd_a120 X130 |
% 6.98/6.59 bnd_c1_2 bnd_a120 X130) |
% 6.98/6.59 ~ bnd_c6_2 bnd_a120 X130)) &
% 6.98/6.59 ~ bnd_c5_1 bnd_a120) &
% 6.98/6.59 (ALL X131.
% 6.98/6.59 bnd_ndr1_1 bnd_a120 -->
% 6.98/6.59 (~ bnd_c5_2 bnd_a120 X131 |
% 6.98/6.59 ~ bnd_c1_2 bnd_a120 X131) |
% 6.98/6.59 ~ bnd_c7_2 bnd_a120 X131) |
% 6.98/6.59 ((bnd_ndr1_0 &
% 6.98/6.59 (ALL X132.
% 6.98/6.59 bnd_ndr1_1 bnd_a121 -->
% 6.98/6.59 (bnd_c8_2 bnd_a121 X132 |
% 6.98/6.59 ~ bnd_c7_2 bnd_a121 X132) |
% 6.98/6.59 bnd_c5_2 bnd_a121 X132)) &
% 6.98/6.59 bnd_c5_1 bnd_a121) &
% 6.98/6.59 bnd_c3_1 bnd_a121)) &
% 6.98/6.59 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a122) &
% 6.98/6.59 bnd_c5_2 bnd_a122 bnd_a123) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a122 bnd_a123) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a122 bnd_a123) &
% 6.98/6.59 bnd_c8_1 bnd_a122) &
% 6.98/6.59 ~ bnd_c1_1 bnd_a122 |
% 6.98/6.59 bnd_c2_0)) &
% 6.98/6.59 (((((((((bnd_ndr1_0 & bnd_c4_1 bnd_a124) &
% 6.98/6.59 bnd_ndr1_1 bnd_a124) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a124 bnd_a125) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a124 bnd_a125) &
% 6.98/6.59 bnd_c6_2 bnd_a124 bnd_a125) &
% 6.98/6.59 bnd_ndr1_1 bnd_a124) &
% 6.98/6.59 bnd_c8_2 bnd_a124 bnd_a126) &
% 6.98/6.59 bnd_c6_2 bnd_a124 bnd_a126 |
% 6.98/6.59 ~ bnd_c3_0) |
% 6.98/6.59 (ALL X133.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c7_1 X133 | ~ bnd_c6_1 X133) |
% 6.98/6.59 (ALL X134.
% 6.98/6.59 bnd_ndr1_1 X133 -->
% 6.98/6.59 (bnd_c6_2 X133 X134 | bnd_c8_2 X133 X134) |
% 6.98/6.59 ~ bnd_c2_2 X133 X134)))) &
% 6.98/6.59 (((ALL X135.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((ALL X136.
% 6.98/6.59 bnd_ndr1_1 X135 -->
% 6.98/6.59 (bnd_c4_2 X135 X136 |
% 6.98/6.59 ~ bnd_c8_2 X135 X136) |
% 6.98/6.59 bnd_c3_2 X135 X136) |
% 6.98/6.59 ~ bnd_c4_1 X135) |
% 6.98/6.59 (ALL X137.
% 6.98/6.59 bnd_ndr1_1 X135 -->
% 6.98/6.59 (~ bnd_c7_2 X135 X137 |
% 6.98/6.59 bnd_c8_2 X135 X137) |
% 6.98/6.59 bnd_c6_2 X135 X137)) |
% 6.98/6.59 ((bnd_ndr1_0 & bnd_c8_1 bnd_a127) &
% 6.98/6.59 bnd_c3_1 bnd_a127) &
% 6.98/6.59 ~ bnd_c5_1 bnd_a127) |
% 6.98/6.59 ~ bnd_c7_0)) &
% 6.98/6.59 ((~ bnd_c1_0 |
% 6.98/6.59 (ALL X138.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 X138 & ~ bnd_c7_2 X138 bnd_a128) &
% 6.98/6.59 ~ bnd_c8_2 X138 bnd_a128) &
% 6.98/6.59 ~ bnd_c4_2 X138 bnd_a128 |
% 6.98/6.59 ~ bnd_c1_1 X138)) |
% 6.98/6.59 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a129) &
% 6.98/6.59 ~ bnd_c6_2 bnd_a129 bnd_a130) &
% 6.98/6.59 ~ bnd_c8_2 bnd_a129 bnd_a130) &
% 6.98/6.59 bnd_c3_2 bnd_a129 bnd_a130) &
% 6.98/6.59 bnd_ndr1_1 bnd_a129) &
% 6.98/6.59 bnd_c1_2 bnd_a129 bnd_a131) &
% 6.98/6.59 ~ bnd_c7_2 bnd_a129 bnd_a131) &
% 6.98/6.59 bnd_c8_2 bnd_a129 bnd_a131) &
% 6.98/6.59 ~ bnd_c6_1 bnd_a129)) &
% 6.98/6.59 (((ALL X139.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_c8_1 X139 | bnd_c2_1 X139) |
% 6.98/6.59 ~ bnd_c7_1 X139) |
% 6.98/6.59 (ALL X140.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c1_1 X140 | ~ bnd_c8_1 X140) |
% 6.98/6.59 (ALL X141.
% 6.98/6.59 bnd_ndr1_1 X140 -->
% 6.98/6.59 (bnd_c7_2 X140 X141 | ~ bnd_c2_2 X140 X141) |
% 6.98/6.59 bnd_c3_2 X140 X141))) |
% 6.98/6.59 (ALL X142.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c4_1 X142 | ~ bnd_c6_1 X142) |
% 6.98/6.59 ~ bnd_c5_1 X142))) &
% 6.98/6.59 ((ALL X143.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (((bnd_ndr1_1 X143 & ~ bnd_c3_2 X143 bnd_a132) &
% 6.98/6.59 ~ bnd_c8_2 X143 bnd_a132) &
% 6.98/6.59 ~ bnd_c6_2 X143 bnd_a132 |
% 6.98/6.59 ~ bnd_c1_1 X143) |
% 6.98/6.59 (ALL X144.
% 6.98/6.59 bnd_ndr1_1 X143 -->
% 6.98/6.59 (~ bnd_c4_2 X143 X144 | bnd_c7_2 X143 X144) |
% 6.98/6.59 ~ bnd_c8_2 X143 X144)) |
% 6.98/6.59 ~ bnd_c8_0)) &
% 6.98/6.59 ((ALL X145.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c6_1 X145 | ~ bnd_c2_1 X145) |
% 6.98/6.59 ((bnd_ndr1_1 X145 & ~ bnd_c1_2 X145 bnd_a133) &
% 6.98/6.59 ~ bnd_c5_2 X145 bnd_a133) &
% 6.98/6.59 bnd_c3_2 X145 bnd_a133) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 ((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a134) &
% 6.98/6.59 bnd_ndr1_1 bnd_a134) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a134 bnd_a135) &
% 6.98/6.59 bnd_c8_2 bnd_a134 bnd_a135) &
% 6.98/6.59 bnd_c3_2 bnd_a134 bnd_a135) &
% 6.98/6.59 (ALL X146.
% 6.98/6.59 bnd_ndr1_1 bnd_a134 -->
% 6.98/6.59 bnd_c1_2 bnd_a134 X146 | bnd_c8_2 bnd_a134 X146) |
% 6.98/6.59 (ALL X147.
% 6.98/6.59 bnd_ndr1_0 --> bnd_c8_1 X147 | ~ bnd_c2_1 X147))) &
% 6.98/6.59 bnd_ndr1_0) &
% 6.98/6.59 bnd_c5_1 bnd_a136) &
% 6.98/6.59 (ALL X148.
% 6.98/6.59 bnd_ndr1_1 bnd_a136 -->
% 6.98/6.59 (bnd_c8_2 bnd_a136 X148 | bnd_c3_2 bnd_a136 X148) |
% 6.98/6.59 bnd_c7_2 bnd_a136 X148)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a136) &
% 6.98/6.59 bnd_c1_2 bnd_a136 bnd_a137) &
% 6.98/6.59 bnd_c3_2 bnd_a136 bnd_a137) &
% 6.98/6.59 bnd_c5_2 bnd_a136 bnd_a137) &
% 6.98/6.59 ((~ bnd_c3_0 |
% 6.98/6.59 (((((((bnd_ndr1_0 &
% 6.98/6.59 (ALL X149.
% 6.98/6.59 bnd_ndr1_1 bnd_a138 -->
% 6.98/6.59 (bnd_c3_2 bnd_a138 X149 | ~ bnd_c4_2 bnd_a138 X149) |
% 6.98/6.59 ~ bnd_c6_2 bnd_a138 X149)) &
% 6.98/6.59 bnd_ndr1_1 bnd_a138) &
% 6.98/6.59 bnd_c6_2 bnd_a138 bnd_a139) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a138 bnd_a139) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a138 bnd_a139) &
% 6.98/6.59 bnd_ndr1_1 bnd_a138) &
% 6.98/6.59 bnd_c5_2 bnd_a138 bnd_a140) &
% 6.98/6.59 ~ bnd_c4_2 bnd_a138 bnd_a140) |
% 6.98/6.59 bnd_c7_0)) &
% 6.98/6.59 ((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a141) & bnd_c8_1 bnd_a141) &
% 6.98/6.59 bnd_ndr1_1 bnd_a141) &
% 6.98/6.59 ~ bnd_c3_2 bnd_a141 bnd_a142) &
% 6.98/6.59 bnd_c8_2 bnd_a141 bnd_a142 |
% 6.98/6.59 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a143) & bnd_ndr1_1 bnd_a143) &
% 6.98/6.59 ~ bnd_c1_2 bnd_a143 bnd_a144) &
% 6.98/6.59 ~ bnd_c5_2 bnd_a143 bnd_a144) &
% 6.98/6.59 bnd_c2_2 bnd_a143 bnd_a144) |
% 6.98/6.59 ~ bnd_c2_0)) &
% 6.98/6.59 (bnd_c7_0 |
% 6.98/6.59 (ALL X150.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 ((bnd_ndr1_1 X150 & ~ bnd_c4_2 X150 bnd_a145) &
% 6.98/6.59 bnd_c6_2 X150 bnd_a145) &
% 6.98/6.59 bnd_c5_2 X150 bnd_a145))) &
% 6.98/6.59 ((~ bnd_c2_0 | ~ bnd_c1_0) |
% 6.98/6.59 (ALL X151.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (bnd_ndr1_1 X151 & ~ bnd_c2_2 X151 bnd_a146 | bnd_c2_1 X151) |
% 6.98/6.59 (ALL X152.
% 6.98/6.59 bnd_ndr1_1 X151 -->
% 6.98/6.59 (bnd_c5_2 X151 X152 | ~ bnd_c1_2 X151 X152) |
% 6.98/6.59 bnd_c8_2 X151 X152)))) &
% 6.98/6.59 ~ bnd_c2_0) &
% 6.98/6.59 (bnd_c7_0 |
% 6.98/6.59 (ALL X153.
% 6.98/6.59 bnd_ndr1_0 -->
% 6.98/6.59 (~ bnd_c3_1 X153 | bnd_c1_1 X153) |
% 6.98/6.59 (ALL X154.
% 6.98/6.59 bnd_ndr1_1 X153 -->
% 6.98/6.59 (bnd_c2_2 X153 X154 | ~ bnd_c8_2 X153 X154) |
% 6.98/6.59 bnd_c6_2 X153 X154)))) &
% 6.98/6.59 ~ bnd_c3_0)
% 15.38/14.99 Unfolded term: ~ (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c7_1 U | ~ bnd_c5_1 U) | bnd_c2_1 U) |
% 15.38/14.99 (ALL V.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 V & ~ bnd_c4_2 V bnd_a1) &
% 15.38/14.99 ~ bnd_c1_2 V bnd_a1 |
% 15.38/14.99 ((bnd_ndr1_1 V & ~ bnd_c1_2 V bnd_a2) &
% 15.38/14.99 bnd_c7_2 V bnd_a2) &
% 15.38/14.99 bnd_c4_2 V bnd_a2) |
% 15.38/14.99 (bnd_ndr1_1 V & ~ bnd_c7_2 V bnd_a3) &
% 15.38/14.99 bnd_c6_2 V bnd_a3)) |
% 15.38/14.99 ~ bnd_c5_0) &
% 15.38/14.99 (((ALL W.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c1_1 W |
% 15.38/14.99 ((bnd_ndr1_1 W & ~ bnd_c4_2 W bnd_a4) &
% 15.38/14.99 ~ bnd_c3_2 W bnd_a4) &
% 15.38/14.99 ~ bnd_c7_2 W bnd_a4) |
% 15.38/14.99 ((bnd_ndr1_1 W & ~ bnd_c4_2 W bnd_a5) &
% 15.38/14.99 bnd_c3_2 W bnd_a5) &
% 15.38/14.99 ~ bnd_c5_2 W bnd_a5) |
% 15.38/14.99 (ALL X.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL Y.
% 15.38/14.99 bnd_ndr1_1 X -->
% 15.38/14.99 (~ bnd_c2_2 X Y | ~ bnd_c4_2 X Y) |
% 15.38/14.99 ~ bnd_c5_2 X Y) |
% 15.38/14.99 ~ bnd_c1_1 X) |
% 15.38/14.99 bnd_c2_1 X)) |
% 15.38/14.99 ~ bnd_c8_0)) &
% 15.38/14.99 ((bnd_c5_0 |
% 15.38/14.99 (ALL Z.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 Z & bnd_c2_2 Z bnd_a6) &
% 15.38/14.99 ~ bnd_c7_2 Z bnd_a6) &
% 15.38/14.99 bnd_c8_2 Z bnd_a6 |
% 15.38/14.99 ~ bnd_c2_1 Z) |
% 15.38/14.99 ~ bnd_c3_1 Z)) |
% 15.38/14.99 (ALL X1.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X1 & bnd_c1_2 X1 bnd_a7) &
% 15.38/14.99 bnd_c6_2 X1 bnd_a7) &
% 15.38/14.99 bnd_c3_2 X1 bnd_a7 |
% 15.38/14.99 ~ bnd_c8_1 X1) |
% 15.38/14.99 (ALL X2.
% 15.38/14.99 bnd_ndr1_1 X1 -->
% 15.38/14.99 (~ bnd_c2_2 X1 X2 | bnd_c4_2 X1 X2) |
% 15.38/14.99 bnd_c3_2 X1 X2)))) &
% 15.38/14.99 ((~ bnd_c2_0 |
% 15.38/14.99 (ALL X3.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ~ bnd_c5_1 X3 |
% 15.38/14.99 (bnd_ndr1_1 X3 & ~ bnd_c4_2 X3 bnd_a8) &
% 15.38/14.99 bnd_c2_2 X3 bnd_a8)) |
% 15.38/14.99 ((bnd_ndr1_0 & bnd_c4_1 bnd_a9) &
% 15.38/14.99 (ALL X4.
% 15.38/14.99 bnd_ndr1_1 bnd_a9 -->
% 15.38/14.99 (~ bnd_c1_2 bnd_a9 X4 | ~ bnd_c5_2 bnd_a9 X4) |
% 15.38/14.99 ~ bnd_c4_2 bnd_a9 X4)) &
% 15.38/14.99 bnd_c3_1 bnd_a9)) &
% 15.38/14.99 (((ALL X5.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X6.
% 15.38/14.99 bnd_ndr1_1 X5 -->
% 15.38/14.99 ~ bnd_c8_2 X5 X6 | bnd_c7_2 X5 X6) |
% 15.38/14.99 bnd_c7_1 X5) |
% 15.38/14.99 (ALL X7.
% 15.38/14.99 bnd_ndr1_1 X5 -->
% 15.38/14.99 (~ bnd_c8_2 X5 X7 | ~ bnd_c2_2 X5 X7) |
% 15.38/14.99 ~ bnd_c4_2 X5 X7)) |
% 15.38/14.99 bnd_c1_0) |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 (((ALL X8.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c4_1 X8 |
% 15.38/14.99 (ALL X9.
% 15.38/14.99 bnd_ndr1_1 X8 -->
% 15.38/14.99 bnd_c6_2 X8 X9 | ~ bnd_c2_2 X8 X9)) |
% 15.38/14.99 ~ bnd_c5_1 X8) |
% 15.38/14.99 ~ bnd_c8_0) |
% 15.38/14.99 ~ bnd_c4_0)) &
% 15.38/14.99 (((ALL X10.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X10 & ~ bnd_c5_2 X10 bnd_a10) &
% 15.38/14.99 bnd_c7_2 X10 bnd_a10) &
% 15.38/14.99 ~ bnd_c6_2 X10 bnd_a10 |
% 15.38/14.99 (ALL X11.
% 15.38/14.99 bnd_ndr1_1 X10 -->
% 15.38/14.99 (bnd_c3_2 X10 X11 | bnd_c2_2 X10 X11) |
% 15.38/14.99 ~ bnd_c1_2 X10 X11)) |
% 15.38/14.99 ~ bnd_c1_1 X10) |
% 15.38/14.99 ((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a11) &
% 15.38/14.99 bnd_ndr1_1 bnd_a11) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a11 bnd_a12) &
% 15.38/14.99 bnd_c5_2 bnd_a11 bnd_a12) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a11 bnd_a12) |
% 15.38/14.99 bnd_c7_0)) &
% 15.38/14.99 (((ALL X12.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X13.
% 15.38/14.99 bnd_ndr1_1 X12 -->
% 15.38/14.99 bnd_c5_2 X12 X13 | bnd_c1_2 X12 X13) |
% 15.38/14.99 ~ bnd_c1_1 X12) |
% 15.38/14.99 ((bnd_ndr1_1 X12 & ~ bnd_c2_2 X12 bnd_a13) &
% 15.38/14.99 ~ bnd_c8_2 X12 bnd_a13) &
% 15.38/14.99 bnd_c6_2 X12 bnd_a13) |
% 15.38/14.99 (((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a14) &
% 15.38/14.99 bnd_ndr1_1 bnd_a14) &
% 15.38/14.99 bnd_c6_2 bnd_a14 bnd_a15) &
% 15.38/14.99 bnd_c3_2 bnd_a14 bnd_a15) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a14 bnd_a15) &
% 15.38/14.99 ~ bnd_c7_1 bnd_a14) |
% 15.38/14.99 ~ bnd_c3_0)) &
% 15.38/14.99 ((bnd_c2_0 | ~ bnd_c8_0) |
% 15.38/14.99 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a16) & ~ bnd_c8_1 bnd_a16) &
% 15.38/14.99 bnd_c1_1 bnd_a16)) &
% 15.38/14.99 ((bnd_c7_0 | bnd_c2_0) |
% 15.38/14.99 (ALL X14.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X14 & ~ bnd_c6_2 X14 bnd_a17) &
% 15.38/14.99 bnd_c5_2 X14 bnd_a17) &
% 15.38/14.99 bnd_c3_2 X14 bnd_a17 |
% 15.38/14.99 bnd_c8_1 X14) |
% 15.38/14.99 ~ bnd_c5_1 X14))) &
% 15.38/14.99 ((~ bnd_c5_0 |
% 15.38/14.99 (ALL X15.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c1_1 X15 |
% 15.38/14.99 (ALL X16.
% 15.38/14.99 bnd_ndr1_1 X15 -->
% 15.38/14.99 bnd_c7_2 X15 X16 | ~ bnd_c2_2 X15 X16)) |
% 15.38/14.99 (ALL X17.
% 15.38/14.99 bnd_ndr1_1 X15 -->
% 15.38/14.99 (bnd_c5_2 X15 X17 | ~ bnd_c2_2 X15 X17) |
% 15.38/14.99 bnd_c8_2 X15 X17))) |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 ((~ bnd_c6_0 |
% 15.38/14.99 (ALL X18.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X19.
% 15.38/14.99 bnd_ndr1_1 X18 -->
% 15.38/14.99 (~ bnd_c1_2 X18 X19 | ~ bnd_c7_2 X18 X19) |
% 15.38/14.99 bnd_c2_2 X18 X19) |
% 15.38/14.99 bnd_c2_1 X18) |
% 15.38/14.99 bnd_c3_1 X18)) |
% 15.38/14.99 (bnd_ndr1_0 & bnd_c6_1 bnd_a18) & bnd_c1_1 bnd_a18)) &
% 15.38/14.99 ((~ bnd_c1_0 |
% 15.38/14.99 ((((((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X20.
% 15.38/14.99 bnd_ndr1_1 bnd_a19 -->
% 15.38/14.99 (bnd_c6_2 bnd_a19 X20 | bnd_c8_2 bnd_a19 X20) |
% 15.38/14.99 bnd_c3_2 bnd_a19 X20)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a19) &
% 15.38/14.99 bnd_c4_2 bnd_a19 bnd_a20) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a19 bnd_a20) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a19 bnd_a20) &
% 15.38/14.99 bnd_ndr1_1 bnd_a19) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a19 bnd_a21) &
% 15.38/14.99 bnd_c3_2 bnd_a19 bnd_a21) &
% 15.38/14.99 bnd_c7_2 bnd_a19 bnd_a21) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 (((ALL X21.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 X21 & ~ bnd_c7_2 X21 bnd_a22) &
% 15.38/14.99 ~ bnd_c6_2 X21 bnd_a22 |
% 15.38/14.99 ((bnd_ndr1_1 X21 & ~ bnd_c6_2 X21 bnd_a23) &
% 15.38/14.99 ~ bnd_c3_2 X21 bnd_a23) &
% 15.38/14.99 ~ bnd_c2_2 X21 bnd_a23) |
% 15.38/14.99 (ALL X22.
% 15.38/14.99 bnd_ndr1_1 X21 -->
% 15.38/14.99 (~ bnd_c8_2 X21 X22 | bnd_c1_2 X21 X22) |
% 15.38/14.99 ~ bnd_c5_2 X21 X22)) |
% 15.38/14.99 bnd_c5_0) |
% 15.38/14.99 bnd_c8_0)) &
% 15.38/14.99 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a24) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a24 bnd_a25) &
% 15.38/14.99 bnd_c3_2 bnd_a24 bnd_a25) &
% 15.38/14.99 bnd_c1_2 bnd_a24 bnd_a25) &
% 15.38/14.99 ~ bnd_c2_1 bnd_a24) &
% 15.38/14.99 bnd_ndr1_1 bnd_a24) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a24 bnd_a26) &
% 15.38/14.99 bnd_c2_2 bnd_a24 bnd_a26) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a24 bnd_a26 |
% 15.38/14.99 (((((bnd_ndr1_0 & bnd_c8_1 bnd_a27) &
% 15.38/14.99 (ALL X23.
% 15.38/14.99 bnd_ndr1_1 bnd_a27 -->
% 15.38/14.99 (bnd_c5_2 bnd_a27 X23 | bnd_c8_2 bnd_a27 X23) |
% 15.38/14.99 ~ bnd_c7_2 bnd_a27 X23)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a27) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a27 bnd_a28) &
% 15.38/14.99 bnd_c2_2 bnd_a27 bnd_a28) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a27 bnd_a28) |
% 15.38/14.99 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a29) &
% 15.38/14.99 bnd_c7_2 bnd_a29 bnd_a30) &
% 15.38/14.99 bnd_c2_2 bnd_a29 bnd_a30) &
% 15.38/14.99 bnd_c1_2 bnd_a29 bnd_a30) &
% 15.38/14.99 bnd_ndr1_1 bnd_a29) &
% 15.38/14.99 bnd_c5_2 bnd_a29 bnd_a31) &
% 15.38/14.99 bnd_c6_2 bnd_a29 bnd_a31) &
% 15.38/14.99 (ALL X24.
% 15.38/14.99 bnd_ndr1_1 bnd_a29 -->
% 15.38/14.99 (bnd_c1_2 bnd_a29 X24 | ~ bnd_c6_2 bnd_a29 X24) |
% 15.38/14.99 bnd_c5_2 bnd_a29 X24))) &
% 15.38/14.99 ((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X25.
% 15.38/14.99 bnd_ndr1_1 bnd_a32 -->
% 15.38/14.99 bnd_c4_2 bnd_a32 X25 | bnd_c1_2 bnd_a32 X25)) &
% 15.38/14.99 (ALL X26.
% 15.38/14.99 bnd_ndr1_1 bnd_a32 -->
% 15.38/14.99 (bnd_c6_2 bnd_a32 X26 | bnd_c1_2 bnd_a32 X26) |
% 15.38/14.99 ~ bnd_c3_2 bnd_a32 X26)) &
% 15.38/14.99 bnd_c2_1 bnd_a32 |
% 15.38/14.99 (ALL X27.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c1_1 X27 |
% 15.38/14.99 ((bnd_ndr1_1 X27 & bnd_c4_2 X27 bnd_a33) &
% 15.38/14.99 bnd_c1_2 X27 bnd_a33) &
% 15.38/14.99 bnd_c3_2 X27 bnd_a33) |
% 15.38/14.99 ~ bnd_c4_1 X27)) |
% 15.38/14.99 ~ bnd_c1_0)) &
% 15.38/14.99 ((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X28. bnd_ndr1_1 bnd_a34 --> ~ bnd_c7_2 bnd_a34 X28)) &
% 15.38/14.99 (ALL X29.
% 15.38/14.99 bnd_ndr1_1 bnd_a34 -->
% 15.38/14.99 (~ bnd_c1_2 bnd_a34 X29 | bnd_c2_2 bnd_a34 X29) |
% 15.38/14.99 bnd_c7_2 bnd_a34 X29)) &
% 15.38/14.99 (ALL X30.
% 15.38/14.99 bnd_ndr1_1 bnd_a34 -->
% 15.38/14.99 (bnd_c1_2 bnd_a34 X30 | ~ bnd_c8_2 bnd_a34 X30) |
% 15.38/14.99 bnd_c4_2 bnd_a34 X30) |
% 15.38/14.99 bnd_c2_0) |
% 15.38/14.99 bnd_c3_0)) &
% 15.38/14.99 (((((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X31.
% 15.38/14.99 bnd_ndr1_1 bnd_a35 -->
% 15.38/14.99 (bnd_c8_2 bnd_a35 X31 | ~ bnd_c1_2 bnd_a35 X31) |
% 15.38/14.99 ~ bnd_c2_2 bnd_a35 X31)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a35) &
% 15.38/14.99 ~ bnd_c2_2 bnd_a35 bnd_a36) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a35 bnd_a36) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a35 bnd_a36) &
% 15.38/14.99 ~ bnd_c4_1 bnd_a35 |
% 15.38/14.99 (((((bnd_ndr1_0 & ~ bnd_c6_1 bnd_a37) & bnd_ndr1_1 bnd_a37) &
% 15.38/14.99 bnd_c5_2 bnd_a37 bnd_a38) &
% 15.38/14.99 bnd_c4_2 bnd_a37 bnd_a38) &
% 15.38/14.99 bnd_c3_2 bnd_a37 bnd_a38) &
% 15.38/14.99 ~ bnd_c1_1 bnd_a37) |
% 15.38/14.99 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a39) &
% 15.38/14.99 bnd_c5_2 bnd_a39 bnd_a40) &
% 15.38/14.99 bnd_c3_2 bnd_a39 bnd_a40) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a39 bnd_a40) &
% 15.38/14.99 (ALL X32.
% 15.38/14.99 bnd_ndr1_1 bnd_a39 -->
% 15.38/14.99 ~ bnd_c8_2 bnd_a39 X32 | bnd_c7_2 bnd_a39 X32)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a39) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a39 bnd_a41) &
% 15.38/14.99 bnd_c6_2 bnd_a39 bnd_a41) &
% 15.38/14.99 ~ bnd_c2_2 bnd_a39 bnd_a41)) &
% 15.38/14.99 ((bnd_c2_0 | bnd_c7_0) | ~ bnd_c4_0)) &
% 15.38/14.99 ((~ bnd_c8_0 |
% 15.38/14.99 (ALL X33.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X34.
% 15.38/14.99 bnd_ndr1_1 X33 -->
% 15.38/14.99 (~ bnd_c2_2 X33 X34 | bnd_c3_2 X33 X34) |
% 15.38/14.99 ~ bnd_c6_2 X33 X34) |
% 15.38/14.99 ~ bnd_c8_1 X33) |
% 15.38/14.99 bnd_c7_1 X33)) |
% 15.38/14.99 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a42) & ~ bnd_c7_2 bnd_a42 bnd_a43) &
% 15.38/14.99 bnd_c8_2 bnd_a42 bnd_a43) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a42 bnd_a43) &
% 15.38/14.99 ~ bnd_c7_1 bnd_a42) &
% 15.38/14.99 (ALL X35.
% 15.38/14.99 bnd_ndr1_1 bnd_a42 -->
% 15.38/14.99 (bnd_c1_2 bnd_a42 X35 | ~ bnd_c7_2 bnd_a42 X35) |
% 15.38/14.99 bnd_c4_2 bnd_a42 X35))) &
% 15.38/14.99 ((((((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a44) & bnd_ndr1_1 bnd_a44) &
% 15.38/14.99 bnd_c5_2 bnd_a44 bnd_a45) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a44 bnd_a45) &
% 15.38/14.99 (ALL X36.
% 15.38/14.99 bnd_ndr1_1 bnd_a44 -->
% 15.38/14.99 ~ bnd_c4_2 bnd_a44 X36 | ~ bnd_c5_2 bnd_a44 X36) |
% 15.38/14.99 (ALL X37.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X38.
% 15.38/14.99 bnd_ndr1_1 X37 -->
% 15.38/14.99 (bnd_c4_2 X37 X38 | ~ bnd_c6_2 X37 X38) | bnd_c5_2 X37 X38) |
% 15.38/14.99 (bnd_ndr1_1 X37 & ~ bnd_c8_2 X37 bnd_a46) &
% 15.38/14.99 ~ bnd_c3_2 X37 bnd_a46) |
% 15.38/14.99 ~ bnd_c7_1 X37)) |
% 15.38/14.99 (ALL X39.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c3_1 X39 |
% 15.38/14.99 (ALL X40.
% 15.38/14.99 bnd_ndr1_1 X39 -->
% 15.38/14.99 (bnd_c3_2 X39 X40 | bnd_c6_2 X39 X40) | bnd_c4_2 X39 X40)) |
% 15.38/14.99 (ALL X41.
% 15.38/14.99 bnd_ndr1_1 X39 -->
% 15.38/14.99 (bnd_c5_2 X39 X41 | bnd_c1_2 X39 X41) | bnd_c8_2 X39 X41)))) &
% 15.38/14.99 (bnd_c8_0 |
% 15.38/14.99 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a47) & ~ bnd_c2_2 bnd_a47 bnd_a48) &
% 15.38/14.99 bnd_c8_2 bnd_a47 bnd_a48) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a47 bnd_a48) &
% 15.38/14.99 ~ bnd_c6_1 bnd_a47) &
% 15.38/14.99 bnd_ndr1_1 bnd_a47) &
% 15.38/14.99 ~ bnd_c2_2 bnd_a47 bnd_a49) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a47 bnd_a49) &
% 15.38/14.99 bnd_c7_2 bnd_a47 bnd_a49)) &
% 15.38/14.99 (((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a50) & bnd_c1_1 bnd_a50 | bnd_c7_0) |
% 15.38/14.99 bnd_c4_0)) &
% 15.38/14.99 ((~ bnd_c8_0 |
% 15.38/14.99 (ALL X42.
% 15.38/14.99 bnd_ndr1_0 --> (~ bnd_c5_1 X42 | bnd_c6_1 X42) | bnd_c2_1 X42)) |
% 15.38/14.99 ~ bnd_c4_0)) &
% 15.38/14.99 ((bnd_c2_0 | bnd_c3_0) |
% 15.38/14.99 ((bnd_ndr1_0 & bnd_c5_1 bnd_a51) & ~ bnd_c7_1 bnd_a51) &
% 15.38/14.99 (ALL X43.
% 15.38/14.99 bnd_ndr1_1 bnd_a51 -->
% 15.38/14.99 (bnd_c3_2 bnd_a51 X43 | ~ bnd_c5_2 bnd_a51 X43) |
% 15.38/14.99 bnd_c4_2 bnd_a51 X43))) &
% 15.38/14.99 ((ALL X44.
% 15.38/14.99 bnd_ndr1_0 --> (~ bnd_c3_1 X44 | bnd_c2_1 X44) | ~ bnd_c7_1 X44) |
% 15.38/14.99 (ALL X45.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c1_1 X45 |
% 15.38/14.99 (ALL X46.
% 15.38/14.99 bnd_ndr1_1 X45 -->
% 15.38/14.99 (bnd_c4_2 X45 X46 | ~ bnd_c6_2 X45 X46) | ~ bnd_c3_2 X45 X46)) |
% 15.38/14.99 ~ bnd_c6_1 X45))) &
% 15.38/14.99 ((~ bnd_c7_0 | ~ bnd_c6_0) |
% 15.38/14.99 ~ bnd_c3_0)) &
% 15.38/14.99 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a52) &
% 15.38/14.99 (ALL X47.
% 15.38/14.99 bnd_ndr1_1 bnd_a52 -->
% 15.38/14.99 (~ bnd_c5_2 bnd_a52 X47 | ~ bnd_c8_2 bnd_a52 X47) |
% 15.38/14.99 ~ bnd_c7_2 bnd_a52 X47)) &
% 15.38/14.99 bnd_c8_1 bnd_a52 |
% 15.38/14.99 (((((((bnd_ndr1_0 &
% 15.38/14.99 bnd_ndr1_1 bnd_a53) &
% 15.38/14.99 bnd_c4_2 bnd_a53 bnd_a54) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a53 bnd_a54) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a53 bnd_a54) &
% 15.38/14.99 bnd_c1_1 bnd_a53) &
% 15.38/14.99 bnd_ndr1_1 bnd_a53) &
% 15.38/14.99 bnd_c2_2 bnd_a53 bnd_a55) &
% 15.38/14.99 bnd_c6_2 bnd_a53 bnd_a55) |
% 15.38/14.99 ~ bnd_c5_0)) &
% 15.38/14.99 ((bnd_c8_0 |
% 15.38/14.99 (ALL X48.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c5_1 X48 |
% 15.38/14.99 (ALL X49.
% 15.38/14.99 bnd_ndr1_1 X48 -->
% 15.38/14.99 (~ bnd_c4_2 X48 X49 | ~ bnd_c1_2 X48 X49) | ~ bnd_c6_2 X48 X49)) |
% 15.38/14.99 ((bnd_ndr1_1 X48 & bnd_c3_2 X48 bnd_a56) & ~ bnd_c2_2 X48 bnd_a56) &
% 15.38/14.99 bnd_c7_2 X48 bnd_a56)) |
% 15.38/14.99 (ALL X50.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X50 & ~ bnd_c7_2 X50 bnd_a57) & bnd_c2_2 X50 bnd_a57) &
% 15.38/14.99 bnd_c5_2 X50 bnd_a57 |
% 15.38/14.99 ~ bnd_c3_1 X50) |
% 15.38/14.99 ((bnd_ndr1_1 X50 & ~ bnd_c3_2 X50 bnd_a58) & ~ bnd_c5_2 X50 bnd_a58) &
% 15.38/14.99 bnd_c6_2 X50 bnd_a58))) &
% 15.38/14.99 ((bnd_c3_0 | bnd_c2_0) |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X51.
% 15.38/14.99 bnd_ndr1_1 bnd_a59 --> bnd_c7_2 bnd_a59 X51 | bnd_c5_2 bnd_a59 X51)) &
% 15.38/14.99 ~ bnd_c4_1 bnd_a59) &
% 15.38/14.99 bnd_c3_1 bnd_a59)) &
% 15.38/14.99 ((~ bnd_c4_0 | ~ bnd_c2_0) | bnd_c3_0)) &
% 15.38/14.99 (((ALL X52.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 bnd_c1_1 X52 | ~ bnd_c4_1 X52) |
% 15.38/14.99 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a60) &
% 15.38/14.99 ~ bnd_c2_2 bnd_a60 bnd_a61) &
% 15.38/14.99 bnd_c8_2 bnd_a60 bnd_a61) &
% 15.38/14.99 bnd_c5_2 bnd_a60 bnd_a61) &
% 15.38/14.99 (ALL X53.
% 15.38/14.99 bnd_ndr1_1 bnd_a60 -->
% 15.38/14.99 (~ bnd_c7_2 bnd_a60 X53 | bnd_c5_2 bnd_a60 X53) |
% 15.38/14.99 ~ bnd_c2_2 bnd_a60 X53)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a60) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a60 bnd_a62) &
% 15.38/14.99 bnd_c2_2 bnd_a60 bnd_a62) &
% 15.38/14.99 bnd_c3_2 bnd_a60 bnd_a62) |
% 15.38/14.99 (ALL X54.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c2_1 X54 | ~ bnd_c3_1 X54) |
% 15.38/14.99 (ALL X55.
% 15.38/14.99 bnd_ndr1_1 X54 -->
% 15.38/14.99 (~ bnd_c3_2 X54 X55 | bnd_c5_2 X54 X55) | bnd_c6_2 X54 X55)))) &
% 15.38/14.99 (((ALL X56.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c7_1 X56 | bnd_c6_1 X56) |
% 15.38/14.99 ((bnd_ndr1_1 X56 &
% 15.38/14.99 ~ bnd_c2_2 X56 bnd_a63) &
% 15.38/14.99 bnd_c4_2 X56 bnd_a63) &
% 15.38/14.99 ~ bnd_c5_2 X56 bnd_a63) |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X57.
% 15.38/14.99 bnd_ndr1_1 bnd_a64 -->
% 15.38/14.99 (bnd_c4_2 bnd_a64 X57 |
% 15.38/14.99 ~ bnd_c2_2 bnd_a64 X57) |
% 15.38/14.99 bnd_c8_2 bnd_a64 X57)) &
% 15.38/14.99 ~ bnd_c1_1 bnd_a64) &
% 15.38/14.99 (ALL X58.
% 15.38/14.99 bnd_ndr1_1 bnd_a64 -->
% 15.38/14.99 (bnd_c1_2 bnd_a64 X58 |
% 15.38/14.99 bnd_c4_2 bnd_a64 X58) |
% 15.38/14.99 bnd_c6_2 bnd_a64 X58)) |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 (((ALL X59.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X59 |
% 15.38/14.99 (ALL X60.
% 15.38/14.99 bnd_ndr1_1 X59 -->
% 15.38/14.99 (~ bnd_c7_2 X59 X60 | bnd_c5_2 X59 X60) | bnd_c8_2 X59 X60)) |
% 15.38/14.99 ~ bnd_c8_1 X59) |
% 15.38/14.99 bnd_c5_0) |
% 15.38/14.99 ~ bnd_c3_0)) &
% 15.38/14.99 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a65) &
% 15.38/14.99 (ALL X61.
% 15.38/14.99 bnd_ndr1_1 bnd_a65 -->
% 15.38/14.99 (bnd_c1_2 bnd_a65 X61 |
% 15.38/14.99 bnd_c4_2 bnd_a65 X61) |
% 15.38/14.99 bnd_c5_2 bnd_a65 X61)) &
% 15.38/14.99 bnd_c6_1 bnd_a65 |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X62.
% 15.38/14.99 bnd_ndr1_1 bnd_a66 -->
% 15.38/14.99 (bnd_c3_2 bnd_a66 X62 |
% 15.38/14.99 ~ bnd_c8_2 bnd_a66 X62) |
% 15.38/14.99 bnd_c5_2 bnd_a66 X62)) &
% 15.38/14.99 (ALL X63.
% 15.38/14.99 bnd_ndr1_1 bnd_a66 -->
% 15.38/14.99 (bnd_c2_2 bnd_a66 X63 |
% 15.38/14.99 ~ bnd_c8_2 bnd_a66 X63) |
% 15.38/14.99 bnd_c3_2 bnd_a66 X63)) &
% 15.38/14.99 ~ bnd_c3_1 bnd_a66) |
% 15.38/14.99 ~ bnd_c1_0)) &
% 15.38/14.99 ((ALL X64.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c2_1 X64 | bnd_c3_1 X64) |
% 15.38/14.99 bnd_c5_1 X64) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 ((~ bnd_c7_0 |
% 15.38/14.99 (ALL X65.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 X65 & ~ bnd_c4_2 X65 bnd_a67) &
% 15.38/14.99 ~ bnd_c7_2 X65 bnd_a67 |
% 15.38/14.99 bnd_c6_1 X65) |
% 15.38/14.99 bnd_c2_1 X65)) |
% 15.38/14.99 ((bnd_ndr1_0 & bnd_c2_1 bnd_a68) &
% 15.38/14.99 (ALL X66.
% 15.38/14.99 bnd_ndr1_1 bnd_a68 -->
% 15.38/14.99 bnd_c7_2 bnd_a68 X66 |
% 15.38/14.99 bnd_c6_2 bnd_a68 X66)) &
% 15.38/14.99 bnd_c5_1 bnd_a68)) &
% 15.38/14.99 ((~ bnd_c7_0 | ~ bnd_c8_0) |
% 15.38/14.99 (ALL X67.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c3_1 X67 |
% 15.38/14.99 ((bnd_ndr1_1 X67 & ~ bnd_c1_2 X67 bnd_a69) &
% 15.38/14.99 ~ bnd_c6_2 X67 bnd_a69) &
% 15.38/14.99 bnd_c5_2 X67 bnd_a69) |
% 15.38/14.99 ((bnd_ndr1_1 X67 & ~ bnd_c6_2 X67 bnd_a70) &
% 15.38/14.99 bnd_c7_2 X67 bnd_a70) &
% 15.38/14.99 bnd_c4_2 X67 bnd_a70))) &
% 15.38/14.99 (((ALL X68.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X68 & ~ bnd_c1_2 X68 bnd_a71) &
% 15.38/14.99 ~ bnd_c3_2 X68 bnd_a71) &
% 15.38/14.99 bnd_c5_2 X68 bnd_a71 |
% 15.38/14.99 ((bnd_ndr1_1 X68 & ~ bnd_c1_2 X68 bnd_a72) &
% 15.38/14.99 bnd_c8_2 X68 bnd_a72) &
% 15.38/14.99 bnd_c7_2 X68 bnd_a72) |
% 15.38/14.99 bnd_c4_1 X68) |
% 15.38/14.99 ~ bnd_c8_0) |
% 15.38/14.99 bnd_c5_0)) &
% 15.38/14.99 ((~ bnd_c3_0 |
% 15.38/14.99 ((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X69.
% 15.38/14.99 bnd_ndr1_1 bnd_a73 -->
% 15.38/14.99 (~ bnd_c1_2 bnd_a73 X69 |
% 15.38/14.99 ~ bnd_c2_2 bnd_a73 X69) |
% 15.38/14.99 ~ bnd_c4_2 bnd_a73 X69)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a73) &
% 15.38/14.99 bnd_c5_2 bnd_a73 bnd_a74) &
% 15.38/14.99 bnd_c4_2 bnd_a73 bnd_a74) &
% 15.38/14.99 bnd_c1_1 bnd_a73) |
% 15.38/14.99 ~ bnd_c7_0)) &
% 15.38/14.99 ((bnd_c8_0 |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X70.
% 15.38/14.99 bnd_ndr1_1 bnd_a75 -->
% 15.38/14.99 (bnd_c6_2 bnd_a75 X70 |
% 15.38/14.99 ~ bnd_c2_2 bnd_a75 X70) |
% 15.38/14.99 ~ bnd_c4_2 bnd_a75 X70)) &
% 15.38/14.99 (ALL X71.
% 15.38/14.99 bnd_ndr1_1 bnd_a75 -->
% 15.38/14.99 (~ bnd_c4_2 bnd_a75 X71 |
% 15.38/14.99 ~ bnd_c6_2 bnd_a75 X71) |
% 15.38/14.99 bnd_c3_2 bnd_a75 X71)) &
% 15.38/14.99 (ALL X72.
% 15.38/14.99 bnd_ndr1_1 bnd_a75 -->
% 15.38/14.99 bnd_c8_2 bnd_a75 X72 | ~ bnd_c1_2 bnd_a75 X72)) |
% 15.38/14.99 bnd_c7_0)) &
% 15.38/14.99 ((bnd_c2_0 | bnd_c5_0) |
% 15.38/14.99 (ALL X73.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c3_1 X73 | ~ bnd_c2_1 X73) | bnd_c7_1 X73))) &
% 15.38/14.99 ((bnd_c7_0 |
% 15.38/14.99 (ALL X74.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c1_1 X74 |
% 15.38/14.99 ((bnd_ndr1_1 X74 & ~ bnd_c6_2 X74 bnd_a76) &
% 15.38/14.99 bnd_c7_2 X74 bnd_a76) &
% 15.38/14.99 bnd_c4_2 X74 bnd_a76) |
% 15.38/14.99 (ALL X75.
% 15.38/14.99 bnd_ndr1_1 X74 -->
% 15.38/14.99 (bnd_c8_2 X74 X75 | bnd_c7_2 X74 X75) |
% 15.38/14.99 ~ bnd_c3_2 X74 X75))) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 (bnd_c8_0 |
% 15.38/14.99 (ALL X76.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c3_1 X76 | bnd_c7_1 X76) |
% 15.38/14.99 (ALL X77.
% 15.38/14.99 bnd_ndr1_1 X76 -->
% 15.38/14.99 (~ bnd_c3_2 X76 X77 | bnd_c7_2 X76 X77) |
% 15.38/14.99 bnd_c1_2 X76 X77)))) &
% 15.38/14.99 (((bnd_ndr1_0 & bnd_c7_1 bnd_a77) &
% 15.38/14.99 (ALL X78.
% 15.38/14.99 bnd_ndr1_1 bnd_a77 -->
% 15.38/14.99 (bnd_c1_2 bnd_a77 X78 | bnd_c7_2 bnd_a77 X78) |
% 15.38/14.99 bnd_c8_2 bnd_a77 X78) |
% 15.38/14.99 ~ bnd_c1_0) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 ((ALL X79. bnd_ndr1_0 --> bnd_c7_1 X79 | ~ bnd_c8_1 X79) |
% 15.38/14.99 bnd_c3_0)) &
% 15.38/14.99 (~ bnd_c3_0 |
% 15.38/14.99 ((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X80.
% 15.38/14.99 bnd_ndr1_1 bnd_a78 -->
% 15.38/14.99 (bnd_c3_2 bnd_a78 X80 | ~ bnd_c7_2 bnd_a78 X80) |
% 15.38/14.99 bnd_c5_2 bnd_a78 X80)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a78) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a78 bnd_a79) &
% 15.38/14.99 bnd_c6_2 bnd_a78 bnd_a79) &
% 15.38/14.99 ~ bnd_c1_1 bnd_a78)) &
% 15.38/14.99 ((bnd_c7_0 | bnd_c6_0) |
% 15.38/14.99 (bnd_ndr1_0 & ~ bnd_c4_1 bnd_a80) & ~ bnd_c2_1 bnd_a80)) &
% 15.38/14.99 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a81) &
% 15.38/14.99 bnd_c4_2 bnd_a81 bnd_a82) &
% 15.38/14.99 bnd_c8_2 bnd_a81 bnd_a82) &
% 15.38/14.99 bnd_c3_2 bnd_a81 bnd_a82) &
% 15.38/14.99 ~ bnd_c6_1 bnd_a81) &
% 15.38/14.99 bnd_c7_1 bnd_a81 |
% 15.38/14.99 ~ bnd_c1_0)) &
% 15.38/14.99 ((bnd_c1_0 |
% 15.38/14.99 (((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a83) & bnd_ndr1_1 bnd_a83) &
% 15.38/14.99 bnd_c5_2 bnd_a83 bnd_a84) &
% 15.38/14.99 ~ bnd_c2_2 bnd_a83 bnd_a84) &
% 15.38/14.99 bnd_c3_2 bnd_a83 bnd_a84) &
% 15.38/14.99 ~ bnd_c7_1 bnd_a83) |
% 15.38/14.99 (((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a85) & bnd_ndr1_1 bnd_a85) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a85 bnd_a86) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a85 bnd_a86) &
% 15.38/14.99 bnd_c7_2 bnd_a85 bnd_a86) &
% 15.38/14.99 bnd_c7_1 bnd_a85)) &
% 15.38/14.99 (((ALL X81.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c7_1 X81 |
% 15.38/14.99 (ALL X82.
% 15.38/14.99 bnd_ndr1_1 X81 -->
% 15.38/14.99 (~ bnd_c4_2 X81 X82 | bnd_c8_2 X81 X82) |
% 15.38/14.99 bnd_c7_2 X81 X82)) |
% 15.38/14.99 ~ bnd_c5_1 X81) |
% 15.38/14.99 (ALL X83.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X83 & bnd_c8_2 X83 bnd_a87) &
% 15.38/14.99 bnd_c5_2 X83 bnd_a87) &
% 15.38/14.99 bnd_c1_2 X83 bnd_a87 |
% 15.38/14.99 ~ bnd_c7_1 X83) |
% 15.38/14.99 (bnd_ndr1_1 X83 & ~ bnd_c7_2 X83 bnd_a88) &
% 15.38/14.99 bnd_c1_2 X83 bnd_a88)) |
% 15.38/14.99 (ALL X84.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c2_1 X84 | bnd_c3_1 X84) |
% 15.38/14.99 (ALL X85.
% 15.38/14.99 bnd_ndr1_1 X84 -->
% 15.38/14.99 (bnd_c4_2 X84 X85 | bnd_c1_2 X84 X85) |
% 15.38/14.99 ~ bnd_c6_2 X84 X85)))) &
% 15.38/14.99 bnd_c6_0) &
% 15.38/14.99 bnd_c4_0) &
% 15.38/14.99 (((ALL X86.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 bnd_c5_1 X86 |
% 15.38/14.99 ((bnd_ndr1_1 X86 & bnd_c2_2 X86 bnd_a89) &
% 15.38/14.99 ~ bnd_c7_2 X86 bnd_a89) &
% 15.38/14.99 bnd_c1_2 X86 bnd_a89) |
% 15.38/14.99 (((((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X87.
% 15.38/14.99 bnd_ndr1_1 bnd_a90 -->
% 15.38/14.99 (~ bnd_c1_2 bnd_a90 X87 | ~ bnd_c2_2 bnd_a90 X87) |
% 15.38/14.99 ~ bnd_c6_2 bnd_a90 X87)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a90) &
% 15.38/14.99 bnd_c1_2 bnd_a90 bnd_a91) &
% 15.38/14.99 bnd_c3_2 bnd_a90 bnd_a91) &
% 15.38/14.99 bnd_ndr1_1 bnd_a90) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a90 bnd_a92) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a90 bnd_a92) &
% 15.38/14.99 bnd_c7_2 bnd_a90 bnd_a92) |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X88.
% 15.38/14.99 bnd_ndr1_1 bnd_a93 -->
% 15.38/14.99 (bnd_c5_2 bnd_a93 X88 | ~ bnd_c6_2 bnd_a93 X88) |
% 15.38/14.99 bnd_c8_2 bnd_a93 X88)) &
% 15.38/14.99 (ALL X89.
% 15.38/14.99 bnd_ndr1_1 bnd_a93 -->
% 15.38/14.99 ~ bnd_c4_2 bnd_a93 X89 | bnd_c6_2 bnd_a93 X89)) &
% 15.38/14.99 (ALL X90.
% 15.38/14.99 bnd_ndr1_1 bnd_a93 -->
% 15.38/14.99 ~ bnd_c6_2 bnd_a93 X90 | ~ bnd_c7_2 bnd_a93 X90))) &
% 15.38/14.99 ((bnd_c5_0 |
% 15.38/14.99 (ALL X91.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c5_1 X91 | bnd_c4_1 X91) | bnd_c1_1 X91)) |
% 15.38/14.99 (ALL X92.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c2_1 X92 |
% 15.38/14.99 ((bnd_ndr1_1 X92 & ~ bnd_c5_2 X92 bnd_a94) &
% 15.38/14.99 bnd_c6_2 X92 bnd_a94) &
% 15.38/14.99 bnd_c2_2 X92 bnd_a94) |
% 15.38/14.99 ((bnd_ndr1_1 X92 & bnd_c5_2 X92 bnd_a95) &
% 15.38/14.99 bnd_c1_2 X92 bnd_a95) &
% 15.38/14.99 bnd_c6_2 X92 bnd_a95))) &
% 15.38/14.99 (((ALL X93.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X94.
% 15.38/14.99 bnd_ndr1_1 X93 -->
% 15.38/14.99 (bnd_c4_2 X93 X94 | ~ bnd_c1_2 X93 X94) |
% 15.38/14.99 bnd_c2_2 X93 X94) |
% 15.38/14.99 bnd_c6_1 X93) |
% 15.38/14.99 bnd_c1_1 X93) |
% 15.38/14.99 bnd_c3_0) |
% 15.38/14.99 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a96) & bnd_c3_1 bnd_a96) &
% 15.38/14.99 bnd_ndr1_1 bnd_a96) &
% 15.38/14.99 bnd_c7_2 bnd_a96 bnd_a97) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a96 bnd_a97) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a96 bnd_a97)) &
% 15.38/14.99 ((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a98) & ~ bnd_c5_1 bnd_a98) &
% 15.38/14.99 (ALL X95.
% 15.38/14.99 bnd_ndr1_1 bnd_a98 -->
% 15.38/14.99 (bnd_c5_2 bnd_a98 X95 | bnd_c4_2 bnd_a98 X95) |
% 15.38/14.99 bnd_c8_2 bnd_a98 X95) |
% 15.38/14.99 ~ bnd_c3_0) |
% 15.38/14.99 ~ bnd_c8_0)) &
% 15.38/14.99 (((ALL X96.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (ALL X97.
% 15.38/14.99 bnd_ndr1_1 X96 -->
% 15.38/14.99 (~ bnd_c2_2 X96 X97 | ~ bnd_c1_2 X96 X97) |
% 15.38/14.99 bnd_c6_2 X96 X97) |
% 15.38/14.99 ((bnd_ndr1_1 X96 & ~ bnd_c6_2 X96 bnd_a99) &
% 15.38/14.99 ~ bnd_c5_2 X96 bnd_a99) &
% 15.38/14.99 bnd_c4_2 X96 bnd_a99) |
% 15.38/14.99 (ALL X98.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X98 | ~ bnd_c2_1 X98) |
% 15.38/14.99 (ALL X99.
% 15.38/14.99 bnd_ndr1_1 X98 -->
% 15.38/14.99 (~ bnd_c1_2 X98 X99 | bnd_c3_2 X98 X99) |
% 15.38/14.99 ~ bnd_c5_2 X98 X99))) |
% 15.38/14.99 ~ bnd_c8_0)) &
% 15.38/14.99 ((~ bnd_c1_0 |
% 15.38/14.99 (ALL X100.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X101.
% 15.38/14.99 bnd_ndr1_1 X100 -->
% 15.38/14.99 (bnd_c6_2 X100 X101 | ~ bnd_c3_2 X100 X101) |
% 15.38/14.99 bnd_c2_2 X100 X101) |
% 15.38/14.99 (ALL X102.
% 15.38/14.99 bnd_ndr1_1 X100 -->
% 15.38/14.99 (bnd_c7_2 X100 X102 | ~ bnd_c5_2 X100 X102) |
% 15.38/14.99 ~ bnd_c8_2 X100 X102)) |
% 15.38/14.99 bnd_c7_1 X100)) |
% 15.38/14.99 (ALL X103.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c3_1 X103 | ~ bnd_c1_1 X103) | bnd_c4_1 X103))) &
% 15.38/14.99 (((ALL X104.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X104 & bnd_c4_2 X104 bnd_a100) &
% 15.38/14.99 bnd_c5_2 X104 bnd_a100) &
% 15.38/14.99 bnd_c2_2 X104 bnd_a100 |
% 15.38/14.99 bnd_c8_1 X104) |
% 15.38/14.99 (ALL X105.
% 15.38/14.99 bnd_ndr1_1 X104 -->
% 15.38/14.99 (bnd_c7_2 X104 X105 | ~ bnd_c2_2 X104 X105) |
% 15.38/14.99 bnd_c4_2 X104 X105)) |
% 15.38/14.99 ~ bnd_c5_0) |
% 15.38/14.99 (ALL X106.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X107.
% 15.38/14.99 bnd_ndr1_1 X106 --> bnd_c2_2 X106 X107 | bnd_c4_2 X106 X107) |
% 15.38/14.99 ((bnd_ndr1_1 X106 & bnd_c7_2 X106 bnd_a101) &
% 15.38/14.99 ~ bnd_c2_2 X106 bnd_a101) &
% 15.38/14.99 bnd_c4_2 X106 bnd_a101) |
% 15.38/14.99 ((bnd_ndr1_1 X106 & bnd_c7_2 X106 bnd_a102) &
% 15.38/14.99 ~ bnd_c1_2 X106 bnd_a102) &
% 15.38/14.99 ~ bnd_c4_2 X106 bnd_a102))) &
% 15.38/14.99 (~ bnd_c1_0 | ~ bnd_c2_0)) &
% 15.38/14.99 ((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X108.
% 15.38/14.99 bnd_ndr1_1 bnd_a103 -->
% 15.38/14.99 (bnd_c5_2 bnd_a103 X108 | bnd_c4_2 bnd_a103 X108) |
% 15.38/14.99 bnd_c1_2 bnd_a103 X108)) &
% 15.38/14.99 bnd_c3_1 bnd_a103) &
% 15.38/14.99 (ALL X109.
% 15.38/14.99 bnd_ndr1_1 bnd_a103 -->
% 15.38/14.99 (~ bnd_c4_2 bnd_a103 X109 | bnd_c8_2 bnd_a103 X109) |
% 15.38/14.99 ~ bnd_c5_2 bnd_a103 X109) |
% 15.38/14.99 bnd_c5_0) |
% 15.38/14.99 ~ bnd_c8_0)) &
% 15.38/14.99 ((~ bnd_c7_0 | bnd_c8_0) |
% 15.38/14.99 (ALL X110.
% 15.38/14.99 bnd_ndr1_0 --> (~ bnd_c8_1 X110 | bnd_c6_1 X110) | bnd_c4_1 X110))) &
% 15.38/14.99 (((ALL X111.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X112.
% 15.38/14.99 bnd_ndr1_1 X111 -->
% 15.38/14.99 (bnd_c6_2 X111 X112 | bnd_c5_2 X111 X112) | ~ bnd_c2_2 X111 X112) |
% 15.38/14.99 ~ bnd_c2_1 X111) |
% 15.38/14.99 ~ bnd_c6_1 X111) |
% 15.38/14.99 bnd_c5_0) |
% 15.38/14.99 (bnd_ndr1_0 & ~ bnd_c5_1 bnd_a104) &
% 15.38/14.99 (ALL X113.
% 15.38/14.99 bnd_ndr1_1 bnd_a104 -->
% 15.38/14.99 ~ bnd_c1_2 bnd_a104 X113 | bnd_c8_2 bnd_a104 X113))) &
% 15.38/14.99 (~ bnd_c2_0 |
% 15.38/14.99 ((((((((bnd_ndr1_0 &
% 15.38/14.99 bnd_ndr1_1 bnd_a105) &
% 15.38/14.99 bnd_c1_2 bnd_a105 bnd_a106) &
% 15.38/14.99 bnd_c7_2 bnd_a105 bnd_a106) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a105 bnd_a106) &
% 15.38/14.99 bnd_ndr1_1 bnd_a105) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a105 bnd_a107) &
% 15.38/14.99 bnd_c4_2 bnd_a105 bnd_a107) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a105 bnd_a107) &
% 15.38/14.99 bnd_c3_1 bnd_a105)) &
% 15.38/14.99 ((ALL X114.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X114 |
% 15.38/14.99 (ALL X115.
% 15.38/14.99 bnd_ndr1_1 X114 --> ~ bnd_c5_2 X114 X115 | ~ bnd_c8_2 X114 X115)) |
% 15.38/14.99 ((bnd_ndr1_1 X114 & bnd_c6_2 X114 bnd_a108) & ~ bnd_c5_2 X114 bnd_a108) &
% 15.38/14.99 ~ bnd_c7_2 X114 bnd_a108) |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 (((ALL X116.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X116 |
% 15.38/14.99 ((bnd_ndr1_1 X116 & bnd_c7_2 X116 bnd_a109) & bnd_c1_2 X116 bnd_a109) &
% 15.38/14.99 ~ bnd_c4_2 X116 bnd_a109) |
% 15.38/14.99 bnd_c6_1 X116) |
% 15.38/14.99 ~ bnd_c2_0) |
% 15.38/14.99 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a110) &
% 15.38/14.99 bnd_c4_2 bnd_a110 bnd_a111) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a110 bnd_a111) &
% 15.38/14.99 bnd_c1_1 bnd_a110) &
% 15.38/14.99 bnd_ndr1_1 bnd_a110) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a110 bnd_a112) &
% 15.38/14.99 bnd_c5_2 bnd_a110 bnd_a112) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a110 bnd_a112)) &
% 15.38/14.99 ((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a113) &
% 15.38/14.99 ~ bnd_c4_1 bnd_a113) &
% 15.38/14.99 (ALL X117.
% 15.38/14.99 bnd_ndr1_1 bnd_a113 -->
% 15.38/14.99 (~ bnd_c4_2 bnd_a113 X117 | bnd_c8_2 bnd_a113 X117) |
% 15.38/14.99 bnd_c7_2 bnd_a113 X117) |
% 15.38/14.99 (ALL X118.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X118 & bnd_c5_2 X118 bnd_a114) & bnd_c1_2 X118 bnd_a114) &
% 15.38/14.99 bnd_c8_2 X118 bnd_a114 |
% 15.38/14.99 bnd_c3_1 X118) |
% 15.38/14.99 ~ bnd_c7_1 X118)) |
% 15.38/14.99 ~ bnd_c1_0)) &
% 15.38/14.99 ((~ bnd_c2_0 |
% 15.38/14.99 (ALL X119.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X120.
% 15.38/14.99 bnd_ndr1_1 X119 -->
% 15.38/14.99 (bnd_c7_2 X119 X120 | bnd_c2_2 X119 X120) | ~ bnd_c1_2 X119 X120) |
% 15.38/14.99 bnd_c6_1 X119) |
% 15.38/14.99 ~ bnd_c4_1 X119)) |
% 15.38/14.99 (ALL X121.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 bnd_c1_1 X121 |
% 15.38/14.99 (ALL X122.
% 15.38/14.99 bnd_ndr1_1 X121 -->
% 15.38/14.99 (bnd_c5_2 X121 X122 | ~ bnd_c6_2 X121 X122) | ~ bnd_c7_2 X121 X122)))) &
% 15.38/14.99 ((~ bnd_c7_0 |
% 15.38/14.99 (ALL X123.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 X123 &
% 15.38/14.99 ~ bnd_c3_2 X123 bnd_a115) &
% 15.38/14.99 ~ bnd_c7_2 X123 bnd_a115) &
% 15.38/14.99 ~ bnd_c8_2 X123 bnd_a115 |
% 15.38/14.99 ~ bnd_c8_1 X123)) |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 ((ALL X124.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c4_1 X124 | bnd_c8_1 X124) |
% 15.38/14.99 ((bnd_ndr1_1 X124 &
% 15.38/14.99 bnd_c2_2 X124 bnd_a116) &
% 15.38/14.99 bnd_c1_2 X124 bnd_a116) &
% 15.38/14.99 ~ bnd_c5_2 X124 bnd_a116) |
% 15.38/14.99 (ALL X125.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X125 | bnd_c4_1 X125) |
% 15.38/14.99 (ALL X126.
% 15.38/14.99 bnd_ndr1_1 X125 -->
% 15.38/14.99 (~ bnd_c4_2 X125 X126 | bnd_c6_2 X125 X126) | bnd_c1_2 X125 X126)))) &
% 15.38/14.99 ((~ bnd_c1_0 |
% 15.38/14.99 (ALL X127.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ~ bnd_c8_1 X127 | ~ bnd_c7_1 X127)) |
% 15.38/14.99 bnd_c7_0)) &
% 15.38/14.99 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a117) &
% 15.38/14.99 bnd_c8_1 bnd_a117 |
% 15.38/14.99 bnd_c3_0)) &
% 15.38/14.99 (((((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X128.
% 15.38/14.99 bnd_ndr1_1 bnd_a118 -->
% 15.38/14.99 (bnd_c8_2 bnd_a118 X128 |
% 15.38/14.99 bnd_c1_2 bnd_a118 X128) |
% 15.38/14.99 ~ bnd_c6_2 bnd_a118 X128)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a118) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a118 bnd_a119) &
% 15.38/14.99 bnd_c2_2 bnd_a118 bnd_a119) &
% 15.38/14.99 bnd_c7_2 bnd_a118 bnd_a119) &
% 15.38/14.99 (ALL X129.
% 15.38/14.99 bnd_ndr1_1 bnd_a118 -->
% 15.38/14.99 (bnd_c2_2 bnd_a118 X129 |
% 15.38/14.99 bnd_c5_2 bnd_a118 X129) |
% 15.38/14.99 ~ bnd_c4_2 bnd_a118 X129) |
% 15.38/14.99 ~ bnd_c2_0) |
% 15.38/14.99 ~ bnd_c7_0)) &
% 15.38/14.99 (((bnd_ndr1_0 &
% 15.38/14.99 (ALL X130.
% 15.38/14.99 bnd_ndr1_1 bnd_a120 -->
% 15.38/14.99 (~ bnd_c8_2 bnd_a120 X130 |
% 15.38/14.99 bnd_c1_2 bnd_a120 X130) |
% 15.38/14.99 ~ bnd_c6_2 bnd_a120 X130)) &
% 15.38/14.99 ~ bnd_c5_1 bnd_a120) &
% 15.38/14.99 (ALL X131.
% 15.38/14.99 bnd_ndr1_1 bnd_a120 -->
% 15.38/14.99 (~ bnd_c5_2 bnd_a120 X131 |
% 15.38/14.99 ~ bnd_c1_2 bnd_a120 X131) |
% 15.38/14.99 ~ bnd_c7_2 bnd_a120 X131) |
% 15.38/14.99 ((bnd_ndr1_0 &
% 15.38/14.99 (ALL X132.
% 15.38/14.99 bnd_ndr1_1 bnd_a121 -->
% 15.38/14.99 (bnd_c8_2 bnd_a121 X132 |
% 15.38/14.99 ~ bnd_c7_2 bnd_a121 X132) |
% 15.38/14.99 bnd_c5_2 bnd_a121 X132)) &
% 15.38/14.99 bnd_c5_1 bnd_a121) &
% 15.38/14.99 bnd_c3_1 bnd_a121)) &
% 15.38/14.99 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a122) &
% 15.38/14.99 bnd_c5_2 bnd_a122 bnd_a123) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a122 bnd_a123) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a122 bnd_a123) &
% 15.38/14.99 bnd_c8_1 bnd_a122) &
% 15.38/14.99 ~ bnd_c1_1 bnd_a122 |
% 15.38/14.99 bnd_c2_0)) &
% 15.38/14.99 (((((((((bnd_ndr1_0 & bnd_c4_1 bnd_a124) &
% 15.38/14.99 bnd_ndr1_1 bnd_a124) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a124 bnd_a125) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a124 bnd_a125) &
% 15.38/14.99 bnd_c6_2 bnd_a124 bnd_a125) &
% 15.38/14.99 bnd_ndr1_1 bnd_a124) &
% 15.38/14.99 bnd_c8_2 bnd_a124 bnd_a126) &
% 15.38/14.99 bnd_c6_2 bnd_a124 bnd_a126 |
% 15.38/14.99 ~ bnd_c3_0) |
% 15.38/14.99 (ALL X133.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c7_1 X133 | ~ bnd_c6_1 X133) |
% 15.38/14.99 (ALL X134.
% 15.38/14.99 bnd_ndr1_1 X133 -->
% 15.38/14.99 (bnd_c6_2 X133 X134 | bnd_c8_2 X133 X134) |
% 15.38/14.99 ~ bnd_c2_2 X133 X134)))) &
% 15.38/14.99 (((ALL X135.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((ALL X136.
% 15.38/14.99 bnd_ndr1_1 X135 -->
% 15.38/14.99 (bnd_c4_2 X135 X136 |
% 15.38/14.99 ~ bnd_c8_2 X135 X136) |
% 15.38/14.99 bnd_c3_2 X135 X136) |
% 15.38/14.99 ~ bnd_c4_1 X135) |
% 15.38/14.99 (ALL X137.
% 15.38/14.99 bnd_ndr1_1 X135 -->
% 15.38/14.99 (~ bnd_c7_2 X135 X137 |
% 15.38/14.99 bnd_c8_2 X135 X137) |
% 15.38/14.99 bnd_c6_2 X135 X137)) |
% 15.38/14.99 ((bnd_ndr1_0 & bnd_c8_1 bnd_a127) &
% 15.38/14.99 bnd_c3_1 bnd_a127) &
% 15.38/14.99 ~ bnd_c5_1 bnd_a127) |
% 15.38/14.99 ~ bnd_c7_0)) &
% 15.38/14.99 ((~ bnd_c1_0 |
% 15.38/14.99 (ALL X138.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 X138 & ~ bnd_c7_2 X138 bnd_a128) &
% 15.38/14.99 ~ bnd_c8_2 X138 bnd_a128) &
% 15.38/14.99 ~ bnd_c4_2 X138 bnd_a128 |
% 15.38/14.99 ~ bnd_c1_1 X138)) |
% 15.38/14.99 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a129) &
% 15.38/14.99 ~ bnd_c6_2 bnd_a129 bnd_a130) &
% 15.38/14.99 ~ bnd_c8_2 bnd_a129 bnd_a130) &
% 15.38/14.99 bnd_c3_2 bnd_a129 bnd_a130) &
% 15.38/14.99 bnd_ndr1_1 bnd_a129) &
% 15.38/14.99 bnd_c1_2 bnd_a129 bnd_a131) &
% 15.38/14.99 ~ bnd_c7_2 bnd_a129 bnd_a131) &
% 15.38/14.99 bnd_c8_2 bnd_a129 bnd_a131) &
% 15.38/14.99 ~ bnd_c6_1 bnd_a129)) &
% 15.38/14.99 (((ALL X139.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_c8_1 X139 | bnd_c2_1 X139) |
% 15.38/14.99 ~ bnd_c7_1 X139) |
% 15.38/14.99 (ALL X140.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c1_1 X140 | ~ bnd_c8_1 X140) |
% 15.38/14.99 (ALL X141.
% 15.38/14.99 bnd_ndr1_1 X140 -->
% 15.38/14.99 (bnd_c7_2 X140 X141 | ~ bnd_c2_2 X140 X141) |
% 15.38/14.99 bnd_c3_2 X140 X141))) |
% 15.38/14.99 (ALL X142.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c4_1 X142 | ~ bnd_c6_1 X142) |
% 15.38/14.99 ~ bnd_c5_1 X142))) &
% 15.38/14.99 ((ALL X143.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (((bnd_ndr1_1 X143 & ~ bnd_c3_2 X143 bnd_a132) &
% 15.38/14.99 ~ bnd_c8_2 X143 bnd_a132) &
% 15.38/14.99 ~ bnd_c6_2 X143 bnd_a132 |
% 15.38/14.99 ~ bnd_c1_1 X143) |
% 15.38/14.99 (ALL X144.
% 15.38/14.99 bnd_ndr1_1 X143 -->
% 15.38/14.99 (~ bnd_c4_2 X143 X144 | bnd_c7_2 X143 X144) |
% 15.38/14.99 ~ bnd_c8_2 X143 X144)) |
% 15.38/14.99 ~ bnd_c8_0)) &
% 15.38/14.99 ((ALL X145.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c6_1 X145 | ~ bnd_c2_1 X145) |
% 15.38/14.99 ((bnd_ndr1_1 X145 & ~ bnd_c1_2 X145 bnd_a133) &
% 15.38/14.99 ~ bnd_c5_2 X145 bnd_a133) &
% 15.38/14.99 bnd_c3_2 X145 bnd_a133) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 ((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a134) &
% 15.38/14.99 bnd_ndr1_1 bnd_a134) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a134 bnd_a135) &
% 15.38/14.99 bnd_c8_2 bnd_a134 bnd_a135) &
% 15.38/14.99 bnd_c3_2 bnd_a134 bnd_a135) &
% 15.38/14.99 (ALL X146.
% 15.38/14.99 bnd_ndr1_1 bnd_a134 -->
% 15.38/14.99 bnd_c1_2 bnd_a134 X146 | bnd_c8_2 bnd_a134 X146) |
% 15.38/14.99 (ALL X147.
% 15.38/14.99 bnd_ndr1_0 --> bnd_c8_1 X147 | ~ bnd_c2_1 X147))) &
% 15.38/14.99 bnd_ndr1_0) &
% 15.38/14.99 bnd_c5_1 bnd_a136) &
% 15.38/14.99 (ALL X148.
% 15.38/14.99 bnd_ndr1_1 bnd_a136 -->
% 15.38/14.99 (bnd_c8_2 bnd_a136 X148 | bnd_c3_2 bnd_a136 X148) |
% 15.38/14.99 bnd_c7_2 bnd_a136 X148)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a136) &
% 15.38/14.99 bnd_c1_2 bnd_a136 bnd_a137) &
% 15.38/14.99 bnd_c3_2 bnd_a136 bnd_a137) &
% 15.38/14.99 bnd_c5_2 bnd_a136 bnd_a137) &
% 15.38/14.99 ((~ bnd_c3_0 |
% 15.38/14.99 (((((((bnd_ndr1_0 &
% 15.38/14.99 (ALL X149.
% 15.38/14.99 bnd_ndr1_1 bnd_a138 -->
% 15.38/14.99 (bnd_c3_2 bnd_a138 X149 | ~ bnd_c4_2 bnd_a138 X149) |
% 15.38/14.99 ~ bnd_c6_2 bnd_a138 X149)) &
% 15.38/14.99 bnd_ndr1_1 bnd_a138) &
% 15.38/14.99 bnd_c6_2 bnd_a138 bnd_a139) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a138 bnd_a139) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a138 bnd_a139) &
% 15.38/14.99 bnd_ndr1_1 bnd_a138) &
% 15.38/14.99 bnd_c5_2 bnd_a138 bnd_a140) &
% 15.38/14.99 ~ bnd_c4_2 bnd_a138 bnd_a140) |
% 15.38/14.99 bnd_c7_0)) &
% 15.38/14.99 ((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a141) & bnd_c8_1 bnd_a141) &
% 15.38/14.99 bnd_ndr1_1 bnd_a141) &
% 15.38/14.99 ~ bnd_c3_2 bnd_a141 bnd_a142) &
% 15.38/14.99 bnd_c8_2 bnd_a141 bnd_a142 |
% 15.38/14.99 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a143) & bnd_ndr1_1 bnd_a143) &
% 15.38/14.99 ~ bnd_c1_2 bnd_a143 bnd_a144) &
% 15.38/14.99 ~ bnd_c5_2 bnd_a143 bnd_a144) &
% 15.38/14.99 bnd_c2_2 bnd_a143 bnd_a144) |
% 15.38/14.99 ~ bnd_c2_0)) &
% 15.38/14.99 (bnd_c7_0 |
% 15.38/14.99 (ALL X150.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 ((bnd_ndr1_1 X150 & ~ bnd_c4_2 X150 bnd_a145) &
% 15.38/14.99 bnd_c6_2 X150 bnd_a145) &
% 15.38/14.99 bnd_c5_2 X150 bnd_a145))) &
% 15.38/14.99 ((~ bnd_c2_0 | ~ bnd_c1_0) |
% 15.38/14.99 (ALL X151.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (bnd_ndr1_1 X151 & ~ bnd_c2_2 X151 bnd_a146 | bnd_c2_1 X151) |
% 15.38/14.99 (ALL X152.
% 15.38/14.99 bnd_ndr1_1 X151 -->
% 15.38/14.99 (bnd_c5_2 X151 X152 | ~ bnd_c1_2 X151 X152) |
% 15.38/14.99 bnd_c8_2 X151 X152)))) &
% 15.38/14.99 ~ bnd_c2_0) &
% 15.38/14.99 (bnd_c7_0 |
% 15.38/14.99 (ALL X153.
% 15.38/14.99 bnd_ndr1_0 -->
% 15.38/14.99 (~ bnd_c3_1 X153 | bnd_c1_1 X153) |
% 15.38/14.99 (ALL X154.
% 15.38/14.99 bnd_ndr1_1 X153 -->
% 15.38/14.99 (bnd_c2_2 X153 X154 | ~ bnd_c8_2 X153 X154) |
% 15.38/14.99 bnd_c6_2 X153 X154)))) &
% 15.38/14.99 ~ bnd_c3_0)
% 15.38/14.99 Adding axioms...
% 15.38/15.00 Typedef.type_definition_def
% 42.04/41.55 ...done.
% 42.04/41.58 Ground types: ?'b, TPTP_Interpret.ind
% 42.04/41.58 Translating term (sizes: 1, 1) ...
% 63.47/62.96 Invoking SAT solver...
% 63.47/62.96 No model exists.
% 63.47/62.96 Translating term (sizes: 2, 1) ...
% 85.63/85.01 Invoking SAT solver...
% 85.63/85.01 No model exists.
% 85.63/85.01 Translating term (sizes: 1, 2) ...
% 125.24/124.55 Invoking SAT solver...
% 126.36/125.67 Model found:
% 126.36/125.67 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 126.36/125.67 bnd_a146: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a145: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a144: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a143: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a142: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a141: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a140: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a139: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a138: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a137: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a136: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a135: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a134: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a133: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a132: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a131: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a130: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a129: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a128: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a127: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a126: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a125: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a124: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a123: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a122: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a121: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a120: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a119: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a118: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a117: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a116: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a115: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a114: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a113: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a112: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a111: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a110: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a109: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a108: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a107: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a106: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a105: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a104: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a103: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a102: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a101: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a100: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a99: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a98: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a97: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a96: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a95: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a94: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a93: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a92: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a91: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a90: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a89: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a88: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a87: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a86: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a85: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a84: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a83: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a82: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a81: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a80: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a79: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a78: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a77: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a76: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a75: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a74: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a73: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a72: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a71: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a70: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a69: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a68: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a67: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a66: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a65: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a64: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a63: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a62: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a61: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a60: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a59: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a58: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a57: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a56: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a55: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a54: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a53: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a52: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a51: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a50: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a49: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a48: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a47: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a46: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a45: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a44: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a43: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a42: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a41: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a40: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a39: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a38: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a37: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a36: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a35: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a34: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_a33: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a32: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a31: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a30: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a29: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a28: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a27: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a26: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a25: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a24: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a23: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a22: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a21: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a20: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a19: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a18: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_c6_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 126.36/125.67 bnd_c6_0: True
% 126.36/125.67 bnd_a17: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a16: ??.TPTP_Interpret.ind1
% 126.36/125.67 bnd_c3_0: False
% 126.36/125.67 bnd_a15: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a14: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a13: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c7_0: True
% 126.36/125.67 bnd_a12: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a11: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_a10: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c4_0: True
% 126.36/125.67 bnd_c1_0: False
% 126.36/125.67 bnd_a9: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c4_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 126.36/125.67 bnd_a8: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c2_0: False
% 126.36/125.67 bnd_c8_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 126.36/125.67 bnd_a7: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c3_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 126.36/125.67 bnd_c8_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 126.36/125.67 bnd_a6: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c8_0: True
% 126.36/125.67 bnd_c2_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 126.36/125.67 bnd_c5_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 126.36/125.67 bnd_a5: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c3_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 126.36/125.67 bnd_a4: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c1_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 126.36/125.67 bnd_c5_0: False
% 126.36/125.67 bnd_c6_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 126.36/125.67 bnd_a3: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c7_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 126.36/125.67 bnd_a2: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c1_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 126.36/125.67 bnd_a1: ??.TPTP_Interpret.ind0
% 126.36/125.67 bnd_c4_2: {(??.TPTP_Interpret.ind0,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}),
% 126.36/125.67 (??.TPTP_Interpret.ind1,
% 126.36/125.67 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}
% 126.36/125.67 bnd_ndr1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 126.36/125.67 bnd_c2_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}
% 126.36/125.67 bnd_c5_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 126.36/125.67 bnd_c7_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 126.36/125.67 bnd_ndr1_0: True
% 126.36/125.67
% 126.36/125.67 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------