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