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