ltNat : Nat Nat -> Bool
       n1 : -> Nat
       n2 : -> Nat
       n3 : -> Nat
       n4 : -> Nat
       n5 : -> Nat
       n6 : -> Nat
       n7 : -> Nat
       n8 : -> Nat
       n9 : -> Nat
       n10 : -> Nat
       n11 : -> Nat
       n12 : -> Nat
       n13 : -> Nat
       n14 : -> Nat
       n15 : -> Nat
       n16 : -> Nat
       n17 : -> Nat
       n18 : -> Nat
       n19 : -> Nat
       n20 : -> Nat
       n21 : -> Nat
       n22 : -> Nat
       n254 : -> Nat
       n256 : -> Nat
       n4100 : -> Nat
     VARS
       N N' : Nat
     RULES
       addNat (N, zero) -> N
       addNat (N, succ (N')) -> addNat (succ (N), N')

       multNat (N, zero) -> zero
       multNat (N, succ (N')) -> addNat (N, multNat (N, N'))

       eqNat (zero, zero) -> true
       eqNat (zero, succ (N')) -> false
       eqNat (succ (N), zero) -> false
       eqNat (succ (N), succ (N')) -> eqNat (N, N')

       ltNat (zero, zero) -> false
       ltNat (zero, succ (N')) -> true
       ltNat (succ (N'), zero) -> false
       ltNat (succ (N), succ (N')) -> ltNat (N, N')

       n1 -> succ (zero)
       n2 -> succ 