DC-Build-Header: hol-light 20170109-2 / 2018-05-02 12:00:49 +0000 DC-Task: type:rebuild-binarch-only source:hol-light version:20170109-2 chroot:unstable esttime: logfile:/tmp/hol-light_20170109-2_unstable_clang60.log modes:clang60:binarch-only DC-Sbuild-call: su user42 -c 'sbuild -n --arch-any --apt-update -d unstable -v --chroot-setup-commands=/tmp/clang60 hol-light_20170109-2' sbuild (Debian sbuild) 0.73.0 (23 Dec 2016) on ip-172-31-2-93.eu-central-1.compute.internal +==============================================================================+ | hol-light 20170109-2 (amd64) Wed, 02 May 2018 12:00:49 +0000 | +==============================================================================+ Package: hol-light Version: 20170109-2 Source Version: 20170109-2 Distribution: unstable Machine Architecture: amd64 Host Architecture: amd64 Build Architecture: amd64 Build Type: any I: NOTICE: Log filtering will replace 'var/run/schroot/mount/unstable-amd64-sbuild-0146b459-eed1-42b5-9406-88612449840c' with '<>' +------------------------------------------------------------------------------+ | Chroot Setup Commands | +------------------------------------------------------------------------------+ /tmp/clang60 ------------ + echo 'Entering customization script...' Entering customization script... + CLANG_VERSION=6.0 + echo 'Install of clang-6.0' Install of clang-6.0 + apt-get update Get:1 http://127.0.0.1:9999/debian unstable InRelease [242 kB] Get:2 http://127.0.0.1:9999/debian unstable/main Sources.diff/Index [27.9 kB] Get:3 http://127.0.0.1:9999/debian unstable/main amd64 Packages.diff/Index [27.9 kB] Get:4 http://127.0.0.1:9999/debian unstable/main Sources 2018-05-02-0830.09.pdiff [16.2 kB] Get:4 http://127.0.0.1:9999/debian unstable/main Sources 2018-05-02-0830.09.pdiff [16.2 kB] Get:5 http://127.0.0.1:9999/debian unstable/main amd64 Packages 2018-05-02-0830.09.pdiff [1781 B] Get:5 http://127.0.0.1:9999/debian unstable/main amd64 Packages 2018-05-02-0830.09.pdiff [1781 B] Get:6 http://127.0.0.1:9999/debian unstable/main Translation-en [6016 kB] Fetched 6332 kB in 2s (3400 kB/s) Reading package lists... + apt-get install --yes --no-install-recommends --force-yes clang-6.0 Reading package lists... Building dependency tree... Reading state information... The following additional packages will be installed: lib32gcc1 lib32stdc++6 libbsd0 libc6-i386 libclang-common-6.0-dev libclang1-6.0 libedit2 libjsoncpp1 libllvm6.0 libncurses5 libobjc-7-dev libobjc4 Suggested packages: gnustep gnustep-devel clang-6.0-doc Recommended packages: llvm-6.0-dev python libomp-dev libgpm2 The following NEW packages will be installed: clang-6.0 lib32gcc1 lib32stdc++6 libbsd0 libc6-i386 libclang-common-6.0-dev libclang1-6.0 libedit2 libjsoncpp1 libllvm6.0 libncurses5 libobjc-7-dev libobjc4 0 upgraded, 13 newly installed, 0 to remove and 0 not upgraded. Need to get 37.7 MB of archives. After this operation, 187 MB of additional disk space will be used. Get:1 http://127.0.0.1:9999/debian unstable/main amd64 libjsoncpp1 amd64 1.7.4-3 [75.6 kB] Get:2 http://127.0.0.1:9999/debian unstable/main amd64 libbsd0 amd64 0.8.7-1 [92.1 kB] Get:3 http://127.0.0.1:9999/debian unstable/main amd64 libncurses5 amd64 6.1+20180210-2 [95.7 kB] Get:4 http://127.0.0.1:9999/debian unstable/main amd64 libedit2 amd64 3.1-20170329-1 [85.2 kB] Get:5 http://127.0.0.1:9999/debian unstable/main amd64 libllvm6.0 amd64 1:6.0-3 [14.5 MB] Get:6 http://127.0.0.1:9999/debian unstable/main amd64 libobjc4 amd64 8-20180425-1 [52.4 kB] Get:7 http://127.0.0.1:9999/debian unstable/main amd64 libobjc-7-dev amd64 7.3.0-17 [204 kB] Get:8 http://127.0.0.1:9999/debian unstable/main amd64 libc6-i386 amd64 2.27-3 [2855 kB] Get:9 http://127.0.0.1:9999/debian unstable/main amd64 lib32gcc1 amd64 1:8-20180425-1 [47.8 kB] Get:10 http://127.0.0.1:9999/debian unstable/main amd64 lib32stdc++6 amd64 8-20180425-1 [406 kB] Get:11 http://127.0.0.1:9999/debian unstable/main amd64 libclang-common-6.0-dev amd64 1:6.0-3 [3102 kB] Get:12 http://127.0.0.1:9999/debian unstable/main amd64 libclang1-6.0 amd64 1:6.0-3 [6995 kB] Get:13 http://127.0.0.1:9999/debian unstable/main amd64 clang-6.0 amd64 1:6.0-3 [9175 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 37.7 MB in 0s (95.4 MB/s) Selecting previously unselected package libjsoncpp1:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 10022 files and directories currently installed.) Preparing to unpack .../00-libjsoncpp1_1.7.4-3_amd64.deb ... Unpacking libjsoncpp1:amd64 (1.7.4-3) ... Selecting previously unselected package libbsd0:amd64. Preparing to unpack .../01-libbsd0_0.8.7-1_amd64.deb ... Unpacking libbsd0:amd64 (0.8.7-1) ... Selecting previously unselected package libncurses5:amd64. Preparing to unpack .../02-libncurses5_6.1+20180210-2_amd64.deb ... Unpacking libncurses5:amd64 (6.1+20180210-2) ... Selecting previously unselected package libedit2:amd64. Preparing to unpack .../03-libedit2_3.1-20170329-1_amd64.deb ... Unpacking libedit2:amd64 (3.1-20170329-1) ... Selecting previously unselected package libllvm6.0:amd64. Preparing to unpack .../04-libllvm6.0_1%3a6.0-3_amd64.deb ... Unpacking libllvm6.0:amd64 (1:6.0-3) ... Selecting previously unselected package libobjc4:amd64. Preparing to unpack .../05-libobjc4_8-20180425-1_amd64.deb ... Unpacking libobjc4:amd64 (8-20180425-1) ... Selecting previously unselected package libobjc-7-dev:amd64. Preparing to unpack .../06-libobjc-7-dev_7.3.0-17_amd64.deb ... Unpacking libobjc-7-dev:amd64 (7.3.0-17) ... Selecting previously unselected package libc6-i386. Preparing to unpack .../07-libc6-i386_2.27-3_amd64.deb ... Unpacking libc6-i386 (2.27-3) ... Selecting previously unselected package lib32gcc1. Preparing to unpack .../08-lib32gcc1_1%3a8-20180425-1_amd64.deb ... Unpacking lib32gcc1 (1:8-20180425-1) ... Selecting previously unselected package lib32stdc++6. Preparing to unpack .../09-lib32stdc++6_8-20180425-1_amd64.deb ... Unpacking lib32stdc++6 (8-20180425-1) ... Selecting previously unselected package libclang-common-6.0-dev. Preparing to unpack .../10-libclang-common-6.0-dev_1%3a6.0-3_amd64.deb ... Unpacking libclang-common-6.0-dev (1:6.0-3) ... Selecting previously unselected package libclang1-6.0:amd64. Preparing to unpack .../11-libclang1-6.0_1%3a6.0-3_amd64.deb ... Unpacking libclang1-6.0:amd64 (1:6.0-3) ... Selecting previously unselected package clang-6.0. Preparing to unpack .../12-clang-6.0_1%3a6.0-3_amd64.deb ... Unpacking clang-6.0 (1:6.0-3) ... Setting up libncurses5:amd64 (6.1+20180210-2) ... Setting up libobjc4:amd64 (8-20180425-1) ... Setting up libc6-i386 (2.27-3) ... Setting up libbsd0:amd64 (0.8.7-1) ... Setting up libobjc-7-dev:amd64 (7.3.0-17) ... Processing triggers for libc-bin (2.27-3) ... Setting up lib32gcc1 (1:8-20180425-1) ... Setting up libjsoncpp1:amd64 (1.7.4-3) ... Setting up libedit2:amd64 (3.1-20170329-1) ... Setting up libllvm6.0:amd64 (1:6.0-3) ... Setting up libclang1-6.0:amd64 (1:6.0-3) ... Setting up lib32stdc++6 (8-20180425-1) ... Setting up libclang-common-6.0-dev (1:6.0-3) ... Setting up clang-6.0 (1:6.0-3) ... Processing triggers for libc-bin (2.27-3) ... W: --force-yes is deprecated, use one of the options starting with --allow instead. + echo 'Replace gcc, g++ & cpp by clang' Replace gcc, g++ & cpp by clang + VERSIONS='4.6 4.7 4.8 4.9 5 6 7 8' + cd /usr/bin + for VERSION in $VERSIONS + rm -f g++-4.6 gcc-4.6 cpp-4.6 gcc + ln -s clang++-6.0 g++-4.6 + ln -s clang-6.0 gcc-4.6 + ln -s clang-6.0 cpp-4.6 + ln -s clang-6.0 gcc + echo 'gcc-4.6 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-4.6 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-4.6 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-4.6 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + for VERSION in $VERSIONS + rm -f g++-4.7 gcc-4.7 cpp-4.7 gcc + ln -s clang++-6.0 g++-4.7 + ln -s clang-6.0 gcc-4.7 + ln -s clang-6.0 cpp-4.7 + ln -s clang-6.0 gcc + echo 'gcc-4.7 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-4.7 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-4.7 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-4.7 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + for VERSION in $VERSIONS + rm -f g++-4.8 gcc-4.8 cpp-4.8 gcc + ln -s clang++-6.0 g++-4.8 + ln -s clang-6.0 gcc-4.8 + ln -s clang-6.0 cpp-4.8 + ln -s clang-6.0 gcc + echo 'gcc-4.8 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-4.8 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-4.8 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-4.8 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + for VERSION in $VERSIONS + rm -f g++-4.9 gcc-4.9 cpp-4.9 gcc + ln -s clang++-6.0 g++-4.9 + ln -s clang-6.0 gcc-4.9 + ln -s clang-6.0 cpp-4.9 + ln -s clang-6.0 gcc + echo 'gcc-4.9 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-4.9 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-4.9 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-4.9 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + for VERSION in $VERSIONS + rm -f g++-5 gcc-5 cpp-5 gcc + ln -s clang++-6.0 g++-5 + ln -s clang-6.0 gcc-5 + ln -s clang-6.0 cpp-5 + ln -s clang-6.0 gcc + echo 'gcc-5 hold' + dpkg --set-selections + echo 'g++-5 hold' + dpkg --set-selections + for VERSION in $VERSIONS + rm -f g++-6 gcc-6 cpp-6 gcc + ln -s clang++-6.0 g++-6 + ln -s clang-6.0 gcc-6 + ln -s clang-6.0 cpp-6 + ln -s clang-6.0 gcc + echo 'gcc-6 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-6 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-6 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-6 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + for VERSION in $VERSIONS + rm -f g++-7 gcc-7 cpp-7 gcc + ln -s clang++-6.0 g++-7 + ln -s clang-6.0 gcc-7 + ln -s clang-6.0 cpp-7 + ln -s clang-6.0 gcc + echo 'gcc-7 hold' + dpkg --set-selections + echo 'g++-7 hold' + dpkg --set-selections + for VERSION in $VERSIONS + rm -f g++-8 gcc-8 cpp-8 gcc + ln -s clang++-6.0 g++-8 + ln -s clang-6.0 gcc-8 + ln -s clang-6.0 cpp-8 + ln -s clang-6.0 gcc + echo 'gcc-8 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: gcc-8 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + echo 'g++-8 hold' + dpkg --set-selections dpkg: warning: package not in status nor available database at line 1: g++-8 dpkg: warning: found unknown packages; this might mean the available database is outdated, and needs to be updated through a frontend method; please see the FAQ + cd - /build/hol-light-gu41lz + echo 'Check if gcc, g++ & cpp are actually clang' Check if gcc, g++ & cpp are actually clang + gcc --version + grep clang + cpp --version + grep clang + g++ --version + grep clang I: Finished running '/tmp/clang60'. Finished processing commands. -------------------------------------------------------------------------------- +------------------------------------------------------------------------------+ | Update chroot | +------------------------------------------------------------------------------+ Hit:1 http://127.0.0.1:9999/debian unstable InRelease Reading package lists... Reading package lists... Building dependency tree... Reading state information... Calculating upgrade... 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. +------------------------------------------------------------------------------+ | Fetch source files | +------------------------------------------------------------------------------+ Check APT --------- Checking available source versions... Download source files with APT ------------------------------ Reading package lists... NOTICE: 'hol-light' packaging is maintained in the 'Git' version control system at: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/hol-light.git Please use: git clone https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/hol-light.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 6089 kB of source archives. Get:1 http://127.0.0.1:9999/debian unstable/main hol-light 20170109-2 (dsc) [1683 B] Get:2 http://127.0.0.1:9999/debian unstable/main hol-light 20170109-2 (tar) [6078 kB] Get:3 http://127.0.0.1:9999/debian unstable/main hol-light 20170109-2 (diff) [9488 B] Fetched 6089 kB in 0s (41.1 MB/s) Download complete and in download only mode I: NOTICE: Log filtering will replace 'build/hol-light-gu41lz/hol-light-20170109' with '<>' I: NOTICE: Log filtering will replace 'build/hol-light-gu41lz' with '<>' +------------------------------------------------------------------------------+ | Install build-essential | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: build-essential, fakeroot Filtered Build-Depends: build-essential, fakeroot dpkg-deb: building package 'sbuild-build-depends-core-dummy' in '/<>/resolver-Vpdung/apt_archive/sbuild-build-depends-core-dummy.deb'. dpkg-scanpackages: warning: Packages in archive but missing from override file: dpkg-scanpackages: warning: sbuild-build-depends-core-dummy dpkg-scanpackages: info: Wrote 1 entries to output Packages file. Ign:1 copy:/<>/resolver-Vpdung/apt_archive ./ InRelease Get:2 copy:/<>/resolver-Vpdung/apt_archive ./ Release [957 B] Ign:3 copy:/<>/resolver-Vpdung/apt_archive ./ Release.gpg Get:4 copy:/<>/resolver-Vpdung/apt_archive ./ Sources [349 B] Get:5 copy:/<>/resolver-Vpdung/apt_archive ./ Packages [429 B] Fetched 1735 B in 0s (0 B/s) Reading package lists... Reading package lists... Install core build dependencies (apt-based resolver) ---------------------------------------------------- Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following NEW packages will be installed: sbuild-build-depends-core-dummy 0 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 852 B of archives. After this operation, 0 B of additional disk space will be used. Get:1 copy:/<>/resolver-Vpdung/apt_archive ./ sbuild-build-depends-core-dummy 0.invalid.0 [852 B] debconf: delaying package configuration, since apt-utils is not installed Fetched 852 B in 0s (0 B/s) Selecting previously unselected package sbuild-build-depends-core-dummy. (Reading database ... 10771 files and directories currently installed.) Preparing to unpack .../sbuild-build-depends-core-dummy_0.invalid.0_amd64.deb ... Unpacking sbuild-build-depends-core-dummy (0.invalid.0) ... Setting up sbuild-build-depends-core-dummy (0.invalid.0) ... +------------------------------------------------------------------------------+ | Check architectures | +------------------------------------------------------------------------------+ Arch check ok (amd64 included in any) +------------------------------------------------------------------------------+ | Install package build dependencies | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: camlp5 (>= 7.01), ocaml-base-nox, dh-ocaml (>= 0.9~), debhelper (>= 9.0.0) Filtered Build-Depends: camlp5 (>= 7.01), ocaml-base-nox, dh-ocaml (>= 0.9~), debhelper (>= 9.0.0) dpkg-deb: building package 'sbuild-build-depends-hol-light-dummy' in '/<>/resolver-Vpdung/apt_archive/sbuild-build-depends-hol-light-dummy.deb'. dpkg-scanpackages: warning: Packages in archive but missing from override file: dpkg-scanpackages: warning: sbuild-build-depends-core-dummy sbuild-build-depends-hol-light-dummy dpkg-scanpackages: info: Wrote 2 entries to output Packages file. Ign:1 copy:/<>/resolver-Vpdung/apt_archive ./ InRelease Get:2 copy:/<>/resolver-Vpdung/apt_archive ./ Release [963 B] Ign:3 copy:/<>/resolver-Vpdung/apt_archive ./ Release.gpg Get:4 copy:/<>/resolver-Vpdung/apt_archive ./ Sources [523 B] Get:5 copy:/<>/resolver-Vpdung/apt_archive ./ Packages [605 B] Fetched 2091 B in 0s (0 B/s) Reading package lists... Reading package lists... Install hol-light build dependencies (apt-based resolver) --------------------------------------------------------- Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following additional packages will be installed: autoconf automake autopoint autotools-dev bsdmainutils camlp5 debhelper dh-autoreconf dh-ocaml dh-strip-nondeterminism file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcroco3 libfile-stripnondeterminism-perl libglib2.0-0 libicu57 libmagic-mgc libmagic1 libncurses-dev libncurses5-dev libncurses6 libncursesw6 libpipeline1 libsigsegv2 libtimedate-perl libtool libxml2 m4 man-db ocaml-base-nox ocaml-compiler-libs ocaml-interp ocaml-nox po-debconf Suggested packages: autoconf-archive gnu-standards autoconf-doc wamerican | wordlist whois vacation ocaml-findlib dh-make dwz git gettext-doc libasprintf-dev libgettextpo-dev groff libtool-doc gfortran | fortran95-compiler gcj-jdk m4-doc apparmor less www-browser ocaml-doc tuareg-mode | ocaml-mode libmail-box-perl Recommended packages: curl | wget | lynx libarchive-cpio-perl libglib2.0-data shared-mime-info xdg-user-dirs libgpm2 libltdl-dev ledit | readline-editor camlp4 libmail-sendmail-perl The following NEW packages will be installed: autoconf automake autopoint autotools-dev bsdmainutils camlp5 debhelper dh-autoreconf dh-ocaml dh-strip-nondeterminism file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcroco3 libfile-stripnondeterminism-perl libglib2.0-0 libicu57 libmagic-mgc libmagic1 libncurses-dev libncurses5-dev libncurses6 libncursesw6 libpipeline1 libsigsegv2 libtimedate-perl libtool libxml2 m4 man-db ocaml-base-nox ocaml-compiler-libs ocaml-interp ocaml-nox po-debconf sbuild-build-depends-hol-light-dummy 0 upgraded, 39 newly installed, 0 to remove and 0 not upgraded. Need to get 74.4 MB of archives. After this operation, 333 MB of additional disk space will be used. Get:1 copy:/<>/resolver-Vpdung/apt_archive ./ sbuild-build-depends-hol-light-dummy 0.invalid.0 [892 B] Get:2 http://127.0.0.1:9999/debian unstable/main amd64 bsdmainutils amd64 11.1.2 [190 kB] Get:3 http://127.0.0.1:9999/debian unstable/main amd64 groff-base amd64 1.22.3-10 [1176 kB] Get:4 http://127.0.0.1:9999/debian unstable/main amd64 libpipeline1 amd64 1.5.0-1 [29.0 kB] Get:5 http://127.0.0.1:9999/debian unstable/main amd64 man-db amd64 2.8.3-2 [1180 kB] Get:6 http://127.0.0.1:9999/debian unstable/main amd64 libmagic-mgc amd64 1:5.33-2 [234 kB] Get:7 http://127.0.0.1:9999/debian unstable/main amd64 libmagic1 amd64 1:5.33-2 [113 kB] Get:8 http://127.0.0.1:9999/debian unstable/main amd64 file amd64 1:5.33-2 [65.6 kB] Get:9 http://127.0.0.1:9999/debian unstable/main amd64 gettext-base amd64 0.19.8.1-6 [122 kB] Get:10 http://127.0.0.1:9999/debian unstable/main amd64 libsigsegv2 amd64 2.12-2 [32.8 kB] Get:11 http://127.0.0.1:9999/debian unstable/main amd64 m4 amd64 1.4.18-1 [202 kB] Get:12 http://127.0.0.1:9999/debian unstable/main amd64 autoconf all 2.69-11 [341 kB] Get:13 http://127.0.0.1:9999/debian unstable/main amd64 autotools-dev all 20180224.1 [77.0 kB] Get:14 http://127.0.0.1:9999/debian unstable/main amd64 automake all 1:1.15.1-3.1 [736 kB] Get:15 http://127.0.0.1:9999/debian unstable/main amd64 autopoint all 0.19.8.1-6 [434 kB] Get:16 http://127.0.0.1:9999/debian unstable/main amd64 ocaml-base-nox amd64 4.05.0-10 [655 kB] Get:17 http://127.0.0.1:9999/debian unstable/main amd64 libncurses6 amd64 6.1+20180210-2 [101 kB] Get:18 http://127.0.0.1:9999/debian unstable/main amd64 libncursesw6 amd64 6.1+20180210-2 [131 kB] Get:19 http://127.0.0.1:9999/debian unstable/main amd64 libncurses-dev amd64 6.1+20180210-2 [334 kB] Get:20 http://127.0.0.1:9999/debian unstable/main amd64 libncurses5-dev amd64 6.1+20180210-2 [924 B] Get:21 http://127.0.0.1:9999/debian unstable/main amd64 ocaml-interp amd64 4.05.0-10 [3581 kB] Get:22 http://127.0.0.1:9999/debian unstable/main amd64 ocaml-nox amd64 4.05.0-10 [27.6 MB] Get:23 http://127.0.0.1:9999/debian unstable/main amd64 ocaml-compiler-libs amd64 4.05.0-10 [19.0 MB] Get:24 http://127.0.0.1:9999/debian unstable/main amd64 camlp5 amd64 7.01-1+b1 [3175 kB] Get:25 http://127.0.0.1:9999/debian unstable/main amd64 libtool all 2.4.6-2.1 [547 kB] Get:26 http://127.0.0.1:9999/debian unstable/main amd64 dh-autoreconf all 17 [16.5 kB] Get:27 http://127.0.0.1:9999/debian unstable/main amd64 libarchive-zip-perl all 1.60-1 [95.6 kB] Get:28 http://127.0.0.1:9999/debian unstable/main amd64 libfile-stripnondeterminism-perl all 0.041-1 [19.9 kB] Get:29 http://127.0.0.1:9999/debian unstable/main amd64 libtimedate-perl all 2.3000-2 [42.2 kB] Get:30 http://127.0.0.1:9999/debian unstable/main amd64 dh-strip-nondeterminism all 0.041-1 [12.0 kB] Get:31 http://127.0.0.1:9999/debian unstable/main amd64 libglib2.0-0 amd64 2.56.1-2 [2928 kB] Get:32 http://127.0.0.1:9999/debian unstable/main amd64 libicu57 amd64 57.1-9 [7698 kB] Get:33 http://127.0.0.1:9999/debian unstable/main amd64 libxml2 amd64 2.9.4+dfsg1-6.1 [725 kB] Get:34 http://127.0.0.1:9999/debian unstable/main amd64 libcroco3 amd64 0.6.12-2 [144 kB] Get:35 http://127.0.0.1:9999/debian unstable/main amd64 gettext amd64 0.19.8.1-6 [1302 kB] Get:36 http://127.0.0.1:9999/debian unstable/main amd64 intltool-debian all 0.35.0+20060710.4 [26.3 kB] Get:37 http://127.0.0.1:9999/debian unstable/main amd64 po-debconf all 1.0.20 [247 kB] Get:38 http://127.0.0.1:9999/debian unstable/main amd64 debhelper all 11.2.1 [1013 kB] Get:39 http://127.0.0.1:9999/debian unstable/main amd64 dh-ocaml all 1.1.0 [83.3 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 74.4 MB in 1s (93.6 MB/s) Selecting previously unselected package bsdmainutils. (Reading database ... 10771 files and directories currently installed.) Preparing to unpack .../00-bsdmainutils_11.1.2_amd64.deb ... Unpacking bsdmainutils (11.1.2) ... Selecting previously unselected package groff-base. Preparing to unpack .../01-groff-base_1.22.3-10_amd64.deb ... Unpacking groff-base (1.22.3-10) ... Selecting previously unselected package libpipeline1:amd64. Preparing to unpack .../02-libpipeline1_1.5.0-1_amd64.deb ... Unpacking libpipeline1:amd64 (1.5.0-1) ... Selecting previously unselected package man-db. Preparing to unpack .../03-man-db_2.8.3-2_amd64.deb ... Unpacking man-db (2.8.3-2) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../04-libmagic-mgc_1%3a5.33-2_amd64.deb ... Unpacking libmagic-mgc (1:5.33-2) ... Selecting previously unselected package libmagic1:amd64. Preparing to unpack .../05-libmagic1_1%3a5.33-2_amd64.deb ... Unpacking libmagic1:amd64 (1:5.33-2) ... Selecting previously unselected package file. Preparing to unpack .../06-file_1%3a5.33-2_amd64.deb ... Unpacking file (1:5.33-2) ... Selecting previously unselected package gettext-base. Preparing to unpack .../07-gettext-base_0.19.8.1-6_amd64.deb ... Unpacking gettext-base (0.19.8.1-6) ... Selecting previously unselected package libsigsegv2:amd64. Preparing to unpack .../08-libsigsegv2_2.12-2_amd64.deb ... Unpacking libsigsegv2:amd64 (2.12-2) ... Selecting previously unselected package m4. Preparing to unpack .../09-m4_1.4.18-1_amd64.deb ... Unpacking m4 (1.4.18-1) ... Selecting previously unselected package autoconf. Preparing to unpack .../10-autoconf_2.69-11_all.deb ... Unpacking autoconf (2.69-11) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../11-autotools-dev_20180224.1_all.deb ... Unpacking autotools-dev (20180224.1) ... Selecting previously unselected package automake. Preparing to unpack .../12-automake_1%3a1.15.1-3.1_all.deb ... Unpacking automake (1:1.15.1-3.1) ... Selecting previously unselected package autopoint. Preparing to unpack .../13-autopoint_0.19.8.1-6_all.deb ... Unpacking autopoint (0.19.8.1-6) ... Selecting previously unselected package ocaml-base-nox. Preparing to unpack .../14-ocaml-base-nox_4.05.0-10_amd64.deb ... Unpacking ocaml-base-nox (4.05.0-10) ... Selecting previously unselected package libncurses6:amd64. Preparing to unpack .../15-libncurses6_6.1+20180210-2_amd64.deb ... Unpacking libncurses6:amd64 (6.1+20180210-2) ... Selecting previously unselected package libncursesw6:amd64. Preparing to unpack .../16-libncursesw6_6.1+20180210-2_amd64.deb ... Unpacking libncursesw6:amd64 (6.1+20180210-2) ... Selecting previously unselected package libncurses-dev:amd64. Preparing to unpack .../17-libncurses-dev_6.1+20180210-2_amd64.deb ... Unpacking libncurses-dev:amd64 (6.1+20180210-2) ... Selecting previously unselected package libncurses5-dev:amd64. Preparing to unpack .../18-libncurses5-dev_6.1+20180210-2_amd64.deb ... Unpacking libncurses5-dev:amd64 (6.1+20180210-2) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../19-ocaml-interp_4.05.0-10_amd64.deb ... Unpacking ocaml-interp (4.05.0-10) ... Selecting previously unselected package ocaml-nox. Preparing to unpack .../20-ocaml-nox_4.05.0-10_amd64.deb ... Unpacking ocaml-nox (4.05.0-10) ... Selecting previously unselected package ocaml-compiler-libs. Preparing to unpack .../21-ocaml-compiler-libs_4.05.0-10_amd64.deb ... Unpacking ocaml-compiler-libs (4.05.0-10) ... Selecting previously unselected package camlp5. Preparing to unpack .../22-camlp5_7.01-1+b1_amd64.deb ... Unpacking camlp5 (7.01-1+b1) ... Selecting previously unselected package libtool. Preparing to unpack .../23-libtool_2.4.6-2.1_all.deb ... Unpacking libtool (2.4.6-2.1) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../24-dh-autoreconf_17_all.deb ... Unpacking dh-autoreconf (17) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../25-libarchive-zip-perl_1.60-1_all.deb ... Unpacking libarchive-zip-perl (1.60-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../26-libfile-stripnondeterminism-perl_0.041-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (0.041-1) ... Selecting previously unselected package libtimedate-perl. Preparing to unpack .../27-libtimedate-perl_2.3000-2_all.deb ... Unpacking libtimedate-perl (2.3000-2) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../28-dh-strip-nondeterminism_0.041-1_all.deb ... Unpacking dh-strip-nondeterminism (0.041-1) ... Selecting previously unselected package libglib2.0-0:amd64. Preparing to unpack .../29-libglib2.0-0_2.56.1-2_amd64.deb ... Unpacking libglib2.0-0:amd64 (2.56.1-2) ... Selecting previously unselected package libicu57:amd64. Preparing to unpack .../30-libicu57_57.1-9_amd64.deb ... Unpacking libicu57:amd64 (57.1-9) ... Selecting previously unselected package libxml2:amd64. Preparing to unpack .../31-libxml2_2.9.4+dfsg1-6.1_amd64.deb ... Unpacking libxml2:amd64 (2.9.4+dfsg1-6.1) ... Selecting previously unselected package libcroco3:amd64. Preparing to unpack .../32-libcroco3_0.6.12-2_amd64.deb ... Unpacking libcroco3:amd64 (0.6.12-2) ... Selecting previously unselected package gettext. Preparing to unpack .../33-gettext_0.19.8.1-6_amd64.deb ... Unpacking gettext (0.19.8.1-6) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../34-intltool-debian_0.35.0+20060710.4_all.deb ... Unpacking intltool-debian (0.35.0+20060710.4) ... Selecting previously unselected package po-debconf. Preparing to unpack .../35-po-debconf_1.0.20_all.deb ... Unpacking po-debconf (1.0.20) ... Selecting previously unselected package debhelper. Preparing to unpack .../36-debhelper_11.2.1_all.deb ... Unpacking debhelper (11.2.1) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../37-dh-ocaml_1.1.0_all.deb ... Unpacking dh-ocaml (1.1.0) ... Selecting previously unselected package sbuild-build-depends-hol-light-dummy. Preparing to unpack .../38-sbuild-build-depends-hol-light-dummy_0.invalid.0_amd64.deb ... Unpacking sbuild-build-depends-hol-light-dummy (0.invalid.0) ... Setting up libarchive-zip-perl (1.60-1) ... Setting up libtimedate-perl (2.3000-2) ... Setting up libsigsegv2:amd64 (2.12-2) ... Setting up groff-base (1.22.3-10) ... Setting up libglib2.0-0:amd64 (2.56.1-2) ... No schema files found: doing nothing. Setting up libncursesw6:amd64 (6.1+20180210-2) ... Setting up ocaml-base-nox (4.05.0-10) ... Setting up dh-ocaml (1.1.0) ... Setting up gettext-base (0.19.8.1-6) ... Setting up libpipeline1:amd64 (1.5.0-1) ... Setting up m4 (1.4.18-1) ... Setting up libicu57:amd64 (57.1-9) ... Setting up libxml2:amd64 (2.9.4+dfsg1-6.1) ... Setting up libmagic-mgc (1:5.33-2) ... Setting up libmagic1:amd64 (1:5.33-2) ... Setting up libcroco3:amd64 (0.6.12-2) ... Processing triggers for libc-bin (2.27-3) ... Setting up autotools-dev (20180224.1) ... Setting up bsdmainutils (11.1.2) ... update-alternatives: using /usr/bin/bsd-write to provide /usr/bin/write (write) in auto mode update-alternatives: using /usr/bin/bsd-from to provide /usr/bin/from (from) in auto mode Setting up libncurses6:amd64 (6.1+20180210-2) ... Setting up autopoint (0.19.8.1-6) ... Setting up libfile-stripnondeterminism-perl (0.041-1) ... Setting up gettext (0.19.8.1-6) ... Setting up autoconf (2.69-11) ... Setting up file (1:5.33-2) ... Setting up intltool-debian (0.35.0+20060710.4) ... Setting up automake (1:1.15.1-3.1) ... update-alternatives: using /usr/bin/automake-1.15 to provide /usr/bin/automake (automake) in auto mode Setting up man-db (2.8.3-2) ... Not building database; man-db/auto-update is not 'true'. Setting up libncurses-dev:amd64 (6.1+20180210-2) ... Setting up libtool (2.4.6-2.1) ... Setting up po-debconf (1.0.20) ... Setting up libncurses5-dev:amd64 (6.1+20180210-2) ... Setting up dh-autoreconf (17) ... Setting up ocaml-interp (4.05.0-10) ... Setting up debhelper (11.2.1) ... Setting up ocaml-nox (4.05.0-10) ... Setting up dh-strip-nondeterminism (0.041-1) ... Setting up ocaml-compiler-libs (4.05.0-10) ... Setting up camlp5 (7.01-1+b1) ... Setting up sbuild-build-depends-hol-light-dummy (0.invalid.0) ... Processing triggers for libc-bin (2.27-3) ... +------------------------------------------------------------------------------+ | Build environment | +------------------------------------------------------------------------------+ Kernel: Linux 4.9.0-5-amd64 amd64 (x86_64) Toolchain package versions: binutils_2.30-16 dpkg-dev_1.19.0.5 g++-7_7.3.0-17 gcc-7_7.3.0-17 libc6-dev_2.27-3 libstdc++-7-dev_7.3.0-17 libstdc++6_8-20180425-1 linux-libc-dev_4.15.17-1 Package versions: adduser_3.117 apt_1.6.1 autoconf_2.69-11 automake_1:1.15.1-3.1 autopoint_0.19.8.1-6 autotools-dev_20180224.1 base-files_10.1 base-passwd_3.5.45 bash_4.4.18-2 binutils_2.30-16 binutils-common_2.30-16 binutils-x86-64-linux-gnu_2.30-16 bsdmainutils_11.1.2 bsdutils_1:2.31.1-0.5 build-essential_12.5 bzip2_1.0.6-8.1 camlp5_7.01-1+b1 clang-6.0_1:6.0-3 coreutils_8.28-1 cpp_4:7.3.0-3 cpp-7_7.3.0-17 dash_0.5.8-2.10 debconf_1.5.66 debfoster_2.7-2.1+b1 debhelper_11.2.1 debian-archive-keyring_2017.7 debianutils_4.8.4 dh-autoreconf_17 dh-ocaml_1.1.0 dh-strip-nondeterminism_0.041-1 diffutils_1:3.6-1 dpkg_1.19.0.5 dpkg-dev_1.19.0.5 e2fslibs_1.44.1-2 e2fsprogs_1.44.1-2 eatmydata_105-6 fakeroot_1.22-2 fdisk_2.31.1-0.5 file_1:5.33-2 findutils_4.6.0+git+20171230-2 g++_4:7.3.0-3 g++-7_7.3.0-17 gcc_4:7.3.0-3 gcc-6-base_6.4.0-17 gcc-7_7.3.0-17 gcc-7-base_7.3.0-17 gcc-8-base_8-20180425-1 gettext_0.19.8.1-6 gettext-base_0.19.8.1-6 gpgv_2.2.5-1 grep_3.1-2 groff-base_1.22.3-10 gzip_1.6-5+b1 hostname_3.20 init-system-helpers_1.51 intltool-debian_0.35.0+20060710.4 lib32gcc1_1:8-20180425-1 lib32stdc++6_8-20180425-1 libacl1_2.2.52-3+b1 libapt-pkg5.0_1.6.1 libarchive-zip-perl_1.60-1 libasan4_7.3.0-17 libatomic1_8-20180425-1 libattr1_1:2.4.47-2+b2 libaudit-common_1:2.8.3-1 libaudit1_1:2.8.3-1 libbinutils_2.30-16 libblkid1_2.31.1-0.5 libbsd0_0.8.7-1 libbz2-1.0_1.0.6-8.1 libc-bin_2.27-3 libc-dev-bin_2.27-3 libc6_2.27-3 libc6-dev_2.27-3 libc6-i386_2.27-3 libcap-ng0_0.7.9-1 libcc1-0_8-20180425-1 libcilkrts5_7.3.0-17 libclang-common-6.0-dev_1:6.0-3 libclang1-6.0_1:6.0-3 libcom-err2_1.44.1-2 libcomerr2_1.44.1-2 libcroco3_0.6.12-2 libdb5.3_5.3.28-13.1+b1 libdebconfclient0_0.243 libdpkg-perl_1.19.0.5 libeatmydata1_105-6 libedit2_3.1-20170329-1 libext2fs2_1.44.1-2 libfakeroot_1.22-2 libfdisk1_2.31.1-0.5 libffi6_3.2.1-8 libfile-stripnondeterminism-perl_0.041-1 libgc1c2_1:7.4.2-8.2 libgcc-7-dev_7.3.0-17 libgcc1_1:8-20180425-1 libgcrypt20_1.8.2-2 libgdbm-compat4_1.14.1-6 libgdbm3_1.8.3-14 libgdbm5_1.14.1-6 libglib2.0-0_2.56.1-2 libgmp10_2:6.1.2+dfsg-3 libgnutls30_3.5.18-1 libgomp1_8-20180425-1 libgpg-error0_1.29-4 libhogweed4_3.4-1 libicu57_57.1-9 libidn2-0_2.0.4-1.1 libisl15_0.18-4 libisl19_0.19-1 libitm1_8-20180425-1 libjsoncpp1_1.7.4-3 libllvm6.0_1:6.0-3 liblsan0_8-20180425-1 liblz4-1_1.8.1.2-1 liblzma5_5.2.2-1.3 libmagic-mgc_1:5.33-2 libmagic1_1:5.33-2 libmount1_2.31.1-0.5 libmpc3_1.1.0-1 libmpfr4_3.1.6-1 libmpfr6_4.0.1-1 libmpx2_8-20180425-1 libncurses-dev_6.1+20180210-2 libncurses5_6.1+20180210-2 libncurses5-dev_6.1+20180210-2 libncurses6_6.1+20180210-2 libncursesw5_6.1+20180210-2 libncursesw6_6.1+20180210-2 libnettle6_3.4-1 libobjc-7-dev_7.3.0-17 libobjc4_8-20180425-1 libp11-kit0_0.23.10-2 libpam-modules_1.1.8-3.7 libpam-modules-bin_1.1.8-3.7 libpam-runtime_1.1.8-3.7 libpam0g_1.1.8-3.7 libpcre3_2:8.39-9 libperl5.26_5.26.2-3 libpipeline1_1.5.0-1 libquadmath0_8-20180425-1 libseccomp2_2.3.3-1 libselinux1_2.7-2+b2 libsemanage-common_2.7-2 libsemanage1_2.7-2+b2 libsepol1_2.7-1 libsigsegv2_2.12-2 libsmartcols1_2.31.1-0.5 libss2_1.44.1-2 libstdc++-7-dev_7.3.0-17 libstdc++6_8-20180425-1 libsystemd0_238-4 libtasn1-6_4.13-2 libtimedate-perl_2.3000-2 libtinfo5_6.1+20180210-2 libtinfo6_6.1+20180210-2 libtool_2.4.6-2.1 libtsan0_8-20180425-1 libubsan0_7.3.0-17 libudev1_238-4 libunistring2_0.9.8-1 libustr-1.0-1_1.0.4-6 libuuid1_2.31.1-0.5 libxml2_2.9.4+dfsg1-6.1 libzstd1_1.3.4+dfsg-1 linux-libc-dev_4.15.17-1 login_1:4.5-1 m4_1.4.18-1 make_4.2.1-1 man-db_2.8.3-2 mawk_1.3.3-17+b3 mount_2.31.1-0.5 multiarch-support_2.27-3 ncurses-base_6.1+20180210-2 ncurses-bin_6.1+20180210-2 ocaml-base-nox_4.05.0-10 ocaml-compiler-libs_4.05.0-10 ocaml-interp_4.05.0-10 ocaml-nox_4.05.0-10 passwd_1:4.5-1 patch_2.7.6-2 perl_5.26.2-3 perl-base_5.26.2-3 perl-modules-5.26_5.26.2-3 po-debconf_1.0.20 sbuild-build-depends-core-dummy_0.invalid.0 sbuild-build-depends-hol-light-dummy_0.invalid.0 sed_4.4-2 sensible-utils_0.0.12 sysvinit-utils_2.88dsf-59.10 tar_1.30+dfsg-1 util-linux_2.31.1-0.5 xz-utils_5.2.2-1.3 zlib1g_1:1.2.11.dfsg-1 +------------------------------------------------------------------------------+ | Build | +------------------------------------------------------------------------------+ Unpack source ------------- gpgv: unknown type of key resource 'trustedkeys.kbx' gpgv: keyblock resource '/sbuild-nonexistent/.gnupg/trustedkeys.kbx': General error gpgv: Signature made Thu Aug 3 01:19:17 2017 UTC gpgv: using RSA key CAC2D8B9CD2CA5F9 gpgv: Can't check signature: No public key dpkg-source: warning: failed to verify signature on ./hol-light_20170109-2.dsc dpkg-source: info: extracting hol-light in /<> dpkg-source: info: unpacking hol-light_20170109.orig.tar.gz dpkg-source: info: unpacking hol-light_20170109-2.debian.tar.xz dpkg-source: info: applying default-hollight-dir dpkg-source: info: applying holtest-no-proof-recording.patch dpkg-source: info: applying cd-holtest-parallel.patch dpkg-source: info: applying camlp5-7.patch Check disk space ---------------- Sufficient free space for build User Environment ---------------- APT_CONFIG=/var/lib/sbuild/apt.conf HOME=/sbuild-nonexistent LANG=en_US.UTF-8 LC_ALL=POSIX LOGNAME=user42 PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SCHROOT_ALIAS_NAME=unstable-amd64-sbuild SCHROOT_CHROOT_NAME=unstable-amd64-sbuild SCHROOT_COMMAND=env SCHROOT_GID=1001 SCHROOT_GROUP=user42 SCHROOT_SESSION_ID=unstable-amd64-sbuild-0146b459-eed1-42b5-9406-88612449840c SCHROOT_UID=1001 SCHROOT_USER=user42 SHELL=/bin/sh USER=user42 dpkg-buildpackage ----------------- dpkg-buildpackage: info: source package hol-light dpkg-buildpackage: info: source version 20170109-2 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Hendrik Tews dpkg-source --before-build hol-light-20170109 dpkg-buildpackage: info: host architecture amd64 fakeroot debian/rules clean dh clean --with ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/<>' dh_auto_clean make -j1 clean make[2]: Entering directory '/<>' rm -f pa_j.ml pa_j.cmi pa_j.cmo hol hol.multivariate hol.sosa hol.card hol.complex; make[2]: Leaving directory '/<>' make -C Mizarlight clean make[2]: Entering directory '/<>/Mizarlight' rm -f pa_f.cmi pa_f.cmo make[2]: Leaving directory '/<>/Mizarlight' make[1]: Leaving directory '/<>' dh_ocamlclean dh_clean debian/rules build-arch dh build-arch --with ocaml dh_update_autotools_config -a dh_ocamlinit -a dh_auto_configure -a debian/rules override_dh_auto_build make[1]: Entering directory '/<>' cp pa_j_3.1x_6.11.ml pa_j.ml make make[2]: Entering directory '/<>' if test `ocamlc -version | cut -c1-3` = "3.0" ; \ then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I `camlp4 -where` pa_j.ml ; \ else if test `ocamlc -version | cut -c1-3` = "3.1" -o `ocamlc -version | cut -c1-4` = "4.00" -o `ocamlc -version | cut -c1-4` = "4.01" -o `ocamlc -version | cut -c1-4` = "4.02" -o `ocamlc -version | cut -c1-4` = "4.03" ; \ then ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \ else ocamlc -safe-string -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \ fi \ fi File "pa_j.ml", line 806, characters 23-39: Warning 3: deprecated: String.uppercase Use String.uppercase_ascii instead. File "pa_j.ml", line 807, characters 28-44: Warning 3: deprecated: String.lowercase Use String.lowercase_ascii instead. make[2]: Leaving directory '/<>' make[1]: Leaving directory '/<>' debian/rules override_dh_auto_test make[1]: Entering directory '/<>' debian/test-hol-light ######################## HOL Light test Library/agm.ml ################### OCaml version 4.05.0 File "/<>/fusion.ml", line 238, characters 19-71: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Tyapp ("fun", _::_::_::_)|Tyapp ("fun", _::[])|Tyapp ("fun", [])| Tyapp ("", _)|Tyvar _) File "/<>/fusion.ml", line 235, characters 4-189: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Abs ((Const (_, _)|Comb (_, _)|Abs (_, _)), _) File "/<>/fusion.ml", line 330, characters 4-231: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Abs ((Const (_, _)|Comb (_, _)|Abs (_, _)), _) File "/<>/fusion.ml", line 443, characters 4-551: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ((Abs (Var (_, _), _), Abs ((Const (_, _)|Comb (_, _)|Abs (_, _)), _))| (Abs ((Const (_, _)|Comb (_, _)|Abs (_, _)), _), Abs (_, _))) File "fusion.ml" already loaded File "/<>/basics.ml", line 149, characters 18-24: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/basics.ml", line 171, characters 6-18: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (("fun", _::_::_::_)|("fun", _::[])|("fun", [])|("", _)) File "basics.ml" already loaded File "/<>/nets.ml", line 59, characters 52-61: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "nets.ml" already loaded File "/<>/printer.ml", line 200, characters 26-116: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/printer.ml", line 284, characters 14-177: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/printer.ml", line 357, characters 11-316: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/printer.ml", line 358, characters 11-294: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/printer.ml", line 458, characters 4-194: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "/<>/printer.ml", line 465, characters 4-313: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::[]|[]) File "printer.ml" already loaded File "/<>/preterm.ml", line 365, characters 4-462: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Typing (_, _) File "/<>/preterm.ml", line 382, characters 4-499: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Typing (_, _) File "preterm.ml" already loaded File "/<>/parser.ml", line 277, characters 15-60: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Combp (Combp (Varp ("", _), _), _)| Combp (Combp ((Constp (_, _)|Combp (_, _)|Absp (_, _)|Typing (_, _)), _), _)| Combp ((Varp (_, _)|Constp (_, _)|Absp (_, _)|Typing (_, _)), _)|Varp (_, _)| Constp (_, _)|Absp (_, _)|Typing (_, _)) File "/<>/parser.ml", line 333, characters 10-65: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Resword _ File "/<>/parser.ml", line 353, characters 24-164: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/parser.ml", line 354, characters 24-117: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/parser.ml", line 483, characters 12-128: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/parser.ml", line 484, characters 12-93: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "printer.ml" already loaded File "equal.ml" already loaded File "bool.ml" already loaded File "/<>/drule.ml", line 168, characters 17-23: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/drule.ml", line 173, characters 17-23: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/drule.ml", line 185, characters 21-27: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/drule.ml", line 201, characters 24-102: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/drule.ml", line 304, characters 19-25: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/drule.ml", line 309, characters 19-25: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "drule.ml" already loaded File "/<>/tactics.ml", line 125, characters 7-98: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/tactics.ml", line 134, characters 24-31: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "/<>/tactics.ml", line 135, characters 25-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "/<>/tactics.ml", line 177, characters 31-41: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 246, characters 10-54: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 323, characters 25-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "/<>/tactics.ml", line 345, characters 28-68: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 364, characters 14-113: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 374, characters 14-43: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_|_::[]|[]) File "/<>/tactics.ml", line 423, characters 14-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 428, characters 14-61: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 434, characters 10-47: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 440, characters 14-52: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_|_::[]|[]) File "/<>/tactics.ml", line 448, characters 13-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 454, characters 14-47: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 475, characters 14-37: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 488, characters 16-59: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 494, characters 10-61: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 518, characters 39-64: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_|_::[]|[]) File "/<>/tactics.ml", line 524, characters 32-66: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 530, characters 34-68: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 541, characters 16-71: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_|_::[]|[]) File "/<>/tactics.ml", line 545, characters 25-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "/<>/tactics.ml", line 552, characters 25-50: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "/<>/tactics.ml", line 577, characters 29-66: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 707, characters 14-65: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 720, characters 10-59: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 846, characters 16-47: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) File "/<>/tactics.ml", line 909, characters 6-27: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "/<>/tactics.ml", line 917, characters 6-17: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "tactics.ml" already loaded File "/<>/itab.ml", line 20, characters 8-31: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_ File "itab.ml" already loaded File "/<>/simp.ml", line 95, characters 2-1072: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (Comb (Const ("", _), _), Comb (Comb (Const ("", _), _), _))| Comb (Comb (Const ("", _), _), Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), _))| Comb (Comb (Const ("", _), _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (Comb (Const ("", _), _), (Var (_, _)|Const (_, _)|Abs (_, _)))| Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), Comb (Comb (Const ("", _), _), _))| Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), _))| Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), (Var (_, _)|Const (_, _)|Abs (_, _)))| Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)|Var (_, _)|Const (_, _)| Abs (_, _)) Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Warning: inventing type variables Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 File "simp.ml" already loaded Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 2 Warning: inventing type variables Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Warning: inventing type variables Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 5 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 5 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Warning: inventing type variables Searching with limit 0 Searching with limit 1 Searching with limit 2 File "theorems.ml" already loaded File "/<>/ind_defs.ml", line 84, characters 10-14: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "/<>/ind_defs.ml", line 262, characters 32-69: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_|[]) Searching with limit 0 Searching with limit 1 File "ind_defs.ml" already loaded File "/<>/class.ml", line 89, characters 26-150: Warning 3: deprecated: Pervasives.& Use (&&) instead. Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables File "class.ml" already loaded File "trivia.ml" already loaded File "/<>/canon.ml", line 117, characters 6-51: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) Warning: inventing type variables Warning: inventing type variables File "canon.ml" already loaded File "/<>/meson.ml", line 234, characters 30-36: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 246, characters 23-29: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 252, characters 23-29: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 269, characters 23-29: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 274, characters 23-29: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 304, characters 17-23: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 329, characters 31-37: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/meson.ml", line 431, characters 20-25: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "meson.ml" already loaded File "meson.ml" already loaded 0..0..1..3..7..15..26..54..86..136..solved at 208 0..0..1..solved at 4 0..0..solved at 2 0..0..1..4..solved at 10 0..0..1..4..9..solved at 21 0..0..solved at 2 0..0..1..solved at 4 0..0..1..2..6..11..22..38..70..solved at 116 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..11..22..41..76..solved at 108 0..0..1..solved at 4 0..0..solved at 2 File "/<>/impconv.ml", line 313, characters 8-174: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Var_ (_, _)|Const_ (_, _, _)) File "/<>/impconv.ml", line 454, characters 22-45: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "/<>/impconv.ml", line 1088, characters 18-34: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/impconv.ml", line 1116, characters 18-34: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/impconv.ml", line 1596, characters 19-36: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "/<>/impconv.ml", line 1749, characters 8-13: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "/<>/impconv.ml", line 1778, characters 16-27: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_, []) File "quot.ml" already loaded Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..1..2..6..11..solved at 22 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..1..5..13..solved at 26 0..0..1..5..13..solved at 26 0..0..solved at 2 Warning: inventing type variables File "pair.ml" already loaded 0..0..2..solved at 5 0..0..solved at 2 0..0..1..3..solved at 9 0..0..1..2..5..9..15..29..44..68..142..260..solved at 420 File "/<>/nums.ml", line 156, characters 4-39: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) 0..0..solved at 3 0..0..solved at 2 File "/<>/nums.ml", line 267, characters 8-71: Warning 10: this expression should have type unit. File "nums.ml" already loaded File "recursion.ml" already loaded 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..7..14..35..62..solved at 73 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..7..14..35..62..solved at 73 0..0..2..12..solved at 18 0..0..1..5..13..27..solved at 33 0..0..1..5..11..22..49..95..171..305..solved at 319 0..0..3..13..37..solved at 48 0..0..3..solved at 8 0..0..2..8..solved at 23 0..0..solved at 2 0..0..0..1..3..5..solved at 10 0..0..1..3..solved at 7 0..0..1..2..3..7..13..21..solved at 31 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 3 Searching with limit 4 Searching with limit 0 Searching with limit 1 Searching with limit 2 Searching with limit 0 Searching with limit 1 0..0..1..4..solved at 10 0..0..2..8..31..79..254..629..1685..solved at 3183 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..1..4..13..29..74..solved at 99 0..0..1..4..19..49..130..solved at 165 0..0..3..10..29..63..170..solved at 283 0..0..solved at 2 0..0..solved at 5 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 7 0..0..2..4..solved at 10 0..0..solved at 2 0..0..solved at 2 0..0..4..8..solved at 17 0..0..2..4..solved at 11 0..0..solved at 2 0..0..solved at 3 0..0..6..12..solved at 24 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..2..7..16..32..solved at 45 0..0..2..solved at 5 0..0..2..solved at 5 0..0..2..6..15..solved at 21 0..0..2..6..15..57..160..883..4135..solved at 8792 0..0..2..solved at 5 0..0..2..6..13..45..solved at 52 0..0..2..solved at 5 0..0..2..6..18..42..solved at 52 0..0..1..solved at 4 0..0..2..4..solved at 8 0..0..1..3..5..10..19..31..52..solved at 74 0..0..2..4..10..24..solved at 34 0..0..solved at 2 0..0..solved at 2 0..0..2..7..solved at 11 0..0..2..4..solved at 9 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..1..2..solved at 6 0..0..2..6..17..solved at 25 0..0..2..solved at 5 0..0..2..solved at 6 0..0..2..5..11..22..40..solved at 53 0..0..1..solved at 4 0..0..3..6..14..32..57..102..188..solved at 204 0..0..3..6..22..41..72..122..175..248..386..solved at 407 0..0..1..2..6..11..19..32..45..60..solved at 73 0..0..1..2..6..11..19..32..45..60..solved at 73 0..0..1..3..6..15..34..67..132..266..solved at 510 0..0..1..3..6..13..29..59..110..solved at 162 0..0..1..3..6..15..34..68..130..solved at 182 0..0..1..3..6..15..34..67..132..266..solved at 510 0..0..3..10..solved at 15 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..2..solved at 7 0..0..2..5..solved at 17 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..0..1..solved at 9 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 5 0..0..1..5..16..32..solved at 40 0..0..1..5..18..37..solved at 48 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..2..solved at 7 0..0..2..5..solved at 17 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..0..1..solved at 9 0..0..solved at 2 0..0..solved at 2 0..0..2..5..14..66..287..1310..solved at 1325 0..0..solved at 3 0..0..2..5..16..72..302..solved at 311 0..0..1..2..3..7..12..17..23..29..35..solved at 84 0..0..1..2..solved at 6 0..0..solved at 2 0..0..2..4..7..solved at 21 0..0..2..4..solved at 10 0..0..0..0..1..solved at 7 0..0..solved at 2 0..0..solved at 2 0..0..0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..10..19..32..55..112..263..solved at 489 0..0..0..1..2..3..solved at 8 0..0..0..1..2..3..7..14..22..33..57..84..141..221..305..441..638..849..solved at 1042 0..0..0..1..2..3..4..5..6..11..16..21..40..59..78..103..128..153..192..231..270..358..446..534..650..766..882..1036..1190..1344..solved at 3172 File "arith.ml" already loaded 0..0..solved at 2 0..0..solved at 2 0..0..0..0..2..5..8..25..57..89..solved at 97 0..0..0..1..5..10..solved at 15 0..0..0..0..2..5..8..25..57..89..solved at 97 0..0..solved at 2 0..0..2..10..25..solved at 35 0..0..0..1..4..7..solved at 12 0..0..solved at 2 0..0..0..3..6..9..solved at 16 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..3..solved at 7 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 3 0..0..2..4..8..solved at 13 0..0..solved at 3 0..0..2..4..8..solved at 13 0..0..solved at 3 0..0..solved at 2 0..0..2..10..25..solved at 35 0..0..solved at 2 0..0..1..3..11..solved at 20 0..0..1..2..4..12..24..45..78..125..solved at 140 0..0..0..2..7..solved at 12 0..0..1..3..13..29..63..128..226..388..642..977..1459..2097..3319..solved at 3649 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 2 0..0..1..4..15..41..98..211..420..solved at 656 0..0..1..2..5..9..17..33..55..97..162..262..411..solved at 543 0..0..1..6..23..68..172..410..880..solved at 911 0..0..0..1..4..7..solved at 16 0..0..2..8..24..54..solved at 69 0..0..1..solved at 6 0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables 0..0..2..8..solved at 12 0..0..2..8..solved at 13 0..0..solved at 2 0..0..0..solved at 3 0..0..0..solved at 5 0..0..0..0..solved at 4 0..0..solved at 2 0..0..3..7..20..54..150..solved at 180 0..0..solved at 2 0..0..2..6..solved at 13 0..0..1..3..solved at 7 0..0..1..3..solved at 8 0..0..2..6..solved at 14 0..0..1..3..solved at 8 0..0..2..4..solved at 11 0..0..5..12..39..solved at 71 0..0..4..10..30..solved at 55 0..0..5..13..38..solved at 66 0..0..4..10..31..solved at 57 0..0..3..6..19..35..60..118..solved at 270 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..5..15..51..120..259..solved at 434 0..0..1..5..15..51..120..259..solved at 394 0..0..1..4..13..31..solved at 37 0..0..1..2..solved at 6 0..0..1..5..15..51..120..259..solved at 394 0..0..1..5..15..51..120..259..solved at 434 0..0..1..4..12..28..58..118..solved at 128 0..0..2..9..28..85..206..492..solved at 618 0..0..2..9..28..94..222..491..1165..solved at 1499 0..0..2..9..28..94..223..491..1149..solved at 1472 0..0..2..10..28..82..204..solved at 236 0..0..1..4..11..43..116..246..648..1354..solved at 1611 0..0..solved at 2 0..0..1..5..15..51..120..259..solved at 434 0..0..1..5..15..51..120..259..solved at 394 0..0..1..4..13..31..solved at 37 0..0..2..7..24..55..104..223..440..827..1504..solved at 1616 0..0..2..7..24..65..133..290..574..solved at 904 0..0..2..7..24..65..134..294..583..solved at 913 0..0..2..8..25..52..110..solved at 145 0..0..1..2..7..13..26..50..83..132..216..308..447..705..1020..1530..2268..3184..4455..6310..solved at 8365 0..0..1..3..9..17..43..86..154..300..472..714..1138..1664..2466..4129..6181..solved at 6305 0..0..2..7..20..49..89..185..solved at 215 0..0..1..2..7..17..34..70..132..223..396..solved at 427 0..0..1..2..6..12..23..46..74..119..197..285..418..630..886..solved at 1210 0..0..2..8..24..solved at 32 0..0..2..7..24..61..134..280..548..1144..solved at 1169 0..0..3..solved at 7 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..solved at 2 File "wf.ml" already loaded File "/<>/calc_num.ml", line 209, characters 6-58: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 246, characters 4-177: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (Const ("", _), _)|Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _)| Const ("", _)|Var (_, _)|Abs (_, _)) File "/<>/calc_num.ml", line 267, characters 6-630: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ((Comb (Const ("BIT1", _), _), Const ("", _))| (Comb (Const ("BIT1", _), _), Comb (Const ("", _), _))| (Comb (Const ("BIT1", _), _), Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _))| (Comb (Const ("BIT1", _), _), (Var (_, _)|Abs (_, _)))| (Comb (Const ("BIT0", _), _), Const ("", _))| (Comb (Const ("BIT0", _), _), Comb (Const ("", _), _))| (Comb (Const ("BIT0", _), _), Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _))| (Comb (Const ("BIT0", _), _), (Var (_, _)|Abs (_, _)))| (Comb (Const ("", _), _), Const ("", _))| (Comb (Const ("", _), _), (Var (_, _)|Comb (_, _)|Abs (_, _)))| (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), Const ("", _))| (Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _), (Var (_, _)|Comb (_, _)|Abs (_, _)))|(Const ("", _), Const ("", _))| (Const ("", _), (Var (_, _)|Comb (_, _)|Abs (_, _)))| ((Var (_, _)|Abs (_, _)), Const ("", _))| ((Var (_, _)|Abs (_, _)), (Var (_, _)|Comb (_, _)|Abs (_, _)))) File "/<>/calc_num.ml", line 386, characters 13-146: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Var (_, _)|Const (_, _)|Abs (_, _)) File "/<>/calc_num.ml", line 390, characters 13-146: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Var (_, _)|Const (_, _)|Abs (_, _)) File "/<>/calc_num.ml", line 382, characters 6-479: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: 4 File "/<>/calc_num.ml", line 405, characters 13-146: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Var (_, _)|Const (_, _)|Abs (_, _)) File "/<>/calc_num.ml", line 409, characters 13-146: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Var (_, _)|Const (_, _)|Abs (_, _)) File "/<>/calc_num.ml", line 401, characters 6-479: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: 4 File "/<>/calc_num.ml", line 560, characters 10-489: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)))| Comb (_, Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 571, characters 12-345: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)))| Comb (_, Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 579, characters 12-199: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)))| Comb (_, Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 585, characters 12-197: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)))| Comb (_, Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 686, characters 20-49: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 913, characters 20-229: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (_, Comb (_, Comb (_, Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))))| Comb (_, Comb (_, Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))))| Comb (_, Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (_, (Var (_, _)|Const (_, _)|Abs (_, _)))|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 920, characters 18-57: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _)))| Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 945, characters 18-111: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Comb (Comb (_, _), Comb (Comb (_, _), Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))))| Comb (Comb (_, _), Comb (Comb (_, _), Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _)))))| Comb (Comb (_, _), Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)))| Comb (Comb (_, _), Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _))))| Comb (Comb (_, _), Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _))| Comb (Comb (_, _), (Var (_, _)|Const (_, _)|Abs (_, _)))| Comb ((Var (_, _)|Const (_, _)|Abs (_, _)), _)|Var (_, _)|Const (_, _)| Abs (_, _)) File "/<>/calc_num.ml", line 964, characters 18-31: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) File "/<>/calc_num.ml", line 882, characters 6-4505: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Const ("", _)|Comb (Const ("", _), _)| Comb ((Var (_, _)|Comb (_, _)|Abs (_, _)), _)|Var (_, _)|Abs (_, _)) 0..0..1..2..8..18..solved at 48 0..0..1..2..8..18..solved at 55 0..0..1..2..10..24..118..279..1321..3190..solved at 4661 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..2..6..12..28..51..solved at 84 0..0..1..2..6..12..28..57..solved at 90 0..0..1..solved at 4 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..8..18..68..147..solved at 443 0..0..1..2..8..18..67..146..solved at 427 0..0..1..2..8..18..solved at 55 0..0..1..2..8..18..solved at 48 0..0..1..2..7..14..solved at 23 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..3..12..31..100..solved at 139 0..0..1..2..solved at 8 0..0..1..2..6..13..29..solved at 39 0..0..1..2..6..12..28..51..solved at 80 0..0..1..2..6..13..29..solved at 39 0..0..1..2..6..12..28..51..solved at 80 0..0..1..2..7..15..35..77..161..solved at 177 0..0..1..2..6..12..28..51..104..192..solved at 349 0..0..1..solved at 4 0..0..1..2..3..solved at 8 0..0..solved at 2 0..0..1..2..3..solved at 8 0..0..1..solved at 4 0..0..2..solved at 5 0..0..2..solved at 6 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..solved at 5 0..0..solved at 2 0..0..1..solved at 4 File "calc_num.ml" already loaded File "/<>/normalizer.ml", line 96, characters 5-371: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::_::_::_::_::_::_::_| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_:: _::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::[]|_::_::_::_::_::_::[]| _::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]|_::_::[]|_::[]|[]) 0..0..solved at 2 0..0..1..2..solved at 9 0..0..1..2..9..20..73..154..solved at 284 0..0..1..2..solved at 8 0..0..solved at 2 0..0..1..2..solved at 8 0..0..1..2..9..20..73..154..solved at 229 0..0..1..2..8..18..65..140..472..992..solved at 2047 0..0..0..1..2..3..4..5..6..solved at 20 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 File "normalizer.ml" already loaded File "/<>/grobner.ml", line 200, characters 48-259: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/grobner.ml", line 201, characters 21-185: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/grobner.ml", line 202, characters 21-135: Warning 3: deprecated: Pervasives.& Use (&&) instead. File "/<>/grobner.ml", line 521, characters 14-28: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_, []) File "/<>/grobner.ml", line 618, characters 12-88: Warning 3: deprecated: Pervasives.& Use (&&) instead. 0..0..2..4..10..20..52..96..204..356..638..1042..1916..3036..solved at 4498 0..0..1..2..7..16..42..78..161..285..685..solved at 954 0..0..1..2..7..16..42..78..160..281..solved at 672 0..0..2..4..11..21..59..116..239..426..800..1336..solved at 1840 0..0..1..2..7..16..45..86..174..312..724..solved at 772 0..0..1..2..7..16..44..84..168..solved at 185 0..0..2..4..11..21..59..116..239..426..solved at 540 0..0..1..2..7..18..46..solved at 77 0..0..1..2..7..18..47..92..185..solved at 281 0..0..2..4..12..22..solved at 41 0..0..1..2..7..solved at 21 0..0..1..2..7..solved at 18 File "grobner.ml" already loaded Searching with limit 0 Searching with limit 1 Searching with limit 2 File "/<>/ind_types.ml", line 796, characters 12-23: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ((_, _::_::_::_)|(_, _::[])|(_, [])) File "/<>/ind_types.ml", line 807, characters 12-23: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ((_, _::_::_::_)|(_, _::[])|(_, [])) 0..0..1..2..6..13..30..solved at 70 0..0..1..2..6..13..30..solved at 70 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..6..11..solved at 22 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 Warning: inventing type variables File "/<>/ind_types.ml", line 1459, characters 22-191: Warning 3: deprecated: Pervasives.& Use (&&) instead. Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 5 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables File "/<>/ind_types.ml", line 1540, characters 10-143: Warning 3: deprecated: Pervasives.& Use (&&) instead. Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 File "ind_types.ml" already loaded Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..10..19..32..55..112..263..solved at 489 Warning: inventing type variables 0..0..0..0..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..6..12..solved at 26 Warning: inventing type variables 0..0..2..4..solved at 9 0..0..2..4..solved at 9 0..0..solved at 3 0..0..solved at 3 0..0..1..2..solved at 7 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..3..6..solved at 10 0..0..3..6..solved at 13 0..0..solved at 2 0..0..3..6..solved at 10 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 5 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..3..solved at 7 0..0..3..solved at 7 0..0..solved at 2 0..0..solved at 4 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 5 0..0..solved at 3 0..0..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables 0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 0..0..1..solved at 6 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 3 0..0..3..solved at 9 0..0..1..solved at 7 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..2..4..10..20..40..solved at 67 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 0..0..1..2..solved at 6 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..1..2..6..12..27..solved at 44 Warning: inventing type variables Warning: inventing type variables 0..0..2..solved at 6 0..0..1..solved at 4 0..0..2..solved at 6 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..9..15..22..29..36..solved at 56 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..3..8..16..solved at 33 0..0..3..8..16..solved at 35 0..0..solved at 2 0..0..3..8..16..solved at 35 0..0..solved at 5 0..0..solved at 5 0..0..solved at 2 0..0..4..10..22..75..155..solved at 209 0..0..solved at 3 0..0..1..solved at 5 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..2..3..solved at 8 0..0..1..solved at 4 0..0..1..3..solved at 9 0..0..1..3..6..22..49..93..169..273..405..601..837..1131..1577..2127..solved at 2538 0..0..solved at 3 0..0..solved at 3 0..0..2..4..6..solved at 25 0..0..2..4..6..solved at 18 0..0..1..2..3..14..solved at 25 0..0..solved at 2 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 5 0..0..2..solved at 5 File "/<>/lists.ml", line 719, characters 4-1245: Error: This kind of expression is not allowed as right-hand side of `let rec' Error in included file /<>/lists.ml File "lists.ml" already loaded File "/<>/realax.ml", line 149, characters 6-47: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) Searching with limit 0 Searching with limit 1 Searching with limit 2 0..0..1..2..3..10..solved at 16 0..0..1..3..6..12..solved at 21 0..0..1..3..6..16..solved at 33 0..0..1..4..10..23..48..94..solved at 172 0..0..1..4..8..solved at 13 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..3..solved at 8 0..0..1..2..5..19..42..solved at 59 0..0..1..3..6..16..37..70..121..205..325..solved at 432 0..0..1..2..solved at 6 Searching with limit 0 Searching with limit 1 Searching with limit 2 0..0..1..4..8..solved at 17 0..0..1..4..solved at 10 0..0..3..6..solved at 10 0..0..3..8..15..solved at 20 0..0..3..12..23..40..63..solved at 72 0..0..3..6..18..34..61..94..145..206..solved at 249 0..0..3..14..36..111..307..901..solved at 935 File "/<>/realax.ml", line 1297, characters 4-364: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::[]|_::_::_::_::_::_::[]| _::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/realax.ml", line 1737, characters 4-341: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::[]|_::_::_::_::_::_::[]| _::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]|_::_::[]|_::[]|[]) File "realax.ml" already loaded File "/<>/calc_int.ml", line 41, characters 29-161: Warning 3: deprecated: Pervasives.& Use (&&) instead. 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..7..14..35..62..solved at 73 0..0..1..2..solved at 6 0..0..1..3..8..19..44..solved at 81 0..0..solved at 2 0..0..1..3..9..25..64..166..437..1159..3190..solved at 4411 0..0..1..2..solved at 6 0..0..1..3..8..19..44..112..275..694..solved at 932 0..0..1..3..8..19..40..85..174..348..696..1556..3482..solved at 6840 0..0..1..2..6..12..28..solved at 55 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..2..6..11..19..36..53..76..121..solved at 164 0..0..3..solved at 9 File "/<>/calc_int.ml", line 187, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/calc_int.ml", line 200, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/calc_int.ml", line 212, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/calc_int.ml", line 223, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/calc_int.ml", line 234, characters 6-46: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/calc_int.ml", line 284, characters 6-42: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_|_::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]| _::_::[]|_::[]|[]) File "calc_int.ml" already loaded 0..0..1..7..solved at 12 0..0..1..5..12..24..solved at 30 0..0..1..5..12..23..solved at 30 0..0..1..2..5..solved at 10 0..0..1..2..6..17..34..81..solved at 102 0..0..0..solved at 3 0..0..1..2..solved at 6 0..0..2..solved at 7 0..0..1..solved at 4 0..0..1..9..solved at 16 0..0..0..2..solved at 6 0..0..2..6..16..solved at 22 0..0..1..2..5..15..28..59..solved at 68 0..0..1..2..4..10..19..solved at 27 0..0..1..2..5..solved at 10 0..0..1..2..solved at 7 File "/<>/realarith.ml", line 253, characters 6-165: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_::_::_::_::_|_::_::_::_::_::_::_::_::_::[]| _::_::_::_::_::_::_::_::[]|_::_::_::_::_::_::_::[]|_::_::_::_::_::_::[]| _::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]|_::_::[]|_::[]|[]) 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..solved at 4 0..0..2..4..solved at 13 0..0..2..4..11..32..75..solved at 142 0..0..2..4..12..33..75..solved at 143 0..0..2..4..solved at 8 0..0..1..2..solved at 6 0..0..1..2..4..17..34..solved at 61 0..0..1..2..solved at 6 0..0..1..2..5..18..35..solved at 63 0..0..1..2..solved at 6 0..0..2..4..10..18..34..76..138..336..872..2366..solved at 5076 CPU time (user): 0.38 File "realarith.ml" already loaded 0..0..1..2..7..14..37..72..174..325..solved at 392 0..0..2..solved at 5 0..0..1..2..6..11..21..34..52..73..solved at 103 0..0..1..2..3..11..21..solved at 28 0..0..1..2..3..11..21..solved at 28 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..1..2..6..12..27..solved at 44 0..0..solved at 2 0..0..solved at 3 0..0..2..4..8..17..30..solved at 47 0..0..solved at 3 0..0..2..4..8..solved at 15 0..0..1..2..6..14..39..solved at 73 0..0..solved at 2 0..0..solved at 2 0..0..2..4..solved at 8 0..0..1..3..solved at 8 0..0..1..3..9..solved at 15 0..0..1..2..5..11..20..solved at 29 0..0..1..2..5..15..29..solved at 49 0..0..1..2..7..19..41..79..146..solved at 200 0..0..1..2..7..19..41..solved at 77 0..0..1..2..7..19..41..79..146..solved at 175 0..0..1..2..7..19..41..solved at 68 0..0..1..2..9..23..64..133..315..solved at 511 0..0..1..2..9..23..64..solved at 116 0..0..1..2..9..23..64..133..315..solved at 415 0..0..1..2..9..23..64..solved at 116 0..0..2..9..solved at 14 0..0..2..9..20..40..87..solved at 94 0..0..2..8..18..34..73..solved at 91 0..0..1..5..12..23..solved at 29 0..0..2..4..8..solved at 13 0..0..2..4..8..solved at 13 0..0..2..4..solved at 8 0..0..3..6..solved at 13 0..0..solved at 4 0..0..solved at 3 0..0..1..4..9..17..solved at 23 0..0..1..4..solved at 9 0..0..1..5..10..18..solved at 24 0..0..1..5..solved at 10 0..0..1..2..solved at 6 0..0..2..5..solved at 10 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..3..solved at 7 0..0..2..11..34..84..193..424..970..solved at 1151 0..0..1..2..3..8..solved at 14 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..12..27..48..solved at 81 0..0..1..5..13..27..solved at 33 0..0..1..5..11..22..49..95..171..305..solved at 319 File "real.ml" already loaded 0..0..3..solved at 6 0..0..1..4..12..53..156..809..solved at 3536 0..0..1..2..solved at 6 0..0..1..solved at 4 File "/<>/calc_rat.ml", line 581, characters 14-104: Warning 3: deprecated: Pervasives.& Use (&&) instead. 0..0..solved at 3 0..0..1..solved at 4 0..0..0..2..solved at 6 0..0..solved at 2 File "calc_rat.ml" already loaded 0..0..1..3..solved at 7 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 5 0..0..0..solved at 3 0..0..0..solved at 3 0..0..1..solved at 4 0..0..1..2..5..solved at 11 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..solved at 2 0..0..1..5..solved at 9 0..0..1..2..5..8..solved at 14 0..0..2..5..11..23..42..71..111..171..262..solved at 304 0..0..2..solved at 6 0..0..2..solved at 5 0..0..2..solved at 5 0..0..2..solved at 5 File "/<>/int.ml", line 754, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/int.ml", line 767, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/int.ml", line 779, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/int.ml", line 790, characters 6-44: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/int.ml", line 801, characters 6-46: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_|_::_::_::[]|_::_::[]|_::[]|[]) File "/<>/int.ml", line 851, characters 6-42: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_::_::_::_|_::_::_::_::_::[]|_::_::_::_::[]|_::_::_::[]| _::_::[]|_::[]|[]) 4 basis elements and 1 critical pairs 5 basis elements and 0 critical pairs Translating certificate to HOL inferences 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 3 basis elements and 2 critical pairs 4 basis elements and 3 critical pairs 5 basis elements and 0 critical pairs Translating certificate to HOL inferences 0..0..1..2..5..solved at 13 0..0..1..2..5..solved at 13 Warning: inventing type variables 0..0..1..4..11..25..54..solved at 82 0..0..1..4..solved at 12 1 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs 0..0..0..2..6..solved at 11 0..0..0..2..6..solved at 11 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 3 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 3 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 3 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 3 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 2 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 2 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 0..0..0..0..0..solved at 5 0..0..0..0..0..2..7..12..27..solved at 38 0..0..solved at 2 0..0..1..solved at 4 0..0..1..2..3..solved at 8 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..solved at 3 0..0..0..solved at 3 2 basis elements and 0 critical pairs 1 basis elements and 0 critical pairs Translating certificate to HOL inferences 0..0..2..4..8..16..27..42..58..77..100..128..160..222..solved at 242 File "int.ml" already loaded Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 2 0..0..0..solved at 3 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 5 0..0..0..solved at 4 0..0..0..solved at 3 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 5 0..0..1..solved at 4 0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..3..solved at 7 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..solved at 10 0..0..2..solved at 7 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..8..solved at 12 0..0..2..6..solved at 10 0..0..2..solved at 7 0..0..1..solved at 4 0..0..2..5..solved at 9 0..0..1..3..solved at 7 0..0..2..solved at 7 0..0..1..solved at 5 0..0..2..6..solved at 10 0..0..1..3..solved at 7 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 5 0..0..1..solved at 4 0..0..2..solved at 5 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 5 0..0..1..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 5 0..0..1..solved at 4 0..0..2..solved at 7 0..0..2..solved at 5 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..2..4..solved at 8 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..5..solved at 11 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..2..7..12..solved at 26 0..0..1..2..solved at 6 0..0..1..3..9..17..46..solved at 96 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 5 0..0..0..solved at 3 0..0..0..solved at 5 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..1..5..16..36..114..solved at 121 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 0..0..0..solved at 4 0..0..solved at 2 0..0..1..solved at 5 0..0..1..solved at 5 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..2..4..12..21..solved at 31 0..0..3..solved at 6 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..0..solved at 3 0..0..1..solved at 4 0..0..2..solved at 5 0..0..solved at 2 0..0..2..4..solved at 8 0..0..2..4..solved at 8 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..1..3..9..18..34..59..100..167..solved at 240 0..0..1..solved at 4 0..0..solved at 2 0..0..2..solved at 5 0..0..1..3..solved at 7 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 5 0..0..1..solved at 4 0..0..2..solved at 5 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 5 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..solved at 6 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..0..solved at 3 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..0..solved at 5 0..0..0..solved at 3 Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 5 0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..0..3..11..solved at 23 0..0..0..2..solved at 7 0..0..1..solved at 4 0..0..0..0..3..11..solved at 23 0..0..1..solved at 5 0..0..0..2..solved at 6 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..0..1..solved at 5 Warning: inventing type variables 0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 5 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..1..3..5..solved at 11 Warning: inventing type variables 0..0..0..0..3..8..solved at 14 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 3 0..0..2..solved at 7 0..0..2..solved at 7 Warning: inventing type variables 0..0..3..solved at 9 0..0..2..4..6..14..26..solved at 42 0..0..1..solved at 4 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..3..7..solved at 13 0..0..1..4..solved at 8 Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 6 0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..solved at 5 0..0..0..solved at 3 0..0..0..solved at 5 0..0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..2..solved at 6 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..4..10..16..31..solved at 42 0..0..1..solved at 5 0..0..1..2..5..9..15..22..31..44..62..solved at 80 0..0..0..2..4..solved at 9 0..0..1..solved at 5 0..0..1..2..5..9..15..23..solved at 37 0..0..0..2..4..solved at 9 0..0..1..solved at 5 0..0..1..2..7..13..solved at 19 0..0..1..3..7..solved at 12 0..0..1..solved at 5 0..0..1..2..5..12..22..solved at 33 0..0..1..3..7..solved at 12 Warning: inventing type variables 0..0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..1..2..3..7..solved at 17 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 5 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 Warning: inventing type variables 0..0..1..solved at 4 0..0..0..1..2..3..5..7..9..15..21..27..solved at 44 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..3..7..12..17..28..39..50..77..104..131..solved at 160 0..0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..1..2..5..9..15..25..40..66..123..229..496..solved at 530 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..2..solved at 6 0..0..0..1..2..3..6..12..19..29..44..60..90..132..174..237..347..461..671..924..1242..1638..2121..2674..3528..4540..5883..7460..9417..solved at 9827 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 5 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 2 0..0..0..solved at 3 Warning: inventing type variables 0..0..solved at 2 0..0..0..solved at 3 0..0..1..solved at 4 0..0..0..solved at 3 0..0..0..1..2..3..6..9..12..solved at 20 0..0..0..1..2..3..solved at 8 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..1..2..3..16..solved at 25 0..0..0..2..5..solved at 10 0..0..0..2..solved at 6 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..4..10..20..36..57..80..solved at 102 0..0..0..0..4..10..20..36..solved at 56 Warning: inventing type variables 0..0..0..2..solved at 6 0..0..0..1..2..3..6..12..20..32..49..67..101..149..197..269..393..521..756..1037..1386..1819..2341..2939..3838..4894..solved at 5394 Warning: inventing type variables 0..0..0..solved at 3 0..0..1..2..solved at 6 0..0..0..0..3..7..13..23..37..56..84..121..167..232..306..397..505..632..811..1028..1316..1696..2170..2748..3498..4387..5428..6873..8564..10748..13749..solved at 17244 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..2..4..14..35..60..99..166..245..378..solved at 392 0..0..4..8..20..44..77..154..265..solved at 316 0..0..4..9..27..63..114..solved at 128 0..0..3..solved at 7 0..0..3..solved at 8 0..0..1..solved at 4 0..0..3..7..15..solved at 21 0..0..3..6..13..30..55..solved at 72 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..4..10..22..41..solved at 51 0..0..0..0..4..10..solved at 20 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..solved at 13 0..0..solved at 2 0..0..1..2..5..solved at 13 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..1..3..8..21..46..solved at 96 0..0..1..2..5..9..15..22..29..36..solved at 45 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..2..5..9..15..29..44..68..108..150..213..348..523..solved at 570 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..1..3..8..18..40..86..solved at 175 0..0..1..3..7..15..26..46..68..96..129..166..207..268..333..414..solved at 465 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..1..2..5..solved at 11 0..0..1..2..5..solved at 11 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..11..solved at 22 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..0..1..2..3..4..5..6..solved at 20 0..0..1..2..solved at 6 0..0..0..solved at 3 0..0..1..2..solved at 6 0..0..0..0..0..2..9..20..46..solved at 72 0..0..0..2..6..solved at 11 0..0..1..3..8..17..33..59..98..146..217..solved at 276 Warning: inventing type variables 0..0..1..2..5..9..15..solved at 24 0..0..2..4..solved at 8 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..2..4..12..21..solved at 31 0..0..1..2..solved at 6 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..1..3..solved at 7 0..0..solved at 3 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 Warning: inventing type variables 0..0..0..4..solved at 10 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 5 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..3..solved at 7 0..0..3..solved at 9 0..0..solved at 2 0..0..1..solved at 6 0..0..0..solved at 3 0..0..0..solved at 4 0..0..0..1..3..7..solved at 14 0..0..0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 0..0..0..0..1..4..9..solved at 17 0..0..1..2..3..7..13..21..solved at 34 0..0..1..2..11..25..52..solved at 59 Warning: inventing type variables 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..0..1..2..3..8..solved at 16 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..3..7..15..26..46..77..solved at 96 0..0..solved at 2 0..0..0..0..1..4..9..solved at 22 0..0..1..2..5..9..15..solved at 26 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..1..2..3..solved at 8 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..solved at 4 Warning: inventing type variables 0..0..0..0..0..2..4..6..9..12..15..23..31..39..56..73..90..116..142..168..276..solved at 403 0..0..0..0..0..0..2..4..6..10..14..18..27..36..45..61..77..93..120..147..174..213..252..291..465..651..890..solved at 1040 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..1..2..11..27..56..102..183..274..437..655..987..1746..2662..solved at 2980 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..solved at 13 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..solved at 13 0..0..solved at 2 0..0..1..2..11..27..57..106..187..276..416..594..882..1624..2521..solved at 2830 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..0..1..2..3..solved at 10 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..0..solved at 4 0..0..0..0..1..4..9..17..26..35..50..65..105..solved at 128 Warning: inventing type variables 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..3..6..solved at 10 0..0..3..6..solved at 10 0..0..2..6..11..23..47..91..186..333..537..880..1386..2121..3496..5629..8957..14874..24097..37962..solved at 40441 0..0..2..7..13..27..57..114..242..439..707..1140..1754..2620..4198..6611..10369..17055..27259..42383..solved at 45658 0..0..3..6..13..31..58..118..solved at 181 0..0..solved at 2 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..solved at 11 0..0..2..solved at 8 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..10..solved at 14 0..0..2..8..solved at 12 0..0..0..2..solved at 6 0..0..0..1..7..18..40..73..113..191..298..467..830..solved at 1350 0..0..1..solved at 4 0..0..0..2..solved at 6 Warning: inventing type variables 0..0..solved at 3 0..0..2..4..8..16..28..solved at 37 0..0..solved at 2 0..0..1..5..10..15..30..solved at 37 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 8 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 3 0..0..2..4..8..16..28..solved at 37 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..2..5..8..11..28..solved at 35 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 6 0..0..2..solved at 5 0..0..solved at 2 0..0..solved at 2 0..0..2..4..6..8..10..18..38..58..solved at 71 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..0..0..1..5..11..solved at 19 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..1..2..7..13..23..34..45..56..80..104..141..237..solved at 327 0..0..1..3..7..17..solved at 23 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..2..solved at 5 0..0..3..solved at 6 0..0..3..solved at 6 Warning: inventing type variables 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 4 0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..5..9..15..25..35..47..67..87..114..solved at 152 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..2..4..10..18..30..48..66..88..solved at 99 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 7 0..0..0..0..solved at 5 0..0..0..0..solved at 4 0..0..2..4..7..17..31..66..117..228..383..696..1122..1957..solved at 2075 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..0..2..8..20..49..103..solved at 184 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..0..solved at 3 0..0..1..2..solved at 6 0..0..1..2..3..solved at 8 0..0..1..2..solved at 6 0..0..solved at 3 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..1..2..5..12..22..37..56..solved at 74 Warning: inventing type variables 0..0..1..2..5..solved at 13 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..7..15..25..40..62..93..159..253..solved at 294 0..0..1..solved at 4 0..0..solved at 2 0..0..2..solved at 5 0..0..1..solved at 4 0..0..1..5..14..solved at 24 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 7 0..0..0..0..solved at 5 0..0..0..0..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..0..solved at 3 0..0..solved at 2 0..0..0..solved at 4 0..0..0..solved at 3 Warning: inventing type variables 0..0..3..6..16..33..60..123..solved at 148 0..0..2..4..10..20..35..77..136..243..470..842..1459..solved at 2793 0..0..3..9..24..59..112..228..solved at 259 0..0..2..solved at 5 0..0..1..2..9..21..47..87..161..241..405..578..951..1711..2759..solved at 3322 0..0..0..1..2..3..8..solved at 16 0..0..1..solved at 4 0..0..1..2..5..9..15..23..solved at 37 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..4..6..8..18..solved at 30 Warning: inventing type variables 0..0..1..2..9..21..47..87..161..241..405..578..951..1711..2759..solved at 3322 0..0..1..2..6..13..24..41..61..90..135..187..273..solved at 328 0..0..2..solved at 7 0..0..solved at 3 0..0..1..solved at 5 0..0..0..solved at 3 0..0..solved at 5 0..0..4..solved at 10 0..0..solved at 4 0..0..3..solved at 8 0..0..solved at 5 0..0..solved at 4 0..0..3..solved at 7 0..0..3..solved at 7 0..0..2..solved at 5 0..0..2..solved at 5 0..0..1..2..3..7..solved at 16 0..0..1..2..solved at 6 0..0..0..1..2..3..solved at 8 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..4..14..41..solved at 109 0..0..1..4..14..41..solved at 109 0..0..solved at 4 0..0..solved at 3 0..0..2..solved at 7 0..0..2..solved at 6 0..0..1..solved at 5 0..0..1..solved at 4 0..0..1..solved at 5 0..0..0..solved at 3 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..1..solved at 6 0..0..0..0..solved at 4 0..0..0..0..solved at 5 0..0..1..2..3..7..14..26..47..77..solved at 94 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..0..1..solved at 6 0..0..0..0..solved at 5 0..0..0..0..solved at 4 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..0..0..solved at 4 0..0..0..0..solved at 4 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..0..solved at 5 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..solved at 2 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..4..8..solved at 12 0..0..2..solved at 6 0..0..2..solved at 5 0..0..solved at 2 0..0..3..solved at 6 0..0..4..solved at 7 0..0..2..6..14..46..85..182..345..630..solved at 708 Warning: inventing type variables 0..0..1..3..7..13..24..63..102..180..268..solved at 277 Warning: inventing type variables 0..0..1..3..5..11..21..32..45..68..91..solved at 100 0..0..1..3..7..13..24..55..86..143..207..solved at 216 0..0..1..3..7..12..20..30..40..71..106..solved at 115 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..3..8..14..solved at 20 0..0..1..3..8..13..solved at 19 0..0..0..solved at 3 Warning: inventing type variables 0..0..2..solved at 6 0..0..solved at 2 0..0..2..solved at 6 0..0..2..4..10..22..42..solved at 53 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..2..4..solved at 8 0..0..2..7..14..32..82..191..466..1144..2508..5758..13277..28479..solved at 31328 0..0..1..4..8..15..solved at 34 0..0..1..6..18..solved at 25 0..0..0..2..6..14..solved at 32 0..0..0..solved at 3 0..0..1..2..solved at 6 Warning: inventing type variables 5 basis elements and 1 critical pairs 5 basis elements and 0 critical pairs 5 basis elements and 3 critical pairs 6 basis elements and 4 critical pairs 6 basis elements and 3 critical pairs 7 basis elements and 4 critical pairs 7 basis elements and 3 critical pairs 8 basis elements and 3 critical pairs 8 basis elements and 2 critical pairs 8 basis elements and 1 critical pairs 8 basis elements and 0 critical pairs 5 basis elements and 2 critical pairs 6 basis elements and 2 critical pairs 6 basis elements and 1 critical pairs 7 basis elements and 1 critical pairs 7 basis elements and 0 critical pairs 5 basis elements and 3 critical pairs 6 basis elements and 4 critical pairs 6 basis elements and 3 critical pairs 7 basis elements and 5 critical pairs 7 basis elements and 4 critical pairs 8 basis elements and 5 critical pairs 9 basis elements and 0 critical pairs 4 basis elements and 1 critical pairs 5 basis elements and 1 critical pairs 5 basis elements and 0 critical pairs 2 basis elements and 0 critical pairs 5 basis elements and 2 critical pairs 6 basis elements and 0 critical pairs 5 basis elements and 3 critical pairs 6 basis elements and 4 critical pairs 6 basis elements and 3 critical pairs 7 basis elements and 0 critical pairs 0..0..1..5..solved at 10 0..0..solved at 2 0..0..1..solved at 5 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..2..6..solved at 19 0..0..3..8..solved at 22 0..0..2..6..solved at 19 0..0..solved at 2 0..0..3..8..solved at 22 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..2..6..solved at 22 0..0..solved at 3 0..0..solved at 2 0..0..2..solved at 9 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..3..7..22..54..solved at 65 0..0..0..4..11..21..46..76..solved at 89 0..0..2..4..14..solved at 32 0..0..1..2..8..solved at 17 0..0..solved at 2 0..0..1..2..8..solved at 18 0..0..1..2..5..12..21..solved at 30 0..0..1..2..5..12..23..solved at 35 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..0..2..14..38..solved at 134 0..0..0..2..14..solved at 42 0..0..0..solved at 3 0..0..0..1..solved at 8 0..0..solved at 2 0..0..3..7..solved at 11 0..0..solved at 2 0..0..3..7..solved at 11 0..0..solved at 2 0..0..2..5..11..26..solved at 51 Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 5 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 5 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..2..4..8..19..40..67..101..solved at 127 Warning: inventing type variables 0..0..2..4..8..18..31..46..solved at 60 Warning: inventing type variables 0..0..2..4..8..solved at 13 0..0..2..4..8..solved at 13 0..0..2..4..8..solved at 19 0..0..2..4..8..solved at 16 Warning: inventing type variables 0..0..2..4..8..28..54..solved at 68 0..0..2..4..8..solved at 13 0..0..2..4..8..solved at 19 0..0..solved at 2 0..0..2..4..solved at 8 0..0..2..4..10..22..solved at 31 0..0..2..4..8..solved at 16 Warning: inventing type variables 0..0..3..7..15..31..53..solved at 71 0..0..2..5..10..22..44..solved at 56 Warning: inventing type variables 0..0..2..4..8..solved at 17 0..0..2..4..8..solved at 19 0..0..3..6..13..32..58..solved at 74 0..0..3..6..13..32..58..solved at 70 0..0..2..4..8..solved at 17 0..0..2..4..8..22..48..87..137..213..310..439..solved at 478 0..0..2..4..8..22..48..87..137..213..310..439..solved at 486 0..0..2..4..8..solved at 16 0..0..2..4..8..16..36..71..114..180..267..433..653..908..1270..solved at 1348 Warning: inventing type variables 0..0..2..5..solved at 9 0..0..1..solved at 4 0..0..0..solved at 3 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 6 0..0..solved at 3 0..0..solved at 2 0..0..0..0..0..solved at 5 0..0..0..0..solved at 4 0..0..1..solved at 6 0..0..1..solved at 5 Warning: inventing type variables 0..0..2..solved at 5 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..solved at 3 0..0..2..8..solved at 20 0..0..solved at 2 0..0..2..solved at 5 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..3..solved at 6 0..0..2..4..solved at 8 0..0..0..0..2..6..13..25..solved at 34 0..0..0..0..2..6..13..25..solved at 34 Warning: inventing type variables Warning: inventing type variables 0..0..1..3..7..solved at 13 0..0..3..7..15..solved at 28 0..0..solved at 2 0..0..4..9..18..solved at 35 0..0..2..solved at 7 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..12..22..34..48..69..99..140..211..307..435..642..905..1303..1847..solved at 2499 0..0..1..7..23..57..137..284..501..solved at 666 0..0..0..1..2..3..12..solved at 21 0..0..1..2..5..12..22..36..52..74..106..152..212..321..452..711..1026..1572..2205..3406..5353..8956..solved at 11113 0..0..1..2..5..solved at 13 0..0..2..9..20..43..82..solved at 135 Warning: inventing type variables 0..0..1..2..5..9..15..22..solved at 38 0..0..solved at 3 0..0..solved at 3 0..0..5..10..24..51..solved at 66 0..0..solved at 2 0..0..4..8..19..41..solved at 64 0..0..4..8..19..42..solved at 65 0..0..5..10..24..solved at 32 Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..1..solved at 5 0..0..0..solved at 4 0..0..0..solved at 3 0..0..1..2..5..8..11..14..17..20..36..56..78..109..148..191..248..317..solved at 371 0..0..1..2..5..8..11..14..17..20..36..56..78..109..148..191..248..317..solved at 375 0..0..1..solved at 4 0..0..solved at 2 0..0..0..1..2..3..5..7..9..solved at 17 0..0..solved at 2 0..0..solved at 2 0..0..0..0..1..2..3..4..5..6..9..12..15..21..27..33..solved at 55 0..0..1..2..5..8..11..14..17..20..28..36..44..55..66..77..solved at 97 0..0..1..2..5..8..11..14..17..20..28..36..44..55..66..77..solved at 97 0..0..solved at 2 0..0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..1..3..solved at 7 0..0..solved at 2 0..0..1..2..5..9..17..26..38..solved at 48 0..0..1..2..7..solved at 12 0..0..1..2..5..9..15..23..34..48..solved at 65 0..0..1..solved at 4 0..0..0..solved at 3 0..0..1..2..5..11..solved at 18 0..0..1..2..5..solved at 13 0..0..1..solved at 4 0..0..1..2..5..10..18..31..46..63..88..solved at 117 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..1..2..3..8..solved at 16 0..0..1..solved at 4 0..0..1..2..5..9..15..30..47..76..solved at 120 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..3..8..15..29..60..solved at 90 0..0..1..3..8..15..solved at 21 0..0..2..4..solved at 8 0..0..solved at 2 0..0..2..5..13..34..70..160..300..605..1071..2263..3998..8099..solved at 12555 0..0..3..solved at 6 0..0..3..solved at 6 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..solved at 10 0..0..2..solved at 7 0..0..3..solved at 8 0..0..2..solved at 6 0..0..3..8..solved at 12 0..0..2..6..solved at 10 0..0..2..solved at 5 0..0..2..5..solved at 10 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..1..2..3..solved at 8 0..0..0..1..2..3..6..9..12..21..30..39..58..77..96..solved at 107 Warning: inventing type variables 0..0..0..1..2..3..8..solved at 16 0..0..0..1..2..3..8..solved at 16 Warning: inventing type variables 0..0..2..solved at 5 0..0..2..solved at 5 0..0..2..7..17..36..76..145..262..solved at 474 0..0..1..6..16..31..71..132..229..443..713..1082..1694..2623..4077..6756..11110..18048..29639..47994..76336..solved at 115499 0..0..2..4..8..22..42..66..112..161..223..297..381..481..707..949..1227..1650..2105..2606..3270..3978..4770..5888..7090..8445..10095..11890..14206..solved at 14609 0..0..2..8..16..42..99..163..346..solved at 408 0..0..1..3..10..solved at 15 0..0..2..4..12..30..56..solved at 64 0..0..2..4..11..26..47..solved at 55 0..0..2..5..13..solved at 18 0..0..1..3..10..solved at 15 0..0..2..4..12..27..47..solved at 54 0..0..2..4..11..26..46..solved at 53 0..0..2..5..13..solved at 18 0..0..1..3..8..14..36..77..126..246..516..1204..3264..solved at 3298 0..0..1..solved at 7 0..0..1..7..15..33..83..171..solved at 204 0..0..2..5..10..33..62..93..150..209..272..339..414..499..747..1045..1349..solved at 1473 0..0..solved at 2 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 2 0..0..1..3..solved at 7 0..0..solved at 2 0..0..2..solved at 5 0..0..1..4..8..12..16..solved at 25 0..0..1..5..14..solved at 20 0..0..2..4..8..16..28..44..solved at 54 0..0..2..solved at 7 0..0..2..solved at 7 0..0..1..solved at 5 0..0..3..10..23..57..122..234..solved at 262 0..0..1..4..12..31..76..162..294..558..959..1533..2548..solved at 2588 0..0..2..4..9..25..48..84..142..210..337..solved at 387 0..0..2..5..11..35..65..100..176..254..338..437..544..687..1040..1443..1912..solved at 2135 0..0..1..5..11..solved at 16 0..0..1..3..7..solved at 17 0..0..3..8..18..53..99..155..287..423..569..733..913..1145..1693..2329..3064..solved at 3378 0..0..3..8..18..53..99..155..287..423..569..733..913..1145..1693..2329..3064..solved at 3370 0..0..3..6..14..41..79..141..244..366..591..solved at 701 0..0..3..6..14..41..79..141..244..366..591..solved at 662 0..0..1..2..3..10..21..32..55..solved at 64 0..0..2..solved at 9 0..0..3..12..30..77..192..408..957..2317..5293..solved at 9312 0..0..2..8..solved at 14 0..0..2..10..solved at 17 0..0..3..11..28..74..192..410..solved at 619 0..0..2..10..31..89..255..622..1544..3861..9467..solved at 9606 0..0..2..7..17..36..76..145..262..solved at 483 0..0..1..6..16..31..71..132..229..443..713..1082..1694..2617..4067..6744..11120..18071..29739..48196..76749..solved at 117331 0..0..2..4..8..22..42..66..112..161..223..297..381..481..707..949..1227..1650..2105..2606..3270..3978..4770..5891..7096..8454..10131..11953..14289..solved at 14763 0..0..2..8..16..42..99..163..346..solved at 408 0..0..2..4..12..27..48..solved at 56 0..0..2..5..13..solved at 18 0..0..1..3..10..solved at 15 0..0..2..4..11..29..55..solved at 63 0..0..2..4..12..27..47..solved at 54 0..0..2..5..13..solved at 18 0..0..1..3..10..solved at 15 0..0..2..4..11..26..46..solved at 53 0..0..1..3..8..14..36..77..126..246..516..1202..3262..solved at 3309 0..0..1..solved at 7 0..0..1..7..15..33..83..171..solved at 204 0..0..2..5..10..33..62..93..150..209..272..339..414..499..749..1049..1355..solved at 1479 0..0..solved at 2 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 2 0..0..1..3..solved at 7 0..0..solved at 2 0..0..2..solved at 5 0..0..1..5..14..solved at 20 0..0..1..4..8..12..16..solved at 27 0..0..2..4..8..16..28..45..solved at 55 0..0..2..solved at 7 0..0..1..solved at 5 0..0..2..solved at 7 0..0..2..6..16..41..78..solved at 112 0..0..3..solved at 6 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..2..5..solved at 11 0..0..2..5..11..43..97..169..307..507..781..1260..1924..solved at 2571 0..0..2..5..11..40..91..161..351..626..solved at 723 0..0..1..4..11..30..75..161..294..559..961..1532..2548..solved at 2599 Warning: inventing type variables 0..0..2..4..10..26..49..86..143..211..338..solved at 362 0..0..2..5..11..35..65..100..176..254..338..437..544..687..1042..1447..1918..solved at 2141 0..0..1..5..11..solved at 16 0..0..1..3..7..solved at 17 0..0..3..8..18..53..99..155..287..423..569..733..913..1145..1695..2333..3070..solved at 3384 0..0..3..8..18..53..99..155..287..423..569..733..913..1145..1695..2333..3070..solved at 3376 0..0..3..6..16..43..81..145..246..368..593..solved at 658 0..0..3..6..16..43..81..145..246..368..593..solved at 619 0..0..1..2..3..10..21..32..55..solved at 64 File "sets.ml" already loaded 0..0..1..7..solved at 11 0..0..0..4..13..solved at 25 0..0..2..7..15..39..100..234..587..1410..3140..7378..16891..solved at 18714 0..0..1..2..solved at 6 0..0..1..2..5..9..15..24..33..44..67..90..125..solved at 185 0..0..1..2..5..8..11..solved at 19 0..0..3..6..15..54..118..265..680..1689..5287..solved at 11598 0..0..0..0..2..4..6..10..14..18..30..42..68..114..161..216..305..399..508..670..875..1105..solved at 1498 0..0..1..3..8..solved at 13 0..0..0..0..1..3..5..12..21..41..70..112..159..242..330..451..600..781..1008..1316..1670..solved at 2062 0..0..1..solved at 4 0..0..2..8..19..solved at 25 0..0..2..8..18..solved at 24 0..0..1..solved at 4 0..0..solved at 2 0..0..1..2..5..9..15..27..41..66..107..solved at 125 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..3..6..19..42..78..127..186..270..412..638..solved at 776 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..4..8..23..51..93..156..solved at 192 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..1..2..solved at 9 0..0..2..4..solved at 8 0..0..1..2..solved at 9 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 7 0..0..solved at 2 0..0..1..2..solved at 7 0..0..1..2..8..17..53..104..solved at 158 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 6 0..0..1..solved at 5 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..2..4..11..20..34..72..114..190..381..solved at 438 0..0..solved at 2 0..0..2..4..10..solved at 16 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..solved at 3 0..0..solved at 4 0..0..solved at 2 0..0..0..solved at 5 0..0..0..solved at 3 0..0..solved at 2 0..0..1..solved at 5 Warning: inventing type variables 0..0..1..2..5..9..15..solved at 22 0..0..solved at 2 0..0..3..6..12..25..46..94..155..254..479..solved at 599 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..1..solved at 4 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..5..9..15..22..29..36..53..70..97..132..167..210..282..354..455..576..697..838..1034..1230..1481..solved at 1835 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..2..10..33..89..264..814..2481..solved at 6396 0..0..1..2..6..solved at 11 0..0..1..2..5..9..15..solved at 26 0..0..1..6..22..48..121..253..441..992..1771..3020..5157..8831..solved at 12430 Warning: inventing type variables Warning: inventing type variables 0..0..3..6..13..solved at 24 0..0..2..4..8..16..28..43..67..95..155..236..348..490..727..solved at 823 0..0..4..8..19..solved at 30 0..0..3..6..solved at 13 0..0..1..9..19..37..76..127..solved at 141 0..0..solved at 2 0..0..1..8..17..34..67..112..solved at 126 0..0..0..1..3..7..20..solved at 34 0..0..1..solved at 4 0..0..1..2..5..9..15..35..solved at 65 Warning: inventing type variables 0..0..0..solved at 3 0..0..0..1..solved at 6 0..0..0..0..solved at 5 0..0..0..0..solved at 4 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..solved at 11 0..0..solved at 2 0..0..1..2..5..10..20..solved at 31 0..0..solved at 2 0..0..1..7..solved at 11 0..0..3..7..solved at 11 0..0..2..4..12..24..44..84..solved at 142 Warning: inventing type variables 0..0..0..1..2..3..8..solved at 16 0..0..1..solved at 4 0..0..1..2..10..22..49..93..171..282..522..811..solved at 842 0..0..1..2..5..9..15..23..solved at 37 0..0..0..1..2..3..solved at 8 0..0..1..2..5..9..15..30..47..76..solved at 121 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..2..solved at 6 0..0..0..2..4..8..solved at 18 0..0..1..2..5..solved at 13 0..0..3..11..31..solved at 42 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..2..4..solved at 9 0..0..solved at 2 0..0..2..4..solved at 8 0..0..solved at 2 0..0..2..solved at 5 0..0..4..8..18..34..solved at 48 0..0..2..4..solved at 8 0..0..4..8..18..34..solved at 48 0..0..2..4..8..16..39..83..147..248..472..749..1436..solved at 2196 0..0..4..8..18..solved at 32 0..0..2..4..8..solved at 14 0..0..1..3..solved at 8 0..0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..11..25..55..100..209..399..solved at 697 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..5..9..15..solved at 26 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..2..6..solved at 12 0..0..1..solved at 4 Warning: inventing type variables 0..0..1..2..solved at 8 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..2..6..15..30..73..134..229..368..553..800..1208..1747..2508..3645..5152..7046..solved at 7159 Warning: inventing type variables Warning: inventing type variables 0..0..3..6..9..solved at 14 0..0..3..6..9..solved at 14 0..0..2..5..8..solved at 18 0..0..2..solved at 6 Warning: inventing type variables 0..0..1..3..7..13..30..solved at 37 0..0..1..solved at 4 0..0..solved at 2 0..0..1..5..15..30..solved at 36 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..2..solved at 5 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..1..5..15..solved at 22 0..0..2..6..22..76..261..solved at 597 0..0..1..2..7..13..26..42..67..97..161..234..375..537..790..1087..1727..2450..solved at 2485 Warning: inventing type variables 0..0..0..solved at 3 Warning: inventing type variables 0..0..2..6..15..30..77..142..261..426..699..1038..1725..2554..4260..6426..11402..17097..solved at 17200 Warning: inventing type variables 0..0..1..2..5..9..15..23..31..39..57..75..103..solved at 139 0..0..1..2..6..11..19..34..49..70..117..164..237..386..553..836..1215..1685..2287..solved at 2748 Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 5 0..0..1..2..4..9..15..solved at 21 0..0..solved at 2 0..0..1..2..5..9..15..26..38..52..75..98..130..solved at 171 0..0..solved at 2 0..0..1..2..5..11..19..solved at 26 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..3..solved at 7 0..0..solved at 2 0..0..1..4..12..30..solved at 51 0..0..solved at 2 0..0..1..3..7..14..32..solved at 40 0..0..solved at 2 0..0..1..3..7..14..30..solved at 38 Warning: inventing type variables Warning: inventing type variables 0..0..2..4..10..18..30..solved at 46 0..0..2..4..8..16..28..59..103..173..solved at 212 0..0..1..4..13..29..64..122..204..solved at 247 0..0..1..7..18..38..78..147..solved at 161 0..0..2..4..solved at 8 Warning: inventing type variables 0..0..2..4..8..27..52..93..143..223..solved at 280 Warning: inventing type variables 0..0..1..2..solved at 8 0..0..solved at 2 0..0..solved at 2 0..0..1..2..solved at 8 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 Warning: inventing type variables 0..0..2..6..15..30..73..134..229..368..553..800..1208..1747..2508..3645..5152..7046..solved at 7159 0..0..solved at 2 0..0..1..solved at 4 0..0..0..solved at 3 0..0..solved at 2 0..0..2..8..solved at 12 0..0..1..5..15..31..solved at 37 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..3..solved at 6 0..0..3..solved at 6 0..0..3..6..9..25..47..79..153..solved at 167 0..0..3..6..9..25..48..84..158..solved at 175 0..0..2..5..8..19..37..63..117..solved at 165 0..0..2..solved at 6 Warning: inventing type variables 0..0..1..2..3..4..9..22..35..56..81..solved at 94 0..0..1..solved at 4 0..0..2..9..16..26..59..solved at 68 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..1..5..15..solved at 22 0..0..2..6..22..76..261..solved at 597 0..0..1..2..7..13..26..42..67..97..161..234..375..537..790..1087..1727..2450..solved at 2485 Warning: inventing type variables 0..0..2..5..10..21..39..63..93..149..232..400..714..1313..2437..solved at 3778 0..0..0..solved at 3 Warning: inventing type variables 0..0..2..6..15..30..77..142..253..408..645..946..1535..2256..3565..5301..8800..12859..solved at 12962 0..0..2..5..10..25..47..75..111..180..279..473..834..1570..2960..5933..11269..solved at 19226 Warning: inventing type variables 0..0..1..2..5..9..15..23..31..39..57..75..103..solved at 139 0..0..1..2..6..11..19..34..49..70..117..164..237..386..553..836..1213..1681..2277..solved at 2734 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..1..solved at 5 0..0..1..2..4..9..15..solved at 21 0..0..solved at 2 0..0..1..2..5..9..15..26..38..52..75..98..130..solved at 171 0..0..solved at 2 0..0..1..2..5..11..19..solved at 26 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..3..solved at 7 0..0..solved at 2 0..0..1..4..10..25..solved at 41 0..0..1..solved at 4 Warning: inventing type variables Warning: inventing type variables 0..0..2..4..10..18..30..solved at 46 0..0..2..4..8..16..28..59..103..173..solved at 214 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..2..solved at 6 0..0..0..1..2..3..8..solved at 16 0..0..0..0..solved at 4 0..0..1..4..13..29..64..122..204..solved at 247 0..0..1..7..18..38..78..147..solved at 161 0..0..1..2..6..12..28..48..72..100..147..195..316..458..652..894..1207..1592..2128..2732..3491..4404..5471..6812..8440..10222..12256..14610..17294..solved at 19757 Warning: inventing type variables File "/<>/iterate.ml", line 2225, characters 6-27: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) Warning: inventing type variables 0..0..1..solved at 5 0..0..1..3..5..10..19..31..60..103..157..249..361..504..748..1123..1718..2921..solved at 3656 Warning: inventing type variables 0..0..1..3..7..16..35..68..116..212..392..759..solved at 1033 0..0..solved at 2 0..0..solved at 2 0..0..1..3..8..19..39..solved at 69 0..0..solved at 2 0..0..1..5..20..solved at 25 0..0..solved at 2 0..0..2..8..27..solved at 33 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 File "iterate.ml" already loaded 0..0..1..2..5..9..15..solved at 32 0..0..2..solved at 6 0..0..0..1..2..3..5..7..9..solved at 16 0..0..1..2..5..9..15..30..47..76..solved at 127 0..0..1..solved at 4 0..0..1..solved at 4 0..0..0..1..4..solved at 9 0..0..1..2..5..9..15..30..47..76..solved at 124 0..0..1..2..5..9..15..22..solved at 36 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..10..solved at 16 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..6..12..27..solved at 44 0..0..1..2..5..9..15..solved at 30 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..1..2..5..9..solved at 16 0..0..1..2..5..9..solved at 16 Warning: inventing type variables 0..0..0..0..4..9..18..30..solved at 42 0..0..0..0..0..4..10..16..26..36..46..64..82..100..131..162..193..solved at 219 0..0..0..1..2..3..5..7..9..solved at 16 0..0..1..2..5..9..15..40..67..116..solved at 201 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..1..2..6..12..27..48..solved at 81 Warning: inventing type variables 0..0..solved at 2 0..0..1..2..solved at 6 Warning: inventing type variables 0..0..1..2..8..15..solved at 40 0..0..solved at 2 0..0..0..1..2..3..5..7..9..solved at 16 0..0..1..3..5..10..19..32..60..solved at 97 0..0..1..3..5..10..18..28..52..solved at 83 0..0..2..5..8..17..31..47..86..solved at 135 0..0..1..3..5..10..18..28..51..solved at 81 0..0..2..5..8..17..31..47..87..solved at 133 0..0..2..5..8..17..31..49..92..solved at 144 0..0..3..7..11..24..43..62..111..solved at 167 0..0..1..2..5..9..15..40..67..116..solved at 198 0..0..2..4..8..16..29..65..127..215..solved at 297 0..0..2..4..8..16..31..73..144..245..solved at 327 0..0..3..6..11..23..45..104..216..372..solved at 528 0..0..2..4..8..16..29..65..128..217..solved at 299 0..0..3..6..11..23..43..96..200..344..solved at 500 0..0..3..6..11..23..43..90..185..310..solved at 396 0..0..4..8..14..30..57..127..269..465..solved at 707 0..0..2..4..8..16..30..69..136..231..solved at 313 0..0..3..6..11..23..42..92..192..330..solved at 486 0..0..3..6..11..23..44..94..193..324..solved at 410 0..0..4..8..14..30..56..123..261..451..solved at 693 0..0..3..6..11..23..42..86..177..296..solved at 382 0..0..4..8..14..30..54..115..245..423..solved at 665 0..0..4..8..14..30..54..103..214..353..solved at 447 0..0..5..10..17..37..66..138..294..508..solved at 848 0..0..2..4..8..16..30..69..135..229..solved at 311 0..0..3..6..11..23..42..92..189..324..solved at 480 0..0..3..6..11..23..44..94..194..326..solved at 412 0..0..4..8..14..30..56..123..260..449..solved at 691 0..0..3..6..11..23..44..94..194..326..solved at 412 0..0..4..8..14..30..56..123..260..449..solved at 691 0..0..4..8..14..30..56..111..233..387..solved at 481 0..0..5..10..17..37..68..146..311..538..solved at 878 0..0..3..6..11..23..45..98..202..340..solved at 426 0..0..4..8..14..30..55..119..252..435..solved at 677 0..0..4..8..14..30..57..115..241..401..solved at 495 0..0..5..10..17..37..67..142..303..524..solved at 864 0..0..4..8..14..30..57..115..241..401..solved at 495 0..0..5..10..17..37..67..142..303..524..solved at 864 0..0..5..10..17..37..67..124..260..426..solved at 532 0..0..6..12..20..44..77..157..334..577..solved at 1027 0..0..2..4..8..16..29..65..126..213..solved at 295 0..0..3..6..11..23..43..96..198..340..solved at 465 0..0..3..6..11..23..43..90..185..310..solved at 395 0..0..4..8..14..30..57..127..269..465..solved at 673 0..0..3..6..11..23..43..90..185..310..solved at 395 0..0..4..8..14..30..57..127..269..465..solved at 673 0..0..4..8..14..30..55..107..224..371..solved at 463 0..0..5..10..17..37..69..150..320..554..solved at 857 0..0..3..6..11..23..44..94..193..324..solved at 409 0..0..4..8..14..30..56..123..261..451..solved at 659 0..0..4..8..14..30..56..111..232..385..solved at 477 0..0..5..10..17..37..68..146..312..540..solved at 843 0..0..4..8..14..30..56..111..232..385..solved at 477 0..0..5..10..17..37..68..146..312..540..solved at 843 0..0..5..10..17..37..66..120..251..410..solved at 513 0..0..6..12..20..44..78..161..343..593..solved at 1003 0..0..3..6..11..23..42..86..176..294..solved at 379 0..0..4..8..14..30..54..115..242..417..solved at 625 0..0..4..8..14..30..54..103..217..359..solved at 451 0..0..5..10..17..37..66..138..295..510..solved at 813 0..0..4..8..14..30..56..111..233..387..solved at 479 0..0..5..10..17..37..68..146..311..538..solved at 841 0..0..5..10..17..37..66..120..254..416..solved at 519 0..0..6..12..20..44..78..161..344..595..solved at 1005 0..0..4..8..14..30..57..115..241..401..solved at 493 0..0..5..10..17..37..67..142..303..524..solved at 827 0..0..5..10..17..37..67..124..262..430..solved at 533 0..0..6..12..20..44..77..157..336..581..solved at 991 0..0..5..10..17..37..69..132..278..458..solved at 561 0..0..6..12..20..44..79..165..352..609..solved at 1019 0..0..6..12..20..44..77..133..279..451..solved at 569 0..0..7..14..23..51..87..172..365..630..solved at 1159 0..0..1..8..31..110..474..1716..solved at 3337 0..0..0..1..2..3..5..7..9..solved at 16 0..0..1..2..5..9..15..40..67..116..solved at 201 0..0..0..1..2..3..5..7..9..solved at 16 0..0..1..2..5..9..15..30..47..76..solved at 124 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..2..4..7..19..solved at 33 0..0..1..2..3..10..solved at 17 0..0..2..4..7..19..solved at 33 0..0..1..2..3..10..solved at 16 0..0..3..6..17..36..64..solved at 95 0..0..2..4..13..27..47..solved at 60 0..0..1..2..6..12..27..solved at 44 0..0..solved at 2 0..0..1..3..8..14..solved at 20 0..0..1..3..8..13..solved at 19 Warning: inventing type variables 0..0..solved at 2 0..0..0..0..solved at 4 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..1..solved at 4 Warning: inventing type variables 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..2..solved at 6 0..0..solved at 3 0..0..2..solved at 5 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..2..solved at 5 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..2..5..8..solved at 16 0..0..0..0..solved at 4 0..0..0..0..solved at 4 0..0..solved at 2 0..0..0..0..solved at 4 0..0..solved at 2 0..0..solved at 2 0..0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..0..solved at 5 0..0..0..solved at 3 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..solved at 2 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..0..solved at 3 0..0..solved at 2 Warning: inventing type variables 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..2..solved at 6 0..0..1..2..solved at 6 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..1..solved at 4 0..0..solved at 2 0..0..1..solved at 4 0..0..1..solved at 4 File "cart.ml" already loaded Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..0..0..1..9..solved at 20 0..0..0..0..3..12..solved at 27 0..0..1..2..6..16..solved at 31 0..0..solved at 2 0..0..1..2..10..23..45..73..109..150..237..341..solved at 482 0..0..2..7..17..57..111..252..solved at 259 0..0..1..2..5..9..15..24..33..44..67..90..125..186..247..334..524..solved at 604 Warning: inventing type variables Warning: inventing type variables Warning: inventing type variables 0..0..solved at 3 0..0..solved at 3 0..0..solved at 4 0..0..solved at 5 Warning: inventing type variables 0..0..1..3..solved at 7 0..0..1..2..6..11..19..28..37..46..73..100..145..212..279..368..509..650..841..1124..1407..1782..2305..2828..3499..solved at 4403 0..0..1..2..6..12..25..47..84..141..245..solved at 353 0..0..1..2..3..7..35..80..139..252..387..solved at 519 0..0..1..2..3..7..35..80..139..252..387..solved at 463 0..0..1..2..6..11..19..29..39..50..91..141..235..375..577..845..1399..solved at 1533 Warning: inventing type variables Warning: inventing type variables 0..0..1..2..6..12..24..45..76..125..208..solved at 288 0..0..2..4..8..16..28..44..69..101..151..223..solved at 286 0..0..2..4..8..16..28..44..69..100..149..220..309..441..solved at 521 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..6..11..19..38..65..106..192..292..436..solved at 553 0..0..2..4..9..18..52..121..210..359..620..solved at 701 0..0..2..4..9..18..52..121..210..359..620..solved at 878 0..0..3..6..12..25..83..212..381..638..1118..1786..2598..solved at 2715 Warning: inventing type variables 0..0..1..2..7..13..27..43..69..98..153..212..305..432..589..787..1065..1365..1753..2218..2731..3327..4085..4879..5831..solved at 6125 0..0..1..2..7..13..27..43..69..98..153..212..305..432..589..787..1063..1361..1745..2206..2715..3307..4060..4849..5795..6839..7919..9094..10526..11984..13723..solved at 14089 0..0..1..2..7..13..27..43..69..98..153..212..305..410..545..699..915..1153..1461..1852..2291..2819..3481..4179..5007..5941..6911..7984..9353..10748..12463..14302..16229..18272..20734..23204..26101..solved at 26928 0..0..1..2..7..13..27..43..69..98..153..212..305..410..545..699..915..1153..1461..1852..2291..2819..3479..4175..4999..5929..6895..7964..9326..10714..12419..14242..16153..18174..20613..23060..25933..29025..32229..35676..39609..43606..48073..solved at 49267 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..7..19..42..78..137..solved at 187 0..0..1..2..7..19..42..78..137..solved at 187 0..0..1..2..3..7..15..33..92..182..286..491..717..1000..1344..solved at 1660 0..0..1..2..3..7..15..33..92..182..286..491..717..1000..1344..solved at 1547 0..0..1..2..7..13..26..42..66..109..184..282..450..645..906..1214..1585..solved at 1922 0..0..1..2..7..13..26..42..66..109..184..282..450..645..906..1214..1585..solved at 1922 0..0..1..2..6..12..25..41..68..113..197..307..500..726..1041..1410..1881..solved at 2329 0..0..1..2..6..12..25..41..68..113..197..307..500..726..1041..1410..1881..solved at 2329 Warning: inventing type variables 0..0..solved at 2 Warning: inventing type variables 0..0..1..2..7..19..42..78..137..solved at 187 0..0..1..2..3..7..13..23..41..70..112..191..solved at 250 Warning: inventing type variables 0..0..1..2..7..19..42..78..137..solved at 187 0..0..2..4..14..35..68..solved at 84 0..0..2..4..14..35..68..solved at 104 Warning: inventing type variables 0..0..1..2..solved at 6 0..0..1..2..7..19..42..78..140..solved at 193 0..0..2..4..16..39..78..solved at 101 0..0..2..4..16..39..78..solved at 121 0..0..2..4..12..33..80..solved at 109 0..0..1..2..3..7..28..58..93..156..224..320..452..612..798..1098..1416..1822..2337..2900..3583..solved at 4191 0..0..2..4..12..33..80..solved at 89 0..0..1..2..3..7..28..58..93..156..224..320..452..612..798..1098..1416..1822..2337..2900..3583..solved at 4521 0..0..1..2..9..26..54..solved at 83 0..0..1..2..3..7..20..41..67..110..157..227..331..463..620..867..1133..1468..1887..2352..2941..solved at 3821 0..0..1..2..9..26..54..solved at 63 0..0..1..2..3..7..20..41..67..110..157..227..331..463..620..867..1133..1468..1887..2352..2941..solved at 3463 0..0..1..2..solved at 6 0..0..2..4..solved at 9 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 0..0..solved at 4 0..0..solved at 3 0..0..solved at 2 0..0..solved at 2 0..0..solved at 6 0..0..solved at 5 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..0..solved at 3 0..0..1..2..6..12..25..solved at 45 0..0..1..2..3..10..solved at 17 0..0..1..2..9..26..53..solved at 82 0..0..solved at 2 0..0..1..2..9..26..53..solved at 62 0..0..solved at 2 0..0..1..2..5..9..15..22..29..36..67..104..175..273..solved at 350 0..0..0..solved at 3 0..0..0..0..solved at 4 0..0..1..2..6..12..25..41..67..solved at 102 0..0..1..2..3..7..17..30..46..70..97..140..solved at 190 0..0..1..2..9..26..53..solved at 82 0..0..0..solved at 3 0..0..1..2..9..26..53..solved at 62 0..0..0..solved at 3 0..0..1..2..5..9..15..22..29..36..53..70..97..161..232..370..554..815..1134..1579..2071..2741..3531..4571..5783..7374..solved at 8357 Warning: inventing type variables 0..0..solved at 2 0..0..1..3..11..33..69..solved at 111 0..0..1..3..11..33..69..solved at 89 0..0..1..4..13..solved at 18 0..0..1..4..13..solved at 19 0..0..1..4..13..solved at 19 0..0..1..2..solved at 6 0..0..1..3..11..31..61..114..201..302..473..solved at 633 0..0..1..3..11..31..61..114..201..302..473..solved at 562 0..0..1..4..12..27..55..116..196..solved at 236 0..0..1..4..12..27..55..108..178..solved at 219 0..0..2..6..19..50..101..solved at 143 0..0..2..6..19..50..101..solved at 121 0..0..2..7..21..solved at 26 0..0..2..7..21..solved at 27 0..0..1..2..5..11..19..32..solved at 51 0..0..2..5..solved at 9 Warning: inventing type variables 0..0..1..6..11..28..59..115..212..391..solved at 471 Warning: inventing type variables 0..0..1..3..solved at 9 0..0..1..solved at 4 0..0..1..3..solved at 12 0..0..solved at 2 0..0..1..solved at 5 0..0..1..3..solved at 7 0..0..1..solved at 4 0..0..1..3..solved at 8 0..0..3..7..solved at 12 0..0..3..7..solved at 14 0..0..3..8..solved at 17 0..0..3..7..solved at 15 0..0..3..solved at 7 0..0..3..solved at 8 0..0..3..solved at 6 0..0..3..solved at 8 0..0..3..7..solved at 12 0..0..3..7..solved at 14 0..0..3..8..solved at 17 0..0..2..5..solved at 14 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 0..0..solved at 3 Warning: inventing type variables Warning: inventing type variables 0..0..1..2..5..10..17..solved at 26 Warning: inventing type variables Warning: inventing type variables File "/<>/define.ml", line 500, characters 8-29: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (_::_::_::_::_|_::_::[]|_::[]|[]) File "/<>/define.ml", line 726, characters 8-95: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables 0..0..solved at 2 0..0..solved at 2 Warning: inventing type variables Warning: inventing type variables 0..0..0..solved at 3 File "define.ml" already loaded File "/<>/help.ml", line 67, characters 24-40: Warning 3: deprecated: String.uppercase Use String.uppercase_ascii instead. File "/<>/help.ml", line 67, characters 45-61: Warning 3: deprecated: String.uppercase Use String.uppercase_ascii instead. Camlp5 parsing version 7.01 # File "help.ml" already loaded - : unit = () Warning: inventing type variables val nproduct : thm = |- nproduct = iterate (*) Warning: inventing type variables val NPRODUCT_CLAUSES : thm = |- (!f. nproduct {} f = 1) /\ (!x f s. FINITE s ==> nproduct (x INSERT s) f = (if x IN s then nproduct s f else f x * nproduct s f)) Warning: inventing type variables val NPRODUCT_SUPPORT : thm = |- !f s. nproduct (support (*) f s) f = nproduct s f Warning: inventing type variables val NPRODUCT_UNION : thm = |- !f s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> nproduct (s UNION t) f = nproduct s f * nproduct t f Warning: inventing type variables val NPRODUCT_IMAGE : thm = |- !f g s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> nproduct (IMAGE f s) g = nproduct s (g o f) val NPRODUCT_ADD_SPLIT : thm = |- !f m n p. m <= n + 1 ==> nproduct (m..n + p) f = nproduct (m..n) f * nproduct (n + 1..n + p) f Warning: inventing type variables val NPRODUCT_POS_LT : thm = |- !f s. FINITE s /\ (!x. x IN s ==> 0 < f x) ==> 0 < nproduct s f val NPRODUCT_POS_LT_NUMSEG : thm = |- !f m n. (!x. m <= x /\ x <= n ==> 0 < f x) ==> 0 < nproduct (m..n) f val NPRODUCT_OFFSET : thm = |- !f m p. nproduct (m + p..n + p) f = nproduct (m..n) (\i. f (i + p)) Warning: inventing type variables val NPRODUCT_SING : thm = |- !f x. nproduct {x} f = f x val NPRODUCT_SING_NUMSEG : thm = |- !f n. nproduct (n..n) f = f n val NPRODUCT_CLAUSES_NUMSEG : thm = |- (!m. nproduct (m..0) f = (if m = 0 then f 0 else 1)) /\ (!m n. nproduct (m..SUC n) f = (if m <= SUC n then nproduct (m..n) f * f (SUC n) else nproduct (m..n) f)) Warning: inventing type variables val NPRODUCT_EQ : thm = |- !f g s. (!x. x IN s ==> f x = g x) ==> nproduct s f = nproduct s g 0..0..1..4..13..29..64..122..204..solved at 247 val NPRODUCT_EQ_NUMSEG : thm = |- !f g m n. (!i. m <= i /\ i <= n ==> f i = g i) ==> nproduct (m..n) f = nproduct (m..n) g Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 5 0..0..solved at 2 0..0..2..solved at 7 0..0..2..solved at 8 0..0..2..solved at 7 0..0..solved at 2 0..0..3..solved at 9 val NPRODUCT_EQ_0 : thm = |- !f s. FINITE s ==> (nproduct s f = 0 <=> (?x. x IN s /\ f x = 0)) val NPRODUCT_EQ_0_NUMSEG : thm = |- !f m n. nproduct (m..n) f = 0 <=> (?x. m <= x /\ x <= n /\ f x = 0) Warning: inventing type variables 0..0..solved at 2 0..0..3..solved at 6 0..0..2..4..7..solved at 17 val NPRODUCT_LE : thm = |- !f s. FINITE s /\ (!x. x IN s ==> 0 <= f x /\ f x <= g x) ==> nproduct s f <= nproduct s g val NPRODUCT_LE_NUMSEG : thm = |- !f m n. (!i. m <= i /\ i <= n ==> 0 <= f i /\ f i <= g i) ==> nproduct (m..n) f <= nproduct (m..n) g val NPRODUCT_EQ_1 : thm = |- !f s. (!x. x IN s ==> f x = 1) ==> nproduct s f = 1 val NPRODUCT_EQ_1_NUMSEG : thm = |- !f m n. (!i. m <= i /\ i <= n ==> f i = 1) ==> nproduct (m..n) f = 1 Warning: inventing type variables val NPRODUCT_MUL_GEN : thm = |- !f g s. FINITE {x | x IN s /\ ~(f x = 1)} /\ FINITE {x | x IN s /\ ~(g x = 1)} ==> nproduct s (\x. f x * g x) = nproduct s f * nproduct s g Warning: inventing type variables val NPRODUCT_MUL : thm = |- !f g s. FINITE s ==> nproduct s (\x. f x * g x) = nproduct s f * nproduct s g val NPRODUCT_MUL_NUMSEG : thm = |- !f g m n. nproduct (m..n) (\x. f x * g x) = nproduct (m..n) f * nproduct (m..n) g Warning: inventing type variables val NPRODUCT_CONST : thm = |- !c s. FINITE s ==> nproduct s (\x. c) = c EXP CARD s val NPRODUCT_CONST_NUMSEG : thm = |- !c m n. nproduct (m..n) (\x. c) = c EXP ((n + 1) - m) val NPRODUCT_CONST_NUMSEG_1 : thm = |- !c n. nproduct (1..n) (\x. c) = c EXP n Warning: inventing type variables val NPRODUCT_ONE : thm = |- !s. nproduct s (\n. 1) = 1 val NPRODUCT_CLOSED : thm = |- !P f s. P 1 /\ (!x y. P x /\ P y ==> P (x * y)) /\ (!a. a IN s ==> P (f a)) ==> P (nproduct s f) val NPRODUCT_CLAUSES_LEFT : thm = |- !f m n. m <= n ==> nproduct (m..n) f = f m * nproduct (m + 1..n) f val NPRODUCT_CLAUSES_RIGHT : thm = |- !f m n. 0 < n /\ m <= n ==> nproduct (m..n) f = nproduct (m..n - 1) f * f n val NPRODUCT_SUPERSET : thm = |- !f u v. u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> f x = 1) ==> nproduct v f = nproduct u f val NPRODUCT_UNIV : thm = |- !f s. support (*) f (:A) SUBSET s ==> nproduct s f = nproduct (:A) f val NPRODUCT_PAIR : thm = |- !f m n. nproduct (2 * m..2 * n + 1) f = nproduct (m..n) (\i. f (2 * i) * f (2 * i + 1)) val NPRODUCT_REFLECT : thm = |- !x m n. nproduct (m..n) x = (if n < m then 1 else nproduct (0..n - m) (\i. x (n - i))) Warning: inventing type variables val NPRODUCT_DELETE : thm = |- !f s a. FINITE s /\ a IN s ==> f a * nproduct (s DELETE a) f = nproduct s f val NPRODUCT_FACT : thm = |- !n. nproduct (1..n) (\m. m) = FACT n Warning: inventing type variables val NPRODUCT_DELTA : thm = |- !s a. nproduct s (\x. if x = a then b else 1) = (if a IN s then b else 1) Warning: inventing type variables 0..0..solved at 2 0..0..solved at 3 0..0..solved at 2 0..0..2..4..7..19..solved at 33 0..0..1..2..3..10..solved at 17 0..0..2..4..7..19..solved at 33 0..0..1..2..3..10..solved at 16 0..0..3..6..17..36..64..solved at 95 0..0..2..4..13..27..47..solved at 60 0..0..solved at 3 0..0..solved at 2 val HAS_SIZE_CART : thm = |- !P m. (!i. 1 <= i /\ i <= dimindex (:N) ==> {x | P i x} HAS_SIZE m i) ==> {v | !i. 1 <= i /\ i <= dimindex (:N) ==> P i (v$i)} HAS_SIZE nproduct (1..dimindex (:N)) m Warning: inventing type variables 0..0..1..solved at 4 val CARD_CART : thm = |- !P. (!i. 1 <= i /\ i <= dimindex (:N) ==> FINITE {x | P i x}) ==> CARD {v | !i. 1 <= i /\ i <= dimindex (:N) ==> P i (v$i)} = nproduct (1..dimindex (:N)) (\i. CARD {x | P i x}) Warning: inventing type variables - : unit = () - : unit = () Warning: inventing type variables val product : thm = |- product = iterate (*) Warning: inventing type variables val PRODUCT_CLAUSES : thm = |- (!f. product {} f = &1) /\ (!x f s. FINITE s ==> product (x INSERT s) f = (if x IN s then product s f else f x * product s f)) Warning: inventing type variables val PRODUCT_SUPPORT : thm = |- !f s. product (support (*) f s) f = product s f Warning: inventing type variables val PRODUCT_UNION : thm = |- !f s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> product (s UNION t) f = product s f * product t f Warning: inventing type variables val PRODUCT_IMAGE : thm = |- !f g s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> product (IMAGE f s) g = product s (g o f) val PRODUCT_ADD_SPLIT : thm = |- !f m n p. m <= n + 1 ==> product (m..n + p) f = product (m..n) f * product (n + 1..n + p) f Warning: inventing type variables val PRODUCT_POS_LE : thm = |- !f s. FINITE s /\ (!x. x IN s ==> &0 <= f x) ==> &0 <= product s f val PRODUCT_POS_LE_NUMSEG : thm = |- !f m n. (!x. m <= x /\ x <= n ==> &0 <= f x) ==> &0 <= product (m..n) f Warning: inventing type variables val PRODUCT_POS_LT : thm = |- !f s. FINITE s /\ (!x. x IN s ==> &0 < f x) ==> &0 < product s f val PRODUCT_POS_LT_NUMSEG : thm = |- !f m n. (!x. m <= x /\ x <= n ==> &0 < f x) ==> &0 < product (m..n) f val PRODUCT_OFFSET : thm = |- !f m p. product (m + p..n + p) f = product (m..n) (\i. f (i + p)) Warning: inventing type variables val PRODUCT_SING : thm = |- !f x. product {x} f = f x val PRODUCT_SING_NUMSEG : thm = |- !f n. product (n..n) f = f n val PRODUCT_CLAUSES_NUMSEG : thm = |- (!m. product (m..0) f = (if m = 0 then f 0 else &1)) /\ (!m n. product (m..SUC n) f = (if m <= SUC n then product (m..n) f * f (SUC n) else product (m..n) f)) Warning: inventing type variables val PRODUCT_EQ : thm = |- !f g s. (!x. x IN s ==> f x = g x) ==> product s f = product s g 0..0..1..4..13..29..64..122..204..solved at 247 val PRODUCT_EQ_NUMSEG : thm = |- !f g m n. (!i. m <= i /\ i <= n ==> f i = g i) ==> product (m..n) f = product (m..n) g Warning: inventing type variables 0..0..1..solved at 5 0..0..1..solved at 5 0..0..solved at 2 0..0..2..solved at 7 0..0..2..solved at 8 0..0..2..solved at 7 0..0..solved at 2 0..0..3..solved at 9 val PRODUCT_EQ_0 : thm = |- !f s. FINITE s ==> (product s f = &0 <=> (?x. x IN s /\ f x = &0)) val PRODUCT_EQ_0_NUMSEG : thm = |- !f m n. product (m..n) f = &0 <=> (?x. m <= x /\ x <= n /\ f x = &0) Warning: inventing type variables 0..0..3..solved at 6 0..0..3..solved at 6 0..0..2..4..6..14..26..40..57..77..98..142..190..245..338..solved at 450 val PRODUCT_LE : thm = |- !f s. FINITE s /\ (!x. x IN s ==> &0 <= f x /\ f x <= g x) ==> product s f <= product s g val PRODUCT_LE_NUMSEG : thm = |- !f m n. (!i. m <= i /\ i <= n ==> &0 <= f i /\ f i <= g i) ==> product (m..n) f <= product (m..n) g val PRODUCT_EQ_1 : thm = |- !f s. (!x. x IN s ==> f x = &1) ==> product s f = &1 val PRODUCT_EQ_1_NUMSEG : thm = |- !f m n. (!i. m <= i /\ i <= n ==> f i = &1) ==> product (m..n) f = &1 Warning: inventing type variables val PRODUCT_MUL_GEN : thm = |- !f g s. FINITE {x | x IN s /\ ~(f x = &1)} /\ FINITE {x | x IN s /\ ~(g x = &1)} ==> product s (\x. f x * g x) = product s f * product s g Warning: inventing type variables val PRODUCT_MUL : thm = |- !f g s. FINITE s ==> product s (\x. f x * g x) = product s f * product s g val PRODUCT_MUL_NUMSEG : thm = |- !f g m n. product (m..n) (\x. f x * g x) = product (m..n) f * product (m..n) g Warning: inventing type variables val PRODUCT_CONST : thm = |- !c s. FINITE s ==> product s (\x. c) = c pow CARD s val PRODUCT_CONST_NUMSEG : thm = |- !c m n. product (m..n) (\x. c) = c pow ((n + 1) - m) val PRODUCT_CONST_NUMSEG_1 : thm = |- !c n. product (1..n) (\x. c) = c pow n val PRODUCT_NEG : thm = |- !f s. FINITE s ==> product s (\i. --f i) = -- &1 pow CARD s * product s f val PRODUCT_NEG_NUMSEG : thm = |- !f m n. product (m..n) (\i. --f i) = -- &1 pow ((n + 1) - m) * product (m..n) f val PRODUCT_NEG_NUMSEG_1 : thm = |- !f n. product (1..n) (\i. --f i) = -- &1 pow n * product (1..n) f Warning: inventing type variables val PRODUCT_INV : thm = |- !f s. FINITE s ==> product s (\x. inv (f x)) = inv (product s f) Warning: inventing type variables val PRODUCT_DIV : thm = |- !f g s. FINITE s ==> product s (\x. f x / g x) = product s f / product s g val PRODUCT_DIV_NUMSEG : thm = |- !f g m n. product (m..n) (\x. f x / g x) = product (m..n) f / product (m..n) g Warning: inventing type variables val PRODUCT_ONE : thm = |- !s. product s (\n. &1) = &1 Warning: inventing type variables val PRODUCT_LE_1 : thm = |- !f s. FINITE s /\ (!x. x IN s ==> &0 <= f x /\ f x <= &1) ==> product s f <= &1 Warning: inventing type variables val PRODUCT_ABS : thm = |- !f s. FINITE s ==> product s (\x. abs (f x)) = abs (product s f) val PRODUCT_CLOSED : thm = |- !P f s. P (&1) /\ (!x y. P x /\ P y ==> P (x * y)) /\ (!a. a IN s ==> P (f a)) ==> P (product s f) val PRODUCT_CLAUSES_LEFT : thm = |- !f m n. m <= n ==> product (m..n) f = f m * product (m + 1..n) f val PRODUCT_CLAUSES_RIGHT : thm = |- !f m n. 0 < n /\ m <= n ==> product (m..n) f = product (m..n - 1) f * f n val REAL_OF_NUM_NPRODUCT : thm = |- !f s. FINITE s ==> &(nproduct s f) = product s (\x. &(f x)) val PRODUCT_SUPERSET : thm = |- !f u v. u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> f x = &1) ==> product v f = product u f val PRODUCT_UNIV : thm = |- !f s. support (*) f (:A) SUBSET s ==> product s f = product (:A) f val PRODUCT_PAIR : thm = |- !f m n. product (2 * m..2 * n + 1) f = product (m..n) (\i. f (2 * i) * f (2 * i + 1)) val PRODUCT_REFLECT : thm = |- !x m n. product (m..n) x = (if n < m then &1 else product (0..n - m) (\i. x (n - i))) Warning: inventing type variables val PRODUCT_DELETE : thm = |- !f s a. FINITE s /\ a IN s ==> f a * product (s DELETE a) f = product s f Warning: inventing type variables val PRODUCT_DELTA : thm = |- !s a. product s (\x. if x = a then b else &1) = (if a IN s then b else &1) val POLYNOMIAL_FUNCTION_PRODUCT : thm = |- !s p. FINITE s /\ (!i. i IN s ==> polynomial_function (\x. p x i)) ==> polynomial_function (\x. product s (p x)) Warning: inventing type variables - : unit = () - : unit = () - : unit = () 0..0..1..2..6..10..14..solved at 20 0..0..1..2..6..10..14..solved at 22 0..0..1..2..5..10..19..30..45..72..115..188..391..solved at 648 val FORALL_2 : thm = |- !P. (!i. 1 <= i /\ i <= 2 ==> P i) <=> P 1 /\ P 2 val NUMSEG_2 : thm = |- 1..2 = {1, 2} val AGM_2 : thm = |- !x y. x * y <= ((x + y) / &2) pow 2 val SUM_SPLIT_2 : thm = |- sum (1..2 * n) f = sum (1..n) f + sum (n + 1..2 * n) f val PRODUCT_SPLIT_2 : thm = |- product (1..2 * n) f = product (1..n) f * product (n + 1..2 * n) f 0..0..1..4..11..25..51..106..solved at 153 0..0..1..4..11..solved at 21 0..0..1..5..15..37..85..209..492..solved at 962 0..0..1..4..11..25..55..120..227..404..688..1152..1863..3160..solved at 4748 val CAUCHY_INDUCT : thm = |- !P. P 2 /\ (!n. P n ==> P (2 * n)) /\ (!n. P (n + 1) ==> P n) ==> (!n. P n) 1 basis elements and 0 critical pairs 3 basis elements and 0 critical pairs 3 basis elements and 0 critical pairs 3 basis elements and 3 critical pairs 4 basis elements and 5 critical pairs 4 basis elements and 4 critical pairs 4 basis elements and 3 critical pairs 5 basis elements and 0 critical pairs 0..0..1..2..5..solved at 10 0..0..1..solved at 4 0..0..1..2..5..solved at 10 0..0..1..2..4..solved at 9 0..0..1..solved at 4 0..0..1..2..4..6..8..11..14..17..solved at 27 val AGM : thm = |- !n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a i) ==> product (1..n) a <= (sum (1..n) a / &n) pow n val it : unit = () # Error: This kind of expression is not allowed as right-hand side of `let rec' Error in included file /<>/lists.ml Error in Library/agm.ml, test failed make[1]: *** [debian/rules:48: override_dh_auto_test] Error 1 make[1]: Leaving directory '/<>' make: *** [debian/rules:22: build-arch] Error 2 dpkg-buildpackage: error: debian/rules build-arch subprocess returned exit status 2 -------------------------------------------------------------------------------- Build finished at 2018-05-02T12:02:38Z Finished -------- +------------------------------------------------------------------------------+ | Cleanup | +------------------------------------------------------------------------------+ Purging /<> Not cleaning session: cloned chroot in use E: Build failure (dpkg-buildpackage died) +------------------------------------------------------------------------------+ | Summary | +------------------------------------------------------------------------------+ Build Architecture: amd64 Build Type: any Build-Space: 37120 Build-Time: 82 Distribution: unstable Fail-Stage: build Host Architecture: amd64 Install-Time: 12 Job: hol-light_20170109-2 Machine Architecture: amd64 Package: hol-light Package-Time: 109 Source-Version: 20170109-2 Space: 37120 Status: attempted Version: 20170109-2 -------------------------------------------------------------------------------- Finished at 2018-05-02T12:02:38Z Build needed 00:01:49, 37120k disk space E: Build failure (dpkg-buildpackage died) DC-Status: Failed 110.438205694s DC-Time-Estimation: 110.438205694 versus expected 1 (r/m: 109.438205694 ; m: 1.0)