| 1993 |
2024/02/01 01:13:54
|
n < m \/ n = m \/ n > m
|
test1234 |
Success |
|
|
| 1992 |
2024/01/31 21:30:38
|
n * S m = n + n * m
|
test1234 |
Success |
|
|
| 1991 |
2024/01/31 19:57:03
|
forall f: bool -> bool, f^3(x) = f(x)
|
test1234 |
Success |
|
|
| 1990 |
2024/01/31 08:19:38
|
1 + 1 = 2
|
test1234 |
Success |
|
|
| 1989 |
2024/01/31 08:15:20
|
plus_comm
|
test1234 |
Success |
|
|
| 1988 |
2024/01/31 07:25:43
|
plus_assoc
|
test1234 |
Success |
|
|
| 1987 |
2023/09/04 21:27:58
|
unique (unique l) = l
|
aai |
Success |
|
|
| 1986 |
2023/09/04 20:56:41
|
count l n = count (rev l) n
|
aai |
Failure |
|
|
| 1985 |
2023/09/04 12:42:22
|
Multiplication in F_2 is idempotent
|
aai |
Success |
|
|
| 1984 |
2023/09/03 16:01:40
|
n < m \/ n = m \/ n > m
|
aai |
Success |
|
|
| 1983 |
2023/09/03 15:47:47
|
Definitions of injectivity
|
aai |
Success |
|
|
| 1982 |
2023/09/03 15:46:24
|
Definitions of injectivity
|
aai |
Failure |
|
|
| 1981 |
2023/09/03 15:07:57
|
Cumulative sum of list
|
aai |
Success |
|
|
| 1980 |
2023/09/02 21:28:06
|
Three is prime
|
aai |
Success |
|
|
| 1979 |
2023/09/02 18:10:46
|
Boolean-hole principle
|
aai |
Success |
|
|
| 1978 |
2023/09/02 17:53:58
|
De Morgan's laws in Coq
|
aai |
Success |
|
|
| 1977 |
2023/09/02 14:22:35
|
mult_n_O
|
aai |
Success |
|
|
| 1976 |
2023/09/02 14:20:37
|
gcd(n, n+1) = 1
|
aai |
Success |
|
|
| 1975 |
2023/09/02 13:53:48
|
Summand of one
|
aai |
Success |
|
|
| 1974 |
2023/09/02 13:44:03
|
forall l: list nat, l @ [0] <> []
|
aai |
Success |
|
|
| 1973 |
2023/09/02 09:29:49
|
n * S m = n + n * m
|
aai |
Success |
|
|
| 1972 |
2023/09/02 09:08:30
|
forall f: bool -> bool, f^3(x) = f(x)
|
aai |
Success |
|
|
| 1971 |
2023/09/01 22:07:49
|
1 + 1 = 2
|
aai |
Success |
|
|
| 1970 |
2023/09/01 22:02:31
|
plus_comm
|
aai |
Success |
|
|
| 1969 |
2023/09/01 21:39:44
|
plus_assoc
|
aai |
Success |
|
|
| 1968 |
2023/07/17 11:38:37
|
1 + 1 = 2
|
fakeprogrammer |
Success |
|
|
| 1967 |
2023/04/09 04:50:31
|
1 + 1 = 2
|
kivantium |
Success |
|
|
| 1966 |
2023/04/09 04:19:52
|
plus_comm
|
kivantium |
Success |
|
|
| 1965 |
2023/04/09 04:03:17
|
plus_assoc
|
kivantium |
Success |
|
|
| 1964 |
2023/04/09 04:02:36
|
plus_assoc
|
kivantium |
Failure |
|
|
| 1963 |
2022/10/20 20:13:13
|
plus_assoc
|
mii |
Success |
|
|
| 1962 |
2022/10/20 20:12:22
|
plus_assoc
|
mii |
Failure |
|
|
| 1961 |
2022/09/23 05:39:01
|
n < m \/ n = m \/ n > m
|
jeb |
Success |
|
|
| 1960 |
2022/09/23 05:18:03
|
n < m \/ n = m \/ n > m
|
jeb |
Failure |
|
|
| 1959 |
2022/09/23 02:46:52
|
n * S m = n + n * m
|
jeb |
Success |
|
|
| 1958 |
2022/09/23 02:19:00
|
n * S m = n + n * m
|
jeb |
Failure |
|
|
| 1957 |
2022/09/23 02:14:02
|
n * S m = n + n * m
|
jeb |
Failure |
|
|
| 1956 |
2022/09/23 02:01:14
|
n * S m = n + n * m
|
jeb |
Failure |
|
|
| 1955 |
2022/09/23 01:50:50
|
n * S m = n + n * m
|
jeb |
Failure |
|
|
| 1954 |
2022/09/23 01:01:30
|
forall f: bool -> bool, f^3(x) = f(x)
|
jeb |
Success |
|
|
| 1953 |
2022/09/23 00:28:34
|
1 + 1 = 2
|
jeb |
Success |
|
|
| 1952 |
2022/07/25 01:02:10
|
Product of n consecutive integers is divisible by n!
|
fairy_lettuce |
Success |
|
|
| 1951 |
2022/07/23 20:45:57
|
n < m \/ n = m \/ n > m
|
fairy_lettuce |
Success |
|
|
| 1950 |
2022/07/23 18:59:51
|
n * S m = n + n * m
|
fairy_lettuce |
Success |
|
|
| 1949 |
2022/07/23 18:56:02
|
forall f: bool -> bool, f^3(x) = f(x)
|
fairy_lettuce |
Success |
|
|
| 1948 |
2022/07/23 17:58:57
|
plus_comm
|
fairy_lettuce |
Success |
|
|
| 1947 |
2022/07/23 17:57:28
|
1 + 1 = 2
|
fairy_lettuce |
Success |
|
|
| 1946 |
2022/07/23 17:55:16
|
plus_comm
|
fairy_lettuce |
Success |
|
|
| 1945 |
2022/07/23 17:49:01
|
plus_assoc
|
fairy_lettuce |
Success |
|
|
| 1944 |
2022/07/23 17:48:03
|
plus_assoc
|
fairy_lettuce |
Failure |
|
|
| 1943 |
2022/07/18 21:02:43
|
forall f: bool -> bool, f^3(x) = f(x)
|
platypus |
Success |
|
|
| 1942 |
2022/06/23 17:54:09
|
mult_n_O
|
toga |
Success |
|
|
| 1941 |
2022/06/23 13:54:12
|
plus_assoc
|
nikosai |
Failure |
|
|
| 1940 |
2022/06/23 13:12:05
|
gcd(n, n+1) = 1
|
toga |
Success |
|
|
| 1939 |
2022/06/22 14:15:44
|
forall l: list nat, l @ [0] <> []
|
toga |
Success |
|
|
| 1938 |
2022/06/22 14:01:02
|
forall f: bool -> bool, f^3(x) = f(x)
|
toga |
Success |
|
|
| 1937 |
2022/06/21 14:28:39
|
Summand of one
|
toga |
Success |
|
|
| 1936 |
2022/06/15 16:06:22
|
n * S m = n + n * m
|
toga |
Success |
|
|
| 1935 |
2022/06/14 12:26:41
|
plus_comm
|
toga |
Success |
|
|
| 1934 |
2022/06/13 19:51:17
|
plus_comm
|
toga |
Success |
|
|
| 1933 |
2022/06/13 18:39:02
|
1 + 1 = 2
|
toga |
Success |
|
|
| 1932 |
2022/06/11 17:58:25
|
plus_assoc
|
toga |
Success |
|
|
| 1931 |
2022/04/20 04:08:08
|
count_occ_app
|
minus3theta |
Success |
|
|
| 1930 |
2022/04/19 06:42:20
|
Flat CPO
|
minus3theta |
Success |
|
|
| 1929 |
2022/04/19 05:57:43
|
Swap twice
|
minus3theta |
Success |
|
|
| 1928 |
2022/04/19 05:56:05
|
S preserves comparison
|
minus3theta |
Success |
|
|
| 1927 |
2022/04/19 05:54:18
|
Sum of n^3
|
minus3theta |
Success |
|
|
| 1926 |
2022/04/19 05:48:38
|
Boolean-hole principle revisited
|
minus3theta |
Success |
|
|
| 1925 |
2022/04/19 05:37:35
|
Cumulative sum of list
|
minus3theta |
Success |
|
|
| 1924 |
2022/04/19 05:02:26
|
Zero test
|
minus3theta |
Success |
|
|
| 1923 |
2022/04/19 05:00:07
|
eq_sym?
|
minus3theta |
Success |
|
|
| 1922 |
2022/04/11 17:42:24
|
Zero test
|
minus3theta |
Failure |
|
|
| 1921 |
2022/04/11 15:49:29
|
Double
|
minus3theta |
Success |
|
|
| 1920 |
2022/04/11 15:21:22
|
Yoneda embedding for preorder
|
minus3theta |
Success |
|
|
| 1919 |
2022/04/11 15:20:37
|
Yoneda embedding for preorder
|
minus3theta |
Failure |
|
|
| 1918 |
2022/04/11 14:25:45
|
unique (unique l) = l
|
minus3theta |
Success |
|
|
| 1917 |
2022/04/10 02:57:17
|
Boolean-hole principle
|
minus3theta |
Success |
|
|
| 1916 |
2022/04/10 00:57:00
|
De Morgan's laws in Coq
|
minus3theta |
Success |
|
|
| 1915 |
2022/04/10 00:48:01
|
mult_n_O
|
minus3theta |
Success |
|
|
| 1914 |
2022/04/09 00:59:02
|
count l n = count (rev l) n
|
minus3theta |
Failure |
|
|
| 1913 |
2022/04/08 21:12:55
|
gcd(n, n+1) = 1
|
minus3theta |
Success |
|
|
| 1912 |
2022/04/08 21:11:47
|
gcd(n, n+1) = 1
|
minus3theta |
Failure |
|
|
| 1911 |
2022/04/08 20:53:14
|
Identity permutation
|
minus3theta |
Success |
|
|
| 1910 |
2022/04/08 18:26:29
|
Multiplication in F_2 is idempotent
|
minus3theta |
Success |
|
|
| 1909 |
2022/04/08 17:19:30
|
Definitions of injectivity
|
minus3theta |
Success |
|
|
| 1908 |
2022/04/08 16:06:22
|
Definitions of injectivity
|
minus3theta |
Rejected |
|
|
| 1907 |
2022/04/08 12:45:09
|
Summand of one
|
minus3theta |
Success |
|
|
| 1906 |
2022/04/08 12:44:34
|
Summand of one
|
minus3theta |
Failure |
|
|
| 1905 |
2022/04/08 12:43:42
|
Summand of one
|
minus3theta |
Failure |
|
|
| 1904 |
2022/01/30 22:09:07
|
Summand of one
|
myazakky |
Success |
|
|
| 1903 |
2022/01/30 21:59:58
|
plus_comm
|
myazakky |
Success |
|
|
| 1902 |
2022/01/30 21:54:31
|
plus_assoc
|
myazakky |
Success |
|
|
| 1901 |
2022/01/10 18:23:46
|
plus_assoc
|
magurofly |
Success |
|
|
| 1900 |
2021/09/18 22:03:19
|
1 + 1 = 2
|
jambo |
Success |
|
|
| 1899 |
2021/09/18 22:02:46
|
1 + 1 = 2
|
jambo |
Failure |
|
|
| 1898 |
2021/09/17 12:28:24
|
1 + 1 = 2
|
platypus |
Success |
|
|
| 1897 |
2021/09/17 12:27:25
|
plus_comm
|
platypus |
Success |
|
|
| 1896 |
2021/09/17 12:26:50
|
plus_comm
|
platypus |
Failure |
|
|
| 1895 |
2021/09/17 12:25:14
|
plus_comm
|
platypus |
Failure |
|
|
| 1894 |
2021/09/17 11:45:38
|
plus_assoc
|
platypus |
Success |
|
|
| 1893 |
2021/09/15 03:02:43
|
n * S m = n + n * m
|
TanakaTaroh |
Success |
|
|
| 1892 |
2021/09/15 03:02:12
|
n * S m = n + n * m
|
TanakaTaroh |
Failure |
|
|
| 1891 |
2021/09/15 02:34:40
|
forall f: bool -> bool, f^3(x) = f(x)
|
TanakaTaroh |
Success |
|
|
| 1890 |
2021/09/14 18:43:13
|
1 + 1 = 2
|
TanakaTaroh |
Success |
|
|
| 1889 |
2021/09/14 18:36:34
|
plus_comm
|
TanakaTaroh |
Success |
|
|
| 1888 |
2021/09/13 04:34:22
|
plus_assoc
|
TanakaTaroh |
Success |
|
|
| 1887 |
2021/04/29 19:05:18
|
Friends and strangers
|
pyusuke |
Success |
|
|
| 1886 |
2021/04/29 18:56:28
|
Flat CPO
|
pyusuke |
Success |
|
|
| 1885 |
2021/04/10 11:54:41
|
n < m \/ n = m \/ n > m
|
sash0 |
Success |
|
|
| 1884 |
2021/04/10 00:07:43
|
plus_comm
|
sash0 |
Success |
|
|
| 1883 |
2021/04/09 23:49:52
|
plus_assoc
|
sash0 |
Success |
|
|
| 1882 |
2021/03/19 11:38:30
|
1 + 1 = 2
|
jeb |
Success |
|
|
| 1881 |
2021/02/20 13:34:52
|
Definitions of injectivity
|
matonix |
Success |
|
|
| 1880 |
2021/02/17 00:53:46
|
Summand of one
|
matonix |
Success |
|
|
| 1879 |
2021/02/15 01:36:56
|
Cumulative sum of list
|
matonix |
Success |
|
|
| 1878 |
2021/02/10 01:12:35
|
forall l: list nat, l @ [0] <> []
|
matonix |
Success |
|
|
| 1877 |
2021/02/08 23:16:38
|
Product of n consecutive integers is divisible by n!
|
matonix |
Success |
|
|
| 1876 |
2021/01/15 01:54:09
|
n < m \/ n = m \/ n > m
|
matonix |
Success |
|
|
| 1875 |
2021/01/13 01:39:58
|
n * S m = n + n * m
|
matonix |
Success |
|
|
| 1874 |
2021/01/12 01:00:16
|
forall f: bool -> bool, f^3(x) = f(x)
|
matonix |
Success |
|
|
| 1873 |
2021/01/12 00:22:20
|
1 + 1 = 2
|
matonix |
Success |
|
|
| 1872 |
2021/01/10 20:09:34
|
plus_comm
|
matonix |
Success |
|
|
| 1871 |
2021/01/08 01:58:25
|
plus_assoc
|
matonix |
Success |
|
|
| 1870 |
2021/01/08 01:57:17
|
plus_assoc
|
matonix |
Failure |
|
|
| 1869 |
2020/11/29 18:28:54
|
Definitions of injectivity
|
pyusuke |
Success |
|
|
| 1868 |
2020/11/29 18:28:25
|
Definitions of injectivity
|
pyusuke |
Failure |
|
|
| 1867 |
2020/11/29 17:53:06
|
Zero test
|
pyusuke |
Success |
|
|
| 1866 |
2020/11/29 17:26:45
|
Constructor is injective
|
pyusuke |
Success |
|
|
| 1865 |
2020/11/29 17:26:19
|
Constructor is injective
|
pyusuke |
Failure |
|
|
| 1864 |
2020/11/29 17:21:01
|
Yoneda embedding for preorder
|
pyusuke |
Success |
|
|
| 1863 |
2020/11/29 17:20:27
|
Yoneda embedding for preorder
|
pyusuke |
Failure |
|
|
| 1862 |
2020/11/29 17:19:04
|
Yoneda embedding for preorder
|
pyusuke |
Failure |
|
|
| 1861 |
2020/11/29 17:11:04
|
De Morgan's laws in Coq
|
pyusuke |
Success |
|
|
| 1860 |
2020/11/29 16:47:45
|
mult_n_O
|
pyusuke |
Success |
|
|
| 1859 |
2020/11/29 16:38:45
|
Three is prime
|
pyusuke |
Success |
|
|
| 1858 |
2020/11/29 15:52:21
|
Boolean-hole principle
|
pyusuke |
Success |
|
|
| 1857 |
2020/11/29 15:51:27
|
Summand of one
|
pyusuke |
Failure |
|
|
| 1856 |
2020/11/29 13:13:21
|
forall l: list nat, l @ [0] <> []
|
pyusuke |
Success |
|
|
| 1855 |
2020/11/28 17:55:41
|
plus_comm
|
pyusuke |
Success |
|
|
| 1854 |
2020/11/28 17:55:08
|
plus_comm
|
pyusuke |
Failure |
|
|
| 1853 |
2020/11/28 17:53:26
|
plus_assoc
|
pyusuke |
Success |
|
|
| 1852 |
2020/11/28 17:31:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
pyusuke |
Success |
|
|
| 1851 |
2020/11/28 16:54:16
|
forall f: bool -> bool, f^3(x) = f(x)
|
pyusuke |
Success |
|
|
| 1850 |
2020/11/28 16:29:37
|
1 + 1 = 2
|
pyusuke |
Success |
|
|
| 1849 |
2020/11/28 16:25:34
|
n * S m = n + n * m
|
pyusuke |
Success |
|
|
| 1848 |
2020/11/28 15:59:55
|
1 + 1 = 2
|
pyusuke |
Success |
|
|
| 1847 |
2020/11/07 19:23:19
|
Summand of one
|
hiromi_mi |
Success |
|
|
| 1846 |
2020/11/07 18:30:25
|
forall l: list nat, l @ [0] <> []
|
hiromi_mi |
Success |
|
|
| 1845 |
2020/11/07 18:10:14
|
n < m \/ n = m \/ n > m
|
hiromi_mi |
Success |
|
|
| 1844 |
2020/11/07 18:08:18
|
n * S m = n + n * m
|
hiromi_mi |
Success |
|
|
| 1843 |
2020/11/07 18:06:57
|
forall f: bool -> bool, f^3(x) = f(x)
|
hiromi_mi |
Success |
|
|
| 1842 |
2020/11/07 17:52:43
|
1 + 1 = 2
|
hiromi_mi |
Success |
|
|
| 1841 |
2020/11/07 17:52:14
|
1 + 1 = 2
|
hiromi_mi |
Failure |
|
|
| 1840 |
2020/11/07 17:51:18
|
plus_comm
|
hiromi_mi |
Success |
|
|
| 1839 |
2020/11/07 17:48:50
|
plus_assoc
|
hiromi_mi |
Success |
|
|
| 1838 |
2020/11/03 16:51:47
|
Definitions of injectivity
|
aaaa |
Success |
|
|
| 1837 |
2020/11/03 16:48:17
|
Definitions of injectivity
|
aaaa |
Failure |
|
|
| 1836 |
2020/11/03 16:21:18
|
Definitions of injectivity
|
aaaa |
Rejected |
|
|
| 1835 |
2020/11/03 16:03:11
|
forall l: list nat, l @ [0] <> []
|
aaaa |
Success |
|
|
| 1834 |
2020/11/03 15:50:54
|
Two is not Three
|
aaaa |
Success |
|
|
| 1833 |
2020/11/03 15:46:19
|
Two is not Three
|
aaaa |
Success |
|
|
| 1832 |
2020/11/03 15:43:11
|
Boolean-hole principle
|
aaaa |
Success |
|
|
| 1831 |
2020/11/03 15:36:28
|
Boolean-hole principle
|
aaaa |
Success |
|
|
| 1830 |
2020/11/03 15:19:08
|
Two is not Three
|
aaaa |
Success |
|
|
| 1829 |
2020/11/03 13:51:07
|
1 + 1 = 2
|
aaaa |
Success |
|
|
| 1828 |
2020/11/03 13:47:20
|
n < m \/ n = m \/ n > m
|
aaaa |
Success |
|
|
| 1827 |
2020/11/03 12:03:14
|
Summand of one
|
aaaa |
Success |
|
|
| 1826 |
2020/11/03 11:46:37
|
n * S m = n + n * m
|
aaaa |
Success |
|
|
| 1825 |
2020/11/03 11:11:36
|
plus_assoc
|
aaaa |
Success |
|
|
| 1824 |
2020/11/03 11:00:10
|
plus_comm
|
aaaa |
Success |
|
|
| 1823 |
2020/11/02 23:20:02
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1822 |
2020/11/02 23:17:37
|
mult_n_O
|
aaaa |
Success |
|
|
| 1821 |
2020/11/02 23:08:20
|
mult_n_O
|
aaaa |
Success |
|
|
| 1820 |
2020/11/02 16:01:08
|
De Morgan's laws in Coq
|
aaaa |
Success |
|
|
| 1819 |
2020/11/02 06:29:56
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1818 |
2020/11/02 06:25:18
|
plus_comm
|
aaaa |
Success |
|
|
| 1817 |
2020/11/02 06:22:58
|
plus_comm
|
aaaa |
Success |
|
|
| 1816 |
2020/11/02 06:19:08
|
plus_comm
|
aaaa |
Success |
|
|
| 1815 |
2020/11/02 06:12:07
|
plus_comm
|
aaaa |
Success |
|
|
| 1814 |
2020/11/02 06:02:27
|
plus_assoc
|
aaaa |
Success |
|
|
| 1813 |
2020/11/02 05:58:49
|
plus_assoc
|
aaaa |
Success |
|
|
| 1812 |
2020/11/02 04:35:46
|
plus_assoc
|
aaaa |
Success |
|
|
| 1811 |
2020/11/02 04:30:00
|
plus_assoc
|
aaaa |
Success |
|
|
| 1810 |
2020/11/02 04:25:02
|
plus_assoc
|
aaaa |
Success |
|
|
| 1809 |
2020/11/02 03:50:19
|
1 + 1 = 2
|
aaaa |
Success |
|
|
| 1808 |
2020/11/02 03:48:23
|
1 + 1 = 2
|
aaaa |
Success |
|
|
| 1807 |
2020/11/02 03:45:31
|
1 + 1 = 2
|
aaaa |
Success |
|
|
| 1806 |
2020/11/02 03:43:06
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1805 |
2020/11/02 03:42:26
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1804 |
2020/11/02 03:31:38
|
1 + 1 = 2
|
sabataro |
Failure |
|
|
| 1803 |
2020/11/02 03:28:20
|
1 + 1 = 2
|
sabataro |
Failure |
|
|
| 1802 |
2020/11/02 03:26:29
|
1 + 1 = 2
|
sabataro |
Success |
|
|
| 1801 |
2020/11/02 03:23:43
|
1 + 1 = 2
|
sabataro |
Success |
|
|
| 1800 |
2020/11/02 03:20:55
|
1 + 1 = 2
|
sabataro |
Success |
|
|
| 1799 |
2020/11/02 03:17:18
|
1 + 1 = 2
|
sabataro |
Success |
|
|
| 1798 |
2020/11/02 03:12:20
|
1 + 1 = 2
|
sabataro |
Success |
|
|
| 1797 |
2020/11/02 03:01:36
|
1 + 1 = 2
|
sabataro |
Failure |
|
|
| 1796 |
2020/10/31 18:45:39
|
plus_assoc
|
xsd |
Success |
|
|
| 1795 |
2020/10/31 18:44:45
|
plus_assoc
|
xsd |
Failure |
|
|
| 1794 |
2020/10/31 14:04:47
|
plus_assoc
|
xsd |
Failure |
|
|
| 1793 |
2020/10/31 14:02:56
|
plus_assoc
|
xsd |
Failure |
|
|
| 1792 |
2020/10/26 00:43:18
|
Perfect Square?
|
fetburner |
Success |
|
|
| 1791 |
2020/10/25 03:15:22
|
If zero were not nat
|
fetburner |
Success |
|
|
| 1790 |
2020/10/25 02:58:23
|
Flat CPO
|
fetburner |
Success |
|
|
| 1789 |
2020/10/21 10:56:27
|
Eat the Candies
|
tanakh |
Success |
|
|
| 1788 |
2020/10/21 06:23:48
|
Perfect Square?
|
tanakh |
Success |
|
|
| 1787 |
2020/10/21 06:12:24
|
Perfect Square?
|
tanakh |
Success |
|
|
| 1786 |
2020/10/21 04:50:18
|
If zero were not nat
|
tanakh |
Success |
|
|
| 1785 |
2020/10/21 04:24:10
|
Flat CPO
|
tanakh |
Success |
|
|
| 1784 |
2020/10/19 08:15:36
|
The set of all finite sequences of bool is countable
|
kkob |
Success |
|
|
| 1783 |
2020/10/19 03:46:08
|
Friends and strangers
|
tanakh |
Success |
|
|
| 1782 |
2020/10/19 03:14:44
|
The set of all finite sequences of bool is countable
|
tanakh |
Success |
|
|
| 1781 |
2020/10/18 05:53:22
|
Fibonacci numbers modulo 2
|
tanakh |
Success |
|
|
| 1780 |
2020/10/17 23:29:32
|
Rotate once
|
tanakh |
Success |
|
|
| 1779 |
2020/10/17 23:27:04
|
Rotate once
|
tanakh |
Success |
|
|
| 1778 |
2020/10/17 21:17:24
|
Sum of n^3
|
tanakh |
Success |
|
|
| 1777 |
2020/10/12 04:06:50
|
forall f: bool -> bool, f^3(x) = f(x)
|
uenoku |
Success |
|
|
| 1776 |
2020/10/12 03:47:20
|
1 + 1 = 2
|
uenoku |
Success |
|
|
| 1775 |
2020/10/12 03:26:20
|
plus_assoc
|
uenoku |
Success |
|
|
| 1774 |
2020/10/12 03:20:57
|
forall l: list nat, l @ [0] <> []
|
uenoku |
Success |
|
|
| 1773 |
2020/10/12 03:20:03
|
forall l: list nat, l @ [0] <> []
|
uenoku |
Failure |
|
|
| 1772 |
2020/10/12 03:19:32
|
forall l: list nat, l @ [0] <> []
|
uenoku |
Failure |
|
|
| 1771 |
2020/10/10 14:40:30
|
Grand Garden
|
yodvhskd |
Success |
|
|
| 1770 |
2020/10/10 01:56:09
|
unique (unique l) = l
|
shift0 |
Success |
|
|
| 1769 |
2020/10/10 01:12:38
|
gcd(n, n+1) = 1
|
shift0 |
Success |
|
|
| 1768 |
2020/10/10 01:11:42
|
gcd(n, n+1) = 1
|
shift0 |
Failure |
|
|
| 1767 |
2020/10/10 01:01:48
|
Multiplication in F_2 is idempotent
|
shift0 |
Success |
|
|
| 1766 |
2020/10/09 23:38:38
|
Definitions of injectivity
|
shift0 |
Success |
|
|
| 1765 |
2020/10/09 22:56:59
|
Cumulative sum of list
|
shift0 |
Success |
|
|
| 1764 |
2020/10/09 21:25:16
|
forall l: list nat, l @ [0] <> []
|
shift0 |
Success |
|
|
| 1763 |
2020/10/09 21:24:28
|
forall l: list nat, l @ [0] <> []
|
shift0 |
Failure |
|
|
| 1762 |
2020/10/09 21:23:36
|
forall l: list nat, l @ [0] <> []
|
shift0 |
Failure |
|
|
| 1761 |
2020/10/05 22:27:03
|
unique count
|
yodvhskd |
Success |
|
|
| 1760 |
2020/09/30 19:21:22
|
Eat the Candies
|
yodvhskd |
Success |
|
|
| 1759 |
2020/09/30 09:54:31
|
Eat the Candies
|
kkob |
Success |
|
|
| 1758 |
2020/09/29 21:05:57
|
Flat CPO
|
nekodesu |
Failure |
|
|
| 1757 |
2020/09/29 20:45:08
|
Flat CPO
|
nuip |
Failure |
|
|
| 1756 |
2020/09/29 20:27:57
|
Double
|
shift0 |
Success |
|
|
| 1755 |
2020/09/29 20:27:05
|
Double
|
shift0 |
Failure |
|
|
| 1754 |
2020/09/29 20:25:42
|
Double
|
shift0 |
Failure |
|
|
| 1753 |
2020/09/29 20:24:34
|
Double
|
shift0 |
Failure |
|
|
| 1752 |
2020/09/29 19:40:43
|
Yoneda embedding for preorder
|
shift0 |
Success |
|
|
| 1751 |
2020/09/29 19:39:49
|
Yoneda embedding for preorder
|
shift0 |
Failure |
|
|
| 1750 |
2020/09/29 17:32:20
|
Sum of n^3
|
shift0 |
Success |
|
|
| 1749 |
2020/09/29 16:00:06
|
Perfect Square?
|
shift0 |
Success |
|
|
| 1748 |
2020/09/29 12:26:02
|
If zero were not nat
|
shift0 |
Success |
|
|
| 1747 |
2020/09/29 12:21:26
|
If zero were not nat
|
shift0 |
Failure |
|
|
| 1746 |
2020/09/29 12:20:27
|
If zero were not nat
|
shift0 |
Failure |
|
|
| 1745 |
2020/09/29 12:18:57
|
If zero were not nat
|
shift0 |
Failure |
|
|
| 1744 |
2020/09/29 11:37:45
|
Flat CPO
|
shift0 |
Success |
|
|
| 1743 |
2020/09/29 10:29:23
|
n < m \/ n = m \/ n > m
|
shift0 |
Success |
|
|
| 1742 |
2020/09/29 09:40:31
|
forall f: bool -> bool, f^3(x) = f(x)
|
shift0 |
Success |
|
|
| 1741 |
2020/09/28 10:11:49
|
Eat the Candies
|
kkob |
Success |
|
|
| 1740 |
2020/09/28 04:19:42
|
n * S m = n + n * m
|
shift0 |
Success |
|
|
| 1739 |
2020/09/28 03:00:58
|
1 + 1 = 2
|
shift0 |
Success |
|
|
| 1738 |
2020/09/28 02:59:45
|
plus_comm
|
shift0 |
Success |
|
|
| 1737 |
2020/09/28 02:41:25
|
plus_assoc
|
shift0 |
Success |
|
|
| 1736 |
2020/09/28 02:34:05
|
plus_assoc
|
shift0 |
Failure |
|
|
| 1735 |
2020/09/28 02:32:55
|
plus_assoc
|
shift0 |
Failure |
|
|
| 1734 |
2020/09/28 02:14:29
|
Eat the Candies
|
kik |
Success |
|
|
| 1733 |
2020/09/28 02:03:15
|
Eat the Candies
|
kik |
Success |
|
|
| 1732 |
2020/09/28 01:51:11
|
Eat the Candies
|
kik |
Success |
|
|
| 1731 |
2020/09/27 23:24:11
|
Eat the Candies
|
kik |
Success |
|
|
| 1730 |
2020/09/27 22:00:58
|
Eat the Candies
|
sorata |
Failure |
|
|
| 1729 |
2020/09/27 21:57:52
|
Eat the Candies
|
kik |
Failure |
|
|
| 1728 |
2020/09/27 21:45:17
|
Eat the Candies
|
kkob |
Success |
|
|
| 1727 |
2020/09/27 20:52:06
|
Flat CPO
|
kano |
Success |
|
|
| 1726 |
2020/09/27 20:49:26
|
If zero were not nat
|
kano |
Success |
|
|
| 1725 |
2020/09/27 20:46:56
|
Perfect Square?
|
sorata |
Success |
|
|
| 1724 |
2020/09/27 20:46:17
|
Perfect Square?
|
sorata |
Failure |
|
|
| 1723 |
2020/09/27 20:25:42
|
Perfect Square?
|
kik |
Success |
|
|
| 1722 |
2020/09/27 20:14:16
|
Perfect Square?
|
yodvhskd |
Success |
|
|
| 1721 |
2020/09/27 20:13:24
|
If zero were not nat
|
sorata |
Success |
|
|
| 1720 |
2020/09/27 20:12:24
|
Perfect Square?
|
kkob |
Success |
|
|
| 1719 |
2020/09/27 20:09:54
|
If zero were not nat
|
kik |
Success |
|
|
| 1718 |
2020/09/27 20:05:32
|
If zero were not nat
|
yodvhskd |
Success |
|
|
| 1717 |
2020/09/27 20:04:59
|
If zero were not nat
|
kkob |
Success |
|
|
| 1716 |
2020/09/27 20:04:22
|
Flat CPO
|
kik |
Success |
|
|
| 1715 |
2020/09/27 20:02:15
|
Flat CPO
|
yodvhskd |
Success |
|
|
| 1714 |
2020/09/27 20:01:56
|
Flat CPO
|
kkob |
Success |
|
|
| 1713 |
2020/09/27 20:01:18
|
Flat CPO
|
sorata |
Success |
|
|
| 1712 |
2020/09/27 13:23:44
|
Sum of n^3
|
kkob |
Success |
|
|
| 1711 |
2020/09/27 13:16:18
|
1 + 1 = 2
|
kkob |
Success |
|
|
| 1710 |
2020/09/27 13:16:02
|
1 + 1 = 2
|
kkob |
Success |
|
|
| 1709 |
2020/09/27 12:47:34
|
plus_assoc
|
kkob |
Success |
|
|
| 1708 |
2020/09/27 11:49:22
|
plus_assoc
|
kkob |
Success |
|
|
| 1707 |
2020/09/27 11:44:15
|
Friends and strangers
|
kkob |
Failure |
|
|
| 1706 |
2020/09/24 20:21:01
|
Perfect Square?
|
kozima |
Success |
|
|
| 1705 |
2020/09/24 20:19:38
|
Eat the Candies
|
kozima |
Success |
|
|
| 1704 |
2020/09/24 20:16:19
|
Perfect Square?
|
kozima |
Failure |
|
|
| 1703 |
2020/09/24 20:14:57
|
If zero were not nat
|
kozima |
Success |
|
|
| 1702 |
2020/09/24 20:13:02
|
Flat CPO
|
kozima |
Success |
|
|
| 1701 |
2020/09/22 19:05:41
|
Friends and strangers
|
fetburner |
Success |
|
|
| 1700 |
2020/09/22 18:42:31
|
The set of all finite sequences of bool is countable
|
fetburner |
Success |
|
|
| 1699 |
2020/08/18 21:33:51
|
Fibonacci numbers modulo 2
|
fetburner |
Success |
|
|
| 1698 |
2020/08/18 20:43:29
|
Rotate once
|
fetburner |
Success |
|
|
| 1697 |
2020/08/18 19:06:51
|
Sum of n^3
|
fetburner |
Success |
|
|
| 1696 |
2020/08/17 18:14:08
|
Friends and strangers (corrected)
|
kozima |
Success |
|
|
| 1695 |
2020/08/17 00:45:27
|
Friends and strangers (corrected)
|
yodvhskd |
Success |
|
|
| 1694 |
2020/08/16 23:46:03
|
Friends and strangers
|
kozima |
Success |
|
|
| 1693 |
2020/08/16 23:45:28
|
Friends and strangers
|
sorata |
Success |
|
|
| 1692 |
2020/08/16 22:36:09
|
Friends and strangers
|
kik |
Success |
|
|
| 1691 |
2020/08/16 22:03:55
|
The set of all finite sequences of bool is countable
|
kozima |
Success |
|
|
| 1690 |
2020/08/16 21:42:40
|
Rotate once
|
sorata |
Success |
|
|
| 1689 |
2020/08/16 21:27:51
|
Fibonacci numbers modulo 2
|
kik |
Success |
|
|
| 1688 |
2020/08/16 21:18:35
|
Rotate once
|
kozima |
Success |
|
|
| 1687 |
2020/08/16 20:26:26
|
Sum of n^3
|
mttm |
Success |
|
|
| 1686 |
2020/08/16 20:21:59
|
Sum of n^3
|
mttm |
Rejected |
|
|
| 1685 |
2020/08/16 20:17:04
|
Fibonacci numbers modulo 2
|
kozima |
Success |
|
|
| 1684 |
2020/08/16 20:15:44
|
Sum of n^3
|
kano |
Success |
|
|
| 1683 |
2020/08/16 20:11:15
|
Sum of n^3
|
kik |
Success |
|
|
| 1682 |
2020/08/16 20:06:17
|
Sum of n^3
|
sorata |
Success |
|
|
| 1681 |
2020/08/16 20:02:15
|
Sum of n^3
|
kozima |
Success |
|
|
| 1680 |
2020/08/15 16:38:16
|
Friends and strangers
|
yodvhskd |
Success |
|
|
| 1679 |
2020/08/15 00:35:04
|
The set of all finite sequences of bool is countable
|
yodvhskd |
Success |
|
|
| 1678 |
2020/08/09 21:56:40
|
Fibonacci numbers modulo 2
|
yodvhskd |
Success |
|
|
| 1677 |
2020/08/09 21:48:28
|
Rotate once
|
yodvhskd |
Success |
|
|
| 1676 |
2020/08/09 21:38:32
|
Sum of n^3
|
yodvhskd |
Success |
|
|
| 1675 |
2020/08/01 14:16:57
|
1 + 1 = 2
|
pandaman |
Success |
|
|
| 1674 |
2020/08/01 14:16:30
|
forall f: bool -> bool, f^3(x) = f(x)
|
pandaman |
Success |
|
|
| 1673 |
2020/08/01 14:07:07
|
1 + 1 = 2
|
pandaman |
Failure |
|
|
| 1672 |
2020/08/01 14:05:41
|
plus_comm
|
pandaman |
Success |
|
|
| 1671 |
2020/08/01 13:48:55
|
plus_assoc
|
pandaman |
Success |
|
|
| 1670 |
2020/07/20 00:32:34
|
Multiplication in F_2 is idempotent
|
mttm |
Success |
|
|
| 1669 |
2020/07/20 00:11:02
|
Definitions of injectivity
|
mttm |
Success |
|
|
| 1668 |
2020/07/19 05:51:58
|
De Morgan's laws in Coq
|
Eldora |
Failure |
|
|
| 1667 |
2020/07/19 05:50:56
|
De Morgan's laws in Coq
|
Eldora |
Rejected |
|
|
| 1666 |
2020/07/19 05:48:43
|
De Morgan's laws in Coq
|
Eldora |
Failure |
|
|
| 1665 |
2020/07/19 05:48:03
|
De Morgan's laws in Coq
|
Eldora |
Rejected |
|
|
| 1664 |
2020/07/19 05:45:09
|
and_comm (Lean)
|
Eldora |
Failure |
|
|
| 1663 |
2020/07/19 05:41:04
|
De Morgan's laws in Coq
|
Eldora |
Rejected |
|
|
| 1662 |
2020/07/19 05:02:03
|
Summand of one
|
Eldora |
Success |
|
|
| 1661 |
2020/07/19 00:51:17
|
n < m \/ n = m \/ n > m
|
Eldora |
Success |
|
|
| 1660 |
2020/07/19 00:50:48
|
n < m \/ n = m \/ n > m
|
Eldora |
Failure |
|
|
| 1659 |
2020/07/19 00:50:28
|
n < m \/ n = m \/ n > m
|
Eldora |
Failure |
|
|
| 1658 |
2020/07/16 00:54:37
|
Not a sum of squares
|
kano |
Success |
|
|
| 1657 |
2020/07/16 00:53:06
|
Not a sum of squares
|
kano |
Failure |
|
|
| 1656 |
2020/07/15 02:27:41
|
Postorder traversal
|
kano |
Success |
|
|
| 1655 |
2020/07/15 01:43:34
|
Yoneda embedding for preorder
|
kano |
Success |
|
|
| 1654 |
2020/07/05 03:35:20
|
infinite bool sequence is uncountable
|
kano |
Success |
|
|
| 1653 |
2020/07/05 02:16:57
|
Boolean-hole principle revisited
|
kano |
Success |
|
|
| 1652 |
2020/07/04 19:29:05
|
Double
|
kano |
Success |
|
|
| 1651 |
2020/07/04 18:20:54
|
Tree addressing is injective
|
kano |
Success |
|
|
| 1650 |
2020/07/04 18:20:08
|
Tree addressing is injective
|
kano |
Failure |
|
|
| 1649 |
2020/07/04 16:43:45
|
Any natural number is expressible in binary notation
|
kano |
Success |
|
|
| 1648 |
2020/07/04 16:43:09
|
Any natural number is expressible in binary notation
|
kano |
Failure |
|
|
| 1647 |
2020/07/04 14:53:09
|
Two is not Three
|
kano |
Success |
|
|
| 1646 |
2020/07/04 04:40:45
|
Infinite duplication
|
kkob |
Success |
|
|
| 1645 |
2020/07/03 23:08:30
|
unique count
|
kano |
Success |
|
|
| 1644 |
2020/07/02 22:49:59
|
unique (unique l) = l
|
kano |
Success |
|
|
| 1643 |
2020/07/01 21:56:07
|
Multiplication in F_2 is idempotent
|
kano |
Success |
|
|
| 1642 |
2020/07/01 21:55:44
|
Multiplication in F_2 is idempotent
|
kano |
Failure |
|
|
| 1641 |
2020/07/01 02:03:34
|
Definitions of injectivity
|
kano |
Success |
|
|
| 1640 |
2020/07/01 02:00:25
|
Definitions of injectivity
|
kano |
Failure |
|
|
| 1639 |
2020/06/30 01:54:04
|
Tree Syntax Unambiguity
|
kkob |
Success |
|
|
| 1638 |
2020/06/30 01:51:34
|
Tree Syntax Unambiguity
|
kkob |
Failure |
|
|
| 1637 |
2020/06/30 01:49:56
|
Tree Syntax Unambiguity
|
kkob |
Failure |
|
|
| 1636 |
2020/06/28 16:21:36
|
Cumulative sum of list
|
kano |
Success |
|
|
| 1635 |
2020/06/26 19:49:27
|
count l n = count (rev l) n
|
kano |
Success |
|
|
| 1634 |
2020/06/26 19:47:19
|
count l n = count (rev l) n
|
kano |
Failure |
|
|
| 1633 |
2020/06/26 15:56:14
|
Upper triangular (completeness)
|
kano |
Success |
|
|
| 1632 |
2020/06/25 05:52:23
|
n < m \/ n = m \/ n > m
|
dareka |
Failure |
|
|
| 1631 |
2020/06/23 23:23:24
|
Upper triangular (soundness)
|
kano |
Success |
|
|
| 1630 |
2020/06/23 16:49:13
|
Drinker paradox?
|
kano |
Success |
|
|
| 1629 |
2020/06/23 16:10:38
|
n < m \/ n = m \/ n > m
|
kano |
Success |
|
|
| 1628 |
2020/06/23 16:09:44
|
n < m \/ n = m \/ n > m
|
kano |
Failure |
|
|
| 1627 |
2020/06/20 00:00:53
|
Midpoint
|
kano |
Success |
|
|
| 1626 |
2020/06/19 22:43:22
|
Zero test
|
kano |
Success |
|
|
| 1625 |
2020/06/19 21:53:32
|
Tree Syntax Unambiguity
|
fetburner |
Success |
|
|
| 1624 |
2020/06/19 20:14:26
|
Constructor is injective
|
kano |
Success |
|
|
| 1623 |
2020/06/19 20:10:48
|
Constructor is injective
|
kano |
Failure |
|
|
| 1622 |
2020/06/19 20:01:48
|
Three is prime
|
kano |
Success |
|
|
| 1621 |
2020/06/19 19:48:34
|
Three is prime
|
kano |
Success |
|
|
| 1620 |
2020/06/19 19:17:16
|
Tree Induction
|
fetburner |
Success |
|
|
| 1619 |
2020/06/19 19:09:18
|
count_occ_app
|
fetburner |
Success |
|
|
| 1618 |
2020/06/19 19:05:33
|
S preserves comparison
|
fetburner |
Success |
|
|
| 1617 |
2020/06/19 18:58:19
|
Infinite duplication
|
fetburner |
Success |
|
|
| 1616 |
2020/06/17 22:53:49
|
n < m \/ n = m \/ n > m
|
ry3s |
Success |
|
|
| 1615 |
2020/06/17 21:58:51
|
Summand of one
|
mttm |
Success |
|
|
| 1614 |
2020/06/17 01:30:07
|
Cumulative sum of list
|
mttm |
Success |
|
|
| 1613 |
2020/06/16 20:11:50
|
n * S m = n + n * m
|
algon |
Success |
|
|
| 1612 |
2020/06/16 19:15:18
|
forall f: bool -> bool, f^3(x) = f(x)
|
algon |
Success |
|
|
| 1611 |
2020/06/16 18:25:36
|
1 + 1 = 2
|
algon |
Success |
|
|
| 1610 |
2020/06/16 18:19:06
|
plus_comm
|
algon |
Success |
|
|
| 1609 |
2020/06/16 17:47:42
|
plus_assoc
|
algon |
Success |
|
|
| 1608 |
2020/06/15 20:22:41
|
forall l: list nat, l @ [0] <> []
|
Eldora |
Success |
|
|
| 1607 |
2020/06/15 19:06:03
|
S preserves comparison
|
Eldora |
Failure |
|
|
| 1606 |
2020/06/15 19:05:15
|
S preserves comparison
|
Eldora |
Success |
|
|
| 1605 |
2020/06/15 19:04:46
|
S preserves comparison
|
Eldora |
Failure |
|
|
| 1604 |
2020/06/15 17:09:18
|
plus_assoc
|
peroxyacyl |
Success |
|
|
| 1603 |
2020/06/15 03:02:55
|
1 + 1 = 2
|
yamaNote |
Success |
|
|
| 1602 |
2020/06/15 03:00:26
|
plus_comm
|
yamaNote |
Success |
|
|
| 1601 |
2020/06/15 02:54:05
|
plus_assoc
|
yamaNote |
Success |
|
|
| 1600 |
2020/06/15 02:42:43
|
plus_assoc
|
yamaNote |
Success |
|
|
| 1599 |
2020/06/15 02:27:45
|
plus_assoc
|
yamaNote |
Failure |
|
|
| 1598 |
2020/06/14 22:34:39
|
Tree Syntax Unambiguity
|
kozima |
Success |
|
|
| 1597 |
2020/06/14 22:24:33
|
Tree Syntax Unambiguity
|
yodvhskd |
Success |
|
|
| 1596 |
2020/06/14 21:33:55
|
Tree Induction
|
kik |
Rejected |
|
|
| 1595 |
2020/06/14 21:21:11
|
count_occ_app
|
mttm |
Success |
|
|
| 1594 |
2020/06/14 21:16:30
|
S preserves comparison
|
mttm |
Success |
|
|
| 1593 |
2020/06/14 21:03:53
|
Tree Syntax Unambiguity
|
yodvhskd |
Success |
|
|
| 1592 |
2020/06/14 20:41:03
|
Tree Induction
|
efk |
Success |
|
|
| 1591 |
2020/06/14 20:11:44
|
Tree Induction
|
tanakh |
Success |
|
|
| 1590 |
2020/06/14 20:10:36
|
Tree Induction
|
tanakh |
Failure |
|
|
| 1589 |
2020/06/14 20:05:38
|
count_occ_app
|
kano |
Success |
|
|
| 1588 |
2020/06/14 19:47:10
|
count_occ_app
|
efk |
Success |
|
|
| 1587 |
2020/06/14 19:36:48
|
Tree Induction
|
sorata |
Success |
|
|
| 1586 |
2020/06/14 19:25:29
|
Tree Induction
|
yodvhskd |
Success |
|
|
| 1585 |
2020/06/14 19:21:38
|
count_occ_app
|
natsugiri |
Success |
|
|
| 1584 |
2020/06/14 19:21:37
|
S preserves comparison
|
efk |
Success |
|
|
| 1583 |
2020/06/14 19:18:13
|
Tree Induction
|
kozima |
Success |
|
|
| 1582 |
2020/06/14 19:15:31
|
count_occ_app
|
tanakh |
Success |
|
|
| 1581 |
2020/06/14 19:15:10
|
count_occ_app
|
kik |
Success |
|
|
| 1580 |
2020/06/14 19:09:23
|
count_occ_app
|
kozima |
Success |
|
|
| 1579 |
2020/06/14 19:07:49
|
S preserves comparison
|
kik |
Success |
|
|
| 1578 |
2020/06/14 19:06:38
|
count_occ_app
|
yodvhskd |
Success |
|
|
| 1577 |
2020/06/14 19:05:53
|
count_occ_app
|
sorata |
Success |
|
|
| 1576 |
2020/06/14 19:05:47
|
S preserves comparison
|
tanakh |
Success |
|
|
| 1575 |
2020/06/14 19:05:15
|
S preserves comparison
|
natsugiri |
Success |
|
|
| 1574 |
2020/06/14 19:04:13
|
S preserves comparison
|
natsugiri |
Failure |
|
|
| 1573 |
2020/06/14 19:03:58
|
S preserves comparison
|
kano |
Success |
|
|
| 1572 |
2020/06/14 19:03:48
|
S preserves comparison
|
yodvhskd |
Success |
|
|
| 1571 |
2020/06/14 19:02:11
|
S preserves comparison
|
kozima |
Success |
|
|
| 1570 |
2020/06/14 19:01:35
|
S preserves comparison
|
sorata |
Success |
|
|
| 1569 |
2020/06/14 18:55:43
|
Boolean-hole principle
|
kano |
Success |
|
|
| 1568 |
2020/06/13 15:34:20
|
Tree Induction
|
kkob |
Success |
|
|
| 1567 |
2020/06/13 15:29:21
|
Tree Induction
|
kkob |
Success |
|
|
| 1566 |
2020/06/11 17:29:01
|
S preserves comparison
|
kkob |
Success |
|
|
| 1565 |
2020/06/09 20:09:15
|
n < m \/ n = m \/ n > m
|
hammer |
Success |
|
|
| 1564 |
2020/06/09 18:33:49
|
n * S m = n + n * m
|
hammer |
Success |
|
|
| 1563 |
2020/06/09 18:11:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
hammer |
Success |
|
|
| 1562 |
2020/06/09 17:33:07
|
1 + 1 = 2
|
hammer |
Success |
|
|
| 1561 |
2020/06/09 17:31:47
|
plus_comm
|
hammer |
Success |
|
|
| 1560 |
2020/06/09 17:01:10
|
plus_assoc
|
hammer |
Success |
|
|
| 1559 |
2020/06/09 16:58:24
|
plus_assoc
|
hammer |
Failure |
|
|
| 1558 |
2020/06/08 00:38:06
|
count_occ_app
|
kkob |
Success |
|
|
| 1557 |
2020/06/08 00:37:28
|
Tree Syntax Unambiguity
|
kkob |
Success |
|
|
| 1556 |
2020/06/08 00:17:20
|
Tree Induction
|
kkob |
Success |
|
|
| 1555 |
2020/06/04 01:33:54
|
De Morgan's laws in Coq
|
kano |
Success |
|
|
| 1554 |
2020/06/04 00:43:28
|
gcd(n, n+1) = 1
|
kano |
Success |
|
|
| 1553 |
2020/06/04 00:32:25
|
gcd(n, n+1) = 1
|
kano |
Failure |
|
|
| 1552 |
2020/06/04 00:20:54
|
forall l: list nat, l @ [0] <> []
|
kano |
Success |
|
|
| 1551 |
2020/06/04 00:15:54
|
Summand of one
|
kano |
Success |
|
|
| 1550 |
2020/05/28 10:38:02
|
1 + 1 = 2
|
Tqk |
Success |
|
|
| 1549 |
2020/05/21 20:39:56
|
Yoneda embedding for preorder
|
efk |
Success |
|
|
| 1548 |
2020/05/21 20:08:57
|
Swap twice
|
kkob |
Rejected |
|
|
| 1547 |
2020/05/21 19:33:02
|
Boolean-hole principle
|
efk |
Success |
|
|
| 1546 |
2020/05/20 20:26:35
|
plus_assoc
|
aaa |
Success |
|
|
| 1545 |
2020/05/20 20:26:01
|
plus_assoc
|
aaa |
Failure |
|
|
| 1544 |
2020/05/20 13:36:38
|
Boolean-hole principle
|
cympfh |
Success |
|
|
| 1543 |
2020/05/13 02:21:51
|
eq_sym?
|
cympfh |
Success |
|
|
| 1542 |
2020/05/10 19:34:47
|
eq_sym?
|
kano |
Success |
|
|
| 1541 |
2020/05/10 19:23:22
|
mult_n_O
|
kano |
Success |
|
|
| 1540 |
2020/05/10 19:20:34
|
n * S m = n + n * m
|
kano |
Success |
|
|
| 1539 |
2020/05/10 18:51:45
|
forall f: bool -> bool, f^3(x) = f(x)
|
kano |
Success |
|
|
| 1538 |
2020/05/10 18:40:39
|
1 + 1 = 2
|
kano |
Success |
|
|
| 1537 |
2020/05/10 18:39:40
|
plus_comm
|
kano |
Success |
|
|
| 1536 |
2020/05/08 23:40:34
|
Infinite duplication
|
tzik |
Success |
|
|
| 1535 |
2020/05/08 19:29:47
|
Swap twice
|
cympfh |
Success |
|
|
| 1534 |
2020/05/08 19:29:11
|
Swap twice
|
cympfh |
Failure |
|
|
| 1533 |
2020/05/05 05:39:20
|
Cycle detection
|
aaa |
Success |
|
|
| 1532 |
2020/05/05 05:37:43
|
Cycle detection
|
aaa |
Failure |
|
|
| 1531 |
2020/05/05 02:23:06
|
Equivalent two quicksorts
|
yodvhskd |
Success |
|
|
| 1530 |
2020/05/05 02:18:06
|
Equivalent two quicksorts
|
yodvhskd |
Failure |
|
|
| 1529 |
2020/05/03 23:50:39
|
Upper triangular (soundness)
|
mttm |
Success |
|
|
| 1528 |
2020/05/03 23:39:22
|
Drinker paradox?
|
mttm |
Success |
|
|
| 1527 |
2020/05/03 21:51:34
|
Infinite duplication
|
kik |
Success |
|
|
| 1526 |
2020/05/03 21:49:17
|
Upper triangular (completeness)
|
natsugiri |
Success |
|
|
| 1525 |
2020/05/03 21:43:42
|
Infinite duplication
|
yodvhskd |
Success |
|
|
| 1524 |
2020/05/03 21:42:51
|
Infinite duplication
|
hirosegolf |
Failure |
|
|
| 1523 |
2020/05/03 21:02:03
|
Upper triangular (completeness)
|
tzik |
Success |
|
|
| 1522 |
2020/05/03 20:54:52
|
Upper triangular (completeness)
|
hirosegolf |
Success |
|
|
| 1521 |
2020/05/03 20:54:27
|
Upper triangular (soundness)
|
hirosegolf |
Failure |
|
|
| 1520 |
2020/05/03 20:41:38
|
Upper triangular (completeness)
|
kik |
Success |
|
|
| 1519 |
2020/05/03 20:41:08
|
Drinker paradox?
|
tzik |
Success |
|
|
| 1518 |
2020/05/03 20:32:54
|
Upper triangular (soundness)
|
hirosegolf |
Success |
|
|
| 1517 |
2020/05/03 20:32:43
|
Upper triangular (completeness)
|
tanakh |
Success |
|
|
| 1516 |
2020/05/03 20:31:11
|
Upper triangular (completeness)
|
yodvhskd |
Success |
|
|
| 1515 |
2020/05/03 20:26:22
|
Upper triangular (soundness)
|
natsugiri |
Success |
|
|
| 1514 |
2020/05/03 20:26:13
|
Drinker paradox?
|
hirosegolf |
Success |
|
|
| 1513 |
2020/05/03 20:22:53
|
Upper triangular (soundness)
|
yodvhskd |
Success |
|
|
| 1512 |
2020/05/03 20:21:57
|
Upper triangular (soundness)
|
kik |
Success |
|
|
| 1511 |
2020/05/03 20:20:25
|
Upper triangular (completeness)
|
fetburner |
Success |
|
|
| 1510 |
2020/05/03 20:19:57
|
Drinker paradox?
|
natsugiri |
Success |
|
|
| 1509 |
2020/05/03 20:17:30
|
Drinker paradox?
|
yodvhskd |
Success |
|
|
| 1508 |
2020/05/03 20:11:01
|
Upper triangular (soundness)
|
tzik |
Success |
|
|
| 1507 |
2020/05/03 20:08:44
|
Upper triangular (soundness)
|
fetburner |
Success |
|
|
| 1506 |
2020/05/03 20:08:43
|
Upper triangular (soundness)
|
tanakh |
Success |
|
|
| 1505 |
2020/05/03 20:06:25
|
Drinker paradox?
|
fetburner |
Success |
|
|
| 1504 |
2020/05/03 20:06:18
|
Swap twice
|
hirosegolf |
Success |
|
|
| 1503 |
2020/05/03 20:05:43
|
Drinker paradox?
|
tanakh |
Success |
|
|
| 1502 |
2020/05/03 20:05:33
|
Drinker paradox?
|
kik |
Success |
|
|
| 1501 |
2020/05/03 20:04:35
|
Swap twice
|
natsugiri |
Success |
|
|
| 1500 |
2020/05/03 20:04:34
|
Swap twice
|
tzik |
Success |
|
|
| 1499 |
2020/05/03 20:03:08
|
Swap twice
|
kano |
Success |
|
|
| 1498 |
2020/05/03 20:02:01
|
Swap twice
|
mttm |
Success |
|
|
| 1497 |
2020/05/03 20:01:42
|
Swap twice
|
kik |
Success |
|
|
| 1496 |
2020/05/03 20:01:36
|
Swap twice
|
fetburner |
Success |
|
|
| 1495 |
2020/05/03 20:01:00
|
Swap twice
|
yodvhskd |
Success |
|
|
| 1494 |
2020/05/03 20:00:59
|
Swap twice
|
tanakh |
Success |
|
|
| 1493 |
2020/05/03 19:50:49
|
Not a sum of squares
|
fetburner |
Success |
|
|
| 1492 |
2020/05/03 19:20:24
|
plus_assoc
|
kano |
Success |
|
|
| 1491 |
2020/05/03 14:51:10
|
Infinite duplication
|
kozima |
Success |
|
|
| 1490 |
2020/05/03 14:50:41
|
Upper triangular (completeness)
|
kozima |
Success |
|
|
| 1489 |
2020/05/01 04:37:17
|
Cycle detection
|
kaz |
Failure |
|
|
| 1488 |
2020/05/01 04:31:29
|
Cycle detection
|
kaz |
Failure |
|
|
| 1487 |
2020/04/29 12:12:49
|
Drinker paradox?
|
kozima |
Success |
|
|
| 1486 |
2020/04/29 12:12:30
|
Upper triangular (soundness)
|
kozima |
Success |
|
|
| 1485 |
2020/04/29 12:12:12
|
Upper triangular (completeness)
|
kozima |
Failure |
|
|
| 1484 |
2020/04/29 12:11:50
|
Infinite duplication
|
kozima |
Failure |
|
|
| 1483 |
2020/04/29 12:11:28
|
Swap twice
|
kozima |
Success |
|
|
| 1482 |
2020/04/26 22:55:33
|
1 + 1 = 2
|
gaxiiiiiiiiiiii |
Success |
|
|
| 1481 |
2020/04/26 22:53:49
|
plus_comm
|
gaxiiiiiiiiiiii |
Success |
|
|
| 1480 |
2020/04/26 22:43:48
|
plus_assoc
|
gaxiiiiiiiiiiii |
Success |
|
|
| 1479 |
2020/04/17 14:12:53
|
n * S m = n + n * m
|
Eldora |
Success |
|
|
| 1478 |
2020/04/16 18:38:41
|
and_comm (Lean)
|
yodvhskd |
Success |
|
|
| 1477 |
2020/03/31 17:24:14
|
Binary search
|
tanakh |
Success |
|
|
| 1476 |
2020/03/31 05:56:11
|
l1 <> l2 if l2 is an odd permutation of l1
|
tanakh |
Success |
|
|
| 1475 |
2020/03/28 01:18:40
|
Equivalent two quicksorts
|
tanakh |
Success |
|
|
| 1474 |
2020/03/28 01:17:19
|
Equivalent two quicksorts
|
tanakh |
Failure |
|
|
| 1473 |
2020/03/21 12:56:49
|
1 + 1 = 2
|
smizoe |
Success |
|
|
| 1472 |
2020/03/21 12:55:40
|
1 + 1 = 2
|
smizoe |
Failure |
|
|
| 1471 |
2020/03/21 12:53:27
|
1 + 1 = 2
|
smizoe |
Failure |
|
|
| 1470 |
2020/03/19 00:03:22
|
n < m \/ n = m \/ n > m
|
shimomire |
Success |
|
|
| 1469 |
2020/03/18 23:58:52
|
n * S m = n + n * m
|
shimomire |
Success |
|
|
| 1468 |
2020/03/18 22:10:28
|
forall f: bool -> bool, f^3(x) = f(x)
|
shimomire |
Success |
|
|
| 1467 |
2020/03/18 21:47:20
|
forall f: bool -> bool, f^3(x) = f(x)
|
shimomire |
Success |
|
|
| 1466 |
2020/03/18 21:19:41
|
1 + 1 = 2
|
shimomire |
Success |
|
|
| 1465 |
2020/03/18 21:17:41
|
plus_comm
|
shimomire |
Success |
|
|
| 1464 |
2020/03/18 21:03:12
|
plus_assoc
|
shimomire |
Success |
|
|
| 1463 |
2020/03/18 08:07:24
|
Sum of binomial coefficients
|
tanakh |
Success |
|
|
| 1462 |
2020/03/18 08:02:32
|
Sum of binomial coefficients
|
tanakh |
Rejected |
|
|
| 1461 |
2020/03/18 00:20:45
|
Iterated iteration
|
tanakh |
Success |
|
|
| 1460 |
2020/03/18 00:17:37
|
Iterated iteration
|
tanakh |
Success |
|
|
| 1459 |
2020/03/18 00:16:37
|
Iterated iteration
|
tanakh |
Failure |
|
|
| 1458 |
2020/03/17 23:26:23
|
Iterated iteration
|
tanakh |
Rejected |
|
|
| 1457 |
2020/03/17 17:20:57
|
eq_sym?
|
a_kawashiro |
Failure |
|
|
| 1456 |
2020/03/17 17:19:41
|
eq_sym?
|
a_kawashiro |
Failure |
|
|
| 1455 |
2020/03/17 16:32:12
|
De Morgan's laws in Coq
|
zer0star |
Success |
|
|
| 1454 |
2020/03/17 16:10:46
|
mult_n_O
|
zer0star |
Success |
|
|
| 1453 |
2020/03/17 15:59:12
|
Multiplication in F_2 is idempotent
|
zer0star |
Success |
|
|
| 1452 |
2020/03/17 15:07:58
|
Definitions of injectivity
|
zer0star |
Success |
|
|
| 1451 |
2020/03/16 09:25:30
|
Postorder traversal
|
tzik |
Success |
|
|
| 1450 |
2020/03/16 09:25:06
|
Not a sum of squares
|
tzik |
Success |
|
|
| 1449 |
2020/03/16 09:24:47
|
eq_sym?
|
tzik |
Success |
|
|
| 1448 |
2020/03/16 07:48:16
|
Cycle detection
|
tzik |
Success |
|
|
| 1447 |
2020/03/16 02:55:12
|
Cycle detection
|
yodvhskd |
Success |
|
|
| 1446 |
2020/03/16 01:04:29
|
Postorder traversal
|
tanakh |
Success |
|
|
| 1445 |
2020/03/15 23:52:52
|
Cumulative sum of list
|
zer0star |
Success |
|
|
| 1444 |
2020/03/15 23:51:17
|
Cumulative sum of list
|
zer0star |
Failure |
|
|
| 1443 |
2020/03/15 23:48:12
|
Cumulative sum of list
|
zer0star |
Failure |
|
|
| 1442 |
2020/03/15 23:09:42
|
forall l: list nat, l @ [0] <> []
|
zer0star |
Success |
|
|
| 1441 |
2020/03/15 22:57:09
|
Cycle detection
|
kkob |
Success |
|
|
| 1440 |
2020/03/15 22:54:37
|
Cycle detection
|
fetburner |
Success |
|
|
| 1439 |
2020/03/15 22:54:36
|
n < m \/ n = m \/ n > m
|
zer0star |
Success |
|
|
| 1438 |
2020/03/15 22:50:54
|
n * S m = n + n * m
|
zer0star |
Success |
|
|
| 1437 |
2020/03/15 22:47:54
|
forall f: bool -> bool, f^3(x) = f(x)
|
zer0star |
Success |
|
|
| 1436 |
2020/03/15 22:43:09
|
and_comm (Lean)
|
tanakh |
Success |
|
|
| 1435 |
2020/03/15 22:39:38
|
1 + 1 = 2
|
KisaragiEffective |
Success |
|
|
| 1434 |
2020/03/15 22:36:28
|
Cycle detection
|
kkob |
Success |
|
|
| 1433 |
2020/03/15 22:28:01
|
and_comm (Lean)
|
tanakh |
Success |
|
|
| 1432 |
2020/03/15 22:13:34
|
1 + 1 = 2
|
zer0star |
Success |
|
|
| 1431 |
2020/03/15 22:08:35
|
Not a sum of squares
|
kimiyuki |
Success |
|
|
| 1430 |
2020/03/15 21:57:38
|
Not a sum of squares
|
tanakh |
Success |
|
|
| 1429 |
2020/03/15 21:57:28
|
Not a sum of squares
|
kimiyuki |
Success |
|
|
| 1428 |
2020/03/15 21:30:44
|
Postorder traversal
|
kik |
Success |
|
|
| 1427 |
2020/03/15 21:25:10
|
Cycle detection
|
kaz |
Success |
|
|
| 1426 |
2020/03/15 21:16:50
|
Postorder traversal
|
natsugiri |
Success |
|
|
| 1425 |
2020/03/15 21:14:51
|
Postorder traversal
|
yamarten |
Success |
|
|
| 1424 |
2020/03/15 21:11:56
|
Not a sum of squares
|
tzik |
Success |
|
|
| 1423 |
2020/03/15 21:06:54
|
Postorder traversal
|
kimiyuki |
Success |
|
|
| 1422 |
2020/03/15 21:05:31
|
Not a sum of squares
|
kik |
Success |
|
|
| 1421 |
2020/03/15 20:57:09
|
eq_sym?
|
mttm |
Success |
|
|
| 1420 |
2020/03/15 20:52:49
|
eq_sym?
|
natsugiri |
Success |
|
|
| 1419 |
2020/03/15 20:46:23
|
Postorder traversal
|
tzik |
Success |
|
|
| 1418 |
2020/03/15 20:42:52
|
Postorder traversal
|
yodvhskd |
Success |
|
|
| 1417 |
2020/03/15 20:41:50
|
Postorder traversal
|
sorata |
Success |
|
|
| 1416 |
2020/03/15 20:35:39
|
Not a sum of squares
|
yodvhskd |
Success |
|
|
| 1415 |
2020/03/15 20:29:20
|
Not a sum of squares
|
sorata |
Success |
|
|
| 1414 |
2020/03/15 20:28:38
|
Postorder traversal
|
kkob |
Success |
|
|
| 1413 |
2020/03/15 20:28:17
|
Postorder traversal
|
sorata |
Failure |
|
|
| 1412 |
2020/03/15 20:22:59
|
Not a sum of squares
|
kkob |
Success |
|
|
| 1411 |
2020/03/15 20:18:13
|
Postorder traversal
|
kaz |
Success |
|
|
| 1410 |
2020/03/15 20:13:52
|
Postorder traversal
|
fetburner |
Success |
|
|
| 1409 |
2020/03/15 20:13:01
|
Not a sum of squares
|
kaz |
Success |
|
|
| 1408 |
2020/03/15 20:12:07
|
eq_sym?
|
kik |
Success |
|
|
| 1407 |
2020/03/15 20:05:23
|
eq_sym?
|
tanakh |
Success |
|
|
| 1406 |
2020/03/15 20:04:11
|
eq_sym?
|
prime |
Success |
|
|
| 1405 |
2020/03/15 20:04:02
|
eq_sym?
|
kimiyuki |
Success |
|
|
| 1404 |
2020/03/15 20:03:50
|
eq_sym?
|
sorata |
Success |
|
|
| 1403 |
2020/03/15 20:03:45
|
eq_sym?
|
tzik |
Success |
|
|
| 1402 |
2020/03/15 20:03:16
|
eq_sym?
|
fetburner |
Success |
|
|
| 1401 |
2020/03/15 20:02:44
|
eq_sym?
|
yamarten |
Success |
|
|
| 1400 |
2020/03/15 20:01:34
|
eq_sym?
|
kkob |
Success |
|
|
| 1399 |
2020/03/15 20:01:02
|
eq_sym?
|
yodvhskd |
Success |
|
|
| 1398 |
2020/03/15 20:01:00
|
eq_sym?
|
kaz |
Success |
|
|
| 1397 |
2020/03/15 19:47:54
|
Zero test
|
yodvhskd |
Success |
|
|
| 1396 |
2020/03/15 19:20:09
|
Three is prime
|
prime |
Failure |
|
|
| 1395 |
2020/03/15 18:42:47
|
Boolean-hole principle
|
prime |
Success |
|
|
| 1394 |
2020/03/12 20:05:52
|
mult_n_O
|
nekodesu |
Failure |
|
|
| 1393 |
2020/03/12 19:55:51
|
gcd(n, n+1) = 1
|
nekodesu |
Failure |
|
|
| 1392 |
2020/03/10 19:46:44
|
Cycle detection
|
kozima |
Success |
|
|
| 1391 |
2020/03/10 19:46:08
|
Postorder traversal
|
kozima |
Success |
|
|
| 1390 |
2020/03/10 19:45:06
|
Not a sum of squares
|
kozima |
Success |
|
|
| 1389 |
2020/03/10 19:44:14
|
eq_sym?
|
kozima |
Success |
|
|
| 1388 |
2020/03/05 19:00:38
|
and_comm (Lean)
|
ukikagi |
Success |
|
|
| 1387 |
2020/02/26 14:48:34
|
n < m \/ n = m \/ n > m
|
yishibashi |
Success |
|
|
| 1386 |
2020/02/25 17:50:45
|
Zero test
|
proofninja |
Failure |
|
|
| 1385 |
2020/02/24 03:44:57
|
Zero test
|
chir |
Success |
|
|
| 1384 |
2020/02/24 03:01:08
|
n < m \/ n = m \/ n > m
|
chir |
Success |
|
|
| 1383 |
2020/02/24 02:45:21
|
n * S m = n + n * m
|
chir |
Success |
|
|
| 1382 |
2020/02/24 02:21:42
|
forall f: bool -> bool, f^3(x) = f(x)
|
chir |
Success |
|
|
| 1381 |
2020/02/24 02:10:16
|
1 + 1 = 2
|
chir |
Success |
|
|
| 1380 |
2020/02/20 08:11:11
|
n < m \/ n = m \/ n > m
|
emoken |
Success |
|
|
| 1379 |
2020/02/18 12:27:11
|
n * S m = n + n * m
|
emoken |
Success |
|
|
| 1378 |
2020/02/18 12:21:58
|
forall f: bool -> bool, f^3(x) = f(x)
|
emoken |
Success |
|
|
| 1377 |
2020/02/18 12:11:50
|
1 + 1 = 2
|
emoken |
Success |
|
|
| 1376 |
2020/02/18 12:07:53
|
plus_comm
|
emoken |
Success |
|
|
| 1375 |
2020/02/18 12:00:19
|
plus_comm
|
emoken |
Success |
|
|
| 1374 |
2020/02/18 11:53:06
|
plus_assoc
|
emoken |
Success |
|
|
| 1373 |
2020/02/13 19:01:51
|
and_comm (Lean)
|
na4zagin3 |
Success |
|
|
| 1372 |
2020/02/13 18:38:32
|
and_comm (Lean)
|
blue_jam |
Success |
|
|
| 1371 |
2020/02/08 07:20:41
|
and_comm (Lean)
|
tzik |
Success |
|
|
| 1370 |
2020/02/07 14:55:59
|
forall l: list nat, l @ [0] <> []
|
mttm |
Success |
|
|
| 1369 |
2020/02/07 14:42:57
|
Product of n consecutive integers is divisible by n!
|
mttm |
Success |
|
|
| 1368 |
2020/02/06 19:07:17
|
gcd(n, n+1) = 1
|
nekodesu |
Failure |
|
|
| 1367 |
2020/02/05 13:46:12
|
n < m \/ n = m \/ n > m
|
mttm |
Success |
|
|
| 1366 |
2020/02/05 08:19:22
|
and_comm (Lean)
|
nekodesu |
Success |
|
|
| 1365 |
2020/02/05 04:09:02
|
and_comm (Lean)
|
nuip |
Failure |
|
|
| 1364 |
2020/02/05 04:07:26
|
and_comm (Lean)
|
nuip |
Success |
|
|
| 1363 |
2020/02/05 04:06:47
|
and_comm (Lean)
|
nuip |
Failure |
|
|
| 1362 |
2020/02/05 03:15:54
|
and_comm (Lean)
|
asi1024 |
Success |
|
|
| 1361 |
2020/02/05 00:36:18
|
and_comm (Lean)
|
asi1024 |
Failure |
|
|
| 1360 |
2020/02/01 00:25:23
|
Boolean-hole principle
|
na4zagin3 |
Success |
|
|
| 1359 |
2020/02/01 00:25:22
|
De Morgan's laws in Coq
|
na4zagin3 |
Success |
|
|
| 1358 |
2020/02/01 00:25:20
|
mult_n_O
|
na4zagin3 |
Success |
|
|
| 1357 |
2020/02/01 00:25:19
|
gcd(n, n+1) = 1
|
na4zagin3 |
Success |
|
|
| 1356 |
2020/02/01 00:25:18
|
Summand of one
|
na4zagin3 |
Success |
|
|
| 1355 |
2020/02/01 00:25:16
|
forall l: list nat, l @ [0] <> []
|
na4zagin3 |
Success |
|
|
| 1354 |
2020/01/31 23:54:12
|
n * S m = n + n * m
|
na4zagin3 |
Success |
|
|
| 1353 |
2020/01/31 23:54:10
|
forall f: bool -> bool, f^3(x) = f(x)
|
na4zagin3 |
Success |
|
|
| 1352 |
2020/01/31 23:54:08
|
1 + 1 = 2
|
na4zagin3 |
Success |
|
|
| 1351 |
2020/01/31 23:54:05
|
plus_comm
|
na4zagin3 |
Success |
|
|
| 1350 |
2020/01/31 23:27:47
|
plus_assoc
|
na4zagin3 |
Success |
|
|
| 1349 |
2020/01/30 20:15:04
|
Summand of one
|
nekodesu |
Failure |
|
|
| 1348 |
2020/01/30 19:54:36
|
n < m \/ n = m \/ n > m
|
nekodesu |
Failure |
|
|
| 1347 |
2020/01/24 14:17:34
|
mult_n_O
|
Eldora |
Success |
|
|
| 1346 |
2020/01/24 14:11:34
|
Boolean-hole principle
|
Eldora |
Success |
|
|
| 1345 |
2020/01/23 20:14:48
|
n < m \/ n = m \/ n > m
|
nuip |
Failure |
|
|
| 1344 |
2020/01/23 20:12:40
|
n < m \/ n = m \/ n > m
|
nuip |
Failure |
|
|
| 1343 |
2020/01/23 19:42:11
|
n < m \/ n = m \/ n > m
|
blue_jam |
Failure |
|
|
| 1342 |
2020/01/20 15:23:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
Eldora |
Success |
|
|
| 1341 |
2020/01/20 15:08:24
|
forall f: bool -> bool, f^3(x) = f(x)
|
Eldora |
Success |
|
|
| 1340 |
2020/01/20 14:15:29
|
plus_comm
|
Eldora |
Success |
|
|
| 1339 |
2020/01/20 13:29:41
|
plus_assoc
|
Eldora |
Success |
|
|
| 1338 |
2020/01/16 20:41:29
|
Any natural number is expressible in binary notation
|
na4zagin3 |
Failure |
|
|
| 1337 |
2020/01/16 20:37:44
|
Any natural number is expressible in binary notation
|
nuip |
Failure |
|
|
| 1336 |
2020/01/16 20:37:35
|
Multiplication of non-zero value in F_p is injective
|
nuip |
Failure |
|
|
| 1335 |
2020/01/16 20:31:40
|
Any natural number is expressible in binary notation
|
blue_jam |
Failure |
|
|
| 1334 |
2020/01/16 20:06:35
|
Any natural number is expressible in binary notation
|
nekodesu |
Failure |
|
|
| 1333 |
2020/01/13 14:38:15
|
Three is prime
|
kurgm |
Success |
|
|
| 1332 |
2020/01/13 12:52:06
|
Boolean-hole principle
|
kurgm |
Success |
|
|
| 1331 |
2020/01/09 20:04:51
|
n * S m = n + n * m
|
nekodesu |
Failure |
|
|
| 1330 |
2020/01/09 20:04:32
|
forall f: bool -> bool, f^3(x) = f(x)
|
nekodesu |
Failure |
|
|
| 1329 |
2020/01/09 20:03:43
|
infinite bool sequence is uncountable
|
blue_jam |
Failure |
|
|
| 1328 |
2020/01/09 19:59:54
|
n * S m = n + n * m
|
nuip |
Failure |
|
|
| 1327 |
2020/01/09 19:53:06
|
forall f: bool -> bool, f^3(x) = f(x)
|
nuip |
Failure |
|
|
| 1326 |
2020/01/09 19:39:15
|
infinite bool sequence is uncountable
|
nuip |
Failure |
|
|
| 1325 |
2020/01/09 18:54:16
|
1 + 1 = 2
|
nekodesu |
Failure |
|
|
| 1324 |
2020/01/09 18:51:16
|
plus_comm
|
nekodesu |
Failure |
|
|
| 1323 |
2020/01/09 18:49:04
|
plus_assoc
|
nekodesu |
Failure |
|
|
| 1322 |
2020/01/04 20:34:47
|
plus_comm
|
Eldora |
Success |
|
|
| 1321 |
2020/01/04 05:39:42
|
1 + 1 = 2
|
Eldora |
Success |
|
|
| 1320 |
2020/01/04 05:39:23
|
1 + 1 = 2
|
Eldora |
Failure |
|
|
| 1319 |
2019/12/26 23:13:56
|
Relative prime squares
|
fetburner |
Success |
|
|
| 1318 |
2019/12/24 17:34:20
|
Multiplication of non-zero value in F_p is injective
|
fetburner |
Success |
|
|
| 1317 |
2019/12/22 21:20:17
|
n < m \/ n = m \/ n > m
|
nmjr31 |
Success |
|
|
| 1316 |
2019/12/22 11:51:52
|
l1 <> l2 if l2 is an odd permutation of l1
|
fetburner |
Success |
|
|
| 1315 |
2019/12/22 09:05:44
|
Equivalent two quicksorts
|
fetburner |
Success |
|
|
| 1314 |
2019/12/22 08:58:19
|
Equivalent two quicksorts
|
fetburner |
Failure |
|
|
| 1313 |
2019/12/21 23:12:41
|
n * S m = n + n * m
|
nmjr31 |
Success |
|
|
| 1312 |
2019/12/21 22:48:32
|
forall f: bool -> bool, f^3(x) = f(x)
|
nmjr31 |
Success |
|
|
| 1311 |
2019/12/21 22:23:29
|
1 + 1 = 2
|
nmjr31 |
Success |
|
|
| 1310 |
2019/12/21 22:21:41
|
plus_comm
|
nmjr31 |
Success |
|
|
| 1309 |
2019/12/21 22:02:40
|
plus_assoc
|
nmjr31 |
Success |
|
|
| 1308 |
2019/12/21 22:00:49
|
plus_assoc
|
nmjr31 |
Failure |
|
|
| 1307 |
2019/12/21 16:31:58
|
n * S m = n + n * m
|
ry3s |
Success |
|
|
| 1306 |
2019/12/21 16:10:00
|
forall f: bool -> bool, f^3(x) = f(x)
|
ry3s |
Success |
|
|
| 1305 |
2019/12/21 15:58:36
|
1 + 1 = 2
|
ry3s |
Success |
|
|
| 1304 |
2019/12/21 15:55:31
|
plus_comm
|
ry3s |
Success |
|
|
| 1303 |
2019/12/21 15:33:37
|
plus_assoc
|
ry3s |
Success |
|
|
| 1302 |
2019/12/20 16:13:13
|
Uniqueness of inequality proofs
|
fetburner |
Success |
|
|
| 1301 |
2019/12/20 15:08:28
|
Binary search
|
fetburner |
Success |
|
|
| 1300 |
2019/12/20 14:02:28
|
Iterated iteration
|
fetburner |
Success |
|
|
| 1299 |
2019/12/20 12:01:04
|
Grand Garden
|
fetburner |
Success |
|
|
| 1298 |
2019/12/20 10:13:28
|
Sum of binomial coefficients
|
fetburner |
Success |
|
|
| 1297 |
2019/12/20 09:30:37
|
Tree addressing is injective
|
fetburner |
Success |
|
|
| 1296 |
2019/12/20 09:19:16
|
infinite bool sequence is uncountable
|
fetburner |
Success |
|
|
| 1295 |
2019/12/20 09:07:02
|
Double
|
fetburner |
Success |
|
|
| 1294 |
2019/12/19 20:19:06
|
Zero test
|
nekodesu |
Failure |
|
|
| 1293 |
2019/12/19 20:09:31
|
Boolean-hole principle revisited
|
nuip |
Failure |
|
|
| 1292 |
2019/12/19 20:03:05
|
Boolean-hole principle revisited
|
nekodesu |
Failure |
|
|
| 1291 |
2019/12/18 23:58:47
|
Boolean-hole principle revisited
|
fetburner |
Success |
|
|
| 1290 |
2019/12/18 23:54:11
|
Midpoint
|
fetburner |
Success |
|
|
| 1289 |
2019/12/18 23:23:05
|
Zero test
|
fetburner |
Success |
|
|
| 1288 |
2019/12/18 23:20:57
|
Constructor is injective
|
fetburner |
Success |
|
|
| 1287 |
2019/12/18 23:19:55
|
Yoneda embedding for preorder
|
fetburner |
Success |
|
|
| 1286 |
2019/12/18 23:06:13
|
Two is not Three
|
fetburner |
Success |
|
|
| 1285 |
2019/12/18 22:52:38
|
Three is prime
|
fetburner |
Success |
|
|
| 1284 |
2019/12/18 22:38:47
|
Boolean-hole principle
|
fetburner |
Success |
|
|
| 1283 |
2019/12/18 22:36:49
|
De Morgan's laws in Coq
|
fetburner |
Success |
|
|
| 1282 |
2019/12/18 22:32:35
|
Any natural number is expressible in binary notation
|
fetburner |
Success |
|
|
| 1281 |
2019/12/18 22:21:03
|
De Morgan's laws in Coq
|
fetburner |
Rejected |
|
|
| 1280 |
2019/12/18 22:08:28
|
mult_n_O
|
fetburner |
Success |
|
|
| 1279 |
2019/12/18 20:28:17
|
unique count
|
fetburner |
Success |
|
|
| 1278 |
2019/12/18 18:42:09
|
Tree addressing is injective
|
natsugiri |
Success |
|
|
| 1277 |
2019/12/18 16:07:16
|
count l n = count (rev l) n
|
fetburner |
Success |
|
|
| 1276 |
2019/12/18 15:36:37
|
unique (unique l) = l
|
fetburner |
Success |
|
|
| 1275 |
2019/12/18 15:35:25
|
unique count
|
fetburner |
Failure |
|
|
| 1274 |
2019/12/18 15:23:38
|
unique count
|
fetburner |
Failure |
|
|
| 1273 |
2019/12/18 14:54:21
|
gcd(n, n+1) = 1
|
fetburner |
Success |
|
|
| 1272 |
2019/12/18 14:34:59
|
Identity permutation
|
fetburner |
Success |
|
|
| 1271 |
2019/12/18 14:27:26
|
Multiplication in F_2 is idempotent
|
fetburner |
Success |
|
|
| 1270 |
2019/12/18 14:04:07
|
Summand of one
|
fetburner |
Success |
|
|
| 1269 |
2019/12/18 14:03:43
|
Definitions of injectivity
|
fetburner |
Success |
|
|
| 1268 |
2019/12/18 13:58:24
|
Summand of one
|
fetburner |
Failure |
|
|
| 1267 |
2019/12/18 13:55:14
|
Cumulative sum of list
|
fetburner |
Success |
|
|
| 1266 |
2019/12/18 13:39:04
|
forall l: list nat, l @ [0] <> []
|
fetburner |
Success |
|
|
| 1265 |
2019/12/17 02:12:58
|
Equivalent two quicksorts
|
tzik |
Success |
|
|
| 1264 |
2019/12/14 04:21:16
|
Product of n consecutive integers is divisible by n!
|
fetburner |
Success |
|
|
| 1263 |
2019/12/14 04:14:37
|
Product of n consecutive integers is divisible by n!
|
fetburner |
Success |
|
|
| 1262 |
2019/12/14 02:46:17
|
n < m \/ n = m \/ n > m
|
fetburner |
Success |
|
|
| 1261 |
2019/12/14 02:42:56
|
n * S m = n + n * m
|
fetburner |
Success |
|
|
| 1260 |
2019/12/14 02:39:35
|
forall f: bool -> bool, f^3(x) = f(x)
|
fetburner |
Success |
|
|
| 1259 |
2019/12/14 02:36:49
|
1 + 1 = 2
|
fetburner |
Success |
|
|
| 1258 |
2019/12/14 02:35:48
|
plus_comm
|
fetburner |
Success |
|
|
| 1257 |
2019/12/14 02:32:44
|
plus_assoc
|
fetburner |
Success |
|
|
| 1256 |
2019/12/12 23:11:45
|
Midpoint
|
natsugiri |
Success |
|
|
| 1255 |
2019/12/12 20:26:03
|
Zero test
|
CoiL |
Success |
|
|
| 1254 |
2019/12/12 20:11:40
|
Iterated iteration
|
CoiL |
Success |
|
|
| 1253 |
2019/12/12 19:33:10
|
Iterated iteration
|
CoiL |
Rejected |
|
|
| 1252 |
2019/12/10 21:38:47
|
Midpoint
|
maple |
Success |
|
|
| 1251 |
2019/12/10 18:14:22
|
Zero test
|
maple |
Success |
|
|
| 1250 |
2019/12/10 17:04:59
|
plus_comm
|
maple |
Success |
|
|
| 1249 |
2019/12/10 16:55:06
|
plus_assoc
|
maple |
Success |
|
|
| 1248 |
2019/12/10 12:54:47
|
Iterated iteration
|
chy |
Success |
|
|
| 1247 |
2019/12/10 12:54:04
|
Iterated iteration
|
chy |
Failure |
|
|
| 1246 |
2019/12/10 03:08:26
|
Binary search
|
tzik |
Success |
|
|
| 1245 |
2019/12/09 23:48:52
|
Midpoint
|
tzik |
Success |
|
|
| 1244 |
2019/12/09 21:09:15
|
Boolean-hole principle revisited
|
natsugiri |
Success |
|
|
| 1243 |
2019/12/09 12:57:53
|
Zero test
|
muratak |
Success |
|
|
| 1242 |
2019/12/09 04:21:46
|
Multiplication of non-zero value in F_p is injective
|
tanakh |
Success |
|
|
| 1241 |
2019/12/09 04:20:25
|
Multiplication of non-zero value in F_p is injective
|
tanakh |
Failure |
|
|
| 1240 |
2019/12/09 02:52:18
|
Binary search
|
yodvhskd |
Success |
|
|
| 1239 |
2019/12/09 02:27:53
|
Binary search
|
yodvhskd |
Success |
|
|
| 1238 |
2019/12/08 23:54:53
|
Binary search
|
yodvhskd |
Success |
|
|
| 1237 |
2019/12/08 23:11:05
|
Boolean-hole principle revisited
|
tanakh |
Success |
|
|
| 1236 |
2019/12/08 23:06:52
|
Boolean-hole principle revisited
|
tzik |
Success |
|
|
| 1235 |
2019/12/08 23:05:42
|
Zero test
|
tanakh |
Success |
|
|
| 1234 |
2019/12/08 23:04:29
|
Boolean-hole principle revisited
|
tzik |
Success |
|
|
| 1233 |
2019/12/08 22:32:31
|
Binary search
|
kkob |
Success |
|
|
| 1232 |
2019/12/08 22:10:28
|
Zero test
|
a_kawashiro |
Success |
|
|
| 1231 |
2019/12/08 22:09:18
|
Midpoint
|
mttm |
Success |
|
|
| 1230 |
2019/12/08 21:55:21
|
Midpoint
|
tzik |
Success |
|
|
| 1229 |
2019/12/08 21:46:19
|
Boolean-hole principle revisited
|
mttm |
Success |
|
|
| 1228 |
2019/12/08 21:45:50
|
Midpoint
|
na4zagin3 |
Success |
|
|
| 1227 |
2019/12/08 21:42:20
|
Boolean-hole principle revisited
|
mttm |
Success |
|
|
| 1226 |
2019/12/08 21:41:27
|
Binary search
|
kik |
Success |
|
|
| 1225 |
2019/12/08 21:31:06
|
Zero test
|
tzik |
Success |
|
|
| 1224 |
2019/12/08 21:24:36
|
Boolean-hole principle revisited
|
chy |
Success |
|
|
| 1223 |
2019/12/08 21:02:38
|
Boolean-hole principle revisited
|
yodvhskd |
Success |
|
|
| 1222 |
2019/12/08 21:02:00
|
Boolean-hole principle revisited
|
na4zagin3 |
Success |
|
|
| 1221 |
2019/12/08 20:57:39
|
Midpoint
|
chy |
Success |
|
|
| 1220 |
2019/12/08 20:46:49
|
Midpoint
|
tanakh |
Success |
|
|
| 1219 |
2019/12/08 20:42:55
|
Zero test
|
natsugiri |
Success |
|
|
| 1218 |
2019/12/08 20:41:59
|
Zero test
|
natsugiri |
Failure |
|
|
| 1217 |
2019/12/08 20:41:54
|
Binary search
|
kkob |
Success |
|
|
| 1216 |
2019/12/08 20:39:42
|
Boolean-hole principle revisited
|
kik |
Success |
|
|
| 1215 |
2019/12/08 20:37:59
|
Midpoint
|
yodvhskd |
Success |
|
|
| 1214 |
2019/12/08 20:33:35
|
Boolean-hole principle revisited
|
kaz |
Success |
|
|
| 1213 |
2019/12/08 20:31:14
|
Midpoint
|
kaz |
Success |
|
|
| 1212 |
2019/12/08 20:30:40
|
Zero test
|
chy |
Success |
|
|
| 1211 |
2019/12/08 20:29:42
|
Midpoint
|
kik |
Success |
|
|
| 1210 |
2019/12/08 20:22:49
|
Zero test
|
mttm |
Success |
|
|
| 1209 |
2019/12/08 20:19:22
|
Boolean-hole principle revisited
|
kkob |
Success |
|
|
| 1208 |
2019/12/08 20:11:47
|
Midpoint
|
kkob |
Success |
|
|
| 1207 |
2019/12/08 20:09:50
|
Zero test
|
kik |
Success |
|
|
| 1206 |
2019/12/08 20:06:56
|
Zero test
|
kaz |
Success |
|
|
| 1205 |
2019/12/08 20:06:55
|
Zero test
|
kkob |
Success |
|
|
| 1204 |
2019/12/08 20:05:45
|
Zero test
|
na4zagin3 |
Success |
|
|
| 1203 |
2019/12/08 20:03:56
|
Zero test
|
yodvhskd |
Success |
|
|
| 1202 |
2019/12/08 09:58:50
|
Identity permutation
|
tanakh |
Success |
|
|
| 1201 |
2019/12/08 09:21:37
|
Product of n consecutive integers is divisible by n!
|
tanakh |
Success |
|
|
| 1200 |
2019/12/08 03:24:24
|
infinite bool sequence is uncountable
|
tanakh |
Success |
|
|
| 1199 |
2019/12/08 03:10:19
|
Tree addressing is injective
|
tanakh |
Success |
|
|
| 1198 |
2019/12/08 00:18:39
|
Double
|
tanakh |
Success |
|
|
| 1197 |
2019/12/08 00:11:10
|
Two is not Three
|
tanakh |
Success |
|
|
| 1196 |
2019/12/07 23:45:27
|
Any natural number is expressible in binary notation
|
tanakh |
Success |
|
|
| 1195 |
2019/12/07 21:16:45
|
unique count
|
tanakh |
Success |
|
|
| 1194 |
2019/12/05 07:33:18
|
unique (unique l) = l
|
tanakh |
Success |
|
|
| 1193 |
2019/12/05 07:31:08
|
unique (unique l) = l
|
tanakh |
Success |
|
|
| 1192 |
2019/12/04 21:40:19
|
Multiplication in F_2 is idempotent
|
tanakh |
Success |
|
|
| 1191 |
2019/12/04 21:39:48
|
Multiplication in F_2 is idempotent
|
tanakh |
Failure |
|
|
| 1190 |
2019/12/04 21:35:02
|
count l n = count (rev l) n
|
tanakh |
Success |
|
|
| 1189 |
2019/12/04 21:34:27
|
count l n = count (rev l) n
|
tanakh |
Failure |
|
|
| 1188 |
2019/12/04 21:33:39
|
count l n = count (rev l) n
|
tanakh |
Failure |
|
|
| 1187 |
2019/12/04 20:32:59
|
Binary search
|
kozima |
Success |
|
|
| 1186 |
2019/12/04 20:31:47
|
Boolean-hole principle revisited
|
kozima |
Success |
|
|
| 1185 |
2019/12/04 20:31:25
|
Midpoint
|
kozima |
Success |
|
|
| 1184 |
2019/12/04 20:30:51
|
Zero test
|
kozima |
Success |
|
|
| 1183 |
2019/12/04 06:31:07
|
Definitions of injectivity
|
tanakh |
Success |
|
|
| 1182 |
2019/12/04 05:17:13
|
Definitions of injectivity
|
tanakh |
Rejected |
|
|
| 1181 |
2019/12/04 04:37:21
|
Cumulative sum of list
|
tanakh |
Success |
|
|
| 1180 |
2019/12/04 04:36:46
|
Cumulative sum of list
|
tanakh |
Failure |
|
|
| 1179 |
2019/12/04 04:36:28
|
Cumulative sum of list
|
tanakh |
Failure |
|
|
| 1178 |
2019/12/04 02:42:18
|
Grand Garden
|
tzik |
Success |
|
|
| 1177 |
2019/12/02 04:25:54
|
Sum of binomial coefficients
|
tzik |
Success |
|
|
| 1176 |
2019/12/01 15:58:41
|
n < m \/ n = m \/ n > m
|
na4zagin3 |
Success |
|
|
| 1175 |
2019/12/01 15:46:54
|
Three is prime
|
na4zagin3 |
Success |
|
|
| 1174 |
2019/11/30 23:48:24
|
Product of n consecutive integers is divisible by n!
|
kik |
Success |
|
|
| 1173 |
2019/11/30 19:21:16
|
n < m \/ n = m \/ n > m
|
cyan |
Success |
|
|
| 1172 |
2019/11/30 03:27:51
|
n < m \/ n = m \/ n > m
|
kik |
Success |
|
|
| 1171 |
2019/11/30 03:22:43
|
n * S m = n + n * m
|
kik |
Success |
|
|
| 1170 |
2019/11/30 03:05:30
|
1 + 1 = 2
|
kik |
Success |
|
|
| 1169 |
2019/11/30 03:04:00
|
plus_comm
|
kik |
Success |
|
|
| 1168 |
2019/11/30 02:38:10
|
plus_assoc
|
kik |
Success |
|
|
| 1167 |
2019/11/30 02:21:55
|
forall f: bool -> bool, f^3(x) = f(x)
|
kik |
Success |
|
|
| 1166 |
2019/11/30 01:43:19
|
forall f: bool -> bool, f^3(x) = f(x)
|
natsugiri |
Success |
|
|
| 1165 |
2019/11/29 23:24:54
|
Two is not Three
|
na4zagin3 |
Success |
|
|
| 1164 |
2019/11/29 10:59:09
|
n * S m = n + n * m
|
cyan |
Success |
|
|
| 1163 |
2019/11/29 04:57:32
|
forall l: list nat, l @ [0] <> []
|
natsugiri |
Success |
|
|
| 1162 |
2019/11/29 02:18:37
|
plus_assoc
|
natsugiri |
Success |
|
|
| 1161 |
2019/11/28 22:33:57
|
Relative prime squares
|
tzik |
Success |
|
|
| 1160 |
2019/11/28 20:56:50
|
Multiplication of non-zero value in F_p is injective
|
CoiL |
Success |
|
|
| 1159 |
2019/11/28 20:38:33
|
Two is not Three
|
blue_jam |
Failure |
|
|
| 1158 |
2019/11/28 20:38:24
|
Summand of one
|
blue_jam |
Failure |
|
|
| 1157 |
2019/11/28 20:37:32
|
Two is not Three
|
nuip |
Failure |
|
|
| 1156 |
2019/11/28 20:37:29
|
Two is not Three
|
nekodesu |
Failure |
|
|
| 1155 |
2019/11/28 19:11:30
|
Double
|
natsugiri |
Success |
|
|
| 1154 |
2019/11/28 18:52:43
|
forall f: bool -> bool, f^3(x) = f(x)
|
cyan |
Success |
|
|
| 1153 |
2019/11/28 18:35:38
|
1 + 1 = 2
|
cyan |
Success |
|
|
| 1152 |
2019/11/28 18:33:54
|
plus_comm
|
cyan |
Success |
|
|
| 1151 |
2019/11/28 18:11:56
|
n < m \/ n = m \/ n > m
|
tanakh |
Success |
|
|
| 1150 |
2019/11/28 17:43:10
|
plus_assoc
|
cyan |
Success |
|
|
| 1149 |
2019/11/28 17:09:16
|
Three is prime
|
tanakh |
Success |
|
|
| 1148 |
2019/11/28 15:52:15
|
Uniqueness of inequality proofs
|
yodvhskd |
Success |
|
|
| 1147 |
2019/11/28 10:01:37
|
Multiplication of non-zero value in F_p is injective
|
tzik |
Success |
|
|
| 1146 |
2019/11/28 07:27:14
|
Iterated iteration
|
tzik |
Success |
|
|
| 1145 |
2019/11/28 03:22:36
|
unique (unique l) = l
|
natsugiri |
Success |
|
|
| 1144 |
2019/11/27 22:29:22
|
Multiplication in F_2 is idempotent
|
natsugiri |
Success |
|
|
| 1143 |
2019/11/27 22:29:09
|
Multiplication in F_2 is idempotent
|
natsugiri |
Failure |
|
|
| 1142 |
2019/11/27 20:52:25
|
Definitions of injectivity
|
natsugiri |
Success |
|
|
| 1141 |
2019/11/27 16:12:53
|
De Morgan's laws in Coq
|
tanakh |
Success |
|
|
| 1140 |
2019/11/27 16:12:00
|
De Morgan's laws in Coq
|
tanakh |
Rejected |
|
|
| 1139 |
2019/11/27 02:45:47
|
Cumulative sum of list
|
natsugiri |
Success |
|
|
| 1138 |
2019/11/27 01:37:47
|
Two is not Three
|
tzik |
Success |
|
|
| 1137 |
2019/11/27 01:37:14
|
Identity permutation
|
tzik |
Success |
|
|
| 1136 |
2019/11/26 23:46:59
|
n < m \/ n = m \/ n > m
|
natsugiri |
Success |
|
|
| 1135 |
2019/11/26 23:28:49
|
infinite bool sequence is uncountable
|
mttm |
Success |
|
|
| 1134 |
2019/11/26 22:57:57
|
Constructor is injective
|
natsugiri |
Success |
|
|
| 1133 |
2019/11/26 22:57:25
|
Constructor is injective
|
natsugiri |
Failure |
|
|
| 1132 |
2019/11/26 22:56:44
|
Constructor is injective
|
natsugiri |
Failure |
|
|
| 1131 |
2019/11/26 22:53:50
|
Yoneda embedding for preorder
|
natsugiri |
Success |
|
|
| 1130 |
2019/11/26 05:02:00
|
count l n = count (rev l) n
|
natsugiri |
Success |
|
|
| 1129 |
2019/11/26 03:18:29
|
Three is prime
|
natsugiri |
Success |
|
|
| 1128 |
2019/11/26 03:04:53
|
Relative prime squares
|
yodvhskd |
Success |
|
|
| 1127 |
2019/11/26 02:32:48
|
Boolean-hole principle
|
natsugiri |
Success |
|
|
| 1126 |
2019/11/26 02:28:31
|
De Morgan's laws in Coq
|
natsugiri |
Success |
|
|
| 1125 |
2019/11/26 02:28:03
|
De Morgan's laws in Coq
|
natsugiri |
Rejected |
|
|
| 1124 |
2019/11/26 01:30:34
|
mult_n_O
|
natsugiri |
Success |
|
|
| 1123 |
2019/11/26 01:29:01
|
gcd(n, n+1) = 1
|
natsugiri |
Success |
|
|
| 1122 |
2019/11/26 01:27:19
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1121 |
2019/11/26 01:25:16
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1120 |
2019/11/26 01:22:41
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1119 |
2019/11/26 01:01:15
|
Summand of one
|
natsugiri |
Success |
|
|
| 1118 |
2019/11/26 00:08:57
|
Summand of one
|
saitou |
Success |
|
|
| 1117 |
2019/11/26 00:03:52
|
forall l: list nat, l @ [0] <> []
|
saitou |
Success |
|
|
| 1116 |
2019/11/25 04:46:29
|
unique (unique l) = l
|
tzik |
Success |
|
|
| 1115 |
2019/11/25 04:32:56
|
unique count
|
tzik |
Success |
|
|
| 1114 |
2019/11/25 03:31:31
|
Double
|
tzik |
Success |
|
|
| 1113 |
2019/11/25 03:30:32
|
n * S m = n + n * m
|
natsugiri |
Success |
|
|
| 1112 |
2019/11/25 03:22:50
|
Yoneda embedding for preorder
|
tanakh |
Success |
|
|
| 1111 |
2019/11/25 03:12:16
|
Any natural number is expressible in binary notation
|
tzik |
Success |
|
|
| 1110 |
2019/11/25 03:09:56
|
Boolean-hole principle
|
tanakh |
Success |
|
|
| 1109 |
2019/11/25 03:05:39
|
mult_n_O
|
tanakh |
Success |
|
|
| 1108 |
2019/11/25 03:03:56
|
mult_n_O
|
tanakh |
Success |
|
|
| 1107 |
2019/11/25 03:02:14
|
gcd(n, n+1) = 1
|
tanakh |
Success |
|
|
| 1106 |
2019/11/25 02:48:46
|
Summand of one
|
tanakh |
Success |
|
|
| 1105 |
2019/11/25 02:46:12
|
Boolean-hole principle
|
tzik |
Success |
|
|
| 1104 |
2019/11/25 02:43:36
|
De Morgan's laws in Coq
|
tzik |
Success |
|
|
| 1103 |
2019/11/25 02:20:14
|
mult_n_O
|
tzik |
Success |
|
|
| 1102 |
2019/11/25 02:06:26
|
Three is prime
|
tzik |
Success |
|
|
| 1101 |
2019/11/25 01:56:33
|
forall l: list nat, l @ [0] <> []
|
tanakh |
Success |
|
|
| 1100 |
2019/11/25 00:23:16
|
Relative prime squares
|
kkob |
Success |
|
|
| 1099 |
2019/11/24 23:51:36
|
Yoneda embedding for preorder
|
tzik |
Success |
|
|
| 1098 |
2019/11/24 22:59:09
|
plus_comm
|
lion |
Success |
|
|
| 1097 |
2019/11/24 22:56:17
|
Tree addressing is injective
|
mttm |
Success |
|
|
| 1096 |
2019/11/24 22:50:59
|
plus_comm
|
lion |
Failure |
|
|
| 1095 |
2019/11/24 22:32:09
|
plus_comm
|
lion |
Failure |
|
|
| 1094 |
2019/11/24 22:15:14
|
1 + 1 = 2
|
lion |
Success |
|
|
| 1093 |
2019/11/24 22:14:40
|
1 + 1 = 2
|
lion |
Failure |
|
|
| 1092 |
2019/11/24 21:53:22
|
Tree addressing is injective
|
yamarten |
Success |
|
|
| 1091 |
2019/11/24 21:36:45
|
Relative prime squares
|
kozima |
Success |
|
|
| 1090 |
2019/11/24 21:35:09
|
1 + 1 = 2
|
lion |
Failure |
|
|
| 1089 |
2019/11/24 21:18:11
|
infinite bool sequence is uncountable
|
saitou |
Success |
|
|
| 1088 |
2019/11/24 21:11:02
|
infinite bool sequence is uncountable
|
hirosegolf |
Success |
|
|
| 1087 |
2019/11/24 21:07:27
|
infinite bool sequence is uncountable
|
hirosegolf |
Failure |
|
|
| 1086 |
2019/11/24 21:04:22
|
infinite bool sequence is uncountable
|
hirosegolf |
Failure |
|
|
| 1085 |
2019/11/24 21:01:11
|
Constructor is injective
|
tanakh |
Success |
|
|
| 1084 |
2019/11/24 21:00:48
|
Constructor is injective
|
tanakh |
Failure |
|
|
| 1083 |
2019/11/24 20:49:38
|
Tree addressing is injective
|
hirosegolf |
Success |
|
|
| 1082 |
2019/11/24 20:46:12
|
infinite bool sequence is uncountable
|
tzik |
Success |
|
|
| 1081 |
2019/11/24 20:42:17
|
infinite bool sequence is uncountable
|
na4zagin3 |
Success |
|
|
| 1080 |
2019/11/24 20:35:26
|
infinite bool sequence is uncountable
|
na4zagin3 |
Failure |
|
|
| 1079 |
2019/11/24 20:33:10
|
infinite bool sequence is uncountable
|
chy |
Success |
|
|
| 1078 |
2019/11/24 20:32:29
|
Tree addressing is injective
|
tzik |
Success |
|
|
| 1077 |
2019/11/24 20:26:35
|
Tree addressing is injective
|
pekempey |
Success |
|
|
| 1076 |
2019/11/24 20:24:34
|
Tree addressing is injective
|
saitou |
Success |
|
|
| 1075 |
2019/11/24 20:21:56
|
Tree addressing is injective
|
chy |
Success |
|
|
| 1074 |
2019/11/24 20:20:05
|
infinite bool sequence is uncountable
|
sorata |
Success |
|
|
| 1073 |
2019/11/24 20:18:56
|
Tree addressing is injective
|
chy |
Failure |
|
|
| 1072 |
2019/11/24 20:18:44
|
infinite bool sequence is uncountable
|
kaz |
Success |
|
|
| 1071 |
2019/11/24 20:16:26
|
infinite bool sequence is uncountable
|
yodvhskd |
Success |
|
|
| 1070 |
2019/11/24 20:15:29
|
Tree addressing is injective
|
na4zagin3 |
Success |
|
|
| 1069 |
2019/11/24 20:13:48
|
infinite bool sequence is uncountable
|
kozima |
Success |
|
|
| 1068 |
2019/11/24 20:11:27
|
Tree addressing is injective
|
sorata |
Success |
|
|
| 1067 |
2019/11/24 20:11:21
|
Constructor is injective
|
yamarten |
Success |
|
|
| 1066 |
2019/11/24 20:10:35
|
Tree addressing is injective
|
kozima |
Success |
|
|
| 1065 |
2019/11/24 20:09:43
|
Tree addressing is injective
|
kaz |
Success |
|
|
| 1064 |
2019/11/24 20:09:41
|
Constructor is injective
|
kaz |
Success |
|
|
| 1063 |
2019/11/24 20:09:22
|
Constructor is injective
|
mttm |
Success |
|
|
| 1062 |
2019/11/24 20:09:21
|
Tree addressing is injective
|
yodvhskd |
Success |
|
|
| 1061 |
2019/11/24 20:05:09
|
Constructor is injective
|
hirosegolf |
Success |
|
|
| 1060 |
2019/11/24 20:03:30
|
Constructor is injective
|
saitou |
Success |
|
|
| 1059 |
2019/11/24 20:03:05
|
Constructor is injective
|
pekempey |
Success |
|
|
| 1058 |
2019/11/24 20:03:02
|
Constructor is injective
|
tzik |
Success |
|
|
| 1057 |
2019/11/24 20:02:16
|
Constructor is injective
|
na4zagin3 |
Success |
|
|
| 1056 |
2019/11/24 20:01:44
|
Constructor is injective
|
sorata |
Success |
|
|
| 1055 |
2019/11/24 20:01:25
|
Constructor is injective
|
chy |
Success |
|
|
| 1054 |
2019/11/24 20:01:06
|
Constructor is injective
|
kozima |
Success |
|
|
| 1053 |
2019/11/24 20:01:01
|
Constructor is injective
|
yodvhskd |
Success |
|
|
| 1052 |
2019/11/24 17:53:38
|
1 + 1 = 2
|
kano |
Success |
|
|
| 1051 |
2019/11/24 17:46:46
|
plus_comm
|
kano |
Success |
|
|
| 1050 |
2019/11/24 17:41:25
|
plus_assoc
|
kano |
Success |
|
|
| 1049 |
2019/11/24 17:38:56
|
plus_assoc
|
kano |
Failure |
|
|
| 1048 |
2019/11/24 17:37:45
|
plus_assoc
|
kano |
Failure |
|
|
| 1047 |
2019/11/24 17:36:56
|
plus_assoc
|
kano |
Failure |
|
|
| 1046 |
2019/11/22 03:07:00
|
count l n = count (rev l) n
|
tzik |
Success |
|
|
| 1045 |
2019/11/22 02:42:23
|
gcd(n, n+1) = 1
|
tzik |
Success |
|
|
| 1044 |
2019/11/22 02:29:50
|
Multiplication in F_2 is idempotent
|
tzik |
Success |
|
|
| 1043 |
2019/11/22 01:53:49
|
Definitions of injectivity
|
tzik |
Success |
|
|
| 1042 |
2019/11/21 21:09:59
|
Summand of one
|
tzik |
Success |
|
|
| 1041 |
2019/11/21 20:39:21
|
Cumulative sum of list
|
tzik |
Success |
|
|
| 1040 |
2019/11/21 20:08:40
|
Multiplication in F_2 is idempotent
|
nekodesu |
Failure |
|
|
| 1039 |
2019/11/21 20:06:02
|
forall l: list nat, l @ [0] <> []
|
tzik |
Success |
|
|
| 1038 |
2019/11/21 19:55:59
|
Product of n consecutive integers is divisible by n!
|
tzik |
Success |
|
|
| 1037 |
2019/11/21 19:54:29
|
Product of n consecutive integers is divisible by n!
|
tzik |
Failure |
|
|
| 1036 |
2019/11/21 19:53:42
|
n < m \/ n = m \/ n > m
|
tzik |
Success |
|
|
| 1035 |
2019/11/21 00:10:55
|
Relative prime squares
|
kkob |
Success |
|
|
| 1034 |
2019/11/20 20:27:36
|
n * S m = n + n * m
|
tanakh |
Success |
|
|
| 1033 |
2019/11/20 20:10:26
|
plus_comm
|
tanakh |
Success |
|
|
| 1032 |
2019/11/20 19:50:06
|
plus_assoc
|
tanakh |
Success |
|
|
| 1031 |
2019/11/20 19:32:16
|
forall f: bool -> bool, f^3(x) = f(x)
|
tanakh |
Success |
|
|
| 1030 |
2019/11/20 19:09:36
|
1 + 1 = 2
|
tanakh |
Success |
|
|
| 1029 |
2019/11/20 18:56:43
|
1 + 1 = 2
|
a_kawashiro |
Success |
|
|
| 1028 |
2019/11/19 02:48:05
|
n * S m = n + n * m
|
tzik |
Success |
|
|
| 1027 |
2019/11/19 02:33:59
|
forall f: bool -> bool, f^3(x) = f(x)
|
tzik |
Success |
|
|
| 1026 |
2019/11/18 20:57:49
|
plus_comm
|
tzik |
Success |
|
|
| 1025 |
2019/11/18 20:55:03
|
plus_assoc
|
tzik |
Success |
|
|
| 1024 |
2019/11/18 20:53:25
|
1 + 1 = 2
|
tzik |
Success |
|
|
| 1023 |
2019/11/18 20:52:58
|
1 + 1 = 2
|
tzik |
Failure |
|
|
| 1022 |
2019/11/18 05:49:58
|
infinite bool sequence is uncountable
|
kkob |
Success |
|
|
| 1021 |
2019/11/18 05:48:11
|
Tree addressing is injective
|
kkob |
Success |
|
|
| 1020 |
2019/11/18 05:46:25
|
Constructor is injective
|
kkob |
Success |
|
|
| 1019 |
2019/11/14 20:34:43
|
gcd(n, n+1) = 1
|
blue_jam |
Failure |
|
|
| 1018 |
2019/11/14 20:33:02
|
gcd(n, n+1) = 1
|
nuip |
Failure |
|
|
| 1017 |
2019/11/11 01:23:21
|
Uniqueness of inequality proofs
|
yodvhskd |
Success |
|
|
| 1016 |
2019/11/10 22:21:39
|
De Morgan's laws in Coq
|
yodvhskd |
Success |
|
|
| 1015 |
2019/11/10 22:15:03
|
mult_n_O
|
yodvhskd |
Success |
|
|
| 1014 |
2019/11/10 22:13:42
|
n * S m = n + n * m
|
yodvhskd |
Success |
|
|
| 1013 |
2019/11/10 22:11:58
|
Summand of one
|
yodvhskd |
Success |
|
|
| 1012 |
2019/11/10 22:07:56
|
n < m \/ n = m \/ n > m
|
yodvhskd |
Success |
|
|
| 1011 |
2019/11/10 22:07:01
|
Definitions of injectivity
|
yodvhskd |
Success |
|
|
| 1010 |
2019/11/10 21:59:54
|
Any natural number is expressible in binary notation
|
yodvhskd |
Success |
|
|
| 1009 |
2019/11/10 21:48:52
|
Any natural number is expressible in binary notation
|
yodvhskd |
Rejected |
|
|
| 1008 |
2019/11/10 21:04:29
|
Multiplication of non-zero value in F_p is injective
|
yodvhskd |
Success |
|
|
| 1007 |
2019/11/10 19:19:56
|
Grand Garden
|
yodvhskd |
Success |
|
|
| 1006 |
2019/11/10 16:49:26
|
Identity permutation
|
yodvhskd |
Success |
|
|
| 1005 |
2019/11/10 03:38:44
|
Equivalent two quicksorts
|
yodvhskd |
Success |
|
|
| 1004 |
2019/11/09 22:00:05
|
n < m \/ n = m \/ n > m
|
lo48576 |
Success |
|
|
| 1003 |
2019/11/09 20:22:48
|
Three is prime
|
lo48576 |
Success |
|
|
| 1002 |
2019/11/09 15:52:44
|
Boolean-hole principle
|
lo48576 |
Success |
|
|
| 1001 |
2019/11/09 15:49:14
|
Boolean-hole principle
|
lo48576 |
Success |
|
|
| 1000 |
2019/11/09 04:05:18
|
De Morgan's laws in Coq
|
lo48576 |
Success |
|
|
| 999 |
2019/11/09 02:07:44
|
mult_n_O
|
lo48576 |
Success |
|
|
| 998 |
2019/11/09 02:00:36
|
gcd(n, n+1) = 1
|
lo48576 |
Success |
|
|
| 997 |
2019/11/08 03:36:46
|
Summand of one
|
lo48576 |
Success |
|
|
| 996 |
2019/11/08 02:54:03
|
forall l: list nat, l @ [0] <> []
|
lo48576 |
Success |
|
|
| 995 |
2019/11/08 02:50:23
|
forall l: list nat, l @ [0] <> []
|
lo48576 |
Failure |
|
|
| 994 |
2019/11/07 23:16:42
|
n * S m = n + n * m
|
lo48576 |
Success |
|
|
| 993 |
2019/11/07 21:15:46
|
Definitions of injectivity
|
na4zagin3 |
Success |
|
|
| 992 |
2019/11/07 21:13:42
|
Definitions of injectivity
|
nuip |
Failure |
|
|
| 991 |
2019/11/07 20:37:25
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Success |
|
|
| 990 |
2019/11/07 20:37:01
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Failure |
|
|
| 989 |
2019/11/07 20:09:28
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Failure |
|
|
| 988 |
2019/11/07 20:05:22
|
Multiplication in F_2 is idempotent
|
nuip |
Failure |
|
|
| 987 |
2019/11/07 19:46:45
|
Multiplication in F_2 is idempotent
|
yodvhskd |
Success |
|
|
| 986 |
2019/11/07 19:33:35
|
Cumulative sum of list
|
nekodesu |
Failure |
|
|
| 985 |
2019/11/07 19:22:49
|
forall f: bool -> bool, f^3(x) = f(x)
|
lo48576 |
Success |
|
|
| 984 |
2019/11/07 17:36:01
|
plus_comm
|
lo48576 |
Success |
|
|
| 983 |
2019/11/07 17:11:20
|
1 + 1 = 2
|
lo48576 |
Success |
|
|
| 982 |
2019/11/07 16:58:51
|
plus_comm
|
lo48576 |
Success |
|
|
| 981 |
2019/11/07 15:33:17
|
plus_assoc
|
lo48576 |
Success |
|
|
| 980 |
2019/11/07 15:27:50
|
plus_assoc
|
lo48576 |
Success |
|
|
| 979 |
2019/11/06 23:58:13
|
Product of n consecutive integers is divisible by n!
|
yodvhskd |
Success |
|
|
| 978 |
2019/11/05 23:55:09
|
l1 <> l2 if l2 is an odd permutation of l1
|
yodvhskd |
Success |
|
|
| 977 |
2019/11/05 12:53:39
|
n * S m = n + n * m
|
saitou |
Success |
|
|
| 976 |
2019/11/05 12:53:09
|
n * S m = n + n * m
|
saitou |
Success |
|
|
| 975 |
2019/11/05 12:36:33
|
forall f: bool -> bool, f^3(x) = f(x)
|
saitou |
Success |
|
|
| 974 |
2019/11/05 12:23:52
|
1 + 1 = 2
|
saitou |
Success |
|
|
| 973 |
2019/11/05 12:22:53
|
plus_comm
|
saitou |
Success |
|
|
| 972 |
2019/11/05 12:13:41
|
plus_assoc
|
saitou |
Success |
|
|
| 971 |
2019/11/04 22:01:49
|
plus_comm
|
CoiL |
Failure |
|
|
| 970 |
2019/11/04 20:54:24
|
Sum of binomial coefficients
|
yodvhskd |
Success |
|
|
| 969 |
2019/11/04 20:44:39
|
Sum of binomial coefficients
|
yodvhskd |
Failure |
|
|
| 968 |
2019/11/04 20:40:13
|
Sum of binomial coefficients
|
yodvhskd |
Failure |
|
|
| 967 |
2019/11/04 04:34:31
|
Yoneda embedding for preorder
|
ukikagi |
Success |
|
|
| 966 |
2019/11/03 19:57:59
|
mult_n_O
|
egashira |
Success |
|
|
| 965 |
2019/11/03 19:56:29
|
Double
|
egashira |
Success |
|
|
| 964 |
2019/11/01 12:33:30
|
n < m \/ n = m \/ n > m
|
chy |
Success |
|
|
| 963 |
2019/11/01 11:17:15
|
Sum of binomial coefficients
|
chy |
Success |
|
|
| 962 |
2019/11/01 11:16:29
|
Sum of binomial coefficients
|
chy |
Failure |
|
|
| 961 |
2019/11/01 11:15:32
|
Sum of binomial coefficients
|
chy |
Failure |
|
|
| 960 |
2019/10/31 23:22:12
|
Sum of binomial coefficients
|
nuip |
Failure |
|
|
| 959 |
2019/10/31 22:39:21
|
Double
|
chy |
Success |
|
|
| 958 |
2019/10/31 22:14:45
|
Yoneda embedding for preorder
|
chy |
Success |
|
|
| 957 |
2019/10/31 20:38:57
|
Identity permutation
|
CoiL |
Success |
|
|
| 956 |
2019/10/31 20:16:52
|
1 + 1 = 2
|
sh_mug |
Success |
|
|
| 955 |
2019/10/31 20:12:24
|
plus_comm
|
sh_mug |
Success |
|
|
| 954 |
2019/10/31 19:32:56
|
plus_assoc
|
sh_mug |
Success |
|
|
| 953 |
2019/10/31 19:23:02
|
plus_assoc
|
sh_mug |
Failure |
|
|
| 952 |
2019/10/30 17:23:46
|
Double
|
yodvhskd |
Success |
|
|
| 951 |
2019/10/30 17:00:58
|
Yoneda embedding for preorder
|
yodvhskd |
Success |
|
|
| 950 |
2019/10/29 11:04:04
|
Uniqueness of inequality proofs
|
splatoon_suki |
Success |
|
|
| 949 |
2019/10/29 10:58:49
|
Uniqueness of inequality proofs
|
splatoon_suki |
Success |
|
|
| 948 |
2019/10/28 13:25:53
|
Double
|
mttm |
Success |
|
|
| 947 |
2019/10/28 12:21:35
|
Yoneda embedding for preorder
|
mttm |
Success |
|
|
| 946 |
2019/10/26 22:02:02
|
Yoneda embedding for preorder
|
momohatt |
Success |
|
|
| 945 |
2019/10/26 19:24:59
|
Double
|
na4zagin3 |
Success |
|
|
| 944 |
2019/10/26 18:47:08
|
Sum of binomial coefficients
|
kaz |
Success |
|
|
| 943 |
2019/10/26 18:43:06
|
Sum of binomial coefficients
|
kkob |
Success |
|
|
| 942 |
2019/10/26 18:37:32
|
Yoneda embedding for preorder
|
spica314 |
Success |
|
|
| 941 |
2019/10/26 18:36:28
|
Double
|
yamarten |
Success |
|
|
| 940 |
2019/10/26 18:30:10
|
Yoneda embedding for preorder
|
yamarten |
Success |
|
|
| 939 |
2019/10/26 18:15:52
|
Double
|
miya |
Success |
|
|
| 938 |
2019/10/26 18:11:37
|
Double
|
pekempey |
Success |
|
|
| 937 |
2019/10/26 18:07:24
|
Yoneda embedding for preorder
|
yamarten |
Failure |
|
|
| 936 |
2019/10/26 18:07:02
|
Double
|
kaz |
Success |
|
|
| 935 |
2019/10/26 18:06:08
|
Yoneda embedding for preorder
|
miya |
Success |
|
|
| 934 |
2019/10/26 18:05:26
|
Yoneda embedding for preorder
|
miya |
Failure |
|
|
| 933 |
2019/10/26 18:04:36
|
Yoneda embedding for preorder
|
na4zagin3 |
Success |
|
|
| 932 |
2019/10/26 18:03:48
|
Yoneda embedding for preorder
|
kaz |
Success |
|
|
| 931 |
2019/10/26 18:03:42
|
Double
|
kkob |
Success |
|
|
| 930 |
2019/10/26 18:03:05
|
Yoneda embedding for preorder
|
pekempey |
Success |
|
|
| 929 |
2019/10/26 18:02:31
|
Yoneda embedding for preorder
|
pekempey |
Failure |
|
|
| 928 |
2019/10/26 18:02:06
|
Yoneda embedding for preorder
|
kkob |
Success |
|
|
| 927 |
2019/10/26 17:39:44
|
Boolean-hole principle
|
na4zagin3 |
Failure |
|
|
| 926 |
2019/10/25 22:21:27
|
Cumulative sum of list
|
na4zagin3 |
Success |
|
|
| 925 |
2019/10/25 22:07:55
|
Cumulative sum of list
|
na4zagin3 |
Failure |
|
|
| 924 |
2019/10/25 21:39:40
|
Uniqueness of inequality proofs
|
kozima |
Rejected |
|
|
| 923 |
2019/10/25 18:33:56
|
Uniqueness of inequality proofs
|
kozima |
Success |
|
|
| 922 |
2019/10/25 18:29:26
|
Sum of binomial coefficients
|
kozima |
Success |
|
|
| 921 |
2019/10/25 18:26:53
|
Double
|
kozima |
Success |
|
|
| 920 |
2019/10/25 18:20:43
|
Yoneda embedding for preorder
|
kozima |
Success |
|
|
| 919 |
2019/10/24 20:49:48
|
Cumulative sum of list
|
nuip |
Failure |
|
|
| 918 |
2019/10/24 19:13:57
|
forall l: list nat, l @ [0] <> []
|
nekodesu |
Failure |
|
|
| 917 |
2019/10/23 23:52:21
|
n < m \/ n = m \/ n > m
|
miya |
Success |
|
|
| 916 |
2019/10/22 16:34:00
|
Cumulative sum of list
|
miya |
Success |
|
|
| 915 |
2019/10/22 15:57:16
|
Three is prime
|
miya |
Success |
|
|
| 914 |
2019/10/22 15:44:07
|
Boolean-hole principle
|
miya |
Success |
|
|
| 913 |
2019/10/22 15:39:23
|
De Morgan's laws in Coq
|
miya |
Success |
|
|
| 912 |
2019/10/22 15:28:46
|
mult_n_O
|
miya |
Success |
|
|
| 911 |
2019/10/22 15:27:15
|
gcd(n, n+1) = 1
|
miya |
Success |
|
|
| 910 |
2019/10/22 15:18:35
|
Summand of one
|
miya |
Success |
|
|
| 909 |
2019/10/22 15:10:09
|
forall l: list nat, l @ [0] <> []
|
miya |
Success |
|
|
| 908 |
2019/10/22 15:00:56
|
n < m \/ n = m \/ n > m
|
egashira |
Success |
|
|
| 907 |
2019/10/22 14:59:53
|
n < m \/ n = m \/ n > m
|
egashira |
Success |
|
|
| 906 |
2019/10/22 14:07:00
|
n * S m = n + n * m
|
miya |
Success |
|
|
| 905 |
2019/10/22 13:45:56
|
forall f: bool -> bool, f^3(x) = f(x)
|
miya |
Success |
|
|
| 904 |
2019/10/22 13:25:26
|
1 + 1 = 2
|
miya |
Success |
|
|
| 903 |
2019/10/22 13:20:45
|
plus_comm
|
miya |
Success |
|
|
| 902 |
2019/10/22 13:16:02
|
plus_assoc
|
miya |
Success |
|
|
| 901 |
2019/10/22 02:47:53
|
plus_comm
|
yamunaku_ |
Success |
|
|
| 900 |
2019/10/22 02:31:09
|
plus_assoc
|
yamunaku_ |
Success |
|
|
| 899 |
2019/10/22 02:30:46
|
plus_assoc
|
yamunaku_ |
Failure |
|
|
| 898 |
2019/10/21 15:20:50
|
Definitions of injectivity
|
momohatt |
Success |
|
|
| 897 |
2019/10/21 15:07:05
|
Identity permutation
|
momohatt |
Success |
|
|
| 896 |
2019/10/17 20:43:40
|
Three is prime
|
nuip |
Failure |
|
|
| 895 |
2019/10/17 20:39:58
|
count l n = count (rev l) n
|
CoiL |
Success |
|
|
| 894 |
2019/10/17 20:06:30
|
Multiplication in F_2 is idempotent
|
CoiL |
Success |
|
|
| 893 |
2019/10/17 19:37:43
|
Cumulative sum of list
|
CoiL |
Success |
|
|
| 892 |
2019/10/17 19:36:37
|
Cumulative sum of list
|
CoiL |
Success |
|
|
| 891 |
2019/10/12 19:32:42
|
Boolean-hole principle
|
nikeya |
Success |
|
|
| 890 |
2019/10/10 23:35:45
|
plus_assoc
|
JP3BGY |
Success |
|
|
| 889 |
2019/10/10 19:58:25
|
Definitions of injectivity
|
CoiL |
Success |
|
|
| 888 |
2019/10/10 16:38:33
|
1 + 1 = 2
|
ta12ka7shi |
Success |
|
|
| 887 |
2019/10/09 16:10:53
|
Two is not Three
|
CoiL |
Success |
|
|
| 886 |
2019/10/09 16:09:22
|
Two is not Three
|
CoiL |
Failure |
|
|
| 885 |
2019/10/08 13:48:20
|
Boolean-hole principle
|
spica314 |
Success |
|
|
| 884 |
2019/10/08 11:58:14
|
unique count
|
coorde |
Success |
|
|
| 883 |
2019/10/07 15:53:55
|
Any natural number is expressible in binary notation
|
momohatt |
Success |
|
|
| 882 |
2019/10/07 15:51:57
|
Any natural number is expressible in binary notation
|
momohatt |
Failure |
|
|
| 881 |
2019/10/07 15:51:00
|
Any natural number is expressible in binary notation
|
momohatt |
Failure |
|
|
| 880 |
2019/10/07 15:49:51
|
Any natural number is expressible in binary notation
|
momohatt |
Failure |
|
|
| 879 |
2019/10/07 15:36:46
|
Multiplication of non-zero value in F_p is injective
|
momohatt |
Success |
|
|
| 878 |
2019/10/07 14:07:48
|
Three is prime
|
mttm |
Success |
|
|
| 877 |
2019/10/07 09:18:20
|
Two is not Three
|
splatoon_suki |
Success |
|
|
| 876 |
2019/10/06 22:40:11
|
Three is prime
|
pekempey |
Success |
|
|
| 875 |
2019/10/06 22:29:50
|
Two is not Three
|
pekempey |
Success |
|
|
| 874 |
2019/10/06 22:14:52
|
Iterated iteration
|
kaz |
Success |
|
|
| 873 |
2019/10/06 22:06:44
|
Iterated iteration
|
kaz |
Success |
|
|
| 872 |
2019/10/06 22:03:51
|
Iterated iteration
|
coorde |
Success |
|
|
| 871 |
2019/10/06 21:41:56
|
Iterated iteration
|
pekempey |
Success |
|
|
| 870 |
2019/10/06 21:41:43
|
Iterated iteration
|
coorde |
Rejected |
|
|
| 869 |
2019/10/06 21:41:08
|
Iterated iteration
|
coorde |
Failure |
|
|
| 868 |
2019/10/06 21:28:45
|
Iterated iteration
|
hirosegolf |
Success |
|
|
| 867 |
2019/10/06 21:28:07
|
Iterated iteration
|
hirosegolf |
Failure |
|
|
| 866 |
2019/10/06 21:21:20
|
Two is not Three
|
momohatt |
Success |
|
|
| 865 |
2019/10/06 21:17:34
|
Two is not Three
|
sorata |
Success |
|
|
| 864 |
2019/10/06 21:03:23
|
Iterated iteration
|
yodvhskd |
Success |
|
|
| 863 |
2019/10/06 20:59:47
|
Iterated iteration
|
pekempey |
Rejected |
|
|
| 862 |
2019/10/06 20:48:47
|
Three is prime
|
sorata |
Success |
|
|
| 861 |
2019/10/06 20:48:25
|
Boolean-hole principle
|
sorata |
Success |
|
|
| 860 |
2019/10/06 20:46:58
|
Iterated iteration
|
sorata |
Success |
|
|
| 859 |
2019/10/06 20:46:50
|
Boolean-hole principle
|
mttm |
Success |
|
|
| 858 |
2019/10/06 20:42:38
|
Three is prime
|
coorde |
Success |
|
|
| 857 |
2019/10/06 20:42:03
|
Three is prime
|
okaduki |
Success |
|
|
| 856 |
2019/10/06 20:40:08
|
Two is not Three
|
yodvhskd |
Success |
|
|
| 855 |
2019/10/06 20:40:04
|
Two is not Three
|
kkob |
Success |
|
|
| 854 |
2019/10/06 20:35:36
|
Boolean-hole principle
|
coorde |
Success |
|
|
| 853 |
2019/10/06 20:34:40
|
Three is prime
|
yamarten |
Success |
|
|
| 852 |
2019/10/06 20:32:23
|
Two is not Three
|
hirosegolf |
Success |
|
|
| 851 |
2019/10/06 20:31:17
|
Iterated iteration
|
momohatt |
Success |
|
|
| 850 |
2019/10/06 20:27:29
|
Three is prime
|
pekempey |
Success |
|
|
| 849 |
2019/10/06 20:27:27
|
Iterated iteration
|
kaz |
Success |
|
|
| 848 |
2019/10/06 20:27:25
|
Iterated iteration
|
momohatt |
Rejected |
|
|
| 847 |
2019/10/06 20:26:17
|
Iterated iteration
|
momohatt |
Failure |
|
|
| 846 |
2019/10/06 20:22:25
|
Iterated iteration
|
kkob |
Success |
|
|
| 845 |
2019/10/06 20:19:44
|
Boolean-hole principle
|
yamarten |
Success |
|
|
| 844 |
2019/10/06 20:18:32
|
Three is prime
|
sorata |
Failure |
|
|
| 843 |
2019/10/06 20:15:31
|
Three is prime
|
yodvhskd |
Success |
|
|
| 842 |
2019/10/06 20:13:00
|
Three is prime
|
hirosegolf |
Success |
|
|
| 841 |
2019/10/06 20:10:59
|
Two is not Three
|
kaz |
Success |
|
|
| 840 |
2019/10/06 20:08:51
|
Three is prime
|
momohatt |
Success |
|
|
| 839 |
2019/10/06 20:07:03
|
Boolean-hole principle
|
yodvhskd |
Success |
|
|
| 838 |
2019/10/06 20:05:49
|
Boolean-hole principle
|
okaduki |
Success |
|
|
| 837 |
2019/10/06 20:04:41
|
Three is prime
|
kaz |
Success |
|
|
| 836 |
2019/10/06 20:02:27
|
Boolean-hole principle
|
kaz |
Success |
|
|
| 835 |
2019/10/06 20:02:00
|
Boolean-hole principle
|
sorata |
Failure |
|
|
| 834 |
2019/10/06 20:01:56
|
Three is prime
|
kkob |
Success |
|
|
| 833 |
2019/10/06 20:01:41
|
Boolean-hole principle
|
hirosegolf |
Success |
|
|
| 832 |
2019/10/06 20:01:15
|
Boolean-hole principle
|
momohatt |
Success |
|
|
| 831 |
2019/10/06 20:01:03
|
Boolean-hole principle
|
pekempey |
Success |
|
|
| 830 |
2019/10/06 20:00:50
|
Boolean-hole principle
|
kkob |
Success |
|
|
| 829 |
2019/10/05 14:01:43
|
Any natural number is expressible in binary notation
|
hirosegolf |
Success |
|
|
| 828 |
2019/10/05 11:43:31
|
unique (unique l) = l
|
hirosegolf |
Success |
|
|
| 827 |
2019/10/05 10:20:49
|
count l n = count (rev l) n
|
hirosegolf |
Success |
|
|
| 826 |
2019/10/05 10:19:14
|
count l n = count (rev l) n
|
hirosegolf |
Failure |
|
|
| 825 |
2019/10/05 10:18:20
|
count l n = count (rev l) n
|
hirosegolf |
Failure |
|
|
| 824 |
2019/10/05 09:13:55
|
gcd(n, n+1) = 1
|
hirosegolf |
Success |
|
|
| 823 |
2019/10/05 01:58:21
|
Multiplication in F_2 is idempotent
|
hirosegolf |
Success |
|
|
| 822 |
2019/10/05 01:08:07
|
Definitions of injectivity
|
hirosegolf |
Success |
|
|
| 821 |
2019/10/05 01:06:07
|
Definitions of injectivity
|
hirosegolf |
Failure |
|
|
| 820 |
2019/10/05 00:49:38
|
Summand of one
|
hirosegolf |
Success |
|
|
| 819 |
2019/10/05 00:46:51
|
Cumulative sum of list
|
hirosegolf |
Success |
|
|
| 818 |
2019/10/04 23:51:04
|
forall l: list nat, l @ [0] <> []
|
hirosegolf |
Success |
|
|
| 817 |
2019/10/04 23:39:24
|
n < m \/ n = m \/ n > m
|
hirosegolf |
Success |
|
|
| 816 |
2019/10/04 23:37:00
|
n * S m = n + n * m
|
hirosegolf |
Success |
|
|
| 815 |
2019/10/04 23:32:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
hirosegolf |
Success |
|
|
| 814 |
2019/10/04 23:17:23
|
1 + 1 = 2
|
hirosegolf |
Success |
|
|
| 813 |
2019/10/03 21:23:07
|
Iterated iteration
|
kozima |
Success |
|
|
| 812 |
2019/10/03 21:22:47
|
Two is not Three
|
kozima |
Success |
|
|
| 811 |
2019/10/03 21:22:23
|
Boolean-hole principle
|
kozima |
Success |
|
|
| 810 |
2019/10/03 21:22:11
|
Three is prime
|
kozima |
Success |
|
|
| 809 |
2019/10/03 21:20:52
|
Boolean-hole principle
|
kozima |
Failure |
|
|
| 808 |
2019/10/03 12:42:53
|
forall l: list nat, l @ [0] <> []
|
nikeya |
Success |
|
|
| 807 |
2019/10/03 12:20:28
|
mult_n_O
|
nikeya |
Success |
|
|
| 806 |
2019/10/03 12:18:21
|
De Morgan's laws in Coq
|
nikeya |
Success |
|
|
| 805 |
2019/10/02 18:16:50
|
1 + 1 = 2
|
nikeya |
Success |
|
|
| 804 |
2019/10/02 18:15:34
|
plus_comm
|
nikeya |
Success |
|
|
| 803 |
2019/10/02 18:14:45
|
plus_comm
|
nikeya |
Failure |
|
|
| 802 |
2019/10/02 17:24:14
|
plus_assoc
|
nikeya |
Success |
|
|
| 801 |
2019/10/01 02:53:35
|
plus_assoc
|
test |
Success |
|
|
| 800 |
2019/09/27 19:48:06
|
mult_n_O
|
yishibashi |
Success |
|
|
| 799 |
2019/09/27 19:21:56
|
n * S m = n + n * m
|
yishibashi |
Success |
|
|
| 798 |
2019/09/27 19:10:58
|
plus_comm
|
yishibashi |
Success |
|
|
| 797 |
2019/09/27 18:48:04
|
plus_assoc
|
yishibashi |
Success |
|
|
| 796 |
2019/09/27 18:24:22
|
Summand of one
|
yishibashi |
Success |
|
|
| 795 |
2019/09/26 13:40:51
|
unique (unique l) = l
|
coorde |
Success |
|
|
| 794 |
2019/09/26 13:38:55
|
unique (unique l) = l
|
coorde |
Failure |
|
|
| 793 |
2019/09/25 15:05:16
|
Any natural number is expressible in binary notation
|
kurgm |
Success |
|
|
| 792 |
2019/09/25 13:58:23
|
De Morgan's laws in Coq
|
kurgm |
Success |
|
|
| 791 |
2019/09/25 13:40:48
|
mult_n_O
|
kurgm |
Success |
|
|
| 790 |
2019/09/25 00:45:20
|
forall l: list nat, l @ [0] <> []
|
kkob |
Success |
|
|
| 789 |
2019/09/25 00:44:43
|
n < m \/ n = m \/ n > m
|
kkob |
Success |
|
|
| 788 |
2019/09/25 00:44:08
|
n * S m = n + n * m
|
kkob |
Success |
|
|
| 787 |
2019/09/25 00:42:54
|
forall f: bool -> bool, f^3(x) = f(x)
|
kkob |
Success |
|
|
| 786 |
2019/09/25 00:40:39
|
1 + 1 = 2
|
kkob |
Success |
|
|
| 785 |
2019/09/25 00:39:22
|
plus_comm
|
kkob |
Success |
|
|
| 784 |
2019/09/24 09:14:21
|
count l n = count (rev l) n
|
coorde |
Success |
|
|
| 783 |
2019/09/24 09:04:50
|
count l n = count (rev l) n
|
coorde |
Failure |
|
|
| 782 |
2019/09/24 08:48:07
|
gcd(n, n+1) = 1
|
coorde |
Success |
|
|
| 781 |
2019/09/23 14:52:40
|
forall f: bool -> bool, f^3(x) = f(x)
|
melan |
Success |
|
|
| 780 |
2019/09/23 12:55:30
|
De Morgan's laws in Coq
|
mkakh |
Success |
|
|
| 779 |
2019/09/23 04:26:51
|
Multiplication of non-zero value in F_p is injective
|
kkob |
Success |
|
|
| 778 |
2019/09/23 04:20:43
|
plus_assoc
|
kkob |
Success |
|
|
| 777 |
2019/09/23 04:20:40
|
plus_assoc
|
kkob |
Success |
|
|
| 776 |
2019/09/23 04:20:36
|
plus_assoc
|
kkob |
Success |
|
|
| 775 |
2019/09/23 04:20:28
|
plus_assoc
|
kkob |
Success |
|
|
| 774 |
2019/09/23 04:19:18
|
plus_assoc
|
kkob |
Success |
|
|
| 773 |
2019/09/23 04:18:55
|
plus_assoc
|
kkob |
Success |
|
|
| 772 |
2019/09/23 03:13:17
|
plus_assoc
|
kkob |
Success |
|
|
| 771 |
2019/09/23 03:02:18
|
plus_assoc
|
kkob |
Success |
|
|
| 770 |
2019/09/23 02:59:02
|
plus_assoc
|
kkob |
Success |
|
|
| 769 |
2019/09/23 02:50:15
|
plus_assoc
|
kkob |
Success |
|
|
| 768 |
2019/09/23 02:33:24
|
1 + 1 = 2
|
melan |
Success |
|
|
| 767 |
2019/09/23 02:32:20
|
1 + 1 = 2
|
melan |
Failure |
|
|
| 766 |
2019/09/23 00:17:36
|
mult_n_O
|
kozima |
Success |
|
|
| 765 |
2019/09/23 00:00:10
|
Multiplication of non-zero value in F_p is injective
|
muratak |
Success |
|
|
| 764 |
2019/09/22 23:59:21
|
Multiplication of non-zero value in F_p is injective
|
muratak |
Failure |
|
|
| 763 |
2019/09/22 22:37:07
|
Multiplication of non-zero value in F_p is injective
|
kkob |
Success |
|
|
| 762 |
2019/09/22 22:01:31
|
Multiplication of non-zero value in F_p is injective
|
prime |
Success |
|
|
| 761 |
2019/09/22 21:56:45
|
Multiplication of non-zero value in F_p is injective
|
drafear |
Failure |
|
|
| 760 |
2019/09/22 21:56:02
|
Multiplication of non-zero value in F_p is injective
|
pekempey |
Success |
|
|
| 759 |
2019/09/22 21:54:35
|
De Morgan's laws in Coq
|
mkakh |
Rejected |
|
|
| 758 |
2019/09/22 21:49:06
|
Any natural number is expressible in binary notation
|
spica314 |
Success |
|
|
| 757 |
2019/09/22 21:47:16
|
Any natural number is expressible in binary notation
|
yamarten |
Success |
|
|
| 756 |
2019/09/22 21:46:21
|
Any natural number is expressible in binary notation
|
muratak |
Success |
|
|
| 755 |
2019/09/22 21:46:10
|
Any natural number is expressible in binary notation
|
yamarten |
Failure |
|
|
| 754 |
2019/09/22 21:45:42
|
Any natural number is expressible in binary notation
|
muratak |
Failure |
|
|
| 753 |
2019/09/22 21:44:59
|
Any natural number is expressible in binary notation
|
muratak |
Failure |
|
|
| 752 |
2019/09/22 21:35:06
|
Any natural number is expressible in binary notation
|
efk |
Success |
|
|
| 751 |
2019/09/22 21:24:50
|
De Morgan's laws in Coq
|
Haar |
Success |
|
|
| 750 |
2019/09/22 21:17:12
|
Any natural number is expressible in binary notation
|
wass88 |
Success |
|
|
| 749 |
2019/09/22 21:16:40
|
Any natural number is expressible in binary notation
|
wass88 |
Failure |
|
|
| 748 |
2019/09/22 21:13:42
|
Any natural number is expressible in binary notation
|
taisei |
Success |
|
|
| 747 |
2019/09/22 21:12:05
|
Any natural number is expressible in binary notation
|
wass88 |
Failure |
|
|
| 746 |
2019/09/22 21:10:58
|
Any natural number is expressible in binary notation
|
wass88 |
Failure |
|
|
| 745 |
2019/09/22 21:08:06
|
Any natural number is expressible in binary notation
|
taisei |
Failure |
|
|
| 744 |
2019/09/22 21:06:37
|
Any natural number is expressible in binary notation
|
prime |
Success |
|
|
| 743 |
2019/09/22 21:06:10
|
De Morgan's laws in Coq
|
minaminao |
Success |
|
|
| 742 |
2019/09/22 21:05:27
|
Any natural number is expressible in binary notation
|
taisei |
Failure |
|
|
| 741 |
2019/09/22 21:04:28
|
De Morgan's laws in Coq
|
minaminao |
Rejected |
|
|
| 740 |
2019/09/22 21:03:14
|
Any natural number is expressible in binary notation
|
taisei |
Failure |
|
|
| 739 |
2019/09/22 21:02:29
|
Multiplication of non-zero value in F_p is injective
|
sorata |
Success |
|
|
| 738 |
2019/09/22 20:59:35
|
Any natural number is expressible in binary notation
|
taisei |
Failure |
|
|
| 737 |
2019/09/22 20:55:34
|
De Morgan's laws in Coq
|
Haar |
Rejected |
|
|
| 736 |
2019/09/22 20:53:08
|
De Morgan's laws in Coq
|
mkakh |
Rejected |
|
|
| 735 |
2019/09/22 20:48:03
|
De Morgan's laws in Coq
|
okaduki |
Success |
|
|
| 734 |
2019/09/22 20:46:14
|
Any natural number is expressible in binary notation
|
kaz |
Success |
|
|
| 733 |
2019/09/22 20:45:54
|
Multiplication of non-zero value in F_p is injective
|
kozima |
Success |
|
|
| 732 |
2019/09/22 20:45:21
|
mult_n_O
|
minaminao |
Success |
|
|
| 731 |
2019/09/22 20:42:52
|
De Morgan's laws in Coq
|
okaduki |
Rejected |
|
|
| 730 |
2019/09/22 20:39:55
|
Any natural number is expressible in binary notation
|
coorde |
Success |
|
|
| 729 |
2019/09/22 20:36:34
|
Any natural number is expressible in binary notation
|
pekempey |
Success |
|
|
| 728 |
2019/09/22 20:34:50
|
Any natural number is expressible in binary notation
|
pekempey |
Failure |
|
|
| 727 |
2019/09/22 20:34:24
|
Any natural number is expressible in binary notation
|
drafear |
Success |
|
|
| 726 |
2019/09/22 20:32:58
|
Multiplication of non-zero value in F_p is injective
|
kkob |
Success |
|
|
| 725 |
2019/09/22 20:32:37
|
Any natural number is expressible in binary notation
|
pekempey |
Failure |
|
|
| 724 |
2019/09/22 20:30:10
|
Any natural number is expressible in binary notation
|
drafear |
Failure |
|
|
| 723 |
2019/09/22 20:25:52
|
Any natural number is expressible in binary notation
|
sorata |
Success |
|
|
| 722 |
2019/09/22 20:24:48
|
De Morgan's laws in Coq
|
coorde |
Success |
|
|
| 721 |
2019/09/22 20:24:44
|
De Morgan's laws in Coq
|
mttm |
Success |
|
|
| 720 |
2019/09/22 20:24:35
|
De Morgan's laws in Coq
|
prime |
Success |
|
|
| 719 |
2019/09/22 20:24:29
|
mult_n_O
|
okaduki |
Success |
|
|
| 718 |
2019/09/22 20:24:22
|
De Morgan's laws in Coq
|
kaz |
Success |
|
|
| 717 |
2019/09/22 20:24:21
|
mult_n_O
|
kaz |
Success |
|
|
| 716 |
2019/09/22 20:22:37
|
De Morgan's laws in Coq
|
drafear |
Success |
|
|
| 715 |
2019/09/22 20:20:25
|
De Morgan's laws in Coq
|
efk |
Success |
|
|
| 714 |
2019/09/22 20:20:23
|
De Morgan's laws in Coq
|
wass88 |
Success |
|
|
| 713 |
2019/09/22 20:19:12
|
Any natural number is expressible in binary notation
|
drafear |
Failure |
|
|
| 712 |
2019/09/22 20:18:25
|
Any natural number is expressible in binary notation
|
kkob |
Success |
|
|
| 711 |
2019/09/22 20:15:35
|
De Morgan's laws in Coq
|
spica314 |
Success |
|
|
| 710 |
2019/09/22 20:13:32
|
De Morgan's laws in Coq
|
cympfh |
Success |
|
|
| 709 |
2019/09/22 20:12:54
|
Any natural number is expressible in binary notation
|
kozima |
Success |
|
|
| 708 |
2019/09/22 20:11:41
|
mult_n_O
|
coorde |
Success |
|
|
| 707 |
2019/09/22 20:11:15
|
mult_n_O
|
mttm |
Success |
|
|
| 706 |
2019/09/22 20:11:00
|
De Morgan's laws in Coq
|
yamarten |
Success |
|
|
| 705 |
2019/09/22 20:10:38
|
mult_n_O
|
efk |
Success |
|
|
| 704 |
2019/09/22 20:10:05
|
De Morgan's laws in Coq
|
drafear |
Rejected |
|
|
| 703 |
2019/09/22 20:09:57
|
mult_n_O
|
wass88 |
Success |
|
|
| 702 |
2019/09/22 20:09:28
|
Any natural number is expressible in binary notation
|
drafear |
Failure |
|
|
| 701 |
2019/09/22 20:09:13
|
De Morgan's laws in Coq
|
taisei |
Success |
|
|
| 700 |
2019/09/22 20:09:02
|
De Morgan's laws in Coq
|
sorata |
Success |
|
|
| 699 |
2019/09/22 20:05:48
|
De Morgan's laws in Coq
|
muratak |
Success |
|
|
| 698 |
2019/09/22 20:05:37
|
De Morgan's laws in Coq
|
pekempey |
Success |
|
|
| 697 |
2019/09/22 20:05:32
|
mult_n_O
|
drafear |
Success |
|
|
| 696 |
2019/09/22 20:04:10
|
mult_n_O
|
Haar |
Success |
|
|
| 695 |
2019/09/22 20:03:31
|
De Morgan's laws in Coq
|
kkob |
Success |
|
|
| 694 |
2019/09/22 20:03:19
|
mult_n_O
|
taisei |
Success |
|
|
| 693 |
2019/09/22 20:02:57
|
mult_n_O
|
sorata |
Success |
|
|
| 692 |
2019/09/22 20:02:46
|
De Morgan's laws in Coq
|
kozima |
Success |
|
|
| 691 |
2019/09/22 20:02:37
|
mult_n_O
|
yamarten |
Success |
|
|
| 690 |
2019/09/22 20:02:09
|
mult_n_O
|
cympfh |
Success |
|
|
| 689 |
2019/09/22 20:01:22
|
mult_n_O
|
kozima |
Success |
|
|
| 688 |
2019/09/22 20:01:21
|
mult_n_O
|
spica314 |
Success |
|
|
| 687 |
2019/09/22 20:01:19
|
mult_n_O
|
kkob |
Success |
|
|
| 686 |
2019/09/22 20:01:13
|
mult_n_O
|
prime |
Success |
|
|
| 685 |
2019/09/22 20:01:08
|
mult_n_O
|
mkakh |
Success |
|
|
| 684 |
2019/09/22 20:01:06
|
mult_n_O
|
muratak |
Success |
|
|
| 683 |
2019/09/22 20:00:52
|
mult_n_O
|
cympfh |
Failure |
|
|
| 682 |
2019/09/22 20:00:27
|
mult_n_O
|
pekempey |
Success |
|
|
| 681 |
2019/09/22 14:19:13
|
Multiplication of non-zero value in F_p is injective
|
kimiyuki |
Success |
|
|
| 680 |
2019/09/22 14:17:48
|
Any natural number is expressible in binary notation
|
kimiyuki |
Success |
|
|
| 679 |
2019/09/22 14:15:39
|
De Morgan's laws in Coq
|
kimiyuki |
Success |
|
|
| 678 |
2019/09/22 14:13:25
|
De Morgan's laws in Coq
|
kimiyuki |
Failure |
|
|
| 677 |
2019/09/22 14:11:29
|
mult_n_O
|
kimiyuki |
Success |
|
|
| 676 |
2019/09/22 04:46:50
|
plus_assoc
|
kivantium |
Success |
|
|
| 675 |
2019/09/21 17:08:01
|
forall l: list nat, l @ [0] <> []
|
mkakh |
Success |
|
|
| 674 |
2019/09/21 00:40:22
|
unique count
|
okaduki |
Success |
|
|
| 673 |
2019/09/20 22:14:26
|
n < m \/ n = m \/ n > m
|
anqou |
Success |
|
|
| 672 |
2019/09/20 19:40:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
mkakh |
Success |
|
|
| 671 |
2019/09/20 19:27:55
|
n * S m = n + n * m
|
mkakh |
Success |
|
|
| 670 |
2019/09/20 19:17:30
|
n < m \/ n = m \/ n > m
|
mkakh |
Success |
|
|
| 669 |
2019/09/20 18:31:36
|
unique (unique l) = l
|
mkakh |
Failure |
|
|
| 668 |
2019/09/20 17:29:43
|
plus_assoc
|
mkakh |
Success |
|
|
| 667 |
2019/09/20 17:25:12
|
plus_assoc
|
mkakh |
Failure |
|
|
| 666 |
2019/09/20 16:59:39
|
plus_comm
|
mkakh |
Success |
|
|
| 665 |
2019/09/20 16:36:02
|
1 + 1 = 2
|
mkakh |
Success |
|
|
| 664 |
2019/09/20 16:33:45
|
gcd(n, n+1) = 1
|
mkakh |
Success |
|
|
| 663 |
2019/09/20 12:42:03
|
n * S m = n + n * m
|
anqou |
Success |
|
|
| 662 |
2019/09/20 02:44:25
|
unique (unique l) = l
|
okaduki |
Success |
|
|
| 661 |
2019/09/20 00:43:05
|
1 + 1 = 2
|
hiromi_mi |
Success |
|
|
| 660 |
2019/09/20 00:09:21
|
forall f: bool -> bool, f^3(x) = f(x)
|
anqou |
Success |
|
|
| 659 |
2019/09/19 23:54:47
|
1 + 1 = 2
|
anqou |
Success |
|
|
| 658 |
2019/09/19 20:14:12
|
n * S m = n + n * m
|
youjotape |
Success |
|
|
| 657 |
2019/09/19 19:22:45
|
forall f: bool -> bool, f^3(x) = f(x)
|
youjotape |
Success |
|
|
| 656 |
2019/09/19 15:27:11
|
1 + 1 = 2
|
youjotape |
Success |
|
|
| 655 |
2019/09/19 15:00:40
|
plus_comm
|
youjotape |
Success |
|
|
| 654 |
2019/09/19 14:52:55
|
plus_assoc
|
youjotape |
Success |
|
|
| 653 |
2019/09/19 10:02:12
|
plus_assoc
|
stretchybox |
Success |
|
|
| 652 |
2019/09/18 22:41:18
|
plus_comm
|
stretchybox |
Success |
|
|
| 651 |
2019/09/18 22:40:54
|
plus_comm
|
stretchybox |
Success |
|
|
| 650 |
2019/09/18 22:33:54
|
plus_assoc
|
stretchybox |
Success |
|
|
| 649 |
2019/09/18 19:54:27
|
Cumulative sum of list
|
spica314 |
Success |
|
|
| 648 |
2019/09/18 15:35:28
|
unique count
|
spica314 |
Success |
|
|
| 647 |
2019/09/18 15:33:48
|
unique count
|
spica314 |
Success |
|
|
| 646 |
2019/09/18 14:41:50
|
unique (unique l) = l
|
spica314 |
Success |
|
|
| 645 |
2019/09/18 02:02:04
|
unique count
|
kimiyuki |
Success |
|
|
| 644 |
2019/09/18 01:33:41
|
unique (unique l) = l
|
kimiyuki |
Success |
|
|
| 643 |
2019/09/18 00:33:37
|
count l n = count (rev l) n
|
kimiyuki |
Success |
|
|
| 642 |
2019/09/18 00:12:13
|
gcd(n, n+1) = 1
|
kimiyuki |
Success |
|
|
| 641 |
2019/09/17 22:51:30
|
unique count
|
yodvhskd |
Success |
|
|
| 640 |
2019/09/17 22:07:57
|
unique (unique l) = l
|
yodvhskd |
Success |
|
|
| 639 |
2019/09/17 20:16:52
|
gcd(n, n+1) = 1
|
a_happin |
Success |
|
|
| 638 |
2019/09/17 20:15:21
|
gcd(n, n+1) = 1
|
a_happin |
Failure |
|
|
| 637 |
2019/09/17 19:57:59
|
Summand of one
|
a_happin |
Success |
|
|
| 636 |
2019/09/17 16:24:56
|
unique count
|
cympfh |
Success |
|
|
| 635 |
2019/09/17 00:38:09
|
count l n = count (rev l) n
|
yodvhskd |
Success |
|
|
| 634 |
2019/09/17 00:16:08
|
gcd(n, n+1) = 1
|
yodvhskd |
Success |
|
|
| 633 |
2019/09/16 20:48:40
|
forall l: list nat, l @ [0] <> []
|
efk |
Success |
|
|
| 632 |
2019/09/16 18:18:07
|
n < m \/ n = m \/ n > m
|
efk |
Success |
|
|
| 631 |
2019/09/16 18:17:00
|
n * S m = n + n * m
|
efk |
Success |
|
|
| 630 |
2019/09/16 18:15:49
|
forall f: bool -> bool, f^3(x) = f(x)
|
efk |
Success |
|
|
| 629 |
2019/09/16 17:56:17
|
plus_comm
|
efk |
Success |
|
|
| 628 |
2019/09/16 17:55:38
|
1 + 1 = 2
|
efk |
Success |
|
|
| 627 |
2019/09/16 17:53:50
|
plus_comm
|
efk |
Failure |
|
|
| 626 |
2019/09/16 17:52:06
|
plus_assoc
|
efk |
Success |
|
|
| 625 |
2019/09/16 17:32:11
|
Grand Garden
|
sorata |
Success |
|
|
| 624 |
2019/09/16 14:32:21
|
gcd(n, n+1) = 1
|
efk |
Success |
|
|
| 623 |
2019/09/16 03:32:48
|
Multiplication in F_2 is idempotent
|
taisei |
Success |
|
|
| 622 |
2019/09/16 01:15:23
|
Grand Garden
|
kkob |
Success |
|
|
| 621 |
2019/09/16 00:47:52
|
Grand Garden
|
kkob |
Rejected |
|
|
| 620 |
2019/09/15 23:11:09
|
unique (unique l) = l
|
kurgm |
Success |
|
|
| 619 |
2019/09/15 23:10:44
|
unique (unique l) = l
|
kurgm |
Failure |
|
|
| 618 |
2019/09/15 22:39:39
|
Grand Garden
|
kozima |
Success |
|
|
| 617 |
2019/09/15 22:37:50
|
unique count
|
mttm |
Success |
|
|
| 616 |
2019/09/15 22:02:07
|
count l n = count (rev l) n
|
kurgm |
Success |
|
|
| 615 |
2019/09/15 22:01:31
|
gcd(n, n+1) = 1
|
minaminao |
Success |
|
|
| 614 |
2019/09/15 22:01:23
|
count l n = count (rev l) n
|
kurgm |
Failure |
|
|
| 613 |
2019/09/15 22:00:55
|
gcd(n, n+1) = 1
|
minaminao |
Failure |
|
|
| 612 |
2019/09/15 21:44:49
|
gcd(n, n+1) = 1
|
kurgm |
Success |
|
|
| 611 |
2019/09/15 19:15:21
|
count l n = count (rev l) n
|
yishibashi |
Success |
|
|
| 610 |
2019/09/15 19:12:46
|
gcd(n, n+1) = 1
|
cympfh |
Success |
|
|
| 609 |
2019/09/15 19:07:29
|
unique (unique l) = l
|
efk |
Success |
|
|
| 608 |
2019/09/15 18:59:21
|
unique (unique l) = l
|
mttm |
Success |
|
|
| 607 |
2019/09/15 18:57:06
|
unique (unique l) = l
|
cympfh |
Success |
|
|
| 606 |
2019/09/15 18:40:52
|
unique (unique l) = l
|
yamarten |
Success |
|
|
| 605 |
2019/09/15 18:40:21
|
count l n = count (rev l) n
|
yamarten |
Success |
|
|
| 604 |
2019/09/15 18:39:00
|
unique count
|
pekempey |
Success |
|
|
| 603 |
2019/09/15 18:38:55
|
unique (unique l) = l
|
yamarten |
Failure |
|
|
| 602 |
2019/09/15 18:37:22
|
Grand Garden
|
kozima |
Success |
|
|
| 601 |
2019/09/15 18:36:41
|
unique count
|
prime |
Success |
|
|
| 600 |
2019/09/15 18:20:18
|
count l n = count (rev l) n
|
yamarten |
Failure |
|
|
| 599 |
2019/09/15 18:10:24
|
unique (unique l) = l
|
pekempey |
Success |
|
|
| 598 |
2019/09/15 18:09:33
|
count l n = count (rev l) n
|
mttm |
Success |
|
|
| 597 |
2019/09/15 18:01:23
|
count l n = count (rev l) n
|
okaduki |
Success |
|
|
| 596 |
2019/09/15 17:58:09
|
unique count
|
sorata |
Success |
|
|
| 595 |
2019/09/15 17:57:32
|
count l n = count (rev l) n
|
spica314 |
Success |
|
|
| 594 |
2019/09/15 17:56:06
|
count l n = count (rev l) n
|
cympfh |
Success |
|
|
| 593 |
2019/09/15 17:45:39
|
gcd(n, n+1) = 1
|
yamarten |
Success |
|
|
| 592 |
2019/09/15 17:44:42
|
gcd(n, n+1) = 1
|
yamarten |
Failure |
|
|
| 591 |
2019/09/15 17:44:15
|
gcd(n, n+1) = 1
|
yishibashi |
Success |
|
|
| 590 |
2019/09/15 17:44:01
|
count l n = count (rev l) n
|
yishibashi |
Failure |
|
|
| 589 |
2019/09/15 17:36:32
|
gcd(n, n+1) = 1
|
cympfh |
Success |
|
|
| 588 |
2019/09/15 17:35:47
|
unique (unique l) = l
|
sorata |
Success |
|
|
| 587 |
2019/09/15 17:35:45
|
unique count
|
kozima |
Success |
|
|
| 586 |
2019/09/15 17:35:43
|
gcd(n, n+1) = 1
|
cympfh |
Failure |
|
|
| 585 |
2019/09/15 17:33:43
|
gcd(n, n+1) = 1
|
cympfh |
Failure |
|
|
| 584 |
2019/09/15 17:28:50
|
unique (unique l) = l
|
prime |
Success |
|
|
| 583 |
2019/09/15 17:26:48
|
unique count
|
kkob |
Success |
|
|
| 582 |
2019/09/15 17:26:40
|
gcd(n, n+1) = 1
|
okaduki |
Success |
|
|
| 581 |
2019/09/15 17:24:55
|
gcd(n, n+1) = 1
|
mttm |
Success |
|
|
| 580 |
2019/09/15 17:23:16
|
unique (unique l) = l
|
kkob |
Success |
|
|
| 579 |
2019/09/15 17:22:52
|
unique (unique l) = l
|
kozima |
Success |
|
|
| 578 |
2019/09/15 17:21:49
|
count l n = count (rev l) n
|
pekempey |
Success |
|
|
| 577 |
2019/09/15 17:20:27
|
count l n = count (rev l) n
|
sorata |
Success |
|
|
| 576 |
2019/09/15 17:19:57
|
count l n = count (rev l) n
|
pekempey |
Failure |
|
|
| 575 |
2019/09/15 17:18:50
|
count l n = count (rev l) n
|
sorata |
Failure |
|
|
| 574 |
2019/09/15 17:15:29
|
count l n = count (rev l) n
|
prime |
Success |
|
|
| 573 |
2019/09/15 17:14:44
|
gcd(n, n+1) = 1
|
spica314 |
Success |
|
|
| 572 |
2019/09/15 17:13:56
|
count l n = count (rev l) n
|
kkob |
Success |
|
|
| 571 |
2019/09/15 17:12:22
|
count l n = count (rev l) n
|
kozima |
Success |
|
|
| 570 |
2019/09/15 17:06:42
|
gcd(n, n+1) = 1
|
sorata |
Success |
|
|
| 569 |
2019/09/15 17:06:29
|
gcd(n, n+1) = 1
|
kkob |
Success |
|
|
| 568 |
2019/09/15 17:06:16
|
gcd(n, n+1) = 1
|
pekempey |
Success |
|
|
| 567 |
2019/09/15 17:05:53
|
gcd(n, n+1) = 1
|
pekempey |
Failure |
|
|
| 566 |
2019/09/15 17:05:51
|
gcd(n, n+1) = 1
|
prime |
Success |
|
|
| 565 |
2019/09/15 17:05:37
|
gcd(n, n+1) = 1
|
sorata |
Failure |
|
|
| 564 |
2019/09/15 17:04:35
|
gcd(n, n+1) = 1
|
pekempey |
Failure |
|
|
| 563 |
2019/09/15 17:03:52
|
gcd(n, n+1) = 1
|
kozima |
Success |
|
|
| 562 |
2019/09/15 16:53:52
|
Multiplication in F_2 is idempotent
|
spica314 |
Success |
|
|
| 561 |
2019/09/15 16:35:29
|
1 + 1 = 2
|
asi1024 |
Success |
|
|
| 560 |
2019/09/14 21:51:35
|
Equivalent two quicksorts
|
kozima |
Success |
|
|
| 559 |
2019/09/14 20:37:23
|
Cumulative sum of list
|
yamarten |
Success |
|
|
| 558 |
2019/09/14 20:34:38
|
Cumulative sum of list
|
yamarten |
Rejected |
|
|
| 557 |
2019/09/14 16:33:21
|
Grand Garden
|
drafear |
Success |
|
|
| 556 |
2019/09/14 16:33:00
|
unique count
|
drafear |
Success |
|
|
| 555 |
2019/09/14 16:32:40
|
unique (unique l) = l
|
drafear |
Success |
|
|
| 554 |
2019/09/14 16:32:20
|
count l n = count (rev l) n
|
drafear |
Success |
|
|
| 553 |
2019/09/14 16:31:57
|
gcd(n, n+1) = 1
|
drafear |
Success |
|
|
| 552 |
2019/09/14 02:56:26
|
Equivalent two quicksorts
|
kkob |
Success |
|
|
| 551 |
2019/09/14 02:54:55
|
Equivalent two quicksorts
|
kkob |
Failure |
|
|
| 550 |
2019/09/13 22:59:28
|
forall l: list nat, l @ [0] <> []
|
minaminao |
Success |
|
|
| 549 |
2019/09/13 22:21:16
|
n * S m = n + n * m
|
minaminao |
Success |
|
|
| 548 |
2019/09/13 22:02:40
|
forall f: bool -> bool, f^3(x) = f(x)
|
minaminao |
Success |
|
|
| 547 |
2019/09/13 21:04:14
|
Summand of one
|
minaminao |
Success |
|
|
| 546 |
2019/09/13 20:33:59
|
1 + 1 = 2
|
minaminao |
Success |
|
|
| 545 |
2019/09/13 20:33:01
|
plus_comm
|
minaminao |
Success |
|
|
| 544 |
2019/09/13 18:00:23
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 543 |
2019/09/13 17:57:53
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 542 |
2019/09/12 23:11:18
|
plus_assoc
|
minaminao |
Success |
|
|
| 541 |
2019/09/12 20:48:27
|
n * S m = n + n * m
|
egashira |
Success |
|
|
| 540 |
2019/09/12 20:30:48
|
plus_comm
|
egashira |
Success |
|
|
| 539 |
2019/09/12 20:25:40
|
plus_assoc
|
egashira |
Success |
|
|
| 538 |
2019/09/12 20:22:52
|
1 + 1 = 2
|
egashira |
Success |
|
|
| 537 |
2019/09/11 21:30:07
|
1 + 1 = 2
|
skwbc |
Success |
|
|
| 536 |
2019/09/10 07:43:52
|
n * S m = n + n * m
|
Haar |
Success |
|
|
| 535 |
2019/09/10 07:36:07
|
forall f: bool -> bool, f^3(x) = f(x)
|
Haar |
Success |
|
|
| 534 |
2019/09/09 18:37:57
|
Identity permutation
|
cympfh |
Success |
|
|
| 533 |
2019/09/09 17:39:14
|
l1 <> l2 if l2 is an odd permutation of l1
|
okaduki |
Success |
|
|
| 532 |
2019/09/09 10:21:58
|
1 + 1 = 2
|
Haar |
Success |
|
|
| 531 |
2019/09/09 10:15:42
|
plus_comm
|
Haar |
Success |
|
|
| 530 |
2019/09/09 10:09:50
|
plus_assoc
|
Haar |
Success |
|
|
| 529 |
2019/09/09 01:28:34
|
Definitions of injectivity
|
spica314 |
Success |
|
|
| 528 |
2019/09/09 00:42:39
|
Cumulative sum of list
|
coorde |
Success |
|
|
| 527 |
2019/09/09 00:36:30
|
Cumulative sum of list
|
kurgm |
Success |
|
|
| 526 |
2019/09/09 00:25:06
|
Definitions of injectivity
|
coorde |
Success |
|
|
| 525 |
2019/09/09 00:19:57
|
plus_assoc
|
spica314 |
Success |
|
|
| 524 |
2019/09/09 00:14:07
|
forall l: list nat, l @ [0] <> []
|
kurgm |
Success |
|
|
| 523 |
2019/09/09 00:02:45
|
Multiplication in F_2 is idempotent
|
coorde |
Success |
|
|
| 522 |
2019/09/09 00:02:22
|
Identity permutation
|
taisei |
Success |
|
|
| 521 |
2019/09/08 23:48:44
|
Multiplication in F_2 is idempotent
|
kurgm |
Success |
|
|
| 520 |
2019/09/08 23:35:28
|
Multiplication in F_2 is idempotent
|
cympfh |
Success |
|
|
| 519 |
2019/09/08 23:30:05
|
Identity permutation
|
okaduki |
Success |
|
|
| 518 |
2019/09/08 23:12:17
|
Identity permutation
|
okaduki |
Success |
|
|
| 517 |
2019/09/08 22:51:49
|
Identity permutation
|
koba |
Success |
|
|
| 516 |
2019/09/08 22:49:39
|
Definitions of injectivity
|
kurgm |
Success |
|
|
| 515 |
2019/09/08 22:34:34
|
Identity permutation
|
kkob |
Success |
|
|
| 514 |
2019/09/08 22:26:18
|
Multiplication in F_2 is idempotent
|
koba |
Success |
|
|
| 513 |
2019/09/08 22:17:51
|
Identity permutation
|
kkob |
Success |
|
|
| 512 |
2019/09/08 22:15:20
|
Definitions of injectivity
|
koba |
Success |
|
|
| 511 |
2019/09/08 22:10:57
|
Definitions of injectivity
|
spica314 |
Rejected |
|
|
| 510 |
2019/09/08 22:06:45
|
Multiplication in F_2 is idempotent
|
prime |
Success |
|
|
| 509 |
2019/09/08 22:03:37
|
Multiplication in F_2 is idempotent
|
efk |
Success |
|
|
| 508 |
2019/09/08 22:00:03
|
Summand of one
|
koba |
Success |
|
|
| 507 |
2019/09/08 21:59:21
|
Identity permutation
|
kkob |
Success |
|
|
| 506 |
2019/09/08 21:52:23
|
Definitions of injectivity
|
spica314 |
Rejected |
|
|
| 505 |
2019/09/08 21:47:13
|
Summand of one
|
kurgm |
Success |
|
|
| 504 |
2019/09/08 21:39:55
|
Identity permutation
|
mttm |
Success |
|
|
| 503 |
2019/09/08 21:34:09
|
Definitions of injectivity
|
okaduki |
Success |
|
|
| 502 |
2019/09/08 21:28:09
|
Definitions of injectivity
|
yamarten |
Success |
|
|
| 501 |
2019/09/08 21:25:31
|
Identity permutation
|
muratak |
Success |
|
|
| 500 |
2019/09/08 21:25:05
|
Identity permutation
|
muratak |
Failure |
|
|
| 499 |
2019/09/08 21:24:25
|
Identity permutation
|
muratak |
Failure |
|
|
| 498 |
2019/09/08 21:12:32
|
Summand of one
|
yamarten |
Success |
|
|
| 497 |
2019/09/08 21:10:48
|
Identity permutation
|
drafear |
Success |
|
|
| 496 |
2019/09/08 21:10:31
|
Identity permutation
|
drafear |
Success |
|
|
| 495 |
2019/09/08 21:10:18
|
Identity permutation
|
kimiyuki |
Success |
|
|
| 494 |
2019/09/08 21:09:02
|
Definitions of injectivity
|
efk |
Success |
|
|
| 493 |
2019/09/08 21:08:04
|
Definitions of injectivity
|
efk |
Failure |
|
|
| 492 |
2019/09/08 21:07:35
|
Multiplication in F_2 is idempotent
|
okaduki |
Success |
|
|
| 491 |
2019/09/08 20:55:08
|
Multiplication in F_2 is idempotent
|
drafear |
Success |
|
|
| 490 |
2019/09/08 20:54:17
|
Identity permutation
|
satos |
Success |
|
|
| 489 |
2019/09/08 20:52:05
|
Identity permutation
|
pekempey |
Success |
|
|
| 488 |
2019/09/08 20:51:22
|
Definitions of injectivity
|
cympfh |
Success |
|
|
| 487 |
2019/09/08 20:47:35
|
Identity permutation
|
sorata |
Success |
|
|
| 486 |
2019/09/08 20:45:16
|
Identity permutation
|
sorata |
Failure |
|
|
| 485 |
2019/09/08 20:43:39
|
Multiplication in F_2 is idempotent
|
kimiyuki |
Success |
|
|
| 484 |
2019/09/08 20:36:35
|
Multiplication in F_2 is idempotent
|
satos |
Success |
|
|
| 483 |
2019/09/08 20:35:30
|
Multiplication in F_2 is idempotent
|
muratak |
Success |
|
|
| 482 |
2019/09/08 20:31:57
|
Definitions of injectivity
|
drafear |
Success |
|
|
| 481 |
2019/09/08 20:25:47
|
Identity permutation
|
kaz |
Success |
|
|
| 480 |
2019/09/08 20:25:46
|
Multiplication in F_2 is idempotent
|
sorata |
Success |
|
|
| 479 |
2019/09/08 20:25:16
|
Summand of one
|
siotouto |
Success |
|
|
| 478 |
2019/09/08 20:24:41
|
Multiplication in F_2 is idempotent
|
pekempey |
Success |
|
|
| 477 |
2019/09/08 20:24:19
|
Summand of one
|
efk |
Success |
|
|
| 476 |
2019/09/08 20:20:41
|
Summand of one
|
spica314 |
Success |
|
|
| 475 |
2019/09/08 20:18:29
|
Summand of one
|
coorde |
Success |
|
|
| 474 |
2019/09/08 20:17:04
|
Summand of one
|
coorde |
Failure |
|
|
| 473 |
2019/09/08 20:15:34
|
Multiplication in F_2 is idempotent
|
kaz |
Success |
|
|
| 472 |
2019/09/08 20:14:54
|
Definitions of injectivity
|
sorata |
Success |
|
|
| 471 |
2019/09/08 20:12:59
|
Definitions of injectivity
|
sorata |
Failure |
|
|
| 470 |
2019/09/08 20:12:52
|
Definitions of injectivity
|
kkob |
Success |
|
|
| 469 |
2019/09/08 20:11:41
|
Definitions of injectivity
|
kimiyuki |
Success |
|
|
| 468 |
2019/09/08 20:11:06
|
Definitions of injectivity
|
muratak |
Success |
|
|
| 467 |
2019/09/08 20:10:30
|
Definitions of injectivity
|
satos |
Success |
|
|
| 466 |
2019/09/08 20:09:51
|
Summand of one
|
prime |
Success |
|
|
| 465 |
2019/09/08 20:08:16
|
Summand of one
|
cympfh |
Success |
|
|
| 464 |
2019/09/08 20:08:07
|
Multiplication in F_2 is idempotent
|
kkob |
Success |
|
|
| 463 |
2019/09/08 20:07:04
|
Definitions of injectivity
|
pekempey |
Success |
|
|
| 462 |
2019/09/08 20:06:49
|
Definitions of injectivity
|
kaz |
Success |
|
|
| 461 |
2019/09/08 20:05:37
|
Summand of one
|
sorata |
Success |
|
|
| 460 |
2019/09/08 20:03:37
|
Summand of one
|
kimiyuki |
Success |
|
|
| 459 |
2019/09/08 20:02:56
|
Summand of one
|
drafear |
Success |
|
|
| 458 |
2019/09/08 20:02:54
|
Summand of one
|
okaduki |
Success |
|
|
| 457 |
2019/09/08 20:02:29
|
Summand of one
|
satos |
Success |
|
|
| 456 |
2019/09/08 20:01:23
|
Summand of one
|
kkob |
Success |
|
|
| 455 |
2019/09/08 20:01:20
|
Summand of one
|
kaz |
Success |
|
|
| 454 |
2019/09/08 20:01:17
|
Summand of one
|
muratak |
Success |
|
|
| 453 |
2019/09/08 20:00:44
|
Summand of one
|
pekempey |
Success |
|
|
| 452 |
2019/09/08 18:22:29
|
Identity permutation
|
kozima |
Success |
|
|
| 451 |
2019/09/08 18:22:07
|
Multiplication in F_2 is idempotent
|
kozima |
Success |
|
|
| 450 |
2019/09/08 18:21:27
|
Definitions of injectivity
|
kozima |
Success |
|
|
| 449 |
2019/09/08 18:20:38
|
Summand of one
|
kozima |
Success |
|
|
| 448 |
2019/09/05 01:14:15
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 447 |
2019/09/03 20:55:59
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Success |
|
|
| 446 |
2019/09/03 20:51:57
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Success |
|
|
| 445 |
2019/09/03 20:43:18
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Failure |
|
|
| 444 |
2019/09/03 20:36:23
|
1 + 1 = 2
|
cympfh |
Success |
|
|
| 443 |
2019/09/03 20:35:22
|
plus_comm
|
cympfh |
Success |
|
|
| 442 |
2019/09/03 20:32:23
|
plus_assoc
|
cympfh |
Success |
|
|
| 441 |
2019/09/03 20:25:26
|
Product of n consecutive integers is divisible by n!
|
cympfh |
Success |
|
|
| 440 |
2019/09/03 20:19:03
|
Product of n consecutive integers is divisible by n!
|
cympfh |
Failure |
|
|
| 439 |
2019/09/03 15:06:03
|
n * S m = n + n * m
|
cympfh |
Success |
|
|
| 438 |
2019/09/03 15:02:43
|
n < m \/ n = m \/ n > m
|
cympfh |
Success |
|
|
| 437 |
2019/09/03 14:52:17
|
n < m \/ n = m \/ n > m
|
cympfh |
Failure |
|
|
| 436 |
2019/09/03 14:32:06
|
Cumulative sum of list
|
cympfh |
Success |
|
|
| 435 |
2019/09/01 19:49:53
|
n < m \/ n = m \/ n > m
|
muratak |
Success |
|
|
| 434 |
2019/09/01 19:33:53
|
Cumulative sum of list
|
muratak |
Success |
|
|
| 433 |
2019/09/01 19:33:20
|
Cumulative sum of list
|
muratak |
Failure |
|
|
| 432 |
2019/09/01 19:16:43
|
forall l: list nat, l @ [0] <> []
|
muratak |
Success |
|
|
| 431 |
2019/08/31 22:19:06
|
forall f: bool -> bool, f^3(x) = f(x)
|
yodvhskd |
Success |
|
|
| 430 |
2019/08/31 22:02:00
|
plus_comm
|
yodvhskd |
Success |
|
|
| 429 |
2019/08/31 18:20:24
|
Cumulative sum of list
|
admitted |
Success |
|
|
| 428 |
2019/08/31 17:53:39
|
forall l: list nat, l @ [0] <> []
|
admitted |
Success |
|
|
| 427 |
2019/08/31 16:35:17
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 426 |
2019/08/31 16:34:26
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 425 |
2019/08/31 16:33:34
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Failure |
|
|
| 424 |
2019/08/31 04:59:27
|
n < m \/ n = m \/ n > m
|
admitted |
Success |
|
|
| 423 |
2019/08/31 04:35:39
|
n * S m = n + n * m
|
admitted |
Success |
|
|
| 422 |
2019/08/31 04:22:47
|
forall f: bool -> bool, f^3(x) = f(x)
|
admitted |
Success |
|
|
| 421 |
2019/08/31 04:05:00
|
1 + 1 = 2
|
admitted |
Success |
|
|
| 420 |
2019/08/31 04:02:26
|
plus_comm
|
admitted |
Success |
|
|
| 419 |
2019/08/31 03:51:03
|
plus_assoc
|
admitted |
Success |
|
|
| 418 |
2019/08/31 00:32:14
|
1 + 1 = 2
|
yodvhskd |
Success |
|
|
| 417 |
2019/08/31 00:28:15
|
1 + 1 = 2
|
yodvhskd |
Success |
|
|
| 416 |
2019/08/30 23:22:39
|
1 + 1 = 2
|
omasanori |
Success |
|
|
| 415 |
2019/08/30 23:21:51
|
1 + 1 = 2
|
omasanori |
Failure |
|
|
| 414 |
2019/08/30 21:29:36
|
n < m \/ n = m \/ n > m
|
kimiyuki |
Success |
|
|
| 413 |
2019/08/30 21:15:10
|
Cumulative sum of list
|
kimiyuki |
Success |
|
|
| 412 |
2019/08/30 18:07:04
|
forall f: bool -> bool, f^3(x) = f(x)
|
pekempey |
Success |
|
|
| 411 |
2019/08/30 17:33:32
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 410 |
2019/08/30 17:24:54
|
forall l: list nat, l @ [0] <> []
|
cympfh |
Success |
|
|
| 409 |
2019/08/29 17:55:20
|
n < m \/ n = m \/ n > m
|
minus3theta |
Success |
|
|
| 408 |
2019/08/29 17:52:24
|
forall l: list nat, l @ [0] <> []
|
minus3theta |
Success |
|
|
| 407 |
2019/08/29 10:05:06
|
n * S m = n + n * m
|
muratak |
Success |
|
|
| 406 |
2019/08/29 10:04:50
|
n * S m = n + n * m
|
muratak |
Failure |
|
|
| 405 |
2019/08/29 01:37:00
|
n * S m = n + n * m
|
muratak |
Rejected |
|
|
| 404 |
2019/08/29 01:32:41
|
forall f: bool -> bool, f^3(x) = f(x)
|
muratak |
Success |
|
|
| 403 |
2019/08/29 01:32:07
|
forall f: bool -> bool, f^3(x) = f(x)
|
muratak |
Failure |
|
|
| 402 |
2019/08/29 01:22:38
|
plus_comm
|
muratak |
Success |
|
|
| 401 |
2019/08/29 01:19:17
|
plus_assoc
|
muratak |
Success |
|
|
| 400 |
2019/08/29 01:17:37
|
1 + 1 = 2
|
muratak |
Success |
|
|
| 399 |
2019/08/28 02:19:34
|
1 + 1 = 2
|
asi1024 |
Success |
|
|
| 398 |
2019/08/27 23:13:17
|
n < m \/ n = m \/ n > m
|
taisei |
Success |
|
|
| 397 |
2019/08/27 23:12:06
|
Product of n consecutive integers is divisible by n!
|
taisei |
Success |
|
|
| 396 |
2019/08/27 18:19:28
|
Product of n consecutive integers is divisible by n!
|
kkob |
Success |
|
|
| 395 |
2019/08/27 16:41:13
|
forall l: list nat, l @ [0] <> []
|
coorde |
Success |
|
|
| 394 |
2019/08/27 16:40:19
|
forall l: list nat, l @ [0] <> []
|
coorde |
Success |
|
|
| 393 |
2019/08/27 16:34:11
|
n < m \/ n = m \/ n > m
|
coorde |
Success |
|
|
| 392 |
2019/08/27 12:23:49
|
Equivalent two quicksorts
|
kkob |
Success |
|
|
| 391 |
2019/08/27 07:22:52
|
forall l: list nat, l @ [0] <> []
|
omochana2 |
Success |
|
|
| 390 |
2019/08/27 00:56:30
|
forall l: list nat, l @ [0] <> []
|
uesugi |
Success |
|
|
| 389 |
2019/08/27 00:55:05
|
forall l: list nat, l @ [0] <> []
|
uesugi |
Failure |
|
|
| 388 |
2019/08/26 22:05:31
|
n * S m = n + n * m
|
coorde |
Success |
|
|
| 387 |
2019/08/26 21:56:04
|
forall f: bool -> bool, f^3(x) = f(x)
|
coorde |
Success |
|
|
| 386 |
2019/08/26 21:50:07
|
plus_comm
|
coorde |
Success |
|
|
| 385 |
2019/08/26 21:49:20
|
n < m \/ n = m \/ n > m
|
cympfh |
Success |
|
|
| 384 |
2019/08/26 21:39:41
|
n * S m = n + n * m
|
cympfh |
Success |
|
|
| 383 |
2019/08/26 21:30:10
|
n < m \/ n = m \/ n > m
|
chiguri |
Success |
|
|
| 382 |
2019/08/26 21:29:56
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Success |
|
|
| 381 |
2019/08/26 21:28:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Failure |
|
|
| 380 |
2019/08/26 21:16:39
|
n * S m = n + n * m
|
chiguri |
Success |
|
|
| 379 |
2019/08/26 21:10:05
|
forall f: bool -> bool, f^3(x) = f(x)
|
cympfh |
Failure |
|
|
| 378 |
2019/08/26 21:09:55
|
1 + 1 = 2
|
cympfh |
Success |
|
|
| 377 |
2019/08/26 21:03:24
|
forall f: bool -> bool, f^3(x) = f(x)
|
chiguri |
Success |
|
|
| 376 |
2019/08/26 20:59:40
|
1 + 1 = 2
|
chiguri |
Success |
|
|
| 375 |
2019/08/26 20:59:29
|
plus_comm
|
cympfh |
Success |
|
|
| 374 |
2019/08/26 20:58:31
|
plus_comm
|
chiguri |
Success |
|
|
| 373 |
2019/08/26 20:56:24
|
plus_assoc
|
coorde |
Success |
|
|
| 372 |
2019/08/26 20:50:10
|
plus_assoc
|
chiguri |
Success |
|
|
| 371 |
2019/08/26 20:49:02
|
plus_assoc
|
chiguri |
Failure |
|
|
| 370 |
2019/08/26 20:34:32
|
1 + 1 = 2
|
coorde |
Success |
|
|
| 369 |
2019/08/26 20:22:31
|
plus_comm
|
drafear |
Success |
|
|
| 368 |
2019/08/26 20:21:59
|
plus_comm
|
drafear |
Failure |
|
|
| 367 |
2019/08/26 19:43:13
|
plus_assoc
|
cympfh |
Success |
|
|
| 366 |
2019/08/26 19:42:32
|
plus_assoc
|
cympfh |
Failure |
|
|
| 365 |
2019/08/26 18:58:12
|
plus_comm
|
mttm |
Success |
|
|
| 364 |
2019/08/26 18:20:38
|
Cumulative sum of list
|
sorata |
Success |
|
|
| 363 |
2019/08/26 14:30:09
|
forall l: list nat, l @ [0] <> []
|
heno239 |
Success |
|
|
| 362 |
2019/08/26 12:30:16
|
l1 <> l2 if l2 is an odd permutation of l1
|
kkob |
Success |
|
|
| 361 |
2019/08/26 10:22:23
|
n < m \/ n = m \/ n > m
|
a_happin |
Success |
|
|
| 360 |
2019/08/26 08:57:52
|
plus_comm
|
spica314 |
Success |
|
|
| 359 |
2019/08/26 08:32:58
|
plus_assoc
|
spica314 |
Success |
|
|
| 358 |
2019/08/26 04:20:30
|
forall l: list nat, l @ [0] <> []
|
pekempey |
Success |
|
|
| 357 |
2019/08/26 03:52:57
|
l1 <> l2 if l2 is an odd permutation of l1
|
suibaka |
Success |
|
|
| 356 |
2019/08/26 03:51:12
|
l1 <> l2 if l2 is an odd permutation of l1
|
suibaka |
Failure |
|
|
| 355 |
2019/08/26 03:48:10
|
l1 <> l2 if l2 is an odd permutation of l1
|
suibaka |
Failure |
|
|
| 354 |
2019/08/26 03:45:48
|
n * S m = n + n * m
|
omochana2 |
Success |
|
|
| 353 |
2019/08/26 03:37:39
|
plus_comm
|
omochana2 |
Success |
|
|
| 352 |
2019/08/26 03:30:24
|
plus_comm
|
omochana2 |
Failure |
|
|
| 351 |
2019/08/26 03:29:33
|
plus_assoc
|
omochana2 |
Success |
|
|
| 350 |
2019/08/26 02:58:33
|
forall f: bool -> bool, f^3(x) = f(x)
|
omochana2 |
Success |
|
|
| 349 |
2019/08/26 02:40:25
|
plus_comm
|
mttm |
Success |
|
|
| 348 |
2019/08/26 02:36:37
|
plus_assoc
|
mttm |
Success |
|
|
| 347 |
2019/08/26 02:36:18
|
n < m \/ n = m \/ n > m
|
spica314 |
Success |
|
|
| 346 |
2019/08/26 02:34:30
|
plus_assoc
|
mttm |
Failure |
|
|
| 345 |
2019/08/26 02:23:02
|
Product of n consecutive integers is divisible by n!
|
prime |
Success |
|
|
| 344 |
2019/08/26 01:50:30
|
n * S m = n + n * m
|
mttm |
Success |
|
|
| 343 |
2019/08/26 01:46:22
|
1 + 1 = 2
|
omochana2 |
Success |
|
|
| 342 |
2019/08/26 01:45:15
|
n * S m = n + n * m
|
spica314 |
Success |
|
|
| 341 |
2019/08/26 01:19:10
|
n * S m = n + n * m
|
prime |
Success |
|
|
| 340 |
2019/08/26 01:16:25
|
1 + 1 = 2
|
prime |
Success |
|
|
| 339 |
2019/08/26 01:13:50
|
forall f: bool -> bool, f^3(x) = f(x)
|
prime |
Success |
|
|
| 338 |
2019/08/26 01:11:50
|
l1 <> l2 if l2 is an odd permutation of l1
|
drafear |
Success |
|
|
| 337 |
2019/08/26 01:11:06
|
l1 <> l2 if l2 is an odd permutation of l1
|
drafear |
Failure |
|
|
| 336 |
2019/08/26 01:11:02
|
forall l: list nat, l @ [0] <> []
|
prime |
Success |
|
|
| 335 |
2019/08/26 01:10:31
|
Cumulative sum of list
|
prime |
Success |
|
|
| 334 |
2019/08/26 01:09:41
|
forall f: bool -> bool, f^3(x) = f(x)
|
mttm |
Success |
|
|
| 333 |
2019/08/26 01:08:42
|
l1 <> l2 if l2 is an odd permutation of l1
|
prime |
Success |
|
|
| 332 |
2019/08/26 00:47:39
|
1 + 1 = 2
|
mttm |
Success |
|
|
| 331 |
2019/08/26 00:38:37
|
forall l: list nat, l @ [0] <> []
|
yishibashi |
Success |
|
|
| 330 |
2019/08/26 00:17:20
|
Cumulative sum of list
|
a_happin |
Success |
|
|
| 329 |
2019/08/26 00:12:22
|
forall f: bool -> bool, f^3(x) = f(x)
|
yishibashi |
Success |
|
|
| 328 |
2019/08/25 23:49:36
|
l1 <> l2 if l2 is an odd permutation of l1
|
kaz |
Failure |
|
|
| 327 |
2019/08/25 23:45:38
|
1 + 1 = 2
|
yishibashi |
Success |
|
|
| 326 |
2019/08/25 23:45:15
|
1 + 1 = 2
|
yishibashi |
Failure |
|
|
| 325 |
2019/08/25 23:43:51
|
forall f: bool -> bool, f^3(x) = f(x)
|
spica314 |
Success |
|
|
| 324 |
2019/08/25 23:42:08
|
Cumulative sum of list
|
kkob |
Success |
|
|
| 323 |
2019/08/25 23:37:32
|
l1 <> l2 if l2 is an odd permutation of l1
|
kaz |
Success |
|
|
| 322 |
2019/08/25 23:32:16
|
l1 <> l2 if l2 is an odd permutation of l1
|
prime |
Success |
|
|
| 321 |
2019/08/25 23:22:46
|
l1 <> l2 if l2 is an odd permutation of l1
|
kaz |
Success |
|
|
| 320 |
2019/08/25 23:22:37
|
1 + 1 = 2
|
spica314 |
Success |
|
|
| 319 |
2019/08/25 23:20:57
|
forall l: list nat, l @ [0] <> []
|
siotouto |
Success |
|
|
| 318 |
2019/08/25 23:20:08
|
forall l: list nat, l @ [0] <> []
|
siotouto |
Failure |
|
|
| 317 |
2019/08/25 23:17:23
|
l1 <> l2 if l2 is an odd permutation of l1
|
satos |
Success |
|
|
| 316 |
2019/08/25 23:17:01
|
l1 <> l2 if l2 is an odd permutation of l1
|
satos |
Failure |
|
|
| 315 |
2019/08/25 23:16:21
|
Cumulative sum of list
|
koba |
Success |
|
|
| 314 |
2019/08/25 23:15:54
|
Cumulative sum of list
|
koba |
Failure |
|
|
| 313 |
2019/08/25 23:14:27
|
l1 <> l2 if l2 is an odd permutation of l1
|
koba |
Success |
|
|
| 312 |
2019/08/25 23:00:00
|
Cumulative sum of list
|
yamarten |
Rejected |
|
|
| 311 |
2019/08/25 22:59:19
|
l1 <> l2 if l2 is an odd permutation of l1
|
satos |
Failure |
|
|
| 310 |
2019/08/25 22:53:38
|
Cumulative sum of list
|
yamarten |
Success |
|
|
| 309 |
2019/08/25 22:53:17
|
Cumulative sum of list
|
yamarten |
Failure |
|
|
| 308 |
2019/08/25 22:37:37
|
l1 <> l2 if l2 is an odd permutation of l1
|
kozima |
Success |
|
|
| 307 |
2019/08/25 22:17:35
|
Cumulative sum of list
|
okaduki |
Success |
|
|
| 306 |
2019/08/25 21:59:34
|
Cumulative sum of list
|
prime |
Success |
|
|
| 305 |
2019/08/25 21:56:16
|
Cumulative sum of list
|
pekempey |
Success |
|
|
| 304 |
2019/08/25 21:43:53
|
Cumulative sum of list
|
kimiyuki |
Success |
|
|
| 303 |
2019/08/25 21:42:38
|
1 + 1 = 2
|
minaminao |
Success |
|
|
| 302 |
2019/08/25 21:42:18
|
forall l: list nat, l @ [0] <> []
|
minaminao |
Failure |
|
|
| 301 |
2019/08/25 21:41:09
|
1 + 1 = 2
|
minaminao |
Failure |
|
|
| 300 |
2019/08/25 21:32:24
|
forall l: list nat, l @ [0] <> []
|
satanic0258 |
Success |
|
|
| 299 |
2019/08/25 21:31:49
|
Cumulative sum of list
|
sorata |
Failure |
|
|
| 298 |
2019/08/25 21:29:46
|
Cumulative sum of list
|
suibaka |
Success |
|
|
| 297 |
2019/08/25 21:29:02
|
Cumulative sum of list
|
drafear |
Success |
|
|
| 296 |
2019/08/25 21:28:07
|
l1 <> l2 if l2 is an odd permutation of l1
|
drafear |
Failure |
|
|
| 295 |
2019/08/25 21:28:02
|
forall l: list nat, l @ [0] <> []
|
a_happin |
Success |
|
|
| 294 |
2019/08/25 21:27:14
|
forall l: list nat, l @ [0] <> []
|
etonagisa |
Success |
|
|
| 293 |
2019/08/25 21:26:53
|
forall l: list nat, l @ [0] <> []
|
pekempey |
Success |
|
|
| 292 |
2019/08/25 21:25:30
|
forall l: list nat, l @ [0] <> []
|
spica314 |
Success |
|
|
| 291 |
2019/08/25 21:24:47
|
Cumulative sum of list
|
satos |
Success |
|
|
| 290 |
2019/08/25 21:23:01
|
forall l: list nat, l @ [0] <> []
|
spica314 |
Failure |
|
|
| 289 |
2019/08/25 21:22:31
|
Cumulative sum of list
|
yodvhskd |
Success |
|
|
| 288 |
2019/08/25 21:19:26
|
Cumulative sum of list
|
yodvhskd |
Failure |
|
|
| 287 |
2019/08/25 21:19:25
|
forall l: list nat, l @ [0] <> []
|
taisei |
Success |
|
|
| 286 |
2019/08/25 21:17:58
|
forall l: list nat, l @ [0] <> []
|
yamarten |
Success |
|
|
| 285 |
2019/08/25 21:17:06
|
Cumulative sum of list
|
momohatt |
Success |
|
|
| 284 |
2019/08/25 21:16:50
|
Cumulative sum of list
|
taisei |
Success |
|
|
| 283 |
2019/08/25 21:14:54
|
Cumulative sum of list
|
kozima |
Success |
|
|
| 282 |
2019/08/25 21:13:07
|
forall l: list nat, l @ [0] <> []
|
satos |
Success |
|
|
| 281 |
2019/08/25 21:12:16
|
Cumulative sum of list
|
splatoon_suki |
Success |
|
|
| 280 |
2019/08/25 21:11:55
|
forall l: list nat, l @ [0] <> []
|
utgwkk |
Success |
|
|
| 279 |
2019/08/25 21:10:57
|
forall l: list nat, l @ [0] <> []
|
suibaka |
Success |
|
|
| 278 |
2019/08/25 21:10:39
|
forall l: list nat, l @ [0] <> []
|
sorata |
Success |
|
|
| 277 |
2019/08/25 21:10:21
|
Cumulative sum of list
|
kaz |
Success |
|
|
| 276 |
2019/08/25 21:08:50
|
forall l: list nat, l @ [0] <> []
|
kanra824 |
Success |
|
|
| 275 |
2019/08/25 21:07:19
|
forall l: list nat, l @ [0] <> []
|
prime |
Success |
|
|
| 274 |
2019/08/25 21:03:51
|
forall l: list nat, l @ [0] <> []
|
suibaka |
Failure |
|
|
| 273 |
2019/08/25 21:03:38
|
forall l: list nat, l @ [0] <> []
|
suibaka |
Failure |
|
|
| 272 |
2019/08/25 21:03:18
|
forall l: list nat, l @ [0] <> []
|
okaduki |
Success |
|
|
| 271 |
2019/08/25 21:03:08
|
forall l: list nat, l @ [0] <> []
|
kozima |
Success |
|
|
| 270 |
2019/08/25 21:03:06
|
forall l: list nat, l @ [0] <> []
|
momohatt |
Success |
|
|
| 269 |
2019/08/25 21:02:03
|
forall l: list nat, l @ [0] <> []
|
drafear |
Success |
|
|
| 268 |
2019/08/25 21:01:56
|
forall l: list nat, l @ [0] <> []
|
splatoon_suki |
Success |
|
|
| 267 |
2019/08/25 21:01:54
|
forall l: list nat, l @ [0] <> []
|
drafear |
Success |
|
|
| 266 |
2019/08/25 21:01:32
|
forall l: list nat, l @ [0] <> []
|
kaz |
Success |
|
|
| 265 |
2019/08/25 21:01:23
|
forall l: list nat, l @ [0] <> []
|
yodvhskd |
Success |
|
|
| 264 |
2019/08/25 21:01:17
|
forall l: list nat, l @ [0] <> []
|
kimiyuki |
Success |
|
|
| 263 |
2019/08/25 20:56:46
|
1 + 1 = 2
|
spica314 |
Success |
|
|
| 262 |
2019/08/25 20:54:16
|
1 + 1 = 2
|
kanra824 |
Success |
|
|
| 261 |
2019/08/25 19:57:58
|
plus_assoc
|
yodvhskd |
Success |
|
|
| 260 |
2019/08/25 11:40:11
|
1 + 1 = 2
|
momohatt |
Success |
|
|
| 259 |
2019/08/25 11:39:43
|
1 + 1 = 2
|
momohatt |
Failure |
|
|
| 258 |
2019/08/25 01:40:53
|
forall l: list nat, l @ [0] <> []
|
asi1024 |
Success |
|
|
| 257 |
2019/08/24 23:41:45
|
plus_comm
|
asi1024 |
Success |
|
|
| 256 |
2019/08/24 21:41:33
|
plus_comm
|
clkbug |
Failure |
|
|
| 255 |
2019/08/24 21:41:28
|
plus_comm
|
clkbug |
Failure |
|
|
| 254 |
2019/08/24 21:37:21
|
plus_comm
|
clkbug |
Failure |
|
|
| 253 |
2019/08/24 21:36:26
|
plus_comm
|
clkbug |
Failure |
|
|
| 252 |
2019/08/24 21:29:45
|
plus_assoc
|
clkbug |
Failure |
|
|
| 251 |
2019/08/24 21:24:32
|
plus_assoc
|
clkbug |
Failure |
|
|
| 250 |
2019/08/24 21:23:25
|
plus_assoc
|
clkbug |
Failure |
|
|
| 249 |
2019/08/24 20:38:23
|
1 + 1 = 2
|
yamarten |
Success |
|
|
| 248 |
2019/08/24 20:27:29
|
1 + 1 = 2
|
yamarten |
Rejected |
|
|
| 247 |
2019/08/24 08:44:10
|
1 + 1 = 2
|
koba |
Failure |
|
|
| 246 |
2019/08/24 08:43:24
|
1 + 1 = 2
|
koba |
Rejected |
|
|
| 245 |
2019/08/23 16:10:05
|
forall f: bool -> bool, f^3(x) = f(x)
|
luma |
Rejected |
|
|
| 244 |
2019/08/23 15:04:04
|
plus_comm
|
rikein12 |
Failure |
|
|
| 243 |
2019/08/23 15:01:02
|
n * S m = n + n * m
|
rikein12 |
Success |
|
|
| 242 |
2019/08/23 08:57:00
|
forall f: bool -> bool, f^3(x) = f(x)
|
splatoon_suki |
Success |
|
|
| 241 |
2019/08/23 03:59:42
|
forall f: bool -> bool, f^3(x) = f(x)
|
rikein12 |
Success |
|
|
| 240 |
2019/08/23 03:55:16
|
1 + 1 = 2
|
rikein12 |
Success |
|
|
| 239 |
2019/08/23 03:35:18
|
plus_assoc
|
rikein12 |
Success |
|
|
| 238 |
2019/08/23 01:42:15
|
forall f: bool -> bool, f^3(x) = f(x)
|
kaz |
Success |
|
|
| 237 |
2019/08/23 01:32:12
|
Product of n consecutive integers is divisible by n!
|
kaz |
Success |
|
|
| 236 |
2019/08/23 01:11:02
|
Product of n consecutive integers is divisible by n!
|
kaz |
Success |
|
|
| 235 |
2019/08/23 01:08:08
|
Product of n consecutive integers is divisible by n!
|
kaz |
Success |
|
|
| 234 |
2019/08/23 01:07:00
|
Product of n consecutive integers is divisible by n!
|
kaz |
Success |
|
|
| 233 |
2019/08/23 01:05:17
|
Product of n consecutive integers is divisible by n!
|
kaz |
Failure |
|
|
| 232 |
2019/08/23 00:02:06
|
1 + 1 = 2
|
kaz |
Success |
|
|
| 231 |
2019/08/22 23:40:30
|
n < m \/ n = m \/ n > m
|
kaz |
Success |
|
|
| 230 |
2019/08/22 23:36:57
|
n * S m = n + n * m
|
kaz |
Success |
|
|
| 229 |
2019/08/22 23:35:05
|
forall f: bool -> bool, f^3(x) = f(x)
|
kaz |
Success |
|
|
| 228 |
2019/08/22 23:31:37
|
plus_comm
|
sorata |
Success |
|
|
| 227 |
2019/08/22 23:31:22
|
1 + 1 = 2
|
kaz |
Success |
|
|
| 226 |
2019/08/22 23:30:52
|
plus_comm
|
kaz |
Success |
|
|
| 225 |
2019/08/22 23:30:09
|
plus_comm
|
kaz |
Failure |
|
|
| 224 |
2019/08/22 23:29:06
|
plus_assoc
|
kaz |
Success |
|
|
| 223 |
2019/08/22 23:27:02
|
plus_assoc
|
sorata |
Success |
|
|
| 222 |
2019/08/22 23:26:04
|
plus_assoc
|
sorata |
Failure |
|
|
| 221 |
2019/08/22 23:24:12
|
plus_assoc
|
sorata |
Failure |
|
|
| 220 |
2019/08/22 14:59:16
|
1 + 1 = 2
|
luma |
Success |
|
|
| 219 |
2019/08/22 09:32:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
kozima |
Success |
|
|
| 218 |
2019/08/22 01:02:03
|
n < m \/ n = m \/ n > m
|
asi1024 |
Success |
|
|
| 217 |
2019/08/22 01:01:39
|
n < m \/ n = m \/ n > m
|
asi1024 |
Failure |
|
|
| 216 |
2019/08/22 01:01:13
|
n < m \/ n = m \/ n > m
|
asi1024 |
Failure |
|
|
| 215 |
2019/08/21 19:52:23
|
n < m \/ n = m \/ n > m
|
efk |
Success |
|
|
| 214 |
2019/08/21 19:47:05
|
n * S m = n + n * m
|
efk |
Success |
|
|
| 213 |
2019/08/21 19:40:34
|
forall f: bool -> bool, f^3(x) = f(x)
|
efk |
Success |
|
|
| 212 |
2019/08/21 19:19:08
|
1 + 1 = 2
|
efk |
Success |
|
|
| 211 |
2019/08/21 18:29:23
|
Product of n consecutive integers is divisible by n!
|
kimiyuki |
Success |
|
|
| 210 |
2019/08/21 17:53:21
|
n * S m = n + n * m
|
a_happin |
Success |
|
|
| 209 |
2019/08/21 17:42:04
|
n * S m = n + n * m
|
a_happin |
Rejected |
|
|
| 208 |
2019/08/21 17:21:56
|
forall f: bool -> bool, f^3(x) = f(x)
|
a_happin |
Success |
|
|
| 207 |
2019/08/21 16:07:20
|
1 + 1 = 2
|
a_happin |
Failure |
|
|
| 206 |
2019/08/21 16:04:48
|
1 + 1 = 2
|
a_happin |
Failure |
|
|
| 205 |
2019/08/21 16:04:03
|
1 + 1 = 2
|
a_happin |
Success |
|
|
| 204 |
2019/08/21 16:03:38
|
1 + 1 = 2
|
a_happin |
Failure |
|
|
| 203 |
2019/08/21 16:03:18
|
1 + 1 = 2
|
a_happin |
Failure |
|
|
| 202 |
2019/08/21 15:59:43
|
plus_comm
|
a_happin |
Success |
|
|
| 201 |
2019/08/21 15:27:39
|
plus_assoc
|
a_happin |
Success |
|
|
| 200 |
2019/08/21 11:58:21
|
n < m \/ n = m \/ n > m
|
pandanoir |
Success |
|
|
| 199 |
2019/08/21 11:48:05
|
n * S m = n + n * m
|
pandanoir |
Success |
|
|
| 198 |
2019/08/21 11:47:59
|
forall f: bool -> bool, f^3(x) = f(x)
|
pandanoir |
Failure |
|
|
| 197 |
2019/08/21 11:30:49
|
forall f: bool -> bool, f^3(x) = f(x)
|
pandanoir |
Success |
|
|
| 196 |
2019/08/21 11:23:21
|
1 + 1 = 2
|
pandanoir |
Success |
|
|
| 195 |
2019/08/21 05:01:28
|
Equivalent two quicksorts
|
satos |
Success |
|
|
| 194 |
2019/08/21 05:00:50
|
Equivalent two quicksorts
|
satos |
Failure |
|
|
| 193 |
2019/08/21 04:59:24
|
Equivalent two quicksorts
|
satos |
Failure |
|
|
| 192 |
2019/08/20 23:30:02
|
Product of n consecutive integers is divisible by n!
|
kozima |
Success |
|
|
| 191 |
2019/08/20 20:02:54
|
plus_comm
|
minus3theta |
Success |
|
|
| 190 |
2019/08/20 19:39:23
|
plus_assoc
|
minus3theta |
Success |
|
|
| 189 |
2019/08/20 00:30:26
|
Product of n consecutive integers is divisible by n!
|
pekempey |
Success |
|
|
| 188 |
2019/08/19 23:39:05
|
Product of n consecutive integers is divisible by n!
|
satos |
Success |
|
|
| 187 |
2019/08/19 23:36:07
|
Product of n consecutive integers is divisible by n!
|
satos |
Failure |
|
|
| 186 |
2019/08/19 19:09:04
|
plus_comm
|
heno239 |
Success |
|
|
| 185 |
2019/08/19 19:02:43
|
plus_assoc
|
heno239 |
Success |
|
|
| 184 |
2019/08/19 18:51:48
|
1 + 1 = 2
|
drafear |
Success |
|
|
| 183 |
2019/08/19 17:57:32
|
n < m \/ n = m \/ n > m
|
okaduki |
Success |
|
|
| 182 |
2019/08/19 17:09:42
|
n * S m = n + n * m
|
okaduki |
Success |
|
|
| 181 |
2019/08/19 17:00:12
|
forall f: bool -> bool, f^3(x) = f(x)
|
okaduki |
Success |
|
|
| 180 |
2019/08/19 16:14:13
|
1 + 1 = 2
|
okaduki |
Success |
|
|
| 179 |
2019/08/19 16:05:38
|
plus_comm
|
okaduki |
Success |
|
|
| 178 |
2019/08/19 15:36:40
|
plus_comm
|
okaduki |
Failure |
|
|
| 177 |
2019/08/19 15:36:09
|
plus_comm
|
okaduki |
Failure |
|
|
| 176 |
2019/08/19 15:32:33
|
plus_assoc
|
okaduki |
Success |
|
|
| 175 |
2019/08/19 15:30:47
|
plus_assoc
|
okaduki |
Success |
|
|
| 174 |
2019/08/19 14:11:42
|
1 + 1 = 2
|
taro |
Failure |
|
|
| 173 |
2019/08/19 14:07:14
|
n * S m = n + n * m
|
selpo |
Success |
|
|
| 172 |
2019/08/19 13:54:08
|
forall f: bool -> bool, f^3(x) = f(x)
|
selpo |
Success |
|
|
| 171 |
2019/08/19 13:47:06
|
n * S m = n + n * m
|
minus3theta |
Success |
|
|
| 170 |
2019/08/19 13:36:10
|
forall f: bool -> bool, f^3(x) = f(x)
|
minus3theta |
Success |
|
|
| 169 |
2019/08/19 12:46:09
|
1 + 1 = 2
|
selpo |
Success |
|
|
| 168 |
2019/08/19 11:43:34
|
1 + 1 = 2
|
minus3theta |
Success |
|
|
| 167 |
2019/08/19 11:34:46
|
Product of n consecutive integers is divisible by n!
|
satanic0258 |
Success |
|
|
| 166 |
2019/08/19 11:17:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
Mayimg |
Success |
|
|
| 165 |
2019/08/19 10:36:23
|
plus_comm
|
Mayimg |
Success |
|
|
| 164 |
2019/08/19 10:28:19
|
plus_assoc
|
Mayimg |
Success |
|
|
| 163 |
2019/08/19 10:27:19
|
plus_assoc
|
Mayimg |
Failure |
|
|
| 162 |
2019/08/19 10:26:33
|
plus_assoc
|
Mayimg |
Failure |
|
|
| 161 |
2019/08/19 10:20:09
|
plus_assoc
|
Mayimg |
Failure |
|
|
| 160 |
2019/08/19 08:57:56
|
n < m \/ n = m \/ n > m
|
pekempey |
Success |
|
|
| 159 |
2019/08/19 08:55:45
|
plus_assoc
|
pekempey |
Success |
|
|
| 158 |
2019/08/19 08:55:02
|
plus_assoc
|
pekempey |
Failure |
|
|
| 157 |
2019/08/19 06:00:58
|
n * S m = n + n * m
|
pekempey |
Success |
|
|
| 156 |
2019/08/19 05:47:38
|
n < m \/ n = m \/ n > m
|
satanic0258 |
Success |
|
|
| 155 |
2019/08/19 05:46:20
|
1 + 1 = 2
|
Mayimg |
Success |
|
|
| 154 |
2019/08/19 05:41:42
|
1 + 1 = 2
|
Mayimg |
Success |
|
|
| 153 |
2019/08/19 05:38:28
|
forall f: bool -> bool, f^3(x) = f(x)
|
pekempey |
Success |
|
|
| 152 |
2019/08/19 05:26:24
|
n * S m = n + n * m
|
satanic0258 |
Success |
|
|
| 151 |
2019/08/19 05:15:39
|
forall f: bool -> bool, f^3(x) = f(x)
|
satanic0258 |
Success |
|
|
| 150 |
2019/08/19 04:48:04
|
1 + 1 = 2
|
pekempey |
Success |
|
|
| 149 |
2019/08/19 04:47:24
|
plus_comm
|
pekempey |
Success |
|
|
| 148 |
2019/08/19 04:47:00
|
plus_comm
|
pekempey |
Failure |
|
|
| 147 |
2019/08/19 04:44:32
|
1 + 1 = 2
|
satanic0258 |
Success |
|
|
| 146 |
2019/08/19 04:42:20
|
plus_comm
|
satanic0258 |
Success |
|
|
| 145 |
2019/08/19 04:38:00
|
plus_assoc
|
pekempey |
Success |
|
|
| 144 |
2019/08/19 04:37:22
|
plus_assoc
|
satanic0258 |
Success |
|
|
| 143 |
2019/08/19 04:36:19
|
plus_assoc
|
satanic0258 |
Success |
|
|
| 142 |
2019/08/19 03:08:03
|
Equivalent two quicksorts
|
koba |
Success |
|
|
| 141 |
2019/08/19 03:00:23
|
Product of n consecutive integers is divisible by n!
|
drafear |
Success |
|
|
| 140 |
2019/08/19 02:59:48
|
Equivalent two quicksorts
|
drafear |
Failure |
|
|
| 139 |
2019/08/19 01:42:35
|
1 + 1 = 2
|
kanra824 |
Success |
|
|
| 138 |
2019/08/19 01:41:53
|
1 + 1 = 2
|
kanra824 |
Failure |
|
|
| 137 |
2019/08/19 01:36:57
|
1 + 1 = 2
|
kanra824 |
Failure |
|
|
| 136 |
2019/08/19 01:26:08
|
Equivalent two quicksorts
|
koba |
Success |
|
|
| 135 |
2019/08/19 00:56:32
|
Equivalent two quicksorts
|
koba |
Rejected |
|
|
| 134 |
2019/08/18 23:56:39
|
Equivalent two quicksorts
|
koba |
Rejected |
|
|
| 133 |
2019/08/18 23:47:12
|
n < m \/ n = m \/ n > m
|
OKU_K |
Success |
|
|
| 132 |
2019/08/18 23:35:07
|
n * S m = n + n * m
|
OKU_K |
Success |
|
|
| 131 |
2019/08/18 23:24:19
|
forall f: bool -> bool, f^3(x) = f(x)
|
OKU_K |
Success |
|
|
| 130 |
2019/08/18 23:11:29
|
1 + 1 = 2
|
OKU_K |
Success |
|
|
| 129 |
2019/08/18 23:08:11
|
plus_comm
|
OKU_K |
Success |
|
|
| 128 |
2019/08/18 23:07:26
|
plus_comm
|
OKU_K |
Failure |
|
|
| 127 |
2019/08/18 22:22:08
|
plus_comm
|
kurgm |
Success |
|
|
| 126 |
2019/08/18 22:17:26
|
plus_assoc
|
kurgm |
Success |
|
|
| 125 |
2019/08/18 22:17:13
|
Product of n consecutive integers is divisible by n!
|
suibaka |
Success |
|
|
| 124 |
2019/08/18 20:54:31
|
Equivalent two quicksorts
|
koba |
Rejected |
|
|
| 123 |
2019/08/18 20:50:01
|
n < m \/ n = m \/ n > m
|
kurgm |
Success |
|
|
| 122 |
2019/08/18 20:29:16
|
n < m \/ n = m \/ n > m
|
satos |
Success |
|
|
| 121 |
2019/08/18 20:27:46
|
n < m \/ n = m \/ n > m
|
satos |
Success |
|
|
| 120 |
2019/08/18 20:25:26
|
n * S m = n + n * m
|
kurgm |
Success |
|
|
| 119 |
2019/08/18 20:24:35
|
n * S m = n + n * m
|
etonagisa |
Success |
|
|
| 118 |
2019/08/18 20:01:22
|
Product of n consecutive integers is divisible by n!
|
prime |
Success |
|
|
| 117 |
2019/08/18 19:57:54
|
1 + 1 = 2
|
kcz |
Failure |
|
|
| 116 |
2019/08/18 19:57:35
|
1 + 1 = 2
|
kcz |
Failure |
|
|
| 115 |
2019/08/18 19:52:07
|
plus_assoc
|
kcz |
Failure |
|
|
| 114 |
2019/08/18 19:51:54
|
plus_assoc
|
kcz |
Failure |
|
|
| 113 |
2019/08/18 19:46:33
|
n * S m = n + n * m
|
heno239 |
Success |
|
|
| 112 |
2019/08/18 19:10:36
|
n * S m = n + n * m
|
kcz |
Failure |
|
|
| 111 |
2019/08/18 19:04:29
|
n < m \/ n = m \/ n > m
|
wass80 |
Success |
|
|
| 110 |
2019/08/18 18:44:23
|
plus_assoc
|
etonagisa |
Failure |
|
|
| 109 |
2019/08/18 18:35:19
|
n * S m = n + n * m
|
siotouto |
Success |
|
|
| 108 |
2019/08/18 18:33:18
|
n < m \/ n = m \/ n > m
|
etonagisa |
Success |
|
|
| 107 |
2019/08/18 18:28:32
|
n < m \/ n = m \/ n > m
|
kcz |
Success |
|
|
| 106 |
2019/08/18 18:18:40
|
Equivalent two quicksorts
|
koba |
Failure |
|
|
| 105 |
2019/08/18 17:47:00
|
forall f: bool -> bool, f^3(x) = f(x)
|
siotouto |
Success |
|
|
| 104 |
2019/08/18 17:46:41
|
forall f: bool -> bool, f^3(x) = f(x)
|
kcz |
Success |
|
|
| 103 |
2019/08/18 17:31:37
|
forall f: bool -> bool, f^3(x) = f(x)
|
kurgm |
Success |
|
|
| 102 |
2019/08/18 17:30:01
|
n * S m = n + n * m
|
etonagisa |
Failure |
|
|
| 101 |
2019/08/18 17:29:27
|
n < m \/ n = m \/ n > m
|
CoiL |
Success |
|
|
| 100 |
2019/08/18 17:29:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
heno239 |
Success |
|
|
| 99 |
2019/08/18 17:17:37
|
n < m \/ n = m \/ n > m
|
CoiL |
Failure |
|
|
| 98 |
2019/08/18 17:16:37
|
n < m \/ n = m \/ n > m
|
CoiL |
Failure |
|
|
| 97 |
2019/08/18 17:03:48
|
n < m \/ n = m \/ n > m
|
utgwkk |
Success |
|
|
| 96 |
2019/08/18 17:03:21
|
n * S m = n + n * m
|
kcz |
Success |
|
|
| 95 |
2019/08/18 17:00:39
|
n < m \/ n = m \/ n > m
|
suibaka |
Success |
|
|
| 94 |
2019/08/18 17:00:12
|
Product of n consecutive integers is divisible by n!
|
koba |
Success |
|
|
| 93 |
2019/08/18 17:00:04
|
1 + 1 = 2
|
kurgm |
Success |
|
|
| 92 |
2019/08/18 16:55:43
|
n < m \/ n = m \/ n > m
|
utgwkk |
Success |
|
|
| 91 |
2019/08/18 16:51:57
|
n < m \/ n = m \/ n > m
|
kimiyuki |
Success |
|
|
| 90 |
2019/08/18 16:49:26
|
n < m \/ n = m \/ n > m
|
hanazuki |
Success |
|
|
| 89 |
2019/08/18 16:45:35
|
n * S m = n + n * m
|
hanazuki |
Success |
|
|
| 88 |
2019/08/18 16:44:37
|
n * S m = n + n * m
|
CoiL |
Success |
|
|
| 87 |
2019/08/18 16:38:17
|
1 + 1 = 2
|
siotouto |
Success |
|
|
| 86 |
2019/08/18 16:37:58
|
n < m \/ n = m \/ n > m
|
prime |
Success |
|
|
| 85 |
2019/08/18 16:37:41
|
forall f: bool -> bool, f^3(x) = f(x)
|
etonagisa |
Success |
|
|
| 84 |
2019/08/18 16:37:24
|
n < m \/ n = m \/ n > m
|
drafear |
Success |
|
|
| 83 |
2019/08/18 16:36:01
|
forall f: bool -> bool, f^3(x) = f(x)
|
hanazuki |
Success |
|
|
| 82 |
2019/08/18 16:32:41
|
n * S m = n + n * m
|
prime |
Success |
|
|
| 81 |
2019/08/18 16:32:27
|
plus_comm
|
prime |
Failure |
|
|
| 80 |
2019/08/18 16:30:46
|
forall f: bool -> bool, f^3(x) = f(x)
|
CoiL |
Success |
|
|
| 79 |
2019/08/18 16:27:01
|
n * S m = n + n * m
|
utgwkk |
Success |
|
|
| 78 |
2019/08/18 16:25:43
|
plus_comm
|
etonagisa |
Success |
|
|
| 77 |
2019/08/18 16:21:36
|
n * S m = n + n * m
|
prime |
Success |
|
|
| 76 |
2019/08/18 16:20:59
|
n * S m = n + n * m
|
suibaka |
Success |
|
|
| 75 |
2019/08/18 16:18:54
|
n * S m = n + n * m
|
drafear |
Success |
|
|
| 74 |
2019/08/18 16:18:42
|
n < m \/ n = m \/ n > m
|
koba |
Success |
|
|
| 73 |
2019/08/18 16:17:35
|
1 + 1 = 2
|
hanazuki |
Success |
|
|
| 72 |
2019/08/18 16:16:33
|
n * S m = n + n * m
|
koba |
Success |
|
|
| 71 |
2019/08/18 16:16:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
utgwkk |
Success |
|
|
| 70 |
2019/08/18 16:16:21
|
forall f: bool -> bool, f^3(x) = f(x)
|
prime |
Success |
|
|
| 69 |
2019/08/18 16:14:40
|
n * S m = n + n * m
|
kimiyuki |
Success |
|
|
| 68 |
2019/08/18 16:12:50
|
forall f: bool -> bool, f^3(x) = f(x)
|
drafear |
Success |
|
|
| 67 |
2019/08/18 16:12:03
|
plus_assoc
|
etonagisa |
Success |
|
|
| 66 |
2019/08/18 16:11:57
|
forall f: bool -> bool, f^3(x) = f(x)
|
koba |
Success |
|
|
| 65 |
2019/08/18 16:11:48
|
1 + 1 = 2
|
heno239 |
Success |
|
|
| 64 |
2019/08/18 16:11:45
|
forall f: bool -> bool, f^3(x) = f(x)
|
kimiyuki |
Success |
|
|
| 63 |
2019/08/18 16:11:15
|
plus_assoc
|
etonagisa |
Failure |
|
|
| 62 |
2019/08/18 16:09:58
|
1 + 1 = 2
|
kcz |
Success |
|
|
| 61 |
2019/08/18 16:09:16
|
1 + 1 = 2
|
kcz |
Failure |
|
|
| 60 |
2019/08/18 16:09:07
|
n * S m = n + n * m
|
utgwkk |
Success |
|
|
| 59 |
2019/08/18 16:08:51
|
n * S m = n + n * m
|
utgwkk |
Failure |
|
|
| 58 |
2019/08/18 16:08:47
|
forall f: bool -> bool, f^3(x) = f(x)
|
drafear |
Failure |
|
|
| 57 |
2019/08/18 16:08:35
|
forall f: bool -> bool, f^3(x) = f(x)
|
drafear |
Failure |
|
|
| 56 |
2019/08/18 16:08:06
|
1 + 1 = 2
|
etonagisa |
Success |
|
|
| 55 |
2019/08/18 16:06:47
|
forall f: bool -> bool, f^3(x) = f(x)
|
suibaka |
Success |
|
|
| 54 |
2019/08/18 16:06:14
|
1 + 1 = 2
|
kimiyuki |
Success |
|
|
| 53 |
2019/08/18 16:06:12
|
1 + 1 = 2
|
CoiL |
Success |
|
|
| 52 |
2019/08/18 16:02:38
|
1 + 1 = 2
|
prime |
Success |
|
|
| 51 |
2019/08/18 16:01:46
|
1 + 1 = 2
|
CoiL |
Failure |
|
|
| 50 |
2019/08/18 16:01:21
|
1 + 1 = 2
|
drafear |
Success |
|
|
| 49 |
2019/08/18 16:00:54
|
1 + 1 = 2
|
suibaka |
Success |
|
|
| 48 |
2019/08/18 16:00:47
|
plus_comm
|
prime |
Success |
|
|
| 47 |
2019/08/18 16:00:42
|
1 + 1 = 2
|
utgwkk |
Success |
|
|
| 46 |
2019/08/18 16:00:30
|
1 + 1 = 2
|
koba |
Success |
|
|
| 45 |
2019/08/18 15:53:01
|
plus_assoc
|
prime |
Success |
|
|
| 44 |
2019/08/18 15:50:06
|
plus_assoc
|
koba |
Success |
|
|
| 43 |
2019/08/18 15:39:21
|
plus_assoc
|
koba |
Success |
|
|
| 42 |
2019/08/18 15:38:54
|
plus_assoc
|
koba |
Failure |
|
|
| 41 |
2019/08/18 12:33:58
|
plus_comm
|
suibaka |
Success |
|
|
| 40 |
2019/08/18 12:30:09
|
plus_assoc
|
suibaka |
Success |
|
|
| 39 |
2019/08/18 09:15:05
|
plus_comm
|
asi1024 |
Success |
|
|
| 38 |
2019/08/17 17:55:48
|
1 + 1 = 2
|
asi1024 |
Success |
|
|
| 37 |
2019/08/15 07:44:49
|
plus_comm
|
taisei |
Success |
|
|
| 36 |
2019/08/15 07:40:23
|
plus_comm
|
taisei |
Failure |
|
|
| 35 |
2019/08/15 07:39:51
|
plus_comm
|
taisei |
Failure |
|
|
| 34 |
2019/08/15 07:39:26
|
plus_assoc
|
taisei |
Success |
|
|
| 33 |
2019/08/15 07:38:13
|
plus_assoc
|
taisei |
Failure |
|
|
| 32 |
2019/08/14 19:55:28
|
plus_assoc
|
kimiyuki |
Rejected |
|
|
| 31 |
2019/08/14 19:54:23
|
plus_assoc
|
kimiyuki |
Failure |
|
|
| 30 |
2019/08/14 19:43:40
|
plus_comm
|
kimiyuki |
Success |
|
|
| 29 |
2019/08/14 19:39:01
|
plus_assoc
|
kimiyuki |
Success |
|
|
| 28 |
2019/08/13 22:40:35
|
plus_assoc
|
OKU_K |
Success |
|
|
| 27 |
2019/08/13 22:39:47
|
plus_assoc
|
OKU_K |
Failure |
|
|
| 26 |
2019/08/13 21:51:34
|
plus_assoc
|
OKU_K |
Failure |
|
|
| 25 |
2019/08/13 21:50:18
|
plus_assoc
|
OKU_K |
Failure |
|
|
| 24 |
2019/08/12 22:56:43
|
plus_assoc
|
ir5 |
Success |
|
|
| 23 |
2019/08/12 22:56:21
|
plus_assoc
|
ir5 |
Failure |
|
|
| 22 |
2019/08/12 22:54:00
|
plus_assoc
|
ir5 |
Failure |
|
|
| 21 |
2019/08/12 22:46:06
|
plus_assoc
|
ir5 |
Failure |
|
|
| 20 |
2019/08/12 22:44:23
|
plus_assoc
|
ir5 |
Failure |
|
|
| 19 |
2019/08/11 22:32:26
|
plus_assoc
|
koba |
Failure |
|
|
| 18 |
2019/08/07 16:24:09
|
plus_assoc
|
drafear |
Success |
|
|
| 17 |
2019/08/07 16:23:44
|
plus_assoc
|
drafear |
Failure |
|
|
| 16 |
2019/08/07 00:44:11
|
plus_comm
|
satos |
Success |
|
|
| 15 |
2019/08/06 17:32:39
|
plus_comm
|
satos |
Success |
|
|
| 14 |
2019/08/06 17:30:44
|
plus_assoc
|
satos |
Success |
|
|
| 13 |
2019/08/06 17:30:18
|
plus_assoc
|
satos |
Failure |
|
|
| 12 |
2019/08/06 17:27:24
|
plus_comm
|
satos |
Failure |
|
|
| 11 |
2019/08/06 17:25:42
|
plus_comm
|
satos |
Failure |
|
|
| 10 |
2019/08/06 17:22:11
|
plus_comm
|
satos |
Failure |
|
|
| 9 |
2019/08/06 17:21:54
|
plus_comm
|
satos |
Failure |
|
|
| 8 |
2019/08/06 01:30:26
|
plus_comm
|
asi1024 |
Success |
|
|
| 7 |
2019/08/05 15:53:36
|
plus_comm
|
utgwkk |
Success |
|
|
| 6 |
2019/08/05 15:46:57
|
plus_assoc
|
utgwkk |
Success |
|
|
| 5 |
2019/08/04 02:58:26
|
plus_comm
|
prime |
Success |
|
|
| 4 |
2019/08/04 02:26:05
|
plus_assoc
|
prime |
Success |
|
|
| 3 |
2019/08/03 07:22:20
|
plus_assoc
|
drafear |
Success |
|
|
| 2 |
2019/08/03 07:15:47
|
plus_assoc
|
drafear |
Rejected |
|
|
| 1 |
2019/08/03 06:12:33
|
plus_assoc
|
asi1024 |
Success |
|
|