%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : SWV484+2 : TPTP v6.4.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n068.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 05:29:00 EDT 2016 % Result : GaveUp 179.74s % Output : None % 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 : SWV484+2 : TPTP v6.4.0. Released v4.0.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.22 % Computer : n068.star.cs.uiowa.edu % 0.03/0.22 % Model : x86_64 x86_64 % 0.03/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.22 % Memory : 32218.75MB % 0.03/0.22 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.22 % CPULimit : 300 % 0.03/0.22 % DateTime : Fri Apr 8 15:49:54 CDT 2016 % 0.03/0.22 % CPUTime : % 6.29/5.84 > val it = (): unit % 6.69/6.26 Trying to find a model that refutes: EX A B C D X1 E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1. % 6.69/6.26 bnd_p F1 E1 D1 C1 B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E % 6.69/6.26 bnd_n1 X1 D C B A % 11.00/10.54 Unfolded term: [| ALL X33 X32 X31 X30 X29 X28 X27 X26 X25 X24 X23 X22 X21 X20 X19 X18 X17 % 11.00/10.54 X16 X15 X14 X13 X12 X11 X10 X9 X8 X7 X6 X5 X4 X3 X2 X1 X0. % 11.00/10.54 bnd_p X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 % 11.00/10.54 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27 X28 X29 X30 X31 X32 X33 --> % 11.00/10.54 ((((((((((((((((((((((((((((((((~ (X0 = bnd_n1) = (X0 = bnd_n0) & % 11.00/10.54 ~ (X1 = bnd_n1) = (X1 = bnd_n0)) & % 11.00/10.54 ~ (X2 = bnd_n1) = (X2 = bnd_n0)) & % 11.00/10.54 ~ (X3 = bnd_n1) = (X3 = bnd_n0)) & % 11.00/10.54 ~ (X4 = bnd_n1) = (X4 = bnd_n0)) & % 11.00/10.54 ~ (X5 = bnd_n1) = (X5 = bnd_n0)) & % 11.00/10.54 ~ (X6 = bnd_n1) = (X6 = bnd_n0)) & % 11.00/10.54 ~ (X7 = bnd_n1) = (X7 = bnd_n0)) & % 11.00/10.54 ~ (X8 = bnd_n1) = (X8 = bnd_n0)) & % 11.00/10.54 ~ (X9 = bnd_n1) = (X9 = bnd_n0)) & % 11.00/10.54 ~ (X10 = bnd_n1) = (X10 = bnd_n0)) & % 11.00/10.54 ~ (X11 = bnd_n1) = (X11 = bnd_n0)) & % 11.00/10.54 ~ (X12 = bnd_n1) = (X12 = bnd_n0)) & % 11.00/10.54 ~ (X13 = bnd_n1) = (X13 = bnd_n0)) & % 11.00/10.54 ~ (X14 = bnd_n1) = (X14 = bnd_n0)) & % 11.00/10.54 ~ (X15 = bnd_n1) = (X15 = bnd_n0)) & % 11.00/10.54 ~ (X16 = bnd_n1) = (X16 = bnd_n0)) & % 11.00/10.54 ~ (X17 = bnd_n1) = (X17 = bnd_n0)) & % 11.00/10.54 ~ (X18 = bnd_n1) = (X18 = bnd_n0)) & % 11.00/10.54 ~ (X19 = bnd_n1) = (X19 = bnd_n0)) & % 11.00/10.54 ~ (X20 = bnd_n1) = (X20 = bnd_n0)) & % 11.00/10.54 ~ (X21 = bnd_n1) = (X21 = bnd_n0)) & % 11.00/10.54 ~ (X22 = bnd_n1) = (X22 = bnd_n0)) & % 11.00/10.54 ~ (X23 = bnd_n1) = (X23 = bnd_n0)) & % 11.00/10.54 ~ (X24 = bnd_n1) = (X24 = bnd_n0)) & % 11.00/10.54 ~ (X25 = bnd_n1) = (X25 = bnd_n0)) & % 11.00/10.54 ~ (X26 = bnd_n1) = (X26 = bnd_n0)) & % 11.00/10.54 ~ (X27 = bnd_n1) = (X27 = bnd_n0)) & % 11.00/10.54 ~ (X28 = bnd_n1) = (X28 = bnd_n0)) & % 11.00/10.54 ~ (X29 = bnd_n1) = (X29 = bnd_n0)) & % 11.00/10.54 ~ (X30 = bnd_n1) = (X30 = bnd_n0)) & % 11.00/10.54 ~ (X31 = bnd_n1) = (X31 = bnd_n0)) & % 11.00/10.54 ~ (X32 = bnd_n1) = (X32 = bnd_n0)) & % 11.00/10.54 ~ (X33 = bnd_n1) = (X33 = bnd_n0); % 11.00/10.54 ALL X8 X7 X6 X4 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A X4 % 11.00/10.54 bnd_n1 X6 X7 X8 bnd_n1 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A X4 % 11.00/10.54 bnd_n1 X6 X7 X8 bnd_n1; % 11.00/10.54 ALL X5 X9 X8 X6 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n0 % 11.00/10.54 bnd_n1 X6 bnd_n1 X8 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 X5 X6 bnd_n1 X8 X9; % 11.00/10.54 ALL X4 X9 X7 X6 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 bnd_n0 X6 X7 bnd_n1 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A X4 % 11.00/10.54 bnd_n1 X6 X7 bnd_n1 X9; % 11.00/10.54 ALL X9 X8 X7 X5 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 X5 bnd_n1 X7 X8 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 X5 bnd_n1 X7 X8 X9; % 11.00/10.54 ALL X8 X7 X6 X4 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A X4 % 11.00/10.54 bnd_n1 X6 X7 X8 bnd_n0 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A X4 % 11.00/10.54 bnd_n1 X6 X7 X8 bnd_n1; % 11.00/10.54 ALL X9 X8 X6 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 bnd_n1 X6 bnd_n0 X8 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 bnd_n1 X6 bnd_n1 X8 X9; % 11.00/10.54 ALL X9 X7 X6 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 bnd_n1 X6 X7 bnd_n0 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 bnd_n1 X6 X7 bnd_n1 X9; % 11.00/10.54 ALL X9 X8 X7 X5 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 % 11.00/10.54 B1. % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 X5 bnd_n0 X7 X8 X9 --> % 11.00/10.54 bnd_p B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E D C B A bnd_n1 % 11.00/10.54 X5 bnd_n1 X7 X8 X9; % 11.00/10.54 ALL X13 X12 X11 X9 X8 X7 X6 X4 X3 A B C D E F G H I J K L M N O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 bnd_n1 % 11.00/10.54 X6 X7 X8 X9 bnd_n1 X11 X12 X13 bnd_n0 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 bnd_n1 % 11.00/10.54 X6 X7 X8 X9 bnd_n1 X11 X12 X13 bnd_n1; % 11.00/10.54 ALL X14 X13 X11 X10 X8 X7 X6 X4 X3 A B C D E F G H I J K L M N O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 bnd_n1 X6 % 11.00/10.54 X7 X8 bnd_n1 X10 X11 bnd_n0 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 bnd_n1 X6 % 11.00/10.54 X7 X8 bnd_n1 X10 X11 bnd_n1 X13 X14; % 11.00/10.54 ALL X14 X12 X11 X9 A B C D E F G X7 X6 X5 X3 X2 H I J K L M N O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 bnd_n1 X5 X6 X7 G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 bnd_n0 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 bnd_n1 X5 X6 X7 G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 bnd_n1 X14; % 11.00/10.54 ALL X14 X13 X12 X10 A B C D E F G X7 X6 X5 X3 X2 H I J K L M N O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 bnd_n1 X5 X6 X7 G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n0 X12 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 bnd_n1 X5 X6 X7 G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n1 X12 X13 X14; % 11.00/10.54 ALL X13 X12 X11 X9 A B C D E F G H I J K L M N X6 X5 X4 X2 X1 O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O bnd_n1 X1 X2 bnd_n1 X4 X5 X6 N M L K J I H G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 X13 bnd_n0 --> % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 bnd_n1 X4 X5 X6 N M L K J I H G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 X13 bnd_n1; % 11.00/10.54 ALL X14 X13 X11 X10 A B C D E F G H I J K L M N X6 X5 X4 X2 X1 O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 bnd_n1 X4 X5 X6 N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 X11 bnd_n0 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 bnd_n1 X4 X5 X6 N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 X11 bnd_n1 X13 X14; % 11.00/10.54 ALL X14 X12 X11 X9 A B C D E F G H I J K L M N O P Q R S T U X5 X4 X3 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 bnd_n1 X3 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A X9 bnd_n1 X11 X12 bnd_n0 X14 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 bnd_n1 X3 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A X9 bnd_n1 X11 X12 bnd_n1 X14; % 11.00/10.54 ALL X14 X13 X12 X10 A B C D E F G H I J K L M N O P Q R S T U X5 X4 X3 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 bnd_n1 X3 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n0 X12 X13 X14 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 bnd_n1 X3 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n1 X12 X13 X14; % 11.00/10.54 ALL X13 X12 X11 X9 X8 X7 X5 X4 X3 A B C D E F G H I J K L M N O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 X5 % 11.00/10.54 bnd_n1 X7 X8 X9 bnd_n0 X11 X12 X13 bnd_n1 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 X5 % 11.00/10.54 bnd_n1 X7 X8 X9 bnd_n1 X11 X12 X13 bnd_n1; % 11.00/10.54 ALL X14 X13 X11 X10 X8 X7 X5 X4 X3 A B C D E F G H I J K L M N O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 X5 bnd_n1 % 11.00/10.54 X7 X8 bnd_n0 X10 X11 bnd_n1 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H G F E D C B A bnd_n1 X3 X4 X5 bnd_n1 % 11.00/10.54 X7 X8 bnd_n1 X10 X11 bnd_n1 X13 X14; % 11.00/10.54 ALL X14 X12 X11 X9 A B C D E F G X7 X6 X4 X3 X2 H I J K L M N O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 X4 bnd_n1 X6 X7 G F % 11.00/10.54 E D C B A X9 bnd_n0 X11 X12 bnd_n1 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 X4 bnd_n1 X6 X7 G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 bnd_n1 X14; % 11.00/10.54 ALL X14 X13 X12 X10 A B C D E F G X7 X6 X4 X3 X2 H I J K L M N O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 X4 bnd_n1 X6 X7 G F E D % 11.00/10.54 C B A bnd_n0 X10 bnd_n1 X12 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O N M L K J I H bnd_n1 X2 X3 X4 bnd_n1 X6 X7 G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n1 X12 X13 X14; % 11.00/10.54 ALL X13 X12 X11 X9 A B C D E F G H I J K L M N X6 X5 X3 X2 X1 O P Q R S T % 11.00/10.54 U. bnd_p U T S R Q P O bnd_n1 X1 X2 X3 bnd_n1 X5 X6 N M L K J I H G F % 11.00/10.54 E D C B A X9 bnd_n0 X11 X12 X13 bnd_n1 --> % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 X3 bnd_n1 X5 X6 N M L K J I H G F % 11.00/10.54 E D C B A X9 bnd_n1 X11 X12 X13 bnd_n1; % 11.00/10.54 ALL X14 X13 X11 X10 A B C D E F G H I J K L M N X6 X5 X3 X2 X1 O P Q R S % 11.00/10.54 T U. % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 X3 bnd_n1 X5 X6 N M L K J I H G F E D % 11.00/10.54 C B A bnd_n0 X10 X11 bnd_n1 X13 X14 --> % 11.00/10.54 bnd_p U T S R Q P O bnd_n1 X1 X2 X3 bnd_n1 X5 X6 N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 X11 bnd_n1 X13 X14; % 11.00/10.54 ALL X14 X12 X11 X9 A B C D E F G H I J K L M N O P Q R S T U X5 X4 X2 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 bnd_n1 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A X9 bnd_n0 X11 X12 bnd_n1 X14 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 bnd_n1 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A X9 bnd_n1 X11 X12 bnd_n1 X14; % 11.00/10.54 ALL X14 X13 X12 X10 A B C D E F G H I J K L M N O P Q R S T U X5 X4 X2 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 bnd_n1 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A bnd_n0 X10 bnd_n1 X12 X13 X14 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 bnd_n1 X4 X5 U T S R Q P O N M L K J I H G F E D % 11.00/10.54 C B A bnd_n1 X10 bnd_n1 X12 X13 X14; % 11.00/10.54 ALL A B C D E F X7 X6 X5 X4 X3 G H I J K L M N O P Q R S T U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 X3 X4 X5 X6 X7 % 11.00/10.54 bnd_n1 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 X3 X4 X5 X6 X7 % 11.00/10.54 bnd_n0 F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X6 X5 X4 X3 X2 N O P Q R S T U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 X2 X3 X4 X5 X6 bnd_n1 M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 X2 X3 X4 X5 X6 bnd_n0 M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X5 X4 X3 X2 X1 U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 X1 X2 X3 X4 X5 bnd_n1 T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 X1 X2 X3 X4 X5 bnd_n0 T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X4 X3 X2 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 A1 Z Y X W V U T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n0 A1 Z Y X W V U T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F X8 X6 X5 X4 X3 G H I J K L M N O P Q R S T U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 X3 X4 X5 X6 % 11.00/10.54 bnd_n0 X8 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 X3 X4 X5 X6 % 11.00/10.54 bnd_n1 X8 F E D C B A; % 11.00/10.54 ALL A B C D E F X8 X7 X5 X4 G H I J K L M N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 X4 X5 % 11.00/10.54 bnd_n0 X7 X8 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 X4 X5 % 11.00/10.54 bnd_n1 X7 X8 F E D C B A; % 11.00/10.54 ALL A B C D E F X8 X7 X6 G H I J K L M N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 bnd_n0 % 11.00/10.54 bnd_n0 X6 X7 X8 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 bnd_n0 % 11.00/10.54 bnd_n1 X6 X7 X8 F E D C B A; % 11.00/10.54 ALL A B C D E F X8 X7 X6 G H I J K L M N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 bnd_n0 % 11.00/10.54 bnd_n0 X6 X7 X8 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 bnd_n1 % 11.00/10.54 bnd_n0 X6 X7 X8 F E D C B A; % 11.00/10.54 ALL A B C D E F X8 X7 X5 G H I J K L M N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n0 bnd_n0 % 11.00/10.54 X5 bnd_n0 X7 X8 F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N M L K J I H G bnd_n1 bnd_n1 bnd_n0 % 11.00/10.54 X5 bnd_n0 X7 X8 F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X7 X5 X4 X3 X2 N O P Q R S T U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 X2 X3 X4 X5 bnd_n0 X7 M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 X2 X3 X4 X5 bnd_n1 X7 M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X7 X6 X4 X3 N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 X3 X4 bnd_n0 X6 X7 M % 11.00/10.54 L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 X3 X4 bnd_n1 X6 X7 M % 11.00/10.54 L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X7 X6 X5 N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 bnd_n0 bnd_n0 X5 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 bnd_n0 bnd_n1 X5 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X7 X6 X5 N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 bnd_n0 bnd_n0 X5 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 bnd_n1 bnd_n0 X5 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M X7 X6 X4 N O P Q R S T U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n0 bnd_n0 X4 bnd_n0 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U T S R Q P O N bnd_n1 bnd_n1 bnd_n0 X4 bnd_n0 X6 % 11.00/10.54 X7 M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X6 X4 X3 X2 X1 U V W X Y Z % 11.00/10.54 A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 X1 X2 X3 X4 bnd_n0 X6 T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 X1 X2 X3 X4 bnd_n1 X6 T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X6 X5 X3 X2 U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 X2 X3 bnd_n0 X5 X6 T S R Q P O N M % 11.00/10.54 L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 X2 X3 bnd_n1 X5 X6 T S R Q P O N M % 11.00/10.54 L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X6 X5 X4 U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 bnd_n0 bnd_n0 X4 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 bnd_n0 bnd_n1 X4 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X6 X5 X4 U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 bnd_n0 bnd_n0 X4 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 bnd_n1 bnd_n0 X4 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T X6 X5 X3 U V W X Y Z A1. % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n0 bnd_n0 X3 bnd_n0 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p A1 Z Y X W V U bnd_n1 bnd_n1 bnd_n0 X3 bnd_n0 X5 X6 T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X5 X3 X2 X1 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 bnd_n0 X5 A1 Z Y X W V U T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 bnd_n1 X5 A1 Z Y X W V U T S R Q P O N M L K % 11.00/10.54 J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X5 X4 X2 X1. % 11.00/10.54 bnd_p bnd_n1 bnd_n0 X1 X2 bnd_n0 X4 X5 A1 Z Y X W V U T S R Q P O N M % 11.00/10.54 L K J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 bnd_n0 X1 X2 bnd_n1 X4 X5 A1 Z Y X W V U T S R Q P O N M % 11.00/10.54 L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X5 X4 X3. % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n0 bnd_n0 X3 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n0 bnd_n1 X3 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X5 X4 X3. % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n0 bnd_n0 X3 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n1 bnd_n0 X3 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 X5 X4 X2. % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n0 X2 bnd_n0 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A --> % 11.00/10.54 bnd_p bnd_n1 bnd_n1 bnd_n0 X2 bnd_n0 X4 X5 A1 Z Y X W V U T S R Q P O % 11.00/10.54 N M L K J I H G F E D C B A; % 11.00/10.54 ALL X12 X11 X10 A B X8 X7 X6 X5 X3 C D E F G H I J K L M N O P Q R S T U % 11.00/10.54 V W. % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J I H G F E D C bnd_n1 X3 bnd_n1 X5 X6 % 11.00/10.54 X7 X8 B A X10 X11 X12 bnd_n1 --> % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J I H G F E D C bnd_n1 X3 bnd_n1 X5 X6 % 11.00/10.54 X7 bnd_n1 B A X10 X11 X12 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B X13 X12 X11 X10 X8 X7 X6 X5 X4 X3 X2 C D E F G H I J % 11.00/10.54 K L M N O P. % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n0 X2 X3 X4 X5 X6 X7 bnd_n1 X8 % 11.00/10.54 bnd_n1 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18 --> % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 X2 X3 X4 X5 X6 bnd_n1 bnd_n1 % 11.00/10.54 X8 bnd_n1 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X17 X16 X15 A B X13 X12 X11 X10 X8 C D E F G H I X6 X5 X4 X3 X2 X1 J % 11.00/10.54 K L M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n0 X1 X2 X3 X4 X5 X6 I H G F E D C bnd_n1 X8 % 11.00/10.54 bnd_n1 X10 X11 X12 X13 B A X15 X16 X17 bnd_n1 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 I H G F E D C bnd_n1 % 11.00/10.54 X8 bnd_n1 X10 X11 X12 X13 B A X15 X16 X17 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B X13 X12 X11 X10 X8 C D E F G H I J K L M N O P X5 X4 % 11.00/10.54 X3 X2 X1 X0. % 11.00/10.54 bnd_p bnd_n0 X0 X1 X2 X3 X4 X5 P O N M L K J I H G F E D C bnd_n1 X8 % 11.00/10.54 bnd_n1 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 X8 bnd_n1 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B X13 X12 X11 X10 X9 X8 X7 X6 X5 X4 X2 C D E F G H I J % 11.00/10.54 K L M N O P. % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 X2 bnd_n1 X4 X5 X6 X7 bnd_n0 % 11.00/10.54 X8 X9 X10 X11 X12 X13 B A X15 X16 bnd_n1 X18 --> % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 X2 bnd_n1 X4 X5 X6 X7 bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X13 X12 X11 A B C D E F G H I X7 X6 X5 X4 X2 J K L M N O P Q R S T U % 11.00/10.54 V W. % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J bnd_n1 X2 bnd_n1 X4 X5 X6 X7 I H G F % 11.00/10.54 E D C B A bnd_n1 X11 X12 X13 --> % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J bnd_n1 X2 bnd_n1 X4 X5 X6 bnd_n1 I H % 11.00/10.54 G F E D C B A bnd_n1 X11 X12 X13; % 11.00/10.54 ALL X18 X16 X15 A B C D E F G H I X12 X11 X10 X9 X7 X6 X5 X4 X3 X2 X1 J K % 11.00/10.54 L M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n0 X1 X2 X3 X4 X5 X6 bnd_n1 X7 bnd_n1 X9 X10 % 11.00/10.54 X11 X12 I H G F E D C B A X15 X16 bnd_n1 X18 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 bnd_n1 X7 bnd_n1 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X18 X17 X16 A B C D E F G H I X12 X11 X10 X9 X7 J K L M N O P X5 X4 % 11.00/10.54 X3 X2 X1 X0. % 11.00/10.54 bnd_p bnd_n0 X0 X1 X2 X3 X4 X5 P O N M L K J bnd_n1 X7 bnd_n1 X9 X10 % 11.00/10.54 X11 X12 I H G F E D C B A bnd_n1 X16 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J bnd_n1 X7 bnd_n1 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A bnd_n1 X16 X17 X18; % 11.00/10.54 ALL X17 X16 X15 A B X13 X12 X11 X10 X9 X8 C D E F G H I X6 X5 X4 X3 X1 J % 11.00/10.54 K L M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 bnd_n1 X3 X4 X5 X6 I H G F E D C bnd_n0 % 11.00/10.54 X8 X9 X10 X11 X12 X13 B A X15 X16 X17 bnd_n1 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 bnd_n1 X3 X4 X5 X6 I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 X17 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B C D E F G H I X12 X11 X10 X9 X8 X7 X6 X5 X4 X3 X1 J K % 11.00/10.54 L M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 bnd_n1 X3 X4 X5 X6 bnd_n0 X7 X8 X9 X10 % 11.00/10.54 X11 X12 I H G F E D C B A X15 bnd_n1 X17 X18 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 bnd_n1 X3 X4 X5 X6 bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X12 X11 X10 A B C D E F G H I J K L M N O P X6 X5 X4 X3 X1 Q R S T U % 11.00/10.54 V W. % 11.00/10.54 bnd_p W V U T S R Q bnd_n1 X1 bnd_n1 X3 X4 X5 X6 P O N M L K J I H G F % 11.00/10.54 E D C B A X10 X11 X12 bnd_n1 --> % 11.00/10.54 bnd_p W V U T S R Q bnd_n1 X1 bnd_n1 X3 X4 X5 bnd_n1 P O N M L K J I H % 11.00/10.54 G F E D C B A X10 X11 X12 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B C D E F G H I J K L M N O P X11 X10 X9 X8 X6 X5 X4 X3 % 11.00/10.54 X2 X1 X0. % 11.00/10.54 bnd_p bnd_n0 X0 X1 X2 X3 X4 X5 bnd_n1 X6 bnd_n1 X8 X9 X10 X11 P O N M % 11.00/10.54 L K J I H G F E D C B A X15 bnd_n1 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 bnd_n1 X6 bnd_n1 X8 X9 X10 X11 P O % 11.00/10.54 N M L K J I H G F E D C B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B X13 X12 X11 X10 X9 X8 C D E F G H I J K L M N O P X5 % 11.00/10.54 X4 X3 X2 X0. % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 P O N M L K J I H G F E D C bnd_n0 % 11.00/10.54 X8 X9 X10 X11 X12 X13 B A X15 X16 bnd_n1 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X18 X17 X16 A B C D E F G H I X12 X11 X10 X9 X8 X7 J K L M N O P X5 % 11.00/10.54 X4 X3 X2 X0. % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 P O N M L K J bnd_n0 X7 X8 X9 X10 % 11.00/10.54 X11 X12 I H G F E D C B A bnd_n1 X16 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 P O N M L K J bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A bnd_n1 X16 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B C D E F G H I J K L M N O P X11 X10 X9 X8 X7 X6 X5 X4 % 11.00/10.54 X3 X2 X0. % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 bnd_n0 X6 X7 X8 X9 X10 X11 P O N M % 11.00/10.54 L K J I H G F E D C B A X15 X16 bnd_n1 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 bnd_n1 X6 X7 X8 X9 X10 bnd_n1 P O N % 11.00/10.54 M L K J I H G F E D C B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X13 X12 X11 A B C D E F G H I J K L M N O P Q R S T U V W X5 X4 X3 X2 % 11.00/10.54 X0. % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 X5 W V U T S R Q P O N M L K J I H G F % 11.00/10.54 E D C B A bnd_n1 X11 X12 X13 --> % 11.00/10.54 bnd_p bnd_n1 X0 bnd_n1 X2 X3 X4 bnd_n1 W V U T S R Q P O N M L K J I H % 11.00/10.54 G F E D C B A bnd_n1 X11 X12 X13; % 11.00/10.54 ALL X12 X11 X10 A B X7 X6 X5 X4 C D E F G H I J K L M N O P Q R S T U V % 11.00/10.54 W. bnd_p W V U T S R Q P O N M L K J I H G F E D C bnd_n1 bnd_n1 X4 X5 % 11.00/10.54 X6 X7 bnd_n1 B A X10 X11 X12 bnd_n0 --> % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J I H G F E D C bnd_n1 bnd_n1 X4 X5 % 11.00/10.54 X6 X7 bnd_n1 B A X10 X11 X12 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B X13 X12 X11 X10 X9 X6 X5 X4 X3 X2 C D E F G H I J K L % 11.00/10.54 M N O P. % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 X2 X3 X4 X5 X6 bnd_n1 bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 bnd_n0 X17 X18 --> % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 X2 X3 X4 X5 X6 bnd_n1 bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X17 X16 X15 A B X13 X12 X11 X10 X9 C D E F G H I X5 X4 X3 X2 X1 J K L % 11.00/10.54 M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 I H G F E D C bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 X16 X17 bnd_n0 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 I H G F E D C bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 X16 X17 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B X13 X12 X11 X10 X9 C D E F G H I J K L M N O P X4 X3 % 11.00/10.54 X2 X1 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 bnd_n0 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 bnd_n1 X9 X10 X11 X12 X13 B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B X12 X11 X10 X9 X8 X7 X6 X5 X4 X3 C D E F G H I J K L % 11.00/10.54 M N O P. % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 bnd_n1 X3 X4 X5 X6 X7 bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n0 X18 --> % 11.00/10.54 bnd_p P O N M L K J I H G F E D C bnd_n1 bnd_n1 X3 X4 X5 X6 X7 bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X13 X12 X11 A B C D E F G H I X6 X5 X4 X3 J K L M N O P Q R S T U V % 11.00/10.54 W. bnd_p W V U T S R Q P O N M L K J bnd_n1 bnd_n1 X3 X4 X5 X6 bnd_n1 % 11.00/10.54 I H G F E D C B A bnd_n0 X11 X12 X13 --> % 11.00/10.54 bnd_p W V U T S R Q P O N M L K J bnd_n1 bnd_n1 X3 X4 X5 X6 bnd_n1 % 11.00/10.54 I H G F E D C B A bnd_n1 X11 X12 X13; % 11.00/10.54 ALL X18 X16 X15 A B C D E F G H I X12 X11 X10 X9 X8 X5 X4 X3 X2 X1 J K L % 11.00/10.54 M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 bnd_n1 bnd_n1 X8 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A X15 X16 bnd_n0 X18 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 X1 X2 X3 X4 X5 bnd_n1 bnd_n1 bnd_n1 X8 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X18 X17 X16 A B C D E F G H I X12 X11 X10 X9 X8 J K L M N O P X4 X3 % 11.00/10.54 X2 X1 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J bnd_n1 bnd_n1 X8 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A bnd_n0 X16 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 P O N M L K J bnd_n1 bnd_n1 X8 X9 % 11.00/10.54 X10 X11 X12 I H G F E D C B A bnd_n1 X16 X17 X18; % 11.00/10.54 ALL X17 X16 X15 A B X12 X11 X10 X9 X8 C D E F G H I X6 X5 X4 X3 X2 J K L % 11.00/10.54 M N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 bnd_n1 X2 X3 X4 X5 X6 I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 X17 bnd_n0 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 bnd_n1 X2 X3 X4 X5 X6 I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 X17 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B C D E F G H I X11 X10 X9 X8 X7 X6 X5 X4 X3 X2 J K L M % 11.00/10.54 N O P. % 11.00/10.54 bnd_p P O N M L K J bnd_n1 bnd_n1 X2 X3 X4 X5 X6 bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A X15 bnd_n0 X17 X18 --> % 11.00/10.54 bnd_p P O N M L K J bnd_n1 bnd_n1 X2 X3 X4 X5 X6 bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X12 X11 X10 A B C D E F G H I J K L M N O P X5 X4 X3 X2 Q R S T U V % 11.00/10.54 W. bnd_p W V U T S R Q bnd_n1 bnd_n1 X2 X3 X4 X5 bnd_n1 P O N M L K J % 11.00/10.54 I H G F E D C B A X10 X11 X12 bnd_n0 --> % 11.00/10.54 bnd_p W V U T S R Q bnd_n1 bnd_n1 X2 X3 X4 X5 bnd_n1 P O N M L K J % 11.00/10.54 I H G F E D C B A X10 X11 X12 bnd_n1; % 11.00/10.54 ALL X18 X17 X15 A B C D E F G H I J K L M N O P X11 X10 X9 X8 X7 X4 X3 X2 % 11.00/10.54 X1 X0. % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 bnd_n1 bnd_n1 X7 X8 X9 X10 X11 P O % 11.00/10.54 N M L K J I H G F E D C B A X15 bnd_n0 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 X0 X1 X2 X3 X4 bnd_n1 bnd_n1 bnd_n1 X7 X8 X9 X10 X11 P O % 11.00/10.54 N M L K J I H G F E D C B A X15 bnd_n1 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B X12 X11 X10 X9 X8 C D E F G H I J K L M N O P X5 X4 % 11.00/10.54 X3 X2 X1. % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n0 X18 --> % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 P O N M L K J I H G F E D C bnd_n1 % 11.00/10.54 X8 X9 X10 X11 X12 bnd_n1 B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X18 X17 X16 A B C D E F G H I X11 X10 X9 X8 X7 J K L M N O P X5 X4 X3 % 11.00/10.54 X2 X1. % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 P O N M L K J bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A bnd_n0 X16 X17 X18 --> % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 P O N M L K J bnd_n1 X7 X8 X9 X10 % 11.00/10.54 X11 bnd_n1 I H G F E D C B A bnd_n1 X16 X17 X18; % 11.00/10.54 ALL X18 X16 X15 A B C D E F G H I J K L M N O P X10 X9 X8 X7 X6 X5 X4 X3 % 11.00/10.54 X2 X1. % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 bnd_n1 X6 X7 X8 X9 X10 bnd_n1 P O N % 11.00/10.54 M L K J I H G F E D C B A X15 X16 bnd_n0 X18 --> % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 X5 bnd_n1 X6 X7 X8 X9 X10 bnd_n1 P O N % 11.00/10.54 M L K J I H G F E D C B A X15 X16 bnd_n1 X18; % 11.00/10.54 ALL X13 X12 X11 A B C D E F G H I J K L M N O P Q R S T U V W X4 X3 X2 % 11.00/10.54 X1. % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 bnd_n1 W V U T S R Q P O N M L K J I H % 11.00/10.54 G F E D C B A bnd_n0 X11 X12 X13 --> % 11.00/10.54 bnd_p bnd_n1 bnd_n1 X1 X2 X3 X4 bnd_n1 W V U T S R Q P O N M L K J I H % 11.00/10.54 G F E D C B A bnd_n1 X11 X12 X13; % 11.00/10.54 bnd_p bnd_n1 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n1 bnd_n1 bnd_n0 % 11.00/10.54 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 11.00/10.54 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 % 11.00/10.54 bnd_n0 bnd_n0 bnd_n0 bnd_n0 bnd_n0 |] % 11.00/10.54 ==> EX A B C D X1 E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 % 11.00/10.54 F1. % 11.00/10.54 bnd_p F1 E1 D1 C1 B1 A1 Z Y X W V U T S R Q P O N M L K J I H G F E % 11.00/10.54 bnd_n1 X1 D C B A % 11.00/10.54 Adding axioms... % 11.00/10.55 Typedef.type_definition_def % 99.33/98.73 ...done. % 99.44/98.87 Ground types: ?'b, TPTP_Interpret.ind % 99.44/98.87 Translating term (sizes: 1, 1) ... % 138.36/137.63 Invoking SAT solver... % 138.36/137.63 No model exists. % 138.36/137.63 Translating term (sizes: 2, 1) ... % 178.10/177.23 Invoking SAT solver... % 178.10/177.23 No model exists. % 178.10/177.23 Translating term (sizes: 1, 2) ... % 179.74/178.89 Search terminated, number of Boolean variables (100000 allowed) exceeded. % 179.74/178.89 % SZS status Unknown %------------------------------------------------------------------------------