# Closed versions of the failing lines (honest standalone lemmas)

412 of 499 lines closed; 87 not closed (their file shows the honest base attempt).
Closed by: pass2 148, H0 86, K5 41, K2pow 29, K1 27, K2 17, K4 10, K3 6, K4b 3, S2 3, S 3, K2K4 2, S_K3 2, K3K4b 2, SC_lib 2, K2b 2, K3K2 2, S_instarg_sqrtnone 1, L_sqrtle0 1, S2_K3 1, K4K5 1, SIMPLE 1, K3K5b 1, S4 1, P25 1, S_split2 1, S_split 1, pairK3K5 1, sc_divsubdivsame 1, cite 1, K2upow 1, K3_K2pow 1, K2c 1, SC_library 1, cite_opaque 1, k5 1, L266_K1K4 1, L283_K2pow 1, L287_K2pow 1, K1K4 1, K3+K2pow 1, split+K2pow 1, SCsplit_helper 1, K3K2pow 1.

Rules: hypotheses = the facts Z3 had at the line, minus the goal itself and minus the asserts of the step's own `by` block; a variant may drop hypotheses, never add any; goal unchanged; one Dafny run per candidate, 30 s.

| line | status | closed by | hypotheses removed (goal / own-block) | Dafny |
|---|---|---|---|---|
| [aime_1983_p1-1057](aime_1983_p1-1057.dfy) | CLOSED | K5 | 0 / 2 | finished with 16 verified, 0 errors |
| [aime_1983_p1-507](aime_1983_p1-507.dfy) | CLOSED | H0 | 1 / 4 | finished with 9 verified, 0 errors |
| [aime_1983_p3-274](aime_1983_p3-274.dfy) | CLOSED | S_instarg_sqrtnone | 0 / 0 | finished with 3 verified, 0 errors |
| [aime_1983_p3-507](aime_1983_p3-507.dfy) | CLOSED | L_sqrtle0 | 0 / 0 | finished with 1 verified, 0 errors |
| [aime_1983_p3-856](aime_1983_p3-856.dfy) | CLOSED | pass2 | 0 / 0 | finished with 5 verified, 0 errors |
| [aime_1984_p1-106](aime_1984_p1-106.dfy) | CLOSED | K2K4 | 0 / 0 | finished with 9 verified, 0 errors |
| [aime_1984_p1-114](aime_1984_p1-114.dfy) | CLOSED | K4b | 0 / 0 | finished with 7 verified, 0 errors |
| [aime_1984_p1-123](aime_1984_p1-123.dfy) | CLOSED | K4b | 0 / 0 | finished with 6 verified, 0 errors |
| [aime_1984_p1-175](aime_1984_p1-175.dfy) | CLOSED | S_K3 | 0 / 0 | finished with 14 verified, 0 errors |
| [aime_1984_p1-180](aime_1984_p1-180.dfy) | CLOSED | K5 | 0 / 0 | finished with 44 verified, 0 errors |
| [aime_1984_p1-192](aime_1984_p1-192.dfy) | CLOSED | S2 | 0 / 0 | finished with 41 verified, 0 errors |
| [aime_1984_p1-35](aime_1984_p1-35.dfy) | CLOSED | K4 | 0 / 0 | finished with 13 verified, 0 errors |
| [aime_1984_p1-408](aime_1984_p1-408.dfy) | CLOSED | K3K4b | 0 / 0 | finished with 5 verified, 0 errors |
| [aime_1984_p1-466](aime_1984_p1-466.dfy) | CLOSED | S_K3 | 0 / 0 | finished with 14 verified, 0 errors |
| [aime_1984_p1-471](aime_1984_p1-471.dfy) | CLOSED | K5 | 0 / 0 | finished with 43 verified, 0 errors |
| [aime_1984_p1-484](aime_1984_p1-484.dfy) | CLOSED | S2_K3 | 0 / 0 | finished with 13 verified, 0 errors |
| [aime_1984_p1-596](aime_1984_p1-596.dfy) | CLOSED | K3K4b | 0 / 0 | finished with 2 verified, 0 errors |
| [aime_1984_p1-62](aime_1984_p1-62.dfy) | CLOSED | K4 | 0 / 0 | finished with 25 verified, 0 errors |
| [aime_1984_p1-82](aime_1984_p1-82.dfy) | CLOSED | K2K4 | 0 / 0 | finished with 9 verified, 0 errors |
| [aime_1984_p1-90](aime_1984_p1-90.dfy) | CLOSED | K4 | 0 / 0 | finished with 6 verified, 0 errors |
| [aime_1984_p1-98](aime_1984_p1-98.dfy) | CLOSED | K4b | 0 / 0 | finished with 7 verified, 0 errors |
| [aime_1987_p5-452](aime_1987_p5-452.dfy) | CLOSED | H0 | 0 / 1 | finished with 9 verified, 0 errors |
| [aime_1987_p5-495](aime_1987_p5-495.dfy) | CLOSED | K4K5 | 0 / 2 | finished with 10 verified, 0 errors |
| [aime_1987_p5-594](aime_1987_p5-594.dfy) | CLOSED | K4 | 0 / 0 | finished with 2 verified, 0 errors |
| [aime_1987_p5-641](aime_1987_p5-641.dfy) | CLOSED | K4 | 0 / 0 | finished with 3 verified, 0 errors |
| [aime_1990_p4-205](aime_1990_p4-205.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [aime_1999_p11-1161](aime_1999_p11-1161.dfy) | CLOSED | pass2 | 0 / 2 | finished with 24 verified, 0 errors |
| [aime_1999_p11-1170](aime_1999_p11-1170.dfy) | CLOSED | K4 | 0 / 0 | finished with 20 verified, 0 errors |
| [aime_1999_p11-1192](aime_1999_p11-1192.dfy) | CLOSED | K5 | 0 / 0 | finished with 23 verified, 0 errors |
| [aime_1999_p11-177](aime_1999_p11-177.dfy) | CLOSED | pass2 | 0 / 5 | finished with 10 verified, 0 errors |
| [aime_1999_p11-187](aime_1999_p11-187.dfy) | CLOSED | pass2 | 0 / 5 | finished with 10 verified, 0 errors |
| [aime_1999_p11-224](aime_1999_p11-224.dfy) | CLOSED | K1 | 0 / 0 | finished with 21 verified, 0 errors |
| [aime_1999_p11-938](aime_1999_p11-938.dfy) | CLOSED | pass2 | 0 / 2 | finished with 48 verified, 0 errors |
| [algebra_9onxpypzleqsum2onxpy-471](algebra_9onxpypzleqsum2onxpy-471.dfy) | CLOSED | K2 | 0 / 7 | finished with 63 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1550](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1550.dfy) | CLOSED | pass2 | 0 / 4 | finished with 191 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1620](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1620.dfy) | CLOSED | pass2 | 1 / 0 | finished with 4 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1725](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-1725.dfy) | CLOSED | H0 | 0 / 5 | finished with 14 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-40](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-40.dfy) | CLOSED | pass2 | 0 / 3 | finished with 7 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-51](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-51.dfy) | CLOSED | pass2 | 0 / 3 | finished with 7 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-62](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-62.dfy) | CLOSED | pass2 | 0 / 3 | finished with 7 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-945](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-945.dfy) | CLOSED | K2 | 0 / 0 | finished with 28 verified, 0 errors |
| [algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-949](algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2-949.dfy) | CLOSED | H0 | 0 / 1 | finished with 27 verified, 0 errors |
| [algebra_absapbon1pabsapbleqsumabsaon1pabsa-312](algebra_absapbon1pabsapbleqsumabsaon1pabsa-312.dfy) | CLOSED | pass2 | 0 / 0 | finished with 12 verified, 0 errors |
| [algebra_amgm_sumasqdivbgeqsuma-803](algebra_amgm_sumasqdivbgeqsuma-803.dfy) | CLOSED | K3 | 0 / 0 | finished with 1 verified, 0 errors |
| [algebra_amgm_sumasqdivbgeqsuma-845](algebra_amgm_sumasqdivbgeqsuma-845.dfy) | CLOSED | pass2 | 1 / 0 | finished with 4 verified, 0 errors |
| [algebra_apbon2pownleqapownpbpowon2-142](algebra_apbon2pownleqapownpbpowon2-142.dfy) | CLOSED | pass2 | 0 / 8 | finished with 9 verified, 0 errors |
| [algebra_apbon2pownleqapownpbpowon2-302](algebra_apbon2pownleqapownpbpowon2-302.dfy) | CLOSED | H0 | 0 / 0 | finished with 22 verified, 0 errors |
| [algebra_apbon2pownleqapownpbpowon2-360](algebra_apbon2pownleqapownpbpowon2-360.dfy) | CLOSED | H0 | 0 / 0 | finished with 35 verified, 0 errors |
| [algebra_apbon2pownleqapownpbpowon2-91](algebra_apbon2pownleqapownpbpowon2-91.dfy) | CLOSED | pass2 | 0 / 8 | finished with 9 verified, 0 errors |
| [algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3-1502](algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3-1502.dfy) | CLOSED | H0 | 0 / 0 | finished with 13 verified, 0 errors |
| [algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3-799](algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3-799.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [algebra_bleqa_apbon2msqrtableqambsqon8b-192](algebra_bleqa_apbon2msqrtableqambsqon8b-192.dfy) | CLOSED | S | 0 / 1 | finished with 57 verified, 0 errors |
| [algebra_bleqa_apbon2msqrtableqambsqon8b-222](algebra_bleqa_apbon2msqrtableqambsqon8b-222.dfy) | CLOSED | S | 0 / 0 | finished with 42 verified, 0 errors |
| [algebra_bleqa_apbon2msqrtableqambsqon8b-231](algebra_bleqa_apbon2msqrtableqambsqon8b-231.dfy) | CLOSED | H0 | 1 / 0 | finished with 1 verified, 0 errors |
| [algebra_bleqa_apbon2msqrtableqambsqon8b-329](algebra_bleqa_apbon2msqrtableqambsqon8b-329.dfy) | CLOSED | H0 | 1 / 0 | finished with 3 verified, 0 errors |
| [algebra_others_exirrpowirrrat-198](algebra_others_exirrpowirrrat-198.dfy) | CLOSED | S | 0 / 0 | finished with 2 verified, 0 errors |
| [algebra_sum1onsqrt2to1onsqrt10000lt198-167](algebra_sum1onsqrt2to1onsqrt10000lt198-167.dfy) | CLOSED | pass2 | 0 / 0 | finished with 14 verified, 0 errors |
| [algebra_sum1onsqrt2to1onsqrt10000lt198-212](algebra_sum1onsqrt2to1onsqrt10000lt198-212.dfy) | CLOSED | K1 | 0 / 0 | finished with 15 verified, 0 errors |
| [algebra_sum1onsqrt2to1onsqrt10000lt198-213](algebra_sum1onsqrt2to1onsqrt10000lt198-213.dfy) | CLOSED | pass2 | 0 / 0 | finished with 16 verified, 0 errors |
| [algebra_sum1onsqrt2to1onsqrt10000lt198-462](algebra_sum1onsqrt2to1onsqrt10000lt198-462.dfy) | CLOSED | K2 | 0 / 0 | finished with 24 verified, 0 errors |
| [amc12_2000_p20-483](amc12_2000_p20-483.dfy) | CLOSED | pass2 | 0 / 4 | finished with 18 verified, 0 errors |
| [amc12_2000_p20-493](amc12_2000_p20-493.dfy) | CLOSED | pass2 | 0 / 4 | finished with 18 verified, 0 errors |
| [amc12_2001_p5-11](amc12_2001_p5-11.dfy) | CLOSED | pass2 | 0 / 3 | finished with 7 verified, 0 errors |
| [amc12_2001_p5-31](amc12_2001_p5-31.dfy) | CLOSED | pass2 | 0 / 0 | finished with 64 verified, 0 errors |
| [amc12_2001_p5-38](amc12_2001_p5-38.dfy) | CLOSED | pass2 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-28](amc12a_2003_p25-28.dfy) | CLOSED | pass2 | 0 / 0 | finished with 5 verified, 0 errors |
| [amc12a_2003_p25-34](amc12a_2003_p25-34.dfy) | CLOSED | pass2 | 0 / 0 | finished with 9 verified, 0 errors |
| [amc12a_2003_p25-40](amc12a_2003_p25-40.dfy) | CLOSED | pass2 | 0 / 0 | finished with 9 verified, 0 errors |
| [amc12a_2003_p25-43](amc12a_2003_p25-43.dfy) | CLOSED | pass2 | 0 / 0 | finished with 5 verified, 0 errors |
| [amc12a_2003_p25-44](amc12a_2003_p25-44.dfy) | CLOSED | pass2 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-45](amc12a_2003_p25-45.dfy) | CLOSED | pass2 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-46](amc12a_2003_p25-46.dfy) | CLOSED | pass2 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-47](amc12a_2003_p25-47.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-49](amc12a_2003_p25-49.dfy) | CLOSED | K5 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-51](amc12a_2003_p25-51.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-58](amc12a_2003_p25-58.dfy) | CLOSED | K5 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-60](amc12a_2003_p25-60.dfy) | CLOSED | pass2 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2003_p25-72](amc12a_2003_p25-72.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-81](amc12a_2003_p25-81.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-82](amc12a_2003_p25-82.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-90](amc12a_2003_p25-90.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2003_p25-91](amc12a_2003_p25-91.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2008_p4-12](amc12a_2008_p4-12.dfy) | CLOSED | pass2 | 0 / 3 | finished with 28 verified, 0 errors |
| [amc12a_2008_p4-22](amc12a_2008_p4-22.dfy) | CLOSED | K4 | 0 / 0 | finished with 56 verified, 0 errors |
| [amc12a_2008_p4-28](amc12a_2008_p4-28.dfy) | CLOSED | SIMPLE | 0 / 0 | finished with 50 verified, 0 errors |
| [amc12a_2009_p15-100](amc12a_2009_p15-100.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p15-107](amc12a_2009_p15-107.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p15-183](amc12a_2009_p15-183.dfy) | CLOSED | S4 | 0 / 0 | finished with 141 verified, 0 errors |
| [amc12a_2009_p15-201](amc12a_2009_p15-201.dfy) | CLOSED | pass2 | 0 / 27 | finished with 156 verified, 0 errors |
| [amc12a_2009_p15-241](amc12a_2009_p15-241.dfy) | CLOSED | H0 | 0 / 0 | finished with 28 verified, 0 errors |
| [amc12a_2009_p15-242](amc12a_2009_p15-242.dfy) | CLOSED | H0 | 0 / 0 | finished with 28 verified, 0 errors |
| [amc12a_2009_p15-282](amc12a_2009_p15-282.dfy) | CLOSED | H0 | 0 / 0 | finished with 31 verified, 0 errors |
| [amc12a_2009_p15-287](amc12a_2009_p15-287.dfy) | CLOSED | H0 | 0 / 0 | finished with 35 verified, 0 errors |
| [amc12a_2009_p15-292](amc12a_2009_p15-292.dfy) | CLOSED | H0 | 0 / 0 | finished with 39 verified, 0 errors |
| [amc12a_2009_p15-297](amc12a_2009_p15-297.dfy) | CLOSED | H0 | 0 / 0 | finished with 43 verified, 0 errors |
| [amc12a_2009_p15-302](amc12a_2009_p15-302.dfy) | CLOSED | K1 | 0 / 0 | finished with 51 verified, 0 errors |
| [amc12a_2009_p15-32](amc12a_2009_p15-32.dfy) | CLOSED | K3K5b | 0 / 0 | finished with 36 verified, 0 errors |
| [amc12a_2009_p15-323](amc12a_2009_p15-323.dfy) | CLOSED | pass2 | 0 / 0 | finished with 186 verified, 0 errors |
| [amc12a_2009_p15-325](amc12a_2009_p15-325.dfy) | CLOSED | pass2 | 0 / 0 | finished with 120 verified, 0 errors |
| [amc12a_2009_p15-45](amc12a_2009_p15-45.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p15-586](amc12a_2009_p15-586.dfy) | CLOSED | pass2 | 0 / 90 | finished with 134 verified, 0 errors |
| [amc12a_2009_p15-597](amc12a_2009_p15-597.dfy) | CLOSED | H0 | 0 / 0 | finished with 17 verified, 0 errors |
| [amc12a_2009_p15-607](amc12a_2009_p15-607.dfy) | CLOSED | H0 | 0 / 0 | finished with 25 verified, 0 errors |
| [amc12a_2009_p15-612](amc12a_2009_p15-612.dfy) | CLOSED | H0 | 0 / 0 | finished with 29 verified, 0 errors |
| [amc12a_2009_p15-617](amc12a_2009_p15-617.dfy) | CLOSED | H0 | 0 / 0 | finished with 33 verified, 0 errors |
| [amc12a_2009_p15-693](amc12a_2009_p15-693.dfy) | CLOSED | H0 | 0 / 0 | finished with 71 verified, 0 errors |
| [amc12a_2009_p15-694](amc12a_2009_p15-694.dfy) | CLOSED | H0 | 0 / 0 | finished with 71 verified, 0 errors |
| [amc12a_2009_p15-696](amc12a_2009_p15-696.dfy) | CLOSED | H0 | 0 / 0 | finished with 71 verified, 0 errors |
| [amc12a_2009_p15-728](amc12a_2009_p15-728.dfy) | CLOSED | pass2 | 0 / 0 | finished with 99 verified, 0 errors |
| [amc12a_2009_p15-729](amc12a_2009_p15-729.dfy) | CLOSED | pass2 | 0 / 0 | finished with 134 verified, 0 errors |
| [amc12a_2009_p15-731](amc12a_2009_p15-731.dfy) | CLOSED | pass2 | 0 / 0 | finished with 93 verified, 0 errors |
| [amc12a_2009_p15-732](amc12a_2009_p15-732.dfy) | CLOSED | pass2 | 0 / 0 | finished with 14 verified, 0 errors |
| [amc12a_2009_p15-735](amc12a_2009_p15-735.dfy) | CLOSED | pass2 | 0 / 0 | finished with 17 verified, 0 errors |
| [amc12a_2009_p15-741](amc12a_2009_p15-741.dfy) | CLOSED | SC_lib | 0 / 0 | finished with 41 verified, 0 errors |
| [amc12a_2009_p15-742](amc12a_2009_p15-742.dfy) | CLOSED | K3 | 0 / 0 | finished with 9 verified, 0 errors |
| [amc12a_2009_p15-743](amc12a_2009_p15-743.dfy) | CLOSED | H0 | 0 / 0 | finished with 134 verified, 0 errors |
| [amc12a_2009_p15-744](amc12a_2009_p15-744.dfy) | CLOSED | SC_lib | 0 / 0 | finished with 20 verified, 0 errors |
| [amc12a_2009_p15-96](amc12a_2009_p15-96.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p15-98](amc12a_2009_p15-98.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p15-99](amc12a_2009_p15-99.dfy) | CLOSED | H0 | 0 / 0 | finished with 104 verified, 0 errors |
| [amc12a_2009_p2-20](amc12a_2009_p2-20.dfy) | CLOSED | K4 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2009_p2-26](amc12a_2009_p2-26.dfy) | CLOSED | K4 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2009_p6-137](amc12a_2009_p6-137.dfy) | CLOSED | K2 | 0 / 0 | finished with 7 verified, 0 errors |
| [amc12a_2009_p6-28](amc12a_2009_p6-28.dfy) | CLOSED | H0 | 0 / 1 | finished with 4 verified, 0 errors |
| [amc12a_2009_p9-181](amc12a_2009_p9-181.dfy) | CLOSED | K1 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12a_2009_p9-388](amc12a_2009_p9-388.dfy) | CLOSED | K1 | 0 / 0 | finished with 5 verified, 0 errors |
| [amc12a_2013_p4-15](amc12a_2013_p4-15.dfy) | CLOSED | K2 | 0 / 0 | finished with 77 verified, 0 errors |
| [amc12a_2013_p4-75](amc12a_2013_p4-75.dfy) | CLOSED | K2 | 0 / 2 | finished with 92 verified, 0 errors |
| [amc12a_2017_p7-28](amc12a_2017_p7-28.dfy) | CLOSED | K1 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12a_2017_p7-48](amc12a_2017_p7-48.dfy) | CLOSED | K1 | 0 / 0 | finished with 16 verified, 0 errors |
| [amc12a_2017_p7-54](amc12a_2017_p7-54.dfy) | CLOSED | K1 | 0 / 0 | finished with 17 verified, 0 errors |
| [amc12a_2017_p7-67](amc12a_2017_p7-67.dfy) | CLOSED | K1 | 0 / 0 | finished with 16 verified, 0 errors |
| [amc12a_2017_p7-74](amc12a_2017_p7-74.dfy) | CLOSED | K1 | 0 / 0 | finished with 17 verified, 0 errors |
| [amc12a_2019_p21-18](amc12a_2019_p21-18.dfy) | CLOSED | P25 | 0 / 0 | finished with 20 verified, 0 errors |
| [amc12a_2019_p21-41](amc12a_2019_p21-41.dfy) | CLOSED | S2 | 0 / 4 | finished with 142 verified, 0 errors |
| [amc12a_2019_p21-67](amc12a_2019_p21-67.dfy) | CLOSED | S2 | 0 / 0 | finished with 143 verified, 0 errors |
| [amc12a_2021_p14-113](amc12a_2021_p14-113.dfy) | CLOSED | K1 | 0 / 0 | finished with 10 verified, 0 errors |
| [amc12a_2021_p14-121](amc12a_2021_p14-121.dfy) | CLOSED | S_split2 | 0 / 0 | finished with 22 verified, 0 errors |
| [amc12a_2021_p14-168](amc12a_2021_p14-168.dfy) | CLOSED | K2pow | 0 / 0 | finished with 52 verified, 0 errors |
| [amc12a_2021_p14-197](amc12a_2021_p14-197.dfy) | CLOSED | S_split | 0 / 0 | finished with 23 verified, 0 errors |
| [amc12a_2021_p14-219](amc12a_2021_p14-219.dfy) | CLOSED | pass2 | 0 / 0 | finished with 136 verified, 0 errors |
| [amc12a_2021_p14-280](amc12a_2021_p14-280.dfy) | CLOSED | K1 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12a_2021_p14-309](amc12a_2021_p14-309.dfy) | CLOSED | K2pow | 0 / 2 | finished with 52 verified, 0 errors |
| [amc12a_2021_p14-357](amc12a_2021_p14-357.dfy) | CLOSED | pass2 | 0 / 3 | finished with 19 verified, 0 errors |
| [amc12a_2021_p14-467](amc12a_2021_p14-467.dfy) | CLOSED | pairK3K5 | 0 / 0 | finished with 8 verified, 0 errors |
| [amc12a_2021_p14-482](amc12a_2021_p14-482.dfy) | CLOSED | pass2 | 0 / 3 | finished with 16 verified, 0 errors |
| [amc12a_2021_p14-484](amc12a_2021_p14-484.dfy) | CLOSED | K1 | 0 / 0 | finished with 13 verified, 0 errors |
| [amc12a_2021_p14-492](amc12a_2021_p14-492.dfy) | CLOSED | K1 | 0 / 0 | finished with 13 verified, 0 errors |
| [amc12a_2021_p14-502](amc12a_2021_p14-502.dfy) | CLOSED | K3 | 0 / 2 | finished with 15 verified, 0 errors |
| [amc12a_2021_p14-542](amc12a_2021_p14-542.dfy) | CLOSED | pass2 | 0 / 2 | finished with 158 verified, 0 errors |
| [amc12a_2021_p14-548](amc12a_2021_p14-548.dfy) | CLOSED | pass2 | 0 / 2 | finished with 44 verified, 0 errors |
| [amc12a_2021_p14-79](amc12a_2021_p14-79.dfy) | CLOSED | K1 | 0 / 0 | finished with 10 verified, 0 errors |
| [amc12a_2021_p14-90](amc12a_2021_p14-90.dfy) | CLOSED | K2 | 0 / 0 | finished with 19 verified, 0 errors |
| [amc12a_2021_p14-95](amc12a_2021_p14-95.dfy) | CLOSED | K2pow | 0 / 0 | finished with 12 verified, 0 errors |
| [amc12a_2021_p18-105](amc12a_2021_p18-105.dfy) | CLOSED | K5 | 0 / 0 | finished with 1 verified, 0 errors |
| [amc12a_2021_p18-140](amc12a_2021_p18-140.dfy) | CLOSED | K2 | 0 / 0 | finished with 5 verified, 0 errors |
| [amc12a_2021_p18-160](amc12a_2021_p18-160.dfy) | CLOSED | K5 | 0 / 0 | finished with 1 verified, 0 errors |
| [amc12a_2021_p18-192](amc12a_2021_p18-192.dfy) | CLOSED | K2 | 0 / 0 | finished with 5 verified, 0 errors |
| [amc12a_2021_p18-225](amc12a_2021_p18-225.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [amc12a_2021_p19-1063](amc12a_2021_p19-1063.dfy) | CLOSED | pass2 | 1 / 0 | finished with 13 verified, 0 errors |
| [amc12a_2021_p19-1344](amc12a_2021_p19-1344.dfy) | CLOSED | K5 | 0 / 0 | finished with 14 verified, 0 errors |
| [amc12a_2021_p19-1348](amc12a_2021_p19-1348.dfy) | CLOSED | K5 | 0 / 0 | finished with 15 verified, 0 errors |
| [amc12a_2021_p19-1352](amc12a_2021_p19-1352.dfy) | CLOSED | K1 | 0 / 2 | finished with 30 verified, 0 errors |
| [amc12a_2021_p19-1556](amc12a_2021_p19-1556.dfy) | CLOSED | K5 | 0 / 0 | finished with 33 verified, 0 errors |
| [amc12a_2021_p19-1560](amc12a_2021_p19-1560.dfy) | CLOSED | K5 | 0 / 0 | finished with 33 verified, 0 errors |
| [amc12a_2021_p19-1564](amc12a_2021_p19-1564.dfy) | CLOSED | K1 | 0 / 2 | finished with 43 verified, 0 errors |
| [amc12a_2021_p19-1668](amc12a_2021_p19-1668.dfy) | CLOSED | K5 | 0 / 0 | finished with 47 verified, 0 errors |
| [amc12a_2021_p19-1722](amc12a_2021_p19-1722.dfy) | CLOSED | K5 | 0 / 0 | finished with 29 verified, 0 errors |
| [amc12a_2021_p19-1726](amc12a_2021_p19-1726.dfy) | CLOSED | K5 | 0 / 0 | finished with 30 verified, 0 errors |
| [amc12a_2021_p19-599](amc12a_2021_p19-599.dfy) | CLOSED | pass2 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12a_2021_p19-855](amc12a_2021_p19-855.dfy) | CLOSED | K1 | 0 / 0 | finished with 40 verified, 0 errors |
| [amc12a_2021_p22-1857](amc12a_2021_p22-1857.dfy) | CLOSED | H0 | 0 / 0 | finished with 0 verified, 0 errors |
| [amc12a_2021_p22-1858](amc12a_2021_p22-1858.dfy) | CLOSED | H0 | 0 / 0 | finished with 0 verified, 0 errors |
| [amc12a_2021_p22-1859](amc12a_2021_p22-1859.dfy) | CLOSED | H0 | 0 / 0 | finished with 0 verified, 0 errors |
| [amc12a_2021_p22-496](amc12a_2021_p22-496.dfy) | CLOSED | pass2 | 0 / 4 | finished with 32 verified, 0 errors |
| [amc12a_2021_p22-507](amc12a_2021_p22-507.dfy) | CLOSED | pass2 | 1 / 1 | finished with 32 verified, 0 errors |
| [amc12b_2003_p17-101](amc12b_2003_p17-101.dfy) | CLOSED | pass2 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12b_2003_p17-102](amc12b_2003_p17-102.dfy) | CLOSED | pass2 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12b_2020_p13-197](amc12b_2020_p13-197.dfy) | CLOSED | K5 | 0 / 5 | finished with 8 verified, 0 errors |
| [amc12b_2020_p13-220](amc12b_2020_p13-220.dfy) | CLOSED | K5 | 0 / 6 | finished with 9 verified, 0 errors |
| [amc12b_2020_p13-452](amc12b_2020_p13-452.dfy) | CLOSED | H0 | 0 / 1 | finished with 27 verified, 0 errors |
| [amc12b_2020_p13-530](amc12b_2020_p13-530.dfy) | CLOSED | K2 | 0 / 1 | finished with 21 verified, 0 errors |
| [amc12b_2020_p21-1245](amc12b_2020_p21-1245.dfy) | CLOSED | K5 | 0 / 0 | finished with 10 verified, 0 errors |
| [amc12b_2020_p21-1289](amc12b_2020_p21-1289.dfy) | CLOSED | K5 | 0 / 0 | finished with 11 verified, 0 errors |
| [amc12b_2020_p21-1338](amc12b_2020_p21-1338.dfy) | CLOSED | K5 | 0 / 0 | finished with 12 verified, 0 errors |
| [amc12b_2020_p21-1387](amc12b_2020_p21-1387.dfy) | CLOSED | K5 | 0 / 0 | finished with 13 verified, 0 errors |
| [amc12b_2020_p21-1436](amc12b_2020_p21-1436.dfy) | CLOSED | K5 | 0 / 0 | finished with 14 verified, 0 errors |
| [amc12b_2020_p21-569](amc12b_2020_p21-569.dfy) | CLOSED | pass2 | 0 / 0 | finished with 14 verified, 0 errors |
| [amc12b_2020_p21-656](amc12b_2020_p21-656.dfy) | CLOSED | pass2 | 0 / 0 | finished with 19 verified, 0 errors |
| [amc12b_2020_p21-698](amc12b_2020_p21-698.dfy) | CLOSED | K4 | 0 / 0 | finished with 7 verified, 0 errors |
| [amc12b_2020_p22-233](amc12b_2020_p22-233.dfy) | CLOSED | pass2 | 0 / 2 | finished with 25 verified, 0 errors |
| [amc12b_2021_p1-366](amc12b_2021_p1-366.dfy) | CLOSED | K5 | 0 / 0 | finished with 3 verified, 0 errors |
| [amc12b_2021_p18-101](amc12b_2021_p18-101.dfy) | CLOSED | pass2 | 0 / 4 | finished with 14 verified, 0 errors |
| [amc12b_2021_p18-31](amc12b_2021_p18-31.dfy) | CLOSED | pass2 | 0 / 4 | finished with 14 verified, 0 errors |
| [amc12b_2021_p18-41](amc12b_2021_p18-41.dfy) | CLOSED | pass2 | 1 / 0 | finished with 12 verified, 0 errors |
| [amc12b_2021_p18-91](amc12b_2021_p18-91.dfy) | CLOSED | pass2 | 0 / 4 | finished with 14 verified, 0 errors |
| [amc12b_2021_p9-412](amc12b_2021_p9-412.dfy) | CLOSED | K3 | 0 / 3 | finished with 9 verified, 0 errors |
| [amc12b_2021_p9-488](amc12b_2021_p9-488.dfy) | CLOSED | K3 | 0 / 3 | finished with 9 verified, 0 errors |
| [amc12b_2021_p9-546](amc12b_2021_p9-546.dfy) | CLOSED | sc_divsubdivsame | 0 / 0 | finished with 4 verified, 0 errors |
| [amc12b_2021_p9-562](amc12b_2021_p9-562.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1959_p1-32](imo_1959_p1-32.dfy) | CLOSED | K5 | 0 / 0 | finished with 21 verified, 0 errors |
| [imo_1959_p1-61](imo_1959_p1-61.dfy) | CLOSED | K5 | 0 / 0 | finished with 36 verified, 0 errors |
| [imo_1960_p2-415](imo_1960_p2-415.dfy) | CLOSED | pass2 | 0 / 2 | finished with 32 verified, 0 errors |
| [imo_1961_p1-447](imo_1961_p1-447.dfy) | CLOSED | pass2 | 1 / 2 | finished with 14 verified, 0 errors |
| [imo_1961_p1-455](imo_1961_p1-455.dfy) | CLOSED | pass2 | 1 / 2 | finished with 14 verified, 0 errors |
| [imo_1961_p1-463](imo_1961_p1-463.dfy) | CLOSED | pass2 | 1 / 2 | finished with 14 verified, 0 errors |
| [imo_1964_p1_1-121](imo_1964_p1_1-121.dfy) | CLOSED | pass2 | 0 / 0 | finished with 24 verified, 0 errors |
| [imo_1964_p1_1-152](imo_1964_p1_1-152.dfy) | CLOSED | H0 | 0 / 2 | finished with 43 verified, 0 errors |
| [imo_1964_p1_1-20](imo_1964_p1_1-20.dfy) | CLOSED | pass2 | 0 / 2 | finished with 25 verified, 0 errors |
| [imo_1964_p1_1-27](imo_1964_p1_1-27.dfy) | CLOSED | pass2 | 0 / 0 | finished with 24 verified, 0 errors |
| [imo_1964_p1_1-40](imo_1964_p1_1-40.dfy) | CLOSED | pass2 | 0 / 1 | finished with 22 verified, 0 errors |
| [imo_1964_p1_1-80](imo_1964_p1_1-80.dfy) | CLOSED | pass2 | 0 / 0 | finished with 13 verified, 0 errors |
| [imo_1964_p1_1-87](imo_1964_p1_1-87.dfy) | CLOSED | pass2 | 0 / 0 | finished with 60 verified, 0 errors |
| [imo_1964_p1_2-101](imo_1964_p1_2-101.dfy) | CLOSED | K2pow | 0 / 0 | finished with 39 verified, 0 errors |
| [imo_1964_p1_2-107](imo_1964_p1_2-107.dfy) | CLOSED | K2pow | 0 / 0 | finished with 55 verified, 0 errors |
| [imo_1964_p1_2-33](imo_1964_p1_2-33.dfy) | CLOSED | K2pow | 0 / 2 | finished with 46 verified, 0 errors |
| [imo_1964_p1_2-48](imo_1964_p1_2-48.dfy) | CLOSED | K2pow | 0 / 2 | finished with 329 verified, 0 errors |
| [imo_1964_p1_2-61](imo_1964_p1_2-61.dfy) | CLOSED | K2pow | 0 / 2 | finished with 149 verified, 0 errors |
| [imo_1964_p1_2-78](imo_1964_p1_2-78.dfy) | CLOSED | K2pow | 0 / 9 | finished with 33 verified, 0 errors |
| [imo_1964_p1_2-84](imo_1964_p1_2-84.dfy) | CLOSED | H0 | 0 / 1 | finished with 114 verified, 0 errors |
| [imo_1964_p1_2-95](imo_1964_p1_2-95.dfy) | CLOSED | K2pow | 0 / 0 | finished with 33 verified, 0 errors |
| [imo_1965_p1-1011](imo_1965_p1-1011.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1013](imo_1965_p1-1013.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1093](imo_1965_p1-1093.dfy) | CLOSED | pass2 | 0 / 3 | finished with 36 verified, 0 errors |
| [imo_1965_p1-1136](imo_1965_p1-1136.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1143](imo_1965_p1-1143.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1146](imo_1965_p1-1146.dfy) | CLOSED | H0 | 1 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1148](imo_1965_p1-1148.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1153](imo_1965_p1-1153.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1161](imo_1965_p1-1161.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1163](imo_1965_p1-1163.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1222](imo_1965_p1-1222.dfy) | CLOSED | pass2 | 0 / 3 | finished with 36 verified, 0 errors |
| [imo_1965_p1-1269](imo_1965_p1-1269.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1274](imo_1965_p1-1274.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1277](imo_1965_p1-1277.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-1282](imo_1965_p1-1282.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-833](imo_1965_p1-833.dfy) | CLOSED | cite | 0 / 3 | finished with 36 verified, 0 errors |
| [imo_1965_p1-885](imo_1965_p1-885.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-893](imo_1965_p1-893.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-903](imo_1965_p1-903.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1965_p1-961](imo_1965_p1-961.dfy) | CLOSED | pass2 | 0 / 3 | finished with 24 verified, 0 errors |
| [imo_1966_p4-156](imo_1966_p4-156.dfy) | CLOSED | pass2 | 0 / 12 | finished with 130 verified, 0 errors |
| [imo_1966_p4-174](imo_1966_p4-174.dfy) | CLOSED | pass2 | 0 / 0 | finished with 33 verified, 0 errors |
| [imo_1966_p4-187](imo_1966_p4-187.dfy) | CLOSED | pass2 | 0 / 0 | finished with 14 verified, 0 errors |
| [imo_1966_p4-189](imo_1966_p4-189.dfy) | CLOSED | pass2 | 0 / 0 | finished with 15 verified, 0 errors |
| [imo_1966_p4-190](imo_1966_p4-190.dfy) | CLOSED | K3_K2pow | 0 / 0 | finished with 2 verified, 0 errors |
| [imo_1966_p4-196](imo_1966_p4-196.dfy) | CLOSED | pass2 | 0 / 0 | finished with 118 verified, 0 errors |
| [imo_1966_p4-204](imo_1966_p4-204.dfy) | CLOSED | pass2 | 0 / 0 | finished with 114 verified, 0 errors |
| [imo_1966_p4-212](imo_1966_p4-212.dfy) | CLOSED | H0 | 0 / 0 | finished with 13 verified, 0 errors |
| [imo_1966_p4-220](imo_1966_p4-220.dfy) | CLOSED | pass2 | 1 / 0 | finished with 114 verified, 0 errors |
| [imo_1966_p4-225](imo_1966_p4-225.dfy) | CLOSED | pass2 | 0 / 0 | finished with 114 verified, 0 errors |
| [imo_1966_p4-230](imo_1966_p4-230.dfy) | CLOSED | H0 | 0 / 0 | finished with 13 verified, 0 errors |
| [imo_1966_p4-233](imo_1966_p4-233.dfy) | CLOSED | pass2 | 1 / 0 | finished with 120 verified, 0 errors |
| [imo_1966_p4-235](imo_1966_p4-235.dfy) | CLOSED | pass2 | 1 / 0 | finished with 115 verified, 0 errors |
| [imo_1966_p4-241](imo_1966_p4-241.dfy) | CLOSED | K2 | 0 / 0 | finished with 17 verified, 0 errors |
| [imo_1966_p4-246](imo_1966_p4-246.dfy) | CLOSED | K2pow | 0 / 0 | finished with 35 verified, 0 errors |
| [imo_1966_p4-254](imo_1966_p4-254.dfy) | CLOSED | K2pow | 0 / 0 | finished with 41 verified, 0 errors |
| [imo_1966_p4-259](imo_1966_p4-259.dfy) | CLOSED | H0 | 0 / 0 | finished with 44 verified, 0 errors |
| [imo_1966_p4-262](imo_1966_p4-262.dfy) | CLOSED | H0 | 0 / 0 | finished with 46 verified, 0 errors |
| [imo_1966_p4-266](imo_1966_p4-266.dfy) | CLOSED | H0 | 0 / 0 | finished with 49 verified, 0 errors |
| [imo_1966_p4-273](imo_1966_p4-273.dfy) | CLOSED | K2pow | 0 / 0 | finished with 52 verified, 0 errors |
| [imo_1966_p4-278](imo_1966_p4-278.dfy) | CLOSED | H0 | 0 / 0 | finished with 55 verified, 0 errors |
| [imo_1966_p4-281](imo_1966_p4-281.dfy) | CLOSED | H0 | 0 / 0 | finished with 57 verified, 0 errors |
| [imo_1966_p4-286](imo_1966_p4-286.dfy) | CLOSED | pass2 | 0 / 0 | finished with 114 verified, 0 errors |
| [imo_1966_p4-291](imo_1966_p4-291.dfy) | CLOSED | K2pow | 0 / 0 | finished with 64 verified, 0 errors |
| [imo_1966_p4-294](imo_1966_p4-294.dfy) | CLOSED | H0 | 0 / 0 | finished with 66 verified, 0 errors |
| [imo_1966_p4-296](imo_1966_p4-296.dfy) | CLOSED | H0 | 0 / 0 | finished with 68 verified, 0 errors |
| [imo_1966_p4-313](imo_1966_p4-313.dfy) | CLOSED | H0 | 0 / 0 | finished with 71 verified, 0 errors |
| [imo_1966_p4-329](imo_1966_p4-329.dfy) | CLOSED | pass2 | 0 / 0 | finished with 114 verified, 0 errors |
| [imo_1966_p4-332](imo_1966_p4-332.dfy) | CLOSED | H0 | 0 / 0 | finished with 76 verified, 0 errors |
| [imo_1966_p4-348](imo_1966_p4-348.dfy) | CLOSED | K2pow | 0 / 0 | finished with 80 verified, 0 errors |
| [imo_1966_p4-364](imo_1966_p4-364.dfy) | CLOSED | pass2 | 0 / 0 | finished with 117 verified, 0 errors |
| [imo_1966_p4-367](imo_1966_p4-367.dfy) | CLOSED | H0 | 0 / 0 | finished with 85 verified, 0 errors |
| [imo_1966_p4-37](imo_1966_p4-37.dfy) | CLOSED | K2upow | 0 / 0 | finished with 21 verified, 0 errors |
| [imo_1966_p4-371](imo_1966_p4-371.dfy) | CLOSED | H0 | 0 / 0 | finished with 88 verified, 0 errors |
| [imo_1966_p4-397](imo_1966_p4-397.dfy) | CLOSED | pass2 | 0 / 2 | finished with 14 verified, 0 errors |
| [imo_1966_p4-400](imo_1966_p4-400.dfy) | CLOSED | pass2 | 0 / 0 | finished with 4 verified, 0 errors |
| [imo_1966_p4-424](imo_1966_p4-424.dfy) | CLOSED | pass2 | 1 / 0 | finished with 19 verified, 0 errors |
| [imo_1966_p4-54](imo_1966_p4-54.dfy) | CLOSED | H0 | 0 / 0 | finished with 24 verified, 0 errors |
| [imo_1966_p4-73](imo_1966_p4-73.dfy) | CLOSED | pass2 | 0 / 0 | finished with 134 verified, 0 errors |
| [imo_1966_p4-77](imo_1966_p4-77.dfy) | CLOSED | pass2 | 0 / 0 | finished with 130 verified, 0 errors |
| [imo_1966_p4-86](imo_1966_p4-86.dfy) | CLOSED | pass2 | 1 / 12 | finished with 117 verified, 0 errors |
| [imo_1973_p3-512](imo_1973_p3-512.dfy) | CLOSED | H0 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1973_p3-524](imo_1973_p3-524.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [imo_1973_p3-531](imo_1973_p3-531.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [imo_1973_p3-564](imo_1973_p3-564.dfy) | CLOSED | pass2 | 0 / 0 | finished with 4 verified, 0 errors |
| [imo_1973_p3-591](imo_1973_p3-591.dfy) | CLOSED | K3 | 0 / 0 | finished with 1 verified, 0 errors |
| [imo_1973_p3-601](imo_1973_p3-601.dfy) | CLOSED | H0 | 0 / 0 | finished with 3 verified, 0 errors |
| [imo_1973_p3-606](imo_1973_p3-606.dfy) | CLOSED | H0 | 0 / 0 | finished with 3 verified, 0 errors |
| [imo_1974_p5-1013](imo_1974_p5-1013.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-1024](imo_1974_p5-1024.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-1035](imo_1974_p5-1035.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-1046](imo_1974_p5-1046.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-1057](imo_1974_p5-1057.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-1567](imo_1974_p5-1567.dfy) | CLOSED | pass2 | 0 / 6 | finished with 158 verified, 0 errors |
| [imo_1974_p5-1629](imo_1974_p5-1629.dfy) | CLOSED | pass2 | 0 / 0 | finished with 95 verified, 0 errors |
| [imo_1974_p5-1801](imo_1974_p5-1801.dfy) | CLOSED | K2 | 0 / 0 | finished with 2 verified, 0 errors |
| [imo_1974_p5-1803](imo_1974_p5-1803.dfy) | CLOSED | pass2 | 0 / 0 | finished with 166 verified, 0 errors |
| [imo_1974_p5-383](imo_1974_p5-383.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-636](imo_1974_p5-636.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1974_p5-717](imo_1974_p5-717.dfy) | CLOSED | pass2 | 1 / 0 | finished with 5 verified, 0 errors |
| [imo_1983_p6-268](imo_1983_p6-268.dfy) | CLOSED | pass2 | 1 / 0 | finished with 1 verified, 0 errors |
| [imo_1984_p2-1685](imo_1984_p2-1685.dfy) | CLOSED | pass2 | 0 / 0 | finished with 199 verified, 0 errors |
| [imo_1984_p2-1713](imo_1984_p2-1713.dfy) | CLOSED | pass2 | 0 / 0 | finished with 80 verified, 0 errors |
| [imo_1984_p2-1725](imo_1984_p2-1725.dfy) | CLOSED | pass2 | 0 / 0 | finished with 27 verified, 0 errors |
| [imo_1984_p2-64](imo_1984_p2-64.dfy) | CLOSED | pass2 | 0 / 5 | finished with 210 verified, 0 errors |
| [imo_1992_p1-1145](imo_1992_p1-1145.dfy) | CLOSED | K2b | 0 / 0 | finished with 7 verified, 0 errors |
| [imo_1992_p1-1303](imo_1992_p1-1303.dfy) | CLOSED | K2 | 0 / 0 | finished with 6 verified, 0 errors |
| [imo_1992_p1-1343](imo_1992_p1-1343.dfy) | CLOSED | K2 | 0 / 0 | finished with 6 verified, 0 errors |
| [imo_1992_p1-1593](imo_1992_p1-1593.dfy) | CLOSED | K2c | 0 / 0 | finished with 9 verified, 0 errors |
| [imo_1992_p1-5471](imo_1992_p1-5471.dfy) | CLOSED | K2 | 0 / 0 | finished with 6 verified, 0 errors |
| [imo_1992_p1-780](imo_1992_p1-780.dfy) | CLOSED | K2 | 0 / 0 | finished with 9 verified, 0 errors |
| [imo_1992_p1-960](imo_1992_p1-960.dfy) | CLOSED | K2b | 0 / 0 | finished with 8 verified, 0 errors |
| [mathd_algebra_156-251](mathd_algebra_156-251.dfy) | CLOSED | K1 | 0 / 0 | finished with 2 verified, 0 errors |
| [mathd_algebra_156-313](mathd_algebra_156-313.dfy) | CLOSED | K1 | 0 / 0 | finished with 2 verified, 0 errors |
| [mathd_algebra_170-285](mathd_algebra_170-285.dfy) | CLOSED | K2 | 0 / 0 | finished with 3 verified, 0 errors |
| [mathd_algebra_342-130](mathd_algebra_342-130.dfy) | CLOSED | K5 | 0 / 1 | finished with 26 verified, 0 errors |
| [mathd_algebra_598-542](mathd_algebra_598-542.dfy) | CLOSED | SC_library | 0 / 2 | finished with 13 verified, 0 errors |
| [mathd_algebra_756-231](mathd_algebra_756-231.dfy) | CLOSED | K1 | 0 / 0 | finished with 2 verified, 0 errors |
| [mathd_algebra_756-438](mathd_algebra_756-438.dfy) | CLOSED | K5 | 0 / 0 | finished with 2 verified, 0 errors |
| [mathd_numbertheory_175-107](mathd_numbertheory_175-107.dfy) | CLOSED | K2pow | 0 / 0 | finished with 14 verified, 0 errors |
| [mathd_numbertheory_175-27](mathd_numbertheory_175-27.dfy) | CLOSED | K2pow | 0 / 0 | finished with 5 verified, 0 errors |
| [mathd_numbertheory_175-54](mathd_numbertheory_175-54.dfy) | CLOSED | cite_opaque | 0 / 0 | finished with 15 verified, 0 errors |
| [mathd_numbertheory_175-71](mathd_numbertheory_175-71.dfy) | CLOSED | K5 | 0 / 0 | finished with 16 verified, 0 errors |
| [mathd_numbertheory_175-79](mathd_numbertheory_175-79.dfy) | CLOSED | pass2 | 0 / 2 | finished with 36 verified, 0 errors |
| [mathd_numbertheory_175-93](mathd_numbertheory_175-93.dfy) | CLOSED | K5 | 0 / 0 | finished with 24 verified, 0 errors |
| [mathd_numbertheory_618-114](mathd_numbertheory_618-114.dfy) | CLOSED | k5 | 0 / 0 | finished with 38 verified, 0 errors |
| [mathd_numbertheory_618-139](mathd_numbertheory_618-139.dfy) | CLOSED | pass2 | 0 / 1 | finished with 213 verified, 0 errors |
| [mathd_numbertheory_618-177](mathd_numbertheory_618-177.dfy) | CLOSED | pass2 | 0 / 0 | finished with 31 verified, 0 errors |
| [mathd_numbertheory_618-183](mathd_numbertheory_618-183.dfy) | CLOSED | pass2 | 0 / 0 | finished with 31 verified, 0 errors |
| [mathd_numbertheory_618-189](mathd_numbertheory_618-189.dfy) | CLOSED | pass2 | 0 / 0 | finished with 31 verified, 0 errors |
| [mathd_numbertheory_618-195](mathd_numbertheory_618-195.dfy) | CLOSED | pass2 | 0 / 0 | finished with 397 verified, 0 errors |
| [mathd_numbertheory_618-201](mathd_numbertheory_618-201.dfy) | CLOSED | pass2 | 0 / 0 | finished with 397 verified, 0 errors |
| [mathd_numbertheory_618-237](mathd_numbertheory_618-237.dfy) | CLOSED | pass2 | 0 / 0 | finished with 397 verified, 0 errors |
| [mathd_numbertheory_618-243](mathd_numbertheory_618-243.dfy) | CLOSED | pass2 | 0 / 0 | finished with 397 verified, 0 errors |
| [mathd_numbertheory_618-267](mathd_numbertheory_618-267.dfy) | CLOSED | pass2 | 0 / 0 | finished with 229 verified, 0 errors |
| [mathd_numbertheory_618-279](mathd_numbertheory_618-279.dfy) | CLOSED | pass2 | 0 / 0 | finished with 229 verified, 0 errors |
| [mathd_numbertheory_618-285](mathd_numbertheory_618-285.dfy) | CLOSED | pass2 | 0 / 0 | finished with 219 verified, 0 errors |
| [mathd_numbertheory_618-291](mathd_numbertheory_618-291.dfy) | CLOSED | pass2 | 0 / 0 | finished with 223 verified, 0 errors |
| [mathd_numbertheory_618-297](mathd_numbertheory_618-297.dfy) | CLOSED | pass2 | 0 / 0 | finished with 219 verified, 0 errors |
| [mathd_numbertheory_618-303](mathd_numbertheory_618-303.dfy) | CLOSED | pass2 | 0 / 0 | finished with 229 verified, 0 errors |
| [mathd_numbertheory_618-309](mathd_numbertheory_618-309.dfy) | CLOSED | pass2 | 0 / 0 | finished with 229 verified, 0 errors |
| [mathd_numbertheory_618-327](mathd_numbertheory_618-327.dfy) | CLOSED | pass2 | 0 / 0 | finished with 227 verified, 0 errors |
| [mathd_numbertheory_618-333](mathd_numbertheory_618-333.dfy) | CLOSED | pass2 | 0 / 0 | finished with 11 verified, 0 errors |
| [mathd_numbertheory_618-345](mathd_numbertheory_618-345.dfy) | CLOSED | pass2 | 0 / 0 | finished with 11 verified, 0 errors |
| [mathd_numbertheory_618-357](mathd_numbertheory_618-357.dfy) | CLOSED | pass2 | 0 / 0 | finished with 613 verified, 0 errors |
| [mathd_numbertheory_618-363](mathd_numbertheory_618-363.dfy) | CLOSED | pass2 | 0 / 0 | finished with 613 verified, 0 errors |
| [mathd_numbertheory_618-369](mathd_numbertheory_618-369.dfy) | CLOSED | K3K2 | 0 / 0 | finished with 11 verified, 0 errors |
| [mathd_numbertheory_618-382](mathd_numbertheory_618-382.dfy) | CLOSED | K3K2 | 0 / 0 | finished with 11 verified, 0 errors |
| [mathd_numbertheory_618-396](mathd_numbertheory_618-396.dfy) | CLOSED | pass2 | 0 / 0 | finished with 613 verified, 0 errors |
| [mathd_numbertheory_84-26](mathd_numbertheory_84-26.dfy) | CLOSED | K5 | 0 / 0 | finished with 8 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-104](numbertheory_2pownm1prime_nprime-104.dfy) | CLOSED | K1 | 0 / 1 | finished with 15 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-284](numbertheory_2pownm1prime_nprime-284.dfy) | CLOSED | pass2 | 0 / 0 | finished with 15 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-286](numbertheory_2pownm1prime_nprime-286.dfy) | CLOSED | K1 | 0 / 0 | finished with 11 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-324](numbertheory_2pownm1prime_nprime-324.dfy) | CLOSED | H0 | 0 / 1 | finished with 12 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-333](numbertheory_2pownm1prime_nprime-333.dfy) | CLOSED | H0 | 0 / 0 | finished with 11 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-338](numbertheory_2pownm1prime_nprime-338.dfy) | CLOSED | H0 | 0 / 0 | finished with 17 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-380](numbertheory_2pownm1prime_nprime-380.dfy) | CLOSED | H0 | 0 / 1 | finished with 14 verified, 0 errors |
| [numbertheory_2pownm1prime_nprime-393](numbertheory_2pownm1prime_nprime-393.dfy) | CLOSED | H0 | 0 / 1 | finished with 14 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-109](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-109.dfy) | CLOSED | pass2 | 1 / 0 | finished with 165 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-111](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-111.dfy) | CLOSED | pass2 | 1 / 1 | finished with 139 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-113](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-113.dfy) | CLOSED | H0 | 0 / 1 | finished with 66 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-124](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-124.dfy) | CLOSED | pass2 | 0 / 0 | finished with 5 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-129](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-129.dfy) | CLOSED | K1 | 0 / 0 | finished with 52 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-146](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-146.dfy) | CLOSED | pass2 | 0 / 1 | finished with 7 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-150](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-150.dfy) | CLOSED | pass2 | 0 / 0 | finished with 3 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-177](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-177.dfy) | CLOSED | pass2 | 0 / 0 | finished with 5 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-182](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-182.dfy) | CLOSED | pass2 | 0 / 0 | finished with 67 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-220](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-220.dfy) | CLOSED | H0 | 0 / 0 | finished with 156 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-221](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-221.dfy) | CLOSED | H0 | 0 / 0 | finished with 332 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-222](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-222.dfy) | CLOSED | H0 | 0 / 0 | finished with 218 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-226](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-226.dfy) | CLOSED | pass2 | 1 / 0 | finished with 50 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-233](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-233.dfy) | CLOSED | pass2 | 1 / 0 | finished with 76 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-240](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-240.dfy) | CLOSED | pass2 | 1 / 0 | finished with 50 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-243](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-243.dfy) | CLOSED | pass2 | 1 / 0 | finished with 50 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-246](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-246.dfy) | CLOSED | pass2 | 1 / 0 | finished with 42 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-250](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-250.dfy) | CLOSED | H0 | 0 / 1 | finished with 77 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-261](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-261.dfy) | CLOSED | pass2 | 0 / 0 | finished with 70 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-266](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-266.dfy) | CLOSED | L266_K1K4 | 0 / 0 | finished with 69 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-283](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-283.dfy) | CLOSED | L283_K2pow | 0 / 1 | finished with 100 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-287](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-287.dfy) | CLOSED | L287_K2pow | 0 / 0 | finished with 61 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-314](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-314.dfy) | CLOSED | pass2 | 0 / 0 | finished with 85 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-319](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-319.dfy) | CLOSED | K1 | 0 / 0 | finished with 78 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-335](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-335.dfy) | CLOSED | H0 | 0 / 0 | finished with 167 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-336](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-336.dfy) | CLOSED | H0 | 0 / 0 | finished with 343 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-337](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-337.dfy) | CLOSED | H0 | 0 / 0 | finished with 229 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-389](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-389.dfy) | CLOSED | K2pow | 0 / 0 | finished with 159 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-390](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-390.dfy) | CLOSED | K2pow | 0 / 0 | finished with 242 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-394](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-394.dfy) | CLOSED | K2pow | 0 / 0 | finished with 254 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-398](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-398.dfy) | CLOSED | H0 | 0 / 0 | finished with 98 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-40](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-40.dfy) | CLOSED | pass2 | 0 / 1 | finished with 104 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-483](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-483.dfy) | CLOSED | K2pow | 0 / 0 | finished with 39 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-516](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-516.dfy) | CLOSED | K1K4 | 0 / 0 | finished with 75 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-545](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-545.dfy) | CLOSED | K5 | 0 / 0 | finished with 87 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-57](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-57.dfy) | CLOSED | pass2 | 0 / 0 | finished with 86 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-59](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-59.dfy) | CLOSED | pass2 | 1 / 4 | finished with 47 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-88](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-88.dfy) | CLOSED | pass2 | 0 / 0 | finished with 47 verified, 0 errors |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-98](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-98.dfy) | CLOSED | pass2 | 1 / 0 | finished with 47 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-113](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-113.dfy) | CLOSED | K2pow | 0 / 0 | finished with 20 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-129](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-129.dfy) | CLOSED | K2pow | 0 / 0 | finished with 21 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-148](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-148.dfy) | CLOSED | K2pow | 0 / 0 | finished with 290 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-150](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-150.dfy) | CLOSED | K2pow | 0 / 0 | finished with 22 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-231](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-231.dfy) | CLOSED | K2pow | 0 / 0 | finished with 26 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-247](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-247.dfy) | CLOSED | K2pow | 0 / 0 | finished with 27 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-265](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-265.dfy) | CLOSED | split+K2pow | 0 / 0 | finished with 24 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-306](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-306.dfy) | CLOSED | K2pow | 0 / 0 | finished with 41 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-390](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-390.dfy) | CLOSED | SCsplit_helper | 0 / 0 | finished with 27 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-408](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-408.dfy) | CLOSED | K1 | 0 / 0 | finished with 55 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-447](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-447.dfy) | CLOSED | K1 | 0 / 0 | finished with 44 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-450](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-450.dfy) | CLOSED | K3K2pow | 0 / 0 | finished with 4 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-60](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-60.dfy) | CLOSED | K3+K2pow | 0 / 0 | finished with 35 verified, 0 errors |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-97](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-97.dfy) | CLOSED | K2pow | 0 / 0 | finished with 19 verified, 0 errors |
| [aime_1983_p3-387](aime_1983_p3-387.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [aime_1984_p1-15](aime_1984_p1-15.dfy) | NOT CLOSED |  | 0 / 1 | failed |
| [aime_1984_p1-22](aime_1984_p1-22.dfy) | NOT CLOSED |  | 0 / 1 | failed |
| [aime_1999_p11-335](aime_1999_p11-335.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [aime_1999_p11-346](aime_1999_p11-346.dfy) | NOT CLOSED |  | 0 / 34 | timeout |
| [algebra_apbon2pownleqapownpbpowon2-243](algebra_apbon2pownleqapownpbpowon2-243.dfy) | NOT CLOSED |  | 1 / 0 | failed |
| [algebra_apbon2pownleqapownpbpowon2-272](algebra_apbon2pownleqapownpbpowon2-272.dfy) | NOT CLOSED |  | 0 / 5 | oor |
| [algebra_apbon2pownleqapownpbpowon2-274](algebra_apbon2pownleqapownpbpowon2-274.dfy) | NOT CLOSED |  | 1 / 5 | failed |
| [algebra_apbon2pownleqapownpbpowon2-648](algebra_apbon2pownleqapownpbpowon2-648.dfy) | NOT CLOSED |  | 1 / 0 | failed |
| [algebra_bleqa_apbon2msqrtableqambsqon8b-33](algebra_bleqa_apbon2msqrtableqambsqon8b-33.dfy) | NOT CLOSED |  | 1 / 0 | failed |
| [amc12_2001_p5-18](amc12_2001_p5-18.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12_2001_p5-53](amc12_2001_p5-53.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12a_2003_p25-26](amc12a_2003_p25-26.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [amc12a_2003_p25-31](amc12a_2003_p25-31.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [amc12a_2003_p25-37](amc12a_2003_p25-37.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [amc12a_2009_p15-106](amc12a_2009_p15-106.dfy) | NOT CLOSED |  | 0 / 0 | error |
| [amc12a_2009_p15-175](amc12a_2009_p15-175.dfy) | NOT CLOSED |  | 0 / 18 | timeout |
| [amc12a_2009_p15-18](amc12a_2009_p15-18.dfy) | NOT CLOSED |  | 0 / 11 | oor |
| [amc12a_2009_p15-496](amc12a_2009_p15-496.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12a_2009_p15-537](amc12a_2009_p15-537.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12a_2009_p15-727](amc12a_2009_p15-727.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12a_2009_p15-737](amc12a_2009_p15-737.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [amc12a_2019_p21-29](amc12a_2019_p21-29.dfy) | NOT CLOSED |  | 0 / 2 | failed |
| [amc12a_2019_p21-76](amc12a_2019_p21-76.dfy) | NOT CLOSED |  | 0 / 4 | oor |
| [amc12a_2021_p19-1733](amc12a_2021_p19-1733.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [amc12b_2020_p21-1485](amc12b_2020_p21-1485.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [amc12b_2020_p22-25](amc12b_2020_p22-25.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [imo_1964_p1_1-45](imo_1964_p1_1-45.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [imo_1965_p1-1021](imo_1965_p1-1021.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [imo_1965_p1-1290](imo_1965_p1-1290.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [imo_1965_p1-1292](imo_1965_p1-1292.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [imo_1965_p1-363](imo_1965_p1-363.dfy) | NOT CLOSED |  | 0 / 4 | failed |
| [imo_1966_p4-264](imo_1966_p4-264.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [imo_1966_p4-27](imo_1966_p4-27.dfy) | NOT CLOSED |  | 0 / 7 | oor |
| [imo_1966_p4-369](imo_1966_p4-369.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [imo_1966_p4-394](imo_1966_p4-394.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [imo_1966_p5-1764](imo_1966_p5-1764.dfy) | NOT CLOSED |  | 0 / 8 | timeout |
| [imo_1966_p5-1775](imo_1966_p5-1775.dfy) | NOT CLOSED |  | 0 / 8 | timeout |
| [mathd_algebra_362-217](mathd_algebra_362-217.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [mathd_numbertheory_618-219](mathd_numbertheory_618-219.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-225](mathd_numbertheory_618-225.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-231](mathd_numbertheory_618-231.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-249](mathd_numbertheory_618-249.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-255](mathd_numbertheory_618-255.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-261](mathd_numbertheory_618-261.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-315](mathd_numbertheory_618-315.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-321](mathd_numbertheory_618-321.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-351](mathd_numbertheory_618-351.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [mathd_numbertheory_618-389](mathd_numbertheory_618-389.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-176](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-176.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-195](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-195.dfy) | NOT CLOSED |  | 0 / 1 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-223](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-223.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-313](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-313.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-338](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-338.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-341](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-341.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-348](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-348.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-355](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-355.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-358](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-358.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-361](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-361.dfy) | NOT CLOSED |  | 0 / 3 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-391](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-391.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-396](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-396.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-397](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-397.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-453](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-453.dfy) | NOT CLOSED |  | 0 / 6 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-460](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-460.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-508](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-508.dfy) | NOT CLOSED |  | 0 / 1 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-510](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-510.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-512](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-512.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-528](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-528.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-535](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-535.dfy) | NOT CLOSED |  | 0 / 1 | oor |
| [numbertheory_3pow2pownm1mod2pownp3eq2pownp2-555](numbertheory_3pow2pownm1mod2pownp3eq2pownp2-555.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_aoddbdiv4asqpbsqmod8eq1-184](numbertheory_aoddbdiv4asqpbsqmod8eq1-184.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-164](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-164.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-170](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-170.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-18](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-18.dfy) | NOT CLOSED |  | 0 / 13 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-189](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-189.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-227](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-227.dfy) | NOT CLOSED |  | 1 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-229](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-229.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-293](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-293.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-317](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-317.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-318](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-318.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-319](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-319.dfy) | NOT CLOSED |  | 0 / 0 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-324](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-324.dfy) | NOT CLOSED |  | 0 / 0 | timeout |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-407](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-407.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-413](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-413.dfy) | NOT CLOSED |  | 0 / 1 | failed |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-442](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-442.dfy) | NOT CLOSED |  | 0 / 0 | failed |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-77](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-77.dfy) | NOT CLOSED |  | 0 / 17 | oor |
| [numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-95](numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown-95.dfy) | NOT CLOSED |  | 0 / 0 | oor |