%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN437+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n092.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:41:48 EDT 2016
% Result : CounterSatisfiable 57.22s
% 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 : SYN437+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.23 % Computer : n092.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.75MB
% 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Fri Apr 8 23:52:09 CDT 2016
% 0.03/0.23 % CPUTime:
% 6.31/5.82 > val it = (): unit
% 6.82/6.32 Trying to find a model that refutes: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~ bnd_hskp0 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a402) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a402) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a402) &
% 6.82/6.32 (~ bnd_hskp1 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a403) &
% 6.82/6.32 bnd_c3_1 bnd_a403) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a403)) &
% 6.82/6.32 (~ bnd_hskp2 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a405) &
% 6.82/6.32 bnd_c0_1 bnd_a405) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a405)) &
% 6.82/6.32 (~ bnd_hskp3 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a407) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a407) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a407)) &
% 6.82/6.32 (~ bnd_hskp4 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a411) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a411) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a411)) &
% 6.82/6.32 (~ bnd_hskp5 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a413) &
% 6.82/6.32 bnd_c0_1 bnd_a413) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a413)) &
% 6.82/6.32 (~ bnd_hskp6 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a416) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a416) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a416)) &
% 6.82/6.32 (~ bnd_hskp7 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a418) &
% 6.82/6.32 bnd_c1_1 bnd_a418) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a418)) &
% 6.82/6.32 (~ bnd_hskp8 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a420) &
% 6.82/6.32 bnd_c1_1 bnd_a420) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a420)) &
% 6.82/6.32 (~ bnd_hskp9 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c3_1 bnd_a421) & bnd_c2_1 bnd_a421) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a421)) &
% 6.82/6.32 (~ bnd_hskp10 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a422) & bnd_c0_1 bnd_a422) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a422)) &
% 6.82/6.32 (~ bnd_hskp11 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a428) & ~ bnd_c1_1 bnd_a428) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a428)) &
% 6.82/6.32 (~ bnd_hskp12 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a430) & bnd_c3_1 bnd_a430) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a430)) &
% 6.82/6.32 (~ bnd_hskp13 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a433) & ~ bnd_c3_1 bnd_a433) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a433)) &
% 6.82/6.32 (~ bnd_hskp14 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a437) & ~ bnd_c1_1 bnd_a437) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a437)) &
% 6.82/6.32 (~ bnd_hskp15 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a440) & bnd_c0_1 bnd_a440) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a440)) &
% 6.82/6.32 (~ bnd_hskp16 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a441) & bnd_c1_1 bnd_a441) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a441)) &
% 6.82/6.32 (~ bnd_hskp17 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a443) & ~ bnd_c1_1 bnd_a443) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a443)) &
% 6.82/6.32 (~ bnd_hskp18 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a444) & bnd_c0_1 bnd_a444) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a444)) &
% 6.82/6.32 (~ bnd_hskp19 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a445) & bnd_c0_1 bnd_a445) &
% 6.82/6.32 ~ bnd_c1_1 bnd_a445)) &
% 6.82/6.32 (~ bnd_hskp20 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a448) & ~ bnd_c1_1 bnd_a448) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a448)) &
% 6.82/6.32 (~ bnd_hskp21 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a450) & bnd_c3_1 bnd_a450) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a450)) &
% 6.82/6.32 (~ bnd_hskp22 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a451) & ~ bnd_c3_1 bnd_a451) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a451)) &
% 6.82/6.32 (~ bnd_hskp23 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a452) & bnd_c3_1 bnd_a452) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a452)) &
% 6.82/6.32 (~ bnd_hskp24 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c0_1 bnd_a454) & ~ bnd_c3_1 bnd_a454) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a454)) &
% 6.82/6.32 (~ bnd_hskp25 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a460) & bnd_c2_1 bnd_a460) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a460)) &
% 6.82/6.32 (~ bnd_hskp26 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a461) & bnd_c3_1 bnd_a461) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a461)) &
% 6.82/6.32 (~ bnd_hskp27 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a404) & ~ bnd_c2_1 bnd_a404) &
% 6.82/6.32 bnd_c1_1 bnd_a404)) &
% 6.82/6.32 (~ bnd_hskp28 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a408) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a408) &
% 6.82/6.32 bnd_c2_1 bnd_a408)) &
% 6.82/6.32 (~ bnd_hskp29 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a409) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a409) &
% 6.82/6.32 bnd_c0_1 bnd_a409)) &
% 6.82/6.32 (~ bnd_hskp30 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a410) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a410) &
% 6.82/6.32 bnd_c1_1 bnd_a410)) &
% 6.82/6.32 (~ bnd_hskp31 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a412) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a412) &
% 6.82/6.32 bnd_c0_1 bnd_a412)) &
% 6.82/6.32 (~ bnd_hskp32 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c3_1 bnd_a414) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a414) &
% 6.82/6.32 bnd_c1_1 bnd_a414)) &
% 6.82/6.32 (~ bnd_hskp33 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a415) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a415) &
% 6.82/6.32 bnd_c0_1 bnd_a415)) &
% 6.82/6.32 (~ bnd_hskp34 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a417) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a417) &
% 6.82/6.32 bnd_c2_1 bnd_a417)) &
% 6.82/6.32 (~ bnd_hskp35 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a419) &
% 6.82/6.32 bnd_c1_1 bnd_a419) &
% 6.82/6.32 bnd_c3_1 bnd_a419)) &
% 6.82/6.32 (~ bnd_hskp36 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a424) &
% 6.82/6.32 bnd_c3_1 bnd_a424) &
% 6.82/6.32 bnd_c2_1 bnd_a424)) &
% 6.82/6.32 (~ bnd_hskp37 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a427) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a427) &
% 6.82/6.32 bnd_c3_1 bnd_a427)) &
% 6.82/6.32 (~ bnd_hskp38 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a429) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a429) &
% 6.82/6.32 bnd_c1_1 bnd_a429)) &
% 6.82/6.32 (~ bnd_hskp39 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c3_1 bnd_a431) &
% 6.82/6.32 bnd_c1_1 bnd_a431) &
% 6.82/6.32 bnd_c2_1 bnd_a431)) &
% 6.82/6.32 (~ bnd_hskp40 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a432) &
% 6.82/6.32 bnd_c1_1 bnd_a432) &
% 6.82/6.32 bnd_c2_1 bnd_a432)) &
% 6.82/6.32 (~ bnd_hskp41 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c0_1 bnd_a434) &
% 6.82/6.32 bnd_c1_1 bnd_a434) &
% 6.82/6.32 bnd_c3_1 bnd_a434)) &
% 6.82/6.32 (~ bnd_hskp42 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a435) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a435) &
% 6.82/6.32 bnd_c0_1 bnd_a435)) &
% 6.82/6.32 (~ bnd_hskp43 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c2_1 bnd_a436) &
% 6.82/6.32 ~ bnd_c0_1 bnd_a436) &
% 6.82/6.32 bnd_c3_1 bnd_a436)) &
% 6.82/6.32 (~ bnd_hskp44 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a438) &
% 6.82/6.32 bnd_c1_1 bnd_a438) &
% 6.82/6.32 bnd_c2_1 bnd_a438)) &
% 6.82/6.32 (~ bnd_hskp45 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c3_1 bnd_a439) &
% 6.82/6.32 ~ bnd_c2_1 bnd_a439) &
% 6.82/6.32 bnd_c0_1 bnd_a439)) &
% 6.82/6.32 (~ bnd_hskp46 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a446) &
% 6.82/6.32 ~ bnd_c3_1 bnd_a446) &
% 6.82/6.32 bnd_c1_1 bnd_a446)) &
% 6.82/6.32 (~ bnd_hskp47 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c0_1 bnd_a449) & ~ bnd_c3_1 bnd_a449) &
% 6.82/6.32 bnd_c1_1 bnd_a449)) &
% 6.82/6.32 (~ bnd_hskp48 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c3_1 bnd_a455) & bnd_c2_1 bnd_a455) &
% 6.82/6.32 bnd_c1_1 bnd_a455)) &
% 6.82/6.32 (~ bnd_hskp49 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a459) & ~ bnd_c1_1 bnd_a459) &
% 6.82/6.32 bnd_c0_1 bnd_a459)) &
% 6.82/6.32 (~ bnd_hskp50 |
% 6.82/6.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a462) & bnd_c3_1 bnd_a462) &
% 6.82/6.32 bnd_c0_1 bnd_a462)) &
% 6.82/6.32 (~ bnd_hskp51 |
% 6.82/6.32 ((bnd_ndr1_0 & bnd_c1_1 bnd_a464) & ~ bnd_c2_1 bnd_a464) &
% 6.82/6.32 bnd_c0_1 bnd_a464)) &
% 6.82/6.32 (((ALL U.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c2_1 U | bnd_c0_1 U) | ~ bnd_c3_1 U) |
% 6.82/6.32 bnd_hskp0) |
% 6.82/6.32 (ALL V.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c1_1 V | bnd_c2_1 V) | ~ bnd_c0_1 V))) &
% 6.82/6.32 (((ALL W.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c1_1 W | ~ bnd_c0_1 W) | ~ bnd_c2_1 W) |
% 6.82/6.32 (ALL X.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c1_1 X | ~ bnd_c3_1 X) | ~ bnd_c2_1 X)) |
% 6.82/6.32 bnd_hskp1)) &
% 6.82/6.32 ((bnd_hskp27 | bnd_hskp2) |
% 6.82/6.32 (ALL Y.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c2_1 Y | ~ bnd_c1_1 Y) | bnd_c3_1 Y))) &
% 6.82/6.32 ((bnd_hskp1 | bnd_hskp3) | bnd_hskp28)) &
% 6.82/6.32 ((bnd_hskp29 |
% 6.82/6.32 (ALL Z.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c0_1 Z | ~ bnd_c3_1 Z) | bnd_c1_1 Z)) |
% 6.82/6.32 bnd_hskp30)) &
% 6.82/6.32 (((ALL X1.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c3_1 X1 | bnd_c1_1 X1) | ~ bnd_c2_1 X1) |
% 6.82/6.32 (ALL X2.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X2 | ~ bnd_c3_1 X2) | bnd_c2_1 X2)) |
% 6.82/6.32 bnd_hskp4)) &
% 6.82/6.32 (((ALL X3.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c0_1 X3 | bnd_c3_1 X3) | ~ bnd_c1_1 X3) |
% 6.82/6.32 bnd_hskp31) |
% 6.82/6.32 (ALL X4.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c0_1 X4 | ~ bnd_c2_1 X4) | bnd_c1_1 X4))) &
% 6.82/6.32 (((ALL X5.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X5 | ~ bnd_c3_1 X5) | ~ bnd_c0_1 X5) |
% 6.82/6.32 bnd_hskp5) |
% 6.82/6.32 (ALL X6.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c2_1 X6 | bnd_c1_1 X6) | ~ bnd_c0_1 X6))) &
% 6.82/6.32 (((ALL X7. bnd_ndr1_0 --> (~ bnd_c1_1 X7 | bnd_c0_1 X7) | bnd_c3_1 X7) |
% 6.82/6.32 (ALL X8.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c3_1 X8 | ~ bnd_c0_1 X8) | ~ bnd_c1_1 X8)) |
% 6.82/6.32 bnd_hskp32)) &
% 6.82/6.32 ((bnd_hskp33 |
% 6.82/6.32 (ALL X9. bnd_ndr1_0 --> (~ bnd_c2_1 X9 | bnd_c0_1 X9) | bnd_c1_1 X9)) |
% 6.82/6.32 bnd_hskp6)) &
% 6.82/6.32 ((bnd_hskp34 |
% 6.82/6.32 (ALL X10.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c2_1 X10 | ~ bnd_c0_1 X10) | bnd_c3_1 X10)) |
% 6.82/6.32 (ALL X11.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c2_1 X11 | ~ bnd_c1_1 X11) | bnd_c0_1 X11))) &
% 6.82/6.32 (((ALL X12.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c3_1 X12 | ~ bnd_c2_1 X12) | bnd_c0_1 X12) |
% 6.82/6.32 (ALL X13.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c1_1 X13 | ~ bnd_c0_1 X13) | ~ bnd_c3_1 X13)) |
% 6.82/6.32 (ALL X14.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c1_1 X14 | ~ bnd_c3_1 X14) | bnd_c2_1 X14))) &
% 6.82/6.32 (((ALL X15.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c0_1 X15 | ~ bnd_c1_1 X15) | ~ bnd_c3_1 X15) |
% 6.82/6.32 (ALL X16.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c1_1 X16 | ~ bnd_c2_1 X16) | ~ bnd_c3_1 X16)) |
% 6.82/6.32 bnd_hskp7)) &
% 6.82/6.32 ((bnd_hskp35 |
% 6.82/6.32 (ALL X17. bnd_ndr1_0 --> (bnd_c1_1 X17 | bnd_c3_1 X17) | ~ bnd_c0_1 X17)) |
% 6.82/6.32 bnd_hskp8)) &
% 6.82/6.32 (((ALL X18.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c3_1 X18 | ~ bnd_c0_1 X18) | bnd_c1_1 X18) |
% 6.82/6.32 bnd_hskp9) |
% 6.82/6.32 bnd_hskp10)) &
% 6.82/6.32 (((ALL X19.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c0_1 X19 | ~ bnd_c1_1 X19) | bnd_c3_1 X19) |
% 6.82/6.32 bnd_hskp0) |
% 6.82/6.32 (ALL X20.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c1_1 X20 | ~ bnd_c2_1 X20) | bnd_c0_1 X20))) &
% 6.82/6.32 ((bnd_hskp36 |
% 6.82/6.32 (ALL X21.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c0_1 X21 | ~ bnd_c3_1 X21) | ~ bnd_c1_1 X21)) |
% 6.82/6.32 (ALL X22.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c0_1 X22 | ~ bnd_c3_1 X22) | bnd_c1_1 X22))) &
% 6.82/6.32 (((ALL X23.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c0_1 X23 | bnd_c1_1 X23) | ~ bnd_c3_1 X23) |
% 6.82/6.32 (ALL X24.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X24 | ~ bnd_c3_1 X24) | ~ bnd_c0_1 X24)) |
% 6.82/6.32 (ALL X25.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X25 | ~ bnd_c0_1 X25) | bnd_c2_1 X25))) &
% 6.82/6.32 ((bnd_hskp3 | bnd_hskp2) | bnd_hskp37)) &
% 6.82/6.32 (((ALL X26.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X26 | ~ bnd_c2_1 X26) |
% 6.82/6.32 bnd_c1_1 X26) |
% 6.82/6.32 bnd_hskp11) |
% 6.82/6.32 (ALL X27.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X27 | ~ bnd_c3_1 X27) |
% 6.82/6.32 ~ bnd_c0_1 X27))) &
% 6.82/6.32 ((bnd_hskp38 |
% 6.82/6.32 (ALL X28.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c3_1 X28 | ~ bnd_c2_1 X28) |
% 6.82/6.32 bnd_c1_1 X28)) |
% 6.82/6.32 bnd_hskp12)) &
% 6.82/6.32 ((bnd_hskp39 | bnd_hskp40) |
% 6.82/6.32 (ALL X29.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X29 | bnd_c0_1 X29) |
% 6.82/6.32 bnd_c1_1 X29))) &
% 6.82/6.32 ((bnd_hskp13 | bnd_hskp41) |
% 6.82/6.32 (ALL X30.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c1_1 X30 | ~ bnd_c0_1 X30) |
% 6.82/6.32 bnd_c2_1 X30))) &
% 6.82/6.32 (((ALL X31.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X31 | ~ bnd_c3_1 X31) |
% 6.82/6.32 ~ bnd_c2_1 X31) |
% 6.82/6.32 (ALL X32.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X32 | ~ bnd_c2_1 X32) |
% 6.82/6.32 ~ bnd_c1_1 X32)) |
% 6.82/6.32 (ALL X33.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X33 | ~ bnd_c2_1 X33) |
% 6.82/6.32 ~ bnd_c1_1 X33))) &
% 6.82/6.32 ((bnd_hskp42 |
% 6.82/6.32 (ALL X34.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c2_1 X34 | bnd_c0_1 X34) |
% 6.82/6.32 bnd_c3_1 X34)) |
% 6.82/6.32 (ALL X35.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X35 | bnd_c1_1 X35) |
% 6.82/6.32 bnd_c3_1 X35))) &
% 6.82/6.32 (((ALL X36.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X36 | ~ bnd_c1_1 X36) |
% 6.82/6.32 ~ bnd_c2_1 X36) |
% 6.82/6.32 bnd_hskp43) |
% 6.82/6.32 (ALL X37.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X37 | ~ bnd_c2_1 X37) |
% 6.82/6.32 bnd_c1_1 X37))) &
% 6.82/6.32 ((bnd_hskp14 |
% 6.82/6.32 (ALL X38.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X38 | bnd_c0_1 X38) |
% 6.82/6.32 bnd_c1_1 X38)) |
% 6.82/6.32 (ALL X39.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X39 | ~ bnd_c3_1 X39) |
% 6.82/6.32 bnd_c1_1 X39))) &
% 6.82/6.32 ((bnd_hskp44 |
% 6.82/6.32 (ALL X40.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X40 | ~ bnd_c0_1 X40) |
% 6.82/6.32 bnd_c1_1 X40)) |
% 6.82/6.32 (ALL X41.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X41 | ~ bnd_c1_1 X41) |
% 6.82/6.32 bnd_c2_1 X41))) &
% 6.82/6.32 (((ALL X42.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X42 | ~ bnd_c2_1 X42) |
% 6.82/6.32 ~ bnd_c1_1 X42) |
% 6.82/6.32 bnd_hskp45) |
% 6.82/6.32 bnd_hskp15)) &
% 6.82/6.32 (((ALL X43.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X43 | bnd_c3_1 X43) | ~ bnd_c0_1 X43) |
% 6.82/6.32 bnd_hskp16) |
% 6.82/6.32 (ALL X44.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X44 | ~ bnd_c2_1 X44) |
% 6.82/6.32 bnd_c3_1 X44))) &
% 6.82/6.32 (((ALL X45.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X45 | ~ bnd_c1_1 X45) | bnd_c3_1 X45) |
% 6.82/6.32 (ALL X46.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X46 | bnd_c1_1 X46) | ~ bnd_c0_1 X46)) |
% 6.82/6.32 bnd_hskp37)) &
% 6.82/6.32 ((bnd_hskp17 | bnd_hskp18) |
% 6.82/6.32 (ALL X47.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c3_1 X47 | ~ bnd_c2_1 X47) |
% 6.82/6.32 ~ bnd_c1_1 X47))) &
% 6.82/6.32 (((ALL X48.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X48 | bnd_c3_1 X48) | ~ bnd_c1_1 X48) |
% 6.82/6.32 (ALL X49.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c2_1 X49 | ~ bnd_c0_1 X49) |
% 6.82/6.32 ~ bnd_c3_1 X49)) |
% 6.82/6.32 bnd_hskp19)) &
% 6.82/6.32 (((ALL X50.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c1_1 X50 | bnd_c0_1 X50) | ~ bnd_c2_1 X50) |
% 6.82/6.32 bnd_hskp46) |
% 6.82/6.32 (ALL X51.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X51 | ~ bnd_c1_1 X51) | bnd_c2_1 X51))) &
% 6.82/6.32 ((bnd_hskp11 |
% 6.82/6.32 (ALL X52.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c1_1 X52 | bnd_c2_1 X52) | ~ bnd_c3_1 X52)) |
% 6.82/6.32 bnd_hskp20)) &
% 6.82/6.32 ((bnd_hskp47 |
% 6.82/6.32 (ALL X53.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X53 | ~ bnd_c1_1 X53) | ~ bnd_c3_1 X53)) |
% 6.82/6.32 bnd_hskp21)) &
% 6.82/6.32 ((bnd_hskp22 |
% 6.82/6.32 (ALL X54.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X54 | bnd_c2_1 X54) | ~ bnd_c3_1 X54)) |
% 6.82/6.32 bnd_hskp23)) &
% 6.82/6.32 ((bnd_hskp36 |
% 6.82/6.32 (ALL X55.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c1_1 X55 | ~ bnd_c3_1 X55) | bnd_c0_1 X55)) |
% 6.82/6.32 (ALL X56.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c3_1 X56 | bnd_c1_1 X56) | ~ bnd_c2_1 X56))) &
% 6.82/6.32 (((ALL X57.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c3_1 X57 | bnd_c0_1 X57) | ~ bnd_c2_1 X57) |
% 6.82/6.32 (ALL X58.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c3_1 X58 | bnd_c2_1 X58) | ~ bnd_c1_1 X58)) |
% 6.82/6.32 (ALL X59.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c0_1 X59 | bnd_c3_1 X59) | bnd_c1_1 X59))) &
% 6.82/6.32 ((bnd_hskp24 | bnd_hskp48) | bnd_hskp46)) &
% 6.82/6.32 ((bnd_hskp40 |
% 6.82/6.32 (ALL X60.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c1_1 X60 | ~ bnd_c2_1 X60) | ~ bnd_c0_1 X60)) |
% 6.82/6.32 (ALL X61.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X61 | bnd_c3_1 X61) | bnd_c1_1 X61))) &
% 6.82/6.32 (((ALL X62.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X62 | bnd_c3_1 X62) | ~ bnd_c0_1 X62) |
% 6.82/6.32 (ALL X63.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c0_1 X63 | ~ bnd_c2_1 X63) | ~ bnd_c1_1 X63)) |
% 6.82/6.32 (ALL X64.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c2_1 X64 | bnd_c0_1 X64) | ~ bnd_c3_1 X64))) &
% 6.82/6.32 (((ALL X65.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X65 | ~ bnd_c1_1 X65) | ~ bnd_c3_1 X65) |
% 6.82/6.32 bnd_hskp11) |
% 6.82/6.32 bnd_hskp49)) &
% 6.82/6.32 (((ALL X66.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X66 | ~ bnd_c1_1 X66) | ~ bnd_c0_1 X66) |
% 6.82/6.32 (ALL X67.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (bnd_c2_1 X67 | ~ bnd_c3_1 X67) | ~ bnd_c1_1 X67)) |
% 6.82/6.32 (ALL X68.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c2_1 X68 | bnd_c1_1 X68) | bnd_c0_1 X68))) &
% 6.82/6.32 (((ALL X69.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X69 | bnd_c2_1 X69) | ~ bnd_c3_1 X69) |
% 6.82/6.32 (ALL X70.
% 6.82/6.32 bnd_ndr1_0 -->
% 6.82/6.32 (~ bnd_c1_1 X70 | bnd_c2_1 X70) | bnd_c3_1 X70)) |
% 6.82/6.32 (ALL X71.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c3_1 X71 | bnd_c1_1 X71) | bnd_c2_1 X71))) &
% 6.82/6.32 (((ALL X72.
% 6.82/6.32 bnd_ndr1_0 --> (bnd_c1_1 X72 | bnd_c0_1 X72) | bnd_c2_1 X72) |
% 6.82/6.32 bnd_hskp25) |
% 6.82/6.32 bnd_hskp26)) &
% 6.82/6.32 ((bnd_hskp50 | bnd_hskp17) | bnd_hskp51)) &
% 6.82/6.32 ((bnd_hskp34 |
% 6.82/6.32 (ALL X73.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c1_1 X73 | bnd_c0_1 X73) | ~ bnd_c2_1 X73)) |
% 6.82/6.32 (ALL X74.
% 6.82/6.32 bnd_ndr1_0 --> (~ bnd_c0_1 X74 | ~ bnd_c2_1 X74) | bnd_c1_1 X74)))
% 10.62/10.13 Unfolded term: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~ bnd_hskp0 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a402) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a402) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a402) &
% 10.62/10.13 (~ bnd_hskp1 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a403) &
% 10.62/10.13 bnd_c3_1 bnd_a403) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a403)) &
% 10.62/10.13 (~ bnd_hskp2 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a405) &
% 10.62/10.13 bnd_c0_1 bnd_a405) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a405)) &
% 10.62/10.13 (~ bnd_hskp3 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a407) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a407) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a407)) &
% 10.62/10.13 (~ bnd_hskp4 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a411) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a411) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a411)) &
% 10.62/10.13 (~ bnd_hskp5 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a413) &
% 10.62/10.13 bnd_c0_1 bnd_a413) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a413)) &
% 10.62/10.13 (~ bnd_hskp6 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a416) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a416) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a416)) &
% 10.62/10.13 (~ bnd_hskp7 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a418) &
% 10.62/10.13 bnd_c1_1 bnd_a418) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a418)) &
% 10.62/10.13 (~ bnd_hskp8 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a420) &
% 10.62/10.13 bnd_c1_1 bnd_a420) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a420)) &
% 10.62/10.13 (~ bnd_hskp9 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c3_1 bnd_a421) & bnd_c2_1 bnd_a421) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a421)) &
% 10.62/10.13 (~ bnd_hskp10 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a422) & bnd_c0_1 bnd_a422) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a422)) &
% 10.62/10.13 (~ bnd_hskp11 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a428) & ~ bnd_c1_1 bnd_a428) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a428)) &
% 10.62/10.13 (~ bnd_hskp12 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a430) & bnd_c3_1 bnd_a430) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a430)) &
% 10.62/10.13 (~ bnd_hskp13 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a433) & ~ bnd_c3_1 bnd_a433) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a433)) &
% 10.62/10.13 (~ bnd_hskp14 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a437) & ~ bnd_c1_1 bnd_a437) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a437)) &
% 10.62/10.13 (~ bnd_hskp15 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a440) & bnd_c0_1 bnd_a440) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a440)) &
% 10.62/10.13 (~ bnd_hskp16 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a441) & bnd_c1_1 bnd_a441) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a441)) &
% 10.62/10.13 (~ bnd_hskp17 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a443) & ~ bnd_c1_1 bnd_a443) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a443)) &
% 10.62/10.13 (~ bnd_hskp18 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a444) & bnd_c0_1 bnd_a444) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a444)) &
% 10.62/10.13 (~ bnd_hskp19 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a445) & bnd_c0_1 bnd_a445) &
% 10.62/10.13 ~ bnd_c1_1 bnd_a445)) &
% 10.62/10.13 (~ bnd_hskp20 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a448) & ~ bnd_c1_1 bnd_a448) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a448)) &
% 10.62/10.13 (~ bnd_hskp21 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a450) & bnd_c3_1 bnd_a450) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a450)) &
% 10.62/10.13 (~ bnd_hskp22 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a451) & ~ bnd_c3_1 bnd_a451) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a451)) &
% 10.62/10.13 (~ bnd_hskp23 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a452) & bnd_c3_1 bnd_a452) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a452)) &
% 10.62/10.13 (~ bnd_hskp24 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c0_1 bnd_a454) & ~ bnd_c3_1 bnd_a454) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a454)) &
% 10.62/10.13 (~ bnd_hskp25 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a460) & bnd_c2_1 bnd_a460) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a460)) &
% 10.62/10.13 (~ bnd_hskp26 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a461) & bnd_c3_1 bnd_a461) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a461)) &
% 10.62/10.13 (~ bnd_hskp27 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a404) & ~ bnd_c2_1 bnd_a404) &
% 10.62/10.13 bnd_c1_1 bnd_a404)) &
% 10.62/10.13 (~ bnd_hskp28 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a408) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a408) &
% 10.62/10.13 bnd_c2_1 bnd_a408)) &
% 10.62/10.13 (~ bnd_hskp29 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a409) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a409) &
% 10.62/10.13 bnd_c0_1 bnd_a409)) &
% 10.62/10.13 (~ bnd_hskp30 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a410) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a410) &
% 10.62/10.13 bnd_c1_1 bnd_a410)) &
% 10.62/10.13 (~ bnd_hskp31 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a412) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a412) &
% 10.62/10.13 bnd_c0_1 bnd_a412)) &
% 10.62/10.13 (~ bnd_hskp32 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c3_1 bnd_a414) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a414) &
% 10.62/10.13 bnd_c1_1 bnd_a414)) &
% 10.62/10.13 (~ bnd_hskp33 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a415) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a415) &
% 10.62/10.13 bnd_c0_1 bnd_a415)) &
% 10.62/10.13 (~ bnd_hskp34 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a417) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a417) &
% 10.62/10.13 bnd_c2_1 bnd_a417)) &
% 10.62/10.13 (~ bnd_hskp35 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a419) &
% 10.62/10.13 bnd_c1_1 bnd_a419) &
% 10.62/10.13 bnd_c3_1 bnd_a419)) &
% 10.62/10.13 (~ bnd_hskp36 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a424) &
% 10.62/10.13 bnd_c3_1 bnd_a424) &
% 10.62/10.13 bnd_c2_1 bnd_a424)) &
% 10.62/10.13 (~ bnd_hskp37 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a427) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a427) &
% 10.62/10.13 bnd_c3_1 bnd_a427)) &
% 10.62/10.13 (~ bnd_hskp38 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a429) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a429) &
% 10.62/10.13 bnd_c1_1 bnd_a429)) &
% 10.62/10.13 (~ bnd_hskp39 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c3_1 bnd_a431) &
% 10.62/10.13 bnd_c1_1 bnd_a431) &
% 10.62/10.13 bnd_c2_1 bnd_a431)) &
% 10.62/10.13 (~ bnd_hskp40 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a432) &
% 10.62/10.13 bnd_c1_1 bnd_a432) &
% 10.62/10.13 bnd_c2_1 bnd_a432)) &
% 10.62/10.13 (~ bnd_hskp41 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c0_1 bnd_a434) &
% 10.62/10.13 bnd_c1_1 bnd_a434) &
% 10.62/10.13 bnd_c3_1 bnd_a434)) &
% 10.62/10.13 (~ bnd_hskp42 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a435) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a435) &
% 10.62/10.13 bnd_c0_1 bnd_a435)) &
% 10.62/10.13 (~ bnd_hskp43 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c2_1 bnd_a436) &
% 10.62/10.13 ~ bnd_c0_1 bnd_a436) &
% 10.62/10.13 bnd_c3_1 bnd_a436)) &
% 10.62/10.13 (~ bnd_hskp44 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c0_1 bnd_a438) &
% 10.62/10.13 bnd_c1_1 bnd_a438) &
% 10.62/10.13 bnd_c2_1 bnd_a438)) &
% 10.62/10.13 (~ bnd_hskp45 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c3_1 bnd_a439) &
% 10.62/10.13 ~ bnd_c2_1 bnd_a439) &
% 10.62/10.13 bnd_c0_1 bnd_a439)) &
% 10.62/10.13 (~ bnd_hskp46 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a446) &
% 10.62/10.13 ~ bnd_c3_1 bnd_a446) &
% 10.62/10.13 bnd_c1_1 bnd_a446)) &
% 10.62/10.13 (~ bnd_hskp47 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c0_1 bnd_a449) & ~ bnd_c3_1 bnd_a449) &
% 10.62/10.13 bnd_c1_1 bnd_a449)) &
% 10.62/10.13 (~ bnd_hskp48 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c3_1 bnd_a455) & bnd_c2_1 bnd_a455) &
% 10.62/10.13 bnd_c1_1 bnd_a455)) &
% 10.62/10.13 (~ bnd_hskp49 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a459) & ~ bnd_c1_1 bnd_a459) &
% 10.62/10.13 bnd_c0_1 bnd_a459)) &
% 10.62/10.13 (~ bnd_hskp50 |
% 10.62/10.13 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a462) & bnd_c3_1 bnd_a462) &
% 10.62/10.13 bnd_c0_1 bnd_a462)) &
% 10.62/10.13 (~ bnd_hskp51 |
% 10.62/10.13 ((bnd_ndr1_0 & bnd_c1_1 bnd_a464) & ~ bnd_c2_1 bnd_a464) &
% 10.62/10.13 bnd_c0_1 bnd_a464)) &
% 10.62/10.13 (((ALL U.
% 10.62/10.13 bnd_ndr1_0 -->
% 10.62/10.13 (~ bnd_c2_1 U | bnd_c0_1 U) | ~ bnd_c3_1 U) |
% 10.62/10.13 bnd_hskp0) |
% 10.62/10.13 (ALL V.
% 10.62/10.13 bnd_ndr1_0 -->
% 10.62/10.13 (bnd_c1_1 V | bnd_c2_1 V) | ~ bnd_c0_1 V))) &
% 10.62/10.13 (((ALL W.
% 10.62/10.13 bnd_ndr1_0 -->
% 10.62/10.13 (~ bnd_c1_1 W | ~ bnd_c0_1 W) | ~ bnd_c2_1 W) |
% 10.62/10.13 (ALL X.
% 10.62/10.13 bnd_ndr1_0 -->
% 10.62/10.13 (bnd_c1_1 X | ~ bnd_c3_1 X) | ~ bnd_c2_1 X)) |
% 10.62/10.13 bnd_hskp1)) &
% 10.62/10.13 ((bnd_hskp27 | bnd_hskp2) |
% 10.62/10.13 (ALL Y.
% 10.62/10.13 bnd_ndr1_0 -->
% 10.62/10.13 (~ bnd_c2_1 Y | ~ bnd_c1_1 Y) | bnd_c3_1 Y))) &
% 10.62/10.13 ((bnd_hskp1 | bnd_hskp3) | bnd_hskp28)) &
% 10.62/10.13 ((bnd_hskp29 |
% 10.62/10.13 (ALL Z.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c0_1 Z | ~ bnd_c3_1 Z) | bnd_c1_1 Z)) |
% 10.62/10.13 bnd_hskp30)) &
% 10.62/10.13 (((ALL X1.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c3_1 X1 | bnd_c1_1 X1) | ~ bnd_c2_1 X1) |
% 10.62/10.13 (ALL X2.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c1_1 X2 | ~ bnd_c3_1 X2) | bnd_c2_1 X2)) |
% 10.62/10.13 bnd_hskp4)) &
% 10.62/10.13 (((ALL X3.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c0_1 X3 | bnd_c3_1 X3) | ~ bnd_c1_1 X3) |
% 10.62/10.13 bnd_hskp31) |
% 10.62/10.13 (ALL X4.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c0_1 X4 | ~ bnd_c2_1 X4) | bnd_c1_1 X4))) &
% 10.62/10.13 (((ALL X5.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c1_1 X5 | ~ bnd_c3_1 X5) | ~ bnd_c0_1 X5) |
% 10.62/10.13 bnd_hskp5) |
% 10.62/10.13 (ALL X6.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c2_1 X6 | bnd_c1_1 X6) | ~ bnd_c0_1 X6))) &
% 10.62/10.13 (((ALL X7. bnd_ndr1_0 --> (~ bnd_c1_1 X7 | bnd_c0_1 X7) | bnd_c3_1 X7) |
% 10.62/10.13 (ALL X8.
% 10.62/10.13 bnd_ndr1_0 --> (bnd_c3_1 X8 | ~ bnd_c0_1 X8) | ~ bnd_c1_1 X8)) |
% 10.62/10.13 bnd_hskp32)) &
% 10.62/10.13 ((bnd_hskp33 |
% 10.62/10.13 (ALL X9. bnd_ndr1_0 --> (~ bnd_c2_1 X9 | bnd_c0_1 X9) | bnd_c1_1 X9)) |
% 10.62/10.13 bnd_hskp6)) &
% 10.62/10.13 ((bnd_hskp34 |
% 10.62/10.13 (ALL X10.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c2_1 X10 | ~ bnd_c0_1 X10) | bnd_c3_1 X10)) |
% 10.62/10.13 (ALL X11.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c2_1 X11 | ~ bnd_c1_1 X11) | bnd_c0_1 X11))) &
% 10.62/10.13 (((ALL X12.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c3_1 X12 | ~ bnd_c2_1 X12) | bnd_c0_1 X12) |
% 10.62/10.13 (ALL X13.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c1_1 X13 | ~ bnd_c0_1 X13) | ~ bnd_c3_1 X13)) |
% 10.62/10.13 (ALL X14.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c1_1 X14 | ~ bnd_c3_1 X14) | bnd_c2_1 X14))) &
% 10.62/10.13 (((ALL X15.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c0_1 X15 | ~ bnd_c1_1 X15) | ~ bnd_c3_1 X15) |
% 10.62/10.13 (ALL X16.
% 10.62/10.13 bnd_ndr1_0 --> (~ bnd_c1_1 X16 | ~ bnd_c2_1 X16) | ~ bnd_c3_1 X16)) |
% 10.62/10.14 bnd_hskp7)) &
% 10.62/10.14 ((bnd_hskp35 |
% 10.62/10.14 (ALL X17. bnd_ndr1_0 --> (bnd_c1_1 X17 | bnd_c3_1 X17) | ~ bnd_c0_1 X17)) |
% 10.62/10.14 bnd_hskp8)) &
% 10.62/10.14 (((ALL X18.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c3_1 X18 | ~ bnd_c0_1 X18) | bnd_c1_1 X18) |
% 10.62/10.14 bnd_hskp9) |
% 10.62/10.14 bnd_hskp10)) &
% 10.62/10.14 (((ALL X19.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c0_1 X19 | ~ bnd_c1_1 X19) | bnd_c3_1 X19) |
% 10.62/10.14 bnd_hskp0) |
% 10.62/10.14 (ALL X20.
% 10.62/10.14 bnd_ndr1_0 --> (~ bnd_c1_1 X20 | ~ bnd_c2_1 X20) | bnd_c0_1 X20))) &
% 10.62/10.14 ((bnd_hskp36 |
% 10.62/10.14 (ALL X21.
% 10.62/10.14 bnd_ndr1_0 --> (~ bnd_c0_1 X21 | ~ bnd_c3_1 X21) | ~ bnd_c1_1 X21)) |
% 10.62/10.14 (ALL X22.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c0_1 X22 | ~ bnd_c3_1 X22) | bnd_c1_1 X22))) &
% 10.62/10.14 (((ALL X23.
% 10.62/10.14 bnd_ndr1_0 --> (~ bnd_c0_1 X23 | bnd_c1_1 X23) | ~ bnd_c3_1 X23) |
% 10.62/10.14 (ALL X24.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c1_1 X24 | ~ bnd_c3_1 X24) | ~ bnd_c0_1 X24)) |
% 10.62/10.14 (ALL X25.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c1_1 X25 | ~ bnd_c0_1 X25) | bnd_c2_1 X25))) &
% 10.62/10.14 ((bnd_hskp3 | bnd_hskp2) | bnd_hskp37)) &
% 10.62/10.14 (((ALL X26.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X26 | ~ bnd_c2_1 X26) |
% 10.62/10.14 bnd_c1_1 X26) |
% 10.62/10.14 bnd_hskp11) |
% 10.62/10.14 (ALL X27.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X27 | ~ bnd_c3_1 X27) |
% 10.62/10.14 ~ bnd_c0_1 X27))) &
% 10.62/10.14 ((bnd_hskp38 |
% 10.62/10.14 (ALL X28.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c3_1 X28 | ~ bnd_c2_1 X28) |
% 10.62/10.14 bnd_c1_1 X28)) |
% 10.62/10.14 bnd_hskp12)) &
% 10.62/10.14 ((bnd_hskp39 | bnd_hskp40) |
% 10.62/10.14 (ALL X29.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X29 | bnd_c0_1 X29) |
% 10.62/10.14 bnd_c1_1 X29))) &
% 10.62/10.14 ((bnd_hskp13 | bnd_hskp41) |
% 10.62/10.14 (ALL X30.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c1_1 X30 | ~ bnd_c0_1 X30) |
% 10.62/10.14 bnd_c2_1 X30))) &
% 10.62/10.14 (((ALL X31.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X31 | ~ bnd_c3_1 X31) |
% 10.62/10.14 ~ bnd_c2_1 X31) |
% 10.62/10.14 (ALL X32.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X32 | ~ bnd_c2_1 X32) |
% 10.62/10.14 ~ bnd_c1_1 X32)) |
% 10.62/10.14 (ALL X33.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X33 | ~ bnd_c2_1 X33) |
% 10.62/10.14 ~ bnd_c1_1 X33))) &
% 10.62/10.14 ((bnd_hskp42 |
% 10.62/10.14 (ALL X34.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c2_1 X34 | bnd_c0_1 X34) |
% 10.62/10.14 bnd_c3_1 X34)) |
% 10.62/10.14 (ALL X35.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X35 | bnd_c1_1 X35) |
% 10.62/10.14 bnd_c3_1 X35))) &
% 10.62/10.14 (((ALL X36.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X36 | ~ bnd_c1_1 X36) |
% 10.62/10.14 ~ bnd_c2_1 X36) |
% 10.62/10.14 bnd_hskp43) |
% 10.62/10.14 (ALL X37.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X37 | ~ bnd_c2_1 X37) |
% 10.62/10.14 bnd_c1_1 X37))) &
% 10.62/10.14 ((bnd_hskp14 |
% 10.62/10.14 (ALL X38.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X38 | bnd_c0_1 X38) |
% 10.62/10.14 bnd_c1_1 X38)) |
% 10.62/10.14 (ALL X39.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X39 | ~ bnd_c3_1 X39) |
% 10.62/10.14 bnd_c1_1 X39))) &
% 10.62/10.14 ((bnd_hskp44 |
% 10.62/10.14 (ALL X40.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X40 | ~ bnd_c0_1 X40) |
% 10.62/10.14 bnd_c1_1 X40)) |
% 10.62/10.14 (ALL X41.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X41 | ~ bnd_c1_1 X41) |
% 10.62/10.14 bnd_c2_1 X41))) &
% 10.62/10.14 (((ALL X42.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X42 | ~ bnd_c2_1 X42) |
% 10.62/10.14 ~ bnd_c1_1 X42) |
% 10.62/10.14 bnd_hskp45) |
% 10.62/10.14 bnd_hskp15)) &
% 10.62/10.14 (((ALL X43.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X43 | bnd_c3_1 X43) | ~ bnd_c0_1 X43) |
% 10.62/10.14 bnd_hskp16) |
% 10.62/10.14 (ALL X44.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X44 | ~ bnd_c2_1 X44) |
% 10.62/10.14 bnd_c3_1 X44))) &
% 10.62/10.14 (((ALL X45.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X45 | ~ bnd_c1_1 X45) | bnd_c3_1 X45) |
% 10.62/10.14 (ALL X46.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X46 | bnd_c1_1 X46) | ~ bnd_c0_1 X46)) |
% 10.62/10.14 bnd_hskp37)) &
% 10.62/10.14 ((bnd_hskp17 | bnd_hskp18) |
% 10.62/10.14 (ALL X47.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c3_1 X47 | ~ bnd_c2_1 X47) |
% 10.62/10.14 ~ bnd_c1_1 X47))) &
% 10.62/10.14 (((ALL X48.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X48 | bnd_c3_1 X48) | ~ bnd_c1_1 X48) |
% 10.62/10.14 (ALL X49.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c2_1 X49 | ~ bnd_c0_1 X49) |
% 10.62/10.14 ~ bnd_c3_1 X49)) |
% 10.62/10.14 bnd_hskp19)) &
% 10.62/10.14 (((ALL X50.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c1_1 X50 | bnd_c0_1 X50) | ~ bnd_c2_1 X50) |
% 10.62/10.14 bnd_hskp46) |
% 10.62/10.14 (ALL X51.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X51 | ~ bnd_c1_1 X51) | bnd_c2_1 X51))) &
% 10.62/10.14 ((bnd_hskp11 |
% 10.62/10.14 (ALL X52.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c1_1 X52 | bnd_c2_1 X52) | ~ bnd_c3_1 X52)) |
% 10.62/10.14 bnd_hskp20)) &
% 10.62/10.14 ((bnd_hskp47 |
% 10.62/10.14 (ALL X53.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X53 | ~ bnd_c1_1 X53) | ~ bnd_c3_1 X53)) |
% 10.62/10.14 bnd_hskp21)) &
% 10.62/10.14 ((bnd_hskp22 |
% 10.62/10.14 (ALL X54.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X54 | bnd_c2_1 X54) | ~ bnd_c3_1 X54)) |
% 10.62/10.14 bnd_hskp23)) &
% 10.62/10.14 ((bnd_hskp36 |
% 10.62/10.14 (ALL X55.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c1_1 X55 | ~ bnd_c3_1 X55) | bnd_c0_1 X55)) |
% 10.62/10.14 (ALL X56.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c3_1 X56 | bnd_c1_1 X56) | ~ bnd_c2_1 X56))) &
% 10.62/10.14 (((ALL X57.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c3_1 X57 | bnd_c0_1 X57) | ~ bnd_c2_1 X57) |
% 10.62/10.14 (ALL X58.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c3_1 X58 | bnd_c2_1 X58) | ~ bnd_c1_1 X58)) |
% 10.62/10.14 (ALL X59.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c0_1 X59 | bnd_c3_1 X59) | bnd_c1_1 X59))) &
% 10.62/10.14 ((bnd_hskp24 | bnd_hskp48) | bnd_hskp46)) &
% 10.62/10.14 ((bnd_hskp40 |
% 10.62/10.14 (ALL X60.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c1_1 X60 | ~ bnd_c2_1 X60) | ~ bnd_c0_1 X60)) |
% 10.62/10.14 (ALL X61.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X61 | bnd_c3_1 X61) | bnd_c1_1 X61))) &
% 10.62/10.14 (((ALL X62.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X62 | bnd_c3_1 X62) | ~ bnd_c0_1 X62) |
% 10.62/10.14 (ALL X63.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c0_1 X63 | ~ bnd_c2_1 X63) | ~ bnd_c1_1 X63)) |
% 10.62/10.14 (ALL X64.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c2_1 X64 | bnd_c0_1 X64) | ~ bnd_c3_1 X64))) &
% 10.62/10.14 (((ALL X65.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X65 | ~ bnd_c1_1 X65) | ~ bnd_c3_1 X65) |
% 10.62/10.14 bnd_hskp11) |
% 10.62/10.14 bnd_hskp49)) &
% 10.62/10.14 (((ALL X66.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X66 | ~ bnd_c1_1 X66) | ~ bnd_c0_1 X66) |
% 10.62/10.14 (ALL X67.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (bnd_c2_1 X67 | ~ bnd_c3_1 X67) | ~ bnd_c1_1 X67)) |
% 10.62/10.14 (ALL X68.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c2_1 X68 | bnd_c1_1 X68) | bnd_c0_1 X68))) &
% 10.62/10.14 (((ALL X69.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c1_1 X69 | bnd_c2_1 X69) | ~ bnd_c3_1 X69) |
% 10.62/10.14 (ALL X70.
% 10.62/10.14 bnd_ndr1_0 -->
% 10.62/10.14 (~ bnd_c1_1 X70 | bnd_c2_1 X70) | bnd_c3_1 X70)) |
% 10.62/10.14 (ALL X71.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c3_1 X71 | bnd_c1_1 X71) | bnd_c2_1 X71))) &
% 10.62/10.14 (((ALL X72.
% 10.62/10.14 bnd_ndr1_0 --> (bnd_c1_1 X72 | bnd_c0_1 X72) | bnd_c2_1 X72) |
% 10.62/10.14 bnd_hskp25) |
% 10.62/10.14 bnd_hskp26)) &
% 10.62/10.14 ((bnd_hskp50 | bnd_hskp17) | bnd_hskp51)) &
% 10.62/10.14 ((bnd_hskp34 |
% 10.62/10.14 (ALL X73.
% 10.62/10.14 bnd_ndr1_0 --> (~ bnd_c1_1 X73 | bnd_c0_1 X73) | ~ bnd_c2_1 X73)) |
% 10.62/10.14 (ALL X74.
% 10.62/10.14 bnd_ndr1_0 --> (~ bnd_c0_1 X74 | ~ bnd_c2_1 X74) | bnd_c1_1 X74)))
% 10.62/10.14 Adding axioms...
% 10.62/10.16 Typedef.type_definition_def
% 20.43/19.92 ...done.
% 20.43/19.93 Ground types: ?'b, TPTP_Interpret.ind
% 20.43/19.93 Translating term (sizes: 1, 1) ...
% 30.75/30.25 Invoking SAT solver...
% 30.75/30.25 No model exists.
% 30.75/30.25 Translating term (sizes: 2, 1) ...
% 41.88/41.30 Invoking SAT solver...
% 41.88/41.30 No model exists.
% 41.88/41.30 Translating term (sizes: 1, 2) ...
% 56.73/56.13 Invoking SAT solver...
% 57.22/56.62 Model found:
% 57.22/56.62 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 57.22/56.62 bnd_a464: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp51: False
% 57.22/56.62 bnd_a462: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp50: False
% 57.22/56.62 bnd_a459: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp49: False
% 57.22/56.62 bnd_a455: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp48: True
% 57.22/56.62 bnd_a449: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp47: False
% 57.22/56.62 bnd_a446: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp46: False
% 57.22/56.62 bnd_a439: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp45: False
% 57.22/56.62 bnd_a438: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp44: False
% 57.22/56.62 bnd_a436: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp43: False
% 57.22/56.62 bnd_a435: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp42: False
% 57.22/56.62 bnd_a434: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp41: False
% 57.22/56.62 bnd_a432: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp40: False
% 57.22/56.62 bnd_a431: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp39: True
% 57.22/56.62 bnd_a429: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp38: False
% 57.22/56.62 bnd_a427: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp37: False
% 57.22/56.62 bnd_a424: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp36: False
% 57.22/56.62 bnd_a419: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp35: False
% 57.22/56.62 bnd_a417: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp34: False
% 57.22/56.62 bnd_a415: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp33: False
% 57.22/56.62 bnd_a414: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp32: False
% 57.22/56.62 bnd_a412: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp31: False
% 57.22/56.62 bnd_a410: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp30: False
% 57.22/56.62 bnd_a409: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp29: False
% 57.22/56.62 bnd_a408: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp28: False
% 57.22/56.62 bnd_a404: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp27: False
% 57.22/56.62 bnd_a461: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp26: False
% 57.22/56.62 bnd_a460: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp25: False
% 57.22/56.62 bnd_a454: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp24: False
% 57.22/56.62 bnd_a452: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp23: False
% 57.22/56.62 bnd_a451: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp22: False
% 57.22/56.62 bnd_a450: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp21: False
% 57.22/56.62 bnd_a448: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp20: False
% 57.22/56.62 bnd_a445: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp19: False
% 57.22/56.62 bnd_a444: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp18: False
% 57.22/56.62 bnd_a443: ??.TPTP_Interpret.ind1
% 57.22/56.62 bnd_hskp17: True
% 57.22/56.62 bnd_a441: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp16: False
% 57.22/56.62 bnd_a440: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp15: False
% 57.22/56.62 bnd_a437: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp14: False
% 57.22/56.62 bnd_a433: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp13: False
% 57.22/56.62 bnd_a430: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp12: False
% 57.22/56.62 bnd_a428: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp11: False
% 57.22/56.62 bnd_a422: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp10: False
% 57.22/56.62 bnd_a421: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp9: False
% 57.22/56.62 bnd_a420: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp8: False
% 57.22/56.62 bnd_a418: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp7: False
% 57.22/56.62 bnd_a416: ??.TPTP_Interpret.ind1
% 57.22/56.62 bnd_hskp6: True
% 57.22/56.62 bnd_a413: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp5: False
% 57.22/56.62 bnd_a411: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp4: False
% 57.22/56.62 bnd_a407: ??.TPTP_Interpret.ind1
% 57.22/56.62 bnd_hskp3: True
% 57.22/56.62 bnd_c0_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}
% 57.22/56.62 bnd_a405: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp2: False
% 57.22/56.62 bnd_a403: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_hskp1: False
% 57.22/56.62 bnd_c1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 57.22/56.62 bnd_c2_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 57.22/56.62 bnd_a402: ??.TPTP_Interpret.ind0
% 57.22/56.62 bnd_c3_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 57.22/56.62 bnd_ndr1_0: True
% 57.22/56.62 bnd_hskp0: False
% 57.22/56.62
% 57.22/56.62 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------