src/HOL/ex/Argo_Examples.thy
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
child 64927 a5a09855e424
permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
     1 (*  Title:      HOL/ex/Argo_Examples.thy
     2     Author:     Sascha Boehme
     3 *)
     4 
     5 section \<open>Argo\<close>
     6 
     7 theory Argo_Examples
     8 imports Complex_Main
     9 begin
    10 
    11 text \<open>
    12   This theory is intended to showcase and test different features of the \<open>argo\<close> proof method.
    13 
    14   The \<open>argo\<close> proof method can be applied to propositional problems, problems involving equality
    15   reasoning and problems of linear real arithmetic.
    16 
    17   The \<open>argo\<close> proof method provides two options. To specify an upper limit of the proof methods
    18   run time in seconds, use the option \<open>argo_timeout\<close>. To specify the amount of output, use the
    19   option \<open>argo_trace\<close> with value \<open>none\<close> for no tracing output, value \<open>basic\<close> for viewing the
    20   underlying propositions and some timings, and value \<open>full\<close> for additionally inspecting the
    21   proof replay steps.
    22 \<close>
    23 
    24 declare[[argo_trace = full]]
    25 
    26 subsection \<open>Propositional logic\<close>
    27 
    28 notepad
    29 begin
    30   have "True" by argo
    31 next
    32   have "~False" by argo
    33 next
    34   fix P :: bool
    35   assume "False"
    36   then have "P" by argo
    37 next
    38   fix P :: bool
    39   assume "~True"
    40   then have "P" by argo
    41 next
    42   fix P :: bool
    43   assume "P"
    44   then have "P" by argo
    45 next
    46   fix P :: bool
    47   assume "~~P"
    48   then have "P" by argo
    49 next
    50   fix P Q R :: bool
    51   assume "P & Q & R"
    52   then have "R & P & Q" by argo
    53 next
    54   fix P Q R :: bool
    55   assume "P & (Q & True & R) & (Q & P) & True"
    56   then have "R & P & Q" by argo
    57 next
    58   fix P Q1 Q2 Q3 Q4 Q5 :: bool
    59   assume "Q1 & (Q2 & P & Q3) & (Q4 & ~P & Q5)"
    60   then have "~True" by argo
    61 next
    62   fix P Q1 Q2 Q3  :: bool
    63   assume "(Q1 & False) & Q2 & Q3"
    64   then have "P::bool" by argo
    65 next
    66   fix P Q R :: bool
    67   assume "P | Q | R"
    68   then have "R | P | Q" by argo
    69 next
    70   fix P Q R :: bool
    71   assume "P | (Q | False | R) | (Q | P) | False"
    72   then have "R | P | Q" by argo
    73 next
    74   fix P Q1 Q2 Q3 Q4 :: bool
    75   have "(Q1 & P & Q2) --> False | (Q3 | (Q4 | P) | False)" by argo
    76 next
    77   fix Q1 Q2 Q3 Q4 :: bool
    78   have "Q1 | (Q2 | True | Q3) | Q4" by argo
    79 next
    80   fix P Q R :: bool
    81   assume "(P & Q) | (P & ~Q) | (P & R) | (P & ~R)"
    82   then have "P" by argo
    83 next
    84   fix P :: bool
    85   assume "P = True"
    86   then have "P" by argo
    87 next
    88   fix P :: bool
    89   assume "False = P"
    90   then have "~P" by argo
    91 next
    92   fix P Q :: bool
    93   assume "P = (~P)"
    94   then have "Q" by argo
    95 next
    96   fix P :: bool
    97   have "(~P) = (~P)" by argo
    98 next
    99   fix P Q :: bool
   100   assume "P" and "~Q"
   101   then have "P = (~Q)" by argo
   102 next
   103   fix P Q :: bool
   104   assume "((P::bool) = Q) | (Q = P)"
   105   then have "(P --> Q) & (Q --> P)" by argo
   106 next
   107   fix P Q :: bool
   108   assume "(P::bool) = Q"
   109   then have "Q = P" by argo
   110 next
   111   fix P Q R :: bool
   112   assume "if P then Q else R"
   113   then have "Q | R" by argo
   114 next
   115   fix P Q :: bool
   116   assume "P | Q"
   117      and "P | ~Q"
   118      and "~P | Q"
   119      and "~P | ~Q"
   120   then have "False" by argo
   121 next
   122   fix P Q R :: bool
   123   assume "P | Q | R"
   124      and "P | Q | ~R"
   125      and "P | ~Q | R"
   126      and "P | ~Q | ~R"
   127      and "~P | Q | R"
   128      and "~P | Q | ~R"
   129      and "~P | ~Q | R"
   130      and "~P | ~Q | ~R"
   131   then have "False" by argo
   132 next
   133   fix a b c d e f g h i j k l m n p q :: bool
   134   assume "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
   135   then have "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" by argo
   136 next
   137   fix P :: bool
   138   have "P=P=P=P=P=P=P=P=P=P" by argo
   139 next
   140   fix a b c d e f p q x :: bool
   141   assume "a | b | c | d"
   142      and "e | f | (a & d)"
   143      and "~(a | (c & ~c)) | b"
   144      and "~(b & (x | ~x)) | c"
   145      and "~(d | False) | c"
   146      and "~(c | (~p & (p | (q & ~q))))"
   147   then have "False" by argo
   148 end
   149 
   150 
   151 subsection \<open>Equality, congruence and predicates\<close>
   152 
   153 notepad
   154 begin
   155   fix t :: "'a"
   156   have "t = t" by argo
   157 next
   158   fix t u :: "'a"
   159   assume "t = u"
   160   then have "u = t" by argo
   161 next
   162   fix s t u :: "'a"
   163   assume "s = t" and "t = u"
   164   then have "s = u" by argo
   165 next
   166   fix s t u v :: "'a"
   167   assume "s = t" and "t = u" and "u = v" and "u = s"
   168   then have "s = v" by argo
   169 next
   170   fix s t u v w :: "'a"
   171   assume "s = t" and "t = u" and "s = v" and "v = w"
   172   then have "w = u" by argo
   173 next
   174   fix s t u a b c :: "'a"
   175   assume "s = t" and "t = u" and "a = b" and "b = c"
   176   then have "s = a --> c = u" by argo
   177 next
   178   fix a b c d :: "'a"
   179   assume "(a = b & b = c) | (a = d & d = c)"
   180   then have "a = c" by argo
   181 next
   182   fix a b1 b2 b3 b4 c d :: "'a"
   183   assume "(a = b1 & ((b1 = b2 & b2 = b3) | (b1 = b4 & b4 = b3)) & b3 = c) | (a = d & d = c)"
   184   then have "a = c" by argo
   185 next
   186   fix a b :: "'a"
   187   have "(if True then a else b) = a" by argo
   188 next
   189   fix a b :: "'a"
   190   have "(if False then a else b) = b" by argo
   191 next
   192   fix a b :: "'a"
   193   have "(if \<not>True then a else b) = b" by argo
   194 next
   195   fix a b :: "'a"
   196   have "(if \<not>False then a else b) = a" by argo
   197 next
   198   fix P :: "bool"
   199   fix a :: "'a"
   200   have "(if P then a else a) = a" by argo
   201 next
   202   fix P :: "bool"
   203   fix a b c :: "'a"
   204   assume "P" and "a = c"
   205   then have "(if P then a else b) = c" by argo
   206 next
   207   fix P :: "bool"
   208   fix a b c :: "'a"
   209   assume "~P" and "b = c"
   210   then have "(if P then a else b) = c" by argo
   211 next
   212   fix P Q :: "bool"
   213   fix a b c d :: "'a"
   214   assume "P" and "Q" and "a = d"
   215   then have "(if P then (if Q then a else b) else c) = d" by argo
   216 next
   217   fix a b c :: "'a"
   218   assume "a \<noteq> b" and "b = c"
   219   then have "a \<noteq> c" by argo
   220 next
   221   fix a b c :: "'a"
   222   assume "a \<noteq> b" and "a = c"
   223   then have "c \<noteq> b" by argo
   224 next
   225   fix a b c d :: "'a"
   226   assume "a = b" and "c = d" and "b \<noteq> d"
   227   then have "a \<noteq> c" by argo
   228 next
   229   fix a b c d :: "'a"
   230   assume "a = b" and "c = d" and "d \<noteq> b"
   231   then have "a \<noteq> c" by argo
   232 next
   233   fix a b c d :: "'a"
   234   assume "a = b" and "c = d" and "b \<noteq> d"
   235   then have "c \<noteq> a" by argo
   236 next
   237   fix a b c d :: "'a"
   238   assume "a = b" and "c = d" and "d \<noteq> b"
   239   then have "c \<noteq> a" by argo
   240 next
   241   fix a b c d e f :: "'a"
   242   assume "a \<noteq> b" and "b = c" and "b = d" and "d = e" and "a = f"
   243   then have "f \<noteq> e" by argo
   244 next
   245   fix a b :: "'a" and f :: "'a \<Rightarrow> 'a"
   246   assume "a = b"
   247   then have "f a = f b" by argo
   248 next
   249   fix a b c :: "'a" and f :: "'a \<Rightarrow> 'a"
   250   assume "f a = f b" and "b = c"
   251   then have "f a = f c" by argo
   252 next
   253   fix a :: "'a" and f :: "'a \<Rightarrow> 'a"
   254   assume "f a = a"
   255   then have "f (f a) = a" by argo
   256 next
   257   fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
   258   assume "a = b"
   259   then have "g (f a) = g (f b)" by argo
   260 next
   261   fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
   262   assume "f a = b" and "g b = a"
   263   then have "f (g (f a)) = b" by argo
   264 next
   265   fix a b :: "'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   266   assume "a = b"
   267   then have "g a b = g b a" by argo
   268 next
   269   fix a b :: "'a" and f :: "'a \<Rightarrow> 'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   270   assume "f a = b"
   271   then have "g (f a) b = g b (f a)" by argo
   272 next
   273   fix a b c d e g h :: "'a" and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   274   assume "c = d" and "e = c" and "e = b" and "b = h" and "f g h = d" and "f g d = a"
   275   then have "a = b" by argo
   276 next
   277   fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
   278   assume "P a" and "a = b"
   279   then have "P b" by argo
   280 next
   281   fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
   282   assume "~ P a" and "a = b"
   283   then have "~ P b" by argo
   284 next
   285   fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   286   assume "P a b" and "a = c" and "b = d"
   287   then have "P c d" by argo
   288 next
   289   fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   290   assume "~ P a b" and "a = c" and "b = d"
   291   then have "~ P c d" by argo
   292 end
   293 
   294 
   295 subsection \<open>Linear real arithmetic\<close>
   296 
   297 subsubsection \<open>Negation and subtraction\<close>
   298 
   299 notepad
   300 begin
   301   fix a b :: real
   302   have
   303     "-a = -1 * a"
   304     "-(-a) = a"
   305     "a - b = a + -1 * b"
   306     "a - (-b) = a + b"
   307     by argo+
   308 end
   309 
   310 
   311 subsubsection \<open>Multiplication\<close>
   312 
   313 notepad
   314 begin
   315   fix a b c d :: real
   316   have
   317     "(2::real) * 3 = 6"
   318     "0 * a = 0"
   319     "a * 0 = 0"
   320     "1 * a = a"
   321     "a * 1 = a"
   322     "2 * a = a * 2"
   323     "2 * a * 3 = 6 * a"
   324     "2 * a * 3 * 5 = 30 * a"
   325     "a * 0 * b = 0"
   326     "a * (0 * b) = 0"
   327     "a * (b * c) = (a * b) * c"
   328     "a * (b * (c * d)) = ((a * b) * c) * d"
   329     "a * (b + c + d) = a * b + a * c + a * d"
   330     by argo+
   331 end
   332 
   333 
   334 subsubsection \<open>Division\<close>
   335 
   336 notepad
   337 begin
   338   fix a b c :: real
   339   have
   340     "(6::real) / 2 = 3"
   341     "a / 0 = a / 0"
   342     "a / 0 <= a / 0"
   343     "~(a / 0 < a / 0)"
   344     "0 / a = 0"
   345     "a / 1 = a"
   346     "a / 3 = 1/3 * a"
   347     "6 * a / 2 = 3 * a"
   348     "a / ((5 * b) / 2) = 2/5 * a / b"
   349     "a / (5 * (b / 2)) = 2/5 * a / b"
   350     "(a / 5) * (b / 2) = 1/10 * a * b"
   351     "a / (3 * b) = 1/3 * a / b"
   352     "(a + b) / 5 = 1/5 * a + 1/5 * b"
   353     "a / (5 * 1/5) = a"
   354     by argo+
   355 end
   356 
   357 
   358 subsubsection \<open>Addition\<close>
   359 
   360 notepad
   361 begin
   362   fix a b c d :: real
   363   have
   364     "a + b = b + a"
   365     "a + b + c = c + b + a"
   366     "a + b + c + d = d + c + b + a"
   367     "a + (b + (c + d)) = ((a + b) + c) + d"
   368     "(5::real) + -3 = 2"
   369     "(3::real) + 5 + -1 = 7"
   370     "2 + a = a + 2"
   371     "a + b + a = b + 2 * a"
   372     "-1 + a + -1 + 2 + b + 5/3 + b + 1/3 + 5 * b + 2/3 = 8/3 + a + 7 * b"
   373     "1 + b + b + 5 * b + 3 * a + 7 + a + 2 = 10 + 4 * a + 7 * b"
   374     by argo+
   375 end
   376 
   377 
   378 subsubsection \<open>Minimum and maximum\<close>
   379 
   380 notepad
   381 begin
   382   fix a b :: real
   383   have
   384     "min (3::real) 5 = 3"
   385     "min (5::real) 3 = 3"
   386     "min (3::real) (-5) = -5"
   387     "min (-5::real) 3 = -5"
   388     "min a a = a"
   389     "a \<le> b \<longrightarrow> min a b = a"
   390     "a > b \<longrightarrow> min a b = b"
   391     "min a b \<le> a"
   392     "min a b \<le> b"
   393     "min a b = min b a"
   394     by argo+
   395 next
   396   fix a b :: real
   397   have
   398     "max (3::real) 5 = 5"
   399     "max (5::real) 3 = 5"
   400     "max (3::real) (-5) = 3"
   401     "max (-5::real) 3 = 3"
   402     "max a a = a"
   403     "a \<le> b \<longrightarrow> max a b = b"
   404     "a > b \<longrightarrow> max a b = a"
   405     "a \<le> max a b"
   406     "b \<le> max a b"
   407     "max a b = max b a"
   408     by argo+
   409 next
   410   fix a b :: real
   411   have
   412     "min a b \<le> max a b"
   413     "min a b + max a b = a + b"
   414     "a < b \<longrightarrow> min a b < max a b"
   415     by argo+
   416 end
   417 
   418 
   419 subsubsection \<open>Absolute value\<close>
   420 
   421 notepad
   422 begin
   423   fix a :: real
   424   have
   425     "abs (3::real) = 3"
   426     "abs (-3::real) = 3"
   427     "0 \<le> abs a"
   428     "a \<le> abs a"
   429     "a \<ge> 0 \<longrightarrow> abs a = a"
   430     "a < 0 \<longrightarrow> abs a = -a"
   431     "abs (abs a) = abs a"
   432     by argo+
   433 end
   434 
   435 
   436 subsubsection \<open>Equality\<close>
   437 
   438 notepad
   439 begin
   440   fix a b c d :: real
   441   have
   442     "(3::real) = 3"
   443     "~((3::real) = 4)"
   444     "~((4::real) = 3)"
   445     "3 * a = 5 --> a = 5/3"
   446     "-3 * a = 5 --> -5/3 = a"
   447     "5 = 3 * a --> 5/3  = a "
   448     "5 = -3 * a --> a = -5/3"
   449     "2 + 3 * a = 4 --> a = 2/3"
   450     "4 = 2 + 3 * a --> 2/3 = a"
   451     "2 + 3 * a + 5 * b + c = 4 --> 3 * a + 5 * b + c = 2"
   452     "4 = 2 + 3 * a + 5 * b + c --> 2 = 3 * a + 5 * b + c"
   453     "-2 * a + b + -3 * c = 7 --> -7 = 2 * a + -1 * b + 3 * c"
   454     "7 = -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c = -7"
   455     "-2 * a + b + -3 * c + 4 * d = 7 --> -7 = 2 * a + -1 * b + 3 * c + -4 * d"
   456     "7 = -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d = -7"
   457     "a + 3 * b = 5 * c + b --> a + 2 * b + -5 * c = 0"
   458     by argo+
   459 end
   460 
   461 
   462 subsubsection \<open>Less-equal\<close>
   463 
   464 notepad
   465 begin
   466   fix a b c d :: real
   467   have
   468     "(3::real) <= 3"
   469     "(3::real) <= 4"
   470     "~((4::real) <= 3)"
   471     "3 * a <= 5 --> a <= 5/3"
   472     "-3 * a <= 5 --> -5/3 <= a"
   473     "5 <= 3 * a --> 5/3  <= a "
   474     "5 <= -3 * a --> a <= -5/3"
   475     "2 + 3 * a <= 4 --> a <= 2/3"
   476     "4 <= 2 + 3 * a --> 2/3 <= a"
   477     "2 + 3 * a + 5 * b + c <= 4 --> 3 * a + 5 * b + c <= 2"
   478     "4 <= 2 + 3 * a + 5 * b + c --> 2 <= 3 * a + 5 * b + c"
   479     "-2 * a + b + -3 * c <= 7 --> -7 <= 2 * a + -1 * b + 3 * c"
   480     "7 <= -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c <= -7"
   481     "-2 * a + b + -3 * c + 4 * d <= 7 --> -7 <= 2 * a + -1 * b + 3 * c + -4 * d"
   482     "7 <= -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d <= -7"
   483     "a + 3 * b <= 5 * c + b --> a + 2 * b + -5 * c <= 0"
   484     by argo+
   485 end
   486 
   487 subsubsection \<open>Less\<close>
   488 
   489 notepad
   490 begin
   491   fix a b c d :: real
   492   have
   493     "(3::real) < 4"
   494     "~((3::real) < 3)"
   495     "~((4::real) < 3)"
   496     "3 * a < 5 --> a < 5/3"
   497     "-3 * a < 5 --> -5/3 < a"
   498     "5 < 3 * a --> 5/3  < a "
   499     "5 < -3 * a --> a < -5/3"
   500     "2 + 3 * a < 4 --> a < 2/3"
   501     "4 < 2 + 3 * a --> 2/3 < a"
   502     "2 + 3 * a + 5 * b + c < 4 --> 3 * a + 5 * b + c < 2"
   503     "4 < 2 + 3 * a + 5 * b + c --> 2 < 3 * a + 5 * b + c"
   504     "-2 * a + b + -3 * c < 7 --> -7 < 2 * a + -1 * b + 3 * c"
   505     "7 < -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c < -7"
   506     "-2 * a + b + -3 * c + 4 * d < 7 --> -7 < 2 * a + -1 * b + 3 * c + -4 * d"
   507     "7 < -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d < -7"
   508     "a + 3 * b < 5 * c + b --> a + 2 * b + -5 * c < 0"
   509     by argo+
   510 end
   511 
   512 
   513 subsubsection \<open>Other examples\<close>
   514 
   515 notepad
   516 begin
   517   have
   518     "(0::real) < 1"
   519     "(47::real) + 11 < 8 * 15"
   520     by argo+
   521 next
   522   fix a :: real
   523   assume "a < 3"
   524   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
   525 next
   526   fix a :: real
   527   assume "a <= 3"
   528   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
   529 next
   530   fix a :: real
   531   assume "~(3 < a)"
   532   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
   533 next
   534   fix a :: real
   535   assume "~(3 <= a)"
   536   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
   537 next
   538   fix a :: real
   539   have "a < 3 | a = 3 | a > 3" by argo
   540 next
   541   fix a b :: real
   542   assume "0 < a" and "a < b"
   543   then have "0 < b" by argo
   544 next
   545   fix a b :: real
   546   assume "0 < a" and "a \<le> b"
   547   then have "0 \<le> b" by argo
   548 next
   549   fix a b :: real
   550   assume "0 \<le> a" and "a < b"
   551   then have "0 \<le> b" by argo
   552 next
   553   fix a b :: real
   554   assume "0 \<le> a" and "a \<le> b"
   555   then have "0 \<le> b" by argo
   556 next
   557   fix a b c :: real
   558   assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
   559   then have "-2 * a + -3 * b + 5 * c < 13" by argo
   560 next
   561   fix a b c :: real
   562   assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
   563   then have "-2 * a + -3 * b + 5 * c \<le> 12" by argo
   564 next
   565   fix a b :: real
   566   assume "a = 2" and "b = 3"
   567   then have "a + b > 5 \<or> a < b" by argo
   568 next
   569   fix a b c :: real
   570   assume "5 < b + c" and "a + c < 0" and "a > 0"
   571   then have "b > 0" by argo
   572 next
   573   fix a b c :: real
   574   assume "a + b < 7" and "5 < b + c" and "a + c < 0" and "a > 0"
   575   then have "0 < b \<and> b < 7" by argo
   576 next
   577   fix a b c :: real
   578   assume "a < b" and "b < c" and "c < a"
   579   then have "False" by argo
   580 next
   581   fix a b :: real
   582   assume "a - 5 > b"
   583   then have "b < a" by argo
   584 next
   585   fix a b :: real
   586   have "(a - b) - a = (a - a) - b" by argo
   587 next
   588   fix n m n' m' :: real
   589   have "
   590     (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
   591     (n = n' & n' < m) | (n = m & m < n') |
   592     (n' < m & m < n) | (n' < m & m = n) |
   593     (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
   594     (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
   595     (m = n & n < n') | (m = n' & n' < n) |
   596     (n' = m & m = n)"
   597     by argo
   598 end
   599 
   600 
   601 subsection \<open>Larger examples\<close>
   602 
   603 declare[[argo_trace = basic, argo_timeout = 60]]
   604 
   605 
   606 text \<open>Translated from TPTP problem library: PUZ015-2.006.dimacs\<close>
   607 
   608 lemma assumes 1: "~x0"
   609   and 2: "~x30"
   610   and 3: "~x29"
   611   and 4: "~x59"
   612   and 5: "x1 | x31 | x0"
   613   and 6: "x2 | x32 | x1"
   614   and 7: "x3 | x33 | x2"
   615   and 8: "x4 | x34 | x3"
   616   and 9: "x35 | x4"
   617   and 10: "x5 | x36 | x30"
   618   and 11: "x6 | x37 | x5 | x31"
   619   and 12: "x7 | x38 | x6 | x32"
   620   and 13: "x8 | x39 | x7 | x33"
   621   and 14: "x9 | x40 | x8 | x34"
   622   and 15: "x41 | x9 | x35"
   623   and 16: "x10 | x42 | x36"
   624   and 17: "x11 | x43 | x10 | x37"
   625   and 18: "x12 | x44 | x11 | x38"
   626   and 19: "x13 | x45 | x12 | x39"
   627   and 20: "x14 | x46 | x13 | x40"
   628   and 21: "x47 | x14 | x41"
   629   and 22: "x15 | x48 | x42"
   630   and 23: "x16 | x49 | x15 | x43"
   631   and 24: "x17 | x50 | x16 | x44"
   632   and 25: "x18 | x51 | x17 | x45"
   633   and 26: "x19 | x52 | x18 | x46"
   634   and 27: "x53 | x19 | x47"
   635   and 28: "x20 | x54 | x48"
   636   and 29: "x21 | x55 | x20 | x49"
   637   and 30: "x22 | x56 | x21 | x50"
   638   and 31: "x23 | x57 | x22 | x51"
   639   and 32: "x24 | x58 | x23 | x52"
   640   and 33: "x59 | x24 | x53"
   641   and 34: "x25 | x54"
   642   and 35: "x26 | x25 | x55"
   643   and 36: "x27 | x26 | x56"
   644   and 37: "x28 | x27 | x57"
   645   and 38: "x29 | x28 | x58"
   646   and 39: "~x1 | ~x31"
   647   and 40: "~x1 | ~x0"
   648   and 41: "~x31 | ~x0"
   649   and 42: "~x2 | ~x32"
   650   and 43: "~x2 | ~x1"
   651   and 44: "~x32 | ~x1"
   652   and 45: "~x3 | ~x33"
   653   and 46: "~x3 | ~x2"
   654   and 47: "~x33 | ~x2"
   655   and 48: "~x4 | ~x34"
   656   and 49: "~x4 | ~x3"
   657   and 50: "~x34 | ~x3"
   658   and 51: "~x35 | ~x4"
   659   and 52: "~x5 | ~x36"
   660   and 53: "~x5 | ~x30"
   661   and 54: "~x36 | ~x30"
   662   and 55: "~x6 | ~x37"
   663   and 56: "~x6 | ~x5"
   664   and 57: "~x6 | ~x31"
   665   and 58: "~x37 | ~x5"
   666   and 59: "~x37 | ~x31"
   667   and 60: "~x5 | ~x31"
   668   and 61: "~x7 | ~x38"
   669   and 62: "~x7 | ~x6"
   670   and 63: "~x7 | ~x32"
   671   and 64: "~x38 | ~x6"
   672   and 65: "~x38 | ~x32"
   673   and 66: "~x6 | ~x32"
   674   and 67: "~x8 | ~x39"
   675   and 68: "~x8 | ~x7"
   676   and 69: "~x8 | ~x33"
   677   and 70: "~x39 | ~x7"
   678   and 71: "~x39 | ~x33"
   679   and 72: "~x7 | ~x33"
   680   and 73: "~x9 | ~x40"
   681   and 74: "~x9 | ~x8"
   682   and 75: "~x9 | ~x34"
   683   and 76: "~x40 | ~x8"
   684   and 77: "~x40 | ~x34"
   685   and 78: "~x8 | ~x34"
   686   and 79: "~x41 | ~x9"
   687   and 80: "~x41 | ~x35"
   688   and 81: "~x9 | ~x35"
   689   and 82: "~x10 | ~x42"
   690   and 83: "~x10 | ~x36"
   691   and 84: "~x42 | ~x36"
   692   and 85: "~x11 | ~x43"
   693   and 86: "~x11 | ~x10"
   694   and 87: "~x11 | ~x37"
   695   and 88: "~x43 | ~x10"
   696   and 89: "~x43 | ~x37"
   697   and 90: "~x10 | ~x37"
   698   and 91: "~x12 | ~x44"
   699   and 92: "~x12 | ~x11"
   700   and 93: "~x12 | ~x38"
   701   and 94: "~x44 | ~x11"
   702   and 95: "~x44 | ~x38"
   703   and 96: "~x11 | ~x38"
   704   and 97: "~x13 | ~x45"
   705   and 98: "~x13 | ~x12"
   706   and 99: "~x13 | ~x39"
   707   and 100: "~x45 | ~x12"
   708   and 101: "~x45 | ~x39"
   709   and 102: "~x12 | ~x39"
   710   and 103: "~x14 | ~x46"
   711   and 104: "~x14 | ~x13"
   712   and 105: "~x14 | ~x40"
   713   and 106: "~x46 | ~x13"
   714   and 107: "~x46 | ~x40"
   715   and 108: "~x13 | ~x40"
   716   and 109: "~x47 | ~x14"
   717   and 110: "~x47 | ~x41"
   718   and 111: "~x14 | ~x41"
   719   and 112: "~x15 | ~x48"
   720   and 113: "~x15 | ~x42"
   721   and 114: "~x48 | ~x42"
   722   and 115: "~x16 | ~x49"
   723   and 116: "~x16 | ~x15"
   724   and 117: "~x16 | ~x43"
   725   and 118: "~x49 | ~x15"
   726   and 119: "~x49 | ~x43"
   727   and 120: "~x15 | ~x43"
   728   and 121: "~x17 | ~x50"
   729   and 122: "~x17 | ~x16"
   730   and 123: "~x17 | ~x44"
   731   and 124: "~x50 | ~x16"
   732   and 125: "~x50 | ~x44"
   733   and 126: "~x16 | ~x44"
   734   and 127: "~x18 | ~x51"
   735   and 128: "~x18 | ~x17"
   736   and 129: "~x18 | ~x45"
   737   and 130: "~x51 | ~x17"
   738   and 131: "~x51 | ~x45"
   739   and 132: "~x17 | ~x45"
   740   and 133: "~x19 | ~x52"
   741   and 134: "~x19 | ~x18"
   742   and 135: "~x19 | ~x46"
   743   and 136: "~x52 | ~x18"
   744   and 137: "~x52 | ~x46"
   745   and 138: "~x18 | ~x46"
   746   and 139: "~x53 | ~x19"
   747   and 140: "~x53 | ~x47"
   748   and 141: "~x19 | ~x47"
   749   and 142: "~x20 | ~x54"
   750   and 143: "~x20 | ~x48"
   751   and 144: "~x54 | ~x48"
   752   and 145: "~x21 | ~x55"
   753   and 146: "~x21 | ~x20"
   754   and 147: "~x21 | ~x49"
   755   and 148: "~x55 | ~x20"
   756   and 149: "~x55 | ~x49"
   757   and 150: "~x20 | ~x49"
   758   and 151: "~x22 | ~x56"
   759   and 152: "~x22 | ~x21"
   760   and 153: "~x22 | ~x50"
   761   and 154: "~x56 | ~x21"
   762   and 155: "~x56 | ~x50"
   763   and 156: "~x21 | ~x50"
   764   and 157: "~x23 | ~x57"
   765   and 158: "~x23 | ~x22"
   766   and 159: "~x23 | ~x51"
   767   and 160: "~x57 | ~x22"
   768   and 161: "~x57 | ~x51"
   769   and 162: "~x22 | ~x51"
   770   and 163: "~x24 | ~x58"
   771   and 164: "~x24 | ~x23"
   772   and 165: "~x24 | ~x52"
   773   and 166: "~x58 | ~x23"
   774   and 167: "~x58 | ~x52"
   775   and 168: "~x23 | ~x52"
   776   and 169: "~x59 | ~x24"
   777   and 170: "~x59 | ~x53"
   778   and 171: "~x24 | ~x53"
   779   and 172: "~x25 | ~x54"
   780   and 173: "~x26 | ~x25"
   781   and 174: "~x26 | ~x55"
   782   and 175: "~x25 | ~x55"
   783   and 176: "~x27 | ~x26"
   784   and 177: "~x27 | ~x56"
   785   and 178: "~x26 | ~x56"
   786   and 179: "~x28 | ~x27"
   787   and 180: "~x28 | ~x57"
   788   and 181: "~x27 | ~x57"
   789   and 182: "~x29 | ~x28"
   790   and 183: "~x29 | ~x58"
   791   and 184: "~x28 | ~x58"
   792   shows "False"
   793     using assms
   794     by argo
   795 
   796 
   797 text \<open>Translated from TPTP problem library: MSC007-1.008.dimacs\<close>
   798 
   799 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
   800   and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
   801   and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
   802   and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
   803   and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
   804   and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
   805   and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
   806   and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
   807   and 9: "~x0 | ~x7"
   808   and 10: "~x0 | ~x14"
   809   and 11: "~x0 | ~x21"
   810   and 12: "~x0 | ~x28"
   811   and 13: "~x0 | ~x35"
   812   and 14: "~x0 | ~x42"
   813   and 15: "~x0 | ~x49"
   814   and 16: "~x7 | ~x14"
   815   and 17: "~x7 | ~x21"
   816   and 18: "~x7 | ~x28"
   817   and 19: "~x7 | ~x35"
   818   and 20: "~x7 | ~x42"
   819   and 21: "~x7 | ~x49"
   820   and 22: "~x14 | ~x21"
   821   and 23: "~x14 | ~x28"
   822   and 24: "~x14 | ~x35"
   823   and 25: "~x14 | ~x42"
   824   and 26: "~x14 | ~x49"
   825   and 27: "~x21 | ~x28"
   826   and 28: "~x21 | ~x35"
   827   and 29: "~x21 | ~x42"
   828   and 30: "~x21 | ~x49"
   829   and 31: "~x28 | ~x35"
   830   and 32: "~x28 | ~x42"
   831   and 33: "~x28 | ~x49"
   832   and 34: "~x35 | ~x42"
   833   and 35: "~x35 | ~x49"
   834   and 36: "~x42 | ~x49"
   835   and 37: "~x1 | ~x8"
   836   and 38: "~x1 | ~x15"
   837   and 39: "~x1 | ~x22"
   838   and 40: "~x1 | ~x29"
   839   and 41: "~x1 | ~x36"
   840   and 42: "~x1 | ~x43"
   841   and 43: "~x1 | ~x50"
   842   and 44: "~x8 | ~x15"
   843   and 45: "~x8 | ~x22"
   844   and 46: "~x8 | ~x29"
   845   and 47: "~x8 | ~x36"
   846   and 48: "~x8 | ~x43"
   847   and 49: "~x8 | ~x50"
   848   and 50: "~x15 | ~x22"
   849   and 51: "~x15 | ~x29"
   850   and 52: "~x15 | ~x36"
   851   and 53: "~x15 | ~x43"
   852   and 54: "~x15 | ~x50"
   853   and 55: "~x22 | ~x29"
   854   and 56: "~x22 | ~x36"
   855   and 57: "~x22 | ~x43"
   856   and 58: "~x22 | ~x50"
   857   and 59: "~x29 | ~x36"
   858   and 60: "~x29 | ~x43"
   859   and 61: "~x29 | ~x50"
   860   and 62: "~x36 | ~x43"
   861   and 63: "~x36 | ~x50"
   862   and 64: "~x43 | ~x50"
   863   and 65: "~x2 | ~x9"
   864   and 66: "~x2 | ~x16"
   865   and 67: "~x2 | ~x23"
   866   and 68: "~x2 | ~x30"
   867   and 69: "~x2 | ~x37"
   868   and 70: "~x2 | ~x44"
   869   and 71: "~x2 | ~x51"
   870   and 72: "~x9 | ~x16"
   871   and 73: "~x9 | ~x23"
   872   and 74: "~x9 | ~x30"
   873   and 75: "~x9 | ~x37"
   874   and 76: "~x9 | ~x44"
   875   and 77: "~x9 | ~x51"
   876   and 78: "~x16 | ~x23"
   877   and 79: "~x16 | ~x30"
   878   and 80: "~x16 | ~x37"
   879   and 81: "~x16 | ~x44"
   880   and 82: "~x16 | ~x51"
   881   and 83: "~x23 | ~x30"
   882   and 84: "~x23 | ~x37"
   883   and 85: "~x23 | ~x44"
   884   and 86: "~x23 | ~x51"
   885   and 87: "~x30 | ~x37"
   886   and 88: "~x30 | ~x44"
   887   and 89: "~x30 | ~x51"
   888   and 90: "~x37 | ~x44"
   889   and 91: "~x37 | ~x51"
   890   and 92: "~x44 | ~x51"
   891   and 93: "~x3 | ~x10"
   892   and 94: "~x3 | ~x17"
   893   and 95: "~x3 | ~x24"
   894   and 96: "~x3 | ~x31"
   895   and 97: "~x3 | ~x38"
   896   and 98: "~x3 | ~x45"
   897   and 99: "~x3 | ~x52"
   898   and 100: "~x10 | ~x17"
   899   and 101: "~x10 | ~x24"
   900   and 102: "~x10 | ~x31"
   901   and 103: "~x10 | ~x38"
   902   and 104: "~x10 | ~x45"
   903   and 105: "~x10 | ~x52"
   904   and 106: "~x17 | ~x24"
   905   and 107: "~x17 | ~x31"
   906   and 108: "~x17 | ~x38"
   907   and 109: "~x17 | ~x45"
   908   and 110: "~x17 | ~x52"
   909   and 111: "~x24 | ~x31"
   910   and 112: "~x24 | ~x38"
   911   and 113: "~x24 | ~x45"
   912   and 114: "~x24 | ~x52"
   913   and 115: "~x31 | ~x38"
   914   and 116: "~x31 | ~x45"
   915   and 117: "~x31 | ~x52"
   916   and 118: "~x38 | ~x45"
   917   and 119: "~x38 | ~x52"
   918   and 120: "~x45 | ~x52"
   919   and 121: "~x4 | ~x11"
   920   and 122: "~x4 | ~x18"
   921   and 123: "~x4 | ~x25"
   922   and 124: "~x4 | ~x32"
   923   and 125: "~x4 | ~x39"
   924   and 126: "~x4 | ~x46"
   925   and 127: "~x4 | ~x53"
   926   and 128: "~x11 | ~x18"
   927   and 129: "~x11 | ~x25"
   928   and 130: "~x11 | ~x32"
   929   and 131: "~x11 | ~x39"
   930   and 132: "~x11 | ~x46"
   931   and 133: "~x11 | ~x53"
   932   and 134: "~x18 | ~x25"
   933   and 135: "~x18 | ~x32"
   934   and 136: "~x18 | ~x39"
   935   and 137: "~x18 | ~x46"
   936   and 138: "~x18 | ~x53"
   937   and 139: "~x25 | ~x32"
   938   and 140: "~x25 | ~x39"
   939   and 141: "~x25 | ~x46"
   940   and 142: "~x25 | ~x53"
   941   and 143: "~x32 | ~x39"
   942   and 144: "~x32 | ~x46"
   943   and 145: "~x32 | ~x53"
   944   and 146: "~x39 | ~x46"
   945   and 147: "~x39 | ~x53"
   946   and 148: "~x46 | ~x53"
   947   and 149: "~x5 | ~x12"
   948   and 150: "~x5 | ~x19"
   949   and 151: "~x5 | ~x26"
   950   and 152: "~x5 | ~x33"
   951   and 153: "~x5 | ~x40"
   952   and 154: "~x5 | ~x47"
   953   and 155: "~x5 | ~x54"
   954   and 156: "~x12 | ~x19"
   955   and 157: "~x12 | ~x26"
   956   and 158: "~x12 | ~x33"
   957   and 159: "~x12 | ~x40"
   958   and 160: "~x12 | ~x47"
   959   and 161: "~x12 | ~x54"
   960   and 162: "~x19 | ~x26"
   961   and 163: "~x19 | ~x33"
   962   and 164: "~x19 | ~x40"
   963   and 165: "~x19 | ~x47"
   964   and 166: "~x19 | ~x54"
   965   and 167: "~x26 | ~x33"
   966   and 168: "~x26 | ~x40"
   967   and 169: "~x26 | ~x47"
   968   and 170: "~x26 | ~x54"
   969   and 171: "~x33 | ~x40"
   970   and 172: "~x33 | ~x47"
   971   and 173: "~x33 | ~x54"
   972   and 174: "~x40 | ~x47"
   973   and 175: "~x40 | ~x54"
   974   and 176: "~x47 | ~x54"
   975   and 177: "~x6 | ~x13"
   976   and 178: "~x6 | ~x20"
   977   and 179: "~x6 | ~x27"
   978   and 180: "~x6 | ~x34"
   979   and 181: "~x6 | ~x41"
   980   and 182: "~x6 | ~x48"
   981   and 183: "~x6 | ~x55"
   982   and 184: "~x13 | ~x20"
   983   and 185: "~x13 | ~x27"
   984   and 186: "~x13 | ~x34"
   985   and 187: "~x13 | ~x41"
   986   and 188: "~x13 | ~x48"
   987   and 189: "~x13 | ~x55"
   988   and 190: "~x20 | ~x27"
   989   and 191: "~x20 | ~x34"
   990   and 192: "~x20 | ~x41"
   991   and 193: "~x20 | ~x48"
   992   and 194: "~x20 | ~x55"
   993   and 195: "~x27 | ~x34"
   994   and 196: "~x27 | ~x41"
   995   and 197: "~x27 | ~x48"
   996   and 198: "~x27 | ~x55"
   997   and 199: "~x34 | ~x41"
   998   and 200: "~x34 | ~x48"
   999   and 201: "~x34 | ~x55"
  1000   and 202: "~x41 | ~x48"
  1001   and 203: "~x41 | ~x55"
  1002   and 204: "~x48 | ~x55"
  1003   shows "False"
  1004     using assms
  1005     by argo
  1006 
  1007 
  1008 lemma "0 \<le> (yc::real) \<and>
  1009        0 \<le> yd \<and> 0 \<le> yb \<and> 0 \<le> ya \<Longrightarrow>
  1010        0 \<le> yf \<and>
  1011        0 \<le> xh \<and> 0 \<le> ye \<and> 0 \<le> yg \<Longrightarrow>
  1012        0 \<le> yw \<and> 0 \<le> xs \<and> 0 \<le> yu \<Longrightarrow>
  1013        0 \<le> aea \<and> 0 \<le> aee \<and> 0 \<le> aed \<Longrightarrow>
  1014        0 \<le> zy \<and> 0 \<le> xz \<and> 0 \<le> zw \<Longrightarrow>
  1015        0 \<le> zb \<and>
  1016        0 \<le> za \<and> 0 \<le> yy \<and> 0 \<le> yz \<Longrightarrow>
  1017        0 \<le> zp \<and> 0 \<le> zo \<and> 0 \<le> yq \<Longrightarrow>
  1018        0 \<le> adp \<and> 0 \<le> aeb \<and> 0 \<le> aec \<Longrightarrow>
  1019        0 \<le> acm \<and> 0 \<le> aco \<and> 0 \<le> acn \<Longrightarrow>
  1020        0 \<le> abl \<Longrightarrow>
  1021        0 \<le> zr \<and> 0 \<le> zq \<and> 0 \<le> abh \<Longrightarrow>
  1022        0 \<le> abq \<and> 0 \<le> zd \<and> 0 \<le> abo \<Longrightarrow>
  1023        0 \<le> acd \<and>
  1024        0 \<le> acc \<and> 0 \<le> xi \<and> 0 \<le> acb \<Longrightarrow>
  1025        0 \<le> acp \<and> 0 \<le> acr \<and> 0 \<le> acq \<Longrightarrow>
  1026        0 \<le> xw \<and>
  1027        0 \<le> xr \<and> 0 \<le> xv \<and> 0 \<le> xu \<Longrightarrow>
  1028        0 \<le> zc \<and> 0 \<le> acg \<and> 0 \<le> ach \<Longrightarrow>
  1029        0 \<le> zt \<and> 0 \<le> zs \<and> 0 \<le> xy \<Longrightarrow>
  1030        0 \<le> ady \<and> 0 \<le> adw \<and> 0 \<le> zg \<Longrightarrow>
  1031        0 \<le> abd \<and>
  1032        0 \<le> abc \<and> 0 \<le> yr \<and> 0 \<le> abb \<Longrightarrow>
  1033        0 \<le> adi \<and>
  1034        0 \<le> x \<and> 0 \<le> adh \<and> 0 \<le> xa \<Longrightarrow>
  1035        0 \<le> aak \<and> 0 \<le> aai \<and> 0 \<le> aad \<Longrightarrow>
  1036        0 \<le> aba \<and> 0 \<le> zh \<and> 0 \<le> aay \<Longrightarrow>
  1037        0 \<le> abg \<and> 0 \<le> ys \<and> 0 \<le> abe \<Longrightarrow>
  1038        0 \<le> abs1 \<and>
  1039        0 \<le> yt \<and> 0 \<le> abr \<and> 0 \<le> zu \<Longrightarrow>
  1040        0 \<le> abv \<and>
  1041        0 \<le> zn \<and> 0 \<le> abw \<and> 0 \<le> zm \<Longrightarrow>
  1042        0 \<le> adl \<and> 0 \<le> adn \<Longrightarrow>
  1043        0 \<le> acf \<and> 0 \<le> aca \<Longrightarrow>
  1044        0 \<le> ads \<and> 0 \<le> aaq \<Longrightarrow>
  1045        0 \<le> ada \<Longrightarrow>
  1046        0 \<le> aaf \<and> 0 \<le> aac \<and> 0 \<le> aag \<Longrightarrow>
  1047        0 \<le> aal \<and>
  1048        0 \<le> acu \<and> 0 \<le> acs \<and> 0 \<le> act \<Longrightarrow>
  1049        0 \<le> aas \<and> 0 \<le> xb \<and> 0 \<le> aat \<Longrightarrow>
  1050        0 \<le> zk \<and> 0 \<le> zj \<and> 0 \<le> zi \<Longrightarrow>
  1051        0 \<le> ack \<and>
  1052        0 \<le> acj \<and> 0 \<le> xc \<and> 0 \<le> aci \<Longrightarrow>
  1053        0 \<le> aav \<and> 0 \<le> aah \<and> 0 \<le> xd \<Longrightarrow>
  1054        0 \<le> abt \<and>
  1055        0 \<le> xo \<and> 0 \<le> abu \<and> 0 \<le> xn \<Longrightarrow>
  1056        0 \<le> adc \<and>
  1057        0 \<le> abz \<and> 0 \<le> adc \<and> 0 \<le> abz \<Longrightarrow>
  1058        0 \<le> xt \<and>
  1059        0 \<le> zz \<and> 0 \<le> aab \<and> 0 \<le> aaa \<Longrightarrow>
  1060        0 \<le> adq \<and>
  1061        0 \<le> xl \<and> 0 \<le> adr \<and> 0 \<le> adb \<Longrightarrow>
  1062        0 \<le> zf \<and> 0 \<le> yh \<and> 0 \<le> yi \<Longrightarrow>
  1063        0 \<le> aao \<and> 0 \<le> aam \<and> 0 \<le> xe \<Longrightarrow>
  1064        0 \<le> abk \<and>
  1065        0 \<le> aby \<and> 0 \<le> abj \<and> 0 \<le> abx \<Longrightarrow>
  1066        0 \<le> yp \<Longrightarrow>
  1067        0 \<le> yl \<and> 0 \<le> yj \<and> 0 \<le> ym \<Longrightarrow>
  1068        0 \<le> acw \<Longrightarrow>
  1069        0 \<le> adk \<and>
  1070        0 \<le> adg \<and> 0 \<le> adj \<and> 0 \<le> adf \<Longrightarrow>
  1071        0 \<le> adv \<and> 0 \<le> xf \<and> 0 \<le> adu \<Longrightarrow>
  1072        yc + yd + yb + ya = 1 \<Longrightarrow>
  1073        yf + xh + ye + yg = 1 \<Longrightarrow>
  1074        yw + xs + yu = 1 \<Longrightarrow>
  1075        aea + aee + aed = 1 \<Longrightarrow>
  1076        zy + xz + zw = 1 \<Longrightarrow>
  1077        zb + za + yy + yz = 1 \<Longrightarrow>
  1078        zp + zo + yq = 1 \<Longrightarrow>
  1079        adp + aeb + aec = 1 \<Longrightarrow>
  1080        acm + aco + acn = 1 \<Longrightarrow>
  1081        abl + abl = 1 \<Longrightarrow>
  1082        zr + zq + abh = 1 \<Longrightarrow>
  1083        abq + zd + abo = 1 \<Longrightarrow>
  1084        acd + acc + xi + acb = 1 \<Longrightarrow>
  1085        acp + acr + acq = 1 \<Longrightarrow>
  1086        xw + xr + xv + xu = 1 \<Longrightarrow>
  1087        zc + acg + ach = 1 \<Longrightarrow>
  1088        zt + zs + xy = 1 \<Longrightarrow>
  1089        ady + adw + zg = 1 \<Longrightarrow>
  1090        abd + abc + yr + abb = 1 \<Longrightarrow>
  1091        adi + x + adh + xa = 1 \<Longrightarrow>
  1092        aak + aai + aad = 1 \<Longrightarrow>
  1093        aba + zh + aay = 1 \<Longrightarrow>
  1094        abg + ys + abe = 1 \<Longrightarrow>
  1095        abs1 + yt + abr + zu = 1 \<Longrightarrow>
  1096        abv + zn + abw + zm = 1 \<Longrightarrow>
  1097        adl + adn = 1 \<Longrightarrow>
  1098        acf + aca = 1 \<Longrightarrow>
  1099        ads + aaq = 1 \<Longrightarrow>
  1100        ada + ada = 1 \<Longrightarrow>
  1101        aaf + aac + aag = 1 \<Longrightarrow>
  1102        aal + acu + acs + act = 1 \<Longrightarrow>
  1103        aas + xb + aat = 1 \<Longrightarrow>
  1104        zk + zj + zi = 1 \<Longrightarrow>
  1105        ack + acj + xc + aci = 1 \<Longrightarrow>
  1106        aav + aah + xd = 1 \<Longrightarrow>
  1107        abt + xo + abu + xn = 1 \<Longrightarrow>
  1108        adc + abz + adc + abz = 1 \<Longrightarrow>
  1109        xt + zz + aab + aaa = 1 \<Longrightarrow>
  1110        adq + xl + adr + adb = 1 \<Longrightarrow>
  1111        zf + yh + yi = 1 \<Longrightarrow>
  1112        aao + aam + xe = 1 \<Longrightarrow>
  1113        abk + aby + abj + abx = 1 \<Longrightarrow>
  1114        yp + yp = 1 \<Longrightarrow>
  1115        yl + yj + ym = 1 \<Longrightarrow>
  1116        acw + acw + acw + acw = 1 \<Longrightarrow>
  1117        adk + adg + adj + adf = 1 \<Longrightarrow>
  1118        adv + xf + adu = 1 \<Longrightarrow>
  1119        yd = 0 \<or> yb = 0 \<Longrightarrow>
  1120        xh = 0 \<or> ye = 0 \<Longrightarrow>
  1121        yy = 0 \<or> za = 0 \<Longrightarrow>
  1122        acc = 0 \<or> xi = 0 \<Longrightarrow>
  1123        xv = 0 \<or> xr = 0 \<Longrightarrow>
  1124        yr = 0 \<or> abc = 0 \<Longrightarrow>
  1125        zn = 0 \<or> abw = 0 \<Longrightarrow>
  1126        xo = 0 \<or> abu = 0 \<Longrightarrow>
  1127        xl = 0 \<or> adr = 0 \<Longrightarrow>
  1128        (yr + abd < abl \<or>
  1129         yr + (abd + abb) < 1) \<or>
  1130        yr + abd = abl \<and>
  1131        yr + (abd + abb) = 1 \<Longrightarrow>
  1132        adb + adr < xn + abu \<or>
  1133        adb + adr = xn + abu \<Longrightarrow>
  1134        (abl < abt \<or> abl < abt + xo) \<or>
  1135        abl = abt \<and> abl = abt + xo \<Longrightarrow>
  1136        yd + yc < abc + abd \<or>
  1137        yd + yc = abc + abd \<Longrightarrow>
  1138        aca < abb + yr \<or> aca = abb + yr \<Longrightarrow>
  1139        acb + acc < xu + xv \<or>
  1140        acb + acc = xu + xv \<Longrightarrow>
  1141        (yq < xu + xr \<or>
  1142         yq + zp < xu + (xr + xw)) \<or>
  1143        yq = xu + xr \<and>
  1144        yq + zp = xu + (xr + xw) \<Longrightarrow>
  1145        (zw < xw \<or>
  1146         zw < xw + xv \<or>
  1147         zw + zy < xw + (xv + xu)) \<or>
  1148        zw = xw \<and>
  1149        zw = xw + xv \<and>
  1150        zw + zy = xw + (xv + xu) \<Longrightarrow>
  1151        xs + yw < zs + zt \<or>
  1152        xs + yw = zs + zt \<Longrightarrow>
  1153        aab + xt < ye + yf \<or>
  1154        aab + xt = ye + yf \<Longrightarrow>
  1155        (ya + yb < yg + ye \<or>
  1156         ya + (yb + yc) < yg + (ye + yf)) \<or>
  1157        ya + yb = yg + ye \<and>
  1158        ya + (yb + yc) = yg + (ye + yf) \<Longrightarrow>
  1159        (xu + xv < acb + acc \<or>
  1160         xu + (xv + xw) < acb + (acc + acd)) \<or>
  1161        xu + xv = acb + acc \<and>
  1162        xu + (xv + xw) = acb + (acc + acd) \<Longrightarrow>
  1163        (zs < xz + zy \<or>
  1164         zs + xy < xz + (zy + zw)) \<or>
  1165        zs = xz + zy \<and>
  1166        zs + xy = xz + (zy + zw) \<Longrightarrow>
  1167        (zs + zt < xz + zy \<or>
  1168         zs + (zt + xy) < xz + (zy + zw)) \<or>
  1169        zs + zt = xz + zy \<and>
  1170        zs + (zt + xy) = xz + (zy + zw) \<Longrightarrow>
  1171        yg + ye < ya + yb \<or>
  1172        yg + ye = ya + yb \<Longrightarrow>
  1173        (abd < yc \<or> abd + abc < yc + yd) \<or>
  1174        abd = yc \<and> abd + abc = yc + yd \<Longrightarrow>
  1175        (ye + yf < adr + adq \<or>
  1176         ye + (yf + yg) < adr + (adq + adb)) \<or>
  1177        ye + yf = adr + adq \<and>
  1178        ye + (yf + yg) = adr + (adq + adb) \<Longrightarrow>
  1179        yh + yi < ym + yj \<or>
  1180        yh + yi = ym + yj \<Longrightarrow>
  1181        (abq < yl \<or> abq + abo < yl + ym) \<or>
  1182        abq = yl \<and> abq + abo = yl + ym \<Longrightarrow>
  1183        (yp < zp \<or>
  1184         yp < zp + zo \<or> 1 < zp + (zo + yq)) \<or>
  1185        yp = zp \<and>
  1186        yp = zp + zo \<and> 1 = zp + (zo + yq) \<Longrightarrow>
  1187        (abb + yr < aca \<or>
  1188         abb + (yr + abd) < aca + acf) \<or>
  1189        abb + yr = aca \<and>
  1190        abb + (yr + abd) = aca + acf \<Longrightarrow>
  1191        adw + zg < abe + ys \<or>
  1192        adw + zg = abe + ys \<Longrightarrow>
  1193        zd + abq < ys + abg \<or>
  1194        zd + abq = ys + abg \<Longrightarrow>
  1195        yt + abs1 < aby + abk \<or>
  1196        yt + abs1 = aby + abk \<Longrightarrow>
  1197        (yu < abx \<or>
  1198         yu < abx + aby \<or>
  1199         yu + yw < abx + (aby + abk)) \<or>
  1200        yu = abx \<and>
  1201        yu = abx + aby \<and>
  1202        yu + yw = abx + (aby + abk) \<Longrightarrow>
  1203        aaf < adv \<or> aaf = adv \<Longrightarrow>
  1204        abj + abk < yy + zb \<or>
  1205        abj + abk = yy + zb \<Longrightarrow>
  1206        (abb < yz \<or>
  1207         abb + abc < yz + za \<or>
  1208         abb + (abc + abd) < yz + (za + zb)) \<or>
  1209        abb = yz \<and>
  1210        abb + abc = yz + za \<and>
  1211        abb + (abc + abd) = yz + (za + zb) \<Longrightarrow>
  1212        (acg + zc < zd + abq \<or>
  1213         acg + (zc + ach)
  1214         < zd + (abq + abo)) \<or>
  1215        acg + zc = zd + abq \<and>
  1216        acg + (zc + ach) =
  1217        zd + (abq + abo) \<Longrightarrow>
  1218        zf < acm \<or> zf = acm \<Longrightarrow>
  1219        (zg + ady < acn + acm \<or>
  1220         zg + (ady + adw)
  1221         < acn + (acm + aco)) \<or>
  1222        zg + ady = acn + acm \<and>
  1223        zg + (ady + adw) =
  1224        acn + (acm + aco) \<Longrightarrow>
  1225        aay + zh < zi + zj \<or>
  1226        aay + zh = zi + zj \<Longrightarrow>
  1227        zy < zk \<or> zy = zk \<Longrightarrow>
  1228        (adn < zm + zn \<or>
  1229         adn + adl < zm + (zn + abv)) \<or>
  1230        adn = zm + zn \<and>
  1231        adn + adl = zm + (zn + abv) \<Longrightarrow>
  1232        zo + zp < zs + zt \<or>
  1233        zo + zp = zs + zt \<Longrightarrow>
  1234        zq + zr < zs + zt \<or>
  1235        zq + zr = zs + zt \<Longrightarrow>
  1236        (aai < adi \<or> aai < adi + adh) \<or>
  1237        aai = adi \<and> aai = adi + adh \<Longrightarrow>
  1238        (abr < acj \<or>
  1239         abr + (abs1 + zu)
  1240         < acj + (aci + ack)) \<or>
  1241        abr = acj \<and>
  1242        abr + (abs1 + zu) =
  1243        acj + (aci + ack) \<Longrightarrow>
  1244        (abl < zw \<or> 1 < zw + zy) \<or>
  1245        abl = zw \<and> 1 = zw + zy \<Longrightarrow>
  1246        (zz + aaa < act + acu \<or>
  1247         zz + (aaa + aab)
  1248         < act + (acu + aal)) \<or>
  1249        zz + aaa = act + acu \<and>
  1250        zz + (aaa + aab) =
  1251        act + (acu + aal) \<Longrightarrow>
  1252        (aam < aac \<or> aam + aao < aac + aaf) \<or>
  1253        aam = aac \<and> aam + aao = aac + aaf \<Longrightarrow>
  1254        (aak < aaf \<or> aak + aad < aaf + aag) \<or>
  1255        aak = aaf \<and> aak + aad = aaf + aag \<Longrightarrow>
  1256        (aah < aai \<or> aah + aav < aai + aak) \<or>
  1257        aah = aai \<and> aah + aav = aai + aak \<Longrightarrow>
  1258        act + (acu + aal) < aam + aao \<or>
  1259        act + (acu + aal) = aam + aao \<Longrightarrow>
  1260        (ads < aat \<or> 1 < aat + aas) \<or>
  1261        ads = aat \<and> 1 = aat + aas \<Longrightarrow>
  1262        (aba < aas \<or> aba + aay < aas + aat) \<or>
  1263        aba = aas \<and> aba + aay = aas + aat \<Longrightarrow>
  1264        acm < aav \<or> acm = aav \<Longrightarrow>
  1265        (ada < aay \<or> 1 < aay + aba) \<or>
  1266        ada = aay \<and> 1 = aay + aba \<Longrightarrow>
  1267        abb + (abc + abd) < abe + abg \<or>
  1268        abb + (abc + abd) = abe + abg \<Longrightarrow>
  1269        (abh < abj \<or> abh < abj + abk) \<or>
  1270        abh = abj \<and> abh = abj + abk \<Longrightarrow>
  1271        1 < abo + abq \<or> 1 = abo + abq \<Longrightarrow>
  1272        (acj < abr \<or> acj + aci < abr + abs1) \<or>
  1273        acj = abr \<and> acj + aci = abr + abs1 \<Longrightarrow>
  1274        (abt < abv \<or> abt + abu < abv + abw) \<or>
  1275        abt = abv \<and> abt + abu = abv + abw \<Longrightarrow>
  1276        (abx < adc \<or> abx + aby < adc + abz) \<or>
  1277        abx = adc \<and> abx + aby = adc + abz \<Longrightarrow>
  1278        (acf < acd \<or>
  1279         acf < acd + acc \<or>
  1280         1 < acd + (acc + acb)) \<or>
  1281        acf = acd \<and>
  1282        acf = acd + acc \<and>
  1283        1 = acd + (acc + acb) \<Longrightarrow>
  1284        acc + acd < acf \<or> acc + acd = acf \<Longrightarrow>
  1285        (acg < acq \<or> acg + ach < acq + acr) \<or>
  1286        acg = acq \<and> acg + ach = acq + acr \<Longrightarrow>
  1287        aci + (acj + ack) < acr + acp \<or>
  1288        aci + (acj + ack) = acr + acp \<Longrightarrow>
  1289        (acm < acp \<or>
  1290         acm + acn < acp + acq \<or>
  1291         acm + (acn + aco)
  1292         < acp + (acq + acr)) \<or>
  1293        acm = acp \<and>
  1294        acm + acn = acp + acq \<and>
  1295        acm + (acn + aco) =
  1296        acp + (acq + acr) \<Longrightarrow>
  1297        (acs + act < acw + acw \<or>
  1298         acs + (act + acu)
  1299         < acw + (acw + acw)) \<or>
  1300        acs + act = acw + acw \<and>
  1301        acs + (act + acu) =
  1302        acw + (acw + acw) \<Longrightarrow>
  1303        (ada < adb + adr \<or>
  1304         1 < adb + (adr + adq)) \<or>
  1305        ada = adb + adr \<and>
  1306        1 = adb + (adr + adq) \<Longrightarrow>
  1307        (adc + adc < adf + adg \<or>
  1308         adc + (adc + abz)
  1309         < adf + (adg + adk)) \<or>
  1310        adc + adc = adf + adg \<and>
  1311        adc + (adc + abz) =
  1312        adf + (adg + adk) \<Longrightarrow>
  1313        adh + adi < adj + adk \<or>
  1314        adh + adi = adj + adk \<Longrightarrow>
  1315        (adl < aec \<or> 1 < aec + adp) \<or>
  1316        adl = aec \<and> 1 = aec + adp \<Longrightarrow>
  1317        (adq < ads \<or> adq + adr < ads) \<or>
  1318        adq = ads \<and> adq + adr = ads \<Longrightarrow>
  1319        adu + adv < aed + aea \<or>
  1320        adu + adv = aed + aea \<Longrightarrow>
  1321        (adw < aee \<or> adw + ady < aee + aea) \<or>
  1322        adw = aee \<and> adw + ady = aee + aea \<Longrightarrow>
  1323        (aeb < aed \<or> aeb + aec < aed + aee) \<or>
  1324        aeb = aed \<and> aeb + aec = aed + aee \<Longrightarrow>
  1325        False"
  1326        by argo
  1327 
  1328 end