; @origtpdbfilename ./TRS/TRCSR/OvConsOS_complete-noand_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_complete-noand_L.xml"
(format TRS)
(fun U114 1)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun U136 1)
(fun cons 1)
(fun zeros 0)
(fun |0| 0)
(fun U101 1)
(fun U102 1)
(fun isNatKind 0)
(fun U103 1)
(fun isNatIListKind 0)
(fun U104 1)
(fun U105 1)
(fun isNat 0)
(fun U106 1)
(fun isNatIList 0)
(fun U11 1)
(fun U12 1)
(fun U111 1)
(fun U112 1)
(fun U113 1)
(fun U13 1)
(fun isNatList 0)
(fun U121 1)
(fun U122 1)
(fun nil 0)
(fun U131 1)
(fun U132 1)
(fun U133 1)
(fun U134 1)
(fun U135 1)
(fun U21 1)
(fun U22 1)
(fun U23 1)
(fun U31 1)
(fun U32 1)
(fun U33 1)
(fun U41 1)
(fun U42 1)
(fun U43 1)
(fun U44 1)
(fun U45 1)
(fun U46 1)
(fun U51 1)
(fun U52 1)
(fun U61 1)
(fun U62 1)
(fun U71 1)
(fun U81 1)
(fun U91 1)
(fun U92 1)
(fun U93 1)
(fun U94 1)
(fun U95 1)
(fun U96 1)
(fun take 2)
(rule (U114 tt) (s (length L)))
(rule (U136 tt) (cons N))
(rule zeros (cons |0|))
(rule (U101 tt) (U102 isNatKind))
(rule (U102 tt) (U103 isNatIListKind))
(rule (U103 tt) (U104 isNatIListKind))
(rule (U104 tt) (U105 isNat))
(rule (U105 tt) (U106 isNatIList))
(rule (U106 tt) tt)
(rule (U11 tt) (U12 isNatIListKind))
(rule (U111 tt) (U112 isNatIListKind))
(rule (U112 tt) (U113 isNat))
(rule (U113 tt) (U114 isNatKind))
(rule (U12 tt) (U13 isNatList))
(rule (U121 tt) (U122 isNatIListKind))
(rule (U122 tt) nil)
(rule (U13 tt) tt)
(rule (U131 tt) (U132 isNatIListKind))
(rule (U132 tt) (U133 isNat))
(rule (U133 tt) (U134 isNatKind))
(rule (U134 tt) (U135 isNat))
(rule (U135 tt) (U136 isNatKind))
(rule (U21 tt) (U22 isNatKind))
(rule (U22 tt) (U23 isNat))
(rule (U23 tt) tt)
(rule (U31 tt) (U32 isNatIListKind))
(rule (U32 tt) (U33 isNatList))
(rule (U33 tt) tt)
(rule (U41 tt) (U42 isNatKind))
(rule (U42 tt) (U43 isNatIListKind))
(rule (U43 tt) (U44 isNatIListKind))
(rule (U44 tt) (U45 isNat))
(rule (U45 tt) (U46 isNatIList))
(rule (U46 tt) tt)
(rule (U51 tt) (U52 isNatIListKind))
(rule (U52 tt) tt)
(rule (U61 tt) (U62 isNatIListKind))
(rule (U62 tt) tt)
(rule (U71 tt) tt)
(rule (U81 tt) tt)
(rule (U91 tt) (U92 isNatKind))
(rule (U92 tt) (U93 isNatIListKind))
(rule (U93 tt) (U94 isNatIListKind))
(rule (U94 tt) (U95 isNat))
(rule (U95 tt) (U96 isNatList))
(rule (U96 tt) tt)
(rule isNat tt)
(rule isNat (U11 isNatIListKind))
(rule isNat (U21 isNatKind))
(rule isNatIList (U31 isNatIListKind))
(rule isNatIList tt)
(rule isNatIList (U41 isNatKind))
(rule isNatIListKind tt)
(rule isNatIListKind (U51 isNatKind))
(rule isNatIListKind (U61 isNatKind))
(rule isNatKind tt)
(rule isNatKind (U71 isNatIListKind))
(rule isNatKind (U81 isNatKind))
(rule isNatList tt)
(rule isNatList (U91 isNatKind))
(rule isNatList (U101 isNatKind))
(rule (length nil) |0|)
(rule (length (cons N)) (U111 isNatList))
(rule (take |0| IL) (U121 isNatIList))
(rule (take (s M) (cons N)) (U131 isNatIList))