Skip to content

Commit

Permalink
prove some nonimplications for Equations 2712 and 3545 (#430)
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha authored Oct 8, 2024
1 parent 11ab32c commit cf97f57
Show file tree
Hide file tree
Showing 5 changed files with 58 additions and 0 deletions.
2 changes: 2 additions & 0 deletions equational_theories/Generated/All4x4Tables.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

22 changes: 22 additions & 0 deletions equational_theories/Generated/All4x4Tables/Refutation742.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

22 changes: 22 additions & 0 deletions equational_theories/Generated/All4x4Tables/Refutation743.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 5 additions & 0 deletions equational_theories/Generated/All4x4Tables/data/extra.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Table [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]]
Proves [1,23,203,208,211,307,323,1629,2238,2243,2246,2253,2256,2263,2266,2273,2277,2281,2441,2443,2446,2449,2452,2456,2466,2476,2644,2646,2696,2706,2709,2712,3050,3065,3142,3253,3306,3456,3458,3519,3522,4065,4118,4128]

Table [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]
Proves [1,3456,3545]
7 changes: 7 additions & 0 deletions equational_theories/Generated/All4x4Tables/data/plan.txt
Original file line number Diff line number Diff line change
Expand Up @@ -2967,3 +2967,10 @@ Magma [[0,2,3,4,6,1,8,5,10,7,9],[2,1,6,5,7,4,10,9,0,8,3],[3,6,2,8,1,7,5,10,9,4,0
Satisfies [474,3113]
Refutes [513,833,879,1026,1682,1721,1851,1885,2503,2650,2699,3079,3474,3868]

Magma [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]]
Satisfies [2712]
Refutes [205,1647,2240,2459,2462,3068]

Magma [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]
Satisfies [3545]
Refutes [3862]

0 comments on commit cf97f57

Please sign in to comment.