Theory Argo_Examples
section ‹Argo›
theory Argo_Examples
imports Complex_Main
begin
text ‹
This theory is intended to showcase and test different features of the ‹argo› proof method.
The ‹argo› proof method can be applied to propositional problems, problems involving equality
reasoning and problems of linear real arithmetic.
The ‹argo› proof method provides two options. To specify an upper limit of the proof methods
run time in seconds, use the option ‹argo_timeout›. To specify the amount of output, use the
option ‹argo_trace› with value ‹none› for no tracing output, value ‹basic› for viewing the
underlying propositions and some timings, and value ‹full› for additionally inspecting the
proof replay steps.
›
declare[[argo_trace = full]]
subsection ‹Propositional logic›
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 ‹Equality, congruence and predicates›
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 ¬True then a else b) = b" by argo
next
fix a b :: "'a"
have "(if ¬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 ≠ b" and "b = c"
then have "a ≠ c" by argo
next
fix a b c :: "'a"
assume "a ≠ b" and "a = c"
then have "c ≠ b" by argo
next
fix a b c d :: "'a"
assume "a = b" and "c = d" and "b ≠ d"
then have "a ≠ c" by argo
next
fix a b c d :: "'a"
assume "a = b" and "c = d" and "d ≠ b"
then have "a ≠ c" by argo
next
fix a b c d :: "'a"
assume "a = b" and "c = d" and "b ≠ d"
then have "c ≠ a" by argo
next
fix a b c d :: "'a"
assume "a = b" and "c = d" and "d ≠ b"
then have "c ≠ a" by argo
next
fix a b c d e f :: "'a"
assume "a ≠ b" and "b = c" and "b = d" and "d = e" and "a = f"
then have "f ≠ e" by argo
next
fix a b :: "'a" and f :: "'a ⇒ 'a"
assume "a = b"
then have "f a = f b" by argo
next
fix a b c :: "'a" and f :: "'a ⇒ 'a"
assume "f a = f b" and "b = c"
then have "f a = f c" by argo
next
fix a :: "'a" and f :: "'a ⇒ 'a"
assume "f a = a"
then have "f (f a) = a" by argo
next
fix a b :: "'a" and f g :: "'a ⇒ 'a"
assume "a = b"
then have "g (f a) = g (f b)" by argo
next
fix a b :: "'a" and f g :: "'a ⇒ '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 ⇒ 'a ⇒ 'a"
assume "a = b"
then have "g a b = g b a" by argo
next
fix a b :: "'a" and f :: "'a ⇒ 'a" and g :: "'a ⇒ 'a ⇒ '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 ⇒ 'a ⇒ '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 ⇒ bool"
assume "P a" and "a = b"
then have "P b" by argo
next
fix a b :: "'a" and P :: "'a ⇒ bool"
assume "~ P a" and "a = b"
then have "~ P b" by argo
next
fix a b c d :: "'a" and P :: "'a ⇒ 'a ⇒ 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 ⇒ 'a ⇒ bool"
assume "~ P a b" and "a = c" and "b = d"
then have "~ P c d" by argo
end
subsection ‹Linear real arithmetic›
subsubsection ‹Negation and subtraction›
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 ‹Multiplication›
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 ‹Division›
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 ‹Addition›
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 ‹Minimum and maximum›
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 ≤ b ⟶ min a b = a"
"a > b ⟶ min a b = b"
"min a b ≤ a"
"min a b ≤ 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 ≤ b ⟶ max a b = b"
"a > b ⟶ max a b = a"
"a ≤ max a b"
"b ≤ max a b"
"max a b = max b a"
by argo+
next
fix a b :: real
have
"min a b ≤ max a b"
"min a b + max a b = a + b"
"a < b ⟶ min a b < max a b"
by argo+
end
subsubsection ‹Absolute value›
notepad
begin
fix a :: real
have
"abs (3::real) = 3"
"abs (-3::real) = 3"
"0 ≤ abs a"
"a ≤ abs a"
"a ≥ 0 ⟶ abs a = a"
"a < 0 ⟶ abs a = -a"
"abs (abs a) = abs a"
by argo+
end
subsubsection ‹Equality›
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 ‹Less-equal›
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 ‹Less›
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 ‹Other examples›
notepad
begin
fix a b :: real
fix f :: "real ⇒ '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 ≤ b"
then have "0 ≤ b" 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 ≤ b"
then have "0 ≤ b" by argo
next
fix a b c :: real
assume "2 ≤ a" and "3 ≤ b" and "c ≤ 5"
then have "-2 * a + -3 * b + 5 * c < 13" by argo
next
fix a b c :: real
assume "2 ≤ a" and "3 ≤ b" and "c ≤ 5"
then have "-2 * a + -3 * b + 5 * c ≤ 12" by argo
next
fix a b :: real
assume "a = 2" and "b = 3"
then have "a + b > 5 ∨ 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 ∧ 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 ‹Larger examples›
declare[[argo_trace = basic, argo_timeout = 120]]
text ‹Translated from TPTP problem library: PUZ015-2.006.dimacs›
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 ‹Translated from TPTP problem library: MSC007-1.008.dimacs›
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 ≤ (yc::real) ∧
0 ≤ yd ∧ 0 ≤ yb ∧ 0 ≤ ya ⟹
0 ≤ yf ∧
0 ≤ xh ∧ 0 ≤ ye ∧ 0 ≤ yg ⟹
0 ≤ yw ∧ 0 ≤ xs ∧ 0 ≤ yu ⟹
0 ≤ aea ∧ 0 ≤ aee ∧ 0 ≤ aed ⟹
0 ≤ zy ∧ 0 ≤ xz ∧ 0 ≤ zw ⟹
0 ≤ zb ∧
0 ≤ za ∧ 0 ≤ yy ∧ 0 ≤ yz ⟹
0 ≤ zp ∧ 0 ≤ zo ∧ 0 ≤ yq ⟹
0 ≤ adp ∧ 0 ≤ aeb ∧ 0 ≤ aec ⟹
0 ≤ acm ∧ 0 ≤ aco ∧ 0 ≤ acn ⟹
0 ≤ abl ⟹
0 ≤ zr ∧ 0 ≤ zq ∧ 0 ≤ abh ⟹
0 ≤ abq ∧ 0 ≤ zd ∧ 0 ≤ abo ⟹
0 ≤ acd ∧
0 ≤ acc ∧ 0 ≤ xi ∧ 0 ≤ acb ⟹
0 ≤ acp ∧ 0 ≤ acr ∧ 0 ≤ acq ⟹
0 ≤ xw ∧
0 ≤ xr ∧ 0 ≤ xv ∧ 0 ≤ xu ⟹
0 ≤ zc ∧ 0 ≤ acg ∧ 0 ≤ ach ⟹
0 ≤ zt ∧ 0 ≤ zs ∧ 0 ≤ xy ⟹
0 ≤ ady ∧ 0 ≤ adw ∧ 0 ≤ zg ⟹
0 ≤ abd ∧
0 ≤ abc ∧ 0 ≤ yr ∧ 0 ≤ abb ⟹
0 ≤ adi ∧
0 ≤ x ∧ 0 ≤ adh ∧ 0 ≤ xa ⟹
0 ≤ aak ∧ 0 ≤ aai ∧ 0 ≤ aad ⟹
0 ≤ aba ∧ 0 ≤ zh ∧ 0 ≤ aay ⟹
0 ≤ abg ∧ 0 ≤ ys ∧ 0 ≤ abe ⟹
0 ≤ abs1 ∧
0 ≤ yt ∧ 0 ≤ abr ∧ 0 ≤ zu ⟹
0 ≤ abv ∧
0 ≤ zn ∧ 0 ≤ abw ∧ 0 ≤ zm ⟹
0 ≤ adl ∧ 0 ≤ adn ⟹
0 ≤ acf ∧ 0 ≤ aca ⟹
0 ≤ ads ∧ 0 ≤ aaq ⟹
0 ≤ ada ⟹
0 ≤ aaf ∧ 0 ≤ aac ∧ 0 ≤ aag ⟹
0 ≤ aal ∧
0 ≤ acu ∧ 0 ≤ acs ∧ 0 ≤ act ⟹
0 ≤ aas ∧ 0 ≤ xb ∧ 0 ≤ aat ⟹
0 ≤ zk ∧ 0 ≤ zj ∧ 0 ≤ zi ⟹
0 ≤ ack ∧
0 ≤ acj ∧ 0 ≤ xc ∧ 0 ≤ aci ⟹
0 ≤ aav ∧ 0 ≤ aah ∧ 0 ≤ xd ⟹
0 ≤ abt ∧
0 ≤ xo ∧ 0 ≤ abu ∧ 0 ≤ xn ⟹
0 ≤ adc ∧
0 ≤ abz ∧ 0 ≤ adc ∧ 0 ≤ abz ⟹
0 ≤ xt ∧
0 ≤ zz ∧ 0 ≤ aab ∧ 0 ≤ aaa ⟹
0 ≤ adq ∧
0 ≤ xl ∧ 0 ≤ adr ∧ 0 ≤ adb ⟹
0 ≤ zf ∧ 0 ≤ yh ∧ 0 ≤ yi ⟹
0 ≤ aao ∧ 0 ≤ aam ∧ 0 ≤ xe ⟹
0 ≤ abk ∧
0 ≤ aby ∧ 0 ≤ abj ∧ 0 ≤ abx ⟹
0 ≤ yp ⟹
0 ≤ yl ∧ 0 ≤ yj ∧ 0 ≤ ym ⟹
0 ≤ acw ⟹
0 ≤ adk ∧
0 ≤ adg ∧ 0 ≤ adj ∧ 0 ≤ adf ⟹
0 ≤ adv ∧ 0 ≤ xf ∧ 0 ≤ adu ⟹
yc + yd + yb + ya = 1 ⟹
yf + xh + ye + yg = 1 ⟹
yw + xs + yu = 1 ⟹
aea + aee + aed = 1 ⟹
zy + xz + zw = 1 ⟹
zb + za + yy + yz = 1 ⟹
zp + zo + yq = 1 ⟹
adp + aeb + aec = 1 ⟹
acm + aco + acn = 1 ⟹
abl + abl = 1 ⟹
zr + zq + abh = 1 ⟹
abq + zd + abo = 1 ⟹
acd + acc + xi + acb = 1 ⟹
acp + acr + acq = 1 ⟹
xw + xr + xv + xu = 1 ⟹
zc + acg + ach = 1 ⟹
zt + zs + xy = 1 ⟹
ady + adw + zg = 1 ⟹
abd + abc + yr + abb = 1 ⟹
adi + x + adh + xa = 1 ⟹
aak + aai + aad = 1 ⟹
aba + zh + aay = 1 ⟹
abg + ys + abe = 1 ⟹
abs1 + yt + abr + zu = 1 ⟹
abv + zn + abw + zm = 1 ⟹
adl + adn = 1 ⟹
acf + aca = 1 ⟹
ads + aaq = 1 ⟹
ada + ada = 1 ⟹
aaf + aac + aag = 1 ⟹
aal + acu + acs + act = 1 ⟹
aas + xb + aat = 1 ⟹
zk + zj + zi = 1 ⟹
ack + acj + xc + aci = 1 ⟹
aav + aah + xd = 1 ⟹
abt + xo + abu + xn = 1 ⟹
adc + abz + adc + abz = 1 ⟹
xt + zz + aab + aaa = 1 ⟹
adq + xl + adr + adb = 1 ⟹
zf + yh + yi = 1 ⟹
aao + aam + xe = 1 ⟹
abk + aby + abj + abx = 1 ⟹
yp + yp = 1 ⟹
yl + yj + ym = 1 ⟹
acw + acw + acw + acw = 1 ⟹
adk + adg + adj + adf = 1 ⟹
adv + xf + adu = 1 ⟹
yd = 0 ∨ yb = 0 ⟹
xh = 0 ∨ ye = 0 ⟹
yy = 0 ∨ za = 0 ⟹
acc = 0 ∨ xi = 0 ⟹
xv = 0 ∨ xr = 0 ⟹
yr = 0 ∨ abc = 0 ⟹
zn = 0 ∨ abw = 0 ⟹
xo = 0 ∨ abu = 0 ⟹
xl = 0 ∨ adr = 0 ⟹
(yr + abd < abl ∨
yr + (abd + abb) < 1) ∨
yr + abd = abl ∧
yr + (abd + abb) = 1 ⟹
adb + adr < xn + abu ∨
adb + adr = xn + abu ⟹
(abl < abt ∨ abl < abt + xo) ∨
abl = abt ∧ abl = abt + xo ⟹
yd + yc < abc + abd ∨
yd + yc = abc + abd ⟹
aca < abb + yr ∨ aca = abb + yr ⟹
acb + acc < xu + xv ∨
acb + acc = xu + xv ⟹
(yq < xu + xr ∨
yq + zp < xu + (xr + xw)) ∨
yq = xu + xr ∧
yq + zp = xu + (xr + xw) ⟹
(zw < xw ∨
zw < xw + xv ∨
zw + zy < xw + (xv + xu)) ∨
zw = xw ∧
zw = xw + xv ∧
zw + zy = xw + (xv + xu) ⟹
xs + yw < zs + zt ∨
xs + yw = zs + zt ⟹
aab + xt < ye + yf ∨
aab + xt = ye + yf ⟹
(ya + yb < yg + ye ∨
ya + (yb + yc) < yg + (ye + yf)) ∨
ya + yb = yg + ye ∧
ya + (yb + yc) = yg + (ye + yf) ⟹
(xu + xv < acb + acc ∨
xu + (xv + xw) < acb + (acc + acd)) ∨
xu + xv = acb + acc ∧
xu + (xv + xw) = acb + (acc + acd) ⟹
(zs < xz + zy ∨
zs + xy < xz + (zy + zw)) ∨
zs = xz + zy ∧
zs + xy = xz + (zy + zw) ⟹
(zs + zt < xz + zy ∨
zs + (zt + xy) < xz + (zy + zw)) ∨
zs + zt = xz + zy ∧
zs + (zt + xy) = xz + (zy + zw) ⟹
yg + ye < ya + yb ∨
yg + ye = ya + yb ⟹
(abd < yc ∨ abd + abc < yc + yd) ∨
abd = yc ∧ abd + abc = yc + yd ⟹
(ye + yf < adr + adq ∨
ye + (yf + yg) < adr + (adq + adb)) ∨
ye + yf = adr + adq ∧
ye + (yf + yg) = adr + (adq + adb) ⟹
yh + yi < ym + yj ∨
yh + yi = ym + yj ⟹
(abq < yl ∨ abq + abo < yl + ym) ∨
abq = yl ∧ abq + abo = yl + ym ⟹
(yp < zp ∨
yp < zp + zo ∨ 1 < zp + (zo + yq)) ∨
yp = zp ∧
yp = zp + zo ∧ 1 = zp + (zo + yq) ⟹
(abb + yr < aca ∨
abb + (yr + abd) < aca + acf) ∨
abb + yr = aca ∧
abb + (yr + abd) = aca + acf ⟹
adw + zg < abe + ys ∨
adw + zg = abe + ys ⟹
zd + abq < ys + abg ∨
zd + abq = ys + abg ⟹
yt + abs1 < aby + abk ∨
yt + abs1 = aby + abk ⟹
(yu < abx ∨
yu < abx + aby ∨
yu + yw < abx + (aby + abk)) ∨
yu = abx ∧
yu = abx + aby ∧
yu + yw = abx + (aby + abk) ⟹
aaf < adv ∨ aaf = adv ⟹
abj + abk < yy + zb ∨
abj + abk = yy + zb ⟹
(abb < yz ∨
abb + abc < yz + za ∨
abb + (abc + abd) < yz + (za + zb)) ∨
abb = yz ∧
abb + abc = yz + za ∧
abb + (abc + abd) = yz + (za + zb) ⟹
(acg + zc < zd + abq ∨
acg + (zc + ach)
< zd + (abq + abo)) ∨
acg + zc = zd + abq ∧
acg + (zc + ach) =
zd + (abq + abo) ⟹
zf < acm ∨ zf = acm ⟹
(zg + ady < acn + acm ∨
zg + (ady + adw)
< acn + (acm + aco)) ∨
zg + ady = acn + acm ∧
zg + (ady + adw) =
acn + (acm + aco) ⟹
aay + zh < zi + zj ∨
aay + zh = zi + zj ⟹
zy < zk ∨ zy = zk ⟹
(adn < zm + zn ∨
adn + adl < zm + (zn + abv)) ∨
adn = zm + zn ∧
adn + adl = zm + (zn + abv) ⟹
zo + zp < zs + zt ∨
zo + zp = zs + zt ⟹
zq + zr < zs + zt ∨
zq + zr = zs + zt ⟹
(aai < adi ∨ aai < adi + adh) ∨
aai = adi ∧ aai = adi + adh ⟹
(abr < acj ∨
abr + (abs1 + zu)
< acj + (aci + ack)) ∨
abr = acj ∧
abr + (abs1 + zu) =
acj + (aci + ack) ⟹
(abl < zw ∨ 1 < zw + zy) ∨
abl = zw ∧ 1 = zw + zy ⟹
(zz + aaa < act + acu ∨
zz + (aaa + aab)
< act + (acu + aal)) ∨
zz + aaa = act + acu ∧
zz + (aaa + aab) =
act + (acu + aal) ⟹
(aam < aac ∨ aam + aao < aac + aaf) ∨
aam = aac ∧ aam + aao = aac + aaf ⟹
(aak < aaf ∨ aak + aad < aaf + aag) ∨
aak = aaf ∧ aak + aad = aaf + aag ⟹
(aah < aai ∨ aah + aav < aai + aak) ∨
aah = aai ∧ aah + aav = aai + aak ⟹
act + (acu + aal) < aam + aao ∨
act + (acu + aal) = aam + aao ⟹
(ads < aat ∨ 1 < aat + aas) ∨
ads = aat ∧ 1 = aat + aas ⟹
(aba < aas ∨ aba + aay < aas + aat) ∨
aba = aas ∧ aba + aay = aas + aat ⟹
acm < aav ∨ acm = aav ⟹
(ada < aay ∨ 1 < aay + aba) ∨
ada = aay ∧ 1 = aay + aba ⟹
abb + (abc + abd) < abe + abg ∨
abb + (abc + abd) = abe + abg ⟹
(abh < abj ∨ abh < abj + abk) ∨
abh = abj ∧ abh = abj + abk ⟹
1 < abo + abq ∨ 1 = abo + abq ⟹
(acj < abr ∨ acj + aci < abr + abs1) ∨
acj = abr ∧ acj + aci = abr + abs1 ⟹
(abt < abv ∨ abt + abu < abv + abw) ∨
abt = abv ∧ abt + abu = abv + abw ⟹
(abx < adc ∨ abx + aby < adc + abz) ∨
abx = adc ∧ abx + aby = adc + abz ⟹
(acf < acd ∨
acf < acd + acc ∨
1 < acd + (acc + acb)) ∨
acf = acd ∧
acf = acd + acc ∧
1 = acd + (acc + acb) ⟹
acc + acd < acf ∨ acc + acd = acf ⟹
(acg < acq ∨ acg + ach < acq + acr) ∨
acg = acq ∧ acg + ach = acq + acr ⟹
aci + (acj + ack) < acr + acp ∨
aci + (acj + ack) = acr + acp ⟹
(acm < acp ∨
acm + acn < acp + acq ∨
acm + (acn + aco)
< acp + (acq + acr)) ∨
acm = acp ∧
acm + acn = acp + acq ∧
acm + (acn + aco) =
acp + (acq + acr) ⟹
(acs + act < acw + acw ∨
acs + (act + acu)
< acw + (acw + acw)) ∨
acs + act = acw + acw ∧
acs + (act + acu) =
acw + (acw + acw) ⟹
(ada < adb + adr ∨
1 < adb + (adr + adq)) ∨
ada = adb + adr ∧
1 = adb + (adr + adq) ⟹
(adc + adc < adf + adg ∨
adc + (adc + abz)
< adf + (adg + adk)) ∨
adc + adc = adf + adg ∧
adc + (adc + abz) =
adf + (adg + adk) ⟹
adh + adi < adj + adk ∨
adh + adi = adj + adk ⟹
(adl < aec ∨ 1 < aec + adp) ∨
adl = aec ∧ 1 = aec + adp ⟹
(adq < ads ∨ adq + adr < ads) ∨
adq = ads ∧ adq + adr = ads ⟹
adu + adv < aed + aea ∨
adu + adv = aed + aea ⟹
(adw < aee ∨ adw + ady < aee + aea) ∨
adw = aee ∧ adw + ady = aee + aea ⟹
(aeb < aed ∨ aeb + aec < aed + aee) ∨
aeb = aed ∧ aeb + aec = aed + aee ⟹
False"
by argo
end