; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete_iGM.xml"
(format TRS)
(fun active 1)
(fun U101 3)
(fun tt 0)
(fun mark 1)
(fun U102 2)
(fun isNatural 1)
(fun U103 1)
(fun isLNat 1)
(fun U11 3)
(fun snd 1)
(fun splitAt 2)
(fun U111 2)
(fun U112 1)
(fun U121 2)
(fun U122 1)
(fun U131 3)
(fun U132 2)
(fun U133 1)
(fun U141 3)
(fun U142 2)
(fun U143 1)
(fun U151 3)
(fun U152 2)
(fun U153 1)
(fun U161 2)
(fun cons 2)
(fun natsFrom 1)
(fun s 1)
(fun U171 3)
(fun head 1)
(fun afterNth 2)
(fun U181 2)
(fun U191 2)
(fun pair 2)
(fun nil 0)
(fun U201 4)
(fun U202 2)
(fun U21 2)
(fun U211 2)
(fun U221 3)
(fun fst 1)
(fun U31 2)
(fun U41 3)
(fun U42 2)
(fun U43 1)
(fun U51 3)
(fun U52 2)
(fun U53 1)
(fun U61 2)
(fun U62 1)
(fun isPLNat 1)
(fun U71 2)
(fun U72 1)
(fun U81 2)
(fun U82 1)
(fun U91 2)
(fun U92 1)
(fun and 2)
(fun isNaturalKind 1)
(fun isLNatKind 1)
(fun isPLNatKind 1)
(fun tail 1)
(fun take 2)
(fun |0| 0)
(fun sel 2)
(rule (active (U101 tt V1 V2)) (mark (U102 (isNatural V1) V2)))
(rule (active (U102 tt V2)) (mark (U103 (isLNat V2))))
(rule (active (U103 tt)) (mark tt))
(rule (active (U11 tt N XS)) (mark (snd (splitAt N XS))))
(rule (active (U111 tt V1)) (mark (U112 (isLNat V1))))
(rule (active (U112 tt)) (mark tt))
(rule (active (U121 tt V1)) (mark (U122 (isNatural V1))))
(rule (active (U122 tt)) (mark tt))
(rule (active (U131 tt V1 V2)) (mark (U132 (isNatural V1) V2)))
(rule (active (U132 tt V2)) (mark (U133 (isLNat V2))))
(rule (active (U133 tt)) (mark tt))
(rule (active (U141 tt V1 V2)) (mark (U142 (isLNat V1) V2)))
(rule (active (U142 tt V2)) (mark (U143 (isLNat V2))))
(rule (active (U143 tt)) (mark tt))
(rule (active (U151 tt V1 V2)) (mark (U152 (isNatural V1) V2)))
(rule (active (U152 tt V2)) (mark (U153 (isLNat V2))))
(rule (active (U153 tt)) (mark tt))
(rule (active (U161 tt N)) (mark (cons N (natsFrom (s N)))))
(rule (active (U171 tt N XS)) (mark (head (afterNth N XS))))
(rule (active (U181 tt Y)) (mark Y))
(rule (active (U191 tt XS)) (mark (pair nil XS)))
(rule (active (U201 tt N X XS)) (mark (U202 (splitAt N XS) X)))
(rule (active (U202 (pair YS ZS) X)) (mark (pair (cons X YS) ZS)))
(rule (active (U21 tt X)) (mark X))
(rule (active (U211 tt XS)) (mark XS))
(rule (active (U221 tt N XS)) (mark (fst (splitAt N XS))))
(rule (active (U31 tt N)) (mark N))
(rule (active (U41 tt V1 V2)) (mark (U42 (isNatural V1) V2)))
(rule (active (U42 tt V2)) (mark (U43 (isLNat V2))))
(rule (active (U43 tt)) (mark tt))
(rule (active (U51 tt V1 V2)) (mark (U52 (isNatural V1) V2)))
(rule (active (U52 tt V2)) (mark (U53 (isLNat V2))))
(rule (active (U53 tt)) (mark tt))
(rule (active (U61 tt V1)) (mark (U62 (isPLNat V1))))
(rule (active (U62 tt)) (mark tt))
(rule (active (U71 tt V1)) (mark (U72 (isNatural V1))))
(rule (active (U72 tt)) (mark tt))
(rule (active (U81 tt V1)) (mark (U82 (isPLNat V1))))
(rule (active (U82 tt)) (mark tt))
(rule (active (U91 tt V1)) (mark (U92 (isLNat V1))))
(rule (active (U92 tt)) (mark tt))
(rule (active (afterNth N XS)) (mark (U11 (and (and (isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS)))
(rule (active (and tt X)) (mark X))
(rule (active (fst (pair X Y))) (mark (U21 (and (and (isLNat X) (isLNatKind X)) (and (isLNat Y) (isLNatKind Y))) X)))
(rule (active (head (cons N XS))) (mark (U31 (and (and (isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N)))
(rule (active (isLNat nil)) (mark tt))
(rule (active (isLNat (afterNth V1 V2))) (mark (U41 (and (isNaturalKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isLNat (cons V1 V2))) (mark (U51 (and (isNaturalKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isLNat (fst V1))) (mark (U61 (isPLNatKind V1) V1)))
(rule (active (isLNat (natsFrom V1))) (mark (U71 (isNaturalKind V1) V1)))
(rule (active (isLNat (snd V1))) (mark (U81 (isPLNatKind V1) V1)))
(rule (active (isLNat (tail V1))) (mark (U91 (isLNatKind V1) V1)))
(rule (active (isLNat (take V1 V2))) (mark (U101 (and (isNaturalKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isLNatKind nil)) (mark tt))
(rule (active (isLNatKind (afterNth V1 V2))) (mark (and (isNaturalKind V1) (isLNatKind V2))))
(rule (active (isLNatKind (cons V1 V2))) (mark (and (isNaturalKind V1) (isLNatKind V2))))
(rule (active (isLNatKind (fst V1))) (mark (isPLNatKind V1)))
(rule (active (isLNatKind (natsFrom V1))) (mark (isNaturalKind V1)))
(rule (active (isLNatKind (snd V1))) (mark (isPLNatKind V1)))
(rule (active (isLNatKind (tail V1))) (mark (isLNatKind V1)))
(rule (active (isLNatKind (take V1 V2))) (mark (and (isNaturalKind V1) (isLNatKind V2))))
(rule (active (isNatural |0|)) (mark tt))
(rule (active (isNatural (head V1))) (mark (U111 (isLNatKind V1) V1)))
(rule (active (isNatural (s V1))) (mark (U121 (isNaturalKind V1) V1)))
(rule (active (isNatural (sel V1 V2))) (mark (U131 (and (isNaturalKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isNaturalKind |0|)) (mark tt))
(rule (active (isNaturalKind (head V1))) (mark (isLNatKind V1)))
(rule (active (isNaturalKind (s V1))) (mark (isNaturalKind V1)))
(rule (active (isNaturalKind (sel V1 V2))) (mark (and (isNaturalKind V1) (isLNatKind V2))))
(rule (active (isPLNat (pair V1 V2))) (mark (U141 (and (isLNatKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isPLNat (splitAt V1 V2))) (mark (U151 (and (isNaturalKind V1) (isLNatKind V2)) V1 V2)))
(rule (active (isPLNatKind (pair V1 V2))) (mark (and (isLNatKind V1) (isLNatKind V2))))
(rule (active (isPLNatKind (splitAt V1 V2))) (mark (and (isNaturalKind V1) (isLNatKind V2))))
(rule (active (natsFrom N)) (mark (U161 (and (isNatural N) (isNaturalKind N)) N)))
(rule (active (sel N XS)) (mark (U171 (and (and (isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS)))
(rule (active (snd (pair X Y))) (mark (U181 (and (and (isLNat X) (isLNatKind X)) (and (isLNat Y) (isLNatKind Y))) Y)))
(rule (active (splitAt |0| XS)) (mark (U191 (and (isLNat XS) (isLNatKind XS)) XS)))
(rule (active (splitAt (s N) (cons X XS))) (mark (U201 (and (and (isNatural N) (isNaturalKind N)) (and (and (isNatural X) (isNaturalKind X)) (and (isLNat XS) (isLNatKind XS)))) N X XS)))
(rule (active (tail (cons N XS))) (mark (U211 (and (and (isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) XS)))
(rule (active (take N XS)) (mark (U221 (and (and (isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS)))
(rule (mark (U101 X1 X2 X3)) (active (U101 (mark X1) X2 X3)))
(rule (mark tt) (active tt))
(rule (mark (U102 X1 X2)) (active (U102 (mark X1) X2)))
(rule (mark (isNatural X)) (active (isNatural X)))
(rule (mark (U103 X)) (active (U103 (mark X))))
(rule (mark (isLNat X)) (active (isLNat X)))
(rule (mark (U11 X1 X2 X3)) (active (U11 (mark X1) X2 X3)))
(rule (mark (snd X)) (active (snd (mark X))))
(rule (mark (splitAt X1 X2)) (active (splitAt (mark X1) (mark X2))))
(rule (mark (U111 X1 X2)) (active (U111 (mark X1) X2)))
(rule (mark (U112 X)) (active (U112 (mark X))))
(rule (mark (U121 X1 X2)) (active (U121 (mark X1) X2)))
(rule (mark (U122 X)) (active (U122 (mark X))))
(rule (mark (U131 X1 X2 X3)) (active (U131 (mark X1) X2 X3)))
(rule (mark (U132 X1 X2)) (active (U132 (mark X1) X2)))
(rule (mark (U133 X)) (active (U133 (mark X))))
(rule (mark (U141 X1 X2 X3)) (active (U141 (mark X1) X2 X3)))
(rule (mark (U142 X1 X2)) (active (U142 (mark X1) X2)))
(rule (mark (U143 X)) (active (U143 (mark X))))
(rule (mark (U151 X1 X2 X3)) (active (U151 (mark X1) X2 X3)))
(rule (mark (U152 X1 X2)) (active (U152 (mark X1) X2)))
(rule (mark (U153 X)) (active (U153 (mark X))))
(rule (mark (U161 X1 X2)) (active (U161 (mark X1) X2)))
(rule (mark (cons X1 X2)) (active (cons (mark X1) X2)))
(rule (mark (natsFrom X)) (active (natsFrom (mark X))))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (U171 X1 X2 X3)) (active (U171 (mark X1) X2 X3)))
(rule (mark (head X)) (active (head (mark X))))
(rule (mark (afterNth X1 X2)) (active (afterNth (mark X1) (mark X2))))
(rule (mark (U181 X1 X2)) (active (U181 (mark X1) X2)))
(rule (mark (U191 X1 X2)) (active (U191 (mark X1) X2)))
(rule (mark (pair X1 X2)) (active (pair (mark X1) (mark X2))))
(rule (mark nil) (active nil))
(rule (mark (U201 X1 X2 X3 X4)) (active (U201 (mark X1) X2 X3 X4)))
(rule (mark (U202 X1 X2)) (active (U202 (mark X1) X2)))
(rule (mark (U21 X1 X2)) (active (U21 (mark X1) X2)))
(rule (mark (U211 X1 X2)) (active (U211 (mark X1) X2)))
(rule (mark (U221 X1 X2 X3)) (active (U221 (mark X1) X2 X3)))
(rule (mark (fst X)) (active (fst (mark X))))
(rule (mark (U31 X1 X2)) (active (U31 (mark X1) X2)))
(rule (mark (U41 X1 X2 X3)) (active (U41 (mark X1) X2 X3)))
(rule (mark (U42 X1 X2)) (active (U42 (mark X1) X2)))
(rule (mark (U43 X)) (active (U43 (mark X))))
(rule (mark (U51 X1 X2 X3)) (active (U51 (mark X1) X2 X3)))
(rule (mark (U52 X1 X2)) (active (U52 (mark X1) X2)))
(rule (mark (U53 X)) (active (U53 (mark X))))
(rule (mark (U61 X1 X2)) (active (U61 (mark X1) X2)))
(rule (mark (U62 X)) (active (U62 (mark X))))
(rule (mark (isPLNat X)) (active (isPLNat X)))
(rule (mark (U71 X1 X2)) (active (U71 (mark X1) X2)))
(rule (mark (U72 X)) (active (U72 (mark X))))
(rule (mark (U81 X1 X2)) (active (U81 (mark X1) X2)))
(rule (mark (U82 X)) (active (U82 (mark X))))
(rule (mark (U91 X1 X2)) (active (U91 (mark X1) X2)))
(rule (mark (U92 X)) (active (U92 (mark X))))
(rule (mark (and X1 X2)) (active (and (mark X1) X2)))
(rule (mark (isNaturalKind X)) (active (isNaturalKind X)))
(rule (mark (isLNatKind X)) (active (isLNatKind X)))
(rule (mark (isPLNatKind X)) (active (isPLNatKind X)))
(rule (mark (tail X)) (active (tail (mark X))))
(rule (mark (take X1 X2)) (active (take (mark X1) (mark X2))))
(rule (mark |0|) (active |0|))
(rule (mark (sel X1 X2)) (active (sel (mark X1) (mark X2))))
(rule (U101 (mark X1) X2 X3) (U101 X1 X2 X3))
(rule (U101 X1 (mark X2) X3) (U101 X1 X2 X3))
(rule (U101 X1 X2 (mark X3)) (U101 X1 X2 X3))
(rule (U101 (active X1) X2 X3) (U101 X1 X2 X3))
(rule (U101 X1 (active X2) X3) (U101 X1 X2 X3))
(rule (U101 X1 X2 (active X3)) (U101 X1 X2 X3))
(rule (U102 (mark X1) X2) (U102 X1 X2))
(rule (U102 X1 (mark X2)) (U102 X1 X2))
(rule (U102 (active X1) X2) (U102 X1 X2))
(rule (U102 X1 (active X2)) (U102 X1 X2))
(rule (isNatural (mark X)) (isNatural X))
(rule (isNatural (active X)) (isNatural X))
(rule (U103 (mark X)) (U103 X))
(rule (U103 (active X)) (U103 X))
(rule (isLNat (mark X)) (isLNat X))
(rule (isLNat (active X)) (isLNat X))
(rule (U11 (mark X1) X2 X3) (U11 X1 X2 X3))
(rule (U11 X1 (mark X2) X3) (U11 X1 X2 X3))
(rule (U11 X1 X2 (mark X3)) (U11 X1 X2 X3))
(rule (U11 (active X1) X2 X3) (U11 X1 X2 X3))
(rule (U11 X1 (active X2) X3) (U11 X1 X2 X3))
(rule (U11 X1 X2 (active X3)) (U11 X1 X2 X3))
(rule (snd (mark X)) (snd X))
(rule (snd (active X)) (snd X))
(rule (splitAt (mark X1) X2) (splitAt X1 X2))
(rule (splitAt X1 (mark X2)) (splitAt X1 X2))
(rule (splitAt (active X1) X2) (splitAt X1 X2))
(rule (splitAt X1 (active X2)) (splitAt X1 X2))
(rule (U111 (mark X1) X2) (U111 X1 X2))
(rule (U111 X1 (mark X2)) (U111 X1 X2))
(rule (U111 (active X1) X2) (U111 X1 X2))
(rule (U111 X1 (active X2)) (U111 X1 X2))
(rule (U112 (mark X)) (U112 X))
(rule (U112 (active X)) (U112 X))
(rule (U121 (mark X1) X2) (U121 X1 X2))
(rule (U121 X1 (mark X2)) (U121 X1 X2))
(rule (U121 (active X1) X2) (U121 X1 X2))
(rule (U121 X1 (active X2)) (U121 X1 X2))
(rule (U122 (mark X)) (U122 X))
(rule (U122 (active X)) (U122 X))
(rule (U131 (mark X1) X2 X3) (U131 X1 X2 X3))
(rule (U131 X1 (mark X2) X3) (U131 X1 X2 X3))
(rule (U131 X1 X2 (mark X3)) (U131 X1 X2 X3))
(rule (U131 (active X1) X2 X3) (U131 X1 X2 X3))
(rule (U131 X1 (active X2) X3) (U131 X1 X2 X3))
(rule (U131 X1 X2 (active X3)) (U131 X1 X2 X3))
(rule (U132 (mark X1) X2) (U132 X1 X2))
(rule (U132 X1 (mark X2)) (U132 X1 X2))
(rule (U132 (active X1) X2) (U132 X1 X2))
(rule (U132 X1 (active X2)) (U132 X1 X2))
(rule (U133 (mark X)) (U133 X))
(rule (U133 (active X)) (U133 X))
(rule (U141 (mark X1) X2 X3) (U141 X1 X2 X3))
(rule (U141 X1 (mark X2) X3) (U141 X1 X2 X3))
(rule (U141 X1 X2 (mark X3)) (U141 X1 X2 X3))
(rule (U141 (active X1) X2 X3) (U141 X1 X2 X3))
(rule (U141 X1 (active X2) X3) (U141 X1 X2 X3))
(rule (U141 X1 X2 (active X3)) (U141 X1 X2 X3))
(rule (U142 (mark X1) X2) (U142 X1 X2))
(rule (U142 X1 (mark X2)) (U142 X1 X2))
(rule (U142 (active X1) X2) (U142 X1 X2))
(rule (U142 X1 (active X2)) (U142 X1 X2))
(rule (U143 (mark X)) (U143 X))
(rule (U143 (active X)) (U143 X))
(rule (U151 (mark X1) X2 X3) (U151 X1 X2 X3))
(rule (U151 X1 (mark X2) X3) (U151 X1 X2 X3))
(rule (U151 X1 X2 (mark X3)) (U151 X1 X2 X3))
(rule (U151 (active X1) X2 X3) (U151 X1 X2 X3))
(rule (U151 X1 (active X2) X3) (U151 X1 X2 X3))
(rule (U151 X1 X2 (active X3)) (U151 X1 X2 X3))
(rule (U152 (mark X1) X2) (U152 X1 X2))
(rule (U152 X1 (mark X2)) (U152 X1 X2))
(rule (U152 (active X1) X2) (U152 X1 X2))
(rule (U152 X1 (active X2)) (U152 X1 X2))
(rule (U153 (mark X)) (U153 X))
(rule (U153 (active X)) (U153 X))
(rule (U161 (mark X1) X2) (U161 X1 X2))
(rule (U161 X1 (mark X2)) (U161 X1 X2))
(rule (U161 (active X1) X2) (U161 X1 X2))
(rule (U161 X1 (active X2)) (U161 X1 X2))
(rule (cons (mark X1) X2) (cons X1 X2))
(rule (cons X1 (mark X2)) (cons X1 X2))
(rule (cons (active X1) X2) (cons X1 X2))
(rule (cons X1 (active X2)) (cons X1 X2))
(rule (natsFrom (mark X)) (natsFrom X))
(rule (natsFrom (active X)) (natsFrom X))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (U171 (mark X1) X2 X3) (U171 X1 X2 X3))
(rule (U171 X1 (mark X2) X3) (U171 X1 X2 X3))
(rule (U171 X1 X2 (mark X3)) (U171 X1 X2 X3))
(rule (U171 (active X1) X2 X3) (U171 X1 X2 X3))
(rule (U171 X1 (active X2) X3) (U171 X1 X2 X3))
(rule (U171 X1 X2 (active X3)) (U171 X1 X2 X3))
(rule (head (mark X)) (head X))
(rule (head (active X)) (head X))
(rule (afterNth (mark X1) X2) (afterNth X1 X2))
(rule (afterNth X1 (mark X2)) (afterNth X1 X2))
(rule (afterNth (active X1) X2) (afterNth X1 X2))
(rule (afterNth X1 (active X2)) (afterNth X1 X2))
(rule (U181 (mark X1) X2) (U181 X1 X2))
(rule (U181 X1 (mark X2)) (U181 X1 X2))
(rule (U181 (active X1) X2) (U181 X1 X2))
(rule (U181 X1 (active X2)) (U181 X1 X2))
(rule (U191 (mark X1) X2) (U191 X1 X2))
(rule (U191 X1 (mark X2)) (U191 X1 X2))
(rule (U191 (active X1) X2) (U191 X1 X2))
(rule (U191 X1 (active X2)) (U191 X1 X2))
(rule (pair (mark X1) X2) (pair X1 X2))
(rule (pair X1 (mark X2)) (pair X1 X2))
(rule (pair (active X1) X2) (pair X1 X2))
(rule (pair X1 (active X2)) (pair X1 X2))
(rule (U201 (mark X1) X2 X3 X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 (mark X2) X3 X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 X2 (mark X3) X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 X2 X3 (mark X4)) (U201 X1 X2 X3 X4))
(rule (U201 (active X1) X2 X3 X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 (active X2) X3 X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 X2 (active X3) X4) (U201 X1 X2 X3 X4))
(rule (U201 X1 X2 X3 (active X4)) (U201 X1 X2 X3 X4))
(rule (U202 (mark X1) X2) (U202 X1 X2))
(rule (U202 X1 (mark X2)) (U202 X1 X2))
(rule (U202 (active X1) X2) (U202 X1 X2))
(rule (U202 X1 (active X2)) (U202 X1 X2))
(rule (U21 (mark X1) X2) (U21 X1 X2))
(rule (U21 X1 (mark X2)) (U21 X1 X2))
(rule (U21 (active X1) X2) (U21 X1 X2))
(rule (U21 X1 (active X2)) (U21 X1 X2))
(rule (U211 (mark X1) X2) (U211 X1 X2))
(rule (U211 X1 (mark X2)) (U211 X1 X2))
(rule (U211 (active X1) X2) (U211 X1 X2))
(rule (U211 X1 (active X2)) (U211 X1 X2))
(rule (U221 (mark X1) X2 X3) (U221 X1 X2 X3))
(rule (U221 X1 (mark X2) X3) (U221 X1 X2 X3))
(rule (U221 X1 X2 (mark X3)) (U221 X1 X2 X3))
(rule (U221 (active X1) X2 X3) (U221 X1 X2 X3))
(rule (U221 X1 (active X2) X3) (U221 X1 X2 X3))
(rule (U221 X1 X2 (active X3)) (U221 X1 X2 X3))
(rule (fst (mark X)) (fst X))
(rule (fst (active X)) (fst X))
(rule (U31 (mark X1) X2) (U31 X1 X2))
(rule (U31 X1 (mark X2)) (U31 X1 X2))
(rule (U31 (active X1) X2) (U31 X1 X2))
(rule (U31 X1 (active X2)) (U31 X1 X2))
(rule (U41 (mark X1) X2 X3) (U41 X1 X2 X3))
(rule (U41 X1 (mark X2) X3) (U41 X1 X2 X3))
(rule (U41 X1 X2 (mark X3)) (U41 X1 X2 X3))
(rule (U41 (active X1) X2 X3) (U41 X1 X2 X3))
(rule (U41 X1 (active X2) X3) (U41 X1 X2 X3))
(rule (U41 X1 X2 (active X3)) (U41 X1 X2 X3))
(rule (U42 (mark X1) X2) (U42 X1 X2))
(rule (U42 X1 (mark X2)) (U42 X1 X2))
(rule (U42 (active X1) X2) (U42 X1 X2))
(rule (U42 X1 (active X2)) (U42 X1 X2))
(rule (U43 (mark X)) (U43 X))
(rule (U43 (active X)) (U43 X))
(rule (U51 (mark X1) X2 X3) (U51 X1 X2 X3))
(rule (U51 X1 (mark X2) X3) (U51 X1 X2 X3))
(rule (U51 X1 X2 (mark X3)) (U51 X1 X2 X3))
(rule (U51 (active X1) X2 X3) (U51 X1 X2 X3))
(rule (U51 X1 (active X2) X3) (U51 X1 X2 X3))
(rule (U51 X1 X2 (active X3)) (U51 X1 X2 X3))
(rule (U52 (mark X1) X2) (U52 X1 X2))
(rule (U52 X1 (mark X2)) (U52 X1 X2))
(rule (U52 (active X1) X2) (U52 X1 X2))
(rule (U52 X1 (active X2)) (U52 X1 X2))
(rule (U53 (mark X)) (U53 X))
(rule (U53 (active X)) (U53 X))
(rule (U61 (mark X1) X2) (U61 X1 X2))
(rule (U61 X1 (mark X2)) (U61 X1 X2))
(rule (U61 (active X1) X2) (U61 X1 X2))
(rule (U61 X1 (active X2)) (U61 X1 X2))
(rule (U62 (mark X)) (U62 X))
(rule (U62 (active X)) (U62 X))
(rule (isPLNat (mark X)) (isPLNat X))
(rule (isPLNat (active X)) (isPLNat X))
(rule (U71 (mark X1) X2) (U71 X1 X2))
(rule (U71 X1 (mark X2)) (U71 X1 X2))
(rule (U71 (active X1) X2) (U71 X1 X2))
(rule (U71 X1 (active X2)) (U71 X1 X2))
(rule (U72 (mark X)) (U72 X))
(rule (U72 (active X)) (U72 X))
(rule (U81 (mark X1) X2) (U81 X1 X2))
(rule (U81 X1 (mark X2)) (U81 X1 X2))
(rule (U81 (active X1) X2) (U81 X1 X2))
(rule (U81 X1 (active X2)) (U81 X1 X2))
(rule (U82 (mark X)) (U82 X))
(rule (U82 (active X)) (U82 X))
(rule (U91 (mark X1) X2) (U91 X1 X2))
(rule (U91 X1 (mark X2)) (U91 X1 X2))
(rule (U91 (active X1) X2) (U91 X1 X2))
(rule (U91 X1 (active X2)) (U91 X1 X2))
(rule (U92 (mark X)) (U92 X))
(rule (U92 (active X)) (U92 X))
(rule (and (mark X1) X2) (and X1 X2))
(rule (and X1 (mark X2)) (and X1 X2))
(rule (and (active X1) X2) (and X1 X2))
(rule (and X1 (active X2)) (and X1 X2))
(rule (isNaturalKind (mark X)) (isNaturalKind X))
(rule (isNaturalKind (active X)) (isNaturalKind X))
(rule (isLNatKind (mark X)) (isLNatKind X))
(rule (isLNatKind (active X)) (isLNatKind X))
(rule (isPLNatKind (mark X)) (isPLNatKind X))
(rule (isPLNatKind (active X)) (isPLNatKind X))
(rule (tail (mark X)) (tail X))
(rule (tail (active X)) (tail X))
(rule (take (mark X1) X2) (take X1 X2))
(rule (take X1 (mark X2)) (take X1 X2))
(rule (take (active X1) X2) (take X1 X2))
(rule (take X1 (active X2)) (take X1 X2))
(rule (sel (mark X1) X2) (sel X1 X2))
(rule (sel X1 (mark X2)) (sel X1 X2))
(rule (sel (active X1) X2) (sel X1 X2))
(rule (sel X1 (active X2)) (sel X1 X2))