Как сделать ограниченное индуктивное доказательство некоторой общей теоремы в теории групп

Question

Я пытаюсь доказательство по индукции, что:

Для группы G, то FORALL (х, у, г)/((у^п) х (г^п) = х) => (Order (G) = п)

Я использую ограниченный индукцию со следующим кодом

;; Derive order n from a single axiom for groups order n. 
;; ((Y^n)X(Z^n) = X)=> (order(G) = n) for 1 < n < 23 
(declare-sort S) 
(declare-fun e() S) 
(declare-fun mult (S S) S) 
(declare-fun power (S Int) S) 
(assert (forall ((x S)) (= e (power x 0)))) 
(assert (forall ((x S)) (= x (power x 1)))) 
(assert (forall ((n Int) (x S)) 
     (=> (and (>= n 2) (<= n 22)) 
      (= (power x n) (mult x (power x (- n 1))))))) 
(assert (= (mult e e) e))  
(check-sat) 
(define-fun p ((x S) (y S) (z S) (w S) (n Int)) Bool 
      (=> (= (mult (power y n) (mult x (power z n))) 
      x) (= (power w n) e)) ) 
(assert (forall ((x S) (y S) (z S) (w S)) (p x y z w 2))) 
(assert (forall ((x S) (y S) (z S) (w S) (n Int)) 
     (=> (and (> n 2) (<= n 22)) 
      (= (p x y z w n) (p x y z w (- n 1)))))) 

;; Bounded inductive proof. 
(assert (not (forall ((x S) (y S) (z S) (w S)) (p x y z w 22)))) 
(check-sat) 

, а выход ожидаемый:

sat 
unsat 

Выполнить этот код онлайн here

Я доказав теорему для 2 < < п 23. Когда я пытаюсь с 2 < < н 24 я получить «тайм-аут».

Вопрос в следующем: как выйти за пределы n = 22 в этом доказательстве?

Answer 1

Используя (set-option :qi-eager-threshold 70000), предложенный Леонардо де Мура, Z3 может доказать теорему до n = 60000 (локально, онлайн до n = 10000).