From 176b52e0b6c31a4021db101023e3e263c82595f6 Mon Sep 17 00:00:00 2001 From: Marcelo Rinesi Date: Thu, 26 Sep 2024 19:21:16 -0300 Subject: [PATCH] Script to generate a list of Most Wanted Implications --- scripts/generate_most_wanted_list.py | 64 ++++++ scripts/most_wanted.md | 328 +++++++++++++++++++++++++++ 2 files changed, 392 insertions(+) create mode 100644 scripts/generate_most_wanted_list.py create mode 100644 scripts/most_wanted.md diff --git a/scripts/generate_most_wanted_list.py b/scripts/generate_most_wanted_list.py new file mode 100644 index 00000000..5555db25 --- /dev/null +++ b/scripts/generate_most_wanted_list.py @@ -0,0 +1,64 @@ +#! /usr/bin/env python3 + +""" +Example usage: + +```sh +$ python scripts/generate_most_wanted_list.py equational_theories/Basic.lean +$ less most_wanted.md +``` +""" + +from process_implications import * +from itertools import product +from datetime import datetime + +def close(known_implies): + # copilot wrote this + new_pairs = closure = set(known_implies) + while new_pairs: + new_pairs = { + (a, d) + for a, b in new_pairs + for c, d in known_implies + if b == c + } - closure + closure |= new_pairs + return closure + +if __name__ == '__main__': + try: + file_name = argv[1] + assert os.path.exists(file_name) + except: + print('Usage: python generate_most_wanted_list.py ') + exit(1) + + + universe, known_implies, known_not_implies = parse_proofs_file(file_name) + known_implies = close(known_implies) + + ascendants = defaultdict(int) # equation -> equations it's implied by + descendants = defaultdict(int) # equation -> equations it implies + for a, b in known_implies: + if a != b: + descendants[a] += 1 + ascendants[b] += 1 + + + edge_value = {} # (a, b) -> value of the a->b implication + for a, b in product(universe, universe): + if (a,b) in known_implies or (a,b) in known_not_implies: + continue + + # This doesn't work with cycles + v = ascendants[a] + descendants[b] + # speed things up by not recording explicitly zero-value edges + if v > 0: + edge_value[(a,b)] = v + + with open('most_wanted.md', 'w+') as fh: + fh.write(f"# Most Wanted list of implications as of ({datetime.now().strftime('%Y-%m-%d %H:%M:%S')})" + "\n\n") + for a,b in sorted(edge_value, key=lambda ab:edge_value[ab], reverse=True): + fh.write(f"* `{a}` -> `{b}` (implied by {ascendants[a]} -> implies {descendants[b]} = {edge_value[(a,b)]})"+'\n') + diff --git a/scripts/most_wanted.md b/scripts/most_wanted.md new file mode 100644 index 00000000..efe3006a --- /dev/null +++ b/scripts/most_wanted.md @@ -0,0 +1,328 @@ +# Most Wanted list of implications as of (2024-09-26 19:19:59) + +* `Equation1` -> `Equation2` (implied by 20 -> implies 13 = 33) +* `Equation1` -> `Equation6` (implied by 20 -> implies 13 = 33) +* `Equation1` -> `Equation7` (implied by 20 -> implies 13 = 33) +* `Equation1` -> `Equation46` (implied by 20 -> implies 8 = 28) +* `Equation1` -> `Equation4` (implied by 20 -> implies 6 = 26) +* `Equation1` -> `Equation4582` (implied by 20 -> implies 4 = 24) +* `Equation1` -> `Equation4552` (implied by 20 -> implies 3 = 23) +* `Equation1` -> `Equation387` (implied by 20 -> implies 2 = 22) +* `Equation1` -> `Equation4513` (implied by 20 -> implies 2 = 22) +* `Equation1` -> `Equation3` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation5` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation8` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation38` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation39` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation40` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation41` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation42` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation43` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation168` (implied by 20 -> implies 1 = 21) +* `Equation1` -> `Equation4512` (implied by 20 -> implies 1 = 21) +* `Equation4512` -> `Equation2` (implied by 8 -> implies 13 = 21) +* `Equation4512` -> `Equation6` (implied by 8 -> implies 13 = 21) +* `Equation4512` -> `Equation7` (implied by 8 -> implies 13 = 21) +* `Equation4513` -> `Equation2` (implied by 7 -> implies 13 = 20) +* `Equation4513` -> `Equation6` (implied by 7 -> implies 13 = 20) +* `Equation4513` -> `Equation7` (implied by 7 -> implies 13 = 20) +* `Equation4552` -> `Equation2` (implied by 6 -> implies 13 = 19) +* `Equation4552` -> `Equation6` (implied by 6 -> implies 13 = 19) +* `Equation4552` -> `Equation7` (implied by 6 -> implies 13 = 19) +* `Equation42` -> `Equation2` (implied by 5 -> implies 13 = 18) +* `Equation42` -> `Equation6` (implied by 5 -> implies 13 = 18) +* `Equation42` -> `Equation7` (implied by 5 -> implies 13 = 18) +* `Equation43` -> `Equation2` (implied by 5 -> implies 13 = 18) +* `Equation43` -> `Equation6` (implied by 5 -> implies 13 = 18) +* `Equation43` -> `Equation7` (implied by 5 -> implies 13 = 18) +* `Equation3` -> `Equation2` (implied by 4 -> implies 13 = 17) +* `Equation3` -> `Equation6` (implied by 4 -> implies 13 = 17) +* `Equation3` -> `Equation7` (implied by 4 -> implies 13 = 17) +* `Equation387` -> `Equation2` (implied by 4 -> implies 13 = 17) +* `Equation387` -> `Equation6` (implied by 4 -> implies 13 = 17) +* `Equation387` -> `Equation7` (implied by 4 -> implies 13 = 17) +* `Equation4582` -> `Equation2` (implied by 4 -> implies 13 = 17) +* `Equation4582` -> `Equation6` (implied by 4 -> implies 13 = 17) +* `Equation4582` -> `Equation7` (implied by 4 -> implies 13 = 17) +* `Equation4` -> `Equation2` (implied by 3 -> implies 13 = 16) +* `Equation4` -> `Equation6` (implied by 3 -> implies 13 = 16) +* `Equation4` -> `Equation7` (implied by 3 -> implies 13 = 16) +* `Equation46` -> `Equation2` (implied by 3 -> implies 13 = 16) +* `Equation46` -> `Equation6` (implied by 3 -> implies 13 = 16) +* `Equation46` -> `Equation7` (implied by 3 -> implies 13 = 16) +* `Equation4512` -> `Equation46` (implied by 8 -> implies 8 = 16) +* `Equation4513` -> `Equation46` (implied by 7 -> implies 8 = 15) +* `Equation4512` -> `Equation4` (implied by 8 -> implies 6 = 14) +* `Equation4552` -> `Equation46` (implied by 6 -> implies 8 = 14) +* `Equation5` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation5` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation5` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation8` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation8` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation8` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation38` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation38` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation38` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation39` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation39` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation39` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation40` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation40` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation40` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation41` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation41` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation41` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation42` -> `Equation46` (implied by 5 -> implies 8 = 13) +* `Equation43` -> `Equation46` (implied by 5 -> implies 8 = 13) +* `Equation168` -> `Equation2` (implied by 0 -> implies 13 = 13) +* `Equation168` -> `Equation6` (implied by 0 -> implies 13 = 13) +* `Equation168` -> `Equation7` (implied by 0 -> implies 13 = 13) +* `Equation4513` -> `Equation4` (implied by 7 -> implies 6 = 13) +* `Equation3` -> `Equation46` (implied by 4 -> implies 8 = 12) +* `Equation387` -> `Equation46` (implied by 4 -> implies 8 = 12) +* `Equation4512` -> `Equation4582` (implied by 8 -> implies 4 = 12) +* `Equation4552` -> `Equation4` (implied by 6 -> implies 6 = 12) +* `Equation4582` -> `Equation46` (implied by 4 -> implies 8 = 12) +* `Equation4` -> `Equation46` (implied by 3 -> implies 8 = 11) +* `Equation42` -> `Equation4` (implied by 5 -> implies 6 = 11) +* `Equation43` -> `Equation4` (implied by 5 -> implies 6 = 11) +* `Equation4512` -> `Equation4552` (implied by 8 -> implies 3 = 11) +* `Equation4513` -> `Equation4582` (implied by 7 -> implies 4 = 11) +* `Equation3` -> `Equation4` (implied by 4 -> implies 6 = 10) +* `Equation387` -> `Equation4` (implied by 4 -> implies 6 = 10) +* `Equation4512` -> `Equation387` (implied by 8 -> implies 2 = 10) +* `Equation4552` -> `Equation4582` (implied by 6 -> implies 4 = 10) +* `Equation4582` -> `Equation4` (implied by 4 -> implies 6 = 10) +* `Equation42` -> `Equation4582` (implied by 5 -> implies 4 = 9) +* `Equation43` -> `Equation4582` (implied by 5 -> implies 4 = 9) +* `Equation4512` -> `Equation3` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation5` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation8` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation38` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation39` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation40` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation41` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation43` (implied by 8 -> implies 1 = 9) +* `Equation4512` -> `Equation168` (implied by 8 -> implies 1 = 9) +* `Equation4513` -> `Equation387` (implied by 7 -> implies 2 = 9) +* `Equation3` -> `Equation4582` (implied by 4 -> implies 4 = 8) +* `Equation5` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation8` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation38` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation39` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation40` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation41` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation42` -> `Equation4552` (implied by 5 -> implies 3 = 8) +* `Equation43` -> `Equation4552` (implied by 5 -> implies 3 = 8) +* `Equation168` -> `Equation46` (implied by 0 -> implies 8 = 8) +* `Equation387` -> `Equation4582` (implied by 4 -> implies 4 = 8) +* `Equation4513` -> `Equation3` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation5` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation8` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation38` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation39` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation40` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation41` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation42` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation43` (implied by 7 -> implies 1 = 8) +* `Equation4513` -> `Equation168` (implied by 7 -> implies 1 = 8) +* `Equation4552` -> `Equation387` (implied by 6 -> implies 2 = 8) +* `Equation3` -> `Equation4552` (implied by 4 -> implies 3 = 7) +* `Equation42` -> `Equation387` (implied by 5 -> implies 2 = 7) +* `Equation42` -> `Equation4513` (implied by 5 -> implies 2 = 7) +* `Equation43` -> `Equation4513` (implied by 5 -> implies 2 = 7) +* `Equation387` -> `Equation4552` (implied by 4 -> implies 3 = 7) +* `Equation4552` -> `Equation3` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation5` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation8` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation38` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation39` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation40` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation41` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation42` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation43` (implied by 6 -> implies 1 = 7) +* `Equation4552` -> `Equation168` (implied by 6 -> implies 1 = 7) +* `Equation3` -> `Equation387` (implied by 4 -> implies 2 = 6) +* `Equation3` -> `Equation4513` (implied by 4 -> implies 2 = 6) +* `Equation5` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation8` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation38` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation39` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation40` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation41` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation42` -> `Equation3` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation5` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation8` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation38` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation39` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation40` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation41` (implied by 5 -> implies 1 = 6) +* `Equation42` -> `Equation168` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation5` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation8` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation38` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation39` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation40` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation41` (implied by 5 -> implies 1 = 6) +* `Equation43` -> `Equation168` (implied by 5 -> implies 1 = 6) +* `Equation168` -> `Equation4` (implied by 0 -> implies 6 = 6) +* `Equation387` -> `Equation4513` (implied by 4 -> implies 2 = 6) +* `Equation4582` -> `Equation387` (implied by 4 -> implies 2 = 6) +* `Equation3` -> `Equation5` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation8` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation38` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation39` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation40` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation41` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation43` (implied by 4 -> implies 1 = 5) +* `Equation3` -> `Equation168` (implied by 4 -> implies 1 = 5) +* `Equation4` -> `Equation387` (implied by 3 -> implies 2 = 5) +* `Equation387` -> `Equation3` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation5` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation8` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation38` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation39` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation40` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation41` (implied by 4 -> implies 1 = 5) +* `Equation387` -> `Equation168` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation3` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation5` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation8` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation38` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation39` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation40` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation41` (implied by 4 -> implies 1 = 5) +* `Equation4582` -> `Equation168` (implied by 4 -> implies 1 = 5) +* `Equation4` -> `Equation5` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation8` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation38` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation39` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation40` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation41` (implied by 3 -> implies 1 = 4) +* `Equation4` -> `Equation168` (implied by 3 -> implies 1 = 4) +* `Equation5` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation8` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation38` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation39` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation40` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation41` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation46` -> `Equation5` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation8` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation38` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation39` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation40` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation41` (implied by 3 -> implies 1 = 4) +* `Equation46` -> `Equation168` (implied by 3 -> implies 1 = 4) +* `Equation168` -> `Equation4582` (implied by 0 -> implies 4 = 4) +* `Equation2` -> `Equation5` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation8` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation38` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation39` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation40` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation41` (implied by 2 -> implies 1 = 3) +* `Equation2` -> `Equation168` (implied by 2 -> implies 1 = 3) +* `Equation5` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation6` -> `Equation5` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation8` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation38` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation39` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation40` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation41` (implied by 2 -> implies 1 = 3) +* `Equation6` -> `Equation168` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation5` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation8` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation38` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation39` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation40` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation41` (implied by 2 -> implies 1 = 3) +* `Equation7` -> `Equation168` (implied by 2 -> implies 1 = 3) +* `Equation8` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation38` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation39` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation40` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation41` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation168` -> `Equation4552` (implied by 0 -> implies 3 = 3) +* `Equation5` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation5` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation8` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation8` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation38` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation38` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation39` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation39` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation40` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation40` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation41` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation41` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation168` -> `Equation387` (implied by 0 -> implies 2 = 2) +* `Equation168` -> `Equation4513` (implied by 0 -> implies 2 = 2) +* `Equation5` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation5` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation8` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation38` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation39` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation40` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation168` (implied by 0 -> implies 1 = 1) +* `Equation41` -> `Equation4512` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation3` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation5` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation8` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation38` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation39` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation40` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation41` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation42` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation43` (implied by 0 -> implies 1 = 1) +* `Equation168` -> `Equation4512` (implied by 0 -> implies 1 = 1)