diff --git a/examples/arithmetic_example.dsp b/examples/arithmetic_example.dsp
new file mode 100644
index 0000000..916beb0
--- /dev/null
+++ b/examples/arithmetic_example.dsp
@@ -0,0 +1,9 @@
+// 初始事实：定义数字 1 和 2 存在
+Exist(Literal(1) :: Int)
+Exist(Literal(2) :: Int)
+
+// 规则：如果 X 存在，Y 存在，且 X + Y = W，则 W 也存在
+Exist(Literal(`X) :: Int), Exist(Literal(`Y) :: Int), Literal(`X) :: Int + Literal(`Y) :: Int == Literal(`W) :: Int => Exist(Literal(`W) :: Int)
+
+// 查询：数字 5 是否存在？
+Exist(Literal(5) :: Int) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_1.dsp b/examples/geometry_for_wo_tool_complex_1.dsp
new file mode 100644
index 0000000..01d5eb3
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_1.dsp
@@ -0,0 +1,97 @@
+// 初始事实
+Collinear(F, A, C)
+Collinear(F, E, B)
+Collinear(D, B, G)
+Collinear(A, G, C)
+Collinear(D, B, H)
+Collinear(I, A, D)
+Collinear(E, I, C)
+Collinear(E, J, B)
+Length(K, A) == Length(K, F)
+Length(K, F) == Length(K, J)
+Length(L, F) == Length(L, G)
+Length(L, B) == Length(L, F)
+Length(M, G) == Length(M, H)
+Length(M, C) == Length(M, G)
+Length(N, D) == Length(N, H)
+Length(N, H) == Length(N, I)
+Length(O, E) == Length(O, I)
+Length(O, I) == Length(O, J)
+Length(K, P) == Length(K, F)
+Length(L, P) == Length(L, F)
+Length(M, Q) == Length(M, G)
+Length(L, Q) == Length(L, G)
+Length(N, R) == Length(N, H)
+Length(M, R) == Length(M, H)
+Length(K, T) == Length(K, J)
+Length(O, T) == Length(O, J)
+Length(O, S) == Length(O, I)
+
+// R1: KA=KF & KF=KJ & KT=KJ => F,A,J,T 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4) => Cyclic(`P3, `P2, `P4, `P5)
+
+// R2: F,A,J,T 共圆 & KA=KF & KP=KF & KF=KJ => A,F,P,T 共圆
+Cyclic(`P1, `P2, `P3, `P4), Length(`P5, `P2) == Length(`P5, `P1), Length(`P5, `P6) == Length(`P5, `P1), Length(`P5, `P1) == Length(`P5, `P3) => Cyclic(`P2, `P1, `P6, `P4)
+
+// R3: ND=NH & NR=NH & NH=NI => D,I,R,H 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P5) => Cyclic(`P2, `P5, `P4, `P3)
+
+// R4: D,I,R,H 共圆 => ∠DHR=∠DIR
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P4, `P3) == Degree(`P1, `P2, `P3)
+
+// R5: MG=MH & MR=MH & MC=MG => H,C,R,G 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P2) => Cyclic(`P3, `P5, `P4, `P2)
+
+// R6: H,C,R,G 共圆 => ∠HGC=∠HRC
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P4, `P2) == Degree(`P1, `P3, `P2)
+
+// R7: I,A,D共线 & ∠DHR=∠DIR & D,B,H共线 & ∠HGC=∠HRC & D,B,G共线 & A,G,C共线 => ∠ACR=∠AIR
+Collinear(`P1, `P2, `P3), Degree(`P3, `P4, `P5) == Degree(`P3, `P1, `P5), Collinear(`P3, `P6, `P4), Degree(`P4, `P7, `P8) == Degree(`P4, `P5, `P8), Collinear(`P3, `P6, `P7), Collinear(`P2, `P7, `P8) => Degree(`P2, `P8, `P5) == Degree(`P2, `P1, `P5)
+
+// R8: ∠ACR=∠AIR => A,I,R,C 共圆
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P1, `P4, `P3, `P2)
+
+// R9: OE=OI & OI=OJ & OT=OJ & OS=OI => E,I,J,T 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P5, `P5)
+
+// R11: E,I,J,T 共圆 => ∠JTI=∠JEI
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P4) == Degree(`P3, `P1, `P2)
+
+// R12: F,A,J,T 共圆 => ∠AFJ=∠ATJ
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P1, `P3) == Degree(`P2, `P4, `P3)
+
+// R13: E,I,C共线 & ∠JTI=∠JEI & E,J,B共线 & ∠AFJ=∠ATJ & F,A,C共线 & F,E,B共线 => ∠CAT=∠CIT
+Collinear(`P1, `P2, `P3), Degree(`P4, `P2, `P8) == Degree(`P4, `P1, `P2), Collinear(`P1, `P4, `P6), Degree(`P7, `P5, `P4) == Degree(`P7, `P8, `P4), Collinear(`P5, `P7, `P3), Collinear(`P5, `P1, `P6) => Degree(`P3, `P7, `P8) == Degree(`P3, `P2, `P8)
+
+// R14: ∠CAT=∠CIT => A,I,T,C 共圆
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P2, `P4, `P3, `P1)
+
+// R15: A,I,R,C 共圆 & A,I,T,C 共圆 => A,C,T,R 共圆
+Cyclic(`P1, `P2, `P3, `P4), Cyclic(`P1, `P2, `P5, `P4) => Cyclic(`P1, `P4, `P5, `P3)
+
+// R16: ∠AFP=∠ATP & F,A,C共线 & ∠CAT=∠CRT => ∠CRT=∠FPT
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Collinear(`P2, `P1, `P5), Degree(`P5, `P1, `P4) == Degree(`P5, `P6, `P4) => Degree(`P5, `P6, `P4) == Degree(`P2, `P3, `P4)
+
+// R17: H,C,R,G 共圆 & MG=MH & MQ=MG & MC=MG => C,R,G,Q 共圆
+Cyclic(`P1, `P2, `P3, `P4), Length(`P5, `P4) == Length(`P5, `P1), Length(`P5, `P6) == Length(`P5, `P4), Length(`P5, `P2) == Length(`P5, `P4) => Cyclic(`P2, `P3, `P4, `P6)
+
+// R18: Q,G,C,R 共圆 => ∠QGC=∠QRC
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3)
+
+// R19: LP=LF & LF=LG & LQ=LG & LB=LF => F,Q,P,G 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P3, `P5, `P2, `P4)
+
+// R20: F,Q,P,G 共圆 => ∠FPQ=∠FGQ
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2)
+
+// R21: ∠QGC=∠QRC & A,G,C共线 & ∠FPQ=∠FGQ & F,A,C共线 => ∠FPQ=∠CRQ
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Collinear(`P6, `P2, `P3), Degree(`P5, `P7, `P1) == Degree(`P5, `P2, `P1), Collinear(`P5, `P6, `P3) => Degree(`P5, `P7, `P1) == Degree(`P3, `P4, `P1)
+
+// R22: ∠CRT=∠FPT & ∠FPQ=∠CRQ => ∠TPQ=∠TRQ
+Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P3), Degree(`P4, `P5, `P6) == Degree(`P1, `P2, `P6) => Degree(`P3, `P5, `P6) == Degree(`P3, `P2, `P6)
+
+// R23: ∠TPQ=∠TRQ => Q,P,R,T 共圆
+Degree(`P3, `P5, `P6) == Degree(`P3, `P2, `P6) => Cyclic(`P6, `P5, `P2, `P3)
+
+// 查询：A,I,T,C 是否共圆？
+Cyclic(A, I, T, C) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_10.dsp b/examples/geometry_for_wo_tool_complex_10.dsp
new file mode 100644
index 0000000..c778479
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_10.dsp
@@ -0,0 +1,68 @@
+// 初始事实
+Collinear(B, A, C)
+Collinear(G, I, E)
+Length(B, A) == Length(B, C)
+Length(D, A) == Length(D, B)
+Length(D, E) == Length(D, B)
+Length(F, B) == Length(F, C)
+Length(F, E) == Length(F, B)
+Length(F, G) == Length(F, B)
+Length(D, I) == Length(D, B)
+Perp(A, G, A, D)
+
+// R1: FB = FC & FG = FB & FE = FB ⇒ F 是 △CGE 的外心
+Length(`P1, `P5) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P4) == Length(`P1, `P5) => Circumcenter(`P1, `P2, `P3, `P4)
+
+// R2: FB = FC & FG = FB & FE = FB ⇒ G,B,E,C 共圆
+Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5)
+
+// R3: G,B,E,C 共圆 ⇒ ∠ECB = ∠EGB
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P4, `P2) == Degree(`P3, `P1, `P2)
+
+// R4: G,B,E,C 共圆 ⇒ ∠EBC = ∠EGC
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P4) == Degree(`P3, `P1, `P4)
+
+// R5: DA = DB & DI = DB & DE = DB ⇒ I,B,E,A 共圆
+Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5)
+
+// R6: I,B,E,A 共圆 ⇒ ∠IEB = ∠IAB
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2)
+
+// R7: B,A,C共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E共线 ⇒ ∠BAI = ∠ACG
+Collinear(`P1, `P2, `P3), Degree(`P4, `P1, `P3) == Degree(`P4, `P5, `P3), Degree(`P6, `P4, `P1) == Degree(`P6, `P2, `P1), Collinear(`P5, `P6, `P4) => Degree(`P1, `P2, `P6) == Degree(`P2, `P3, `P5)
+
+// R8: DA = DB & DI = DB ⇒ D 是 △ABI 的外心
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Circumcenter(`P1, `P2, `P3, `P4)
+
+// R9: D是△ABI的外心 & AG ⟂ AD ⇒ ∠BAG = ∠BIA
+Circumcenter(`P1, `P2, `P3, `P4), Perp(`P2, `P5, `P2, `P1) => Degree(`P3, `P2, `P5) == Degree(`P3, `P4, `P2)
+
+// R10: B,A,C 共线 & ∠BIA = ∠BAG  ⇒  ∠BIA = ∠CAG
+Collinear(`P1, `P2, `P3), Degree(`P1, `P4, `P2) == Degree(`P1, `P2, `P5) => Degree(`P1, `P4, `P2) == Degree(`P3, `P2, `P5)
+
+// R11: ∠BAI = ∠ACG & ∠BIA = ∠CAG  =>  AB:CG = AI:CA
+Degree(`P1, `P2, `P4) == Degree(`P2, `P3, `P5), Degree(`P1, `P4, `P2) == Degree(`P3, `P2, `P5) => Ratio(`P2, `P1, `P3, `P5) == Ratio(`P2, `P4, `P3, `P2)
+
+// R12: AB:CG = AI:CA & BA = BC  =>  BC:GC = IA:CA
+Ratio(`P2, `P1, `P3, `P5) == Ratio(`P2, `P4, `P3, `P2), Length(`P1, `P2) == Length(`P1, `P3) => Ratio(`P1, `P3, `P5, `P3) == Ratio(`P4, `P2, `P3, `P2)
+
+// R13: B,A,C 共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E 共线  =>  ∠BCG = ∠CAI
+Collinear(`P1, `P2, `P3), Degree(`P6, `P1, `P3) == Degree(`P6, `P5, `P3), Degree(`P4, `P6, `P1) == Degree(`P4, `P2, `P1), Collinear(`P5, `P4, `P6) => Degree(`P1, `P3, `P5) == Degree(`P3, `P2, `P4)
+
+// R14: BC:GC = IA:CA & ∠BCG = ∠CAI  =>  ∠CBG = ∠CIA
+Ratio(`P1, `P3, `P5, `P3) == Ratio(`P4, `P2, `P3, `P2), Degree(`P1, `P3, `P5) == Degree(`P3, `P2, `P4) => Degree(`P3, `P1, `P5) == Degree(`P3, `P4, `P2)
+
+// R15: B,A,C 共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E 共线  =>  ∠(IA-BC) = ∠GCB
+Collinear(`P1, `P2, `P3), Degree(`P6, `P1, `P3) == Degree(`P6, `P5, `P3), Degree(`P4, `P6, `P1) == Degree(`P4, `P2, `P1), Collinear(`P5, `P4, `P6) => Angle(`P4, `P2, `P1, `P3) == Degree(`P5, `P3, `P1)
+
+// R16: ∠(IA-BC) = ∠GCB  =>  IA ∥ GC
+Angle(`P4, `P2, `P1, `P3) == Degree(`P5, `P3, `P1) => Para(`P4, `P2, `P5, `P3)
+
+// R17: ∠ECB = ∠EGB & B,A,C 共线 & ∠CBG = ∠CIA & IA ∥ CG  =>  ∠ICG = ∠CEG
+Degree(`P6, `P3, `P1) == Degree(`P6, `P5, `P1), Collinear(`P1, `P2, `P3), Degree(`P3, `P1, `P5) == Degree(`P3, `P4, `P2), Para(`P4, `P2, `P5, `P3) => Degree(`P4, `P3, `P5) == Degree(`P3, `P6, `P5)
+
+// R18: F is the circumcenter of CGE & ∠ICG = ∠CEG ⇒  CF ⟂ CI
+Circumcenter(`P1, `P2, `P3, `P4), Degree(`P5, `P2, `P3) == Degree(`P2, `P4, `P3) => Perp(`P2, `P1, `P2, `P5)
+
+// 查询：CF ⟂ CI？
+Perp(C, F, C, I) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_2.dsp b/examples/geometry_for_wo_tool_complex_2.dsp
new file mode 100644
index 0000000..f05cff5
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_2.dsp
@@ -0,0 +1,45 @@
+// 初始事实
+Collinear(B, C, A)
+Collinear(B, D, F)
+Collinear(E, A, G)
+Collinear(C, G, F)
+Collinear(B, E, H)
+Collinear(C, H, F)
+Collinear(C, I, F)
+Collinear(D, I, A)
+Para(A, E, B, D)
+Para(B, E, A, D)
+Length(C, A) == Length(C, B)
+
+// R1: B,D,F 共线 & E,A,G 共线 & AE ∥ BD => DF ∥ AG
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P5, `P4, `P1, `P2) => Para(`P2, `P3, `P5, `P6)
+
+// R2: C,I,F 共线 & C,G,F 共线 => I,F,G 共线
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P2, `P3, `P4)
+
+// R3: DF ∥ AG & I,F,G 共线 & D,I,A 共线 => IF/IG = FD/GA
+Para(`P1, `P2, `P3, `P4), Collinear(`P5, `P2, `P4), Collinear(`P1, `P5, `P3) => Ratio(`P5, `P2, `P5, `P4) == Ratio(`P2, `P1, `P4, `P3)
+
+// R4: B,D,F 共线 & E,A,G 共线 & AE ∥ BD => BF ∥ AG
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P5, `P4, `P1, `P2) => Para(`P1, `P3, `P5, `P6)
+
+// R5: BF ∥ AG & B,C,A 共线 & C,G,F 共线 => CB/CA = BF/AG
+Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P5, `P3), Collinear(`P5, `P4, `P2) => Ratio(`P5, `P1, `P5, `P3) == Ratio(`P1, `P2, `P3, `P4)
+
+// R6: B,E,H 共线 & D,I,A 共线 & BE ∥ AD => BH ∥ DI
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P1, `P2, `P6, `P4) => Para(`P1, `P3, `P4, `P5)
+
+// R7: C,I,F 共线 & C,H,F 共线 => F,H,I 共线
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P3, `P4, `P2)
+
+// R8: BH ∥ DI & B,D,F 共线 & F,H,I 共线 => BF/DF = HF/IF
+Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P2, `P5, `P4, `P5)
+
+// R9: IF:IG=FD:GA & CB:CA=BF:AG & CA=CB & BF:DF=HF:IF => HF:IF=IG:IF
+Ratio(`P1, `P2, `P1, `P3) == Ratio(`P2, `P4, `P3, `P5), Ratio(`P6, `P7, `P6, `P5) == Ratio(`P7, `P2, `P5, `P3), Length(`P6, `P5) == Length(`P6, `P7), Ratio(`P7, `P2, `P4, `P2) == Ratio(`P8, `P2, `P1, `P2) => Ratio(`P8, `P2, `P1, `P2) == Ratio(`P1, `P3, `P1, `P2)
+
+// R10: HF:IF = IG:IF => HF = IG
+Ratio(`P1, `P2, `P3, `P2) == Ratio(`P3, `P4, `P3, `P2) => Length(`P1, `P2) == Length(`P3, `P4)
+
+// 查询：HF 是否等于 IG？
+Length(H, F) == Length(I, G) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_3.dsp b/examples/geometry_for_wo_tool_complex_3.dsp
new file mode 100644
index 0000000..62624e4
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_3.dsp
@@ -0,0 +1,78 @@
+// 初始事实
+Collinear(B, E, C)
+Collinear(A, D, E)
+Collinear(A, F, C)
+Collinear(B, D, F)
+Collinear(B, I, C)
+Collinear(A, G, B)
+Collinear(G, D, C)
+Collinear(A, H, C)
+Collinear(D, I, C)
+Collinear(B, J, F)
+Para(B, H, E, F)
+Para(E, I, A, B)
+Para(J, E, A, C)
+Intro(A)
+Intro(B)
+Intro(C)
+Intro(D)
+Intro(E)
+Intro(F)
+Intro(G)
+Intro(H)
+Intro(I)
+Intro(J)
+
+// R1: A,B,G 共线 & EI ∥ AB => BG ∥ EI
+Collinear(`P1, `P3, `P2), Para(`P4, `P5, `P1, `P2) => Para(`P2, `P3, `P4, `P5)
+
+// R2: D,I,C 共线 & G,D,C 共线 => C,G,I 共线
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P3) => Collinear(`P3, `P4, `P2)
+
+// R3: D,I,C 共线 & G,D,C 共线 => D,G,I 共线
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P3) => Collinear(`P1, `P4, `P2)
+
+// R4: BG ∥ EI & B,E,C 共线 & C,G,I 共线 => BC:EC = BG:IE
+Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P1, `P2, `P4, `P3)
+
+// R5: A,H,C 共线 & A,F,C 共线 => C,H,F 共线
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P3, `P2, `P4)
+
+// R6: BH ∥ EF & B,E,C 共线 & C,H,F 共线 => BC:EC = BH:EF
+Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P1, `P2, `P3, `P4)
+
+// R7: A,H,C 共线 & A,F,C 共线 & BH ∥ EF & AC ∥ EJ => ∠BHF = ∠FEJ
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3), Para(`P5, `P2, `P6, `P4), Para(`P7, `P6, `P1, `P3) => Degree(`P5, `P2, `P4) == Degree(`P4, `P6, `P7)
+
+// R8: B,D,F 共线 & A,H,C 共线 & A,F,C 共线 & B,J,F 共线 & AC ∥ EJ => ∠BFH = ∠FJE
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Collinear(`P4, `P3, `P6), Collinear(`P1, `P7, `P3), Para(`P7, `P8, `P4, `P6) => Degree(`P1, `P3, `P5) == Degree(`P3, `P7, `P8)
+
+// R9: ∠BHF = ∠FEJ & ∠BFH = ∠FJE => BH:EF = HF:JE
+Degree(`P1, `P2, `P3) == Degree(`P3, `P4, `P5), Degree(`P1, `P3, `P2) == Degree(`P3, `P5, `P4) => Ratio(`P1, `P2, `P4, `P3) == Ratio(`P2, `P3, `P5, `P4)
+
+// R10: 传递性推导
+Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P5, `P3), Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P6, `P3, `P7), Ratio(`P1, `P6, `P3, `P7) == Ratio(`P6, `P7, `P8, `P3) => Ratio(`P6, `P7, `P8, `P3) == Ratio(`P1, `P4, `P5, `P3)
+
+// R11: A,G,B 共线 & EI ∥ AB => AG ∥ EI
+Collinear(`P1, `P2, `P3), Para(`P4, `P5, `P1, `P3) => Para(`P1, `P2, `P4, `P5)
+
+// R12: AG ∥ EI & A,D,E 共线 & G,D,I 共线 => DE:AD = IE:AG
+Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P5, `P3), Collinear(`P2, `P5, `P4) => Ratio(`P5, `P3, `P1, `P5) == Ratio(`P4, `P3, `P1, `P2)
+
+// R13: A,C,F 共线 & EJ ∥ AC => JE ∥ FA
+Collinear(`P1, `P3, `P2), Para(`P4, `P5, `P1, `P2) => Para(`P4, `P5, `P3, `P1)
+
+// R14: B,J,F 共线 & B,D,F 共线 => D,J,F 共线
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P4, `P2, `P3)
+
+// R15: JE ∥ FA & A,D,E 共线 & D,J,F 共线 => DE:AD = JE:AF
+Para(`P1, `P2, `P3, `P4), Collinear(`P4, `P5, `P2), Collinear(`P5, `P1, `P3) => Ratio(`P5, `P2, `P4, `P5) == Ratio(`P1, `P2, `P4, `P3)
+
+// R16: 传递性推导
+Ratio(`P1, `P2, `P3, `P1) == Ratio(`P4, `P2, `P3, `P5), Ratio(`P1, `P2, `P3, `P1) == Ratio(`P6, `P2, `P3, `P7) => Ratio(`P6, `P2, `P3, `P7) == Ratio(`P4, `P2, `P3, `P5)
+
+// R17: 传递性推导
+Ratio(`P1, `P2, `P3, `P4) == Ratio(`P5, `P6, `P7, `P4), Ratio(`P3, `P4, `P8, `P2) == Ratio(`P7, `P4, `P8, `P6) => Ratio(`P1, `P2, `P8, `P2) == Ratio(`P5, `P6, `P8, `P6)
+
+// 查询：HF/AF = BG/AG ?
+Ratio(H, F, A, F) == Ratio(B, G, A, G) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_4.dsp b/examples/geometry_for_wo_tool_complex_4.dsp
new file mode 100644
index 0000000..ec4a568
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_4.dsp
@@ -0,0 +1,37 @@
+// 初始事实
+Collinear(A, B, E)
+Collinear(G, C, E)
+Collinear(G, A, D)
+Collinear(H, C, E)
+Perp(B, C, A, D)
+Perp(C, E, A, B)
+Length(F, A) == Length(F, C)
+Length(F, A) == Length(F, B)
+Length(F, H) == Length(F, C)
+
+// R1: G,C,E 共线 & A,B,E 共线 & H,C,E 共线 & CE ⟂ AB ⇒ ∠GEA = ∠AEH
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P3), Collinear(`P6, `P2, `P3), Perp(`P2, `P3, `P4, `P5) => Degree(`P1, `P3, `P4) == Degree(`P4, `P3, `P6)
+
+// R2: FA = FC & FH = FC & FA = FB ⇒ H,A,B,C 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P2) == Length(`P1, `P5) => Cyclic(`P4, `P2, `P5, `P3)
+
+// R3: H,A,B,C 共圆 ⇒ ∠HAB = ∠HCB
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3)
+
+// R4: G,A,D 共线 & BC ⟂ AD ⇒ CB ⟂ GA
+Collinear(`P1, `P2, `P3), Perp(`P4, `P5, `P2, `P3) => Perp(`P5, `P4, `P1, `P2)
+
+// R5: H,C,E 共线 & G,C,E 共线 & CE ⟂ AB ⇒ AB ⟂ GH
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P2, `P3), Perp(`P2, `P3, `P5, `P6) => Perp(`P5, `P6, `P4, `P1)
+
+// R6: CB ⟂ GA & AB ⟂ GH ⇒ ∠(CB-GH) = ∠GAB
+Perp(`P1, `P2, `P3, `P4), Perp(`P4, `P2, `P3, `P5) => Angle(`P1, `P2, `P3, `P5) == Degree(`P3, `P4, `P2)
+
+// R7: G,A,D共线 & A,B,E共线 & ∠HAB=∠HCB & H,C,E共线 & ∠(CB-GH)=∠GAB & G,C,E共线 ⇒ ∠GAE=∠EAH
+Collinear(`P1, `P2, `P3), Collinear(`P2, `P4, `P5), Degree(`P6, `P2, `P4) == Degree(`P6, `P7, `P4), Collinear(`P6, `P7, `P5), Angle(`P7, `P4, `P1, `P6) == Degree(`P1, `P2, `P4), Collinear(`P1, `P7, `P5) => Degree(`P1, `P2, `P5) == Degree(`P6, `P2, `P5)
+
+// R8: ∠GEA = ∠AEH & ∠GAE = ∠EAH ⇒ EG = EH
+Degree(`P1, `P2, `P3) == Degree(`P4, `P2, `P3), Degree(`P1, `P3, `P2) == Degree(`P4, `P3, `P2) => Length(`P2, `P1) == Length(`P2, `P4)
+
+// 查询：EG 是否等于 EH？
+Length(E, G) == Length(E, H) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_5.dsp b/examples/geometry_for_wo_tool_complex_5.dsp
new file mode 100644
index 0000000..42f21c4
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_5.dsp
@@ -0,0 +1,30 @@
+// 初始事实
+Collinear(D, F, C)
+Collinear(F, B, E)
+Perp(F, H, F, G)
+Length(A, C) == Length(A, B)
+Length(A, D) == Length(A, B)
+Length(A, E) == Length(A, B)
+Length(G, F) == Length(G, B)
+Length(G, D) == Length(G, F)
+
+// 规则 R1: AD=AB, AE=AB, AC=AB => D,B,E,C 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5)
+
+// 规则 R2: 四点共圆 => 圆周角相等 ∠EBD = ∠ECD
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P1) == Degree(`P3, `P4, `P1)
+
+// 规则 R3: GF=GB, GD=GF => G 是 △FBD 的外心
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2) => Circumcenter(`P1, `P2, `P3, `P4)
+
+// 规则 R4: 外心 + 垂直关系 => 弦切角性质 ∠HFB = ∠FDB
+Circumcenter(`P1, `P2, `P3, `P4), Perp(`P2, `P5, `P2, `P1) => Degree(`P5, `P2, `P3) == Degree(`P2, `P4, `P3)
+
+// 规则 R5: 综合共线与角度相等推导角度关系 ∠HFD = Angle(EC, DF)
+Collinear(`P1, `P2, `P3), Degree(`P4, `P5, `P1) == Degree(`P4, `P3, `P1), Degree(`P6, `P2, `P5) == Degree(`P2, `P1, `P5), Collinear(`P2, `P5, `P4) => Degree(`P6, `P2, `P1) == Angle(`P4, `P3, `P1, `P2)
+
+// 规则 R6: 角度相等 => FH ∥ EC
+Degree(`P1, `P2, `P3) == Angle(`P4, `P5, `P3, `P2) => Para(`P2, `P1, `P4, `P5)
+
+// 查询：FH 是否平行于 EC？
+Para(F, H, E, C) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_6.dsp b/examples/geometry_for_wo_tool_complex_6.dsp
new file mode 100644
index 0000000..3b3ef49
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_6.dsp
@@ -0,0 +1,35 @@
+// 初始事实
+Collinear(F, A, C)
+Collinear(F, B, E)
+Collinear(A, G, B)
+Collinear(G, H, E)
+Perp(E, F, A, C)
+Perp(E, G, A, B)
+Length(D, A) == Length(D, B)
+Length(D, B) == Length(D, C)
+Length(D, E) == Length(D, A)
+Length(D, H) == Length(D, E)
+
+// R1: A,G,B共线 & F,A,C共线 & EF⟂AC & EG⟂AB ⇒ ∠EGA = ∠EFA
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P5), Perp(`P6, `P4, `P1, `P5), Perp(`P6, `P2, `P1, `P3) => Degree(`P6, `P2, `P1) == Degree(`P6, `P4, `P1)
+
+// R2: ∠EGA = ∠EFA ⇒ F,A,G,E 共圆
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P4, `P3, `P2, `P1)
+
+// R3: F,A,G,E 共圆 ⇒ ∠FAE = ∠FGE
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P4) == Degree(`P1, `P3, `P4)
+
+// R4: DA=DB & DE=DA & DH=DE & DB=DC ⇒ A,C,H,E 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P3) == Length(`P1, `P6) => Cyclic(`P2, `P6, `P5, `P4)
+
+// R5: A,C,H,E 共圆 ⇒ ∠ACH = ∠AEH
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3)
+
+// R6: G,H,E共线 & ∠FAE=∠FGE & F,A,C共线 & ∠ACH=∠AEH ⇒ ∠CHG=∠FGH
+Collinear(`P1, `P2, `P3), Degree(`P4, `P5, `P3) == Degree(`P4, `P1, `P3), Collinear(`P4, `P5, `P6), Degree(`P5, `P6, `P2) == Degree(`P5, `P3, `P2) => Degree(`P6, `P2, `P1) == Degree(`P4, `P1, `P2)
+
+// R7: ∠CHG = ∠FGH ⇒ HC ∥ FG
+Degree(`P1, `P2, `P3) == Degree(`P4, `P3, `P2) => Para(`P2, `P1, `P4, `P3)
+
+// 查询：HC 是否平行于 FG？
+Para(H, C, F, G) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_7.dsp b/examples/geometry_for_wo_tool_complex_7.dsp
new file mode 100644
index 0000000..482adb5
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_7.dsp
@@ -0,0 +1,35 @@
+// 初始事实
+Para(E, D, B, C)
+Para(G, D, C, F)
+Length(A, C) == Length(A, B)
+Length(A, D) == Length(A, B)
+Length(A, E) == Length(A, B)
+Length(A, F) == Length(A, B)
+Length(A, G) == Length(A, B)
+
+// R1: AD = AB & AF = AB & AE = AB & AC = AB ⇒ F,D,E,C 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P4, `P2, `P5, `P6)
+
+// R2: AF=AB & AG=AB & AE=AB & AD=AB & AC=AB ⇒ G,E,B,C 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P4, `P5, `P3, `P7)
+
+// R3: G,E,B,C 共圆 ⇒ ∠BGE = ∠BCE
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P1, `P2) == Degree(`P3, `P4, `P2)
+
+// R4: F,D,E,C 共圆 ⇒ ∠DFC = ∠DEC
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P1, `P4) == Degree(`P2, `P3, `P4)
+
+// R5: AF=AB & AG=AB & AE=AB & AD=AB & AC=AB ⇒ G,F,D,E 共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P4, `P2, `P6, `P5)
+
+// R6: G,F,D,E 共圆 ⇒ ∠GDF = ∠GEF
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2)
+
+// R7: ∠BGE=∠BCE & ∠DFC=∠DEC & DE∥BC & ∠GDF=∠GEF & DG∥CF ⇒ ∠FEG = ∠BGE
+Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Degree(`P5, `P6, `P4) == Degree(`P5, `P3, `P4), Para(`P5, `P3, `P1, `P4), Degree(`P2, `P5, `P6) == Degree(`P2, `P3, `P6), Para(`P5, `P2, `P4, `P6) => Degree(`P6, `P3, `P2) == Degree(`P1, `P2, `P3)
+
+// R8: ∠FEG = ∠BGE ⇒ FE ∥ GB
+Degree(`P1, `P2, `P3) == Degree(`P4, `P3, `P2) => Para(`P1, `P2, `P3, `P4)
+
+// 查询：FE 是否平行于 GB？
+Para(F, E, G, B) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_8.dsp b/examples/geometry_for_wo_tool_complex_8.dsp
new file mode 100644
index 0000000..fd3a737
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_8.dsp
@@ -0,0 +1,29 @@
+// 初始事实
+Collinear(D, B, H)
+Length(C, A) == Length(C, B)
+Length(C, D) == Length(C, A)
+Length(C, F) == Length(C, A)
+Length(F, C) == Length(F, D)
+Length(C, G) == Length(C, A)
+Length(G, C) == Length(G, D)
+
+// 规则 R1: 如果 CF=CA, CG=CA, CA=CB, CE=CA, CD=CA，则 B, G, F, D 四点共圆
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P5, `P4, `P2, `P7)
+
+// 规则 R2: 四点共圆引出的圆周角相等：∠DBG = ∠DFG
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P3, `P1) == Degree(`P2, `P4, `P1)
+
+// 规则 R3: 四点共圆引出的圆周角相等：∠FGD = ∠FBD
+Cyclic(`P1, `P2, `P3, `P4) => Degree(`P4, `P1, `P2) == Degree(`P4, `P3, `P2)
+
+// 规则 R4: 通过边长相等推导：GC=GD, CG=CA, CF=CA, FC=FD => DF=DG
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P2, `P1) == Length(`P2, `P4), Length(`P2, `P5) == Length(`P2, `P4), Length(`P5, `P2) == Length(`P5, `P3) => Length(`P3, `P5) == Length(`P3, `P1)
+
+// 规则 R5: 等腰三角形推导底角相等：DF=DG => ∠DFG = ∠FGD
+Length(`P1, `P2) == Length(`P1, `P3) => Degree(`P1, `P2, `P3) == Degree(`P2, `P3, `P1)
+
+// 规则 R6: 综合共线与角度相等推导角平分关系：∠FBH = ∠HBG
+Collinear(`P1, `P2, `P3), Degree(`P1, `P2, `P4) == Degree(`P1, `P5, `P4), Degree(`P1, `P5, `P4) == Degree(`P5, `P4, `P1), Degree(`P5, `P4, `P1) == Degree(`P5, `P2, `P1) => Degree(`P5, `P2, `P3) == Degree(`P3, `P2, `P4)
+
+// 查询：∠FBH 是否等于 ∠HBG？
+Degree(F, B, H) == Degree(H, B, G) => Query()
diff --git a/examples/geometry_for_wo_tool_complex_9.dsp b/examples/geometry_for_wo_tool_complex_9.dsp
new file mode 100644
index 0000000..f8ea58a
--- /dev/null
+++ b/examples/geometry_for_wo_tool_complex_9.dsp
@@ -0,0 +1,86 @@
+// 初始事实
+Collinear(C, F, A)
+Collinear(G, B, C)
+Collinear(H, D, G)
+Collinear(E, H, C)
+Collinear(D, F, I)
+Collinear(E, C, I)
+Collinear(E, C, J)
+Collinear(E, K, C)
+Perp(F, J, C, E)
+Perp(C, E, K, G)
+Length(D, B) == Length(D, C)
+Length(D, A) == Length(D, B)
+Length(D, E) == Length(D, A)
+Length(E, A) == Length(E, B)
+Length(F, C) == Length(F, A)
+Length(G, C) == Length(G, B)
+
+// R1: DB = DC & GC = GB ⇒ BC ⟂ DG
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P3) == Length(`P4, `P2) => Perp(`P2, `P3, `P1, `P4)
+
+// R2: DB = DC & DA = DB ⇒ DA = DC
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2) => Length(`P1, `P4) == Length(`P1, `P3)
+
+// R3: DA = DC & FC = FA ⇒ AC ⟂ DF
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P3) == Length(`P4, `P2) => Perp(`P2, `P3, `P1, `P4)
+
+// R4: C,F,A共线 & D,F,I共线 & H,D,G共线 & G,B,C共线 & BC⟂DG & AC⟂DF ⇒ ∠CFI = ∠HGC
+Collinear(`P1, `P2, `P3), Collinear(`P4, `P2, `P5), Collinear(`P6, `P4, `P7), Collinear(`P7, `P8, `P1), Perp(`P8, `P1, `P4, `P7), Perp(`P3, `P1, `P4, `P2) => Degree(`P1, `P2, `P5) == Degree(`P6, `P7, `P1)
+
+// R5: DA=DB & DE=DA & DB=DC ⇒ D 是 △EBC 的外心
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Circumcenter(`P1, `P4, `P3, `P5)
+
+// R6: DA=DB & DE=DA & DB=DC ⇒ D 是 △EAC 的外心
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Circumcenter(`P1, `P4, `P2, `P5)
+
+// R7: DA=DB & DE=DA & DB=DC ⇒ DC = DE
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Length(`P1, `P5) == Length(`P1, `P4)
+
+// R8: G,B,C共线 & GC=GB ⇒ G是CB的中点
+Collinear(`P1, `P2, `P3), Length(`P1, `P3) == Length(`P1, `P2) => Midpoint(`P1, `P3, `P2)
+
+// R9: D是△EBC的外心 & G是CB的中点 ⇒ ∠DBE = ∠(DG-CE)
+Circumcenter(`P1, `P2, `P3, `P4), Midpoint(`P5, `P4, `P3) => Degree(`P1, `P3, `P2) == Angle(`P1, `P5, `P4, `P2)
+
+// R10: DA = DB & EA = EB ⇒ ∠DBE = ∠EAD
+Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P2) == Length(`P4, `P3) => Degree(`P1, `P3, `P4) == Degree(`P4, `P2, `P1)
+
+// R11: C,F,A共线 & FC=FA ⇒ F是CA的中点
+Collinear(`P1, `P2, `P3), Length(`P2, `P1) == Length(`P2, `P3) => Midpoint(`P2, `P1, `P3)
+
+// R12: D是△EAC的外心 & F是CA的中点 ⇒ ∠EAD = ∠(CE-DF)
+Circumcenter(`P1, `P2, `P3, `P4), Midpoint(`P5, `P4, `P3) => Degree(`P2, `P3, `P1) == Angle(`P4, `P2, `P1, `P5)
+
+// R13: ∠CFI=∠HGC & ∠CIF=∠GHC ⇒ IC:HC = IF:HG
+Degree(`P2, `P4, `P1) == Degree(`P3, `P5, `P2), Degree(`P2, `P1, `P4) == Degree(`P5, `P3, `P2) => Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P3, `P5)
+
+// R15: D,F,I共线 & DF⟂AC ⇒ IF⟂CA
+Collinear(`P1, `P2, `P3), Perp(`P4, `P5, `P1, `P2) => Perp(`P3, `P2, `P5, `P4)
+
+// R16: F是CA的中点 & IF⟂CA ⇒ IC = IA
+Midpoint(`P1, `P2, `P3), Perp(`P4, `P1, `P2, `P3) => Length(`P4, `P2) == Length(`P4, `P3)
+
+// R19: ∠GKH=∠IJF & ∠GHK=∠JIF ⇒ GK:FJ = GH:FI
+Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P6), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P6) => Ratio(`P1, `P2, `P6, `P5) == Ratio(`P1, `P3, `P6, `P4)
+
+// R21: DC = DE ⇒ ∠DCE = ∠CED
+Length(`P1, `P2) == Length(`P1, `P3) => Degree(`P1, `P2, `P3) == Degree(`P2, `P3, `P1)
+
+// R22: E,H,C共线 & E,C,I共线 & ∠DCE=∠CED ⇒ ∠DCH = ∠IED
+Collinear(`P1, `P2, `P3), Collinear(`P1, `P3, `P4), Degree(`P5, `P3, `P1) == Degree(`P3, `P1, `P5) => Degree(`P5, `P3, `P2) == Degree(`P4, `P1, `P5)
+
+// R23: ∠DHC=∠EID & ∠DCH=∠IED ⇒ CD:ED = CH:EI
+Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P1), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P1) => Ratio(`P3, `P1, `P4, `P1) == Ratio(`P3, `P2, `P4, `P5)
+
+// R25: E,H,C共线 & E,C,I共线 & ∠DEC=∠ECD ⇒ ∠DEH = ∠ICD
+Collinear(`P2, `P4, `P3), Collinear(`P2, `P3, `P5), Degree(`P1, `P3, `P2) == Degree(`P3, `P2, `P1) => Degree(`P1, `P2, `P4) == Degree(`P5, `P3, `P1)
+
+// R26: ∠DHE=∠CID & ∠DEH=∠ICD ⇒ ED:CD = EH:CI
+Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P1), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P1) => Ratio(`P3, `P1, `P4, `P1) == Ratio(`P3, `P2, `P4, `P5)
+
+// R27: GK:FJ = EI:EH
+Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P3, `P5), Length(`P1, `P2) == Length(`P1, `P6), Ratio(`P5, `P7, `P4, `P8) == Ratio(`P5, `P3, `P4, `P1), Ratio(`P2, `P9, `P10, `P9) == Ratio(`P2, `P3, `P10, `P1), Length(`P9, `P2) == Length(`P9, `P10), Ratio(`P10, `P9, `P2, `P9) == Ratio(`P10, `P3, `P2, `P1) => Ratio(`P5, `P7, `P4, `P8) == Ratio(`P10, `P1, `P10, `P3)
+
+// 查询：GK:FJ 是否等于 EI:EH
+Ratio(G, K, F, J) == Ratio(E, I, E, H) => Query()
diff --git a/examples/main.py b/examples/main.py
new file mode 100644
index 0000000..6f44048
--- /dev/null
+++ b/examples/main.py
@@ -0,0 +1,200 @@
+import sys
+import asyncio
+import tempfile
+import pathlib
+from sqlalchemy import select
+from apyds import Rule, List, Variable, Term, Item
+from apyds_bnf import parse, unparse
+from ddss.orm import initialize_database, insert_or_ignore, Facts, Ideas
+from ddss.chain import main as ds
+from ddss.egg import main as egg
+from ddss.utility import str_rule_get_str_idea
+
+
+def extract_binary_from_term(term: Term) -> tuple[Item, Term, Term] | None:
+    t = term.term
+    if isinstance(t, List) and len(t) == 4 and str(t[0]) == "binary":
+        if isinstance(t[1].term, Item):
+            return t[1].term, t[2], t[3]
+    return None
+
+
+def extract_equality_from_rule(rule: Rule) -> tuple[Term, Term] | None:
+    if len(rule) != 0:
+        return None
+    res = extract_binary_from_term(rule.conclusion)
+    if res and str(res[0]) == "==":
+        return res[1], res[2]
+    return None
+
+
+def extract_literal_from_term(term: Term) -> tuple[Item | Variable, Item] | None:
+    res = extract_binary_from_term(term)
+    if res and str(res[0]) == "::":
+        lhs, rhs = res[1].term, res[2].term
+        if isinstance(lhs, List) and isinstance(rhs, Item):
+            if len(lhs) == 3 and str(lhs[0]) == "function" and str(lhs[1]) == "Literal":
+                if isinstance(lhs[2].term, Item | Variable):
+                    return lhs[2].term, rhs
+    return None
+
+
+async def arithmetic(session):
+    ops = {
+        "+": lambda a, b: a + b,
+        "-": lambda a, b: a - b,
+        "*": lambda a, b: a * b,
+        "/": lambda a, b: a / b if b != 0 else None,
+    }
+    types_map = {"Int": int, "Float": float}
+
+    try:
+        max_idea = -1
+
+        while True:
+            async with session() as sess:
+                pool: list[Rule] = []
+                for i in await sess.scalars(select(Ideas).where(Ideas.id > max_idea)):
+                    max_idea = max(max_idea, i.id)
+                    pool.append(Rule(i.data))
+
+                for rule in pool:
+                    if eq := extract_equality_from_rule(rule):
+                        lhs_term, rhs_term = eq
+
+                        for side in [("lhs", lhs_term, rhs_term), ("rhs", rhs_term, lhs_term)]:
+                            label, bin_expr, val_expr = side
+                            if bin_res := extract_binary_from_term(bin_expr):
+                                op_str = str(bin_res[0])
+                                if (
+                                    (func := ops.get(op_str))
+                                    and (v1_lit := extract_literal_from_term(bin_res[1]))
+                                    and (v2_lit := extract_literal_from_term(bin_res[2]))
+                                    and (v_res_lit := extract_literal_from_term(val_expr))
+                                ):
+                                    val1, type1 = v1_lit
+                                    val2, type2 = v2_lit
+                                    val_res, type_res = v_res_lit
+                                    val1_str = str(val1)
+                                    val2_str = str(val2)
+                                    type_str = str(type_res)
+
+                                    if (
+                                        isinstance(val1, Item)
+                                        and isinstance(val2, Item)
+                                        and isinstance(val_res, Variable)
+                                        and type1 == type2 == type_res
+                                        and (conv := types_map.get(type_str))
+                                    ):
+                                        a = conv(val1_str)
+                                        b = conv(val2_str)
+                                        res = func(a, b)
+
+                                        if res is None:
+                                            continue
+
+                                        v1_str = f"(binary :: (function Literal {val1_str}) {type_str})"
+                                        v2_str = f"(binary :: (function Literal {val2_str}) {type_str})"
+                                        res_str = f"(binary :: (function Literal {res}) {type_str})"
+
+                                        if label == "lhs":
+                                            fact = f"(binary == (binary {op_str} {v1_str} {v2_str}) {res_str})"
+                                        else:
+                                            fact = f"(binary == {res_str} (binary {op_str} {v1_str} {v2_str}))"
+
+                                        await insert_or_ignore(sess, Facts, str(Rule(fact)))
+
+                await sess.commit()
+
+            await asyncio.sleep(0)
+    except asyncio.CancelledError:
+        pass
+
+
+async def output(session):
+    try:
+        max_fact = -1
+        max_idea = -1
+
+        while True:
+            async with session() as sess:
+                for i in await sess.scalars(select(Ideas).where(Ideas.id > max_idea)):
+                    max_idea = max(max_idea, i.id)
+                    print("idea:", unparse(i.data))
+                for i in await sess.scalars(select(Facts).where(Facts.id > max_fact)):
+                    max_fact = max(max_fact, i.id)
+                    print("fact:", unparse(i.data))
+
+                    rule = Rule(i.data)
+                    if len(rule) == 0:
+                        term = rule.conclusion.term
+                        if isinstance(term, List):
+                            if len(term) >= 2 and str(term[0]) == "function" and str(term[1]) == "Query":
+                                print("status:", unparse(i.data))
+                                raise asyncio.CancelledError()
+                await sess.commit()
+
+            await asyncio.sleep(0)
+    except asyncio.CancelledError:
+        pass
+
+
+async def load(session, file_name):
+    async with session() as sess:
+        for line in open(file_name, "rt", encoding="utf-8"):
+            data = line.strip()
+            if data == "":
+                continue
+            if data.startswith("//"):
+                continue
+
+            try:
+                ds = parse(data)
+            except Exception as e:
+                print(f"error: {e}")
+                continue
+
+            await insert_or_ignore(sess, Facts, ds)
+            if idea := str_rule_get_str_idea(ds):
+                await insert_or_ignore(sess, Ideas, idea)
+        await sess.commit()
+
+
+async def run(addr: str, file_name: str) -> None:
+    engine, session = await initialize_database(addr)
+
+    try:
+        await load(session, file_name)
+        tasks = [
+            asyncio.create_task(ds(session)),
+            asyncio.create_task(egg(session)),
+            asyncio.create_task(output(session)),
+            asyncio.create_task(arithmetic(session)),
+        ]
+        done, pending = await asyncio.wait(
+            tasks,
+            return_when=asyncio.FIRST_COMPLETED,
+        )
+        for task in pending:
+            task.cancel()
+        for task in pending:
+            try:
+                await task
+            except asyncio.CancelledError:
+                pass
+    except asyncio.CancelledError:
+        pass
+    finally:
+        await engine.dispose()
+
+
+def main() -> None:
+    tmpdir = tempfile.TemporaryDirectory(prefix="ddss-")
+    path = pathlib.Path(tmpdir.name) / "ddss.db"
+    addr = f"sqlite+aiosqlite:///{path.as_posix()}"
+    file_name = sys.argv[1]
+    asyncio.run(run(addr, file_name))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/examples/main.ts b/examples/main.ts
new file mode 100644
index 0000000..c0afb86
--- /dev/null
+++ b/examples/main.ts
@@ -0,0 +1,241 @@
+import * as fs from "node:fs";
+import * as path from "node:path";
+import * as os from "node:os";
+import { Op, type Sequelize } from "sequelize";
+import { Rule, List, Variable, type Term, Item } from "atsds";
+import { parse, unparse } from "atsds-bnf";
+import { Fact, Idea, initializeDatabase, insertOrIgnore } from "../ddss/orm.ts";
+import { main as ds } from "../ddss/chain.ts";
+import { main as egg } from "../ddss/egg.ts";
+import { strRuleGetStrIdea } from "../ddss/utility.ts";
+
+function extractBinaryFromTerm(term: Term): [Item, Term, Term] | null {
+    const t = term.term();
+    if (t instanceof List && t.length() === 4 && t.getitem(0).toString() === "binary") {
+        const opTerm = t.getitem(1).term();
+        if (opTerm instanceof Item) {
+            return [opTerm, t.getitem(2), t.getitem(3)];
+        }
+    }
+    return null;
+}
+
+function extractEqualityFromRule(rule: Rule): [Term, Term] | null {
+    if (rule.length() !== 0) {
+        return null;
+    }
+    const res = extractBinaryFromTerm(rule.conclusion());
+    if (res && res[0].toString() === "==") {
+        return [res[1], res[2]];
+    }
+    return null;
+}
+
+function extractLiteralFromTerm(term: Term): [Item | Variable, Item] | null {
+    const res = extractBinaryFromTerm(term);
+    if (res && res[0].toString() === "::") {
+        const lhs = res[1].term();
+        const rhs = res[2].term();
+        if (lhs instanceof List && rhs instanceof Item) {
+            if (
+                lhs.length() === 3 &&
+                lhs.getitem(0).toString() === "function" &&
+                lhs.getitem(1).toString() === "Literal"
+            ) {
+                const val = lhs.getitem(2).term();
+                if (val instanceof Item || val instanceof Variable) {
+                    return [val, rhs];
+                }
+            }
+        }
+    }
+    return null;
+}
+
+async function arithmetic() {
+    const ops: Record<string, (a: number, b: number) => number | null> = {
+        "+": (a, b) => a + b,
+        "-": (a, b) => a - b,
+        "*": (a, b) => a * b,
+        "/": (a, b) => (b !== 0 ? a / b : null),
+    };
+
+    const typesMap: Record<string, (v: string) => number> = {
+        Int: (v) => Number.parseInt(v, 10),
+        Float: (v) => Number.parseFloat(v),
+    };
+
+    let maxIdea = -1;
+
+    while (true) {
+        const newIdeas = await Idea.findAll({
+            where: { id: { [Op.gt]: maxIdea } },
+        });
+
+        for (const idea of newIdeas) {
+            maxIdea = Math.max(maxIdea, idea.id);
+            const rule = new Rule(idea.data);
+            const eq = extractEqualityFromRule(rule);
+            if (!eq) continue;
+
+            const [lhsTerm, rhsTerm] = eq;
+            const sides: Array<["lhs" | "rhs", Term, Term]> = [
+                ["lhs", lhsTerm, rhsTerm],
+                ["rhs", rhsTerm, lhsTerm],
+            ];
+
+            for (const [label, binExpr, valExpr] of sides) {
+                const binRes = extractBinaryFromTerm(binExpr);
+                if (binRes) {
+                    const opStr = binRes[0].toString();
+                    const func = ops[opStr];
+                    if (func) {
+                        const v1Lit = extractLiteralFromTerm(binRes[1]);
+                        const v2Lit = extractLiteralFromTerm(binRes[2]);
+                        const vResLit = extractLiteralFromTerm(valExpr);
+
+                        if (v1Lit && v2Lit && vResLit) {
+                            const [val1, type1] = v1Lit;
+                            const [val2, type2] = v2Lit;
+                            const [valRes, typeRes] = vResLit;
+
+                            const val1Str = val1.toString();
+                            const val2Str = val2.toString();
+                            const typeStr = typeRes.toString();
+
+                            if (
+                                val1 instanceof Item &&
+                                val2 instanceof Item &&
+                                valRes instanceof Variable &&
+                                type1.toString() === type2.toString() &&
+                                type1.toString() === typeRes.toString()
+                            ) {
+                                const conv = typesMap[typeStr];
+                                if (conv) {
+                                    const a = conv(val1Str);
+                                    const b = conv(val2Str);
+                                    const res = func(a, b);
+
+                                    if (res !== null) {
+                                        const v1Str = `(binary :: (function Literal ${val1Str}) ${typeStr})`;
+                                        const v2Str = `(binary :: (function Literal ${val2Str}) ${typeStr})`;
+                                        const resStr = `(binary :: (function Literal ${res}) ${typeStr})`;
+
+                                        let factStr: string;
+                                        if (label === "lhs") {
+                                            factStr = `(binary == (binary ${opStr} ${v1Str} ${v2Str}) ${resStr})`;
+                                        } else {
+                                            factStr = `(binary == ${resStr} (binary ${opStr} ${v1Str} ${v2Str}))`;
+                                        }
+
+                                        await insertOrIgnore(Fact, new Rule(factStr).toString());
+                                    }
+                                }
+                            }
+                        }
+                    }
+                }
+            }
+        }
+
+        await new Promise((resolve) => setTimeout(resolve, 0));
+    }
+}
+
+async function output(abortController: AbortController) {
+    let maxFact = -1;
+    let maxIdea = -1;
+
+    while (true) {
+        const newIdeas = await Idea.findAll({
+            where: { id: { [Op.gt]: maxIdea } },
+        });
+        for (const idea of newIdeas) {
+            maxIdea = Math.max(maxIdea, idea.id);
+            console.log("idea:", unparse(idea.data));
+        }
+
+        const newFacts = await Fact.findAll({
+            where: { id: { [Op.gt]: maxFact } },
+        });
+        for (const fact of newFacts) {
+            maxFact = Math.max(maxFact, fact.id);
+            console.log("fact:", unparse(fact.data));
+
+            const rule = new Rule(fact.data);
+            if (rule.length() === 0) {
+                const term = rule.conclusion().term();
+                if (
+                    term instanceof List &&
+                    term.length() >= 2 &&
+                    term.getitem(0).toString() === "function" &&
+                    term.getitem(1).toString() === "Query"
+                ) {
+                    console.log("status:", unparse(fact.data));
+                    abortController.abort();
+                    return;
+                }
+            }
+        }
+
+        await new Promise((resolve) => setTimeout(resolve, 0));
+    }
+}
+
+async function load(fileName: string) {
+    const content = fs.readFileSync(fileName, "utf-8");
+    const lines = content.split("\n");
+
+    for (const line of lines) {
+        const data = line.trim();
+        if (data === "" || data.startsWith("//")) continue;
+
+        try {
+            const dsStr = parse(data);
+            await insertOrIgnore(Fact, dsStr);
+            const idea = strRuleGetStrIdea(dsStr);
+            if (idea) {
+                await insertOrIgnore(Idea, idea);
+            }
+        } catch (e) {
+            console.error(`error: ${(e as Error).message}`);
+        }
+    }
+}
+
+async function run(addr: string, fileName: string) {
+    const sequelize = await initializeDatabase(addr);
+    const abortController = new AbortController();
+
+    try {
+        await load(fileName);
+        await Promise.race([
+            ds(sequelize),
+            egg(sequelize),
+            output(abortController),
+            arithmetic(),
+            new Promise((_, reject) => {
+                abortController.signal.addEventListener("abort", () => reject(new Error("Abort")));
+            }),
+        ]).catch((e) => {
+            if (e.message !== "Abort") throw e;
+        });
+    } finally {
+        await sequelize.close();
+    }
+}
+
+function main() {
+    const fileName = process.argv[2];
+    if (!fileName) {
+        console.error("Please provide a dsp file");
+        process.exit(1);
+    }
+    const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), "ddss-"));
+    const dbPath = path.join(tmpDir, "ddss.sqlite");
+    const addr = `sqlite://${dbPath}`;
+
+    run(addr, fileName).catch(console.error);
+}
+
+main();
diff --git a/examples/relationship.dsp b/examples/relationship.dsp
new file mode 100644
index 0000000..6a0ea35
--- /dev/null
+++ b/examples/relationship.dsp
@@ -0,0 +1,17 @@
+// 初始事实
+Father(Alice, Bob)   // Alice 是 Bob 的父亲（此处沿用代码逻辑）
+Brother(Bob, Carie)  // Bob 是 Carie 的兄弟
+Brother(Mark, Dick)  // Mark 是 Dick 的兄弟
+Father(Mark, Bob)    // Mark 是 Bob 的父亲
+
+// 规则 R1: 如果 X 是 Y 的父亲且 Y 是 Z 的兄弟，则 X 是 Z 的叔伯
+Father(`X, `Y), Brother(`Y, `Z) => Uncle(`X, `Z)
+
+// 规则 R2: 如果 X 和 Y 都是 Z 的父亲，则 X 和 Y 是同胞
+Father(`X, `Z), Father(`Y, `Z) => Sibling(`X, `Y)
+
+// 规则 R3: 如果 X 是 Z 的叔伯且 X 与 Y 是同胞，则 Y 也是 Z 的叔伯
+Uncle(`X, `Z), Sibling(`X, `Y) => Uncle(`Y, `Z)
+
+// 查询：Mark 是谁的叔伯？
+Uncle(Mark, `X) => Query(`X)
diff --git a/examples/relationship_quick_start.dsp b/examples/relationship_quick_start.dsp
new file mode 100644
index 0000000..a3a4064
--- /dev/null
+++ b/examples/relationship_quick_start.dsp
@@ -0,0 +1,9 @@
+// 初始事实：定义父母关系
+Parent(Alice, Bob)
+Parent(Bob, Carie)
+
+// 规则：如果 X 是 Y 的父母，且 Y 是 Z 的父母，则 X 是 Z 的祖父母
+Parent(`X, `Y), Parent(`Y, `Z) => GrandParent(`X, `Z)
+
+// 查询：寻找 Alice 的所有孙辈
+GrandParent(Alice, `X) => Query(`X)