SMT: Assertions: ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀a b. a ⊕ b = (let x = fst a ⊕ fst b; y = snd a ⊕ snd b in if x = None ∨ y = None then None else Some (the x, the y)) ∀x c. Some x = x ⊕ c ⟶ (∃r. Some |x| = c ⊕ r) ∀x c. Some x = x ⊕ c ⟶ (∃r. Some |x| = c ⊕ r) ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀x1 x2. fst (x1, x2) = x1 ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option x2. option = Some x2 ⟶ option ≠ None ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀option. (option = None ⟶ False) ∧ (option = Some (the option) ⟶ False) ⟶ False ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x2. the (Some x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 ∀x1 x2. snd (x1, x2) = x2 Some x = x ⊕ c ¬ ((∀r1 r2. Some |fst x| = fst c ⊕ r1 ∧ Some |snd x| = snd c ⊕ r2 ⟶ thesis) ⟶ thesis) SMT: Names: sorts: A$ = 'a B$ = 'b A_a_prod$ = 'a × 'a A_b_prod$ = 'a × 'b A_option$ = 'a option B_a_prod$ = 'b × 'a B_b_prod$ = 'b × 'b B_option$ = 'b option A_a_a_prod_prod$ = 'a × 'a × 'a A_a_b_prod_prod$ = 'a × 'a × 'b A_a_prod_a_prod$ = ('a × 'a) × 'a A_a_prod_option$ = ('a × 'a) option A_b_a_prod_prod$ = 'a × 'b × 'a A_b_b_prod_prod$ = 'a × 'b × 'b A_b_prod_a_prod$ = ('a × 'b) × 'a A_b_prod_b_prod$ = ('a × 'b) × 'b A_b_prod_option$ = ('a × 'b) option B_a_a_prod_prod$ = 'b × 'a × 'a B_a_b_prod_prod$ = 'b × 'a × 'b B_a_prod_a_prod$ = ('b × 'a) × 'a B_a_prod_b_prod$ = ('b × 'a) × 'b B_a_prod_option$ = ('b × 'a) option B_b_a_prod_prod$ = 'b × 'b × 'a B_b_b_prod_prod$ = 'b × 'b × 'b B_b_prod_a_prod$ = ('b × 'b) × 'a B_b_prod_b_prod$ = ('b × 'b) × 'b B_b_prod_option$ = ('b × 'b) option A_a_a_a_prod_prod_prod$ = 'a × 'a × 'a × 'a A_a_a_b_prod_prod_prod$ = 'a × 'a × 'a × 'b A_a_a_prod_prod_option$ = ('a × 'a × 'a) option A_a_b_a_prod_prod_prod$ = 'a × 'a × 'b × 'a A_a_b_b_prod_prod_prod$ = 'a × 'a × 'b × 'b A_a_b_prod_prod_option$ = ('a × 'a × 'b) option A_a_prod_a_prod_option$ = (('a × 'a) × 'a) option A_b_a_b_prod_prod_prod$ = 'a × 'b × 'a × 'b A_b_a_prod_prod_option$ = ('a × 'b × 'a) option A_b_b_prod_prod_option$ = ('a × 'b × 'b) option A_b_prod_a_b_prod_prod$ = ('a × 'b) × 'a × 'b A_b_prod_a_prod_option$ = (('a × 'b) × 'a) option A_b_prod_b_prod_option$ = (('a × 'b) × 'b) option B_a_a_prod_prod_option$ = ('b × 'a × 'a) option B_a_b_prod_prod_option$ = ('b × 'a × 'b) option B_a_prod_a_prod_option$ = (('b × 'a) × 'a) option B_a_prod_b_prod_option$ = (('b × 'a) × 'b) option B_b_a_prod_prod_option$ = ('b × 'b × 'a) option B_b_b_prod_prod_option$ = ('b × 'b × 'b) option B_b_prod_a_prod_option$ = (('b × 'b) × 'a) option B_b_prod_b_prod_option$ = (('b × 'b) × 'b) option A_a_a_a_a_prod_prod_prod_prod$ = 'a × 'a × 'a × 'a × 'a A_a_a_a_b_prod_prod_prod_prod$ = 'a × 'a × 'a × 'a × 'b A_a_a_a_prod_prod_prod_option$ = ('a × 'a × 'a × 'a) option A_a_a_b_a_prod_prod_prod_prod$ = 'a × 'a × 'a × 'b × 'a A_a_a_b_b_prod_prod_prod_prod$ = 'a × 'a × 'a × 'b × 'b A_a_a_b_prod_prod_prod_option$ = ('a × 'a × 'a × 'b) option A_a_b_a_b_prod_prod_prod_prod$ = 'a × 'a × 'b × 'a × 'b A_a_b_a_prod_prod_prod_option$ = ('a × 'a × 'b × 'a) option A_a_b_b_prod_prod_prod_option$ = ('a × 'a × 'b × 'b) option A_b_a_b_prod_prod_prod_option$ = ('a × 'b × 'a × 'b) option A_b_prod_a_b_prod_prod_option$ = (('a × 'b) × 'a × 'b) option A_a_a_a_b_prod_prod_prod_prod_option$ = ('a × 'a × 'a × 'a × 'b) option A_a_a_b_a_b_prod_prod_prod_prod_prod$ = 'a × 'a × 'a × 'b × 'a × 'b A_a_a_b_a_prod_prod_prod_prod_option$ = ('a × 'a × 'a × 'b × 'a) option A_a_a_b_b_prod_prod_prod_prod_option$ = ('a × 'a × 'a × 'b × 'b) option A_a_b_a_b_prod_prod_prod_prod_option$ = ('a × 'a × 'b × 'a × 'b) option functions: c$ = c x$ = x fst$ = fst snd$ = snd the$ = the core$ = core fst$a = fst fst$b = fst fst$c = fst fst$d = fst fst$e = fst fst$f = fst fst$g = fst fst$h = fst fst$i = fst fst$j = fst fst$k = fst fst$l = fst fst$m = fst fst$n = fst fst$o = fst fst$p = fst fst$q = fst fst$r = fst fst$s = fst fst$t = fst fst$u = fst fst$v = fst fst$w = fst fst$x = fst fst$y = fst fst$z = fst none$ = None pair$ = Pair plus$ = (⊕) snd$a = snd snd$b = snd snd$c = snd snd$d = snd snd$e = snd snd$f = snd snd$g = snd snd$h = snd snd$i = snd snd$j = snd snd$k = snd snd$l = snd snd$m = snd snd$n = snd snd$o = snd snd$p = snd snd$q = snd snd$r = snd snd$s = snd snd$t = snd snd$u = snd snd$v = snd snd$w = snd snd$x = snd snd$y = snd snd$z = snd some$ = Some the$a = the the$b = the the$c = the the$d = the the$e = the the$f = the the$g = the the$h = the the$i = the the$j = the the$k = the the$l = the the$m = the the$n = the the$o = the the$p = the the$q = the the$r = the the$s = the core$a = core fst$aa = fst fst$ab = fst fst$ac = fst fst$ad = fst none$a = None none$b = None none$c = None none$d = None none$e = None none$f = None none$g = None none$h = None none$i = None none$j = None none$k = None none$l = None none$m = None none$n = None none$o = None none$p = None none$q = None none$r = None none$s = None none$t = None none$u = None none$v = None none$w = None none$x = None none$y = None none$z = None pair$a = Pair pair$b = Pair pair$c = Pair pair$d = Pair pair$e = Pair pair$f = Pair pair$g = Pair pair$h = Pair pair$i = Pair pair$j = Pair pair$k = Pair pair$l = Pair pair$m = Pair pair$n = Pair pair$o = Pair pair$p = Pair pair$q = Pair pair$r = Pair pair$s = Pair pair$t = Pair pair$u = Pair pair$v = Pair pair$w = Pair pair$x = Pair pair$y = Pair pair$z = Pair plus$a = (⊕) plus$b = (⊕) plus$c = (⊕) plus$d = (⊕) plus$e = (⊕) plus$f = (⊕) plus$g = (⊕) plus$h = (⊕) plus$i = (⊕) plus$j = (⊕) plus$k = (⊕) plus$l = (⊕) plus$m = (⊕) plus$n = (⊕) plus$o = (⊕) plus$p = (⊕) plus$q = (⊕) plus$r = (⊕) plus$s = (⊕) plus$t = (⊕) plus$u = (⊕) snd$aa = snd snd$ab = snd snd$ac = snd snd$ad = snd some$a = Some some$b = Some some$c = Some some$d = Some some$e = Some some$f = Some some$g = Some some$h = Some some$i = Some some$j = Some some$k = Some some$l = Some some$m = Some some$n = Some some$o = Some some$p = Some some$q = Some some$r = Some some$s = Some some$t = Some some$u = Some some$v = Some some$w = Some some$x = Some some$y = Some some$z = Some none$aa = None none$ab = None none$ac = None none$ad = None pair$aa = Pair pair$ab = Pair pair$ac = Pair pair$ad = Pair some$aa = Some some$ab = Some some$ac = Some some$ad = Some thesis$ = thesis SMT: Problem: ; --proof-with-sharing --proof-define-skolems --proof-prune --proof-merge --disable-print-success --disable-banner --index-sorts --index-fresh-sorts --triggers-new --triggers-sel-rm-specific (set-option :produce-proofs true) (set-logic AUFLIA) (declare-sort A$ 0) (declare-sort B$ 0) (declare-sort A_a_prod$ 0) (declare-sort A_b_prod$ 0) (declare-sort A_option$ 0) (declare-sort B_a_prod$ 0) (declare-sort B_b_prod$ 0) (declare-sort B_option$ 0) (declare-sort A_a_a_prod_prod$ 0) (declare-sort A_a_b_prod_prod$ 0) (declare-sort A_a_prod_a_prod$ 0) (declare-sort A_a_prod_option$ 0) (declare-sort A_b_a_prod_prod$ 0) (declare-sort A_b_b_prod_prod$ 0) (declare-sort A_b_prod_a_prod$ 0) (declare-sort A_b_prod_b_prod$ 0) (declare-sort A_b_prod_option$ 0) (declare-sort B_a_a_prod_prod$ 0) (declare-sort B_a_b_prod_prod$ 0) (declare-sort B_a_prod_a_prod$ 0) (declare-sort B_a_prod_b_prod$ 0) (declare-sort B_a_prod_option$ 0) (declare-sort B_b_a_prod_prod$ 0) (declare-sort B_b_b_prod_prod$ 0) (declare-sort B_b_prod_a_prod$ 0) (declare-sort B_b_prod_b_prod$ 0) (declare-sort B_b_prod_option$ 0) (declare-sort A_a_a_a_prod_prod_prod$ 0) (declare-sort A_a_a_b_prod_prod_prod$ 0) (declare-sort A_a_a_prod_prod_option$ 0) (declare-sort A_a_b_a_prod_prod_prod$ 0) (declare-sort A_a_b_b_prod_prod_prod$ 0) (declare-sort A_a_b_prod_prod_option$ 0) (declare-sort A_a_prod_a_prod_option$ 0) (declare-sort A_b_a_b_prod_prod_prod$ 0) (declare-sort A_b_a_prod_prod_option$ 0) (declare-sort A_b_b_prod_prod_option$ 0) (declare-sort A_b_prod_a_b_prod_prod$ 0) (declare-sort A_b_prod_a_prod_option$ 0) (declare-sort A_b_prod_b_prod_option$ 0) (declare-sort B_a_a_prod_prod_option$ 0) (declare-sort B_a_b_prod_prod_option$ 0) (declare-sort B_a_prod_a_prod_option$ 0) (declare-sort B_a_prod_b_prod_option$ 0) (declare-sort B_b_a_prod_prod_option$ 0) (declare-sort B_b_b_prod_prod_option$ 0) (declare-sort B_b_prod_a_prod_option$ 0) (declare-sort B_b_prod_b_prod_option$ 0) (declare-sort A_a_a_a_a_prod_prod_prod_prod$ 0) (declare-sort A_a_a_a_b_prod_prod_prod_prod$ 0) (declare-sort A_a_a_a_prod_prod_prod_option$ 0) (declare-sort A_a_a_b_a_prod_prod_prod_prod$ 0) (declare-sort A_a_a_b_b_prod_prod_prod_prod$ 0) (declare-sort A_a_a_b_prod_prod_prod_option$ 0) (declare-sort A_a_b_a_b_prod_prod_prod_prod$ 0) (declare-sort A_a_b_a_prod_prod_prod_option$ 0) (declare-sort A_a_b_b_prod_prod_prod_option$ 0) (declare-sort A_b_a_b_prod_prod_prod_option$ 0) (declare-sort A_b_prod_a_b_prod_prod_option$ 0) (declare-sort A_a_a_a_b_prod_prod_prod_prod_option$ 0) (declare-sort A_a_a_b_a_b_prod_prod_prod_prod_prod$ 0) (declare-sort A_a_a_b_a_prod_prod_prod_prod_option$ 0) (declare-sort A_a_a_b_b_prod_prod_prod_prod_option$ 0) (declare-sort A_a_b_a_b_prod_prod_prod_prod_option$ 0) (declare-fun c$ () A_b_prod$) (declare-fun x$ () A_b_prod$) (declare-fun fst$ (A_a_prod$) A$) (declare-fun snd$ (A_a_prod$) A$) (declare-fun the$ (A_option$) A$) (declare-fun core$ (A$) A$) (declare-fun fst$a (B_a_prod$) B$) (declare-fun fst$b (B_b_prod$) B$) (declare-fun fst$c (A_b_prod$) A$) (declare-fun fst$d (A_b_prod_a_prod$) A_b_prod$) (declare-fun fst$e (A_b_prod_b_prod$) A_b_prod$) (declare-fun fst$f (A_a_b_prod_prod$) A$) (declare-fun fst$g (B_a_b_prod_prod$) B$) (declare-fun fst$h (A_b_prod_a_b_prod_prod$) A_b_prod$) (declare-fun fst$i (A_b_b_prod_prod$) A$) (declare-fun fst$j (A_b_a_prod_prod$) A$) (declare-fun fst$k (A_a_a_prod_prod$) A$) (declare-fun fst$l (B_b_b_prod_prod$) B$) (declare-fun fst$m (B_b_a_prod_prod$) B$) (declare-fun fst$n (B_a_a_prod_prod$) B$) (declare-fun fst$o (B_b_prod_a_prod$) B_b_prod$) (declare-fun fst$p (B_b_prod_b_prod$) B_b_prod$) (declare-fun fst$q (B_a_prod_a_prod$) B_a_prod$) (declare-fun fst$r (B_a_prod_b_prod$) B_a_prod$) (declare-fun fst$s (A_a_prod_a_prod$) A_a_prod$) (declare-fun fst$t (A_b_a_b_prod_prod_prod$) A$) (declare-fun fst$u (A_a_a_b_prod_prod_prod$) A$) (declare-fun fst$v (A_a_b_b_prod_prod_prod$) A$) (declare-fun fst$w (A_a_b_a_prod_prod_prod$) A$) (declare-fun fst$x (A_a_a_a_prod_prod_prod$) A$) (declare-fun fst$y (A_a_b_a_b_prod_prod_prod_prod$) A$) (declare-fun fst$z (A_a_a_a_b_prod_prod_prod_prod$) A$) (declare-fun none$ () A_option$) (declare-fun pair$ (A$ A$) A_a_prod$) (declare-fun plus$ (A_a_prod$ A_a_prod$) A_a_prod_option$) (declare-fun snd$a (B_a_prod$) A$) (declare-fun snd$b (B_b_prod$) B$) (declare-fun snd$c (A_b_prod$) B$) (declare-fun snd$d (A_b_prod_a_prod$) A$) (declare-fun snd$e (A_b_prod_b_prod$) B$) (declare-fun snd$f (A_a_b_prod_prod$) A_b_prod$) (declare-fun snd$g (B_a_b_prod_prod$) A_b_prod$) (declare-fun snd$h (A_b_prod_a_b_prod_prod$) A_b_prod$) (declare-fun snd$i (A_b_b_prod_prod$) B_b_prod$) (declare-fun snd$j (A_b_a_prod_prod$) B_a_prod$) (declare-fun snd$k (A_a_a_prod_prod$) A_a_prod$) (declare-fun snd$l (B_b_b_prod_prod$) B_b_prod$) (declare-fun snd$m (B_b_a_prod_prod$) B_a_prod$) (declare-fun snd$n (B_a_a_prod_prod$) A_a_prod$) (declare-fun snd$o (B_b_prod_a_prod$) A$) (declare-fun snd$p (B_b_prod_b_prod$) B$) (declare-fun snd$q (B_a_prod_a_prod$) A$) (declare-fun snd$r (B_a_prod_b_prod$) B$) (declare-fun snd$s (A_a_prod_a_prod$) A$) (declare-fun snd$t (A_b_a_b_prod_prod_prod$) B_a_b_prod_prod$) (declare-fun snd$u (A_a_a_b_prod_prod_prod$) A_a_b_prod_prod$) (declare-fun snd$v (A_a_b_b_prod_prod_prod$) A_b_b_prod_prod$) (declare-fun snd$w (A_a_b_a_prod_prod_prod$) A_b_a_prod_prod$) (declare-fun snd$x (A_a_a_a_prod_prod_prod$) A_a_a_prod_prod$) (declare-fun snd$y (A_a_b_a_b_prod_prod_prod_prod$) A_b_a_b_prod_prod_prod$) (declare-fun snd$z (A_a_a_a_b_prod_prod_prod_prod$) A_a_a_b_prod_prod_prod$) (declare-fun some$ (A_a_prod$) A_a_prod_option$) (declare-fun the$a (B_option$) B$) (declare-fun the$b (A_b_prod_option$) A_b_prod$) (declare-fun the$c (B_b_prod_option$) B_b_prod$) (declare-fun the$d (B_a_prod_option$) B_a_prod$) (declare-fun the$e (A_a_prod_option$) A_a_prod$) (declare-fun the$f (B_a_b_prod_prod_option$) B_a_b_prod_prod$) (declare-fun the$g (A_a_b_prod_prod_option$) A_a_b_prod_prod$) (declare-fun the$h (A_b_b_prod_prod_option$) A_b_b_prod_prod$) (declare-fun the$i (A_b_a_prod_prod_option$) A_b_a_prod_prod$) (declare-fun the$j (A_a_a_prod_prod_option$) A_a_a_prod_prod$) (declare-fun the$k (A_b_a_b_prod_prod_prod_option$) A_b_a_b_prod_prod_prod$) (declare-fun the$l (A_a_a_b_prod_prod_prod_option$) A_a_a_b_prod_prod_prod$) (declare-fun the$m (A_a_b_b_prod_prod_prod_option$) A_a_b_b_prod_prod_prod$) (declare-fun the$n (A_a_b_a_prod_prod_prod_option$) A_a_b_a_prod_prod_prod$) (declare-fun the$o (A_a_a_a_prod_prod_prod_option$) A_a_a_a_prod_prod_prod$) (declare-fun the$p (A_a_b_a_b_prod_prod_prod_prod_option$) A_a_b_a_b_prod_prod_prod_prod$) (declare-fun the$q (A_a_a_a_b_prod_prod_prod_prod_option$) A_a_a_a_b_prod_prod_prod_prod$) (declare-fun the$r (A_a_a_b_b_prod_prod_prod_prod_option$) A_a_a_b_b_prod_prod_prod_prod$) (declare-fun the$s (A_a_a_b_a_prod_prod_prod_prod_option$) A_a_a_b_a_prod_prod_prod_prod$) (declare-fun core$a (B$) B$) (declare-fun fst$aa (A_a_a_b_b_prod_prod_prod_prod$) A$) (declare-fun fst$ab (A_a_a_b_a_prod_prod_prod_prod$) A$) (declare-fun fst$ac (A_a_a_a_a_prod_prod_prod_prod$) A$) (declare-fun fst$ad (A_a_a_b_a_b_prod_prod_prod_prod_prod$) A$) (declare-fun none$a () A_a_prod_option$) (declare-fun none$b () B_option$) (declare-fun none$c () B_a_prod_option$) (declare-fun none$d () B_b_prod_option$) (declare-fun none$e () A_b_prod_option$) (declare-fun none$f () A_b_prod_a_prod_option$) (declare-fun none$g () A_b_prod_b_prod_option$) (declare-fun none$h () A_a_b_prod_prod_option$) (declare-fun none$i () B_a_b_prod_prod_option$) (declare-fun none$j () A_b_prod_a_b_prod_prod_option$) (declare-fun none$k () A_b_b_prod_prod_option$) (declare-fun none$l () A_b_a_prod_prod_option$) (declare-fun none$m () A_a_a_prod_prod_option$) (declare-fun none$n () B_b_b_prod_prod_option$) (declare-fun none$o () B_b_a_prod_prod_option$) (declare-fun none$p () B_a_a_prod_prod_option$) (declare-fun none$q () B_b_prod_a_prod_option$) (declare-fun none$r () B_b_prod_b_prod_option$) (declare-fun none$s () B_a_prod_a_prod_option$) (declare-fun none$t () B_a_prod_b_prod_option$) (declare-fun none$u () A_a_prod_a_prod_option$) (declare-fun none$v () A_b_a_b_prod_prod_prod_option$) (declare-fun none$w () A_a_a_b_prod_prod_prod_option$) (declare-fun none$x () A_a_b_b_prod_prod_prod_option$) (declare-fun none$y () A_a_b_a_prod_prod_prod_option$) (declare-fun none$z () A_a_a_a_prod_prod_prod_option$) (declare-fun pair$a (B$ A$) B_a_prod$) (declare-fun pair$b (B$ B$) B_b_prod$) (declare-fun pair$c (A$ B$) A_b_prod$) (declare-fun pair$d (A_b_prod$ A$) A_b_prod_a_prod$) (declare-fun pair$e (A_b_prod$ B$) A_b_prod_b_prod$) (declare-fun pair$f (A$ A_b_prod$) A_a_b_prod_prod$) (declare-fun pair$g (B$ A_b_prod$) B_a_b_prod_prod$) (declare-fun pair$h (A_b_prod$ A_b_prod$) A_b_prod_a_b_prod_prod$) (declare-fun pair$i (A$ B_b_prod$) A_b_b_prod_prod$) (declare-fun pair$j (A$ B_a_prod$) A_b_a_prod_prod$) (declare-fun pair$k (A$ A_a_prod$) A_a_a_prod_prod$) (declare-fun pair$l (B$ B_b_prod$) B_b_b_prod_prod$) (declare-fun pair$m (B$ B_a_prod$) B_b_a_prod_prod$) (declare-fun pair$n (B$ A_a_prod$) B_a_a_prod_prod$) (declare-fun pair$o (B_b_prod$ A$) B_b_prod_a_prod$) (declare-fun pair$p (B_b_prod$ B$) B_b_prod_b_prod$) (declare-fun pair$q (B_a_prod$ A$) B_a_prod_a_prod$) (declare-fun pair$r (B_a_prod$ B$) B_a_prod_b_prod$) (declare-fun pair$s (A_a_prod$ A$) A_a_prod_a_prod$) (declare-fun pair$t (A$ B_a_b_prod_prod$) A_b_a_b_prod_prod_prod$) (declare-fun pair$u (A$ A_a_b_prod_prod$) A_a_a_b_prod_prod_prod$) (declare-fun pair$v (A$ A_b_b_prod_prod$) A_a_b_b_prod_prod_prod$) (declare-fun pair$w (A$ A_b_a_prod_prod$) A_a_b_a_prod_prod_prod$) (declare-fun pair$x (A$ A_a_a_prod_prod$) A_a_a_a_prod_prod_prod$) (declare-fun pair$y (A$ A_b_a_b_prod_prod_prod$) A_a_b_a_b_prod_prod_prod_prod$) (declare-fun pair$z (A$ A_a_a_b_prod_prod_prod$) A_a_a_a_b_prod_prod_prod_prod$) (declare-fun plus$a (A$ A$) A_option$) (declare-fun plus$b (B_a_prod$ B_a_prod$) B_a_prod_option$) (declare-fun plus$c (B$ B$) B_option$) (declare-fun plus$d (B_b_prod$ B_b_prod$) B_b_prod_option$) (declare-fun plus$e (A_b_prod$ A_b_prod$) A_b_prod_option$) (declare-fun plus$f (A_b_prod_a_prod$ A_b_prod_a_prod$) A_b_prod_a_prod_option$) (declare-fun plus$g (A_b_prod_b_prod$ A_b_prod_b_prod$) A_b_prod_b_prod_option$) (declare-fun plus$h (A_a_b_prod_prod$ A_a_b_prod_prod$) A_a_b_prod_prod_option$) (declare-fun plus$i (B_a_b_prod_prod$ B_a_b_prod_prod$) B_a_b_prod_prod_option$) (declare-fun plus$j (A_b_prod_a_b_prod_prod$ A_b_prod_a_b_prod_prod$) A_b_prod_a_b_prod_prod_option$) (declare-fun plus$k (A_b_b_prod_prod$ A_b_b_prod_prod$) A_b_b_prod_prod_option$) (declare-fun plus$l (A_b_a_prod_prod$ A_b_a_prod_prod$) A_b_a_prod_prod_option$) (declare-fun plus$m (A_a_a_prod_prod$ A_a_a_prod_prod$) A_a_a_prod_prod_option$) (declare-fun plus$n (B_b_b_prod_prod$ B_b_b_prod_prod$) B_b_b_prod_prod_option$) (declare-fun plus$o (B_b_a_prod_prod$ B_b_a_prod_prod$) B_b_a_prod_prod_option$) (declare-fun plus$p (B_a_a_prod_prod$ B_a_a_prod_prod$) B_a_a_prod_prod_option$) (declare-fun plus$q (B_b_prod_a_prod$ B_b_prod_a_prod$) B_b_prod_a_prod_option$) (declare-fun plus$r (B_b_prod_b_prod$ B_b_prod_b_prod$) B_b_prod_b_prod_option$) (declare-fun plus$s (B_a_prod_a_prod$ B_a_prod_a_prod$) B_a_prod_a_prod_option$) (declare-fun plus$t (B_a_prod_b_prod$ B_a_prod_b_prod$) B_a_prod_b_prod_option$) (declare-fun plus$u (A_a_prod_a_prod$ A_a_prod_a_prod$) A_a_prod_a_prod_option$) (declare-fun snd$aa (A_a_a_b_b_prod_prod_prod_prod$) A_a_b_b_prod_prod_prod$) (declare-fun snd$ab (A_a_a_b_a_prod_prod_prod_prod$) A_a_b_a_prod_prod_prod$) (declare-fun snd$ac (A_a_a_a_a_prod_prod_prod_prod$) A_a_a_a_prod_prod_prod$) (declare-fun snd$ad (A_a_a_b_a_b_prod_prod_prod_prod_prod$) A_a_b_a_b_prod_prod_prod_prod$) (declare-fun some$a (B_a_prod$) B_a_prod_option$) (declare-fun some$b (B_b_prod$) B_b_prod_option$) (declare-fun some$c (A_b_prod$) A_b_prod_option$) (declare-fun some$d (A_b_prod_a_prod$) A_b_prod_a_prod_option$) (declare-fun some$e (A_b_prod_b_prod$) A_b_prod_b_prod_option$) (declare-fun some$f (A_a_b_prod_prod$) A_a_b_prod_prod_option$) (declare-fun some$g (B_a_b_prod_prod$) B_a_b_prod_prod_option$) (declare-fun some$h (A_b_prod_a_b_prod_prod$) A_b_prod_a_b_prod_prod_option$) (declare-fun some$i (A_b_b_prod_prod$) A_b_b_prod_prod_option$) (declare-fun some$j (A_b_a_prod_prod$) A_b_a_prod_prod_option$) (declare-fun some$k (A_a_a_prod_prod$) A_a_a_prod_prod_option$) (declare-fun some$l (B_b_b_prod_prod$) B_b_b_prod_prod_option$) (declare-fun some$m (B_b_a_prod_prod$) B_b_a_prod_prod_option$) (declare-fun some$n (B_a_a_prod_prod$) B_a_a_prod_prod_option$) (declare-fun some$o (B_b_prod_a_prod$) B_b_prod_a_prod_option$) (declare-fun some$p (B_b_prod_b_prod$) B_b_prod_b_prod_option$) (declare-fun some$q (B_a_prod_a_prod$) B_a_prod_a_prod_option$) (declare-fun some$r (B_a_prod_b_prod$) B_a_prod_b_prod_option$) (declare-fun some$s (A_a_prod_a_prod$) A_a_prod_a_prod_option$) (declare-fun some$t (A$) A_option$) (declare-fun some$u (B$) B_option$) (declare-fun some$v (A_b_a_b_prod_prod_prod$) A_b_a_b_prod_prod_prod_option$) (declare-fun some$w (A_a_a_b_prod_prod_prod$) A_a_a_b_prod_prod_prod_option$) (declare-fun some$x (A_a_b_b_prod_prod_prod$) A_a_b_b_prod_prod_prod_option$) (declare-fun some$y (A_a_b_a_prod_prod_prod$) A_a_b_a_prod_prod_prod_option$) (declare-fun some$z (A_a_a_a_prod_prod_prod$) A_a_a_a_prod_prod_prod_option$) (declare-fun none$aa () A_a_b_a_b_prod_prod_prod_prod_option$) (declare-fun none$ab () A_a_a_a_b_prod_prod_prod_prod_option$) (declare-fun none$ac () A_a_a_b_b_prod_prod_prod_prod_option$) (declare-fun none$ad () A_a_a_b_a_prod_prod_prod_prod_option$) (declare-fun pair$aa (A$ A_a_b_b_prod_prod_prod$) A_a_a_b_b_prod_prod_prod_prod$) (declare-fun pair$ab (A$ A_a_b_a_prod_prod_prod$) A_a_a_b_a_prod_prod_prod_prod$) (declare-fun pair$ac (A$ A_a_a_a_prod_prod_prod$) A_a_a_a_a_prod_prod_prod_prod$) (declare-fun pair$ad (A$ A_a_b_a_b_prod_prod_prod_prod$) A_a_a_b_a_b_prod_prod_prod_prod_prod$) (declare-fun some$aa (A_a_b_a_b_prod_prod_prod_prod$) A_a_b_a_b_prod_prod_prod_prod_option$) (declare-fun some$ab (A_a_a_a_b_prod_prod_prod_prod$) A_a_a_a_b_prod_prod_prod_prod_option$) (declare-fun some$ac (A_a_a_b_b_prod_prod_prod_prod$) A_a_a_b_b_prod_prod_prod_prod_option$) (declare-fun some$ad (A_a_a_b_a_prod_prod_prod_prod$) A_a_a_b_a_prod_prod_prod_prod_option$) (declare-fun thesis$ () Bool) (assert (! (forall ((?v0 A_a_prod$) (?v1 A_a_prod$)) (= (plus$ ?v0 ?v1) (ite (or (= (plus$a (fst$ ?v0) (fst$ ?v1)) none$) (= (plus$a (snd$ ?v0) (snd$ ?v1)) none$)) none$a (some$ (pair$ (the$ (plus$a (fst$ ?v0) (fst$ ?v1))) (the$ (plus$a (snd$ ?v0) (snd$ ?v1)))))))) :named axiom0)) (assert (! (forall ((?v0 B_a_prod$) (?v1 B_a_prod$)) (= (plus$b ?v0 ?v1) (ite (or (= (plus$c (fst$a ?v0) (fst$a ?v1)) none$b) (= (plus$a (snd$a ?v0) (snd$a ?v1)) none$)) none$c (some$a (pair$a (the$a (plus$c (fst$a ?v0) (fst$a ?v1))) (the$ (plus$a (snd$a ?v0) (snd$a ?v1)))))))) :named axiom1)) (assert (! (forall ((?v0 B_b_prod$) (?v1 B_b_prod$)) (= (plus$d ?v0 ?v1) (ite (or (= (plus$c (fst$b ?v0) (fst$b ?v1)) none$b) (= (plus$c (snd$b ?v0) (snd$b ?v1)) none$b)) none$d (some$b (pair$b (the$a (plus$c (fst$b ?v0) (fst$b ?v1))) (the$a (plus$c (snd$b ?v0) (snd$b ?v1)))))))) :named axiom2)) (assert (! (forall ((?v0 A_b_prod$) (?v1 A_b_prod$)) (= (plus$e ?v0 ?v1) (ite (or (= (plus$a (fst$c ?v0) (fst$c ?v1)) none$) (= (plus$c (snd$c ?v0) (snd$c ?v1)) none$b)) none$e (some$c (pair$c (the$ (plus$a (fst$c ?v0) (fst$c ?v1))) (the$a (plus$c (snd$c ?v0) (snd$c ?v1)))))))) :named axiom3)) (assert (! (forall ((?v0 A_b_prod_a_prod$) (?v1 A_b_prod_a_prod$)) (= (plus$f ?v0 ?v1) (ite (or (= (plus$e (fst$d ?v0) (fst$d ?v1)) none$e) (= (plus$a (snd$d ?v0) (snd$d ?v1)) none$)) none$f (some$d (pair$d (the$b (plus$e (fst$d ?v0) (fst$d ?v1))) (the$ (plus$a (snd$d ?v0) (snd$d ?v1)))))))) :named axiom4)) (assert (! (forall ((?v0 A_b_prod_b_prod$) (?v1 A_b_prod_b_prod$)) (= (plus$g ?v0 ?v1) (ite (or (= (plus$e (fst$e ?v0) (fst$e ?v1)) none$e) (= (plus$c (snd$e ?v0) (snd$e ?v1)) none$b)) none$g (some$e (pair$e (the$b (plus$e (fst$e ?v0) (fst$e ?v1))) (the$a (plus$c (snd$e ?v0) (snd$e ?v1)))))))) :named axiom5)) (assert (! (forall ((?v0 A_a_b_prod_prod$) (?v1 A_a_b_prod_prod$)) (= (plus$h ?v0 ?v1) (ite (or (= (plus$a (fst$f ?v0) (fst$f ?v1)) none$) (= (plus$e (snd$f ?v0) (snd$f ?v1)) none$e)) none$h (some$f (pair$f (the$ (plus$a (fst$f ?v0) (fst$f ?v1))) (the$b (plus$e (snd$f ?v0) (snd$f ?v1)))))))) :named axiom6)) (assert (! (forall ((?v0 B_a_b_prod_prod$) (?v1 B_a_b_prod_prod$)) (= (plus$i ?v0 ?v1) (ite (or (= (plus$c (fst$g ?v0) (fst$g ?v1)) none$b) (= (plus$e (snd$g ?v0) (snd$g ?v1)) none$e)) none$i (some$g (pair$g (the$a (plus$c (fst$g ?v0) (fst$g ?v1))) (the$b (plus$e (snd$g ?v0) (snd$g ?v1)))))))) :named axiom7)) (assert (! (forall ((?v0 A_b_prod_a_b_prod_prod$) (?v1 A_b_prod_a_b_prod_prod$)) (= (plus$j ?v0 ?v1) (ite (or (= (plus$e (fst$h ?v0) (fst$h ?v1)) none$e) (= (plus$e (snd$h ?v0) (snd$h ?v1)) none$e)) none$j (some$h (pair$h (the$b (plus$e (fst$h ?v0) (fst$h ?v1))) (the$b (plus$e (snd$h ?v0) (snd$h ?v1)))))))) :named axiom8)) (assert (! (forall ((?v0 A_b_b_prod_prod$) (?v1 A_b_b_prod_prod$)) (= (plus$k ?v0 ?v1) (ite (or (= (plus$a (fst$i ?v0) (fst$i ?v1)) none$) (= (plus$d (snd$i ?v0) (snd$i ?v1)) none$d)) none$k (some$i (pair$i (the$ (plus$a (fst$i ?v0) (fst$i ?v1))) (the$c (plus$d (snd$i ?v0) (snd$i ?v1)))))))) :named axiom9)) (assert (! (forall ((?v0 A_b_a_prod_prod$) (?v1 A_b_a_prod_prod$)) (= (plus$l ?v0 ?v1) (ite (or (= (plus$a (fst$j ?v0) (fst$j ?v1)) none$) (= (plus$b (snd$j ?v0) (snd$j ?v1)) none$c)) none$l (some$j (pair$j (the$ (plus$a (fst$j ?v0) (fst$j ?v1))) (the$d (plus$b (snd$j ?v0) (snd$j ?v1)))))))) :named axiom10)) (assert (! (forall ((?v0 A_a_a_prod_prod$) (?v1 A_a_a_prod_prod$)) (= (plus$m ?v0 ?v1) (ite (or (= (plus$a (fst$k ?v0) (fst$k ?v1)) none$) (= (plus$ (snd$k ?v0) (snd$k ?v1)) none$a)) none$m (some$k (pair$k (the$ (plus$a (fst$k ?v0) (fst$k ?v1))) (the$e (plus$ (snd$k ?v0) (snd$k ?v1)))))))) :named axiom11)) (assert (! (forall ((?v0 B_b_b_prod_prod$) (?v1 B_b_b_prod_prod$)) (= (plus$n ?v0 ?v1) (ite (or (= (plus$c (fst$l ?v0) (fst$l ?v1)) none$b) (= (plus$d (snd$l ?v0) (snd$l ?v1)) none$d)) none$n (some$l (pair$l (the$a (plus$c (fst$l ?v0) (fst$l ?v1))) (the$c (plus$d (snd$l ?v0) (snd$l ?v1)))))))) :named axiom12)) (assert (! (forall ((?v0 B_b_a_prod_prod$) (?v1 B_b_a_prod_prod$)) (= (plus$o ?v0 ?v1) (ite (or (= (plus$c (fst$m ?v0) (fst$m ?v1)) none$b) (= (plus$b (snd$m ?v0) (snd$m ?v1)) none$c)) none$o (some$m (pair$m (the$a (plus$c (fst$m ?v0) (fst$m ?v1))) (the$d (plus$b (snd$m ?v0) (snd$m ?v1)))))))) :named axiom13)) (assert (! (forall ((?v0 B_a_a_prod_prod$) (?v1 B_a_a_prod_prod$)) (= (plus$p ?v0 ?v1) (ite (or (= (plus$c (fst$n ?v0) (fst$n ?v1)) none$b) (= (plus$ (snd$n ?v0) (snd$n ?v1)) none$a)) none$p (some$n (pair$n (the$a (plus$c (fst$n ?v0) (fst$n ?v1))) (the$e (plus$ (snd$n ?v0) (snd$n ?v1)))))))) :named axiom14)) (assert (! (forall ((?v0 B_b_prod_a_prod$) (?v1 B_b_prod_a_prod$)) (= (plus$q ?v0 ?v1) (ite (or (= (plus$d (fst$o ?v0) (fst$o ?v1)) none$d) (= (plus$a (snd$o ?v0) (snd$o ?v1)) none$)) none$q (some$o (pair$o (the$c (plus$d (fst$o ?v0) (fst$o ?v1))) (the$ (plus$a (snd$o ?v0) (snd$o ?v1)))))))) :named axiom15)) (assert (! (forall ((?v0 B_b_prod_b_prod$) (?v1 B_b_prod_b_prod$)) (= (plus$r ?v0 ?v1) (ite (or (= (plus$d (fst$p ?v0) (fst$p ?v1)) none$d) (= (plus$c (snd$p ?v0) (snd$p ?v1)) none$b)) none$r (some$p (pair$p (the$c (plus$d (fst$p ?v0) (fst$p ?v1))) (the$a (plus$c (snd$p ?v0) (snd$p ?v1)))))))) :named axiom16)) (assert (! (forall ((?v0 B_a_prod_a_prod$) (?v1 B_a_prod_a_prod$)) (= (plus$s ?v0 ?v1) (ite (or (= (plus$b (fst$q ?v0) (fst$q ?v1)) none$c) (= (plus$a (snd$q ?v0) (snd$q ?v1)) none$)) none$s (some$q (pair$q (the$d (plus$b (fst$q ?v0) (fst$q ?v1))) (the$ (plus$a (snd$q ?v0) (snd$q ?v1)))))))) :named axiom17)) (assert (! (forall ((?v0 B_a_prod_b_prod$) (?v1 B_a_prod_b_prod$)) (= (plus$t ?v0 ?v1) (ite (or (= (plus$b (fst$r ?v0) (fst$r ?v1)) none$c) (= (plus$c (snd$r ?v0) (snd$r ?v1)) none$b)) none$t (some$r (pair$r (the$d (plus$b (fst$r ?v0) (fst$r ?v1))) (the$a (plus$c (snd$r ?v0) (snd$r ?v1)))))))) :named axiom18)) (assert (! (forall ((?v0 A_a_prod_a_prod$) (?v1 A_a_prod_a_prod$)) (= (plus$u ?v0 ?v1) (ite (or (= (plus$ (fst$s ?v0) (fst$s ?v1)) none$a) (= (plus$a (snd$s ?v0) (snd$s ?v1)) none$)) none$u (some$s (pair$s (the$e (plus$ (fst$s ?v0) (fst$s ?v1))) (the$ (plus$a (snd$s ?v0) (snd$s ?v1)))))))) :named axiom19)) (assert (! (forall ((?v0 A$) (?v1 A$)) (=> (= (some$t ?v0) (plus$a ?v0 ?v1)) (exists ((?v2 A$)) (= (some$t (core$ ?v0)) (plus$a ?v1 ?v2))))) :named axiom20)) (assert (! (forall ((?v0 B$) (?v1 B$)) (=> (= (some$u ?v0) (plus$c ?v0 ?v1)) (exists ((?v2 B$)) (= (some$u (core$a ?v0)) (plus$c ?v1 ?v2))))) :named axiom21)) (assert (! (forall ((?v0 A$) (?v1 B$)) (= (fst$c (pair$c ?v0 ?v1)) ?v0)) :named axiom22)) (assert (! (forall ((?v0 B$) (?v1 B$)) (= (fst$b (pair$b ?v0 ?v1)) ?v0)) :named axiom23)) (assert (! (forall ((?v0 B$) (?v1 A$)) (= (fst$a (pair$a ?v0 ?v1)) ?v0)) :named axiom24)) (assert (! (forall ((?v0 A$) (?v1 A$)) (= (fst$ (pair$ ?v0 ?v1)) ?v0)) :named axiom25)) (assert (! (forall ((?v0 B$) (?v1 A_b_prod$)) (= (fst$g (pair$g ?v0 ?v1)) ?v0)) :named axiom26)) (assert (! (forall ((?v0 A$) (?v1 A_b_prod$)) (= (fst$f (pair$f ?v0 ?v1)) ?v0)) :named axiom27)) (assert (! (forall ((?v0 A$) (?v1 B_b_prod$)) (= (fst$i (pair$i ?v0 ?v1)) ?v0)) :named axiom28)) (assert (! (forall ((?v0 A$) (?v1 B_a_prod$)) (= (fst$j (pair$j ?v0 ?v1)) ?v0)) :named axiom29)) (assert (! (forall ((?v0 A$) (?v1 A_a_prod$)) (= (fst$k (pair$k ?v0 ?v1)) ?v0)) :named axiom30)) (assert (! (forall ((?v0 A$) (?v1 B_a_b_prod_prod$)) (= (fst$t (pair$t ?v0 ?v1)) ?v0)) :named axiom31)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_prod_prod$)) (= (fst$u (pair$u ?v0 ?v1)) ?v0)) :named axiom32)) (assert (! (forall ((?v0 A$) (?v1 A_b_b_prod_prod$)) (= (fst$v (pair$v ?v0 ?v1)) ?v0)) :named axiom33)) (assert (! (forall ((?v0 A$) (?v1 A_b_a_prod_prod$)) (= (fst$w (pair$w ?v0 ?v1)) ?v0)) :named axiom34)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_prod_prod$)) (= (fst$x (pair$x ?v0 ?v1)) ?v0)) :named axiom35)) (assert (! (forall ((?v0 A$) (?v1 A_b_a_b_prod_prod_prod$)) (= (fst$y (pair$y ?v0 ?v1)) ?v0)) :named axiom36)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_b_prod_prod_prod$)) (= (fst$z (pair$z ?v0 ?v1)) ?v0)) :named axiom37)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_b_prod_prod_prod$)) (= (fst$aa (pair$aa ?v0 ?v1)) ?v0)) :named axiom38)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_a_prod_prod_prod$)) (= (fst$ab (pair$ab ?v0 ?v1)) ?v0)) :named axiom39)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_a_prod_prod_prod$)) (= (fst$ac (pair$ac ?v0 ?v1)) ?v0)) :named axiom40)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_a_b_prod_prod_prod_prod$)) (= (fst$ad (pair$ad ?v0 ?v1)) ?v0)) :named axiom41)) (assert (! (forall ((?v0 A_option$) (?v1 A$)) (=> (= ?v0 (some$t ?v1)) (not (= ?v0 none$)))) :named axiom42)) (assert (! (forall ((?v0 B_option$) (?v1 B$)) (=> (= ?v0 (some$u ?v1)) (not (= ?v0 none$b)))) :named axiom43)) (assert (! (forall ((?v0 A_b_prod_option$) (?v1 A_b_prod$)) (=> (= ?v0 (some$c ?v1)) (not (= ?v0 none$e)))) :named axiom44)) (assert (! (forall ((?v0 B_b_prod_option$) (?v1 B_b_prod$)) (=> (= ?v0 (some$b ?v1)) (not (= ?v0 none$d)))) :named axiom45)) (assert (! (forall ((?v0 B_a_prod_option$) (?v1 B_a_prod$)) (=> (= ?v0 (some$a ?v1)) (not (= ?v0 none$c)))) :named axiom46)) (assert (! (forall ((?v0 A_a_prod_option$) (?v1 A_a_prod$)) (=> (= ?v0 (some$ ?v1)) (not (= ?v0 none$a)))) :named axiom47)) (assert (! (forall ((?v0 B_a_b_prod_prod_option$) (?v1 B_a_b_prod_prod$)) (=> (= ?v0 (some$g ?v1)) (not (= ?v0 none$i)))) :named axiom48)) (assert (! (forall ((?v0 A_a_b_prod_prod_option$) (?v1 A_a_b_prod_prod$)) (=> (= ?v0 (some$f ?v1)) (not (= ?v0 none$h)))) :named axiom49)) (assert (! (forall ((?v0 A_b_b_prod_prod_option$) (?v1 A_b_b_prod_prod$)) (=> (= ?v0 (some$i ?v1)) (not (= ?v0 none$k)))) :named axiom50)) (assert (! (forall ((?v0 A_b_a_prod_prod_option$) (?v1 A_b_a_prod_prod$)) (=> (= ?v0 (some$j ?v1)) (not (= ?v0 none$l)))) :named axiom51)) (assert (! (forall ((?v0 A_a_a_prod_prod_option$) (?v1 A_a_a_prod_prod$)) (=> (= ?v0 (some$k ?v1)) (not (= ?v0 none$m)))) :named axiom52)) (assert (! (forall ((?v0 A_b_a_b_prod_prod_prod_option$) (?v1 A_b_a_b_prod_prod_prod$)) (=> (= ?v0 (some$v ?v1)) (not (= ?v0 none$v)))) :named axiom53)) (assert (! (forall ((?v0 A_a_a_b_prod_prod_prod_option$) (?v1 A_a_a_b_prod_prod_prod$)) (=> (= ?v0 (some$w ?v1)) (not (= ?v0 none$w)))) :named axiom54)) (assert (! (forall ((?v0 A_a_b_b_prod_prod_prod_option$) (?v1 A_a_b_b_prod_prod_prod$)) (=> (= ?v0 (some$x ?v1)) (not (= ?v0 none$x)))) :named axiom55)) (assert (! (forall ((?v0 A_a_b_a_prod_prod_prod_option$) (?v1 A_a_b_a_prod_prod_prod$)) (=> (= ?v0 (some$y ?v1)) (not (= ?v0 none$y)))) :named axiom56)) (assert (! (forall ((?v0 A_a_a_a_prod_prod_prod_option$) (?v1 A_a_a_a_prod_prod_prod$)) (=> (= ?v0 (some$z ?v1)) (not (= ?v0 none$z)))) :named axiom57)) (assert (! (forall ((?v0 A_a_b_a_b_prod_prod_prod_prod_option$) (?v1 A_a_b_a_b_prod_prod_prod_prod$)) (=> (= ?v0 (some$aa ?v1)) (not (= ?v0 none$aa)))) :named axiom58)) (assert (! (forall ((?v0 A_a_a_a_b_prod_prod_prod_prod_option$) (?v1 A_a_a_a_b_prod_prod_prod_prod$)) (=> (= ?v0 (some$ab ?v1)) (not (= ?v0 none$ab)))) :named axiom59)) (assert (! (forall ((?v0 A_a_a_b_b_prod_prod_prod_prod_option$) (?v1 A_a_a_b_b_prod_prod_prod_prod$)) (=> (= ?v0 (some$ac ?v1)) (not (= ?v0 none$ac)))) :named axiom60)) (assert (! (forall ((?v0 A_a_a_b_a_prod_prod_prod_prod_option$) (?v1 A_a_a_b_a_prod_prod_prod_prod$)) (=> (= ?v0 (some$ad ?v1)) (not (= ?v0 none$ad)))) :named axiom61)) (assert (! (forall ((?v0 A_option$)) (=> (and (=> (= ?v0 none$) false) (=> (= ?v0 (some$t (the$ ?v0))) false)) false)) :named axiom62)) (assert (! (forall ((?v0 B_option$)) (=> (and (=> (= ?v0 none$b) false) (=> (= ?v0 (some$u (the$a ?v0))) false)) false)) :named axiom63)) (assert (! (forall ((?v0 A_b_prod_option$)) (=> (and (=> (= ?v0 none$e) false) (=> (= ?v0 (some$c (the$b ?v0))) false)) false)) :named axiom64)) (assert (! (forall ((?v0 B_b_prod_option$)) (=> (and (=> (= ?v0 none$d) false) (=> (= ?v0 (some$b (the$c ?v0))) false)) false)) :named axiom65)) (assert (! (forall ((?v0 B_a_prod_option$)) (=> (and (=> (= ?v0 none$c) false) (=> (= ?v0 (some$a (the$d ?v0))) false)) false)) :named axiom66)) (assert (! (forall ((?v0 A_a_prod_option$)) (=> (and (=> (= ?v0 none$a) false) (=> (= ?v0 (some$ (the$e ?v0))) false)) false)) :named axiom67)) (assert (! (forall ((?v0 B_a_b_prod_prod_option$)) (=> (and (=> (= ?v0 none$i) false) (=> (= ?v0 (some$g (the$f ?v0))) false)) false)) :named axiom68)) (assert (! (forall ((?v0 A_a_b_prod_prod_option$)) (=> (and (=> (= ?v0 none$h) false) (=> (= ?v0 (some$f (the$g ?v0))) false)) false)) :named axiom69)) (assert (! (forall ((?v0 A_b_b_prod_prod_option$)) (=> (and (=> (= ?v0 none$k) false) (=> (= ?v0 (some$i (the$h ?v0))) false)) false)) :named axiom70)) (assert (! (forall ((?v0 A_b_a_prod_prod_option$)) (=> (and (=> (= ?v0 none$l) false) (=> (= ?v0 (some$j (the$i ?v0))) false)) false)) :named axiom71)) (assert (! (forall ((?v0 A_a_a_prod_prod_option$)) (=> (and (=> (= ?v0 none$m) false) (=> (= ?v0 (some$k (the$j ?v0))) false)) false)) :named axiom72)) (assert (! (forall ((?v0 A_b_a_b_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$v) false) (=> (= ?v0 (some$v (the$k ?v0))) false)) false)) :named axiom73)) (assert (! (forall ((?v0 A_a_a_b_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$w) false) (=> (= ?v0 (some$w (the$l ?v0))) false)) false)) :named axiom74)) (assert (! (forall ((?v0 A_a_b_b_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$x) false) (=> (= ?v0 (some$x (the$m ?v0))) false)) false)) :named axiom75)) (assert (! (forall ((?v0 A_a_b_a_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$y) false) (=> (= ?v0 (some$y (the$n ?v0))) false)) false)) :named axiom76)) (assert (! (forall ((?v0 A_a_a_a_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$z) false) (=> (= ?v0 (some$z (the$o ?v0))) false)) false)) :named axiom77)) (assert (! (forall ((?v0 A_a_b_a_b_prod_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$aa) false) (=> (= ?v0 (some$aa (the$p ?v0))) false)) false)) :named axiom78)) (assert (! (forall ((?v0 A_a_a_a_b_prod_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$ab) false) (=> (= ?v0 (some$ab (the$q ?v0))) false)) false)) :named axiom79)) (assert (! (forall ((?v0 A_a_a_b_b_prod_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$ac) false) (=> (= ?v0 (some$ac (the$r ?v0))) false)) false)) :named axiom80)) (assert (! (forall ((?v0 A_a_a_b_a_prod_prod_prod_prod_option$)) (=> (and (=> (= ?v0 none$ad) false) (=> (= ?v0 (some$ad (the$s ?v0))) false)) false)) :named axiom81)) (assert (! (forall ((?v0 A$)) (= (the$ (some$t ?v0)) ?v0)) :named axiom82)) (assert (! (forall ((?v0 B$)) (= (the$a (some$u ?v0)) ?v0)) :named axiom83)) (assert (! (forall ((?v0 A_b_prod$)) (= (the$b (some$c ?v0)) ?v0)) :named axiom84)) (assert (! (forall ((?v0 B_b_prod$)) (= (the$c (some$b ?v0)) ?v0)) :named axiom85)) (assert (! (forall ((?v0 B_a_prod$)) (= (the$d (some$a ?v0)) ?v0)) :named axiom86)) (assert (! (forall ((?v0 A_a_prod$)) (= (the$e (some$ ?v0)) ?v0)) :named axiom87)) (assert (! (forall ((?v0 B_a_b_prod_prod$)) (= (the$f (some$g ?v0)) ?v0)) :named axiom88)) (assert (! (forall ((?v0 A_a_b_prod_prod$)) (= (the$g (some$f ?v0)) ?v0)) :named axiom89)) (assert (! (forall ((?v0 A_b_b_prod_prod$)) (= (the$h (some$i ?v0)) ?v0)) :named axiom90)) (assert (! (forall ((?v0 A_b_a_prod_prod$)) (= (the$i (some$j ?v0)) ?v0)) :named axiom91)) (assert (! (forall ((?v0 A_a_a_prod_prod$)) (= (the$j (some$k ?v0)) ?v0)) :named axiom92)) (assert (! (forall ((?v0 A_b_a_b_prod_prod_prod$)) (= (the$k (some$v ?v0)) ?v0)) :named axiom93)) (assert (! (forall ((?v0 A_a_a_b_prod_prod_prod$)) (= (the$l (some$w ?v0)) ?v0)) :named axiom94)) (assert (! (forall ((?v0 A_a_b_b_prod_prod_prod$)) (= (the$m (some$x ?v0)) ?v0)) :named axiom95)) (assert (! (forall ((?v0 A_a_b_a_prod_prod_prod$)) (= (the$n (some$y ?v0)) ?v0)) :named axiom96)) (assert (! (forall ((?v0 A_a_a_a_prod_prod_prod$)) (= (the$o (some$z ?v0)) ?v0)) :named axiom97)) (assert (! (forall ((?v0 A_a_b_a_b_prod_prod_prod_prod$)) (= (the$p (some$aa ?v0)) ?v0)) :named axiom98)) (assert (! (forall ((?v0 A_a_a_a_b_prod_prod_prod_prod$)) (= (the$q (some$ab ?v0)) ?v0)) :named axiom99)) (assert (! (forall ((?v0 A_a_a_b_b_prod_prod_prod_prod$)) (= (the$r (some$ac ?v0)) ?v0)) :named axiom100)) (assert (! (forall ((?v0 A_a_a_b_a_prod_prod_prod_prod$)) (= (the$s (some$ad ?v0)) ?v0)) :named axiom101)) (assert (! (forall ((?v0 A$) (?v1 B$)) (= (snd$c (pair$c ?v0 ?v1)) ?v1)) :named axiom102)) (assert (! (forall ((?v0 B$) (?v1 B$)) (= (snd$b (pair$b ?v0 ?v1)) ?v1)) :named axiom103)) (assert (! (forall ((?v0 B$) (?v1 A$)) (= (snd$a (pair$a ?v0 ?v1)) ?v1)) :named axiom104)) (assert (! (forall ((?v0 A$) (?v1 A$)) (= (snd$ (pair$ ?v0 ?v1)) ?v1)) :named axiom105)) (assert (! (forall ((?v0 B$) (?v1 A_b_prod$)) (= (snd$g (pair$g ?v0 ?v1)) ?v1)) :named axiom106)) (assert (! (forall ((?v0 A$) (?v1 A_b_prod$)) (= (snd$f (pair$f ?v0 ?v1)) ?v1)) :named axiom107)) (assert (! (forall ((?v0 A$) (?v1 B_b_prod$)) (= (snd$i (pair$i ?v0 ?v1)) ?v1)) :named axiom108)) (assert (! (forall ((?v0 A$) (?v1 B_a_prod$)) (= (snd$j (pair$j ?v0 ?v1)) ?v1)) :named axiom109)) (assert (! (forall ((?v0 A$) (?v1 A_a_prod$)) (= (snd$k (pair$k ?v0 ?v1)) ?v1)) :named axiom110)) (assert (! (forall ((?v0 A$) (?v1 B_a_b_prod_prod$)) (= (snd$t (pair$t ?v0 ?v1)) ?v1)) :named axiom111)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_prod_prod$)) (= (snd$u (pair$u ?v0 ?v1)) ?v1)) :named axiom112)) (assert (! (forall ((?v0 A$) (?v1 A_b_b_prod_prod$)) (= (snd$v (pair$v ?v0 ?v1)) ?v1)) :named axiom113)) (assert (! (forall ((?v0 A$) (?v1 A_b_a_prod_prod$)) (= (snd$w (pair$w ?v0 ?v1)) ?v1)) :named axiom114)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_prod_prod$)) (= (snd$x (pair$x ?v0 ?v1)) ?v1)) :named axiom115)) (assert (! (forall ((?v0 A$) (?v1 A_b_a_b_prod_prod_prod$)) (= (snd$y (pair$y ?v0 ?v1)) ?v1)) :named axiom116)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_b_prod_prod_prod$)) (= (snd$z (pair$z ?v0 ?v1)) ?v1)) :named axiom117)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_b_prod_prod_prod$)) (= (snd$aa (pair$aa ?v0 ?v1)) ?v1)) :named axiom118)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_a_prod_prod_prod$)) (= (snd$ab (pair$ab ?v0 ?v1)) ?v1)) :named axiom119)) (assert (! (forall ((?v0 A$) (?v1 A_a_a_a_prod_prod_prod$)) (= (snd$ac (pair$ac ?v0 ?v1)) ?v1)) :named axiom120)) (assert (! (forall ((?v0 A$) (?v1 A_a_b_a_b_prod_prod_prod_prod$)) (= (snd$ad (pair$ad ?v0 ?v1)) ?v1)) :named axiom121)) (assert (! (= (some$c x$) (plus$e x$ c$)) :named axiom122)) (assert (! (not (=> (forall ((?v0 A$) (?v1 B$)) (=> (and (= (some$t (core$ (fst$c x$))) (plus$a (fst$c c$) ?v0)) (= (some$u (core$a (snd$c x$))) (plus$c (snd$c c$) ?v1))) thesis$)) thesis$)) :named axiom123)) (check-sat) (get-proof) SMT: Invoking SMT solver "verit" ... SMT: Solver: SMT: Result: SMT: Time: 0.847s Solver verit: Solver "verit" failed -- enable tracing using the "smt_trace" option for details