code-conjure 0.5.10 → 0.5.12

raw patch · 72 files changed

+2867/−4720 lines, 72 filesdep ~speculatePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: speculate

API changes (from Hackage documentation)

Files

• .github/workflows/build.yml +91/−49
• Makefile +13/−0
• TODO.md +0/−2
• bench/candidates.hs +3/−3
• bench/candidates.txt +1585/−2107
• bench/erroneous.hs +11/−10
• bench/erroneous.txt +145/−528
• bench/gps.txt +3/−3
• bench/gps2.txt +19/−19
• bench/p12.txt +1/−1
• bench/redundants.hs +8/−7
• bench/redundants.txt +898/−1930
• bench/runtime/lapmatrud/bench/candidates.runtime +1/−1
• bench/runtime/lapmatrud/bench/erroneous.runtime +1/−0
• bench/runtime/lapmatrud/bench/gps2.runtime +1/−1
• bench/runtime/lapmatrud/bench/ill-hit.runtime +1/−1
• bench/runtime/lapmatrud/bench/p12.runtime +1/−1
• bench/runtime/lapmatrud/bench/redundants.runtime +1/−1
• bench/runtime/lapmatrud/bench/terpret.runtime +1/−1
• bench/runtime/lapmatrud/bench/weird.runtime +1/−1
• bench/runtime/lapmatrud/eg/arith.runtime +1/−1
• bench/runtime/lapmatrud/eg/bools.runtime +1/−1
• bench/runtime/lapmatrud/eg/dupos.runtime +1/−1
• bench/runtime/lapmatrud/eg/either.runtime +1/−0
• bench/runtime/lapmatrud/eg/factorial.runtime +1/−1
• bench/runtime/lapmatrud/eg/fib01.runtime +1/−1
• bench/runtime/lapmatrud/eg/fibonacci.runtime +1/−1
• bench/runtime/lapmatrud/eg/higher.runtime +1/−1
• bench/runtime/lapmatrud/eg/ints.runtime +1/−1
• bench/runtime/lapmatrud/eg/list.runtime +1/−1
• bench/runtime/lapmatrud/eg/maybe.runtime +1/−0
• bench/runtime/lapmatrud/eg/oddeven.runtime +1/−0
• bench/runtime/lapmatrud/eg/pow.runtime +1/−1
• bench/runtime/lapmatrud/eg/setelem.runtime +1/−1
• bench/runtime/lapmatrud/eg/sort.runtime +1/−1
• bench/runtime/lapmatrud/eg/spec.runtime +1/−1
• bench/runtime/lapmatrud/eg/subset.runtime +1/−1
• bench/runtime/lapmatrud/eg/tapps.runtime +1/−1
• bench/runtime/lapmatrud/eg/tree.runtime +1/−1
• bench/runtime/lapmatrud/versions +2/−2
• bench/runtime/zero/bench/candidates.runtime +1/−1
• bench/runtime/zero/bench/erroneous.runtime +1/−1
• bench/runtime/zero/bench/gps.runtime +1/−1
• bench/runtime/zero/bench/gps2.runtime +1/−1
• bench/runtime/zero/bench/ill-hit.runtime +1/−1
• bench/runtime/zero/bench/p12.runtime +1/−1
• bench/runtime/zero/bench/redundants.runtime +1/−1
• bench/runtime/zero/bench/terpret.runtime +1/−1
• bench/runtime/zero/bench/weird.runtime +1/−1
• bench/runtime/zero/eg/bst.runtime +1/−1
• bench/runtime/zero/eg/count.runtime +1/−1
• bench/runtime/zero/eg/dupos.runtime +1/−1
• bench/runtime/zero/eg/either.runtime +1/−1
• bench/runtime/zero/eg/fibonacci.runtime +1/−1
• bench/runtime/zero/eg/list.runtime +1/−1
• bench/runtime/zero/eg/oddeven.runtime +1/−1
• bench/runtime/zero/eg/pow.runtime +1/−1
• bench/runtime/zero/eg/replicate.runtime +1/−1
• bench/runtime/zero/eg/sort.runtime +1/−1
• bench/runtime/zero/eg/spec.runtime +1/−1
• bench/runtime/zero/eg/tree.runtime +1/−1
• bench/runtime/zero/versions +1/−1
• bench/weird.hs +2/−2
• changelog.md +8/−0
• code-conjure.cabal +6/−4
• eg/fib01.txt +1/−1
• mk/haskell.mk +7/−2
• src/Conjure/Defn/Test.hs +8/−2
• src/Conjure/Reason.hs +4/−0
• stack.yaml +1/−1
• test/mk +1/−1
• test/sdist +1/−1

@@ -1,8 +1,8 @@ # Builds and tests this Haskell project on "GitHub Actions" #-# 2021-2023  Rudy Matela+# 2021-2024  Rudy Matela #-# some docs: https://github.com/haskell/actions/tree/main/setup+# some docs: https://github.com/haskell-actions/setup # # The official haskell docker image: https://hub.docker.com/_/haskell name: build@@ -11,58 +11,66 @@   build-and-test:     runs-on: ubuntu-latest     steps:+      - run: git   --version+      - run: make  --version+      - run: ghc   --version+      - run: cabal --version -      - name: Cache ~/.cabal/packages+      - name: Check out repository+        uses: actions/checkout@v3++      # check out needs to happen before cache so that hashing works+      - name: Cache hash+        run: echo Cache hash = ${{ hashFiles('*.cabal') }}++      - name: Cache cabal (source) packages         uses: actions/cache@v3         with:-          path: ~/.cabal/packages+          path: |+            ~/.cabal/packages+            ~/.cache/cabal           key:          v1-${{ runner.os }}-cabal-packages-${{ hashFiles('*.cabal') }}           restore-keys: v1-${{ runner.os }}-cabal-packages- -      - name: Cache ~/.cabal and ~/.ghc+      - name: Cache installed cabal packages         uses: actions/cache@v3         with:           path: |             ~/.cabal             !~/.cabal/packages+            ~/.config/cabal+            ~/.local/state/cabal             ~/.ghc           key:          v1-${{ runner.os }}-cabal-ghc-latest-${{ hashFiles('*.cabal') }}-          restore-keys: v1-${{ runner.os }}-cabal-ghc-latest---      - run: du -hd3 ~/.cabal ~/.ghc || true--      - run: make --version+          restore-keys: v1-${{ runner.os }}-cabal-ghc-latest-${{ hashFiles('*.cabal') }}+          # restore with exact match has some versions of cabal have trouble updating        - run: haddock --version || sudo apt-get install ghc-haddock-      - run: ghc     --version-      - run: cabal   --version-      - run: haddock --version-      - run: ghc-pkg list--      - name: Check out repository-        uses: actions/checkout@v3+      # blank line+      # blank line for alignment with matrix scripts -      - run: git --version+      - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true +      - run: ghc-pkg list       - run: make install-dependencies+      - run: ghc-pkg list -      # 2023-07: some projects were failing with missing base for GHC 9.6.-      #          Here we compile through cabal only provisionally.-      # - run: make-      # - run: make test-      # - run: make haddock+      - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true++      - run: make+      - run: make test+      - run: make haddock       - run: make test-sdist-      #- run: make test-via-cabal-      - run: cabal configure --enable-tests --enable-benchmarks --ghc-options="-O0"-      - run: cabal build-      - run: cabal test-      - run: cabal haddock+      - run: make test-via-cabal     test-with-ghc:     strategy:+      max-parallel: 6       matrix:         ghc:+          - '9.8'+          - '9.6'           - '9.4'           - '9.2'           - '9.0'@@ -73,39 +81,52 @@     needs: build-and-test     container: haskell:${{ matrix.ghc }}     steps:-      - name: Cache ~/.cabal/packages+      - run: git   --version || true # git is missing in some images+      - run: make  --version || true # make is missing in some images+      - run: ghc   --version+      - run: cabal --version++      - name: Check out repository+        uses: actions/checkout@v3++      # check out needs to happen before cache so that hashing works+      - name: Cache hash+        run: echo Cache hash = ${{ hashFiles('*.cabal') }}++      - name: Cache cabal (source) packages         uses: actions/cache@v3         with:-          path: ~/.cabal/packages+          path: |+            ~/.cabal/packages+            ~/.cache/cabal           key:          v1-${{ runner.os }}-cabal-packages-${{ hashFiles('*.cabal') }}           restore-keys: v1-${{ runner.os }}-cabal-packages- -      - name: Cache ~/.cabal and ~/.ghc+      - name: Cache installed cabal packages         uses: actions/cache@v3         with:           path: |             ~/.cabal             !~/.cabal/packages+            ~/.config/cabal+            ~/.local/state/cabal             ~/.ghc           key:          v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-${{ hashFiles('*.cabal') }}-          restore-keys: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}---      - run: du -hd3 ~/.cabal ~/.ghc || true+          restore-keys: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-${{ hashFiles('*.cabal') }}+          # restore with exact match has some versions of cabal have trouble updating        - run: make --version || rm /etc/apt/sources.list.d/*.list # faster update       - run: make --version || apt-get update       - run: make --version || apt-get install make -      - run: ghc     --version-      - run: cabal   --version-      - run: haddock --version-      - run: ghc-pkg list--      - name: Check out repository-        uses: actions/checkout@v3+      - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true +      - run: ghc-pkg list       - run: make install-dependencies+      - run: ghc-pkg list +      - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true+       - run: make       - run: make test       - run: make haddock@@ -116,20 +137,41 @@     runs-on: ubuntu-latest     needs: build-and-test     steps:-      - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS-        uses: haskell/actions/setup@v2-        with: # lts-19.19-          ghc-version: '9.0.2'-          cabal-version: '3.4'+      - name: Check out repository+        uses: actions/checkout@v3 -      - uses: actions/cache@v3+      # check out needs to happen before cache so that hashing works+      - name: Cache hash+        run: echo Cache hash = ${{ hashFiles('stack.yaml') }}++      - name: Cache stack folder+        uses: actions/cache@v3         with:           path: ~/.stack           key:          v1-${{ runner.os }}-stack-${{ hashFiles('stack.yaml') }}           restore-keys: v1-${{ runner.os }}-stack- +      - name: Cache ghcup folder+        uses: actions/cache@v3+        with:+          path: |+            ~/.ghcup+            /usr/local/.ghcup/bin+            /usr/local/.ghcup/db+            /usr/local/.ghcup/ghc/9.0.2+          key:          v1-${{ runner.os }}-ghcup-${{ hashFiles('stack.yaml') }}+          restore-keys: v1-${{ runner.os }}-ghcup-++      - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS+        uses: haskell-actions/setup@v2+        with: # lts-19.19+          ghc-version: '9.0.2'+          cabal-version: '3.4'++      - run: du -hd2 ~/.stack ~/.ghcup /usr/local/.ghcup || true+       - run: stack --version -      - name: Check out repository-        uses: actions/checkout@v3       - run: make test-via-stack++      - run: du -hd2 ~/.stack ~/.ghcup /usr/local/.ghcup || true

@@ -10,6 +10,9 @@   | grep -v "^Warning: Couldn't find .haddock for export [A-Z]$$" INSTALL_DEPS = leancheck express speculate template-haskell +NJOBS := $(shell grep ^processor /proc/cpuinfo | head -n -1 | wc -l | sed 's/^0$$/1/')+LONG := $(shell which long >/dev/null 2>/dev/null && echo long)+ EG = \   eg/arith \   eg/count \@@ -104,6 +107,16 @@  test-via-stack: 	stack test code-conjure:test:expr --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal+++fastest:+	$(LONG) make test -j$(NJOBS)++fastestbench:+	$(LONG) make test -j$(NJOBS) && $(LONG) make bench++fastxtestbench:+	$(LONG) make txt -j$(NJOBS) && $(LONG) make test -j$(NJOBS) && $(LONG) make bench  clean: clean-hi-o clean-haddock 	rm -f $(EG) $(TESTS) mk/toplibs

@@ -6,8 +6,6 @@ * improve documentation of `conjureIsDeconstruction`.   Document behaviour outside of function, not inside of it. -* `bench/erroneous`: report number of errors in addition to the example error- * consider non top-level cases  

@@ -37,14 +37,14 @@     [ pr (0 :: Int)     , pr (1 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "-" ((-) :: Int -> Int -> Int)     ] -  printCandidates 9 6 "?" (undefined :: Int -> Int -> Int)+  printCandidates 9 5 "?" (undefined :: Int -> Int -> Int)     [ pr (0 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "dec" (subtract 1 :: Int -> Int)     ] 

@@ -1,2111 +1,1589 @@ Candidates for: foo :: Int -> Int-  pruning with 15/35 rules-  [3,0,7,0,19,0,90,0,454] direct candidates, 0 duplicates-  [3,3,8,9,21,27,98,133,461] pattern candidates, 0 duplicates--rules:-x * y == x + y-x * y == y + x-x - x == 0-x + 0 == x-0 + x == x-x - 0 == x-(x + y) + z == x + (y + z)-(x + y) + z == y + (x + z)-x - (y - z) == z + (x - y)-(x - y) - z == x - (y + z)-(x - y) - z == x - (z + y)-(x + y) - z == x + (y - z)-(x + y) - z == y + (x - z)-x + (y - x) == y-(x - y) + y == x-equations:-y + x == x + y-y + (x + z) == x + (y + z)-z + (x + y) == x + (y + z)-z + (y + x) == x + (y + z)-y + (x - z) == x + (y - z)-(x - z) + y == x + (y - z)-(z - y) + x == (x - y) + z-y - (x + y) == 0 - x-y - (y + x) == 0 - x-z - (y + z) == x - (x + y)-z - (y + z) == x - (y + x)-z - (z + y) == x - (x + y)-z - (z + y) == x - (y + x)-x + (0 - y) == x - y-(0 - y) + x == x - y-x - (x + 1) == 0 - 1-x - (1 + x) == 0 - 1-y - (y + 1) == x - (x + 1)-y - (y + 1) == x - (1 + x)-y - (1 + y) == x - (1 + x)--direct candidates:--foo x  =  x--foo x  =  0--foo x  =  1--foo x  =  x + x--foo x  =  x + 1--foo x  =  1 + 1--foo x  =  x - 1--foo x  =  0 - x--foo x  =  0 - 1--foo x  =  1 - x--foo x  =  x + (x + x)--foo x  =  x + (x + 1)--foo x  =  x + (1 + 1)--foo x  =  x + (x - 1)--foo x  =  x + (0 - 1)--foo x  =  1 + (x + x)--foo x  =  1 + (x + 1)--foo x  =  1 + (1 + 1)--foo x  =  1 + (0 - x)--foo x  =  1 + (1 - x)--foo x  =  x - (x + x)--foo x  =  x - (x + 1)--foo x  =  x - (1 + 1)--foo x  =  0 - (x + x)--foo x  =  0 - (x + 1)--foo x  =  0 - (1 + 1)--foo x  =  1 - (x + x)--foo x  =  1 - (x + 1)--foo x  =  1 - (1 + 1)---pattern candidates:--foo x  =  x--foo x  =  0--foo x  =  1--foo 0  =  0-foo x  =  1--foo 0  =  1-foo x  =  x--foo 0  =  1-foo x  =  0--foo x  =  x + x--foo x  =  x + 1--foo x  =  x - 1--foo x  =  0 - x--foo x  =  1 - x--foo 1  =  0-foo x  =  x--foo 1  =  0-foo x  =  1--foo 1  =  1-foo x  =  0--foo 0  =  0-foo x  =  x + 1--foo 0  =  0-foo x  =  x - 1--foo 0  =  0-foo x  =  1 - x--foo 0  =  1-foo x  =  x + x--foo 0  =  1-foo x  =  x - 1--foo 0  =  1-foo x  =  0 - x--foo 0  =  0-foo 1  =  0-foo x  =  1--foo 0  =  1-foo 1  =  0-foo x  =  x--foo 0  =  1-foo 1  =  1-foo x  =  0--foo x  =  x + (x + x)--foo x  =  x + (x + 1)--foo x  =  x + (x - 1)--foo x  =  1 + (x + x)--foo x  =  1 + (x + 1)--foo x  =  1 + (0 - x)--foo x  =  1 + (1 - x)--foo x  =  x - (x + x)--foo x  =  x - (x + 1)--foo x  =  0 - (x + x)--foo x  =  0 - (x + 1)--foo x  =  1 - (x + x)--foo x  =  1 - (x + 1)--foo 1  =  0-foo x  =  x + x--foo 1  =  0-foo x  =  x + 1--foo 1  =  0-foo x  =  0 - x--foo 1  =  1-foo x  =  x + x--foo 1  =  1-foo x  =  x + 1--foo 1  =  1-foo x  =  x - 1--foo 1  =  1-foo x  =  0 - x--foo 1  =  1-foo x  =  1 - x--foo 0  =  0-foo x  =  x + (x + 1)--foo 0  =  0-foo x  =  x + (x - 1)--foo 0  =  0-foo x  =  1 + (x + x)--foo 0  =  0-foo x  =  1 + (x + 1)--foo 0  =  0-foo x  =  1 + (0 - x)--foo 0  =  0-foo x  =  1 + (1 - x)--foo 0  =  0-foo x  =  x - (x + 1)--foo 0  =  0-foo x  =  0 - (x + 1)--foo 0  =  0-foo x  =  1 - (x + x)--foo 0  =  1-foo x  =  x + (x + x)--foo 0  =  1-foo x  =  x + (x - 1)--foo 0  =  1-foo x  =  1 + (x + 1)--foo 0  =  1-foo x  =  1 + (1 - x)--foo 0  =  1-foo x  =  x - (x + x)--foo 0  =  1-foo x  =  x - (x + 1)--foo 0  =  1-foo x  =  0 - (x + x)--foo 0  =  1-foo x  =  0 - (x + 1)--foo 0  =  1-foo x  =  1 - (x + 1)--foo 0  =  0-foo 1  =  0-foo x  =  x + 1--foo 0  =  0-foo 1  =  1-foo x  =  x + 1--foo 0  =  0-foo 1  =  1-foo x  =  x - 1--foo 0  =  0-foo 1  =  1-foo x  =  1 - x--foo 0  =  1-foo 1  =  0-foo x  =  x + x--foo 0  =  1-foo 1  =  0-foo x  =  0 - x--foo 0  =  1-foo 1  =  1-foo x  =  x + x--foo 0  =  1-foo 1  =  1-foo x  =  x - 1--foo 0  =  1-foo 1  =  1-foo x  =  0 - x---Candidates for: ? :: Int -> Int -> Int-  pruning with 10/23 rules-  [3,3,6,9,21,39,87,180,390] direct candidates, 0 duplicates-  [3,8,22,50,116,302,765,1864,4439] pattern candidates, 0 duplicates--rules:-x * y == x + y-x * y == y + x-x + 0 == x-0 + x == x-dec (x + y) == x + dec y-dec (x + y) == y + dec x-dec (x + y) == dec x + y-dec (x + y) == dec y + x-(x + y) + z == x + (y + z)-(x + y) + z == y + (x + z)-equations:-y + x == x + y-y + dec x == x + dec y-dec x + y == x + dec y-dec y + x == dec x + y-x + dec 0 == dec x-dec 0 + x == dec x-y + (x + z) == x + (y + z)-z + (x + y) == x + (y + z)-z + (y + x) == x + (y + z)-y + dec (dec x) == x + dec (dec y)-dec (dec x) + y == x + dec (dec y)-x + dec (dec 0) == dec (dec x)-dec (dec 0) + x == dec (dec x)--direct candidates:--x ? y  =  x--x ? y  =  y--x ? y  =  0--x ? y  =  dec x--x ? y  =  dec y--x ? y  =  dec 0--x ? y  =  x + x--x ? y  =  x + y--x ? y  =  y + y--x ? y  =  dec (dec x)--x ? y  =  dec (dec y)--x ? y  =  dec (dec 0)--x ? y  =  dec (dec (dec x))--x ? y  =  dec (dec (dec y))--x ? y  =  dec (dec (dec 0))--x ? y  =  x + dec x--x ? y  =  x + dec y--x ? y  =  x + dec 0--x ? y  =  y + dec x--x ? y  =  y + dec y--x ? y  =  y + dec 0--x ? y  =  dec (dec (dec (dec x)))--x ? y  =  dec (dec (dec (dec y)))--x ? y  =  dec (dec (dec (dec 0)))--x ? y  =  x + (x + x)--x ? y  =  x + (x + y)--x ? y  =  x + (y + y)--x ? y  =  x + dec (dec x)--x ? y  =  x + dec (dec y)--x ? y  =  x + dec (dec 0)--x ? y  =  y + (x + x)--x ? y  =  y + (x + y)--x ? y  =  y + (y + y)--x ? y  =  y + dec (dec x)--x ? y  =  y + dec (dec y)--x ? y  =  y + dec (dec 0)--x ? y  =  dec x + dec x--x ? y  =  dec x + dec y--x ? y  =  dec x + dec 0--x ? y  =  dec y + dec y--x ? y  =  dec y + dec 0--x ? y  =  dec 0 + dec 0--x ? y  =  dec (dec (dec (dec (dec x))))--x ? y  =  dec (dec (dec (dec (dec y))))--x ? y  =  dec (dec (dec (dec (dec 0))))--x ? y  =  x + dec (dec (dec x))--x ? y  =  x + dec (dec (dec y))--x ? y  =  x + dec (dec (dec 0))--x ? y  =  x + (x + dec x)--x ? y  =  x + (x + dec y)--x ? y  =  x + (x + dec 0)--x ? y  =  x + (y + dec x)--x ? y  =  x + (y + dec y)--x ? y  =  x + (y + dec 0)--x ? y  =  y + dec (dec (dec x))--x ? y  =  y + dec (dec (dec y))--x ? y  =  y + dec (dec (dec 0))--x ? y  =  y + (x + dec x)--x ? y  =  y + (x + dec y)--x ? y  =  y + (x + dec 0)--x ? y  =  y + (y + dec x)--x ? y  =  y + (y + dec y)--x ? y  =  y + (y + dec 0)--x ? y  =  dec x + (x + x)--x ? y  =  dec x + (x + y)--x ? y  =  dec x + (y + y)--x ? y  =  dec x + dec (dec x)--x ? y  =  dec x + dec (dec y)--x ? y  =  dec x + dec (dec 0)--x ? y  =  dec y + (x + x)--x ? y  =  dec y + (x + y)--x ? y  =  dec y + (y + y)--x ? y  =  dec y + dec (dec x)--x ? y  =  dec y + dec (dec y)--x ? y  =  dec y + dec (dec 0)--x ? y  =  dec 0 + (x + x)--x ? y  =  dec 0 + (x + y)--x ? y  =  dec 0 + (y + y)--x ? y  =  dec 0 + dec (dec x)--x ? y  =  dec 0 + dec (dec y)--x ? y  =  dec 0 + dec (dec 0)---pattern candidates:--x ? y  =  x--x ? y  =  y--x ? y  =  0--x ? y  =  dec x--x ? y  =  dec y--x ? 0  =  x-x ? y  =  y--x ? 0  =  x-x ? y  =  0--x ? 0  =  0-x ? y  =  x--0 ? x  =  x-x ? y  =  x--0 ? x  =  x-x ? y  =  0--0 ? x  =  0-x ? y  =  y--x ? y  =  x + x--x ? y  =  x + y--x ? y  =  y + y--x ? y  =  dec (dec x)--x ? y  =  dec (dec y)--x ? 0  =  x-x ? y  =  dec x--x ? 0  =  x-x ? y  =  dec y--x ? 0  =  0-x ? y  =  dec x--x ? 0  =  0-x ? y  =  dec y--x ? 0  =  dec x-x ? y  =  x--x ? 0  =  dec x-x ? y  =  y--x ? 0  =  dec x-x ? y  =  0--0 ? x  =  x-x ? y  =  dec x--0 ? x  =  x-x ? y  =  dec y--0 ? x  =  0-x ? y  =  dec x--0 ? x  =  0-x ? y  =  dec y--0 ? x  =  dec x-x ? y  =  x--0 ? x  =  dec x-x ? y  =  y--0 ? x  =  dec x-x ? y  =  0--0 ? x  =  x-x ? 0  =  x-x ? y  =  0--0 ? x  =  x-x ? 0  =  0-x ? y  =  x--0 ? x  =  0-x ? 0  =  x-x ? y  =  y--x ? y  =  dec (dec (dec x))--x ? y  =  dec (dec (dec y))--x ? y  =  x + dec x--x ? y  =  x + dec y--x ? y  =  y + dec x--x ? y  =  y + dec y--x ? 0  =  x-x ? y  =  x + x--x ? 0  =  x-x ? y  =  y + y--x ? 0  =  x-x ? y  =  dec (dec x)--x ? 0  =  x-x ? y  =  dec (dec y)--x ? 0  =  0-x ? y  =  x + x--x ? 0  =  0-x ? y  =  x + y--x ? 0  =  0-x ? y  =  dec (dec x)--x ? 0  =  0-x ? y  =  dec (dec y)--x ? 0  =  dec x-x ? y  =  dec y--x ? 0  =  x + x-x ? y  =  x--x ? 0  =  x + x-x ? y  =  y--x ? 0  =  x + x-x ? y  =  0--x ? 0  =  dec (dec x)-x ? y  =  x--x ? 0  =  dec (dec x)-x ? y  =  y--x ? 0  =  dec (dec x)-x ? y  =  0--0 ? x  =  x-x ? y  =  x + x--0 ? x  =  x-x ? y  =  y + y--0 ? x  =  x-x ? y  =  dec (dec x)--0 ? x  =  x-x ? y  =  dec (dec y)--0 ? x  =  0-x ? y  =  x + y--0 ? x  =  0-x ? y  =  y + y--0 ? x  =  0-x ? y  =  dec (dec x)--0 ? x  =  0-x ? y  =  dec (dec y)--0 ? x  =  dec x-x ? y  =  dec x--0 ? x  =  x + x-x ? y  =  x--0 ? x  =  x + x-x ? y  =  y--0 ? x  =  x + x-x ? y  =  0--0 ? x  =  dec (dec x)-x ? y  =  x--0 ? x  =  dec (dec x)-x ? y  =  y--0 ? x  =  dec (dec x)-x ? y  =  0--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec x--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec y--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec x--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec y--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  x--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  0--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec x--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec y--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec x--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec y--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  0--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  x--x ? 0  =  x-x ? y  =  x ? dec y--x ? 0  =  x-x ? y  =  y ? dec x--x ? 0  =  x-x ? y  =  y ? dec y--x ? 0  =  x-x ? y  =  0 ? dec y--x ? 0  =  x-x ? y  =  dec x ? x--x ? 0  =  x-x ? y  =  dec x ? y--x ? 0  =  x-x ? y  =  dec y ? x--0 ? x  =  x-x ? y  =  x ? dec y--0 ? x  =  x-x ? y  =  y ? dec x--0 ? x  =  x-x ? y  =  y ? dec y--0 ? x  =  x-x ? y  =  dec x ? x--0 ? x  =  x-x ? y  =  dec x ? y--0 ? x  =  x-x ? y  =  dec x ? 0--0 ? x  =  x-x ? y  =  dec y ? x--x ? y  =  dec (dec (dec (dec x)))--x ? y  =  dec (dec (dec (dec y)))--x ? y  =  x + (x + x)--x ? y  =  x + (x + y)--x ? y  =  x + (y + y)--x ? y  =  x + dec (dec x)--x ? y  =  x + dec (dec y)--x ? y  =  y + (x + x)--x ? y  =  y + (x + y)--x ? y  =  y + (y + y)--x ? y  =  y + dec (dec x)--x ? y  =  y + dec (dec y)--x ? y  =  dec x + dec x--x ? y  =  dec x + dec y--x ? y  =  dec y + dec y--x ? 0  =  x-x ? y  =  dec (dec (dec x))--x ? 0  =  x-x ? y  =  dec (dec (dec y))--x ? 0  =  x-x ? y  =  x + dec x--x ? 0  =  x-x ? y  =  x + dec y--x ? 0  =  x-x ? y  =  y + dec x--x ? 0  =  x-x ? y  =  y + dec y--x ? 0  =  0-x ? y  =  dec (dec (dec x))--x ? 0  =  0-x ? y  =  dec (dec (dec y))--x ? 0  =  0-x ? y  =  x + dec x--x ? 0  =  0-x ? y  =  x + dec y--x ? 0  =  0-x ? y  =  y + dec x--x ? 0  =  0-x ? y  =  y + dec y--x ? 0  =  dec x-x ? y  =  x + x--x ? 0  =  dec x-x ? y  =  x + y--x ? 0  =  dec x-x ? y  =  y + y--x ? 0  =  dec x-x ? y  =  dec (dec x)--x ? 0  =  dec x-x ? y  =  dec (dec y)--x ? 0  =  x + x-x ? y  =  dec x--x ? 0  =  x + x-x ? y  =  dec y--x ? 0  =  dec (dec x)-x ? y  =  dec x--x ? 0  =  dec (dec x)-x ? y  =  dec y--x ? 0  =  dec (dec (dec x))-x ? y  =  x--x ? 0  =  dec (dec (dec x))-x ? y  =  y--x ? 0  =  dec (dec (dec x))-x ? y  =  0--x ? 0  =  x + dec x-x ? y  =  x--x ? 0  =  x + dec x-x ? y  =  y--x ? 0  =  x + dec x-x ? y  =  0--0 ? x  =  x-x ? y  =  dec (dec (dec x))--0 ? x  =  x-x ? y  =  dec (dec (dec y))--0 ? x  =  x-x ? y  =  x + dec x--0 ? x  =  x-x ? y  =  x + dec y--0 ? x  =  x-x ? y  =  y + dec x--0 ? x  =  x-x ? y  =  y + dec y--0 ? x  =  0-x ? y  =  dec (dec (dec x))--0 ? x  =  0-x ? y  =  dec (dec (dec y))--0 ? x  =  0-x ? y  =  x + dec x--0 ? x  =  0-x ? y  =  x + dec y--0 ? x  =  0-x ? y  =  y + dec x--0 ? x  =  0-x ? y  =  y + dec y--0 ? x  =  dec x-x ? y  =  x + x--0 ? x  =  dec x-x ? y  =  x + y--0 ? x  =  dec x-x ? y  =  y + y--0 ? x  =  dec x-x ? y  =  dec (dec x)--0 ? x  =  dec x-x ? y  =  dec (dec y)--0 ? x  =  x + x-x ? y  =  dec x--0 ? x  =  x + x-x ? y  =  dec y--0 ? x  =  dec (dec x)-x ? y  =  dec x--0 ? x  =  dec (dec x)-x ? y  =  dec y--0 ? x  =  dec (dec (dec x))-x ? y  =  x--0 ? x  =  dec (dec (dec x))-x ? y  =  y--0 ? x  =  dec (dec (dec x))-x ? y  =  0--0 ? x  =  x + dec x-x ? y  =  x--0 ? x  =  x + dec x-x ? y  =  y--0 ? x  =  x + dec x-x ? y  =  0--0 ? x  =  x-x ? 0  =  x-x ? y  =  x + x--0 ? x  =  x-x ? 0  =  x-x ? y  =  y + y--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec (dec x)--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec (dec y)--0 ? x  =  x-x ? 0  =  0-x ? y  =  x + x--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec x)--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec y)--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  dec y--0 ? x  =  x-x ? 0  =  x + x-x ? y  =  x--0 ? x  =  x-x ? 0  =  x + x-x ? y  =  0--0 ? x  =  x-x ? 0  =  dec (dec x)-x ? y  =  x--0 ? x  =  x-x ? 0  =  dec (dec x)-x ? y  =  0--0 ? x  =  0-x ? 0  =  x-x ? y  =  y + y--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec (dec x)--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec (dec y)--0 ? x  =  0-x ? 0  =  0-x ? y  =  x + y--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec (dec x)--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec (dec y)--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  dec y--0 ? x  =  0-x ? 0  =  x + x-x ? y  =  y--0 ? x  =  0-x ? 0  =  dec (dec x)-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  dec x--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  dec x--0 ? x  =  dec x-x ? 0  =  dec x-x ? y  =  x--0 ? x  =  dec x-x ? 0  =  dec x-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  dec x-x ? y  =  0--0 ? x  =  x + x-x ? 0  =  x-x ? y  =  y--0 ? x  =  x + x-x ? 0  =  x-x ? y  =  0--0 ? x  =  x + x-x ? 0  =  0-x ? y  =  x--0 ? x  =  dec (dec x)-x ? 0  =  x-x ? y  =  y--0 ? x  =  dec (dec x)-x ? 0  =  x-x ? y  =  0--0 ? x  =  dec (dec x)-x ? 0  =  0-x ? y  =  x--0 ? 0  =  0-0 ? x  =  dec x-x ? y  =  dec x--x ? 0  =  x-x ? y  =  x ? dec (dec y)--x ? 0  =  x-x ? y  =  y ? dec (dec x)--x ? 0  =  x-x ? y  =  y ? dec (dec y)--x ? 0  =  x-x ? y  =  0 ? dec (dec y)--x ? 0  =  x-x ? y  =  dec x ? dec x--x ? 0  =  x-x ? y  =  dec x ? dec y--x ? 0  =  x-x ? y  =  dec y ? dec x--x ? 0  =  x-x ? y  =  dec y ? dec y--x ? 0  =  x-x ? y  =  dec (dec x) ? x--x ? 0  =  x-x ? y  =  dec (dec x) ? y--x ? 0  =  x-x ? y  =  dec (dec y) ? x--0 ? x  =  x-x ? y  =  x ? dec (dec y)--0 ? x  =  x-x ? y  =  y ? dec (dec x)--0 ? x  =  x-x ? y  =  y ? dec (dec y)--0 ? x  =  x-x ? y  =  dec x ? dec x--0 ? x  =  x-x ? y  =  dec x ? dec y--0 ? x  =  x-x ? y  =  dec y ? dec x--0 ? x  =  x-x ? y  =  dec y ? dec y--0 ? x  =  x-x ? y  =  dec (dec x) ? x--0 ? x  =  x-x ? y  =  dec (dec x) ? y--0 ? x  =  x-x ? y  =  dec (dec x) ? 0--0 ? x  =  x-x ? y  =  dec (dec y) ? x--x ? 0  =  x-x ? y  =  dec (x ? dec y)--x ? 0  =  x-x ? y  =  dec (y ? dec x)--x ? 0  =  x-x ? y  =  dec (y ? dec y)--x ? 0  =  x-x ? y  =  dec (0 ? dec y)--x ? 0  =  x-x ? y  =  dec (dec x ? x)--x ? 0  =  x-x ? y  =  dec (dec x ? y)--x ? 0  =  x-x ? y  =  dec (dec y ? x)--x ? 0  =  0-x ? y  =  dec (x ? dec y)--x ? 0  =  0-x ? y  =  dec (y ? dec x)--x ? 0  =  0-x ? y  =  dec (y ? dec y)--x ? 0  =  0-x ? y  =  dec (0 ? dec y)--x ? 0  =  0-x ? y  =  dec (dec x ? x)--x ? 0  =  0-x ? y  =  dec (dec x ? y)--x ? 0  =  0-x ? y  =  dec (dec y ? x)--x ? 0  =  dec x-x ? y  =  x ? dec y--x ? 0  =  dec x-x ? y  =  y ? dec x--x ? 0  =  dec x-x ? y  =  y ? dec y--x ? 0  =  dec x-x ? y  =  0 ? dec y--x ? 0  =  dec x-x ? y  =  dec x ? x--x ? 0  =  dec x-x ? y  =  dec x ? y--x ? 0  =  dec x-x ? y  =  dec y ? x--0 ? x  =  x-x ? y  =  dec (x ? dec y)--0 ? x  =  x-x ? y  =  dec (y ? dec x)--0 ? x  =  x-x ? y  =  dec (y ? dec y)--0 ? x  =  x-x ? y  =  dec (dec x ? x)--0 ? x  =  x-x ? y  =  dec (dec x ? y)--0 ? x  =  x-x ? y  =  dec (dec x ? 0)--0 ? x  =  x-x ? y  =  dec (dec y ? x)--0 ? x  =  0-x ? y  =  dec (x ? dec y)--0 ? x  =  0-x ? y  =  dec (y ? dec x)--0 ? x  =  0-x ? y  =  dec (y ? dec y)--0 ? x  =  0-x ? y  =  dec (dec x ? x)--0 ? x  =  0-x ? y  =  dec (dec x ? y)--0 ? x  =  0-x ? y  =  dec (dec x ? 0)--0 ? x  =  0-x ? y  =  dec (dec y ? x)--0 ? x  =  dec x-x ? y  =  x ? dec y--0 ? x  =  dec x-x ? y  =  y ? dec x--0 ? x  =  dec x-x ? y  =  y ? dec y--0 ? x  =  dec x-x ? y  =  dec x ? x--0 ? x  =  dec x-x ? y  =  dec x ? y--0 ? x  =  dec x-x ? y  =  dec x ? 0--0 ? x  =  dec x-x ? y  =  dec y ? x--0 ? x  =  x-x ? 0  =  x-x ? y  =  x ? dec y--0 ? x  =  x-x ? 0  =  x-x ? y  =  y ? dec x--0 ? x  =  x-x ? 0  =  x-x ? y  =  y ? dec y--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec x ? x--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec x ? y--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec y ? x--0 ? x  =  x-x ? 0  =  0-x ? y  =  x ? dec y--0 ? x  =  x-x ? 0  =  0-x ? y  =  y ? dec x--0 ? x  =  x-x ? 0  =  0-x ? y  =  y ? dec y--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec x ? x--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec x ? y--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec y ? x--0 ? x  =  0-x ? 0  =  x-x ? y  =  x ? dec y--0 ? x  =  0-x ? 0  =  x-x ? y  =  y ? dec x--0 ? x  =  0-x ? 0  =  x-x ? y  =  y ? dec y--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec x ? x--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec x ? y--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec y ? x--x ? y  =  dec (dec (dec (dec (dec x))))--x ? y  =  dec (dec (dec (dec (dec y))))--x ? y  =  x + dec (dec (dec x))--x ? y  =  x + dec (dec (dec y))--x ? y  =  x + (x + dec x)--x ? y  =  x + (x + dec y)--x ? y  =  x + (y + dec x)--x ? y  =  x + (y + dec y)--x ? y  =  y + dec (dec (dec x))--x ? y  =  y + dec (dec (dec y))--x ? y  =  y + (x + dec x)--x ? y  =  y + (x + dec y)--x ? y  =  y + (y + dec x)--x ? y  =  y + (y + dec y)--x ? y  =  dec x + (x + x)--x ? y  =  dec x + (x + y)--x ? y  =  dec x + (y + y)--x ? y  =  dec x + dec (dec x)--x ? y  =  dec x + dec (dec y)--x ? y  =  dec y + (x + x)--x ? y  =  dec y + (x + y)--x ? y  =  dec y + (y + y)--x ? y  =  dec y + dec (dec x)--x ? y  =  dec y + dec (dec y)--x ? 0  =  x-x ? y  =  dec (dec (dec (dec x)))--x ? 0  =  x-x ? y  =  dec (dec (dec (dec y)))--x ? 0  =  x-x ? y  =  x + (x + x)--x ? 0  =  x-x ? y  =  x + (x + y)--x ? 0  =  x-x ? y  =  x + dec (dec x)--x ? 0  =  x-x ? y  =  x + dec (dec y)--x ? 0  =  x-x ? y  =  y + (x + x)--x ? 0  =  x-x ? y  =  y + (y + y)--x ? 0  =  x-x ? y  =  y + dec (dec x)--x ? 0  =  x-x ? y  =  y + dec (dec y)--x ? 0  =  x-x ? y  =  dec x + dec x--x ? 0  =  x-x ? y  =  dec x + dec y--x ? 0  =  x-x ? y  =  dec y + dec y--x ? 0  =  0-x ? y  =  dec (dec (dec (dec x)))--x ? 0  =  0-x ? y  =  dec (dec (dec (dec y)))--x ? 0  =  0-x ? y  =  x + (x + x)--x ? 0  =  0-x ? y  =  x + (x + y)--x ? 0  =  0-x ? y  =  x + (y + y)--x ? 0  =  0-x ? y  =  x + dec (dec x)--x ? 0  =  0-x ? y  =  x + dec (dec y)--x ? 0  =  0-x ? y  =  y + (x + x)--x ? 0  =  0-x ? y  =  y + (x + y)--x ? 0  =  0-x ? y  =  y + dec (dec x)--x ? 0  =  0-x ? y  =  y + dec (dec y)--x ? 0  =  0-x ? y  =  dec x + dec x--x ? 0  =  0-x ? y  =  dec x + dec y--x ? 0  =  0-x ? y  =  dec y + dec y--x ? 0  =  dec x-x ? y  =  dec (dec (dec x))--x ? 0  =  dec x-x ? y  =  dec (dec (dec y))--x ? 0  =  dec x-x ? y  =  x + dec x--x ? 0  =  dec x-x ? y  =  x + dec y--x ? 0  =  dec x-x ? y  =  y + dec y--x ? 0  =  x + x-x ? y  =  x + y--x ? 0  =  x + x-x ? y  =  y + y--x ? 0  =  x + x-x ? y  =  dec (dec x)--x ? 0  =  x + x-x ? y  =  dec (dec y)--x ? 0  =  dec (dec x)-x ? y  =  x + x--x ? 0  =  dec (dec x)-x ? y  =  x + y--x ? 0  =  dec (dec x)-x ? y  =  y + y--x ? 0  =  dec (dec x)-x ? y  =  dec (dec y)--x ? 0  =  dec (dec (dec x))-x ? y  =  dec x--x ? 0  =  dec (dec (dec x))-x ? y  =  dec y--x ? 0  =  x + dec x-x ? y  =  dec x--x ? 0  =  x + dec x-x ? y  =  dec y--x ? 0  =  dec (dec (dec (dec x)))-x ? y  =  x--x ? 0  =  dec (dec (dec (dec x)))-x ? y  =  y--x ? 0  =  dec (dec (dec (dec x)))-x ? y  =  0--x ? 0  =  x + (x + x)-x ? y  =  x--x ? 0  =  x + (x + x)-x ? y  =  y--x ? 0  =  x + (x + x)-x ? y  =  0--x ? 0  =  x + dec (dec x)-x ? y  =  x--x ? 0  =  x + dec (dec x)-x ? y  =  y--x ? 0  =  x + dec (dec x)-x ? y  =  0--x ? 0  =  dec x + dec x-x ? y  =  x--x ? 0  =  dec x + dec x-x ? y  =  y--x ? 0  =  dec x + dec x-x ? y  =  0--0 ? x  =  x-x ? y  =  dec (dec (dec (dec x)))--0 ? x  =  x-x ? y  =  dec (dec (dec (dec y)))--0 ? x  =  x-x ? y  =  x + (x + x)--0 ? x  =  x-x ? y  =  x + (y + y)--0 ? x  =  x-x ? y  =  x + dec (dec x)--0 ? x  =  x-x ? y  =  x + dec (dec y)--0 ? x  =  x-x ? y  =  y + (x + y)--0 ? x  =  x-x ? y  =  y + (y + y)--0 ? x  =  x-x ? y  =  y + dec (dec x)--0 ? x  =  x-x ? y  =  y + dec (dec y)--0 ? x  =  x-x ? y  =  dec x + dec x--0 ? x  =  x-x ? y  =  dec x + dec y--0 ? x  =  x-x ? y  =  dec y + dec y--0 ? x  =  0-x ? y  =  dec (dec (dec (dec x)))--0 ? x  =  0-x ? y  =  dec (dec (dec (dec y)))--0 ? x  =  0-x ? y  =  x + (x + y)--0 ? x  =  0-x ? y  =  x + (y + y)--0 ? x  =  0-x ? y  =  x + dec (dec x)--0 ? x  =  0-x ? y  =  x + dec (dec y)--0 ? x  =  0-x ? y  =  y + (x + x)--0 ? x  =  0-x ? y  =  y + (x + y)--0 ? x  =  0-x ? y  =  y + (y + y)--0 ? x  =  0-x ? y  =  y + dec (dec x)--0 ? x  =  0-x ? y  =  y + dec (dec y)--0 ? x  =  0-x ? y  =  dec x + dec x--0 ? x  =  0-x ? y  =  dec x + dec y--0 ? x  =  0-x ? y  =  dec y + dec y--0 ? x  =  dec x-x ? y  =  dec (dec (dec x))--0 ? x  =  dec x-x ? y  =  dec (dec (dec y))--0 ? x  =  dec x-x ? y  =  x + dec x--0 ? x  =  dec x-x ? y  =  y + dec x--0 ? x  =  dec x-x ? y  =  y + dec y--0 ? x  =  x + x-x ? y  =  x + x--0 ? x  =  x + x-x ? y  =  x + y--0 ? x  =  x + x-x ? y  =  dec (dec x)--0 ? x  =  x + x-x ? y  =  dec (dec y)--0 ? x  =  dec (dec x)-x ? y  =  x + x--0 ? x  =  dec (dec x)-x ? y  =  x + y--0 ? x  =  dec (dec x)-x ? y  =  y + y--0 ? x  =  dec (dec x)-x ? y  =  dec (dec x)--0 ? x  =  dec (dec (dec x))-x ? y  =  dec x--0 ? x  =  dec (dec (dec x))-x ? y  =  dec y--0 ? x  =  x + dec x-x ? y  =  dec x--0 ? x  =  x + dec x-x ? y  =  dec y--0 ? x  =  dec (dec (dec (dec x)))-x ? y  =  x--0 ? x  =  dec (dec (dec (dec x)))-x ? y  =  y--0 ? x  =  dec (dec (dec (dec x)))-x ? y  =  0--0 ? x  =  x + (x + x)-x ? y  =  x--0 ? x  =  x + (x + x)-x ? y  =  y--0 ? x  =  x + (x + x)-x ? y  =  0--0 ? x  =  x + dec (dec x)-x ? y  =  x--0 ? x  =  x + dec (dec x)-x ? y  =  y--0 ? x  =  x + dec (dec x)-x ? y  =  0--0 ? x  =  dec x + dec x-x ? y  =  x--0 ? x  =  dec x + dec x-x ? y  =  y--0 ? x  =  dec x + dec x-x ? y  =  0--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec (dec (dec x))--0 ? x  =  x-x ? 0  =  x-x ? y  =  dec (dec (dec y))--0 ? x  =  x-x ? 0  =  x-x ? y  =  x + dec x--0 ? x  =  x-x ? 0  =  x-x ? y  =  x + dec y--0 ? x  =  x-x ? 0  =  x-x ? y  =  y + dec x--0 ? x  =  x-x ? 0  =  x-x ? y  =  y + dec y--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec (dec x))--0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec (dec y))--0 ? x  =  x-x ? 0  =  0-x ? y  =  x + dec x--0 ? x  =  x-x ? 0  =  0-x ? y  =  x + dec y--0 ? x  =  x-x ? 0  =  0-x ? y  =  y + dec x--0 ? x  =  x-x ? 0  =  0-x ? y  =  y + dec y--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  x + x--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  y + y--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  dec (dec x)--0 ? x  =  x-x ? 0  =  dec x-x ? y  =  dec (dec y)--0 ? x  =  x-x ? 0  =  x + x-x ? y  =  dec x--0 ? x  =  x-x ? 0  =  x + x-x ? y  =  dec y--0 ? x  =  x-x ? 0  =  dec (dec x)-x ? y  =  dec x--0 ? x  =  x-x ? 0  =  dec (dec x)-x ? y  =  dec y--0 ? x  =  x-x ? 0  =  dec (dec (dec x))-x ? y  =  x--0 ? x  =  x-x ? 0  =  dec (dec (dec x))-x ? y  =  0--0 ? x  =  x-x ? 0  =  x + dec x-x ? y  =  x--0 ? x  =  x-x ? 0  =  x + dec x-x ? y  =  0--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec (dec (dec x))--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec (dec (dec y))--0 ? x  =  0-x ? 0  =  x-x ? y  =  x + dec x--0 ? x  =  0-x ? 0  =  x-x ? y  =  x + dec y--0 ? x  =  0-x ? 0  =  x-x ? y  =  y + dec x--0 ? x  =  0-x ? 0  =  x-x ? y  =  y + dec y--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec (dec (dec x))--0 ? x  =  0-x ? 0  =  0-x ? y  =  dec (dec (dec y))--0 ? x  =  0-x ? 0  =  0-x ? y  =  x + dec x--0 ? x  =  0-x ? 0  =  0-x ? y  =  x + dec y--0 ? x  =  0-x ? 0  =  0-x ? y  =  y + dec x--0 ? x  =  0-x ? 0  =  0-x ? y  =  y + dec y--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  x + y--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  y + y--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  dec (dec x)--0 ? x  =  0-x ? 0  =  dec x-x ? y  =  dec (dec y)--0 ? x  =  0-x ? 0  =  x + x-x ? y  =  dec x--0 ? x  =  0-x ? 0  =  x + x-x ? y  =  dec y--0 ? x  =  0-x ? 0  =  dec (dec x)-x ? y  =  dec x--0 ? x  =  0-x ? 0  =  dec (dec x)-x ? y  =  dec y--0 ? x  =  0-x ? 0  =  dec (dec (dec x))-x ? y  =  y--0 ? x  =  0-x ? 0  =  x + dec x-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  x + x--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  y + y--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  dec (dec x)--0 ? x  =  dec x-x ? 0  =  x-x ? y  =  dec (dec y)--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  x + x--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  x + y--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  dec (dec x)--0 ? x  =  dec x-x ? 0  =  0-x ? y  =  dec (dec y)--0 ? x  =  dec x-x ? 0  =  x + x-x ? y  =  x--0 ? x  =  dec x-x ? 0  =  x + x-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  x + x-x ? y  =  0--0 ? x  =  dec x-x ? 0  =  dec (dec x)-x ? y  =  x--0 ? x  =  dec x-x ? 0  =  dec (dec x)-x ? y  =  y--0 ? x  =  dec x-x ? 0  =  dec (dec x)-x ? y  =  0--0 ? x  =  x + x-x ? 0  =  x-x ? y  =  dec x--0 ? x  =  x + x-x ? 0  =  x-x ? y  =  dec y--0 ? x  =  x + x-x ? 0  =  0-x ? y  =  dec x--0 ? x  =  x + x-x ? 0  =  0-x ? y  =  dec y--0 ? x  =  x + x-x ? 0  =  dec x-x ? y  =  x--0 ? x  =  x + x-x ? 0  =  dec x-x ? y  =  y--0 ? x  =  x + x-x ? 0  =  dec x-x ? y  =  0--0 ? x  =  dec (dec x)-x ? 0  =  x-x ? y  =  dec x--0 ? x  =  dec (dec x)-x ? 0  =  x-x ? y  =  dec y--0 ? x  =  dec (dec x)-x ? 0  =  0-x ? y  =  dec x--0 ? x  =  dec (dec x)-x ? 0  =  0-x ? y  =  dec y--0 ? x  =  dec (dec x)-x ? 0  =  dec x-x ? y  =  x--0 ? x  =  dec (dec x)-x ? 0  =  dec x-x ? y  =  y--0 ? x  =  dec (dec x)-x ? 0  =  dec x-x ? y  =  0--0 ? x  =  dec (dec (dec x))-x ? 0  =  x-x ? y  =  y--0 ? x  =  dec (dec (dec x))-x ? 0  =  x-x ? y  =  0--0 ? x  =  dec (dec (dec x))-x ? 0  =  0-x ? y  =  x--0 ? x  =  x + dec x-x ? 0  =  x-x ? y  =  y--0 ? x  =  x + dec x-x ? 0  =  x-x ? y  =  0--0 ? x  =  x + dec x-x ? 0  =  0-x ? y  =  x--0 ? 0  =  0-0 ? x  =  dec x-x ? y  =  dec (dec x)--0 ? 0  =  0-0 ? x  =  dec x-x ? y  =  dec (dec y)--0 ? 0  =  0-0 ? x  =  dec (dec x)-x ? y  =  dec x--0 ? 0  =  0-0 ? x  =  dec (dec x)-x ? y  =  dec y+  pruning with 27/65 rules+  [3,0,8,0,30,0,194,0,1406] direct candidates, 0 duplicates+  [3,3,9,10,32,39,197,247,1325] pattern candidates, 0 duplicates++rules:+x - x == 0+x * 0 == 0+x * 1 == x+0 * x == 0+1 * x == x+x + 0 == x+0 + x == x+x - 0 == x+(x * y) * z == x * (y * z)+(x * y) * z == y * (x * z)+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+x - (y - z) == z + (x - y)+(x - y) - z == x - (y + z)+(x - y) - z == x - (z + y)+(x + y) - z == x + (y - z)+(x + y) - z == y + (x - z)+(x + x) * y == x * (y + y)+x + (y - x) == y+(x - y) + y == x+x * y - x == x * (y - 1)+x * y - y == y * (x - 1)+x * (y + 1) == x + x * y+x * (y + 1) == x * y + x+(x + 1) * y == y + x * y+0 - x * y == x * (0 - y)+0 - x * y == y * (0 - x)+equations:+y * x == x * y+y + x == x + y+y * (x * z) == x * (y * z)+z * (x * y) == x * (y * z)+z * (y * x) == x * (y * z)+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+y + (x - z) == x + (y - z)+z * y + x == x + y * z+(x - z) + y == x + (y - z)+(z - y) + x == (x - y) + z+y * (x + x) == x * (y + y)+y - (x + y) == 0 - x+y - (y + x) == 0 - x+z - (y + z) == x - (x + y)+z - (y + z) == x - (y + x)+z - (z + y) == x - (x + y)+z - (z + y) == x - (y + x)+x * (1 - y) == x - x * y+x * (1 - y) == x - y * x+y * (0 - x) == x * (0 - y)+(0 - x) * y == x * (0 - y)+(0 - y) * x == (0 - x) * y+(1 - y) * x == x - x * y+(1 - y) * x == x - y * x+x + (0 - y) == x - y+(0 - y) + x == x - y+x - (x + 1) == 0 - 1+x - (1 + x) == 0 - 1+y - (y + 1) == x - (x + 1)+y - (y + 1) == x - (1 + x)+y - (1 + y) == x - (1 + x)+x * (0 - 1) == 0 - x+(0 - 1) * x == 0 - x+(0 - 1) * y == x - (x + y)+(0 - 1) * y == x - (y + x)++direct candidates:++foo x  =  x++foo x  =  0++foo x  =  1++foo x  =  x + x++foo x  =  x + 1++foo x  =  1 + 1++foo x  =  x * x++foo x  =  x - 1++foo x  =  0 - x++foo x  =  0 - 1++foo x  =  1 - x++foo x  =  x * x - 1++foo x  =  x + (x + x)++foo x  =  x + (x + 1)++foo x  =  x + (1 + 1)++foo x  =  x + x * x++foo x  =  x + (x - 1)++foo x  =  x + (0 - 1)++foo x  =  1 + (x + x)++foo x  =  1 + (x + 1)++foo x  =  1 + (1 + 1)++foo x  =  1 + x * x++foo x  =  1 + (0 - x)++foo x  =  1 + (1 - x)++foo x  =  x * (x + x)++foo x  =  x * (x * x)++foo x  =  x * (x - 1)++foo x  =  x * (0 - x)++foo x  =  x * (0 - 1)++foo x  =  x * (1 - x)++foo x  =  x - (x + x)++foo x  =  x - (x + 1)++foo x  =  x - (1 + 1)++foo x  =  x - x * x++foo x  =  0 - (x + x)++foo x  =  0 - (x + 1)++foo x  =  0 - (1 + 1)++foo x  =  1 - (x + x)++foo x  =  1 - (x + 1)++foo x  =  1 - (1 + 1)++foo x  =  1 - x * x+++pattern candidates:++foo x  =  x++foo x  =  0++foo x  =  1++foo 0  =  0+foo x  =  1++foo 0  =  1+foo x  =  x++foo 0  =  1+foo x  =  0++foo x  =  x + x++foo x  =  x + 1++foo x  =  x * x++foo x  =  x - 1++foo x  =  0 - x++foo x  =  1 - x++foo 1  =  0+foo x  =  x++foo 1  =  0+foo x  =  1++foo 1  =  1+foo x  =  0++foo 0  =  0+foo x  =  x + 1++foo 0  =  0+foo x  =  x - 1++foo 0  =  0+foo x  =  1 - x++foo 0  =  1+foo x  =  x + x++foo 0  =  1+foo x  =  x * x++foo 0  =  1+foo x  =  x - 1++foo 0  =  1+foo x  =  0 - x++foo 0  =  0+foo 1  =  0+foo x  =  1++foo 0  =  1+foo 1  =  0+foo x  =  x++foo 0  =  1+foo 1  =  1+foo x  =  0++foo x  =  x * x - 1++foo x  =  x + (x + x)++foo x  =  x + (x + 1)++foo x  =  x + x * x++foo x  =  x + (x - 1)++foo x  =  1 + (x + x)++foo x  =  1 + (x + 1)++foo x  =  1 + x * x++foo x  =  1 + (0 - x)++foo x  =  1 + (1 - x)++foo x  =  x * (x + x)++foo x  =  x * (x * x)++foo x  =  x * (x - 1)++foo x  =  x * (0 - x)++foo x  =  x * (1 - x)++foo x  =  x - (x + x)++foo x  =  x - (x + 1)++foo x  =  x - x * x++foo x  =  0 - (x + x)++foo x  =  0 - (x + 1)++foo x  =  1 - (x + x)++foo x  =  1 - (x + 1)++foo x  =  1 - x * x++foo 1  =  0+foo x  =  x + x++foo 1  =  0+foo x  =  x + 1++foo 1  =  0+foo x  =  x * x++foo 1  =  0+foo x  =  0 - x++foo 1  =  1+foo x  =  x + x++foo 1  =  1+foo x  =  x + 1++foo 1  =  1+foo x  =  x - 1++foo 1  =  1+foo x  =  0 - x++foo 1  =  1+foo x  =  1 - x++foo 0  =  0+foo x  =  x * x - 1++foo 0  =  0+foo x  =  x + (x + 1)++foo 0  =  0+foo x  =  x + (x - 1)++foo 0  =  0+foo x  =  1 + (x + x)++foo 0  =  0+foo x  =  1 + (x + 1)++foo 0  =  0+foo x  =  1 + x * x++foo 0  =  0+foo x  =  1 + (0 - x)++foo 0  =  0+foo x  =  1 + (1 - x)++foo 0  =  0+foo x  =  x - (x + 1)++foo 0  =  0+foo x  =  0 - (x + 1)++foo 0  =  0+foo x  =  1 - (x + x)++foo 0  =  0+foo x  =  1 - x * x++foo 0  =  1+foo x  =  x * x - 1++foo 0  =  1+foo x  =  x + (x + x)++foo 0  =  1+foo x  =  x + x * x++foo 0  =  1+foo x  =  x + (x - 1)++foo 0  =  1+foo x  =  1 + (x + 1)++foo 0  =  1+foo x  =  1 + (1 - x)++foo 0  =  1+foo x  =  x * (x + x)++foo 0  =  1+foo x  =  x * (x * x)++foo 0  =  1+foo x  =  x * (x - 1)++foo 0  =  1+foo x  =  x * (0 - x)++foo 0  =  1+foo x  =  x * (1 - x)++foo 0  =  1+foo x  =  x - (x + x)++foo 0  =  1+foo x  =  x - (x + 1)++foo 0  =  1+foo x  =  x - x * x++foo 0  =  1+foo x  =  0 - (x + x)++foo 0  =  1+foo x  =  0 - (x + 1)++foo 0  =  1+foo x  =  1 - (x + 1)++foo 0  =  0+foo 1  =  0+foo x  =  x + 1++foo 0  =  0+foo 1  =  1+foo x  =  x + 1++foo 0  =  0+foo 1  =  1+foo x  =  x - 1++foo 0  =  0+foo 1  =  1+foo x  =  1 - x++foo 0  =  1+foo 1  =  0+foo x  =  x + x++foo 0  =  1+foo 1  =  0+foo x  =  x * x++foo 0  =  1+foo 1  =  0+foo x  =  0 - x++foo 0  =  1+foo 1  =  1+foo x  =  x + x++foo 0  =  1+foo 1  =  1+foo x  =  x - 1++foo 0  =  1+foo 1  =  1+foo x  =  0 - x+++Candidates for: ? :: Int -> Int -> Int+  pruning with 13/34 rules+  [3,3,9,18,60,162,516,1587,5148] direct candidates, 0 duplicates+  [3,8,25,71,205,632,1976,6067,19140] pattern candidates, 0 duplicates++rules:+x * 0 == 0+0 * x == 0+x + 0 == x+0 + x == x+dec (x + y) == x + dec y+dec (x + y) == y + dec x+dec (x + y) == dec x + y+dec (x + y) == dec y + x+(x * y) * z == x * (y * z)+(x * y) * z == y * (x * z)+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+(x + x) * y == x * (y + y)+equations:+y * x == x * y+y + x == x + y+y + dec x == x + dec y+dec x + y == x + dec y+dec y + x == dec x + y+x + dec 0 == dec x+dec 0 + x == dec x+y * (x * z) == x * (y * z)+z * (x * y) == x * (y * z)+z * (y * x) == x * (y * z)+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+z * y + x == x + y * z+y * (x + x) == x * (y + y)+y + dec (dec x) == x + dec (dec y)+dec (dec x) + y == x + dec (dec y)+dec (dec y) + x == dec (dec x) + y+x + dec (dec 0) == dec (dec x)+dec (dec 0) + x == dec (dec x)++direct candidates:++x ? y  =  x++x ? y  =  y++x ? y  =  0++x ? y  =  dec x++x ? y  =  dec y++x ? y  =  dec 0++x ? y  =  x + x++x ? y  =  x + y++x ? y  =  y + y++x ? y  =  x * x++x ? y  =  x * y++x ? y  =  y * y++x ? y  =  dec (dec x)++x ? y  =  dec (dec y)++x ? y  =  dec (dec 0)++x ? y  =  dec (x * x)++x ? y  =  dec (x * y)++x ? y  =  dec (y * y)++x ? y  =  dec (dec (dec x))++x ? y  =  dec (dec (dec y))++x ? y  =  dec (dec (dec 0))++x ? y  =  x + dec x++x ? y  =  x + dec y++x ? y  =  x + dec 0++x ? y  =  y + dec x++x ? y  =  y + dec y++x ? y  =  y + dec 0++x ? y  =  x * dec x++x ? y  =  x * dec y++x ? y  =  x * dec 0++x ? y  =  y * dec x++x ? y  =  y * dec y++x ? y  =  y * dec 0++x ? y  =  dec (dec (x * x))++x ? y  =  dec (dec (x * y))++x ? y  =  dec (dec (y * y))++x ? y  =  dec (dec (dec (dec x)))++x ? y  =  dec (dec (dec (dec y)))++x ? y  =  dec (dec (dec (dec 0)))++x ? y  =  dec (x * dec x)++x ? y  =  dec (x * dec y)++x ? y  =  dec (x * dec 0)++x ? y  =  dec (y * dec x)++x ? y  =  dec (y * dec y)++x ? y  =  dec (y * dec 0)++x ? y  =  x + (x + x)++x ? y  =  x + (x + y)++x ? y  =  x + (y + y)++x ? y  =  x + x * x++x ? y  =  x + x * y++x ? y  =  x + y * y++x ? y  =  x + dec (dec x)++x ? y  =  x + dec (dec y)++x ? y  =  x + dec (dec 0)++x ? y  =  y + (x + x)++x ? y  =  y + (x + y)++x ? y  =  y + (y + y)++x ? y  =  y + x * x++x ? y  =  y + x * y++x ? y  =  y + y * y++x ? y  =  y + dec (dec x)++x ? y  =  y + dec (dec y)++x ? y  =  y + dec (dec 0)++x ? y  =  x * (x + x)++x ? y  =  x * (x + y)++x ? y  =  x * (y + y)++x ? y  =  x * (x * x)++x ? y  =  x * (x * y)++x ? y  =  x * (y * y)++x ? y  =  x * dec (dec x)++x ? y  =  x * dec (dec y)++x ? y  =  x * dec (dec 0)++x ? y  =  y * (x + x)++x ? y  =  y * (x + y)++x ? y  =  y * (y + y)++x ? y  =  y * (x * x)++x ? y  =  y * (x * y)++x ? y  =  y * (y * y)++x ? y  =  y * dec (dec x)++x ? y  =  y * dec (dec y)++x ? y  =  y * dec (dec 0)++x ? y  =  dec x + dec x++x ? y  =  dec x + dec y++x ? y  =  dec x + dec 0++x ? y  =  dec y + dec y++x ? y  =  dec y + dec 0++x ? y  =  dec 0 + dec 0++x ? y  =  dec x * dec x++x ? y  =  dec x * dec y++x ? y  =  dec x * dec 0++x ? y  =  dec y * dec y++x ? y  =  dec y * dec 0++x ? y  =  dec 0 * dec 0+++pattern candidates:++x ? y  =  x++x ? y  =  y++x ? y  =  0++x ? y  =  dec x++x ? y  =  dec y++x ? 0  =  x+x ? y  =  y++x ? 0  =  x+x ? y  =  0++x ? 0  =  0+x ? y  =  x++0 ? x  =  x+x ? y  =  x++0 ? x  =  x+x ? y  =  0++0 ? x  =  0+x ? y  =  y++x ? y  =  x + x++x ? y  =  x + y++x ? y  =  y + y++x ? y  =  x * x++x ? y  =  x * y++x ? y  =  y * y++x ? y  =  dec (dec x)++x ? y  =  dec (dec y)++x ? 0  =  x+x ? y  =  dec x++x ? 0  =  x+x ? y  =  dec y++x ? 0  =  0+x ? y  =  dec x++x ? 0  =  0+x ? y  =  dec y++x ? 0  =  dec x+x ? y  =  x++x ? 0  =  dec x+x ? y  =  y++x ? 0  =  dec x+x ? y  =  0++0 ? x  =  x+x ? y  =  dec x++0 ? x  =  x+x ? y  =  dec y++0 ? x  =  0+x ? y  =  dec x++0 ? x  =  0+x ? y  =  dec y++0 ? x  =  dec x+x ? y  =  x++0 ? x  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x+x ? 0  =  0+x ? y  =  x++0 ? x  =  0+x ? 0  =  x+x ? y  =  y++x ? y  =  dec (x * x)++x ? y  =  dec (x * y)++x ? y  =  dec (y * y)++x ? y  =  dec (dec (dec x))++x ? y  =  dec (dec (dec y))++x ? y  =  x + dec x++x ? y  =  x + dec y++x ? y  =  y + dec x++x ? y  =  y + dec y++x ? y  =  x * dec x++x ? y  =  x * dec y++x ? y  =  y * dec x++x ? y  =  y * dec y++x ? 0  =  x+x ? y  =  x + x++x ? 0  =  x+x ? y  =  y + y++x ? 0  =  x+x ? y  =  x * x++x ? 0  =  x+x ? y  =  x * y++x ? 0  =  x+x ? y  =  y * y++x ? 0  =  x+x ? y  =  dec (dec x)++x ? 0  =  x+x ? y  =  dec (dec y)++x ? 0  =  0+x ? y  =  x + x++x ? 0  =  0+x ? y  =  x + y++x ? 0  =  0+x ? y  =  x * x++x ? 0  =  0+x ? y  =  dec (dec x)++x ? 0  =  0+x ? y  =  dec (dec y)++x ? 0  =  dec x+x ? y  =  dec y++x ? 0  =  x + x+x ? y  =  x++x ? 0  =  x + x+x ? y  =  y++x ? 0  =  x + x+x ? y  =  0++x ? 0  =  x * x+x ? y  =  x++x ? 0  =  x * x+x ? y  =  y++x ? 0  =  x * x+x ? y  =  0++x ? 0  =  dec (dec x)+x ? y  =  x++x ? 0  =  dec (dec x)+x ? y  =  y++x ? 0  =  dec (dec x)+x ? y  =  0++0 ? x  =  x+x ? y  =  x + x++0 ? x  =  x+x ? y  =  y + y++0 ? x  =  x+x ? y  =  x * x++0 ? x  =  x+x ? y  =  x * y++0 ? x  =  x+x ? y  =  y * y++0 ? x  =  x+x ? y  =  dec (dec x)++0 ? x  =  x+x ? y  =  dec (dec y)++0 ? x  =  0+x ? y  =  x + y++0 ? x  =  0+x ? y  =  y + y++0 ? x  =  0+x ? y  =  y * y++0 ? x  =  0+x ? y  =  dec (dec x)++0 ? x  =  0+x ? y  =  dec (dec y)++0 ? x  =  dec x+x ? y  =  dec x++0 ? x  =  x + x+x ? y  =  x++0 ? x  =  x + x+x ? y  =  y++0 ? x  =  x + x+x ? y  =  0++0 ? x  =  x * x+x ? y  =  x++0 ? x  =  x * x+x ? y  =  y++0 ? x  =  x * x+x ? y  =  0++0 ? x  =  dec (dec x)+x ? y  =  x++0 ? x  =  dec (dec x)+x ? y  =  y++0 ? x  =  dec (dec x)+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  x++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  0++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  0++0 ? x  =  dec x+x ? 0  =  0+x ? y  =  x++x ? 0  =  x+x ? y  =  x ? dec y++x ? 0  =  x+x ? y  =  y ? dec x++x ? 0  =  x+x ? y  =  y ? dec y++x ? 0  =  x+x ? y  =  0 ? dec y++x ? 0  =  x+x ? y  =  dec x ? x++x ? 0  =  x+x ? y  =  dec x ? y++x ? 0  =  x+x ? y  =  dec y ? x++0 ? x  =  x+x ? y  =  x ? dec y++0 ? x  =  x+x ? y  =  y ? dec x++0 ? x  =  x+x ? y  =  y ? dec y++0 ? x  =  x+x ? y  =  dec x ? x++0 ? x  =  x+x ? y  =  dec x ? y++0 ? x  =  x+x ? y  =  dec x ? 0++0 ? x  =  x+x ? y  =  dec y ? x++x ? y  =  dec (dec (x * x))++x ? y  =  dec (dec (x * y))++x ? y  =  dec (dec (y * y))++x ? y  =  dec (dec (dec (dec x)))++x ? y  =  dec (dec (dec (dec y)))++x ? y  =  dec (x * dec x)++x ? y  =  dec (x * dec y)++x ? y  =  dec (y * dec x)++x ? y  =  dec (y * dec y)++x ? y  =  x + (x + x)++x ? y  =  x + (x + y)++x ? y  =  x + (y + y)++x ? y  =  x + x * x++x ? y  =  x + x * y++x ? y  =  x + y * y++x ? y  =  x + dec (dec x)++x ? y  =  x + dec (dec y)++x ? y  =  y + (x + x)++x ? y  =  y + (x + y)++x ? y  =  y + (y + y)++x ? y  =  y + x * x++x ? y  =  y + x * y++x ? y  =  y + y * y++x ? y  =  y + dec (dec x)++x ? y  =  y + dec (dec y)++x ? y  =  x * (x + x)++x ? y  =  x * (x + y)++x ? y  =  x * (y + y)++x ? y  =  x * (x * x)++x ? y  =  x * (x * y)++x ? y  =  x * (y * y)++x ? y  =  x * dec (dec x)++x ? y  =  x * dec (dec y)++x ? y  =  y * (x + x)++x ? y  =  y * (x + y)++x ? y  =  y * (y + y)++x ? y  =  y * (x * x)++x ? y  =  y * (x * y)++x ? y  =  y * (y * y)++x ? y  =  y * dec (dec x)++x ? y  =  y * dec (dec y)++x ? y  =  dec x + dec x++x ? y  =  dec x + dec y++x ? y  =  dec y + dec y++x ? y  =  dec x * dec x++x ? y  =  dec x * dec y++x ? y  =  dec y * dec y++x ? 0  =  x+x ? y  =  dec (x * x)++x ? 0  =  x+x ? y  =  dec (x * y)++x ? 0  =  x+x ? y  =  dec (y * y)++x ? 0  =  x+x ? y  =  dec (dec (dec x))++x ? 0  =  x+x ? y  =  dec (dec (dec y))++x ? 0  =  x+x ? y  =  x + dec x++x ? 0  =  x+x ? y  =  x + dec y++x ? 0  =  x+x ? y  =  y + dec x++x ? 0  =  x+x ? y  =  y + dec y++x ? 0  =  x+x ? y  =  x * dec x++x ? 0  =  x+x ? y  =  x * dec y++x ? 0  =  x+x ? y  =  y * dec x++x ? 0  =  x+x ? y  =  y * dec y++x ? 0  =  0+x ? y  =  dec (x * x)++x ? 0  =  0+x ? y  =  dec (x * y)++x ? 0  =  0+x ? y  =  dec (y * y)++x ? 0  =  0+x ? y  =  dec (dec (dec x))++x ? 0  =  0+x ? y  =  dec (dec (dec y))++x ? 0  =  0+x ? y  =  x + dec x++x ? 0  =  0+x ? y  =  x + dec y++x ? 0  =  0+x ? y  =  y + dec x++x ? 0  =  0+x ? y  =  y + dec y++x ? 0  =  0+x ? y  =  x * dec x++x ? 0  =  0+x ? y  =  x * dec y++x ? 0  =  dec x+x ? y  =  x + x++x ? 0  =  dec x+x ? y  =  x + y++x ? 0  =  dec x+x ? y  =  y + y++x ? 0  =  dec x+x ? y  =  x * x++x ? 0  =  dec x+x ? y  =  x * y++x ? 0  =  dec x+x ? y  =  y * y++x ? 0  =  dec x+x ? y  =  dec (dec x)++x ? 0  =  dec x+x ? y  =  dec (dec y)++x ? 0  =  x + x+x ? y  =  dec x++x ? 0  =  x + x+x ? y  =  dec y++x ? 0  =  x * x+x ? y  =  dec x++x ? 0  =  x * x+x ? y  =  dec y++x ? 0  =  dec (dec x)+x ? y  =  dec x++x ? 0  =  dec (dec x)+x ? y  =  dec y++x ? 0  =  dec (x * x)+x ? y  =  x++x ? 0  =  dec (x * x)+x ? y  =  y++x ? 0  =  dec (x * x)+x ? y  =  0++x ? 0  =  dec (dec (dec x))+x ? y  =  x++x ? 0  =  dec (dec (dec x))+x ? y  =  y++x ? 0  =  dec (dec (dec x))+x ? y  =  0++x ? 0  =  x + dec x+x ? y  =  x++x ? 0  =  x + dec x+x ? y  =  y++x ? 0  =  x + dec x+x ? y  =  0++x ? 0  =  x * dec x+x ? y  =  x++x ? 0  =  x * dec x+x ? y  =  y++x ? 0  =  x * dec x+x ? y  =  0++0 ? x  =  x+x ? y  =  dec (x * x)++0 ? x  =  x+x ? y  =  dec (x * y)++0 ? x  =  x+x ? y  =  dec (y * y)++0 ? x  =  x+x ? y  =  dec (dec (dec x))++0 ? x  =  x+x ? y  =  dec (dec (dec y))++0 ? x  =  x+x ? y  =  x + dec x++0 ? x  =  x+x ? y  =  x + dec y++0 ? x  =  x+x ? y  =  y + dec x++0 ? x  =  x+x ? y  =  y + dec y++0 ? x  =  x+x ? y  =  x * dec x++0 ? x  =  x+x ? y  =  x * dec y++0 ? x  =  x+x ? y  =  y * dec x++0 ? x  =  x+x ? y  =  y * dec y++0 ? x  =  0+x ? y  =  dec (x * x)++0 ? x  =  0+x ? y  =  dec (x * y)++0 ? x  =  0+x ? y  =  dec (y * y)++0 ? x  =  0+x ? y  =  dec (dec (dec x))++0 ? x  =  0+x ? y  =  dec (dec (dec y))++0 ? x  =  0+x ? y  =  x + dec x++0 ? x  =  0+x ? y  =  x + dec y++0 ? x  =  0+x ? y  =  y + dec x++0 ? x  =  0+x ? y  =  y + dec y++0 ? x  =  0+x ? y  =  y * dec x++0 ? x  =  0+x ? y  =  y * dec y++0 ? x  =  dec x+x ? y  =  x + x++0 ? x  =  dec x+x ? y  =  x + y++0 ? x  =  dec x+x ? y  =  y + y++0 ? x  =  dec x+x ? y  =  x * x++0 ? x  =  dec x+x ? y  =  x * y++0 ? x  =  dec x+x ? y  =  y * y++0 ? x  =  dec x+x ? y  =  dec (dec x)++0 ? x  =  dec x+x ? y  =  dec (dec y)++0 ? x  =  x + x+x ? y  =  dec x++0 ? x  =  x + x+x ? y  =  dec y++0 ? x  =  x * x+x ? y  =  dec x++0 ? x  =  x * x+x ? y  =  dec y++0 ? x  =  dec (dec x)+x ? y  =  dec x++0 ? x  =  dec (dec x)+x ? y  =  dec y++0 ? x  =  dec (x * x)+x ? y  =  x++0 ? x  =  dec (x * x)+x ? y  =  y++0 ? x  =  dec (x * x)+x ? y  =  0++0 ? x  =  dec (dec (dec x))+x ? y  =  x++0 ? x  =  dec (dec (dec x))+x ? y  =  y++0 ? x  =  dec (dec (dec x))+x ? y  =  0++0 ? x  =  x + dec x+x ? y  =  x++0 ? x  =  x + dec x+x ? y  =  y++0 ? x  =  x + dec x+x ? y  =  0++0 ? x  =  x * dec x+x ? y  =  x++0 ? x  =  x * dec x+x ? y  =  y++0 ? x  =  x * dec x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  x + x++0 ? x  =  x+x ? 0  =  x+x ? y  =  y + y++0 ? x  =  x+x ? 0  =  x+x ? y  =  x * x++0 ? x  =  x+x ? 0  =  x+x ? y  =  x * y++0 ? x  =  x+x ? 0  =  x+x ? y  =  y * y++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec (dec x)++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec (dec y)++0 ? x  =  x+x ? 0  =  0+x ? y  =  x + x++0 ? x  =  x+x ? 0  =  0+x ? y  =  x * x++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec (dec x)++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec (dec y)++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  x + x+x ? y  =  x++0 ? x  =  x+x ? 0  =  x + x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x * x+x ? y  =  x++0 ? x  =  x+x ? 0  =  x * x+x ? y  =  0++0 ? x  =  x+x ? 0  =  dec (dec x)+x ? y  =  x++0 ? x  =  x+x ? 0  =  dec (dec x)+x ? y  =  0++0 ? x  =  0+x ? 0  =  x+x ? y  =  y + y++0 ? x  =  0+x ? 0  =  x+x ? y  =  y * y++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec (dec x)++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec (dec y)++0 ? x  =  0+x ? 0  =  0+x ? y  =  x + y++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec (dec x)++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec (dec y)++0 ? x  =  0+x ? 0  =  dec x+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  x + x+x ? y  =  y++0 ? x  =  0+x ? 0  =  x * x+x ? y  =  y++0 ? x  =  0+x ? 0  =  dec (dec x)+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  dec x+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  x++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  0++0 ? x  =  x + x+x ? 0  =  x+x ? y  =  y++0 ? x  =  x + x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x + x+x ? 0  =  0+x ? y  =  x++0 ? x  =  x * x+x ? 0  =  x+x ? y  =  y++0 ? x  =  x * x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x * x+x ? 0  =  0+x ? y  =  x++0 ? x  =  dec (dec x)+x ? 0  =  x+x ? y  =  y++0 ? x  =  dec (dec x)+x ? 0  =  x+x ? y  =  0++0 ? x  =  dec (dec x)+x ? 0  =  0+x ? y  =  x++0 ? 0  =  0+0 ? x  =  dec x+x ? y  =  dec x   Candidates for: goo :: [Int] -> [Int]

@@ -31,11 +31,11 @@   putStrLn $ "  " ++ show numErroneous ++ "/" ++ show numCandidates ++ " erroneous candidates"   putStrLn "" --printThy thy-  putStrLn $ unlines . map showDefnWithError $ erroneous+  putStrLn $ unlines . map showDefnWithErrors $ erroneous   where   numCandidates  =  length candidates   numErroneous   =  length erroneous-  erroneous      =  [(c, e) | c <- candidates, Just e <- [findError c]]+  erroneous      =  [(c, e, es) | c <- candidates, (e:es) <- [listErrors c]]   candidates     =  concat css   css            =  take n                  .  discardT isRedundantByIntroduction -- additional pruning rule@@ -45,9 +45,9 @@   nREs           =  length (equations thy) + nRules   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark   maxEvalRecursions  =  60-  findError      =  findDefnError maxTests maxEvalRecursions nm f-  showDefnWithError (d,e)  =  showDefn d-                           ++ "-- " ++ showExpr e ++ "  =  bottom\n"+  listErrors     =  listDefnErrors maxTests maxEvalRecursions nm f+  showDefnWithErrors (d,e,es)  =  showDefn d+                               ++ "-- " ++ showExpr e ++ "  =  bottom  -- and " ++ show (length es) ++ " other errors\n"   main :: IO ()@@ -55,24 +55,25 @@    -- This N value limits the maximum size of candidates,   -- increase it to print erroneous candidates of bigger size.-  let n = 7+  let n = 6 -  printErroneousCandidates n "foo" (undefined :: Int -> Int)+  printErroneousCandidates (n+1) "foo" (undefined :: Int -> Int)     [ pr (0 :: Int)     , pr (1 :: Int)+    , pr (2 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "-" ((-) :: Int -> Int -> Int)     ]    printErroneousCandidates n "?" (undefined :: Int -> Int -> Int)     [ pr (0 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "dec" (subtract 1 :: Int -> Int)     ] -  printErroneousCandidates n "goo" (undefined :: [Int] -> [Int])+  printErroneousCandidates (n+1) "goo" (undefined :: [Int] -> [Int])     [ pr ([] :: [Int])     , prim ":" ((:) :: Int -> [Int] -> [Int])     , prim "++" ((++) :: [Int] -> [Int] -> [Int])

@@ -1,620 +1,237 @@ Erroneous candidates for: foo :: Int -> Int-  pruning with 15/35 rules-  [3,3,8,9,21,27,98] candidates-  0/169 erroneous candidates+  pruning with 41/82 rules+  [4,8,16,42,70,162,493] candidates+  30/795 erroneous candidates +foo 0  =  0+foo x  =  x + foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -Erroneous candidates for: ? :: Int -> Int -> Int-  pruning with 10/23 rules-  [3,8,22,50,116,302,765] candidates-  147/1266 erroneous candidates+foo 0  =  0+foo x  =  foo (x - 2) + 1+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec x ? y--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  foo (x - 2) + 2+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  x ? dec y--- 1 ? 0  =  bottom+foo 0  =  0+foo x  =  x * foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  x ? dec (dec y)--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  x - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  y ? dec (dec x)--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  foo (x - 2) - x+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  y ? dec (dec y)--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  foo (x - 2) - 1+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  0 ? dec (dec y)--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  foo (x - 2) - 2+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec x ? dec x--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  0 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec y ? dec x--- 0 ? 1  =  bottom+foo 0  =  0+foo x  =  1 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec (dec x) ? x--- 1 ? 1  =  bottom+foo 0  =  1+foo x  =  x + foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec (dec x) ? y--- 0 ? 1  =  bottom+foo 0  =  1+foo x  =  foo (x - 2) + 1+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec (dec y) ? x--- 1 ? 1  =  bottom+foo 0  =  1+foo x  =  foo (x - 2) + 2+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  x ? dec (dec y)--- 1 ? 0  =  bottom+foo 0  =  1+foo x  =  x * foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  y ? dec (dec x)--- 1 ? 1  =  bottom+foo 0  =  1+foo x  =  x - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  y ? dec (dec y)--- 1 ? 1  =  bottom+foo 0  =  1+foo x  =  foo (x - 2) - x+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec y ? dec x--- 1 ? 0  =  bottom+foo 0  =  1+foo x  =  foo (x - 2) - 1+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec y ? dec y--- 1 ? 0  =  bottom+foo 0  =  1+foo x  =  foo (x - 2) - 2+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec (dec x) ? x--- 1 ? 0  =  bottom+foo 0  =  1+foo x  =  0 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec (dec x) ? y--- 1 ? 0  =  bottom+foo 0  =  1+foo x  =  1 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec (dec x) ? 0--- 1 ? 0  =  bottom+foo 0  =  2+foo x  =  x + foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec (dec y) ? x--- 1 ? 0  =  bottom+foo 0  =  2+foo x  =  foo (x - 2) + 1+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  dec (dec x ? y)--- 0 ? 1  =  bottom+foo 0  =  2+foo x  =  foo (x - 2) + 2+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  0-x ? y  =  dec (dec x ? y)--- 0 ? 1  =  bottom+foo 0  =  2+foo x  =  x * foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  dec x-x ? y  =  dec x ? y--- 0 ? 1  =  bottom+foo 0  =  2+foo x  =  x - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  x-x ? y  =  dec (x ? dec y)--- 1 ? 0  =  bottom+foo 0  =  2+foo x  =  foo (x - 2) - x+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  0-x ? y  =  dec (x ? dec y)--- 1 ? 0  =  bottom+foo 0  =  2+foo x  =  foo (x - 2) - 1+-- foo 1  =  bottom  -- and 14 other errors -0 ? x  =  dec x-x ? y  =  x ? dec y--- 1 ? 0  =  bottom+foo 0  =  2+foo x  =  foo (x - 2) - 2+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  x ? dec (dec (dec y))--- 0 ? 1  =  bottom+foo 0  =  2+foo x  =  0 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  y ? dec (dec (dec x))--- 0 ? 1  =  bottom+foo 0  =  2+foo x  =  1 - foo (x - 2)+-- foo 1  =  bottom  -- and 14 other errors -x ? 0  =  x-x ? y  =  y ? dec (dec (dec y))--- 0 ? 1  =  bottom -x ? 0  =  x-x ? y  =  0 ? dec (dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec x ? (x + y)--- 1 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec x ? (y + y)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec x ? dec (dec x)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec x ? dec (dec y)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec y ? dec (dec x)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec y ? dec (dec y)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec x) ? dec x--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec y) ? dec x--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec (dec x)) ? x--- 1 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec (dec x)) ? y--- 0 ? 1  =  bottom+Erroneous candidates for: ? :: Int -> Int -> Int+  pruning with 13/34 rules+  [3,8,25,71,205,632] candidates+  26/944 erroneous candidates  x ? 0  =  x-x ? y  =  dec (dec (dec y)) ? x--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  x ? dec (dec (dec y))--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  y ? dec (dec (dec x))--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  y ? dec (dec (dec y))--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  dec y ? dec (dec x)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec y ? dec (dec y)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  (x + x) ? dec y--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  (x + y) ? dec y--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  dec (dec x) ? dec x--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec x) ? dec y--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec y) ? dec x--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec y) ? dec y--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x)) ? x--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x)) ? y--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x)) ? 0--- 1 ? 0  =  bottom+x ? y  =  dec x ? y+-- 0 ? 1  =  bottom  -- and 16 other errors  0 ? x  =  x-x ? y  =  dec (dec (dec y)) ? x--- 1 ? 0  =  bottom--x ? 0  =  x-x ? y  =  dec (x ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (y ? dec (dec x))--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (y ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (0 ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec x ? dec x)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec y ? dec x)--- 0 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec (dec x) ? x)--- 1 ? 1  =  bottom--x ? 0  =  x-x ? y  =  dec (dec (dec x) ? y)--- 0 ? 1  =  bottom+x ? y  =  x ? dec y+-- 1 ? 0  =  bottom  -- and 16 other errors  x ? 0  =  x-x ? y  =  dec (dec (dec y) ? x)--- 1 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (x ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (y ? dec (dec x))--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (y ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (0 ? dec (dec y))--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (dec x ? dec x)--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (dec y ? dec x)--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (dec (dec x) ? x)--- 1 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (dec (dec x) ? y)--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec (dec (dec y) ? x)--- 1 ? 1  =  bottom--x ? 0  =  dec x x ? y  =  x ? dec (dec y)--- 0 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 9 other errors -x ? 0  =  dec x+x ? 0  =  x x ? y  =  y ? dec (dec x)--- 0 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 6 other errors -x ? 0  =  dec x+x ? 0  =  x x ? y  =  y ? dec (dec y)--- 0 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 9 other errors -x ? 0  =  dec x+x ? 0  =  x x ? y  =  0 ? dec (dec y)--- 0 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 9 other errors -x ? 0  =  dec x+x ? 0  =  x x ? y  =  dec x ? dec x--- 0 ? 1  =  bottom--x ? 0  =  dec x-x ? y  =  dec y ? dec x--- 0 ? 1  =  bottom--x ? 0  =  dec x-x ? y  =  dec (dec x) ? x--- 1 ? 1  =  bottom--x ? 0  =  dec x-x ? y  =  dec (dec x) ? y--- 0 ? 1  =  bottom--x ? 0  =  dec x-x ? y  =  dec (dec y) ? x--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  dec (x ? dec (dec y))--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (y ? dec (dec x))--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  dec (y ? dec (dec y))--- 1 ? 1  =  bottom--0 ? x  =  x-x ? y  =  dec (dec y ? dec x)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec y ? dec y)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x) ? x)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x) ? y)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec x) ? 0)--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  dec (dec (dec y) ? x)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (x ? dec (dec y))--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (y ? dec (dec x))--- 1 ? 1  =  bottom--0 ? x  =  0-x ? y  =  dec (y ? dec (dec y))--- 1 ? 1  =  bottom--0 ? x  =  0-x ? y  =  dec (dec y ? dec x)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (dec y ? dec y)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (dec (dec x) ? x)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (dec (dec x) ? y)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (dec (dec x) ? 0)--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  dec (dec (dec y) ? x)--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  x ? dec (dec y)--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  y ? dec (dec x)--- 1 ? 1  =  bottom--0 ? x  =  dec x-x ? y  =  y ? dec (dec y)--- 1 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 4 other errors -0 ? x  =  dec x+x ? 0  =  x x ? y  =  dec y ? dec x--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  dec y ? dec y--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  dec (dec x) ? x--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  dec (dec x) ? y--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  dec (dec x) ? 0--- 1 ? 0  =  bottom--0 ? x  =  dec x-x ? y  =  dec (dec y) ? x--- 1 ? 0  =  bottom+-- 0 ? 1  =  bottom  -- and 5 other errors -0 ? x  =  x x ? 0  =  x-x ? y  =  x ? dec (dec y)--- 1 ? 1  =  bottom--0 ? x  =  x-x ? 0  =  x-x ? y  =  y ? dec (dec x)--- 1 ? 1  =  bottom--0 ? x  =  x-x ? 0  =  x-x ? y  =  y ? dec (dec y)--- 1 ? 1  =  bottom--0 ? x  =  x-x ? 0  =  x x ? y  =  dec (dec x) ? x--- 1 ? 1  =  bottom+-- 1 ? 1  =  bottom  -- and 6 other errors -0 ? x  =  x x ? 0  =  x x ? y  =  dec (dec x) ? y--- 1 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 16 other errors -0 ? x  =  x x ? 0  =  x x ? y  =  dec (dec y) ? x--- 1 ? 1  =  bottom+-- 1 ? 1  =  bottom  -- and 3 other errors  0 ? x  =  x-x ? 0  =  0 x ? y  =  x ? dec (dec y)--- 1 ? 1  =  bottom+-- 1 ? 0  =  bottom  -- and 16 other errors  0 ? x  =  x-x ? 0  =  0 x ? y  =  y ? dec (dec x)--- 1 ? 1  =  bottom+-- 1 ? 1  =  bottom  -- and 3 other errors  0 ? x  =  x-x ? 0  =  0 x ? y  =  y ? dec (dec y)--- 1 ? 1  =  bottom+-- 1 ? 1  =  bottom  -- and 6 other errors  0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec x) ? x--- 1 ? 1  =  bottom+x ? y  =  dec y ? dec x+-- 1 ? 0  =  bottom  -- and 5 other errors  0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec x) ? y--- 1 ? 1  =  bottom+x ? y  =  dec y ? dec y+-- 1 ? 0  =  bottom  -- and 4 other errors  0 ? x  =  x-x ? 0  =  0-x ? y  =  dec (dec y) ? x--- 1 ? 1  =  bottom--0 ? x  =  0-x ? 0  =  x-x ? y  =  x ? dec (dec y)--- 1 ? 1  =  bottom--0 ? x  =  0-x ? 0  =  x-x ? y  =  y ? dec (dec x)--- 1 ? 1  =  bottom--0 ? x  =  0-x ? 0  =  x-x ? y  =  y ? dec (dec y)--- 1 ? 1  =  bottom--0 ? x  =  0-x ? 0  =  x x ? y  =  dec (dec x) ? x--- 1 ? 1  =  bottom+-- 1 ? 0  =  bottom  -- and 9 other errors -0 ? x  =  0-x ? 0  =  x+0 ? x  =  x x ? y  =  dec (dec x) ? y--- 1 ? 1  =  bottom--0 ? x  =  0-x ? 0  =  x-x ? y  =  dec (dec y) ? x--- 1 ? 1  =  bottom+-- 1 ? 0  =  bottom  -- and 9 other errors -x ? 0  =  x-x ? y  =  x + dec x ? y--- 0 ? 1  =  bottom+0 ? x  =  x+x ? y  =  dec (dec x) ? 0+-- 1 ? 0  =  bottom  -- and 9 other errors -x ? 0  =  x-x ? y  =  dec x ? y + y--- 0 ? 1  =  bottom+0 ? x  =  x+x ? y  =  dec (dec y) ? x+-- 1 ? 0  =  bottom  -- and 6 other errors  x ? 0  =  x-x ? y  =  dec (dec (dec x ? y))--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  x + dec x ? y--- 0 ? 1  =  bottom--x ? 0  =  0-x ? y  =  dec x ? y + y--- 0 ? 1  =  bottom+x ? y  =  dec (dec x ? y)+-- 0 ? 1  =  bottom  -- and 16 other errors  x ? 0  =  0-x ? y  =  dec (dec (dec x ? y))--- 0 ? 1  =  bottom--x ? 0  =  dec x x ? y  =  dec (dec x ? y)--- 0 ? 1  =  bottom--x ? 0  =  x + x-x ? y  =  dec x ? y--- 0 ? 1  =  bottom+-- 0 ? 1  =  bottom  -- and 16 other errors -x ? 0  =  dec (dec x)+x ? 0  =  dec x x ? y  =  dec x ? y--- 0 ? 1  =  bottom--0 ? x  =  x-x ? y  =  x + x ? dec y--- 1 ? 0  =  bottom--0 ? x  =  x-x ? y  =  x ? dec y + y--- 1 ? 0  =  bottom+-- 0 ? 1  =  bottom  -- and 16 other errors  0 ? x  =  x-x ? y  =  dec (dec (x ? dec y))--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  x + x ? dec y--- 1 ? 0  =  bottom--0 ? x  =  0-x ? y  =  x ? dec y + y--- 1 ? 0  =  bottom+x ? y  =  dec (x ? dec y)+-- 1 ? 0  =  bottom  -- and 16 other errors  0 ? x  =  0-x ? y  =  dec (dec (x ? dec y))--- 1 ? 0  =  bottom--0 ? x  =  dec x x ? y  =  dec (x ? dec y)--- 1 ? 0  =  bottom--0 ? x  =  x + x-x ? y  =  x ? dec y--- 1 ? 0  =  bottom--0 ? x  =  dec (dec x)-x ? y  =  x ? dec y--- 1 ? 0  =  bottom+-- 1 ? 0  =  bottom  -- and 16 other errors -0 ? 0  =  0 0 ? x  =  dec x x ? y  =  x ? dec y--- 1 ? 0  =  bottom+-- 1 ? 0  =  bottom  -- and 16 other errors   Erroneous candidates for: goo :: [Int] -> [Int]@@ -625,19 +242,19 @@  Erroneous candidates for: ?? :: [Int] -> [Int] -> [Int]   pruning with 4/4 rules-  [3,8,15,43,122,264,830] candidates-  0/1285 erroneous candidates+  [3,8,15,43,122,264] candidates+  0/455 erroneous candidates   Erroneous candidates for: ton :: Bool -> Bool   pruning with 39/49 rules-  [3,2,0,0,0,0,0] candidates+  [3,2,0,0,0,0] candidates   0/5 erroneous candidates   Erroneous candidates for: &| :: Bool -> Bool -> Bool   pruning with 39/49 rules-  [4,12,20,6,2,16,18] candidates-  0/78 erroneous candidates+  [4,12,20,6,2,16] candidates+  0/60 erroneous candidates  

@@ -4,9 +4,9 @@ -- looking through 1 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 1 candidates of size 3--- looking through 1 candidates of size 4+-- looking through 2 candidates of size 4 -- tested 4 candidates-gps1 x y  =  y + fromIntegral x+gps1 x y  =  fromIntegral x + y  gps2 :: Int -> Maybe [Char] -- testing 6 combinations of argument values@@ -334,7 +334,7 @@ -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 1 candidates of size 3--- looking through 9 candidates of size 4+-- looking through 10 candidates of size 4 -- tested 13 candidates gps18 xs ys  =  zipWith (+) xs ys 

@@ -43,11 +43,11 @@ -- pruning with 2/6 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2--- looking through 17 candidates of size 3--- looking through 62 candidates of size 4--- looking through 266 candidates of size 5--- looking through 1154 candidates of size 6--- tested 1503 candidates+-- looking through 18 candidates of size 3+-- looking through 66 candidates of size 4+-- looking through 316 candidates of size 5+-- looking through 1376 candidates of size 6+-- tested 1780 candidates cannot conjure  gps3 :: [Char] -> Int@@ -58,7 +58,7 @@ cannot conjure  gps4 :: [Char] -> [Char]--- pruning with 13/20 rules+-- pruning with 13/21 rules -- looking through 2 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 8 candidates of size 3@@ -259,10 +259,10 @@ -- looking through 2 candidates of size 1 -- looking through 8 candidates of size 2 -- looking through 32 candidates of size 3--- looking through 70 candidates of size 4--- looking through 396 candidates of size 5--- looking through 1016 candidates of size 6--- tested 1524 candidates+-- looking through 74 candidates of size 4+-- looking through 433 candidates of size 5+-- looking through 1218 candidates of size 6+-- tested 1767 candidates cannot conjure  gps19_snowday :: Int -> Double -> Double -> Double -> Double@@ -270,11 +270,11 @@ -- pruning with 6/19 rules -- looking through 3 candidates of size 1 -- looking through 6 candidates of size 2--- looking through 24 candidates of size 3--- looking through 120 candidates of size 4--- looking through 318 candidates of size 5--- looking through 1944 candidates of size 6--- tested 2415 candidates+-- looking through 27 candidates of size 3+-- looking through 138 candidates of size 4+-- looking through 435 candidates of size 5+-- looking through 2715 candidates of size 6+-- tested 3324 candidates cannot conjure  gps20 :: [Char] -> Bool@@ -379,9 +379,9 @@ -- looking through 2 candidates of size 1 -- looking through 9 candidates of size 2 -- looking through 49 candidates of size 3--- looking through 195 candidates of size 4--- looking through 1035 candidates of size 5--- looking through 4596 candidates of size 6--- tested 5886 candidates+-- looking through 200 candidates of size 4+-- looking through 1104 candidates of size 5+-- looking through 5170 candidates of size 6+-- tested 6534 candidates cannot conjure 

@@ -1,7 +1,7 @@ running with 13 primitives factorial :: Int -> Int -- testing 6 combinations of argument values--- pruning with 67/100 rules+-- pruning with 67/101 rules -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 6 candidates of size 3

@@ -58,28 +58,29 @@    -- This N value limits the maximum size of candidates,   -- increase it to print redundant candidates of bigger size.-  let n = 6-  -- With n = 6, this should run in a few seconds.+  let n = 5+  -- With n = 5, this should run in a few seconds.+  -- With n = 6, this should run in a few more seconds.   -- With n = 7 and -O2 optimization,   -- this should take a few minutes to run and generate a ~300K text file.   -- We can also customize the n per-function below: -  printRedundantCandidates n "foo" (undefined :: Int -> Int)+  printRedundantCandidates (n+1) "foo" (undefined :: Int -> Int)     [ pr (0 :: Int)     , pr (1 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "-" ((-) :: Int -> Int -> Int)     ]    printRedundantCandidates n "?" (undefined :: Int -> Int -> Int)     [ pr (0 :: Int)     , prim "+" ((+) :: Int -> Int -> Int)-    , prim "*" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     , prim "dec" (subtract 1 :: Int -> Int)     ] -  printRedundantCandidates n "goo" (undefined :: [Int] -> [Int])+  printRedundantCandidates (n+1) "goo" (undefined :: [Int] -> [Int])     [ pr ([] :: [Int])     , prim ":" ((:) :: Int -> [Int] -> [Int])     , prim "++" ((++) :: [Int] -> [Int] -> [Int])@@ -91,7 +92,7 @@     , prim "++" ((++) :: [Int] -> [Int] -> [Int])     ] -  printRedundantCandidates n "ton" (undefined :: Bool -> Bool)+  printRedundantCandidates (n+1) "ton" (undefined :: Bool -> Bool)     [ pr False     , pr True     , prim "&&" (&&)

@@ -1,1934 +1,902 @@ Redundant candidates for: foo :: Int -> Int-  pruning with 15/35 rules-  [3,3,8,9,21,27] candidates-  63/71 unique candidates-  8/71 redundant candidates--rules:-x * y == x + y-x * y == y + x-x - x == 0-x + 0 == x-0 + x == x-x - 0 == x-(x + y) + z == x + (y + z)-(x + y) + z == y + (x + z)-x - (y - z) == z + (x - y)-(x - y) - z == x - (y + z)-(x - y) - z == x - (z + y)-(x + y) - z == x + (y - z)-(x + y) - z == y + (x - z)-x + (y - x) == y-(x - y) + y == x-equations:-y + x == x + y-y + (x + z) == x + (y + z)-z + (x + y) == x + (y + z)-z + (y + x) == x + (y + z)-y + (x - z) == x + (y - z)-(x - z) + y == x + (y - z)-(z - y) + x == (x - y) + z-y - (x + y) == 0 - x-y - (y + x) == 0 - x-z - (y + z) == x - (x + y)-z - (y + z) == x - (y + x)-z - (z + y) == x - (x + y)-z - (z + y) == x - (y + x)-x + (0 - y) == x - y-(0 - y) + x == x - y-x - (x + 1) == 0 - 1-x - (1 + x) == 0 - 1-y - (y + 1) == x - (x + 1)-y - (y + 1) == x - (1 + x)-y - (1 + y) == x - (1 + x)--class of 3 equivalent candidates:--    foo x  =  0 - x--    foo x  =  x - (x + x)--    foo x  =  1 - (x + 1)---class of 2 equivalent candidates:--    foo x  =  1 - x--    foo x  =  1 + (0 - x)---class of 2 equivalent candidates:--    foo 0  =  0-    foo x  =  1 - x--    foo 0  =  0-    foo x  =  1 + (0 - x)---class of 3 equivalent candidates:--    foo 0  =  1-    foo x  =  0 - x--    foo 0  =  1-    foo x  =  x - (x + x)--    foo 0  =  1-    foo x  =  1 - (x + 1)---class of 2 equivalent candidates:--    foo x  =  x + (x + 1)--    foo x  =  1 + (x + x)---class of 2 equivalent candidates:--    foo 0  =  0-    foo x  =  x + (x + 1)--    foo 0  =  0-    foo x  =  1 + (x + x)----Redundant candidates for: ? :: Int -> Int -> Int-  pruning with 10/23 rules-  [3,8,22,50,116,302] candidates-  410/501 unique candidates-  91/501 redundant candidates--rules:-x * y == x + y-x * y == y + x-x + 0 == x-0 + x == x-dec (x + y) == x + dec y-dec (x + y) == y + dec x-dec (x + y) == dec x + y-dec (x + y) == dec y + x-(x + y) + z == x + (y + z)-(x + y) + z == y + (x + z)-equations:-y + x == x + y-y + dec x == x + dec y-dec x + y == x + dec y-dec y + x == dec x + y-x + dec 0 == dec x-dec 0 + x == dec x-y + (x + z) == x + (y + z)-z + (x + y) == x + (y + z)-z + (y + x) == x + (y + z)-y + dec (dec x) == x + dec (dec y)-dec (dec x) + y == x + dec (dec y)-x + dec (dec 0) == dec (dec x)-dec (dec 0) + x == dec (dec x)--class of 3 equivalent candidates:--    x ? y  =  x--    x ? 0  =  x-    x ? y  =  x ? dec y--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  x ? dec y---class of 3 equivalent candidates:--    x ? y  =  y--    0 ? x  =  x-    x ? y  =  dec x ? y--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  dec x ? y---class of 2 equivalent candidates:--    x ? y  =  dec x--    x ? 0  =  dec x-    x ? y  =  x ? dec y---class of 2 equivalent candidates:--    x ? y  =  dec y--    0 ? x  =  dec x-    x ? y  =  dec x ? y---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  y--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  dec x ? y---class of 6 equivalent candidates:--    x ? 0  =  x-    x ? y  =  0--    x ? 0  =  x-    x ? y  =  0 ? dec y--    x ? 0  =  x-    x ? y  =  dec y ? dec y--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  dec x ? x--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  dec x ? y--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  dec y ? x---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  x ? dec y---class of 6 equivalent candidates:--    0 ? x  =  x-    x ? y  =  0--    0 ? x  =  x-    x ? y  =  dec x ? 0--    0 ? x  =  x-    x ? y  =  dec x ? dec x--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  x ? dec y--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  y ? dec x--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  y ? dec y---class of 2 equivalent candidates:--    x ? 0  =  dec x-    x ? y  =  0--    x ? 0  =  dec x-    x ? y  =  y ? dec y---class of 2 equivalent candidates:--    0 ? x  =  dec x-    x ? y  =  0--    0 ? x  =  dec x-    x ? y  =  dec x ? x---class of 4 equivalent candidates:--    x ? y  =  x + dec y--    x ? y  =  y + dec x--    x ? 0  =  dec x-    x ? y  =  x + dec y--    0 ? x  =  dec x-    x ? y  =  y + dec x---class of 3 equivalent candidates:--    x ? 0  =  x-    x ? y  =  dec x ? y--    x ? 0  =  x-    x ? y  =  dec (dec x) ? y--    x ? 0  =  x-    x ? y  =  dec (dec x ? y)---class of 3 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x ? dec y--    0 ? x  =  x-    x ? y  =  x ? dec (dec y)--    0 ? x  =  x-    x ? y  =  dec (x ? dec y)---class of 2 equivalent candidates:--    x ? y  =  x + (x + y)--    x ? y  =  y + (x + x)---class of 2 equivalent candidates:--    x ? y  =  x + (y + y)--    x ? y  =  y + (x + y)---class of 2 equivalent candidates:--    x ? y  =  x + dec (dec x)--    x ? y  =  dec x + dec x---class of 3 equivalent candidates:--    x ? y  =  x + dec (dec y)--    x ? y  =  y + dec (dec x)--    x ? y  =  dec x + dec y---class of 2 equivalent candidates:--    x ? y  =  y + dec (dec y)--    x ? y  =  dec y + dec y---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  x + dec y--    x ? 0  =  x-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    x ? 0  =  0-    x ? y  =  x + dec y--    x ? 0  =  0-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x + dec y--    0 ? x  =  x-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? y  =  x + dec y--    0 ? x  =  0-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  dec x ? dec y--    x ? 0  =  x-    x ? y  =  dec (x ? dec y)---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  dec x ? dec y--    0 ? x  =  x-    x ? y  =  dec (dec x ? y)---class of 3 equivalent candidates:--    x ? 0  =  0-    x ? y  =  dec (x ? dec y)--    x ? 0  =  0-    x ? y  =  dec (y ? dec y)--    x ? 0  =  0-    x ? y  =  dec (0 ? dec y)---class of 3 equivalent candidates:--    0 ? x  =  0-    x ? y  =  dec (dec x ? x)--    0 ? x  =  0-    x ? y  =  dec (dec x ? y)--    0 ? x  =  0-    x ? y  =  dec (dec x ? 0)---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  y ? dec y--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  dec x ? x---class of 2 equivalent candidates:--    x ? y  =  x + dec (dec (dec x))--    x ? y  =  dec x + dec (dec x)---class of 4 equivalent candidates:--    x ? y  =  x + dec (dec (dec y))--    x ? y  =  y + dec (dec (dec x))--    x ? y  =  dec x + dec (dec y)--    x ? y  =  dec y + dec (dec x)---class of 2 equivalent candidates:--    x ? y  =  x + (x + dec x)--    x ? y  =  dec x + (x + x)---class of 5 equivalent candidates:--    x ? y  =  x + (x + dec y)--    x ? y  =  x + (y + dec x)--    x ? y  =  y + (x + dec x)--    x ? y  =  dec x + (x + y)--    x ? y  =  dec y + (x + x)---class of 5 equivalent candidates:--    x ? y  =  x + (y + dec y)--    x ? y  =  y + (x + dec y)--    x ? y  =  y + (y + dec x)--    x ? y  =  dec x + (y + y)--    x ? y  =  dec y + (x + y)---class of 2 equivalent candidates:--    x ? y  =  y + dec (dec (dec y))--    x ? y  =  dec y + dec (dec y)---class of 2 equivalent candidates:--    x ? y  =  y + (y + dec y)--    x ? y  =  dec y + (y + y)---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  x + (x + y)--    x ? 0  =  x-    x ? y  =  y + (x + x)---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  x + dec (dec x)--    x ? 0  =  x-    x ? y  =  dec x + dec x---class of 3 equivalent candidates:--    x ? 0  =  x-    x ? y  =  x + dec (dec y)--    x ? 0  =  x-    x ? y  =  y + dec (dec x)--    x ? 0  =  x-    x ? y  =  dec x + dec y---class of 2 equivalent candidates:--    x ? 0  =  x-    x ? y  =  y + dec (dec y)--    x ? 0  =  x-    x ? y  =  dec y + dec y---class of 2 equivalent candidates:--    x ? 0  =  0-    x ? y  =  x + (x + y)--    x ? 0  =  0-    x ? y  =  y + (x + x)---class of 2 equivalent candidates:--    x ? 0  =  0-    x ? y  =  x + (y + y)--    x ? 0  =  0-    x ? y  =  y + (x + y)---class of 2 equivalent candidates:--    x ? 0  =  0-    x ? y  =  x + dec (dec x)--    x ? 0  =  0-    x ? y  =  dec x + dec x---class of 3 equivalent candidates:--    x ? 0  =  0-    x ? y  =  x + dec (dec y)--    x ? 0  =  0-    x ? y  =  y + dec (dec x)--    x ? 0  =  0-    x ? y  =  dec x + dec y---class of 2 equivalent candidates:--    x ? 0  =  0-    x ? y  =  y + dec (dec y)--    x ? 0  =  0-    x ? y  =  dec y + dec y---class of 2 equivalent candidates:--    x ? 0  =  x + dec (dec x)-    x ? y  =  x--    x ? 0  =  dec x + dec x-    x ? y  =  x---class of 2 equivalent candidates:--    x ? 0  =  x + dec (dec x)-    x ? y  =  y--    x ? 0  =  dec x + dec x-    x ? y  =  y---class of 2 equivalent candidates:--    x ? 0  =  x + dec (dec x)-    x ? y  =  0--    x ? 0  =  dec x + dec x-    x ? y  =  0---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x + (y + y)--    0 ? x  =  x-    x ? y  =  y + (x + y)---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x + dec (dec x)--    0 ? x  =  x-    x ? y  =  dec x + dec x---class of 3 equivalent candidates:--    0 ? x  =  x-    x ? y  =  x + dec (dec y)--    0 ? x  =  x-    x ? y  =  y + dec (dec x)--    0 ? x  =  x-    x ? y  =  dec x + dec y---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? y  =  y + dec (dec y)--    0 ? x  =  x-    x ? y  =  dec y + dec y---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? y  =  x + (x + y)--    0 ? x  =  0-    x ? y  =  y + (x + x)---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? y  =  x + (y + y)--    0 ? x  =  0-    x ? y  =  y + (x + y)---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? y  =  x + dec (dec x)--    0 ? x  =  0-    x ? y  =  dec x + dec x---class of 3 equivalent candidates:--    0 ? x  =  0-    x ? y  =  x + dec (dec y)--    0 ? x  =  0-    x ? y  =  y + dec (dec x)--    0 ? x  =  0-    x ? y  =  dec x + dec y---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? y  =  y + dec (dec y)--    0 ? x  =  0-    x ? y  =  dec y + dec y---class of 2 equivalent candidates:--    0 ? x  =  x + dec (dec x)-    x ? y  =  x--    0 ? x  =  dec x + dec x-    x ? y  =  x---class of 2 equivalent candidates:--    0 ? x  =  x + dec (dec x)-    x ? y  =  y--    0 ? x  =  dec x + dec x-    x ? y  =  y---class of 2 equivalent candidates:--    0 ? x  =  x + dec (dec x)-    x ? y  =  0--    0 ? x  =  dec x + dec x-    x ? y  =  0---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  x + dec y--    0 ? x  =  x-    x ? 0  =  x-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  x + dec y--    0 ? x  =  x-    x ? 0  =  0-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  x + dec y--    0 ? x  =  0-    x ? 0  =  x-    x ? y  =  y + dec x---class of 2 equivalent candidates:--    0 ? x  =  0-    x ? 0  =  0-    x ? y  =  x + dec y--    0 ? x  =  0-    x ? 0  =  0-    x ? y  =  y + dec x----Redundant candidates for: goo :: [Int] -> [Int]-  pruning with 4/4 rules-  [2,1,1,2,4,7] candidates-  15/17 unique candidates-  2/17 redundant candidates--rules:-xs ++ [] == xs-[] ++ xs == xs-(xs ++ ys) ++ zs == xs ++ (ys ++ zs)-(x:xs) ++ ys == x:(xs ++ ys)--class of 2 equivalent candidates:--    goo xs  =  xs--    goo []  =  []-    goo (x:xs)  =  x:goo xs---class of 2 equivalent candidates:--    goo xs  =  []--    goo []  =  []-    goo (x:xs)  =  goo xs ++ goo xs----Redundant candidates for: ?? :: [Int] -> [Int] -> [Int]-  pruning with 4/4 rules-  [3,8,15,43,122,264] candidates-  325/455 unique candidates-  130/455 redundant candidates--rules:-xs ++ [] == xs-[] ++ xs == xs-(xs ++ ys) ++ zs == xs ++ (ys ++ zs)-(x:xs) ++ ys == x:(xs ++ ys)--class of 9 equivalent candidates:--    xs ?? ys  =  xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ++ [] ?? xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ++ [] ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? xs ++ xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? ys ++ xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  x:xs ?? xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  x:xs ?? ys--    [] ?? xs  =  []-    (x:xs) ?? ys  =  x:xs ?? []---class of 9 equivalent candidates:--    xs ?? ys  =  ys--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  x:xs ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  x:ys ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  x:[] ?? ys--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ++ xs ?? []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ++ ys ?? []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? [] ++ ys--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ?? [] ++ ys---class of 6 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  []--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? ys--    [] ?? xs  =  []-    (x:xs) ?? []  =  x:xs-    (x:xs) ?? (y:ys)  =  []--    xs ?? []  =  xs-    xs ?? (x:ys)  =  (ys ++ ys) ?? ys---class of 6 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs--    [] ?? xs  =  []-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  x:xs--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs ++ [] ?? xs--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs ++ [] ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  [] ?? xs ++ xs--    xs ?? []  =  []-    xs ?? (x:ys)  =  [] ?? ys ++ xs---class of 3 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  xs ?? ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  [] ?? ys---class of 11 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ?? []--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs ?? xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  []--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs ?? []--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys ?? ys--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys ?? []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? (xs ++ xs)---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs--    [] ?? []  =  []-    [] ?? (x:xs)  =  [] ?? xs-    (x:xs) ?? ys  =  xs---class of 7 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? []-    (x:xs) ?? ys  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  [] ?? xs-    (x:xs) ?? ys  =  ys--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ++ xs ?? []--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ++ ys ?? []--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ?? [] ++ ys--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ?? [] ++ ys---class of 2 equivalent candidates:--    xs ?? ys  =  xs ++ xs--    xs ?? []  =  xs ++ xs-    xs ?? (x:ys)  =  xs ?? ys---class of 4 equivalent candidates:--    xs ?? ys  =  xs ++ ys--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:xs ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ++ (x:ys)--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:(xs ++ ys)---class of 4 equivalent candidates:--    xs ?? ys  =  ys ++ xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:xs ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:(ys ++ xs)--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ++ (x:xs)---class of 2 equivalent candidates:--    xs ?? ys  =  ys ++ ys--    [] ?? xs  =  xs ++ xs-    (x:xs) ?? ys  =  xs ?? ys---class of 3 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? ys---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  xs---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  ys---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  [] ?? xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys---class of 5 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? xs--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? []  =  []-    [] ?? (x:xs)  =  [] ?? xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  []---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  xs---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  ys---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? xs-    (x:xs) ?? ys  =  ys---class of 6 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  xs ?? xs--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  xs ?? []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? ys  =  ys ?? []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs ?? xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs ?? []-    (x:xs) ?? (y:ys)  =  []---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? ys---class of 3 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:ys ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:[] ?? ys---class of 4 equivalent candidates:--    xs ?? []  =  xs ++ xs-    xs ?? (x:ys)  =  []--    xs ?? []  =  xs ++ xs-    xs ?? (x:ys)  =  ys ?? ys--    xs ?? []  =  xs ++ xs-    xs ?? (x:ys)  =  [] ?? xs--    xs ?? []  =  xs ++ xs-    xs ?? (x:ys)  =  [] ?? ys---class of 3 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:xs ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:xs ?? []---class of 4 equivalent candidates:--    [] ?? xs  =  xs ++ xs-    (x:xs) ?? ys  =  []--    [] ?? xs  =  xs ++ xs-    (x:xs) ?? ys  =  xs ?? xs--    [] ?? xs  =  xs ++ xs-    (x:xs) ?? ys  =  xs ?? []--    [] ?? xs  =  xs ++ xs-    (x:xs) ?? ys  =  ys ?? []---class of 3 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? xs--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? ys---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? ys--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? []---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? xs--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? []---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? xs-    (x:xs) ?? ys  =  xs--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? []-    (x:xs) ?? ys  =  xs---class of 4 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ++ ys--    [] ?? xs  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ++ xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ++ ys ?? []--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ?? [] ++ xs---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs ++ ys--    [] ?? xs  =  xs-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys ++ xs---class of 4 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ++ ys--    [] ?? xs  =  []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ++ xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ++ ys ?? []--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ?? [] ++ xs---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  xs ++ ys--    [] ?? xs  =  []-    (x:xs) ?? []  =  []-    (x:xs) ?? (y:ys)  =  ys ++ xs---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  (x:ys) ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [x] ?? ys---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  (xs ++ ys) ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ++ ys ?? ys---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  (ys ++ xs) ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ?? ys ++ xs---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? (x:xs)--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? [x]---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? (xs ++ ys)--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? xs ++ ys---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? (ys ++ xs)--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ++ xs ?? xs---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:ys ?? xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  x:(xs ++ ys)---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ++ xs ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  xs ?? ys ++ xs---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ++ ys ?? xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ?? xs ++ ys---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ++ ys ?? ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ++ [] ?? ys---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ++ [] ?? xs--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? xs ++ ys---class of 2 equivalent candidates:--    xs ?? []  =  xs-    xs ?? (x:ys)  =  ys ?? ys ++ ys--    xs ?? []  =  xs-    xs ?? (x:ys)  =  [] ?? ys ++ ys---class of 2 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs ++ xs ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs ?? ys ++ xs---class of 3 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ++ xs ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ++ ys ?? ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ++ [] ?? ys---class of 2 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ++ ys ?? xs--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ?? xs ++ ys---class of 2 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ++ [] ?? xs--    xs ?? []  =  []-    xs ?? (x:ys)  =  [] ?? xs ++ ys---class of 3 equivalent candidates:--    xs ?? []  =  []-    xs ?? (x:ys)  =  xs ?? ys ++ ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  ys ?? ys ++ ys--    xs ?? []  =  []-    xs ?? (x:ys)  =  [] ?? ys ++ ys---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:ys ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  x:(ys ++ xs)---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ++ xs ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ++ xs ?? []---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ++ ys ?? xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ?? xs ++ xs---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  ys ++ xs ?? ys--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? ys ++ ys---class of 2 equivalent candidates:--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? xs ++ xs--    [] ?? xs  =  xs-    (x:xs) ?? ys  =  xs ?? [] ++ xs---class of 3 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ++ xs ?? xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ++ xs ?? ys--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ++ xs ?? []---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ++ ys ?? xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ?? xs ++ xs---class of 2 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  ys ++ xs ?? ys--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ?? ys ++ ys---class of 3 equivalent candidates:--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ?? xs ++ xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ?? ys ++ xs--    [] ?? xs  =  []-    (x:xs) ?? ys  =  xs ?? [] ++ xs---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? xs---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ?? []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  [] ?? xs---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ?? []--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  [] ?? ys---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs ?? xs-    (x:xs) ?? (y:ys)  =  xs--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  [] ?? xs-    (x:xs) ?? (y:ys)  =  xs---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs ?? []-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys---class of 2 equivalent candidates:--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  xs ++ ys--    [] ?? []  =  []-    [] ?? (x:xs)  =  xs-    (x:xs) ?? []  =  xs-    (x:xs) ?? (y:ys)  =  ys ++ xs----Redundant candidates for: ton :: Bool -> Bool-  pruning with 39/49 rules-  [3,2,0,0,0,0] candidates-  4/5 unique candidates-  1/5 redundant candidates--rules:-not False == True-not True == False-p && p == p-p || p == p-not (not p) == p-p && False == False-p && True == p-False && p == False-True && p == p-p || False == p-p || True == True-False || p == p-True || p == True-not (p && q) == not p || not q-not (p && q) == not q || not p-not (p || q) == not p && not q-not (p || q) == not q && not p-p && not p == False-not p && p == False-p || not p == True-not p || p == True-(p && q) && r == p && (q && r)-(p && q) && r == q && (p && r)-(p || q) || r == p || (q || r)-(p || q) || r == q || (p || r)-p && (p && q) == p && q-p && (q && p) == p && q-p && (q && p) == q && p-p || (p || q) == p || q-p || (q || p) == p || q-p || (q || p) == q || p-p && (p || q) == p-p && (q || p) == p-(p || q) && p == p-(p || q) && q == q-p || p && q == p-p || q && p == p-p && q || p == p-p && q || q == q-equations:-q && p == p && q-q || p == p || q-q && (p && r) == p && (q && r)-r && (p && q) == p && (q && r)-r && (q && p) == p && (q && r)-q || (p || r) == p || (q || r)-r || (p || q) == p || (q || r)-r || (q || p) == p || (q || r)-(r || q) && p == p && (q || r)-r && q || p == p || q && r--class of 2 equivalent candidates:--    ton p  =  not p--    ton False  =  True-    ton True  =  False----Redundant candidates for: &| :: Bool -> Bool -> Bool-  pruning with 39/49 rules-  [4,12,20,6,2,16] candidates-  16/60 unique candidates-  44/60 redundant candidates--rules:-not False == True-not True == False-p && p == p-p || p == p-not (not p) == p-p && False == False-p && True == p-False && p == False-True && p == p-p || False == p-p || True == True-False || p == p-True || p == True-not (p && q) == not p || not q-not (p && q) == not q || not p-not (p || q) == not p && not q-not (p || q) == not q && not p-p && not p == False-not p && p == False-p || not p == True-not p || p == True-(p && q) && r == p && (q && r)-(p && q) && r == q && (p && r)-(p || q) || r == p || (q || r)-(p || q) || r == q || (p || r)-p && (p && q) == p && q-p && (q && p) == p && q-p && (q && p) == q && p-p || (p || q) == p || q-p || (q || p) == p || q-p || (q || p) == q || p-p && (p || q) == p-p && (q || p) == p-(p || q) && p == p-(p || q) && q == q-p || p && q == p-p || q && p == p-p && q || p == p-p && q || q == q-equations:-q && p == p && q-q || p == p || q-q && (p && r) == p && (q && r)-r && (p && q) == p && (q && r)-r && (q && p) == p && (q && r)-q || (p || r) == p || (q || r)-r || (p || q) == p || (q || r)-r || (q || p) == p || (q || r)-(r || q) && p == p && (q || r)-r && q || p == p || q && r--class of 5 equivalent candidates:--    p &| q  =  False--    p &| q  =  p && (q && not p)--    p &| q  =  q && (p && not q)--    p &| q  =  not p && (p && q)--    p &| q  =  not q && (p && q)---class of 5 equivalent candidates:--    p &| q  =  True--    p &| q  =  p || (q || not p)--    p &| q  =  q || (p || not q)--    p &| q  =  not p || (p || q)--    p &| q  =  not q || (p || q)---class of 2 equivalent candidates:--    p &| q  =  not p--    False &| p  =  True-    True &| p  =  False---class of 4 equivalent candidates:--    p &| q  =  not q--    p &| False  =  True-    p &| True  =  False--    False &| p  =  not p-    True &| False  =  True-    True &| True  =  False--    False &| False  =  True-    False &| True  =  False-    True &| p  =  not p---class of 5 equivalent candidates:--    p &| False  =  p-    p &| True  =  False--    False &| p  =  False-    True &| p  =  not p--    False &| p  =  False-    True &| False  =  True-    True &| True  =  False--    p &| q  =  p && not q--    p &| q  =  not q && (p || q)---class of 5 equivalent candidates:--    p &| False  =  p-    p &| True  =  True--    False &| p  =  p-    True &| p  =  True--    p &| q  =  p || q--    p &| q  =  p || q && not p--    p &| q  =  q || p && not q---class of 5 equivalent candidates:--    p &| False  =  False-    p &| True  =  p--    False &| p  =  False-    True &| p  =  p--    p &| q  =  p && q--    p &| q  =  p && (q || not p)--    p &| q  =  q && (p || not q)---class of 5 equivalent candidates:--    p &| False  =  True-    p &| True  =  p--    False &| p  =  not p-    True &| p  =  True--    False &| False  =  True-    False &| True  =  False-    True &| p  =  True--    p &| q  =  p || not q--    p &| q  =  not q || p && q---class of 4 equivalent candidates:--    False &| p  =  p-    True &| p  =  False--    p &| False  =  False-    p &| True  =  not p--    p &| q  =  q && not p--    p &| q  =  not p && (p || q)---class of 4 equivalent candidates:--    False &| p  =  True-    True &| p  =  p--    p &| False  =  not p-    p &| True  =  True--    p &| q  =  q || not p--    p &| q  =  not p || p && q+  pruning with 27/65 rules+  [3,3,9,10,32,39] candidates+  86/96 unique candidates+  10/96 redundant candidates++rules:+x - x == 0+x * 0 == 0+x * 1 == x+0 * x == 0+1 * x == x+x + 0 == x+0 + x == x+x - 0 == x+(x * y) * z == x * (y * z)+(x * y) * z == y * (x * z)+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+x - (y - z) == z + (x - y)+(x - y) - z == x - (y + z)+(x - y) - z == x - (z + y)+(x + y) - z == x + (y - z)+(x + y) - z == y + (x - z)+(x + x) * y == x * (y + y)+x + (y - x) == y+(x - y) + y == x+x * y - x == x * (y - 1)+x * y - y == y * (x - 1)+x * (y + 1) == x + x * y+x * (y + 1) == x * y + x+(x + 1) * y == y + x * y+0 - x * y == x * (0 - y)+0 - x * y == y * (0 - x)+equations:+y * x == x * y+y + x == x + y+y * (x * z) == x * (y * z)+z * (x * y) == x * (y * z)+z * (y * x) == x * (y * z)+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+y + (x - z) == x + (y - z)+z * y + x == x + y * z+(x - z) + y == x + (y - z)+(z - y) + x == (x - y) + z+y * (x + x) == x * (y + y)+y - (x + y) == 0 - x+y - (y + x) == 0 - x+z - (y + z) == x - (x + y)+z - (y + z) == x - (y + x)+z - (z + y) == x - (x + y)+z - (z + y) == x - (y + x)+x * (1 - y) == x - x * y+x * (1 - y) == x - y * x+y * (0 - x) == x * (0 - y)+(0 - x) * y == x * (0 - y)+(0 - y) * x == (0 - x) * y+(1 - y) * x == x - x * y+(1 - y) * x == x - y * x+x + (0 - y) == x - y+(0 - y) + x == x - y+x - (x + 1) == 0 - 1+x - (1 + x) == 0 - 1+y - (y + 1) == x - (x + 1)+y - (y + 1) == x - (1 + x)+y - (1 + y) == x - (1 + x)+x * (0 - 1) == 0 - x+(0 - 1) * x == 0 - x+(0 - 1) * y == x - (x + y)+(0 - 1) * y == x - (y + x)++class of 3 equivalent candidates:++    foo x  =  0 - x++    foo x  =  x - (x + x)++    foo x  =  1 - (x + 1)+++class of 2 equivalent candidates:++    foo x  =  1 - x++    foo x  =  1 + (0 - x)+++class of 2 equivalent candidates:++    foo 0  =  0+    foo x  =  1 - x++    foo 0  =  0+    foo x  =  1 + (0 - x)+++class of 3 equivalent candidates:++    foo 0  =  1+    foo x  =  0 - x++    foo 0  =  1+    foo x  =  x - (x + x)++    foo 0  =  1+    foo x  =  1 - (x + 1)+++class of 2 equivalent candidates:++    foo x  =  x + (x + 1)++    foo x  =  1 + (x + x)+++class of 2 equivalent candidates:++    foo x  =  x * (1 - x)++    foo x  =  x - x * x+++class of 2 equivalent candidates:++    foo 0  =  0+    foo x  =  x + (x + 1)++    foo 0  =  0+    foo x  =  1 + (x + x)+++class of 2 equivalent candidates:++    foo 0  =  1+    foo x  =  x * (1 - x)++    foo 0  =  1+    foo x  =  x - x * x++++Redundant candidates for: ? :: Int -> Int -> Int+  pruning with 13/34 rules+  [3,8,25,71,205] candidates+  294/312 unique candidates+  18/312 redundant candidates++rules:+x * 0 == 0+0 * x == 0+x + 0 == x+0 + x == x+dec (x + y) == x + dec y+dec (x + y) == y + dec x+dec (x + y) == dec x + y+dec (x + y) == dec y + x+(x * y) * z == x * (y * z)+(x * y) * z == y * (x * z)+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+(x + x) * y == x * (y + y)+equations:+y * x == x * y+y + x == x + y+y + dec x == x + dec y+dec x + y == x + dec y+dec y + x == dec x + y+x + dec 0 == dec x+dec 0 + x == dec x+y * (x * z) == x * (y * z)+z * (x * y) == x * (y * z)+z * (y * x) == x * (y * z)+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+z * y + x == x + y * z+y * (x + x) == x * (y + y)+y + dec (dec x) == x + dec (dec y)+dec (dec x) + y == x + dec (dec y)+dec (dec y) + x == dec (dec x) + y+x + dec (dec 0) == dec (dec x)+dec (dec 0) + x == dec (dec x)++class of 2 equivalent candidates:++    x ? y  =  x++    x ? 0  =  x+    x ? y  =  x ? dec y+++class of 2 equivalent candidates:++    x ? y  =  y++    0 ? x  =  x+    x ? y  =  dec x ? y+++class of 2 equivalent candidates:++    x ? 0  =  x+    x ? y  =  0++    x ? 0  =  x+    x ? y  =  0 ? dec y+++class of 2 equivalent candidates:++    0 ? x  =  x+    x ? y  =  0++    0 ? x  =  x+    x ? y  =  dec x ? 0+++class of 2 equivalent candidates:++    x ? y  =  x + dec y++    x ? y  =  y + dec x+++class of 2 equivalent candidates:++    x ? y  =  x + (x + y)++    x ? y  =  y + (x + x)+++class of 2 equivalent candidates:++    x ? y  =  x + (y + y)++    x ? y  =  y + (x + y)+++class of 2 equivalent candidates:++    x ? y  =  x + dec (dec x)++    x ? y  =  dec x + dec x+++class of 3 equivalent candidates:++    x ? y  =  x + dec (dec y)++    x ? y  =  y + dec (dec x)++    x ? y  =  dec x + dec y+++class of 2 equivalent candidates:++    x ? y  =  y + dec (dec y)++    x ? y  =  dec y + dec y+++class of 2 equivalent candidates:++    x ? y  =  x * (y + y)++    x ? y  =  y * (x + x)+++class of 2 equivalent candidates:++    x ? y  =  x * (x * y)++    x ? y  =  y * (x * x)+++class of 2 equivalent candidates:++    x ? y  =  x * (y * y)++    x ? y  =  y * (x * y)+++class of 2 equivalent candidates:++    x ? 0  =  x+    x ? y  =  x + dec y++    x ? 0  =  x+    x ? y  =  y + dec x+++class of 2 equivalent candidates:++    x ? 0  =  0+    x ? y  =  x + dec y++    x ? 0  =  0+    x ? y  =  y + dec x+++class of 2 equivalent candidates:++    0 ? x  =  x+    x ? y  =  x + dec y++    0 ? x  =  x+    x ? y  =  y + dec x+++class of 2 equivalent candidates:++    0 ? x  =  0+    x ? y  =  x + dec y++    0 ? x  =  0+    x ? y  =  y + dec x++++Redundant candidates for: goo :: [Int] -> [Int]+  pruning with 4/4 rules+  [2,1,1,2,4,7] candidates+  15/17 unique candidates+  2/17 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++class of 2 equivalent candidates:++    goo xs  =  xs++    goo []  =  []+    goo (x:xs)  =  x:goo xs+++class of 2 equivalent candidates:++    goo xs  =  []++    goo []  =  []+    goo (x:xs)  =  goo xs ++ goo xs++++Redundant candidates for: ?? :: [Int] -> [Int] -> [Int]+  pruning with 4/4 rules+  [3,8,15,43,122] candidates+  150/191 unique candidates+  41/191 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++class of 2 equivalent candidates:++    xs ?? ys  =  xs++    xs ?? []  =  xs+    xs ?? (x:ys)  =  xs ?? ys+++class of 2 equivalent candidates:++    xs ?? ys  =  ys++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  xs ?? ys+++class of 5 equivalent candidates:++    xs ?? []  =  xs+    xs ?? (x:ys)  =  []++    xs ?? []  =  xs+    xs ?? (x:ys)  =  ys ?? ys++    xs ?? []  =  xs+    xs ?? (x:ys)  =  [] ?? xs++    xs ?? []  =  xs+    xs ?? (x:ys)  =  [] ?? ys++    [] ?? xs  =  []+    (x:xs) ?? []  =  x:xs+    (x:xs) ?? (y:ys)  =  []+++class of 2 equivalent candidates:++    xs ?? []  =  []+    xs ?? (x:ys)  =  xs++    [] ?? xs  =  []+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  x:xs+++class of 3 equivalent candidates:++    xs ?? []  =  []+    xs ?? (x:ys)  =  ys++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  xs ?? ys++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  [] ?? ys+++class of 10 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  []++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  xs ?? xs++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  xs ?? []++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  ys ?? []++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs ?? xs+    (x:xs) ?? (y:ys)  =  []++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs ?? []+    (x:xs) ?? (y:ys)  =  []++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs ?? xs++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs ?? []++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys ?? ys++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys ?? []+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? ys  =  xs++    [] ?? []  =  []+    [] ?? (x:xs)  =  [] ?? xs+    (x:xs) ?? ys  =  xs+++class of 3 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? ys  =  ys++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs ?? []+    (x:xs) ?? ys  =  ys++    [] ?? []  =  []+    [] ?? (x:xs)  =  [] ?? xs+    (x:xs) ?? ys  =  ys+++class of 3 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  []++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ?? xs++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ?? ys+++class of 2 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs ?? []+    (x:xs) ?? (y:ys)  =  xs+++class of 2 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs ?? []+    (x:xs) ?? (y:ys)  =  ys+++class of 3 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  []++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ?? xs++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ?? ys+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs ?? []+    (x:xs) ?? (y:ys)  =  xs+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs ?? []+    (x:xs) ?? (y:ys)  =  ys+++class of 2 equivalent candidates:++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  ys++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs ?? xs+    (x:xs) ?? ys  =  ys+++class of 4 equivalent candidates:++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  []++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  xs ?? xs++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  xs ?? []++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs+    (x:xs) ?? ys  =  ys ?? []+++class of 2 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? ys  =  ys ?? xs++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ?? ys+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ?? ys++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ?? []+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ?? xs++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ?? []+++class of 2 equivalent candidates:++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs ?? xs+    (x:xs) ?? ys  =  xs++    [] ?? []  =  []+    [] ?? (x:xs)  =  xs ?? []+    (x:xs) ?? ys  =  xs+++class of 2 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ++ ys++    [] ?? xs  =  xs+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ++ xs+++class of 2 equivalent candidates:++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs ++ ys++    [] ?? xs  =  xs+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys ++ xs+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  xs ++ ys++    [] ?? xs  =  []+    (x:xs) ?? []  =  xs+    (x:xs) ?? (y:ys)  =  ys ++ xs+++class of 2 equivalent candidates:++    [] ?? xs  =  []+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  xs ++ ys++    [] ?? xs  =  []+    (x:xs) ?? []  =  []+    (x:xs) ?? (y:ys)  =  ys ++ xs++++Redundant candidates for: ton :: Bool -> Bool+  pruning with 39/49 rules+  [3,2,0,0,0,0] candidates+  4/5 unique candidates+  1/5 redundant candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++class of 2 equivalent candidates:++    ton p  =  not p++    ton False  =  True+    ton True  =  False++++Redundant candidates for: &| :: Bool -> Bool -> Bool+  pruning with 39/49 rules+  [4,12,20,6,2] candidates+  16/44 unique candidates+  28/44 redundant candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++class of 2 equivalent candidates:++    p &| q  =  not p++    False &| p  =  True+    True &| p  =  False+++class of 4 equivalent candidates:++    p &| q  =  not q++    p &| False  =  True+    p &| True  =  False++    False &| p  =  not p+    True &| False  =  True+    True &| True  =  False++    False &| False  =  True+    False &| True  =  False+    True &| p  =  not p+++class of 4 equivalent candidates:++    p &| False  =  p+    p &| True  =  False++    False &| p  =  False+    True &| p  =  not p++    False &| p  =  False+    True &| False  =  True+    True &| True  =  False++    p &| q  =  p && not q+++class of 3 equivalent candidates:++    p &| False  =  p+    p &| True  =  True++    False &| p  =  p+    True &| p  =  True++    p &| q  =  p || q+++class of 3 equivalent candidates:++    p &| False  =  False+    p &| True  =  p++    False &| p  =  False+    True &| p  =  p++    p &| q  =  p && q+++class of 4 equivalent candidates:++    p &| False  =  True+    p &| True  =  p++    False &| p  =  not p+    True &| p  =  True++    False &| False  =  True+    False &| True  =  False+    True &| p  =  True++    p &| q  =  p || not q+++class of 3 equivalent candidates:++    False &| p  =  p+    True &| p  =  False++    p &| False  =  False+    p &| True  =  not p++    p &| q  =  q && not p+++class of 3 equivalent candidates:++    False &| p  =  True+    True &| p  =  p++    p &| False  =  not p+    p &| True  =  True++    p &| q  =  q || not p   class of 3 equivalent candidates: