src/HOL/ex/Argo_Examples.thy

more data integrity: name vs. address;

(*  Title:      HOL/ex/Argo_Examples.thy
    Author:     Sascha Boehme
*)

section \<open>Argo\<close>

theory Argo_Examples
imports Complex_Main
begin

text \<open>
  This theory is intended to showcase and test different features of the \<open>argo\<close> proof method.

  The \<open>argo\<close> proof method can be applied to propositional problems, problems involving equality
  reasoning and problems of linear real arithmetic.

  The \<open>argo\<close> proof method provides two options. To specify an upper limit of the proof methods
  run time in seconds, use the option \<open>argo_timeout\<close>. To specify the amount of output, use the
  option \<open>argo_trace\<close> with value \<open>none\<close> for no tracing output, value \<open>basic\<close> for viewing the
  underlying propositions and some timings, and value \<open>full\<close> for additionally inspecting the
  proof replay steps.
\<close>

declare[[argo_trace = full]]

subsection \<open>Propositional logic\<close>

notepad
begin
  have "True" by argo
next
  have "~False" by argo
next
  fix P :: bool
  assume "False"
  then have "P" by argo
next
  fix P :: bool
  assume "~True"
  then have "P" by argo
next
  fix P :: bool
  assume "P"
  then have "P" by argo
next
  fix P :: bool
  assume "~~P"
  then have "P" by argo
next
  fix P Q R :: bool
  assume "P & Q & R"
  then have "R & P & Q" by argo
next
  fix P Q R :: bool
  assume "P & (Q & True & R) & (Q & P) & True"
  then have "R & P & Q" by argo
next
  fix P Q1 Q2 Q3 Q4 Q5 :: bool
  assume "Q1 & (Q2 & P & Q3) & (Q4 & ~P & Q5)"
  then have "~True" by argo
next
  fix P Q1 Q2 Q3  :: bool
  assume "(Q1 & False) & Q2 & Q3"
  then have "P::bool" by argo
next
  fix P Q R :: bool
  assume "P | Q | R"
  then have "R | P | Q" by argo
next
  fix P Q R :: bool
  assume "P | (Q | False | R) | (Q | P) | False"
  then have "R | P | Q" by argo
next
  fix P Q1 Q2 Q3 Q4 :: bool
  have "(Q1 & P & Q2) --> False | (Q3 | (Q4 | P) | False)" by argo
next
  fix Q1 Q2 Q3 Q4 :: bool
  have "Q1 | (Q2 | True | Q3) | Q4" by argo
next
  fix P Q R :: bool
  assume "(P & Q) | (P & ~Q) | (P & R) | (P & ~R)"
  then have "P" by argo
next
  fix P :: bool
  assume "P = True"
  then have "P" by argo
next
  fix P :: bool
  assume "False = P"
  then have "~P" by argo
next
  fix P Q :: bool
  assume "P = (~P)"
  then have "Q" by argo
next
  fix P :: bool
  have "(~P) = (~P)" by argo
next
  fix P Q :: bool
  assume "P" and "~Q"
  then have "P = (~Q)" by argo
next
  fix P Q :: bool
  assume "((P::bool) = Q) | (Q = P)"
  then have "(P --> Q) & (Q --> P)" by argo
next
  fix P Q :: bool
  assume "(P::bool) = Q"
  then have "Q = P" by argo
next
  fix P Q R :: bool
  assume "if P then Q else R"
  then have "Q | R" by argo
next
  fix P Q :: bool
  assume "P | Q"
     and "P | ~Q"
     and "~P | Q"
     and "~P | ~Q"
  then have "False" by argo
next
  fix P Q R :: bool
  assume "P | Q | R"
     and "P | Q | ~R"
     and "P | ~Q | R"
     and "P | ~Q | ~R"
     and "~P | Q | R"
     and "~P | Q | ~R"
     and "~P | ~Q | R"
     and "~P | ~Q | ~R"
  then have "False" by argo
next
  fix a b c d e f g h i j k l m n p q :: bool
  assume "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
  then have "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" by argo
next
  fix P :: bool
  have "P=P=P=P=P=P=P=P=P=P" by argo
next
  fix a b c d e f p q x :: bool
  assume "a | b | c | d"
     and "e | f | (a & d)"
     and "~(a | (c & ~c)) | b"
     and "~(b & (x | ~x)) | c"
     and "~(d | False) | c"
     and "~(c | (~p & (p | (q & ~q))))"
  then have "False" by argo
next
  have "(True & True & True) = True" by argo
next
  have "(False | False | False) = False" by argo
end


subsection \<open>Equality, congruence and predicates\<close>

notepad
begin
  fix t :: "'a"
  have "t = t" by argo
next
  fix t u :: "'a"
  assume "t = u"
  then have "u = t" by argo
next
  fix s t u :: "'a"
  assume "s = t" and "t = u"
  then have "s = u" by argo
next
  fix s t u v :: "'a"
  assume "s = t" and "t = u" and "u = v" and "u = s"
  then have "s = v" by argo
next
  fix s t u v w :: "'a"
  assume "s = t" and "t = u" and "s = v" and "v = w"
  then have "w = u" by argo
next
  fix s t u a b c :: "'a"
  assume "s = t" and "t = u" and "a = b" and "b = c"
  then have "s = a --> c = u" by argo
next
  fix a b c d :: "'a"
  assume "(a = b & b = c) | (a = d & d = c)"
  then have "a = c" by argo
next
  fix a b1 b2 b3 b4 c d :: "'a"
  assume "(a = b1 & ((b1 = b2 & b2 = b3) | (b1 = b4 & b4 = b3)) & b3 = c) | (a = d & d = c)"
  then have "a = c" by argo
next
  fix a b :: "'a"
  have "(if True then a else b) = a" by argo
next
  fix a b :: "'a"
  have "(if False then a else b) = b" by argo
next
  fix a b :: "'a"
  have "(if \<not>True then a else b) = b" by argo
next
  fix a b :: "'a"
  have "(if \<not>False then a else b) = a" by argo
next
  fix P :: "bool"
  fix a :: "'a"
  have "(if P then a else a) = a" by argo
next
  fix P :: "bool"
  fix a b c :: "'a"
  assume "P" and "a = c"
  then have "(if P then a else b) = c" by argo
next
  fix P :: "bool"
  fix a b c :: "'a"
  assume "~P" and "b = c"
  then have "(if P then a else b) = c" by argo
next
  fix P Q :: "bool"
  fix a b c d :: "'a"
  assume "P" and "Q" and "a = d"
  then have "(if P then (if Q then a else b) else c) = d" by argo
next
  fix a b c :: "'a"
  assume "a \<noteq> b" and "b = c"
  then have "a \<noteq> c" by argo
next
  fix a b c :: "'a"
  assume "a \<noteq> b" and "a = c"
  then have "c \<noteq> b" by argo
next
  fix a b c d :: "'a"
  assume "a = b" and "c = d" and "b \<noteq> d"
  then have "a \<noteq> c" by argo
next
  fix a b c d :: "'a"
  assume "a = b" and "c = d" and "d \<noteq> b"
  then have "a \<noteq> c" by argo
next
  fix a b c d :: "'a"
  assume "a = b" and "c = d" and "b \<noteq> d"
  then have "c \<noteq> a" by argo
next
  fix a b c d :: "'a"
  assume "a = b" and "c = d" and "d \<noteq> b"
  then have "c \<noteq> a" by argo
next
  fix a b c d e f :: "'a"
  assume "a \<noteq> b" and "b = c" and "b = d" and "d = e" and "a = f"
  then have "f \<noteq> e" by argo
next
  fix a b :: "'a" and f :: "'a \<Rightarrow> 'a"
  assume "a = b"
  then have "f a = f b" by argo
next
  fix a b c :: "'a" and f :: "'a \<Rightarrow> 'a"
  assume "f a = f b" and "b = c"
  then have "f a = f c" by argo
next
  fix a :: "'a" and f :: "'a \<Rightarrow> 'a"
  assume "f a = a"
  then have "f (f a) = a" by argo
next
  fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
  assume "a = b"
  then have "g (f a) = g (f b)" by argo
next
  fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
  assume "f a = b" and "g b = a"
  then have "f (g (f a)) = b" by argo
next
  fix a b :: "'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assume "a = b"
  then have "g a b = g b a" by argo
next
  fix a b :: "'a" and f :: "'a \<Rightarrow> 'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assume "f a = b"
  then have "g (f a) b = g b (f a)" by argo
next
  fix a b c d e g h :: "'a" and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assume "c = d" and "e = c" and "e = b" and "b = h" and "f g h = d" and "f g d = a"
  then have "a = b" by argo
next
  fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
  assume "P a" and "a = b"
  then have "P b" by argo
next
  fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
  assume "~ P a" and "a = b"
  then have "~ P b" by argo
next
  fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assume "P a b" and "a = c" and "b = d"
  then have "P c d" by argo
next
  fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assume "~ P a b" and "a = c" and "b = d"
  then have "~ P c d" by argo
end


subsection \<open>Linear real arithmetic\<close>

subsubsection \<open>Negation and subtraction\<close>

notepad
begin
  fix a b :: real
  have
    "-a = -1 * a"
    "-(-a) = a"
    "a - b = a + -1 * b"
    "a - (-b) = a + b"
    by argo+
end


subsubsection \<open>Multiplication\<close>

notepad
begin
  fix a b c d :: real
  have
    "(2::real) * 3 = 6"
    "0 * a = 0"
    "a * 0 = 0"
    "1 * a = a"
    "a * 1 = a"
    "2 * a = a * 2"
    "2 * a * 3 = 6 * a"
    "2 * a * 3 * 5 = 30 * a"
    "2 * (a * (3 * 5)) = 30 * a"
    "a * 0 * b = 0"
    "a * (0 * b) = 0"
    "a * b = b * a"
    "a * b * a = b * a * a"
    "a * (b * c) = (a * b) * c"
    "a * (b * (c * d)) = ((a * b) * c) * d"
    "a * (b * (c * d)) = ((d * c) * b) * a"
    "a * (b + c + d) = a * b + a * c + a * d"
    "(a + b + c) * d = a * d + b * d + c * d"
    by argo+
end


subsubsection \<open>Division\<close>

notepad
begin
  fix a b c d :: real
  have
    "(6::real) / 2 = 3"
    "a / 0 = a / 0"
    "a / 0 <= a / 0"
    "~(a / 0 < a / 0)"
    "0 / a = 0"
    "a / 1 = a"
    "a / 3 = 1/3 * a"
    "6 * a / 2 = 3 * a"
    "(6 * a) / 2 = 3 * a"
    "a / ((5 * b) / 2) = 2/5 * a / b"
    "a / (5 * (b / 2)) = 2/5 * a / b"
    "(a / 5) * (b / 2) = 1/10 * a * b"
    "a / (3 * b) = 1/3 * a / b"
    "(a + b) / 5 = 1/5 * a + 1/5 * b"
    "a / (5 * 1/5) = a"
    "a * (b / c) = (b * a) / c"
    "(a / b) * c = (c * a) / b"
    "(a / b) / (c / d) = (a * d) / (c * b)"
    "1 / (a * b) = 1 / (b * a)"
    "a / (3 * b) = 1 / 3 * a / b"
    "(a + b + c) / d = a / d + b / d + c / d"
    by argo+
end


subsubsection \<open>Addition\<close>

notepad
begin
  fix a b c d :: real
  have
    "a + b = b + a"
    "a + b + c = c + b + a"
    "a + b + c + d = d + c + b + a"
    "a + (b + (c + d)) = ((a + b) + c) + d"
    "(5::real) + -3 = 2"
    "(3::real) + 5 + -1 = 7"
    "2 + a = a + 2"
    "a + b + a = b + 2 * a"
    "-1 + a + -1 + 2 + b + 5/3 + b + 1/3 + 5 * b + 2/3 = 8/3 + a + 7 * b"
    "1 + b + b + 5 * b + 3 * a + 7 + a + 2 = 10 + 4 * a + 7 * b"
    by argo+
end


subsubsection \<open>Minimum and maximum\<close>

notepad
begin
  fix a b :: real
  have
    "min (3::real) 5 = 3"
    "min (5::real) 3 = 3"
    "min (3::real) (-5) = -5"
    "min (-5::real) 3 = -5"
    "min a a = a"
    "a \<le> b \<longrightarrow> min a b = a"
    "a > b \<longrightarrow> min a b = b"
    "min a b \<le> a"
    "min a b \<le> b"
    "min a b = min b a"
    by argo+
next
  fix a b :: real
  have
    "max (3::real) 5 = 5"
    "max (5::real) 3 = 5"
    "max (3::real) (-5) = 3"
    "max (-5::real) 3 = 3"
    "max a a = a"
    "a \<le> b \<longrightarrow> max a b = b"
    "a > b \<longrightarrow> max a b = a"
    "a \<le> max a b"
    "b \<le> max a b"
    "max a b = max b a"
    by argo+
next
  fix a b :: real
  have
    "min a b \<le> max a b"
    "min a b + max a b = a + b"
    "a < b \<longrightarrow> min a b < max a b"
    by argo+
end


subsubsection \<open>Absolute value\<close>

notepad
begin
  fix a :: real
  have
    "abs (3::real) = 3"
    "abs (-3::real) = 3"
    "0 \<le> abs a"
    "a \<le> abs a"
    "a \<ge> 0 \<longrightarrow> abs a = a"
    "a < 0 \<longrightarrow> abs a = -a"
    "abs (abs a) = abs a"
    by argo+
end


subsubsection \<open>Equality\<close>

notepad
begin
  fix a b c d :: real
  have
    "(3::real) = 3"
    "~((3::real) = 4)"
    "~((4::real) = 3)"
    "3 * a = 5 --> a = 5/3"
    "-3 * a = 5 --> -5/3 = a"
    "5 = 3 * a --> 5/3  = a "
    "5 = -3 * a --> a = -5/3"
    "2 + 3 * a = 4 --> a = 2/3"
    "4 = 2 + 3 * a --> 2/3 = a"
    "2 + 3 * a + 5 * b + c = 4 --> 3 * a + 5 * b + c = 2"
    "4 = 2 + 3 * a + 5 * b + c --> 2 = 3 * a + 5 * b + c"
    "-2 * a + b + -3 * c = 7 --> -7 = 2 * a + -1 * b + 3 * c"
    "7 = -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c = -7"
    "-2 * a + b + -3 * c + 4 * d = 7 --> -7 = 2 * a + -1 * b + 3 * c + -4 * d"
    "7 = -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d = -7"
    "a + 3 * b = 5 * c + b --> a + 2 * b + -5 * c = 0"
    by argo+
end


subsubsection \<open>Less-equal\<close>

notepad
begin
  fix a b c d :: real
  have
    "(3::real) <= 3"
    "(3::real) <= 4"
    "~((4::real) <= 3)"
    "3 * a <= 5 --> a <= 5/3"
    "-3 * a <= 5 --> -5/3 <= a"
    "5 <= 3 * a --> 5/3  <= a "
    "5 <= -3 * a --> a <= -5/3"
    "2 + 3 * a <= 4 --> a <= 2/3"
    "4 <= 2 + 3 * a --> 2/3 <= a"
    "2 + 3 * a + 5 * b + c <= 4 --> 3 * a + 5 * b + c <= 2"
    "4 <= 2 + 3 * a + 5 * b + c --> 2 <= 3 * a + 5 * b + c"
    "-2 * a + b + -3 * c <= 7 --> -7 <= 2 * a + -1 * b + 3 * c"
    "7 <= -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c <= -7"
    "-2 * a + b + -3 * c + 4 * d <= 7 --> -7 <= 2 * a + -1 * b + 3 * c + -4 * d"
    "7 <= -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d <= -7"
    "a + 3 * b <= 5 * c + b --> a + 2 * b + -5 * c <= 0"
    by argo+
end

subsubsection \<open>Less\<close>

notepad
begin
  fix a b c d :: real
  have
    "(3::real) < 4"
    "~((3::real) < 3)"
    "~((4::real) < 3)"
    "3 * a < 5 --> a < 5/3"
    "-3 * a < 5 --> -5/3 < a"
    "5 < 3 * a --> 5/3  < a "
    "5 < -3 * a --> a < -5/3"
    "2 + 3 * a < 4 --> a < 2/3"
    "4 < 2 + 3 * a --> 2/3 < a"
    "2 + 3 * a + 5 * b + c < 4 --> 3 * a + 5 * b + c < 2"
    "4 < 2 + 3 * a + 5 * b + c --> 2 < 3 * a + 5 * b + c"
    "-2 * a + b + -3 * c < 7 --> -7 < 2 * a + -1 * b + 3 * c"
    "7 < -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c < -7"
    "-2 * a + b + -3 * c + 4 * d < 7 --> -7 < 2 * a + -1 * b + 3 * c + -4 * d"
    "7 < -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d < -7"
    "a + 3 * b < 5 * c + b --> a + 2 * b + -5 * c < 0"
    by argo+
end


subsubsection \<open>Other examples\<close>

notepad
begin
  fix a b :: real
  fix f :: "real \<Rightarrow> 'a"
  have "f (a + b) = f (b + a)" by argo
next
  have
    "(0::real) < 1"
    "(47::real) + 11 < 8 * 15"
    by argo+
next
  fix a :: real
  assume "a < 3"
  then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
next
  fix a :: real
  assume "a <= 3"
  then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
next
  fix a :: real
  assume "~(3 < a)"
  then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
next
  fix a :: real
  assume "~(3 <= a)"
  then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
next
  fix a :: real
  have "a < 3 | a = 3 | a > 3" by argo
next
  fix a b :: real
  assume "0 < a" and "a < b"
  then have "0 < b" by argo
next
  fix a b :: real
  assume "0 < a" and "a \<le> b"
  then have "0 \<le> b" by argo
next
  fix a b :: real
  assume "0 \<le> a" and "a < b"
  then have "0 \<le> b" by argo
next
  fix a b :: real
  assume "0 \<le> a" and "a \<le> b"
  then have "0 \<le> b" by argo
next
  fix a b c :: real
  assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
  then have "-2 * a + -3 * b + 5 * c < 13" by argo
next
  fix a b c :: real
  assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
  then have "-2 * a + -3 * b + 5 * c \<le> 12" by argo
next
  fix a b :: real
  assume "a = 2" and "b = 3"
  then have "a + b > 5 \<or> a < b" by argo
next
  fix a b c :: real
  assume "5 < b + c" and "a + c < 0" and "a > 0"
  then have "b > 0" by argo
next
  fix a b c :: real
  assume "a + b < 7" and "5 < b + c" and "a + c < 0" and "a > 0"
  then have "0 < b \<and> b < 7" by argo
next
  fix a b c :: real
  assume "a < b" and "b < c" and "c < a"
  then have "False" by argo
next
  fix a b :: real
  assume "a - 5 > b"
  then have "b < a" by argo
next
  fix a b :: real
  have "(a - b) - a = (a - a) - b" by argo
next
  fix n m n' m' :: real
  have "
    (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
    (n = n' & n' < m) | (n = m & m < n') |
    (n' < m & m < n) | (n' < m & m = n) |
    (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
    (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
    (m = n & n < n') | (m = n' & n' < n) |
    (n' = m & m = n)"
    by argo
end


subsection \<open>Larger examples\<close>

declare[[argo_trace = basic, argo_timeout = 120]]


text \<open>Translated from TPTP problem library: PUZ015-2.006.dimacs\<close>

lemma assumes 1: "~x0"
  and 2: "~x30"
  and 3: "~x29"
  and 4: "~x59"
  and 5: "x1 | x31 | x0"
  and 6: "x2 | x32 | x1"
  and 7: "x3 | x33 | x2"
  and 8: "x4 | x34 | x3"
  and 9: "x35 | x4"
  and 10: "x5 | x36 | x30"
  and 11: "x6 | x37 | x5 | x31"
  and 12: "x7 | x38 | x6 | x32"
  and 13: "x8 | x39 | x7 | x33"
  and 14: "x9 | x40 | x8 | x34"
  and 15: "x41 | x9 | x35"
  and 16: "x10 | x42 | x36"
  and 17: "x11 | x43 | x10 | x37"
  and 18: "x12 | x44 | x11 | x38"
  and 19: "x13 | x45 | x12 | x39"
  and 20: "x14 | x46 | x13 | x40"
  and 21: "x47 | x14 | x41"
  and 22: "x15 | x48 | x42"
  and 23: "x16 | x49 | x15 | x43"
  and 24: "x17 | x50 | x16 | x44"
  and 25: "x18 | x51 | x17 | x45"
  and 26: "x19 | x52 | x18 | x46"
  and 27: "x53 | x19 | x47"
  and 28: "x20 | x54 | x48"
  and 29: "x21 | x55 | x20 | x49"
  and 30: "x22 | x56 | x21 | x50"
  and 31: "x23 | x57 | x22 | x51"
  and 32: "x24 | x58 | x23 | x52"
  and 33: "x59 | x24 | x53"
  and 34: "x25 | x54"
  and 35: "x26 | x25 | x55"
  and 36: "x27 | x26 | x56"
  and 37: "x28 | x27 | x57"
  and 38: "x29 | x28 | x58"
  and 39: "~x1 | ~x31"
  and 40: "~x1 | ~x0"
  and 41: "~x31 | ~x0"
  and 42: "~x2 | ~x32"
  and 43: "~x2 | ~x1"
  and 44: "~x32 | ~x1"
  and 45: "~x3 | ~x33"
  and 46: "~x3 | ~x2"
  and 47: "~x33 | ~x2"
  and 48: "~x4 | ~x34"
  and 49: "~x4 | ~x3"
  and 50: "~x34 | ~x3"
  and 51: "~x35 | ~x4"
  and 52: "~x5 | ~x36"
  and 53: "~x5 | ~x30"
  and 54: "~x36 | ~x30"
  and 55: "~x6 | ~x37"
  and 56: "~x6 | ~x5"
  and 57: "~x6 | ~x31"
  and 58: "~x37 | ~x5"
  and 59: "~x37 | ~x31"
  and 60: "~x5 | ~x31"
  and 61: "~x7 | ~x38"
  and 62: "~x7 | ~x6"
  and 63: "~x7 | ~x32"
  and 64: "~x38 | ~x6"
  and 65: "~x38 | ~x32"
  and 66: "~x6 | ~x32"
  and 67: "~x8 | ~x39"
  and 68: "~x8 | ~x7"
  and 69: "~x8 | ~x33"
  and 70: "~x39 | ~x7"
  and 71: "~x39 | ~x33"
  and 72: "~x7 | ~x33"
  and 73: "~x9 | ~x40"
  and 74: "~x9 | ~x8"
  and 75: "~x9 | ~x34"
  and 76: "~x40 | ~x8"
  and 77: "~x40 | ~x34"
  and 78: "~x8 | ~x34"
  and 79: "~x41 | ~x9"
  and 80: "~x41 | ~x35"
  and 81: "~x9 | ~x35"
  and 82: "~x10 | ~x42"
  and 83: "~x10 | ~x36"
  and 84: "~x42 | ~x36"
  and 85: "~x11 | ~x43"
  and 86: "~x11 | ~x10"
  and 87: "~x11 | ~x37"
  and 88: "~x43 | ~x10"
  and 89: "~x43 | ~x37"
  and 90: "~x10 | ~x37"
  and 91: "~x12 | ~x44"
  and 92: "~x12 | ~x11"
  and 93: "~x12 | ~x38"
  and 94: "~x44 | ~x11"
  and 95: "~x44 | ~x38"
  and 96: "~x11 | ~x38"
  and 97: "~x13 | ~x45"
  and 98: "~x13 | ~x12"
  and 99: "~x13 | ~x39"
  and 100: "~x45 | ~x12"
  and 101: "~x45 | ~x39"
  and 102: "~x12 | ~x39"
  and 103: "~x14 | ~x46"
  and 104: "~x14 | ~x13"
  and 105: "~x14 | ~x40"
  and 106: "~x46 | ~x13"
  and 107: "~x46 | ~x40"
  and 108: "~x13 | ~x40"
  and 109: "~x47 | ~x14"
  and 110: "~x47 | ~x41"
  and 111: "~x14 | ~x41"
  and 112: "~x15 | ~x48"
  and 113: "~x15 | ~x42"
  and 114: "~x48 | ~x42"
  and 115: "~x16 | ~x49"
  and 116: "~x16 | ~x15"
  and 117: "~x16 | ~x43"
  and 118: "~x49 | ~x15"
  and 119: "~x49 | ~x43"
  and 120: "~x15 | ~x43"
  and 121: "~x17 | ~x50"
  and 122: "~x17 | ~x16"
  and 123: "~x17 | ~x44"
  and 124: "~x50 | ~x16"
  and 125: "~x50 | ~x44"
  and 126: "~x16 | ~x44"
  and 127: "~x18 | ~x51"
  and 128: "~x18 | ~x17"
  and 129: "~x18 | ~x45"
  and 130: "~x51 | ~x17"
  and 131: "~x51 | ~x45"
  and 132: "~x17 | ~x45"
  and 133: "~x19 | ~x52"
  and 134: "~x19 | ~x18"
  and 135: "~x19 | ~x46"
  and 136: "~x52 | ~x18"
  and 137: "~x52 | ~x46"
  and 138: "~x18 | ~x46"
  and 139: "~x53 | ~x19"
  and 140: "~x53 | ~x47"
  and 141: "~x19 | ~x47"
  and 142: "~x20 | ~x54"
  and 143: "~x20 | ~x48"
  and 144: "~x54 | ~x48"
  and 145: "~x21 | ~x55"
  and 146: "~x21 | ~x20"
  and 147: "~x21 | ~x49"
  and 148: "~x55 | ~x20"
  and 149: "~x55 | ~x49"
  and 150: "~x20 | ~x49"
  and 151: "~x22 | ~x56"
  and 152: "~x22 | ~x21"
  and 153: "~x22 | ~x50"
  and 154: "~x56 | ~x21"
  and 155: "~x56 | ~x50"
  and 156: "~x21 | ~x50"
  and 157: "~x23 | ~x57"
  and 158: "~x23 | ~x22"
  and 159: "~x23 | ~x51"
  and 160: "~x57 | ~x22"
  and 161: "~x57 | ~x51"
  and 162: "~x22 | ~x51"
  and 163: "~x24 | ~x58"
  and 164: "~x24 | ~x23"
  and 165: "~x24 | ~x52"
  and 166: "~x58 | ~x23"
  and 167: "~x58 | ~x52"
  and 168: "~x23 | ~x52"
  and 169: "~x59 | ~x24"
  and 170: "~x59 | ~x53"
  and 171: "~x24 | ~x53"
  and 172: "~x25 | ~x54"
  and 173: "~x26 | ~x25"
  and 174: "~x26 | ~x55"
  and 175: "~x25 | ~x55"
  and 176: "~x27 | ~x26"
  and 177: "~x27 | ~x56"
  and 178: "~x26 | ~x56"
  and 179: "~x28 | ~x27"
  and 180: "~x28 | ~x57"
  and 181: "~x27 | ~x57"
  and 182: "~x29 | ~x28"
  and 183: "~x29 | ~x58"
  and 184: "~x28 | ~x58"
  shows "False"
    using assms
    by argo


text \<open>Translated from TPTP problem library: MSC007-1.008.dimacs\<close>

lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
  and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
  and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
  and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
  and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
  and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
  and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
  and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
  and 9: "~x0 | ~x7"
  and 10: "~x0 | ~x14"
  and 11: "~x0 | ~x21"
  and 12: "~x0 | ~x28"
  and 13: "~x0 | ~x35"
  and 14: "~x0 | ~x42"
  and 15: "~x0 | ~x49"
  and 16: "~x7 | ~x14"
  and 17: "~x7 | ~x21"
  and 18: "~x7 | ~x28"
  and 19: "~x7 | ~x35"
  and 20: "~x7 | ~x42"
  and 21: "~x7 | ~x49"
  and 22: "~x14 | ~x21"
  and 23: "~x14 | ~x28"
  and 24: "~x14 | ~x35"
  and 25: "~x14 | ~x42"
  and 26: "~x14 | ~x49"
  and 27: "~x21 | ~x28"
  and 28: "~x21 | ~x35"
  and 29: "~x21 | ~x42"
  and 30: "~x21 | ~x49"
  and 31: "~x28 | ~x35"
  and 32: "~x28 | ~x42"
  and 33: "~x28 | ~x49"
  and 34: "~x35 | ~x42"
  and 35: "~x35 | ~x49"
  and 36: "~x42 | ~x49"
  and 37: "~x1 | ~x8"
  and 38: "~x1 | ~x15"
  and 39: "~x1 | ~x22"
  and 40: "~x1 | ~x29"
  and 41: "~x1 | ~x36"
  and 42: "~x1 | ~x43"
  and 43: "~x1 | ~x50"
  and 44: "~x8 | ~x15"
  and 45: "~x8 | ~x22"
  and 46: "~x8 | ~x29"
  and 47: "~x8 | ~x36"
  and 48: "~x8 | ~x43"
  and 49: "~x8 | ~x50"
  and 50: "~x15 | ~x22"
  and 51: "~x15 | ~x29"
  and 52: "~x15 | ~x36"
  and 53: "~x15 | ~x43"
  and 54: "~x15 | ~x50"
  and 55: "~x22 | ~x29"
  and 56: "~x22 | ~x36"
  and 57: "~x22 | ~x43"
  and 58: "~x22 | ~x50"
  and 59: "~x29 | ~x36"
  and 60: "~x29 | ~x43"
  and 61: "~x29 | ~x50"
  and 62: "~x36 | ~x43"
  and 63: "~x36 | ~x50"
  and 64: "~x43 | ~x50"
  and 65: "~x2 | ~x9"
  and 66: "~x2 | ~x16"
  and 67: "~x2 | ~x23"
  and 68: "~x2 | ~x30"
  and 69: "~x2 | ~x37"
  and 70: "~x2 | ~x44"
  and 71: "~x2 | ~x51"
  and 72: "~x9 | ~x16"
  and 73: "~x9 | ~x23"
  and 74: "~x9 | ~x30"
  and 75: "~x9 | ~x37"
  and 76: "~x9 | ~x44"
  and 77: "~x9 | ~x51"
  and 78: "~x16 | ~x23"
  and 79: "~x16 | ~x30"
  and 80: "~x16 | ~x37"
  and 81: "~x16 | ~x44"
  and 82: "~x16 | ~x51"
  and 83: "~x23 | ~x30"
  and 84: "~x23 | ~x37"
  and 85: "~x23 | ~x44"
  and 86: "~x23 | ~x51"
  and 87: "~x30 | ~x37"
  and 88: "~x30 | ~x44"
  and 89: "~x30 | ~x51"
  and 90: "~x37 | ~x44"
  and 91: "~x37 | ~x51"
  and 92: "~x44 | ~x51"
  and 93: "~x3 | ~x10"
  and 94: "~x3 | ~x17"
  and 95: "~x3 | ~x24"
  and 96: "~x3 | ~x31"
  and 97: "~x3 | ~x38"
  and 98: "~x3 | ~x45"
  and 99: "~x3 | ~x52"
  and 100: "~x10 | ~x17"
  and 101: "~x10 | ~x24"
  and 102: "~x10 | ~x31"
  and 103: "~x10 | ~x38"
  and 104: "~x10 | ~x45"
  and 105: "~x10 | ~x52"
  and 106: "~x17 | ~x24"
  and 107: "~x17 | ~x31"
  and 108: "~x17 | ~x38"
  and 109: "~x17 | ~x45"
  and 110: "~x17 | ~x52"
  and 111: "~x24 | ~x31"
  and 112: "~x24 | ~x38"
  and 113: "~x24 | ~x45"
  and 114: "~x24 | ~x52"
  and 115: "~x31 | ~x38"
  and 116: "~x31 | ~x45"
  and 117: "~x31 | ~x52"
  and 118: "~x38 | ~x45"
  and 119: "~x38 | ~x52"
  and 120: "~x45 | ~x52"
  and 121: "~x4 | ~x11"
  and 122: "~x4 | ~x18"
  and 123: "~x4 | ~x25"
  and 124: "~x4 | ~x32"
  and 125: "~x4 | ~x39"
  and 126: "~x4 | ~x46"
  and 127: "~x4 | ~x53"
  and 128: "~x11 | ~x18"
  and 129: "~x11 | ~x25"
  and 130: "~x11 | ~x32"
  and 131: "~x11 | ~x39"
  and 132: "~x11 | ~x46"
  and 133: "~x11 | ~x53"
  and 134: "~x18 | ~x25"
  and 135: "~x18 | ~x32"
  and 136: "~x18 | ~x39"
  and 137: "~x18 | ~x46"
  and 138: "~x18 | ~x53"
  and 139: "~x25 | ~x32"
  and 140: "~x25 | ~x39"
  and 141: "~x25 | ~x46"
  and 142: "~x25 | ~x53"
  and 143: "~x32 | ~x39"
  and 144: "~x32 | ~x46"
  and 145: "~x32 | ~x53"
  and 146: "~x39 | ~x46"
  and 147: "~x39 | ~x53"
  and 148: "~x46 | ~x53"
  and 149: "~x5 | ~x12"
  and 150: "~x5 | ~x19"
  and 151: "~x5 | ~x26"
  and 152: "~x5 | ~x33"
  and 153: "~x5 | ~x40"
  and 154: "~x5 | ~x47"
  and 155: "~x5 | ~x54"
  and 156: "~x12 | ~x19"
  and 157: "~x12 | ~x26"
  and 158: "~x12 | ~x33"
  and 159: "~x12 | ~x40"
  and 160: "~x12 | ~x47"
  and 161: "~x12 | ~x54"
  and 162: "~x19 | ~x26"
  and 163: "~x19 | ~x33"
  and 164: "~x19 | ~x40"
  and 165: "~x19 | ~x47"
  and 166: "~x19 | ~x54"
  and 167: "~x26 | ~x33"
  and 168: "~x26 | ~x40"
  and 169: "~x26 | ~x47"
  and 170: "~x26 | ~x54"
  and 171: "~x33 | ~x40"
  and 172: "~x33 | ~x47"
  and 173: "~x33 | ~x54"
  and 174: "~x40 | ~x47"
  and 175: "~x40 | ~x54"
  and 176: "~x47 | ~x54"
  and 177: "~x6 | ~x13"
  and 178: "~x6 | ~x20"
  and 179: "~x6 | ~x27"
  and 180: "~x6 | ~x34"
  and 181: "~x6 | ~x41"
  and 182: "~x6 | ~x48"
  and 183: "~x6 | ~x55"
  and 184: "~x13 | ~x20"
  and 185: "~x13 | ~x27"
  and 186: "~x13 | ~x34"
  and 187: "~x13 | ~x41"
  and 188: "~x13 | ~x48"
  and 189: "~x13 | ~x55"
  and 190: "~x20 | ~x27"
  and 191: "~x20 | ~x34"
  and 192: "~x20 | ~x41"
  and 193: "~x20 | ~x48"
  and 194: "~x20 | ~x55"
  and 195: "~x27 | ~x34"
  and 196: "~x27 | ~x41"
  and 197: "~x27 | ~x48"
  and 198: "~x27 | ~x55"
  and 199: "~x34 | ~x41"
  and 200: "~x34 | ~x48"
  and 201: "~x34 | ~x55"
  and 202: "~x41 | ~x48"
  and 203: "~x41 | ~x55"
  and 204: "~x48 | ~x55"
  shows "False"
    using assms
    by argo


lemma "0 \<le> (yc::real) \<and>
       0 \<le> yd \<and> 0 \<le> yb \<and> 0 \<le> ya \<Longrightarrow>
       0 \<le> yf \<and>
       0 \<le> xh \<and> 0 \<le> ye \<and> 0 \<le> yg \<Longrightarrow>
       0 \<le> yw \<and> 0 \<le> xs \<and> 0 \<le> yu \<Longrightarrow>
       0 \<le> aea \<and> 0 \<le> aee \<and> 0 \<le> aed \<Longrightarrow>
       0 \<le> zy \<and> 0 \<le> xz \<and> 0 \<le> zw \<Longrightarrow>
       0 \<le> zb \<and>
       0 \<le> za \<and> 0 \<le> yy \<and> 0 \<le> yz \<Longrightarrow>
       0 \<le> zp \<and> 0 \<le> zo \<and> 0 \<le> yq \<Longrightarrow>
       0 \<le> adp \<and> 0 \<le> aeb \<and> 0 \<le> aec \<Longrightarrow>
       0 \<le> acm \<and> 0 \<le> aco \<and> 0 \<le> acn \<Longrightarrow>
       0 \<le> abl \<Longrightarrow>
       0 \<le> zr \<and> 0 \<le> zq \<and> 0 \<le> abh \<Longrightarrow>
       0 \<le> abq \<and> 0 \<le> zd \<and> 0 \<le> abo \<Longrightarrow>
       0 \<le> acd \<and>
       0 \<le> acc \<and> 0 \<le> xi \<and> 0 \<le> acb \<Longrightarrow>
       0 \<le> acp \<and> 0 \<le> acr \<and> 0 \<le> acq \<Longrightarrow>
       0 \<le> xw \<and>
       0 \<le> xr \<and> 0 \<le> xv \<and> 0 \<le> xu \<Longrightarrow>
       0 \<le> zc \<and> 0 \<le> acg \<and> 0 \<le> ach \<Longrightarrow>
       0 \<le> zt \<and> 0 \<le> zs \<and> 0 \<le> xy \<Longrightarrow>
       0 \<le> ady \<and> 0 \<le> adw \<and> 0 \<le> zg \<Longrightarrow>
       0 \<le> abd \<and>
       0 \<le> abc \<and> 0 \<le> yr \<and> 0 \<le> abb \<Longrightarrow>
       0 \<le> adi \<and>
       0 \<le> x \<and> 0 \<le> adh \<and> 0 \<le> xa \<Longrightarrow>
       0 \<le> aak \<and> 0 \<le> aai \<and> 0 \<le> aad \<Longrightarrow>
       0 \<le> aba \<and> 0 \<le> zh \<and> 0 \<le> aay \<Longrightarrow>
       0 \<le> abg \<and> 0 \<le> ys \<and> 0 \<le> abe \<Longrightarrow>
       0 \<le> abs1 \<and>
       0 \<le> yt \<and> 0 \<le> abr \<and> 0 \<le> zu \<Longrightarrow>
       0 \<le> abv \<and>
       0 \<le> zn \<and> 0 \<le> abw \<and> 0 \<le> zm \<Longrightarrow>
       0 \<le> adl \<and> 0 \<le> adn \<Longrightarrow>
       0 \<le> acf \<and> 0 \<le> aca \<Longrightarrow>
       0 \<le> ads \<and> 0 \<le> aaq \<Longrightarrow>
       0 \<le> ada \<Longrightarrow>
       0 \<le> aaf \<and> 0 \<le> aac \<and> 0 \<le> aag \<Longrightarrow>
       0 \<le> aal \<and>
       0 \<le> acu \<and> 0 \<le> acs \<and> 0 \<le> act \<Longrightarrow>
       0 \<le> aas \<and> 0 \<le> xb \<and> 0 \<le> aat \<Longrightarrow>
       0 \<le> zk \<and> 0 \<le> zj \<and> 0 \<le> zi \<Longrightarrow>
       0 \<le> ack \<and>
       0 \<le> acj \<and> 0 \<le> xc \<and> 0 \<le> aci \<Longrightarrow>
       0 \<le> aav \<and> 0 \<le> aah \<and> 0 \<le> xd \<Longrightarrow>
       0 \<le> abt \<and>
       0 \<le> xo \<and> 0 \<le> abu \<and> 0 \<le> xn \<Longrightarrow>
       0 \<le> adc \<and>
       0 \<le> abz \<and> 0 \<le> adc \<and> 0 \<le> abz \<Longrightarrow>
       0 \<le> xt \<and>
       0 \<le> zz \<and> 0 \<le> aab \<and> 0 \<le> aaa \<Longrightarrow>
       0 \<le> adq \<and>
       0 \<le> xl \<and> 0 \<le> adr \<and> 0 \<le> adb \<Longrightarrow>
       0 \<le> zf \<and> 0 \<le> yh \<and> 0 \<le> yi \<Longrightarrow>
       0 \<le> aao \<and> 0 \<le> aam \<and> 0 \<le> xe \<Longrightarrow>
       0 \<le> abk \<and>
       0 \<le> aby \<and> 0 \<le> abj \<and> 0 \<le> abx \<Longrightarrow>
       0 \<le> yp \<Longrightarrow>
       0 \<le> yl \<and> 0 \<le> yj \<and> 0 \<le> ym \<Longrightarrow>
       0 \<le> acw \<Longrightarrow>
       0 \<le> adk \<and>
       0 \<le> adg \<and> 0 \<le> adj \<and> 0 \<le> adf \<Longrightarrow>
       0 \<le> adv \<and> 0 \<le> xf \<and> 0 \<le> adu \<Longrightarrow>
       yc + yd + yb + ya = 1 \<Longrightarrow>
       yf + xh + ye + yg = 1 \<Longrightarrow>
       yw + xs + yu = 1 \<Longrightarrow>
       aea + aee + aed = 1 \<Longrightarrow>
       zy + xz + zw = 1 \<Longrightarrow>
       zb + za + yy + yz = 1 \<Longrightarrow>
       zp + zo + yq = 1 \<Longrightarrow>
       adp + aeb + aec = 1 \<Longrightarrow>
       acm + aco + acn = 1 \<Longrightarrow>
       abl + abl = 1 \<Longrightarrow>
       zr + zq + abh = 1 \<Longrightarrow>
       abq + zd + abo = 1 \<Longrightarrow>
       acd + acc + xi + acb = 1 \<Longrightarrow>
       acp + acr + acq = 1 \<Longrightarrow>
       xw + xr + xv + xu = 1 \<Longrightarrow>
       zc + acg + ach = 1 \<Longrightarrow>
       zt + zs + xy = 1 \<Longrightarrow>
       ady + adw + zg = 1 \<Longrightarrow>
       abd + abc + yr + abb = 1 \<Longrightarrow>
       adi + x + adh + xa = 1 \<Longrightarrow>
       aak + aai + aad = 1 \<Longrightarrow>
       aba + zh + aay = 1 \<Longrightarrow>
       abg + ys + abe = 1 \<Longrightarrow>
       abs1 + yt + abr + zu = 1 \<Longrightarrow>
       abv + zn + abw + zm = 1 \<Longrightarrow>
       adl + adn = 1 \<Longrightarrow>
       acf + aca = 1 \<Longrightarrow>
       ads + aaq = 1 \<Longrightarrow>
       ada + ada = 1 \<Longrightarrow>
       aaf + aac + aag = 1 \<Longrightarrow>
       aal + acu + acs + act = 1 \<Longrightarrow>
       aas + xb + aat = 1 \<Longrightarrow>
       zk + zj + zi = 1 \<Longrightarrow>
       ack + acj + xc + aci = 1 \<Longrightarrow>
       aav + aah + xd = 1 \<Longrightarrow>
       abt + xo + abu + xn = 1 \<Longrightarrow>
       adc + abz + adc + abz = 1 \<Longrightarrow>
       xt + zz + aab + aaa = 1 \<Longrightarrow>
       adq + xl + adr + adb = 1 \<Longrightarrow>
       zf + yh + yi = 1 \<Longrightarrow>
       aao + aam + xe = 1 \<Longrightarrow>
       abk + aby + abj + abx = 1 \<Longrightarrow>
       yp + yp = 1 \<Longrightarrow>
       yl + yj + ym = 1 \<Longrightarrow>
       acw + acw + acw + acw = 1 \<Longrightarrow>
       adk + adg + adj + adf = 1 \<Longrightarrow>
       adv + xf + adu = 1 \<Longrightarrow>
       yd = 0 \<or> yb = 0 \<Longrightarrow>
       xh = 0 \<or> ye = 0 \<Longrightarrow>
       yy = 0 \<or> za = 0 \<Longrightarrow>
       acc = 0 \<or> xi = 0 \<Longrightarrow>
       xv = 0 \<or> xr = 0 \<Longrightarrow>
       yr = 0 \<or> abc = 0 \<Longrightarrow>
       zn = 0 \<or> abw = 0 \<Longrightarrow>
       xo = 0 \<or> abu = 0 \<Longrightarrow>
       xl = 0 \<or> adr = 0 \<Longrightarrow>
       (yr + abd < abl \<or>
        yr + (abd + abb) < 1) \<or>
       yr + abd = abl \<and>
       yr + (abd + abb) = 1 \<Longrightarrow>
       adb + adr < xn + abu \<or>
       adb + adr = xn + abu \<Longrightarrow>
       (abl < abt \<or> abl < abt + xo) \<or>
       abl = abt \<and> abl = abt + xo \<Longrightarrow>
       yd + yc < abc + abd \<or>
       yd + yc = abc + abd \<Longrightarrow>
       aca < abb + yr \<or> aca = abb + yr \<Longrightarrow>
       acb + acc < xu + xv \<or>
       acb + acc = xu + xv \<Longrightarrow>
       (yq < xu + xr \<or>
        yq + zp < xu + (xr + xw)) \<or>
       yq = xu + xr \<and>
       yq + zp = xu + (xr + xw) \<Longrightarrow>
       (zw < xw \<or>
        zw < xw + xv \<or>
        zw + zy < xw + (xv + xu)) \<or>
       zw = xw \<and>
       zw = xw + xv \<and>
       zw + zy = xw + (xv + xu) \<Longrightarrow>
       xs + yw < zs + zt \<or>
       xs + yw = zs + zt \<Longrightarrow>
       aab + xt < ye + yf \<or>
       aab + xt = ye + yf \<Longrightarrow>
       (ya + yb < yg + ye \<or>
        ya + (yb + yc) < yg + (ye + yf)) \<or>
       ya + yb = yg + ye \<and>
       ya + (yb + yc) = yg + (ye + yf) \<Longrightarrow>
       (xu + xv < acb + acc \<or>
        xu + (xv + xw) < acb + (acc + acd)) \<or>
       xu + xv = acb + acc \<and>
       xu + (xv + xw) = acb + (acc + acd) \<Longrightarrow>
       (zs < xz + zy \<or>
        zs + xy < xz + (zy + zw)) \<or>
       zs = xz + zy \<and>
       zs + xy = xz + (zy + zw) \<Longrightarrow>
       (zs + zt < xz + zy \<or>
        zs + (zt + xy) < xz + (zy + zw)) \<or>
       zs + zt = xz + zy \<and>
       zs + (zt + xy) = xz + (zy + zw) \<Longrightarrow>
       yg + ye < ya + yb \<or>
       yg + ye = ya + yb \<Longrightarrow>
       (abd < yc \<or> abd + abc < yc + yd) \<or>
       abd = yc \<and> abd + abc = yc + yd \<Longrightarrow>
       (ye + yf < adr + adq \<or>
        ye + (yf + yg) < adr + (adq + adb)) \<or>
       ye + yf = adr + adq \<and>
       ye + (yf + yg) = adr + (adq + adb) \<Longrightarrow>
       yh + yi < ym + yj \<or>
       yh + yi = ym + yj \<Longrightarrow>
       (abq < yl \<or> abq + abo < yl + ym) \<or>
       abq = yl \<and> abq + abo = yl + ym \<Longrightarrow>
       (yp < zp \<or>
        yp < zp + zo \<or> 1 < zp + (zo + yq)) \<or>
       yp = zp \<and>
       yp = zp + zo \<and> 1 = zp + (zo + yq) \<Longrightarrow>
       (abb + yr < aca \<or>
        abb + (yr + abd) < aca + acf) \<or>
       abb + yr = aca \<and>
       abb + (yr + abd) = aca + acf \<Longrightarrow>
       adw + zg < abe + ys \<or>
       adw + zg = abe + ys \<Longrightarrow>
       zd + abq < ys + abg \<or>
       zd + abq = ys + abg \<Longrightarrow>
       yt + abs1 < aby + abk \<or>
       yt + abs1 = aby + abk \<Longrightarrow>
       (yu < abx \<or>
        yu < abx + aby \<or>
        yu + yw < abx + (aby + abk)) \<or>
       yu = abx \<and>
       yu = abx + aby \<and>
       yu + yw = abx + (aby + abk) \<Longrightarrow>
       aaf < adv \<or> aaf = adv \<Longrightarrow>
       abj + abk < yy + zb \<or>
       abj + abk = yy + zb \<Longrightarrow>
       (abb < yz \<or>
        abb + abc < yz + za \<or>
        abb + (abc + abd) < yz + (za + zb)) \<or>
       abb = yz \<and>
       abb + abc = yz + za \<and>
       abb + (abc + abd) = yz + (za + zb) \<Longrightarrow>
       (acg + zc < zd + abq \<or>
        acg + (zc + ach)
        < zd + (abq + abo)) \<or>
       acg + zc = zd + abq \<and>
       acg + (zc + ach) =
       zd + (abq + abo) \<Longrightarrow>
       zf < acm \<or> zf = acm \<Longrightarrow>
       (zg + ady < acn + acm \<or>
        zg + (ady + adw)
        < acn + (acm + aco)) \<or>
       zg + ady = acn + acm \<and>
       zg + (ady + adw) =
       acn + (acm + aco) \<Longrightarrow>
       aay + zh < zi + zj \<or>
       aay + zh = zi + zj \<Longrightarrow>
       zy < zk \<or> zy = zk \<Longrightarrow>
       (adn < zm + zn \<or>
        adn + adl < zm + (zn + abv)) \<or>
       adn = zm + zn \<and>
       adn + adl = zm + (zn + abv) \<Longrightarrow>
       zo + zp < zs + zt \<or>
       zo + zp = zs + zt \<Longrightarrow>
       zq + zr < zs + zt \<or>
       zq + zr = zs + zt \<Longrightarrow>
       (aai < adi \<or> aai < adi + adh) \<or>
       aai = adi \<and> aai = adi + adh \<Longrightarrow>
       (abr < acj \<or>
        abr + (abs1 + zu)
        < acj + (aci + ack)) \<or>
       abr = acj \<and>
       abr + (abs1 + zu) =
       acj + (aci + ack) \<Longrightarrow>
       (abl < zw \<or> 1 < zw + zy) \<or>
       abl = zw \<and> 1 = zw + zy \<Longrightarrow>
       (zz + aaa < act + acu \<or>
        zz + (aaa + aab)
        < act + (acu + aal)) \<or>
       zz + aaa = act + acu \<and>
       zz + (aaa + aab) =
       act + (acu + aal) \<Longrightarrow>
       (aam < aac \<or> aam + aao < aac + aaf) \<or>
       aam = aac \<and> aam + aao = aac + aaf \<Longrightarrow>
       (aak < aaf \<or> aak + aad < aaf + aag) \<or>
       aak = aaf \<and> aak + aad = aaf + aag \<Longrightarrow>
       (aah < aai \<or> aah + aav < aai + aak) \<or>
       aah = aai \<and> aah + aav = aai + aak \<Longrightarrow>
       act + (acu + aal) < aam + aao \<or>
       act + (acu + aal) = aam + aao \<Longrightarrow>
       (ads < aat \<or> 1 < aat + aas) \<or>
       ads = aat \<and> 1 = aat + aas \<Longrightarrow>
       (aba < aas \<or> aba + aay < aas + aat) \<or>
       aba = aas \<and> aba + aay = aas + aat \<Longrightarrow>
       acm < aav \<or> acm = aav \<Longrightarrow>
       (ada < aay \<or> 1 < aay + aba) \<or>
       ada = aay \<and> 1 = aay + aba \<Longrightarrow>
       abb + (abc + abd) < abe + abg \<or>
       abb + (abc + abd) = abe + abg \<Longrightarrow>
       (abh < abj \<or> abh < abj + abk) \<or>
       abh = abj \<and> abh = abj + abk \<Longrightarrow>
       1 < abo + abq \<or> 1 = abo + abq \<Longrightarrow>
       (acj < abr \<or> acj + aci < abr + abs1) \<or>
       acj = abr \<and> acj + aci = abr + abs1 \<Longrightarrow>
       (abt < abv \<or> abt + abu < abv + abw) \<or>
       abt = abv \<and> abt + abu = abv + abw \<Longrightarrow>
       (abx < adc \<or> abx + aby < adc + abz) \<or>
       abx = adc \<and> abx + aby = adc + abz \<Longrightarrow>
       (acf < acd \<or>
        acf < acd + acc \<or>
        1 < acd + (acc + acb)) \<or>
       acf = acd \<and>
       acf = acd + acc \<and>
       1 = acd + (acc + acb) \<Longrightarrow>
       acc + acd < acf \<or> acc + acd = acf \<Longrightarrow>
       (acg < acq \<or> acg + ach < acq + acr) \<or>
       acg = acq \<and> acg + ach = acq + acr \<Longrightarrow>
       aci + (acj + ack) < acr + acp \<or>
       aci + (acj + ack) = acr + acp \<Longrightarrow>
       (acm < acp \<or>
        acm + acn < acp + acq \<or>
        acm + (acn + aco)
        < acp + (acq + acr)) \<or>
       acm = acp \<and>
       acm + acn = acp + acq \<and>
       acm + (acn + aco) =
       acp + (acq + acr) \<Longrightarrow>
       (acs + act < acw + acw \<or>
        acs + (act + acu)
        < acw + (acw + acw)) \<or>
       acs + act = acw + acw \<and>
       acs + (act + acu) =
       acw + (acw + acw) \<Longrightarrow>
       (ada < adb + adr \<or>
        1 < adb + (adr + adq)) \<or>
       ada = adb + adr \<and>
       1 = adb + (adr + adq) \<Longrightarrow>
       (adc + adc < adf + adg \<or>
        adc + (adc + abz)
        < adf + (adg + adk)) \<or>
       adc + adc = adf + adg \<and>
       adc + (adc + abz) =
       adf + (adg + adk) \<Longrightarrow>
       adh + adi < adj + adk \<or>
       adh + adi = adj + adk \<Longrightarrow>
       (adl < aec \<or> 1 < aec + adp) \<or>
       adl = aec \<and> 1 = aec + adp \<Longrightarrow>
       (adq < ads \<or> adq + adr < ads) \<or>
       adq = ads \<and> adq + adr = ads \<Longrightarrow>
       adu + adv < aed + aea \<or>
       adu + adv = aed + aea \<Longrightarrow>
       (adw < aee \<or> adw + ady < aee + aea) \<or>
       adw = aee \<and> adw + ady = aee + aea \<Longrightarrow>
       (aeb < aed \<or> aeb + aec < aed + aee) \<or>
       aeb = aed \<and> aeb + aec = aed + aee \<Longrightarrow>
       False"
       by argo

end