YES Problem: b(b(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(b(x)) -> b(b(x)) b(c(x)) -> c(c(x)) b(a(x)) -> b(b(x)) b(a(x)) -> b(a(x)) c(b(x)) -> c(a(x)) c(c(x)) -> b(a(x)) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 12 c(b(a(x73))) <-0|0[]- c(c(c(x73))) -0|[]-> b(a(c(x73))) b(b(a(x74))) <-0|0[]- b(c(c(x74))) -3|[]-> c(c(c(x74))) c(c(a(x75))) <-1|0[]- c(c(b(x75))) -0|[]-> b(a(b(x75))) b(c(a(x76))) <-1|0[]- b(c(b(x76))) -3|[]-> c(c(b(x76))) c(b(b(x77))) <-2|0[]- c(b(a(x77))) -1|[]-> c(a(a(x77))) b(b(b(x78))) <-2|0[]- b(b(a(x78))) -5|[]-> a(b(a(x78))) c(c(c(x79))) <-3|0[]- c(b(c(x79))) -1|[]-> c(a(c(x79))) b(c(c(x80))) <-3|0[]- b(b(c(x80))) -5|[]-> a(b(c(x80))) c(c(c(x81))) <-4|0[]- c(c(a(x81))) -0|[]-> b(a(a(x81))) b(c(c(x82))) <-4|0[]- b(c(a(x82))) -3|[]-> c(c(a(x82))) c(a(b(x83))) <-5|0[]- c(b(b(x83))) -1|[]-> c(a(b(x83))) b(a(b(x84))) <-5|0[]- b(b(b(x84))) -5|[]-> a(b(b(x84))) Redundant Rules Transformation: c(c(x)) -> b(a(x)) c(b(x)) -> c(a(x)) b(a(x)) -> b(b(x)) b(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) b(b(x)) -> a(b(x)) c(c(x)) -> b(b(x)) c(b(x)) -> c(c(x)) b(a(x)) -> a(b(x)) b(c(x)) -> b(a(x)) c(a(x)) -> b(a(x)) Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 49 b(b(a(x327))) <-0|0[]- b(c(a(x327))) -1|[]-> b(a(a(x327))) c(b(a(x328))) <-0|0[]- c(c(a(x328))) -4|[]-> b(b(a(x328))) b(a(x)) <-0|[]- c(a(x)) -6|[]-> c(c(x)) b(b(a(x330))) <-0|0[]- b(c(a(x330))) -7|[]-> c(c(a(x330))) c(b(a(x331))) <-0|0[]- c(c(a(x331))) -10|[]-> b(a(a(x331))) c(b(a(x332))) <-1|0[]- c(b(c(x332))) -3|[]-> c(c(c(x332))) b(b(a(x333))) <-1|0[]- b(b(c(x333))) -5|[]-> a(b(c(x333))) b(a(x)) <-1|[]- b(c(x)) -7|[]-> c(c(x)) c(b(a(x335))) <-1|0[]- c(b(c(x335))) -9|[]-> c(a(c(x335))) c(a(b(x336))) <-2|0[]- c(b(a(x336))) -3|[]-> c(c(a(x336))) b(a(b(x337))) <-2|0[]- b(b(a(x337))) -5|[]-> a(b(a(x337))) a(b(x)) <-2|[]- b(a(x)) -8|[]-> b(b(x)) c(a(b(x339))) <-2|0[]- c(b(a(x339))) -9|[]-> c(a(a(x339))) b(c(c(x340))) <-3|0[]- b(c(b(x340))) -1|[]-> b(a(b(x340))) c(c(c(x341))) <-3|0[]- c(c(b(x341))) -4|[]-> b(b(b(x341))) b(c(c(x342))) <-3|0[]- b(c(b(x342))) -7|[]-> c(c(b(x342))) c(c(x)) <-3|[]- c(b(x)) -9|[]-> c(a(x)) c(c(c(x344))) <-3|0[]- c(c(b(x344))) -10|[]-> b(a(b(x344))) b(b(b(x345))) <-4|0[]- b(c(c(x345))) -1|[]-> b(a(c(x345))) c(b(b(x346))) <-4|0[]- c(c(c(x346))) -4|[]-> b(b(c(x346))) b(b(b(x347))) <-4|0[]- b(c(c(x347))) -7|[]-> c(c(c(x347))) b(b(x)) <-4|[]- c(c(x)) -10|[]-> b(a(x)) c(b(b(x349))) <-4|0[]- c(c(c(x349))) -10|[]-> b(a(c(x349))) c(a(b(x350))) <-5|0[]- c(b(b(x350))) -3|[]-> c(c(b(x350))) b(a(b(x351))) <-5|0[]- b(b(b(x351))) -5|[]-> a(b(b(x351))) c(a(b(x352))) <-5|0[]- c(b(b(x352))) -9|[]-> c(a(b(x352))) c(c(x)) <-6|[]- c(a(x)) -0|[]-> b(a(x)) b(c(c(x354))) <-6|0[]- b(c(a(x354))) -1|[]-> b(a(a(x354))) c(c(c(x355))) <-6|0[]- c(c(a(x355))) -4|[]-> b(b(a(x355))) b(c(c(x356))) <-6|0[]- b(c(a(x356))) -7|[]-> c(c(a(x356))) c(c(c(x357))) <-6|0[]- c(c(a(x357))) -10|[]-> b(a(a(x357))) c(c(x)) <-7|[]- b(c(x)) -1|[]-> b(a(x)) c(c(c(x359))) <-7|0[]- c(b(c(x359))) -3|[]-> c(c(c(x359))) b(c(c(x360))) <-7|0[]- b(b(c(x360))) -5|[]-> a(b(c(x360))) c(c(c(x361))) <-7|0[]- c(b(c(x361))) -9|[]-> c(a(c(x361))) b(b(x)) <-8|[]- b(a(x)) -2|[]-> a(b(x)) c(b(b(x363))) <-8|0[]- c(b(a(x363))) -3|[]-> c(c(a(x363))) b(b(b(x364))) <-8|0[]- b(b(a(x364))) -5|[]-> a(b(a(x364))) c(b(b(x365))) <-8|0[]- c(b(a(x365))) -9|[]-> c(a(a(x365))) b(c(a(x366))) <-9|0[]- b(c(b(x366))) -1|[]-> b(a(b(x366))) c(a(x)) <-9|[]- c(b(x)) -3|[]-> c(c(x)) c(c(a(x368))) <-9|0[]- c(c(b(x368))) -4|[]-> b(b(b(x368))) b(c(a(x369))) <-9|0[]- b(c(b(x369))) -7|[]-> c(c(b(x369))) c(c(a(x370))) <-9|0[]- c(c(b(x370))) -10|[]-> b(a(b(x370))) b(b(a(x371))) <-10|0[]- b(c(c(x371))) -1|[]-> b(a(c(x371))) b(a(x)) <-10|[]- c(c(x)) -4|[]-> b(b(x)) c(b(a(x373))) <-10|0[]- c(c(c(x373))) -4|[]-> b(b(c(x373))) b(b(a(x374))) <-10|0[]- b(c(c(x374))) -7|[]-> c(c(c(x374))) c(b(a(x375))) <-10|0[]- c(c(c(x375))) -10|[]-> b(a(c(x375))) Redundant Rules Transformation: c(a(x)) -> b(a(x)) b(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(a(x)) -> b(b(x)) c(b(x)) -> c(a(x)) c(c(x)) -> b(a(x)) c(a(x)) -> a(b(x)) c(a(x)) -> b(b(x)) b(c(x)) -> a(b(x)) b(c(x)) -> b(b(x)) c(b(x)) -> b(b(x)) c(b(x)) -> b(a(x)) c(c(x)) -> a(b(x)) Church Rosser Transformation Processor (dup): strict: weak: c(a(x)) -> b(a(x)) b(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(a(x)) -> b(b(x)) c(b(x)) -> c(a(x)) c(c(x)) -> b(a(x)) c(a(x)) -> a(b(x)) c(a(x)) -> b(b(x)) b(c(x)) -> a(b(x)) b(c(x)) -> b(b(x)) c(b(x)) -> b(b(x)) c(b(x)) -> b(a(x)) c(c(x)) -> a(b(x)) critical peaks: 156 b(b(a(x1024))) <-0|0[]- b(c(a(x1024))) -1|[]-> b(a(a(x1024))) c(b(a(x1025))) <-0|0[]- c(c(a(x1025))) -4|[]-> b(b(a(x1025))) b(a(x)) <-0|[]- c(a(x)) -6|[]-> c(c(x)) b(b(a(x1027))) <-0|0[]- b(c(a(x1027))) -7|[]-> c(c(a(x1027))) c(b(a(x1028))) <-0|0[]- c(c(a(x1028))) -10|[]-> b(a(a(x1028))) b(a(x)) <-0|[]- c(a(x)) -11|[]-> a(b(x)) b(a(x)) <-0|[]- c(a(x)) -12|[]-> b(b(x)) b(b(a(x1031))) <-0|0[]- b(c(a(x1031))) -13|[]-> a(b(a(x1031))) b(b(a(x1032))) <-0|0[]- b(c(a(x1032))) -14|[]-> b(b(a(x1032))) c(b(a(x1033))) <-0|0[]- c(c(a(x1033))) -17|[]-> a(b(a(x1033))) c(b(a(x1034))) <-1|0[]- c(b(c(x1034))) -3|[]-> c(c(c(x1034))) b(b(a(x1035))) <-1|0[]- b(b(c(x1035))) -5|[]-> a(b(c(x1035))) b(a(x)) <-1|[]- b(c(x)) -7|[]-> c(c(x)) c(b(a(x1037))) <-1|0[]- c(b(c(x1037))) -9|[]-> c(a(c(x1037))) b(a(x)) <-1|[]- b(c(x)) -13|[]-> a(b(x)) b(a(x)) <-1|[]- b(c(x)) -14|[]-> b(b(x)) c(b(a(x1040))) <-1|0[]- c(b(c(x1040))) -15|[]-> b(b(c(x1040))) c(b(a(x1041))) <-1|0[]- c(b(c(x1041))) -16|[]-> b(a(c(x1041))) c(a(b(x1042))) <-2|0[]- c(b(a(x1042))) -3|[]-> c(c(a(x1042))) b(a(b(x1043))) <-2|0[]- b(b(a(x1043))) -5|[]-> a(b(a(x1043))) a(b(x)) <-2|[]- b(a(x)) -8|[]-> b(b(x)) c(a(b(x1045))) <-2|0[]- c(b(a(x1045))) -9|[]-> c(a(a(x1045))) c(a(b(x1046))) <-2|0[]- c(b(a(x1046))) -15|[]-> b(b(a(x1046))) c(a(b(x1047))) <-2|0[]- c(b(a(x1047))) -16|[]-> b(a(a(x1047))) b(c(c(x1048))) <-3|0[]- b(c(b(x1048))) -1|[]-> b(a(b(x1048))) c(c(c(x1049))) <-3|0[]- c(c(b(x1049))) -4|[]-> b(b(b(x1049))) b(c(c(x1050))) <-3|0[]- b(c(b(x1050))) -7|[]-> c(c(b(x1050))) c(c(x)) <-3|[]- c(b(x)) -9|[]-> c(a(x)) c(c(c(x1052))) <-3|0[]- c(c(b(x1052))) -10|[]-> b(a(b(x1052))) b(c(c(x1053))) <-3|0[]- b(c(b(x1053))) -13|[]-> a(b(b(x1053))) b(c(c(x1054))) <-3|0[]- b(c(b(x1054))) -14|[]-> b(b(b(x1054))) c(c(x)) <-3|[]- c(b(x)) -15|[]-> b(b(x)) c(c(x)) <-3|[]- c(b(x)) -16|[]-> b(a(x)) c(c(c(x1057))) <-3|0[]- c(c(b(x1057))) -17|[]-> a(b(b(x1057))) b(b(b(x1058))) <-4|0[]- b(c(c(x1058))) -1|[]-> b(a(c(x1058))) c(b(b(x1059))) <-4|0[]- c(c(c(x1059))) -4|[]-> b(b(c(x1059))) b(b(b(x1060))) <-4|0[]- b(c(c(x1060))) -7|[]-> c(c(c(x1060))) b(b(x)) <-4|[]- c(c(x)) -10|[]-> b(a(x)) c(b(b(x1062))) <-4|0[]- c(c(c(x1062))) -10|[]-> b(a(c(x1062))) b(b(b(x1063))) <-4|0[]- b(c(c(x1063))) -13|[]-> a(b(c(x1063))) b(b(b(x1064))) <-4|0[]- b(c(c(x1064))) -14|[]-> b(b(c(x1064))) b(b(x)) <-4|[]- c(c(x)) -17|[]-> a(b(x)) c(b(b(x1066))) <-4|0[]- c(c(c(x1066))) -17|[]-> a(b(c(x1066))) c(a(b(x1067))) <-5|0[]- c(b(b(x1067))) -3|[]-> c(c(b(x1067))) b(a(b(x1068))) <-5|0[]- b(b(b(x1068))) -5|[]-> a(b(b(x1068))) c(a(b(x1069))) <-5|0[]- c(b(b(x1069))) -9|[]-> c(a(b(x1069))) c(a(b(x1070))) <-5|0[]- c(b(b(x1070))) -15|[]-> b(b(b(x1070))) c(a(b(x1071))) <-5|0[]- c(b(b(x1071))) -16|[]-> b(a(b(x1071))) c(c(x)) <-6|[]- c(a(x)) -0|[]-> b(a(x)) b(c(c(x1073))) <-6|0[]- b(c(a(x1073))) -1|[]-> b(a(a(x1073))) c(c(c(x1074))) <-6|0[]- c(c(a(x1074))) -4|[]-> b(b(a(x1074))) b(c(c(x1075))) <-6|0[]- b(c(a(x1075))) -7|[]-> c(c(a(x1075))) c(c(c(x1076))) <-6|0[]- c(c(a(x1076))) -10|[]-> b(a(a(x1076))) c(c(x)) <-6|[]- c(a(x)) -11|[]-> a(b(x)) c(c(x)) <-6|[]- c(a(x)) -12|[]-> b(b(x)) b(c(c(x1079))) <-6|0[]- b(c(a(x1079))) -13|[]-> a(b(a(x1079))) b(c(c(x1080))) <-6|0[]- b(c(a(x1080))) -14|[]-> b(b(a(x1080))) c(c(c(x1081))) <-6|0[]- c(c(a(x1081))) -17|[]-> a(b(a(x1081))) c(c(x)) <-7|[]- b(c(x)) -1|[]-> b(a(x)) c(c(c(x1083))) <-7|0[]- c(b(c(x1083))) -3|[]-> c(c(c(x1083))) b(c(c(x1084))) <-7|0[]- b(b(c(x1084))) -5|[]-> a(b(c(x1084))) c(c(c(x1085))) <-7|0[]- c(b(c(x1085))) -9|[]-> c(a(c(x1085))) c(c(x)) <-7|[]- b(c(x)) -13|[]-> a(b(x)) c(c(x)) <-7|[]- b(c(x)) -14|[]-> b(b(x)) c(c(c(x1088))) <-7|0[]- c(b(c(x1088))) -15|[]-> b(b(c(x1088))) c(c(c(x1089))) <-7|0[]- c(b(c(x1089))) -16|[]-> b(a(c(x1089))) b(b(x)) <-8|[]- b(a(x)) -2|[]-> a(b(x)) c(b(b(x1091))) <-8|0[]- c(b(a(x1091))) -3|[]-> c(c(a(x1091))) b(b(b(x1092))) <-8|0[]- b(b(a(x1092))) -5|[]-> a(b(a(x1092))) c(b(b(x1093))) <-8|0[]- c(b(a(x1093))) -9|[]-> c(a(a(x1093))) c(b(b(x1094))) <-8|0[]- c(b(a(x1094))) -15|[]-> b(b(a(x1094))) c(b(b(x1095))) <-8|0[]- c(b(a(x1095))) -16|[]-> b(a(a(x1095))) b(c(a(x1096))) <-9|0[]- b(c(b(x1096))) -1|[]-> b(a(b(x1096))) c(a(x)) <-9|[]- c(b(x)) -3|[]-> c(c(x)) c(c(a(x1098))) <-9|0[]- c(c(b(x1098))) -4|[]-> b(b(b(x1098))) b(c(a(x1099))) <-9|0[]- b(c(b(x1099))) -7|[]-> c(c(b(x1099))) c(c(a(x1100))) <-9|0[]- c(c(b(x1100))) -10|[]-> b(a(b(x1100))) b(c(a(x1101))) <-9|0[]- b(c(b(x1101))) -13|[]-> a(b(b(x1101))) b(c(a(x1102))) <-9|0[]- b(c(b(x1102))) -14|[]-> b(b(b(x1102))) c(a(x)) <-9|[]- c(b(x)) -15|[]-> b(b(x)) c(a(x)) <-9|[]- c(b(x)) -16|[]-> b(a(x)) c(c(a(x1105))) <-9|0[]- c(c(b(x1105))) -17|[]-> a(b(b(x1105))) b(b(a(x1106))) <-10|0[]- b(c(c(x1106))) -1|[]-> b(a(c(x1106))) b(a(x)) <-10|[]- c(c(x)) -4|[]-> b(b(x)) c(b(a(x1108))) <-10|0[]- c(c(c(x1108))) -4|[]-> b(b(c(x1108))) b(b(a(x1109))) <-10|0[]- b(c(c(x1109))) -7|[]-> c(c(c(x1109))) c(b(a(x1110))) <-10|0[]- c(c(c(x1110))) -10|[]-> b(a(c(x1110))) b(b(a(x1111))) <-10|0[]- b(c(c(x1111))) -13|[]-> a(b(c(x1111))) b(b(a(x1112))) <-10|0[]- b(c(c(x1112))) -14|[]-> b(b(c(x1112))) b(a(x)) <-10|[]- c(c(x)) -17|[]-> a(b(x)) c(b(a(x1114))) <-10|0[]- c(c(c(x1114))) -17|[]-> a(b(c(x1114))) a(b(x)) <-11|[]- c(a(x)) -0|[]-> b(a(x)) b(a(b(x1116))) <-11|0[]- b(c(a(x1116))) -1|[]-> b(a(a(x1116))) c(a(b(x1117))) <-11|0[]- c(c(a(x1117))) -4|[]-> b(b(a(x1117))) a(b(x)) <-11|[]- c(a(x)) -6|[]-> c(c(x)) b(a(b(x1119))) <-11|0[]- b(c(a(x1119))) -7|[]-> c(c(a(x1119))) c(a(b(x1120))) <-11|0[]- c(c(a(x1120))) -10|[]-> b(a(a(x1120))) a(b(x)) <-11|[]- c(a(x)) -12|[]-> b(b(x)) b(a(b(x1122))) <-11|0[]- b(c(a(x1122))) -13|[]-> a(b(a(x1122))) b(a(b(x1123))) <-11|0[]- b(c(a(x1123))) -14|[]-> b(b(a(x1123))) c(a(b(x1124))) <-11|0[]- c(c(a(x1124))) -17|[]-> a(b(a(x1124))) b(b(x)) <-12|[]- c(a(x)) -0|[]-> b(a(x)) b(b(b(x1126))) <-12|0[]- b(c(a(x1126))) -1|[]-> b(a(a(x1126))) c(b(b(x1127))) <-12|0[]- c(c(a(x1127))) -4|[]-> b(b(a(x1127))) b(b(x)) <-12|[]- c(a(x)) -6|[]-> c(c(x)) b(b(b(x1129))) <-12|0[]- b(c(a(x1129))) -7|[]-> c(c(a(x1129))) c(b(b(x1130))) <-12|0[]- c(c(a(x1130))) -10|[]-> b(a(a(x1130))) b(b(x)) <-12|[]- c(a(x)) -11|[]-> a(b(x)) b(b(b(x1132))) <-12|0[]- b(c(a(x1132))) -13|[]-> a(b(a(x1132))) b(b(b(x1133))) <-12|0[]- b(c(a(x1133))) -14|[]-> b(b(a(x1133))) c(b(b(x1134))) <-12|0[]- c(c(a(x1134))) -17|[]-> a(b(a(x1134))) a(b(x)) <-13|[]- b(c(x)) -1|[]-> b(a(x)) c(a(b(x1136))) <-13|0[]- c(b(c(x1136))) -3|[]-> c(c(c(x1136))) b(a(b(x1137))) <-13|0[]- b(b(c(x1137))) -5|[]-> a(b(c(x1137))) a(b(x)) <-13|[]- b(c(x)) -7|[]-> c(c(x)) c(a(b(x1139))) <-13|0[]- c(b(c(x1139))) -9|[]-> c(a(c(x1139))) a(b(x)) <-13|[]- b(c(x)) -14|[]-> b(b(x)) c(a(b(x1141))) <-13|0[]- c(b(c(x1141))) -15|[]-> b(b(c(x1141))) c(a(b(x1142))) <-13|0[]- c(b(c(x1142))) -16|[]-> b(a(c(x1142))) b(b(x)) <-14|[]- b(c(x)) -1|[]-> b(a(x)) c(b(b(x1144))) <-14|0[]- c(b(c(x1144))) -3|[]-> c(c(c(x1144))) b(b(b(x1145))) <-14|0[]- b(b(c(x1145))) -5|[]-> a(b(c(x1145))) b(b(x)) <-14|[]- b(c(x)) -7|[]-> c(c(x)) c(b(b(x1147))) <-14|0[]- c(b(c(x1147))) -9|[]-> c(a(c(x1147))) b(b(x)) <-14|[]- b(c(x)) -13|[]-> a(b(x)) c(b(b(x1149))) <-14|0[]- c(b(c(x1149))) -15|[]-> b(b(c(x1149))) c(b(b(x1150))) <-14|0[]- c(b(c(x1150))) -16|[]-> b(a(c(x1150))) b(b(b(x1151))) <-15|0[]- b(c(b(x1151))) -1|[]-> b(a(b(x1151))) b(b(x)) <-15|[]- c(b(x)) -3|[]-> c(c(x)) c(b(b(x1153))) <-15|0[]- c(c(b(x1153))) -4|[]-> b(b(b(x1153))) b(b(b(x1154))) <-15|0[]- b(c(b(x1154))) -7|[]-> c(c(b(x1154))) b(b(x)) <-15|[]- c(b(x)) -9|[]-> c(a(x)) c(b(b(x1156))) <-15|0[]- c(c(b(x1156))) -10|[]-> b(a(b(x1156))) b(b(b(x1157))) <-15|0[]- b(c(b(x1157))) -13|[]-> a(b(b(x1157))) b(b(b(x1158))) <-15|0[]- b(c(b(x1158))) -14|[]-> b(b(b(x1158))) b(b(x)) <-15|[]- c(b(x)) -16|[]-> b(a(x)) c(b(b(x1160))) <-15|0[]- c(c(b(x1160))) -17|[]-> a(b(b(x1160))) b(b(a(x1161))) <-16|0[]- b(c(b(x1161))) -1|[]-> b(a(b(x1161))) b(a(x)) <-16|[]- c(b(x)) -3|[]-> c(c(x)) c(b(a(x1163))) <-16|0[]- c(c(b(x1163))) -4|[]-> b(b(b(x1163))) b(b(a(x1164))) <-16|0[]- b(c(b(x1164))) -7|[]-> c(c(b(x1164))) b(a(x)) <-16|[]- c(b(x)) -9|[]-> c(a(x)) c(b(a(x1166))) <-16|0[]- c(c(b(x1166))) -10|[]-> b(a(b(x1166))) b(b(a(x1167))) <-16|0[]- b(c(b(x1167))) -13|[]-> a(b(b(x1167))) b(b(a(x1168))) <-16|0[]- b(c(b(x1168))) -14|[]-> b(b(b(x1168))) b(a(x)) <-16|[]- c(b(x)) -15|[]-> b(b(x)) c(b(a(x1170))) <-16|0[]- c(c(b(x1170))) -17|[]-> a(b(b(x1170))) b(a(b(x1171))) <-17|0[]- b(c(c(x1171))) -1|[]-> b(a(c(x1171))) a(b(x)) <-17|[]- c(c(x)) -4|[]-> b(b(x)) c(a(b(x1173))) <-17|0[]- c(c(c(x1173))) -4|[]-> b(b(c(x1173))) b(a(b(x1174))) <-17|0[]- b(c(c(x1174))) -7|[]-> c(c(c(x1174))) a(b(x)) <-17|[]- c(c(x)) -10|[]-> b(a(x)) c(a(b(x1176))) <-17|0[]- c(c(c(x1176))) -10|[]-> b(a(c(x1176))) b(a(b(x1177))) <-17|0[]- b(c(c(x1177))) -13|[]-> a(b(c(x1177))) b(a(b(x1178))) <-17|0[]- b(c(c(x1178))) -14|[]-> b(b(c(x1178))) c(a(b(x1179))) <-17|0[]- c(c(c(x1179))) -17|[]-> a(b(c(x1179))) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: b(c(a(x1024))) -> b(b(a(x1024))) b(c(a(x1024))) -> b(a(a(x1024))) b(a(a(x1024))) -> b(b(a(x1024))) b(b(a(x1024))) -> a(b(a(x1024))) b(a(a(x1024))) -> a(b(a(x1024))) c(c(a(x1025))) -> c(b(a(x1025))) c(c(a(x1025))) -> b(b(a(x1025))) c(b(a(x1025))) -> b(b(a(x1025))) c(a(x)) -> b(a(x)) c(a(x)) -> c(c(x)) c(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(b(x)) b(c(a(x1027))) -> b(b(a(x1027))) b(c(a(x1027))) -> c(c(a(x1027))) c(c(a(x1027))) -> b(b(a(x1027))) b(b(a(x1027))) -> a(b(a(x1027))) c(c(a(x1027))) -> a(b(a(x1027))) c(c(a(x1028))) -> c(b(a(x1028))) c(c(a(x1028))) -> b(a(a(x1028))) c(b(a(x1028))) -> b(b(a(x1028))) b(a(a(x1028))) -> b(b(a(x1028))) c(b(a(x1028))) -> b(a(a(x1028))) c(a(x)) -> b(a(x)) c(a(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(a(x)) -> b(a(x)) c(a(x)) -> b(b(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> b(b(x)) b(c(a(x1031))) -> b(b(a(x1031))) b(c(a(x1031))) -> a(b(a(x1031))) b(b(a(x1031))) -> a(b(a(x1031))) b(c(a(x1032))) -> b(b(a(x1032))) b(c(a(x1032))) -> b(b(a(x1032))) c(c(a(x1033))) -> c(b(a(x1033))) c(c(a(x1033))) -> a(b(a(x1033))) c(b(a(x1033))) -> c(a(b(x1033))) c(a(b(x1033))) -> a(b(b(x1033))) a(b(a(x1033))) -> a(b(b(x1033))) c(b(a(x1033))) -> c(c(a(x1033))) c(c(a(x1033))) -> a(b(a(x1033))) c(b(a(x1033))) -> c(a(a(x1033))) c(a(a(x1033))) -> a(b(a(x1033))) c(b(a(x1033))) -> b(b(a(x1033))) b(b(a(x1033))) -> a(b(a(x1033))) c(b(a(x1033))) -> b(a(a(x1033))) b(a(a(x1033))) -> a(b(a(x1033))) c(b(c(x1034))) -> c(b(a(x1034))) c(b(c(x1034))) -> c(c(c(x1034))) c(c(c(x1034))) -> c(b(a(x1034))) c(b(a(x1034))) -> c(a(b(x1034))) c(c(c(x1034))) -> c(a(b(x1034))) c(b(a(x1034))) -> c(b(b(x1034))) c(c(c(x1034))) -> c(b(b(x1034))) b(b(c(x1035))) -> b(b(a(x1035))) b(b(c(x1035))) -> a(b(c(x1035))) b(b(a(x1035))) -> a(b(a(x1035))) a(b(c(x1035))) -> a(b(a(x1035))) b(c(x)) -> b(a(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(b(c(x1037))) -> c(b(a(x1037))) c(b(c(x1037))) -> c(a(c(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(b(a(x1037))) c(b(a(x1037))) -> c(a(b(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(a(b(x1037))) c(b(a(x1037))) -> c(c(a(x1037))) c(c(a(x1037))) -> c(a(b(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(a(b(x1037))) c(b(a(x1037))) -> c(b(b(x1037))) c(b(b(x1037))) -> c(a(b(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(a(b(x1037))) c(b(a(x1037))) -> c(b(b(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(b(b(x1037))) c(b(a(x1037))) -> c(c(a(x1037))) c(c(a(x1037))) -> c(b(b(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(c(c(x1037))) -> c(b(b(x1037))) c(b(a(x1037))) -> b(b(a(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(a(x1037))) c(b(a(x1037))) -> c(c(a(x1037))) c(c(a(x1037))) -> b(b(a(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(a(x1037))) c(b(a(x1037))) -> c(a(a(x1037))) c(a(a(x1037))) -> b(b(a(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(a(x1037))) c(b(a(x1037))) -> b(a(a(x1037))) b(a(a(x1037))) -> b(b(a(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(a(x1037))) c(b(a(x1037))) -> c(a(b(x1037))) c(a(b(x1037))) -> b(a(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(a(b(x1037))) c(b(a(x1037))) -> c(b(b(x1037))) c(b(b(x1037))) -> b(a(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(a(b(x1037))) c(b(a(x1037))) -> b(b(a(x1037))) b(b(a(x1037))) -> b(a(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(a(b(x1037))) c(b(a(x1037))) -> c(a(b(x1037))) c(a(b(x1037))) -> a(b(b(x1037))) c(a(c(x1037))) -> a(b(c(x1037))) a(b(c(x1037))) -> a(b(b(x1037))) c(b(a(x1037))) -> c(a(b(x1037))) c(a(b(x1037))) -> b(b(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(b(x1037))) c(b(a(x1037))) -> c(b(b(x1037))) c(b(b(x1037))) -> b(b(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(b(x1037))) c(b(a(x1037))) -> b(b(a(x1037))) b(b(a(x1037))) -> b(b(b(x1037))) c(a(c(x1037))) -> b(b(c(x1037))) b(b(c(x1037))) -> b(b(b(x1037))) c(b(a(x1037))) -> c(c(a(x1037))) c(c(a(x1037))) -> c(c(c(x1037))) c(a(c(x1037))) -> c(c(c(x1037))) c(b(a(x1037))) -> c(c(a(x1037))) c(c(a(x1037))) -> a(b(a(x1037))) c(a(c(x1037))) -> a(b(c(x1037))) a(b(c(x1037))) -> a(b(a(x1037))) c(b(a(x1037))) -> c(a(a(x1037))) c(a(a(x1037))) -> a(b(a(x1037))) c(a(c(x1037))) -> a(b(c(x1037))) a(b(c(x1037))) -> a(b(a(x1037))) c(b(a(x1037))) -> b(b(a(x1037))) b(b(a(x1037))) -> a(b(a(x1037))) c(a(c(x1037))) -> a(b(c(x1037))) a(b(c(x1037))) -> a(b(a(x1037))) c(b(a(x1037))) -> b(a(a(x1037))) b(a(a(x1037))) -> a(b(a(x1037))) c(a(c(x1037))) -> a(b(c(x1037))) a(b(c(x1037))) -> a(b(a(x1037))) b(c(x)) -> b(a(x)) b(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(c(x)) -> b(a(x)) b(c(x)) -> b(b(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(b(c(x1040))) -> c(b(a(x1040))) c(b(c(x1040))) -> b(b(c(x1040))) c(b(a(x1040))) -> b(b(a(x1040))) b(b(c(x1040))) -> b(b(a(x1040))) c(b(c(x1041))) -> c(b(a(x1041))) c(b(c(x1041))) -> b(a(c(x1041))) c(b(a(x1041))) -> b(b(a(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(a(x1041))) c(b(a(x1041))) -> c(c(a(x1041))) c(c(a(x1041))) -> b(b(a(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(a(x1041))) c(b(a(x1041))) -> c(a(a(x1041))) c(a(a(x1041))) -> b(b(a(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(a(x1041))) c(b(a(x1041))) -> b(a(a(x1041))) b(a(a(x1041))) -> b(b(a(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(a(x1041))) c(b(a(x1041))) -> c(a(b(x1041))) c(a(b(x1041))) -> b(a(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(a(b(x1041))) c(b(a(x1041))) -> c(b(b(x1041))) c(b(b(x1041))) -> b(a(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(a(b(x1041))) c(b(a(x1041))) -> b(b(a(x1041))) b(b(a(x1041))) -> b(a(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(a(b(x1041))) c(b(a(x1041))) -> c(a(b(x1041))) c(a(b(x1041))) -> a(b(b(x1041))) b(a(c(x1041))) -> a(b(c(x1041))) a(b(c(x1041))) -> a(b(b(x1041))) c(b(a(x1041))) -> c(a(b(x1041))) c(a(b(x1041))) -> b(b(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(b(x1041))) c(b(a(x1041))) -> c(b(b(x1041))) c(b(b(x1041))) -> b(b(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(b(x1041))) c(b(a(x1041))) -> b(b(a(x1041))) b(b(a(x1041))) -> b(b(b(x1041))) b(a(c(x1041))) -> b(b(c(x1041))) b(b(c(x1041))) -> b(b(b(x1041))) c(b(a(x1041))) -> c(c(a(x1041))) c(c(a(x1041))) -> a(b(a(x1041))) b(a(c(x1041))) -> a(b(c(x1041))) a(b(c(x1041))) -> a(b(a(x1041))) c(b(a(x1041))) -> c(a(a(x1041))) c(a(a(x1041))) -> a(b(a(x1041))) b(a(c(x1041))) -> a(b(c(x1041))) a(b(c(x1041))) -> a(b(a(x1041))) c(b(a(x1041))) -> b(b(a(x1041))) b(b(a(x1041))) -> a(b(a(x1041))) b(a(c(x1041))) -> a(b(c(x1041))) a(b(c(x1041))) -> a(b(a(x1041))) c(b(a(x1041))) -> b(a(a(x1041))) b(a(a(x1041))) -> a(b(a(x1041))) b(a(c(x1041))) -> a(b(c(x1041))) a(b(c(x1041))) -> a(b(a(x1041))) c(b(a(x1042))) -> c(a(b(x1042))) c(b(a(x1042))) -> c(c(a(x1042))) c(c(a(x1042))) -> c(a(b(x1042))) b(b(a(x1043))) -> b(a(b(x1043))) b(b(a(x1043))) -> a(b(a(x1043))) b(a(b(x1043))) -> a(b(b(x1043))) a(b(a(x1043))) -> a(b(b(x1043))) b(a(x)) -> a(b(x)) b(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(b(a(x1045))) -> c(a(b(x1045))) c(b(a(x1045))) -> c(a(a(x1045))) c(a(a(x1045))) -> c(c(a(x1045))) c(c(a(x1045))) -> c(a(b(x1045))) c(a(b(x1045))) -> b(a(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(a(b(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> b(a(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(a(b(x1045))) c(a(b(x1045))) -> b(b(b(x1045))) b(b(b(x1045))) -> b(a(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(a(b(x1045))) c(a(b(x1045))) -> a(b(b(x1045))) c(a(a(x1045))) -> a(b(a(x1045))) a(b(a(x1045))) -> a(b(b(x1045))) c(a(b(x1045))) -> b(a(b(x1045))) b(a(b(x1045))) -> a(b(b(x1045))) c(a(a(x1045))) -> a(b(a(x1045))) a(b(a(x1045))) -> a(b(b(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> a(b(b(x1045))) c(a(a(x1045))) -> a(b(a(x1045))) a(b(a(x1045))) -> a(b(b(x1045))) c(a(b(x1045))) -> b(b(b(x1045))) b(b(b(x1045))) -> a(b(b(x1045))) c(a(a(x1045))) -> a(b(a(x1045))) a(b(a(x1045))) -> a(b(b(x1045))) c(a(b(x1045))) -> b(b(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(b(b(x1045))) c(a(b(x1045))) -> b(a(b(x1045))) b(a(b(x1045))) -> b(b(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(b(b(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> b(b(b(x1045))) c(a(a(x1045))) -> b(b(a(x1045))) b(b(a(x1045))) -> b(b(b(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> c(c(c(x1045))) c(a(a(x1045))) -> c(c(a(x1045))) c(c(a(x1045))) -> c(c(c(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> c(c(a(x1045))) c(a(a(x1045))) -> c(c(a(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> c(b(b(x1045))) c(a(a(x1045))) -> c(c(a(x1045))) c(c(a(x1045))) -> c(b(b(x1045))) c(a(b(x1045))) -> c(c(b(x1045))) c(c(b(x1045))) -> c(b(a(x1045))) c(a(a(x1045))) -> c(c(a(x1045))) c(c(a(x1045))) -> c(b(a(x1045))) c(a(b(x1045))) -> a(b(b(x1045))) a(b(b(x1045))) -> a(a(b(x1045))) c(a(a(x1045))) -> a(b(a(x1045))) a(b(a(x1045))) -> a(a(b(x1045))) c(b(a(x1046))) -> c(a(b(x1046))) c(b(a(x1046))) -> b(b(a(x1046))) c(a(b(x1046))) -> b(a(b(x1046))) b(b(a(x1046))) -> b(a(b(x1046))) c(a(b(x1046))) -> b(b(b(x1046))) b(b(a(x1046))) -> b(b(b(x1046))) c(b(a(x1047))) -> c(a(b(x1047))) c(b(a(x1047))) -> b(a(a(x1047))) c(a(b(x1047))) -> b(a(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(a(b(x1047))) c(a(b(x1047))) -> c(c(b(x1047))) c(c(b(x1047))) -> b(a(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(a(b(x1047))) c(a(b(x1047))) -> b(b(b(x1047))) b(b(b(x1047))) -> b(a(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(a(b(x1047))) c(a(b(x1047))) -> a(b(b(x1047))) b(a(a(x1047))) -> a(b(a(x1047))) a(b(a(x1047))) -> a(b(b(x1047))) c(a(b(x1047))) -> b(a(b(x1047))) b(a(b(x1047))) -> a(b(b(x1047))) b(a(a(x1047))) -> a(b(a(x1047))) a(b(a(x1047))) -> a(b(b(x1047))) c(a(b(x1047))) -> c(c(b(x1047))) c(c(b(x1047))) -> a(b(b(x1047))) b(a(a(x1047))) -> a(b(a(x1047))) a(b(a(x1047))) -> a(b(b(x1047))) c(a(b(x1047))) -> b(b(b(x1047))) b(b(b(x1047))) -> a(b(b(x1047))) b(a(a(x1047))) -> a(b(a(x1047))) a(b(a(x1047))) -> a(b(b(x1047))) c(a(b(x1047))) -> b(b(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(b(b(x1047))) c(a(b(x1047))) -> b(a(b(x1047))) b(a(b(x1047))) -> b(b(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(b(b(x1047))) c(a(b(x1047))) -> c(c(b(x1047))) c(c(b(x1047))) -> b(b(b(x1047))) b(a(a(x1047))) -> b(b(a(x1047))) b(b(a(x1047))) -> b(b(b(x1047))) c(a(b(x1047))) -> a(b(b(x1047))) a(b(b(x1047))) -> a(a(b(x1047))) b(a(a(x1047))) -> a(b(a(x1047))) a(b(a(x1047))) -> a(a(b(x1047))) b(c(b(x1048))) -> b(c(c(x1048))) b(c(b(x1048))) -> b(a(b(x1048))) b(c(c(x1048))) -> b(b(b(x1048))) b(a(b(x1048))) -> b(b(b(x1048))) b(c(c(x1048))) -> b(a(b(x1048))) c(c(b(x1049))) -> c(c(c(x1049))) c(c(b(x1049))) -> b(b(b(x1049))) c(c(c(x1049))) -> c(b(b(x1049))) c(b(b(x1049))) -> b(b(b(x1049))) c(c(c(x1049))) -> b(b(c(x1049))) b(b(c(x1049))) -> b(b(b(x1049))) c(c(c(x1049))) -> c(a(b(x1049))) c(a(b(x1049))) -> b(b(b(x1049))) c(c(c(x1049))) -> c(b(b(x1049))) c(b(b(x1049))) -> b(a(b(x1049))) b(b(b(x1049))) -> b(a(b(x1049))) c(c(c(x1049))) -> b(b(c(x1049))) b(b(c(x1049))) -> b(a(b(x1049))) b(b(b(x1049))) -> b(a(b(x1049))) c(c(c(x1049))) -> c(a(b(x1049))) c(a(b(x1049))) -> b(a(b(x1049))) b(b(b(x1049))) -> b(a(b(x1049))) c(c(c(x1049))) -> c(a(b(x1049))) c(a(b(x1049))) -> a(b(b(x1049))) b(b(b(x1049))) -> a(b(b(x1049))) c(c(c(x1049))) -> c(a(b(x1049))) c(a(b(x1049))) -> a(b(b(x1049))) b(b(b(x1049))) -> b(a(b(x1049))) b(a(b(x1049))) -> a(b(b(x1049))) c(c(c(x1049))) -> a(b(c(x1049))) a(b(c(x1049))) -> a(b(b(x1049))) b(b(b(x1049))) -> a(b(b(x1049))) c(c(c(x1049))) -> a(b(c(x1049))) a(b(c(x1049))) -> a(b(b(x1049))) b(b(b(x1049))) -> b(a(b(x1049))) b(a(b(x1049))) -> a(b(b(x1049))) c(c(c(x1049))) -> a(b(c(x1049))) a(b(c(x1049))) -> a(a(b(x1049))) b(b(b(x1049))) -> a(b(b(x1049))) a(b(b(x1049))) -> a(a(b(x1049))) b(c(b(x1050))) -> b(c(c(x1050))) b(c(b(x1050))) -> c(c(b(x1050))) b(c(c(x1050))) -> b(b(b(x1050))) c(c(b(x1050))) -> b(b(b(x1050))) b(c(c(x1050))) -> c(c(c(x1050))) c(c(b(x1050))) -> c(c(c(x1050))) b(c(c(x1050))) -> b(a(b(x1050))) c(c(b(x1050))) -> b(a(b(x1050))) c(b(x)) -> c(c(x)) c(b(x)) -> c(a(x)) c(a(x)) -> c(c(x)) c(c(x)) -> b(b(x)) c(a(x)) -> b(b(x)) c(c(x)) -> b(a(x)) c(a(x)) -> b(a(x)) c(c(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(c(b(x1052))) -> c(c(c(x1052))) c(c(b(x1052))) -> b(a(b(x1052))) c(c(c(x1052))) -> c(b(b(x1052))) c(b(b(x1052))) -> b(b(b(x1052))) b(a(b(x1052))) -> b(b(b(x1052))) c(c(c(x1052))) -> b(b(c(x1052))) b(b(c(x1052))) -> b(b(b(x1052))) b(a(b(x1052))) -> b(b(b(x1052))) c(c(c(x1052))) -> c(a(b(x1052))) c(a(b(x1052))) -> b(b(b(x1052))) b(a(b(x1052))) -> b(b(b(x1052))) c(c(c(x1052))) -> c(b(b(x1052))) c(b(b(x1052))) -> b(a(b(x1052))) c(c(c(x1052))) -> b(b(c(x1052))) b(b(c(x1052))) -> b(a(b(x1052))) c(c(c(x1052))) -> c(a(b(x1052))) c(a(b(x1052))) -> b(a(b(x1052))) c(c(c(x1052))) -> c(a(b(x1052))) c(a(b(x1052))) -> a(b(b(x1052))) b(a(b(x1052))) -> a(b(b(x1052))) c(c(c(x1052))) -> c(a(b(x1052))) c(a(b(x1052))) -> a(b(b(x1052))) b(a(b(x1052))) -> b(b(b(x1052))) b(b(b(x1052))) -> a(b(b(x1052))) c(c(c(x1052))) -> a(b(c(x1052))) a(b(c(x1052))) -> a(b(b(x1052))) b(a(b(x1052))) -> a(b(b(x1052))) c(c(c(x1052))) -> a(b(c(x1052))) a(b(c(x1052))) -> a(b(b(x1052))) b(a(b(x1052))) -> b(b(b(x1052))) b(b(b(x1052))) -> a(b(b(x1052))) c(c(c(x1052))) -> a(b(c(x1052))) a(b(c(x1052))) -> a(a(b(x1052))) b(a(b(x1052))) -> a(b(b(x1052))) a(b(b(x1052))) -> a(a(b(x1052))) b(c(b(x1053))) -> b(c(c(x1053))) b(c(b(x1053))) -> a(b(b(x1053))) b(c(c(x1053))) -> b(b(b(x1053))) b(b(b(x1053))) -> a(b(b(x1053))) b(c(c(x1053))) -> a(b(c(x1053))) a(b(c(x1053))) -> a(b(b(x1053))) b(c(c(x1053))) -> b(a(b(x1053))) b(a(b(x1053))) -> a(b(b(x1053))) b(c(c(x1053))) -> a(b(c(x1053))) a(b(c(x1053))) -> a(a(b(x1053))) a(b(b(x1053))) -> a(a(b(x1053))) b(c(b(x1054))) -> b(c(c(x1054))) b(c(b(x1054))) -> b(b(b(x1054))) b(c(c(x1054))) -> b(b(b(x1054))) b(c(c(x1054))) -> b(a(b(x1054))) b(b(b(x1054))) -> b(a(b(x1054))) c(b(x)) -> c(c(x)) c(b(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(b(x)) -> b(a(x)) c(c(x)) -> b(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(a(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(c(b(x1057))) -> c(c(c(x1057))) c(c(b(x1057))) -> a(b(b(x1057))) c(c(c(x1057))) -> c(a(b(x1057))) c(a(b(x1057))) -> a(b(b(x1057))) c(c(c(x1057))) -> a(b(c(x1057))) a(b(c(x1057))) -> a(b(b(x1057))) c(c(c(x1057))) -> a(b(c(x1057))) a(b(c(x1057))) -> a(a(b(x1057))) a(b(b(x1057))) -> a(a(b(x1057))) b(c(c(x1058))) -> b(b(b(x1058))) b(c(c(x1058))) -> b(a(c(x1058))) b(a(c(x1058))) -> b(b(c(x1058))) b(b(c(x1058))) -> b(b(b(x1058))) b(b(b(x1058))) -> b(a(b(x1058))) b(a(c(x1058))) -> b(b(c(x1058))) b(b(c(x1058))) -> b(a(b(x1058))) b(b(b(x1058))) -> a(b(b(x1058))) b(a(c(x1058))) -> a(b(c(x1058))) a(b(c(x1058))) -> a(b(b(x1058))) b(b(b(x1058))) -> b(a(b(x1058))) b(a(b(x1058))) -> a(b(b(x1058))) b(a(c(x1058))) -> a(b(c(x1058))) a(b(c(x1058))) -> a(b(b(x1058))) b(b(b(x1058))) -> a(b(b(x1058))) a(b(b(x1058))) -> a(a(b(x1058))) b(a(c(x1058))) -> a(b(c(x1058))) a(b(c(x1058))) -> a(a(b(x1058))) c(c(c(x1059))) -> c(b(b(x1059))) c(c(c(x1059))) -> b(b(c(x1059))) c(b(b(x1059))) -> b(b(b(x1059))) b(b(c(x1059))) -> b(b(b(x1059))) c(b(b(x1059))) -> b(a(b(x1059))) b(b(c(x1059))) -> b(a(b(x1059))) b(c(c(x1060))) -> b(b(b(x1060))) b(c(c(x1060))) -> c(c(c(x1060))) c(c(c(x1060))) -> c(b(b(x1060))) c(b(b(x1060))) -> b(b(b(x1060))) c(c(c(x1060))) -> b(b(c(x1060))) b(b(c(x1060))) -> b(b(b(x1060))) c(c(c(x1060))) -> c(a(b(x1060))) c(a(b(x1060))) -> b(b(b(x1060))) b(b(b(x1060))) -> b(a(b(x1060))) c(c(c(x1060))) -> c(b(b(x1060))) c(b(b(x1060))) -> b(a(b(x1060))) b(b(b(x1060))) -> b(a(b(x1060))) c(c(c(x1060))) -> b(b(c(x1060))) b(b(c(x1060))) -> b(a(b(x1060))) b(b(b(x1060))) -> b(a(b(x1060))) c(c(c(x1060))) -> c(a(b(x1060))) c(a(b(x1060))) -> b(a(b(x1060))) b(b(b(x1060))) -> a(b(b(x1060))) c(c(c(x1060))) -> c(a(b(x1060))) c(a(b(x1060))) -> a(b(b(x1060))) b(b(b(x1060))) -> a(b(b(x1060))) c(c(c(x1060))) -> a(b(c(x1060))) a(b(c(x1060))) -> a(b(b(x1060))) b(b(b(x1060))) -> b(a(b(x1060))) b(a(b(x1060))) -> a(b(b(x1060))) c(c(c(x1060))) -> c(a(b(x1060))) c(a(b(x1060))) -> a(b(b(x1060))) b(b(b(x1060))) -> b(a(b(x1060))) b(a(b(x1060))) -> a(b(b(x1060))) c(c(c(x1060))) -> a(b(c(x1060))) a(b(c(x1060))) -> a(b(b(x1060))) b(b(b(x1060))) -> a(b(b(x1060))) a(b(b(x1060))) -> a(a(b(x1060))) c(c(c(x1060))) -> a(b(c(x1060))) a(b(c(x1060))) -> a(a(b(x1060))) c(c(x)) -> b(b(x)) c(c(x)) -> b(a(x)) b(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(c(c(x1062))) -> c(b(b(x1062))) c(c(c(x1062))) -> b(a(c(x1062))) c(b(b(x1062))) -> b(b(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(b(b(x1062))) c(b(b(x1062))) -> c(c(b(x1062))) c(c(b(x1062))) -> b(b(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(b(b(x1062))) c(b(b(x1062))) -> c(a(b(x1062))) c(a(b(x1062))) -> b(b(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(b(b(x1062))) c(b(b(x1062))) -> b(a(b(x1062))) b(a(b(x1062))) -> b(b(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(b(b(x1062))) c(b(b(x1062))) -> b(a(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(a(b(x1062))) c(b(b(x1062))) -> c(c(b(x1062))) c(c(b(x1062))) -> b(a(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(a(b(x1062))) c(b(b(x1062))) -> c(a(b(x1062))) c(a(b(x1062))) -> b(a(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(a(b(x1062))) c(b(b(x1062))) -> b(b(b(x1062))) b(b(b(x1062))) -> b(a(b(x1062))) b(a(c(x1062))) -> b(b(c(x1062))) b(b(c(x1062))) -> b(a(b(x1062))) c(b(b(x1062))) -> c(c(b(x1062))) c(c(b(x1062))) -> a(b(b(x1062))) b(a(c(x1062))) -> a(b(c(x1062))) a(b(c(x1062))) -> a(b(b(x1062))) c(b(b(x1062))) -> c(a(b(x1062))) c(a(b(x1062))) -> a(b(b(x1062))) b(a(c(x1062))) -> a(b(c(x1062))) a(b(c(x1062))) -> a(b(b(x1062))) c(b(b(x1062))) -> b(b(b(x1062))) b(b(b(x1062))) -> a(b(b(x1062))) b(a(c(x1062))) -> a(b(c(x1062))) a(b(c(x1062))) -> a(b(b(x1062))) c(b(b(x1062))) -> b(a(b(x1062))) b(a(b(x1062))) -> a(b(b(x1062))) b(a(c(x1062))) -> a(b(c(x1062))) a(b(c(x1062))) -> a(b(b(x1062))) b(c(c(x1063))) -> b(b(b(x1063))) b(c(c(x1063))) -> a(b(c(x1063))) b(b(b(x1063))) -> a(b(b(x1063))) a(b(c(x1063))) -> a(b(b(x1063))) b(c(c(x1064))) -> b(b(b(x1064))) b(c(c(x1064))) -> b(b(c(x1064))) b(b(c(x1064))) -> b(b(b(x1064))) b(b(b(x1064))) -> b(a(b(x1064))) b(b(c(x1064))) -> b(a(b(x1064))) c(c(x)) -> b(b(x)) c(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(c(c(x1066))) -> c(b(b(x1066))) c(c(c(x1066))) -> a(b(c(x1066))) c(b(b(x1066))) -> c(c(b(x1066))) c(c(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> c(c(b(x1066))) c(c(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(a(x1066))) a(b(a(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> c(c(b(x1066))) c(c(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(c(c(x1066))) a(c(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> c(a(b(x1066))) c(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> c(a(b(x1066))) c(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(a(x1066))) a(b(a(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> c(a(b(x1066))) c(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(c(c(x1066))) a(c(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(b(b(x1066))) b(b(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(b(b(x1066))) b(b(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(a(x1066))) a(b(a(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(b(b(x1066))) b(b(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(c(c(x1066))) a(c(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(a(b(x1066))) b(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(a(b(x1066))) b(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(b(a(x1066))) a(b(a(x1066))) -> a(b(b(x1066))) c(b(b(x1066))) -> b(a(b(x1066))) b(a(b(x1066))) -> a(b(b(x1066))) a(b(c(x1066))) -> a(c(c(x1066))) a(c(c(x1066))) -> a(b(b(x1066))) c(b(b(x1067))) -> c(a(b(x1067))) c(b(b(x1067))) -> c(c(b(x1067))) c(a(b(x1067))) -> b(a(b(x1067))) c(c(b(x1067))) -> b(a(b(x1067))) c(a(b(x1067))) -> c(c(b(x1067))) c(a(b(x1067))) -> a(b(b(x1067))) c(c(b(x1067))) -> a(b(b(x1067))) c(a(b(x1067))) -> b(b(b(x1067))) c(c(b(x1067))) -> b(b(b(x1067))) b(b(b(x1068))) -> b(a(b(x1068))) b(b(b(x1068))) -> a(b(b(x1068))) b(a(b(x1068))) -> a(b(b(x1068))) c(b(b(x1069))) -> c(a(b(x1069))) c(b(b(x1069))) -> c(a(b(x1069))) c(b(b(x1070))) -> c(a(b(x1070))) c(b(b(x1070))) -> b(b(b(x1070))) c(a(b(x1070))) -> b(a(b(x1070))) b(b(b(x1070))) -> b(a(b(x1070))) c(a(b(x1070))) -> a(b(b(x1070))) b(b(b(x1070))) -> a(b(b(x1070))) c(a(b(x1070))) -> b(b(b(x1070))) c(b(b(x1071))) -> c(a(b(x1071))) c(b(b(x1071))) -> b(a(b(x1071))) c(a(b(x1071))) -> b(a(b(x1071))) c(a(b(x1071))) -> a(b(b(x1071))) b(a(b(x1071))) -> a(b(b(x1071))) c(a(b(x1071))) -> b(b(b(x1071))) b(a(b(x1071))) -> b(b(b(x1071))) c(a(x)) -> c(c(x)) c(a(x)) -> b(a(x)) c(c(x)) -> b(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(a(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(c(a(x1073))) -> b(c(c(x1073))) b(c(a(x1073))) -> b(a(a(x1073))) b(c(c(x1073))) -> b(b(a(x1073))) b(a(a(x1073))) -> b(b(a(x1073))) c(c(a(x1074))) -> c(c(c(x1074))) c(c(a(x1074))) -> b(b(a(x1074))) c(c(c(x1074))) -> c(b(b(x1074))) c(b(b(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> c(b(b(x1074))) c(b(b(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) b(a(b(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> b(b(c(x1074))) b(b(c(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> b(b(c(x1074))) b(b(c(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) b(a(b(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> b(b(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) b(a(b(x1074))) -> b(b(b(x1074))) c(c(c(x1074))) -> c(b(b(x1074))) c(b(b(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> c(b(b(x1074))) c(b(b(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) b(b(b(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> b(b(c(x1074))) b(b(c(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> b(b(c(x1074))) b(b(c(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) b(b(b(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> b(a(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) b(b(b(x1074))) -> b(a(b(x1074))) c(c(c(x1074))) -> b(b(c(x1074))) b(b(c(x1074))) -> b(b(a(x1074))) c(c(c(x1074))) -> c(b(a(x1074))) c(b(a(x1074))) -> b(b(a(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) b(a(b(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> a(b(a(x1074))) a(b(a(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> c(a(b(x1074))) c(a(b(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) b(b(b(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> a(b(c(x1074))) a(b(c(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> b(a(b(x1074))) b(a(b(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> a(b(c(x1074))) a(b(c(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> a(b(a(x1074))) a(b(a(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> a(b(c(x1074))) a(b(c(x1074))) -> a(b(b(x1074))) b(b(a(x1074))) -> b(b(b(x1074))) b(b(b(x1074))) -> a(b(b(x1074))) c(c(c(x1074))) -> a(b(c(x1074))) a(b(c(x1074))) -> a(b(a(x1074))) b(b(a(x1074))) -> a(b(a(x1074))) c(c(c(x1074))) -> a(b(c(x1074))) a(b(c(x1074))) -> a(a(b(x1074))) b(b(a(x1074))) -> a(b(a(x1074))) a(b(a(x1074))) -> a(a(b(x1074))) b(c(a(x1075))) -> b(c(c(x1075))) b(c(a(x1075))) -> c(c(a(x1075))) b(c(c(x1075))) -> c(c(c(x1075))) c(c(a(x1075))) -> c(c(c(x1075))) b(c(c(x1075))) -> b(b(a(x1075))) c(c(a(x1075))) -> b(b(a(x1075))) c(c(a(x1076))) -> c(c(c(x1076))) c(c(a(x1076))) -> b(a(a(x1076))) c(c(c(x1076))) -> c(b(b(x1076))) c(b(b(x1076))) -> b(b(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(b(b(x1076))) c(c(c(x1076))) -> b(b(c(x1076))) b(b(c(x1076))) -> b(b(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(b(b(x1076))) c(c(c(x1076))) -> c(a(b(x1076))) c(a(b(x1076))) -> b(b(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(b(b(x1076))) c(c(c(x1076))) -> c(b(b(x1076))) c(b(b(x1076))) -> b(a(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(a(b(x1076))) c(c(c(x1076))) -> b(b(c(x1076))) b(b(c(x1076))) -> b(a(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(a(b(x1076))) c(c(c(x1076))) -> c(a(b(x1076))) c(a(b(x1076))) -> b(a(b(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> b(a(b(x1076))) c(c(c(x1076))) -> b(b(c(x1076))) b(b(c(x1076))) -> b(b(a(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) c(c(c(x1076))) -> c(b(a(x1076))) c(b(a(x1076))) -> b(b(a(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) c(c(c(x1076))) -> c(b(a(x1076))) c(b(a(x1076))) -> b(a(a(x1076))) c(c(c(x1076))) -> c(a(b(x1076))) c(a(b(x1076))) -> a(b(b(x1076))) b(a(a(x1076))) -> a(b(a(x1076))) a(b(a(x1076))) -> a(b(b(x1076))) c(c(c(x1076))) -> a(b(c(x1076))) a(b(c(x1076))) -> a(b(b(x1076))) b(a(a(x1076))) -> a(b(a(x1076))) a(b(a(x1076))) -> a(b(b(x1076))) c(c(c(x1076))) -> a(b(c(x1076))) a(b(c(x1076))) -> a(b(a(x1076))) b(a(a(x1076))) -> a(b(a(x1076))) c(c(c(x1076))) -> a(b(c(x1076))) a(b(c(x1076))) -> a(b(a(x1076))) b(a(a(x1076))) -> b(b(a(x1076))) b(b(a(x1076))) -> a(b(a(x1076))) c(c(c(x1076))) -> a(b(c(x1076))) a(b(c(x1076))) -> a(a(b(x1076))) b(a(a(x1076))) -> a(b(a(x1076))) a(b(a(x1076))) -> a(a(b(x1076))) c(a(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) c(a(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(c(a(x1079))) -> b(c(c(x1079))) b(c(a(x1079))) -> a(b(a(x1079))) b(c(c(x1079))) -> b(b(b(x1079))) b(b(b(x1079))) -> a(b(b(x1079))) a(b(a(x1079))) -> a(b(b(x1079))) b(c(c(x1079))) -> a(b(c(x1079))) a(b(c(x1079))) -> a(b(b(x1079))) a(b(a(x1079))) -> a(b(b(x1079))) b(c(c(x1079))) -> b(a(b(x1079))) b(a(b(x1079))) -> a(b(b(x1079))) a(b(a(x1079))) -> a(b(b(x1079))) b(c(c(x1079))) -> b(b(a(x1079))) b(b(a(x1079))) -> a(b(a(x1079))) b(c(c(x1079))) -> a(b(c(x1079))) a(b(c(x1079))) -> a(b(a(x1079))) b(c(c(x1079))) -> a(b(c(x1079))) a(b(c(x1079))) -> a(a(b(x1079))) a(b(a(x1079))) -> a(a(b(x1079))) b(c(c(x1079))) -> a(b(c(x1079))) a(b(c(x1079))) -> a(a(b(x1079))) a(b(a(x1079))) -> a(b(b(x1079))) a(b(b(x1079))) -> a(a(b(x1079))) b(c(a(x1080))) -> b(c(c(x1080))) b(c(a(x1080))) -> b(b(a(x1080))) b(c(c(x1080))) -> b(b(b(x1080))) b(b(a(x1080))) -> b(b(b(x1080))) b(c(c(x1080))) -> b(b(a(x1080))) b(c(c(x1080))) -> b(a(b(x1080))) b(b(a(x1080))) -> b(a(b(x1080))) c(c(a(x1081))) -> c(c(c(x1081))) c(c(a(x1081))) -> a(b(a(x1081))) c(c(c(x1081))) -> c(a(b(x1081))) c(a(b(x1081))) -> a(b(b(x1081))) a(b(a(x1081))) -> a(b(b(x1081))) c(c(c(x1081))) -> a(b(c(x1081))) a(b(c(x1081))) -> a(b(b(x1081))) a(b(a(x1081))) -> a(b(b(x1081))) c(c(c(x1081))) -> a(b(c(x1081))) a(b(c(x1081))) -> a(b(a(x1081))) c(c(c(x1081))) -> a(b(c(x1081))) a(b(c(x1081))) -> a(a(b(x1081))) a(b(a(x1081))) -> a(a(b(x1081))) c(c(c(x1081))) -> a(b(c(x1081))) a(b(c(x1081))) -> a(a(b(x1081))) a(b(a(x1081))) -> a(b(b(x1081))) a(b(b(x1081))) -> a(a(b(x1081))) b(c(x)) -> c(c(x)) b(c(x)) -> b(a(x)) c(c(x)) -> b(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(a(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(b(c(x1083))) -> c(c(c(x1083))) c(b(c(x1083))) -> c(c(c(x1083))) b(b(c(x1084))) -> b(c(c(x1084))) b(b(c(x1084))) -> a(b(c(x1084))) b(c(c(x1084))) -> a(b(c(x1084))) c(b(c(x1085))) -> c(c(c(x1085))) c(b(c(x1085))) -> c(a(c(x1085))) c(a(c(x1085))) -> c(c(c(x1085))) c(c(c(x1085))) -> b(b(c(x1085))) c(a(c(x1085))) -> b(b(c(x1085))) c(c(c(x1085))) -> b(a(c(x1085))) c(a(c(x1085))) -> b(a(c(x1085))) c(c(c(x1085))) -> a(b(c(x1085))) c(a(c(x1085))) -> a(b(c(x1085))) b(c(x)) -> c(c(x)) b(c(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(c(x)) -> c(c(x)) b(c(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(b(c(x1088))) -> c(c(c(x1088))) c(b(c(x1088))) -> b(b(c(x1088))) c(c(c(x1088))) -> b(b(c(x1088))) c(c(c(x1088))) -> a(b(c(x1088))) b(b(c(x1088))) -> a(b(c(x1088))) c(b(c(x1089))) -> c(c(c(x1089))) c(b(c(x1089))) -> b(a(c(x1089))) c(c(c(x1089))) -> b(b(c(x1089))) b(a(c(x1089))) -> b(b(c(x1089))) c(c(c(x1089))) -> b(a(c(x1089))) c(c(c(x1089))) -> a(b(c(x1089))) b(a(c(x1089))) -> a(b(c(x1089))) b(a(x)) -> b(b(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(b(a(x1091))) -> c(b(b(x1091))) c(b(a(x1091))) -> c(c(a(x1091))) c(c(a(x1091))) -> c(b(b(x1091))) c(b(b(x1091))) -> c(a(b(x1091))) c(c(a(x1091))) -> c(a(b(x1091))) b(b(a(x1092))) -> b(b(b(x1092))) b(b(a(x1092))) -> a(b(a(x1092))) b(b(b(x1092))) -> a(b(b(x1092))) a(b(a(x1092))) -> a(b(b(x1092))) c(b(a(x1093))) -> c(b(b(x1093))) c(b(a(x1093))) -> c(a(a(x1093))) c(a(a(x1093))) -> c(c(a(x1093))) c(c(a(x1093))) -> c(b(b(x1093))) c(b(b(x1093))) -> c(a(b(x1093))) c(a(a(x1093))) -> c(c(a(x1093))) c(c(a(x1093))) -> c(a(b(x1093))) c(b(b(x1093))) -> b(b(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(b(b(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> b(b(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(b(b(x1093))) c(b(b(x1093))) -> c(a(b(x1093))) c(a(b(x1093))) -> b(b(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(b(b(x1093))) c(b(b(x1093))) -> b(a(b(x1093))) b(a(b(x1093))) -> b(b(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(b(b(x1093))) c(b(b(x1093))) -> b(a(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(a(b(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> b(a(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(a(b(x1093))) c(b(b(x1093))) -> c(a(b(x1093))) c(a(b(x1093))) -> b(a(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(a(b(x1093))) c(b(b(x1093))) -> b(b(b(x1093))) b(b(b(x1093))) -> b(a(b(x1093))) c(a(a(x1093))) -> b(b(a(x1093))) b(b(a(x1093))) -> b(a(b(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> c(c(c(x1093))) c(a(a(x1093))) -> c(c(a(x1093))) c(c(a(x1093))) -> c(c(c(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> c(c(a(x1093))) c(a(a(x1093))) -> c(c(a(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> c(b(a(x1093))) c(a(a(x1093))) -> c(c(a(x1093))) c(c(a(x1093))) -> c(b(a(x1093))) c(b(b(x1093))) -> c(c(b(x1093))) c(c(b(x1093))) -> a(b(b(x1093))) c(a(a(x1093))) -> a(b(a(x1093))) a(b(a(x1093))) -> a(b(b(x1093))) c(b(b(x1093))) -> c(a(b(x1093))) c(a(b(x1093))) -> a(b(b(x1093))) c(a(a(x1093))) -> a(b(a(x1093))) a(b(a(x1093))) -> a(b(b(x1093))) c(b(b(x1093))) -> b(b(b(x1093))) b(b(b(x1093))) -> a(b(b(x1093))) c(a(a(x1093))) -> a(b(a(x1093))) a(b(a(x1093))) -> a(b(b(x1093))) c(b(b(x1093))) -> b(a(b(x1093))) b(a(b(x1093))) -> a(b(b(x1093))) c(a(a(x1093))) -> a(b(a(x1093))) a(b(a(x1093))) -> a(b(b(x1093))) c(b(a(x1094))) -> c(b(b(x1094))) c(b(a(x1094))) -> b(b(a(x1094))) c(b(b(x1094))) -> b(b(b(x1094))) b(b(a(x1094))) -> b(b(b(x1094))) c(b(b(x1094))) -> b(a(b(x1094))) b(b(a(x1094))) -> b(a(b(x1094))) c(b(a(x1095))) -> c(b(b(x1095))) c(b(a(x1095))) -> b(a(a(x1095))) c(b(b(x1095))) -> b(b(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(b(b(x1095))) c(b(b(x1095))) -> c(c(b(x1095))) c(c(b(x1095))) -> b(b(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(b(b(x1095))) c(b(b(x1095))) -> c(a(b(x1095))) c(a(b(x1095))) -> b(b(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(b(b(x1095))) c(b(b(x1095))) -> b(a(b(x1095))) b(a(b(x1095))) -> b(b(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(b(b(x1095))) c(b(b(x1095))) -> b(a(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(a(b(x1095))) c(b(b(x1095))) -> c(c(b(x1095))) c(c(b(x1095))) -> b(a(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(a(b(x1095))) c(b(b(x1095))) -> c(a(b(x1095))) c(a(b(x1095))) -> b(a(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(a(b(x1095))) c(b(b(x1095))) -> b(b(b(x1095))) b(b(b(x1095))) -> b(a(b(x1095))) b(a(a(x1095))) -> b(b(a(x1095))) b(b(a(x1095))) -> b(a(b(x1095))) c(b(b(x1095))) -> c(c(b(x1095))) c(c(b(x1095))) -> a(b(b(x1095))) b(a(a(x1095))) -> a(b(a(x1095))) a(b(a(x1095))) -> a(b(b(x1095))) c(b(b(x1095))) -> c(a(b(x1095))) c(a(b(x1095))) -> a(b(b(x1095))) b(a(a(x1095))) -> a(b(a(x1095))) a(b(a(x1095))) -> a(b(b(x1095))) c(b(b(x1095))) -> b(b(b(x1095))) b(b(b(x1095))) -> a(b(b(x1095))) b(a(a(x1095))) -> a(b(a(x1095))) a(b(a(x1095))) -> a(b(b(x1095))) c(b(b(x1095))) -> b(a(b(x1095))) b(a(b(x1095))) -> a(b(b(x1095))) b(a(a(x1095))) -> a(b(a(x1095))) a(b(a(x1095))) -> a(b(b(x1095))) b(c(b(x1096))) -> b(c(a(x1096))) b(c(b(x1096))) -> b(a(b(x1096))) b(c(a(x1096))) -> b(a(b(x1096))) b(c(a(x1096))) -> b(b(b(x1096))) b(a(b(x1096))) -> b(b(b(x1096))) c(b(x)) -> c(a(x)) c(b(x)) -> c(c(x)) c(a(x)) -> b(a(x)) c(c(x)) -> b(a(x)) c(a(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(a(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(c(b(x1098))) -> c(c(a(x1098))) c(c(b(x1098))) -> b(b(b(x1098))) c(c(a(x1098))) -> b(b(a(x1098))) b(b(a(x1098))) -> b(a(b(x1098))) b(b(b(x1098))) -> b(a(b(x1098))) c(c(a(x1098))) -> c(a(b(x1098))) c(a(b(x1098))) -> b(a(b(x1098))) b(b(b(x1098))) -> b(a(b(x1098))) c(c(a(x1098))) -> c(b(b(x1098))) c(b(b(x1098))) -> b(a(b(x1098))) b(b(b(x1098))) -> b(a(b(x1098))) c(c(a(x1098))) -> b(b(a(x1098))) b(b(a(x1098))) -> b(b(b(x1098))) c(c(a(x1098))) -> c(a(b(x1098))) c(a(b(x1098))) -> b(b(b(x1098))) c(c(a(x1098))) -> c(b(b(x1098))) c(b(b(x1098))) -> b(b(b(x1098))) c(c(a(x1098))) -> c(a(b(x1098))) c(a(b(x1098))) -> a(b(b(x1098))) b(b(b(x1098))) -> a(b(b(x1098))) c(c(a(x1098))) -> c(a(b(x1098))) c(a(b(x1098))) -> a(b(b(x1098))) b(b(b(x1098))) -> b(a(b(x1098))) b(a(b(x1098))) -> a(b(b(x1098))) c(c(a(x1098))) -> a(b(a(x1098))) a(b(a(x1098))) -> a(b(b(x1098))) b(b(b(x1098))) -> a(b(b(x1098))) c(c(a(x1098))) -> a(b(a(x1098))) a(b(a(x1098))) -> a(b(b(x1098))) b(b(b(x1098))) -> b(a(b(x1098))) b(a(b(x1098))) -> a(b(b(x1098))) c(c(a(x1098))) -> a(b(a(x1098))) a(b(a(x1098))) -> a(a(b(x1098))) b(b(b(x1098))) -> a(b(b(x1098))) a(b(b(x1098))) -> a(a(b(x1098))) b(c(b(x1099))) -> b(c(a(x1099))) b(c(b(x1099))) -> c(c(b(x1099))) b(c(a(x1099))) -> c(c(a(x1099))) c(c(b(x1099))) -> c(c(a(x1099))) b(c(a(x1099))) -> b(a(b(x1099))) c(c(b(x1099))) -> b(a(b(x1099))) b(c(a(x1099))) -> b(b(b(x1099))) c(c(b(x1099))) -> b(b(b(x1099))) c(c(b(x1100))) -> c(c(a(x1100))) c(c(b(x1100))) -> b(a(b(x1100))) c(c(a(x1100))) -> b(b(a(x1100))) b(b(a(x1100))) -> b(a(b(x1100))) c(c(a(x1100))) -> c(a(b(x1100))) c(a(b(x1100))) -> b(a(b(x1100))) c(c(a(x1100))) -> c(b(b(x1100))) c(b(b(x1100))) -> b(a(b(x1100))) c(c(a(x1100))) -> b(b(a(x1100))) b(b(a(x1100))) -> b(b(b(x1100))) b(a(b(x1100))) -> b(b(b(x1100))) c(c(a(x1100))) -> c(a(b(x1100))) c(a(b(x1100))) -> b(b(b(x1100))) b(a(b(x1100))) -> b(b(b(x1100))) c(c(a(x1100))) -> c(b(b(x1100))) c(b(b(x1100))) -> b(b(b(x1100))) b(a(b(x1100))) -> b(b(b(x1100))) c(c(a(x1100))) -> c(a(b(x1100))) c(a(b(x1100))) -> a(b(b(x1100))) b(a(b(x1100))) -> a(b(b(x1100))) c(c(a(x1100))) -> c(a(b(x1100))) c(a(b(x1100))) -> a(b(b(x1100))) b(a(b(x1100))) -> b(b(b(x1100))) b(b(b(x1100))) -> a(b(b(x1100))) c(c(a(x1100))) -> a(b(a(x1100))) a(b(a(x1100))) -> a(b(b(x1100))) b(a(b(x1100))) -> a(b(b(x1100))) c(c(a(x1100))) -> a(b(a(x1100))) a(b(a(x1100))) -> a(b(b(x1100))) b(a(b(x1100))) -> b(b(b(x1100))) b(b(b(x1100))) -> a(b(b(x1100))) c(c(a(x1100))) -> a(b(a(x1100))) a(b(a(x1100))) -> a(a(b(x1100))) b(a(b(x1100))) -> a(b(b(x1100))) a(b(b(x1100))) -> a(a(b(x1100))) b(c(b(x1101))) -> b(c(a(x1101))) b(c(b(x1101))) -> a(b(b(x1101))) b(c(a(x1101))) -> b(a(b(x1101))) b(a(b(x1101))) -> a(b(b(x1101))) b(c(a(x1101))) -> b(b(b(x1101))) b(b(b(x1101))) -> a(b(b(x1101))) b(c(a(x1101))) -> a(b(a(x1101))) a(b(a(x1101))) -> a(b(b(x1101))) b(c(a(x1101))) -> a(b(a(x1101))) a(b(a(x1101))) -> a(a(b(x1101))) a(b(b(x1101))) -> a(a(b(x1101))) b(c(b(x1102))) -> b(c(a(x1102))) b(c(b(x1102))) -> b(b(b(x1102))) b(c(a(x1102))) -> b(a(b(x1102))) b(b(b(x1102))) -> b(a(b(x1102))) b(c(a(x1102))) -> b(b(b(x1102))) c(b(x)) -> c(a(x)) c(b(x)) -> b(b(x)) c(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(a(x)) -> b(b(x)) c(b(x)) -> c(a(x)) c(b(x)) -> b(a(x)) c(a(x)) -> b(a(x)) c(a(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(a(x)) -> b(b(x)) b(a(x)) -> b(b(x)) c(c(b(x1105))) -> c(c(a(x1105))) c(c(b(x1105))) -> a(b(b(x1105))) c(c(a(x1105))) -> c(a(b(x1105))) c(a(b(x1105))) -> a(b(b(x1105))) c(c(a(x1105))) -> a(b(a(x1105))) a(b(a(x1105))) -> a(b(b(x1105))) c(c(a(x1105))) -> a(b(a(x1105))) a(b(a(x1105))) -> a(a(b(x1105))) a(b(b(x1105))) -> a(a(b(x1105))) b(c(c(x1106))) -> b(b(a(x1106))) b(c(c(x1106))) -> b(a(c(x1106))) b(a(c(x1106))) -> b(b(c(x1106))) b(b(c(x1106))) -> b(b(a(x1106))) b(b(a(x1106))) -> b(a(b(x1106))) b(a(c(x1106))) -> b(b(c(x1106))) b(b(c(x1106))) -> b(a(b(x1106))) b(b(a(x1106))) -> b(b(b(x1106))) b(b(b(x1106))) -> b(a(b(x1106))) b(a(c(x1106))) -> b(b(c(x1106))) b(b(c(x1106))) -> b(a(b(x1106))) b(b(a(x1106))) -> a(b(a(x1106))) b(a(c(x1106))) -> a(b(c(x1106))) a(b(c(x1106))) -> a(b(a(x1106))) b(b(a(x1106))) -> b(b(b(x1106))) b(a(c(x1106))) -> b(b(c(x1106))) b(b(c(x1106))) -> b(b(b(x1106))) b(b(a(x1106))) -> b(a(b(x1106))) b(a(b(x1106))) -> b(b(b(x1106))) b(a(c(x1106))) -> b(b(c(x1106))) b(b(c(x1106))) -> b(b(b(x1106))) b(b(a(x1106))) -> b(a(b(x1106))) b(a(b(x1106))) -> a(b(b(x1106))) b(a(c(x1106))) -> a(b(c(x1106))) a(b(c(x1106))) -> a(b(b(x1106))) b(b(a(x1106))) -> a(b(a(x1106))) a(b(a(x1106))) -> a(b(b(x1106))) b(a(c(x1106))) -> a(b(c(x1106))) a(b(c(x1106))) -> a(b(b(x1106))) b(b(a(x1106))) -> b(b(b(x1106))) b(b(b(x1106))) -> a(b(b(x1106))) b(a(c(x1106))) -> a(b(c(x1106))) a(b(c(x1106))) -> a(b(b(x1106))) b(b(a(x1106))) -> a(b(a(x1106))) a(b(a(x1106))) -> a(a(b(x1106))) b(a(c(x1106))) -> a(b(c(x1106))) a(b(c(x1106))) -> a(a(b(x1106))) c(c(x)) -> b(a(x)) c(c(x)) -> b(b(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(c(c(x1108))) -> c(b(a(x1108))) c(c(c(x1108))) -> b(b(c(x1108))) c(b(a(x1108))) -> b(b(a(x1108))) b(b(c(x1108))) -> b(b(a(x1108))) b(c(c(x1109))) -> b(b(a(x1109))) b(c(c(x1109))) -> c(c(c(x1109))) c(c(c(x1109))) -> b(b(c(x1109))) b(b(c(x1109))) -> b(b(a(x1109))) c(c(c(x1109))) -> c(b(a(x1109))) c(b(a(x1109))) -> b(b(a(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> c(b(b(x1109))) c(b(b(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> b(b(c(x1109))) b(b(c(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) b(b(b(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> c(b(b(x1109))) c(b(b(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) b(b(b(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> b(b(c(x1109))) b(b(c(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) b(b(b(x1109))) -> b(a(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> b(a(b(x1109))) b(b(a(x1109))) -> a(b(a(x1109))) c(c(c(x1109))) -> a(b(c(x1109))) a(b(c(x1109))) -> a(b(a(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> c(b(b(x1109))) c(b(b(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> b(b(c(x1109))) b(b(c(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) b(a(b(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> c(b(b(x1109))) c(b(b(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) b(a(b(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> b(b(c(x1109))) b(b(c(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) b(a(b(x1109))) -> b(b(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> b(b(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) b(a(b(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> b(a(b(x1109))) b(a(b(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> a(b(c(x1109))) a(b(c(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> a(b(a(x1109))) a(b(a(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> a(b(a(x1109))) a(b(a(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> a(b(c(x1109))) a(b(c(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) b(b(b(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> c(a(b(x1109))) c(a(b(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> b(b(b(x1109))) b(b(b(x1109))) -> a(b(b(x1109))) c(c(c(x1109))) -> a(b(c(x1109))) a(b(c(x1109))) -> a(b(b(x1109))) b(b(a(x1109))) -> a(b(a(x1109))) a(b(a(x1109))) -> a(a(b(x1109))) c(c(c(x1109))) -> a(b(c(x1109))) a(b(c(x1109))) -> a(a(b(x1109))) c(c(c(x1110))) -> c(b(a(x1110))) c(c(c(x1110))) -> b(a(c(x1110))) c(b(a(x1110))) -> b(b(a(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(a(x1110))) c(b(a(x1110))) -> c(c(a(x1110))) c(c(a(x1110))) -> b(b(a(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(a(x1110))) c(b(a(x1110))) -> c(a(a(x1110))) c(a(a(x1110))) -> b(b(a(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(a(x1110))) c(b(a(x1110))) -> b(a(a(x1110))) b(a(a(x1110))) -> b(b(a(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(a(x1110))) c(b(a(x1110))) -> c(a(b(x1110))) c(a(b(x1110))) -> b(a(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(a(b(x1110))) c(b(a(x1110))) -> c(b(b(x1110))) c(b(b(x1110))) -> b(a(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(a(b(x1110))) c(b(a(x1110))) -> b(b(a(x1110))) b(b(a(x1110))) -> b(a(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(a(b(x1110))) c(b(a(x1110))) -> c(a(b(x1110))) c(a(b(x1110))) -> a(b(b(x1110))) b(a(c(x1110))) -> a(b(c(x1110))) a(b(c(x1110))) -> a(b(b(x1110))) c(b(a(x1110))) -> c(a(b(x1110))) c(a(b(x1110))) -> b(b(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(b(x1110))) c(b(a(x1110))) -> c(b(b(x1110))) c(b(b(x1110))) -> b(b(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(b(x1110))) c(b(a(x1110))) -> b(b(a(x1110))) b(b(a(x1110))) -> b(b(b(x1110))) b(a(c(x1110))) -> b(b(c(x1110))) b(b(c(x1110))) -> b(b(b(x1110))) c(b(a(x1110))) -> c(c(a(x1110))) c(c(a(x1110))) -> a(b(a(x1110))) b(a(c(x1110))) -> a(b(c(x1110))) a(b(c(x1110))) -> a(b(a(x1110))) c(b(a(x1110))) -> c(a(a(x1110))) c(a(a(x1110))) -> a(b(a(x1110))) b(a(c(x1110))) -> a(b(c(x1110))) a(b(c(x1110))) -> a(b(a(x1110))) c(b(a(x1110))) -> b(b(a(x1110))) b(b(a(x1110))) -> a(b(a(x1110))) b(a(c(x1110))) -> a(b(c(x1110))) a(b(c(x1110))) -> a(b(a(x1110))) c(b(a(x1110))) -> b(a(a(x1110))) b(a(a(x1110))) -> a(b(a(x1110))) b(a(c(x1110))) -> a(b(c(x1110))) a(b(c(x1110))) -> a(b(a(x1110))) b(c(c(x1111))) -> b(b(a(x1111))) b(c(c(x1111))) -> a(b(c(x1111))) b(b(a(x1111))) -> a(b(a(x1111))) a(b(c(x1111))) -> a(b(a(x1111))) b(c(c(x1112))) -> b(b(a(x1112))) b(c(c(x1112))) -> b(b(c(x1112))) b(b(c(x1112))) -> b(b(a(x1112))) b(b(a(x1112))) -> b(a(b(x1112))) b(b(c(x1112))) -> b(a(b(x1112))) b(b(a(x1112))) -> b(b(b(x1112))) b(b(c(x1112))) -> b(b(b(x1112))) c(c(x)) -> b(a(x)) c(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(c(c(x1114))) -> c(b(a(x1114))) c(c(c(x1114))) -> a(b(c(x1114))) c(b(a(x1114))) -> c(a(b(x1114))) c(a(b(x1114))) -> a(b(b(x1114))) a(b(c(x1114))) -> a(b(b(x1114))) c(b(a(x1114))) -> c(a(b(x1114))) c(a(b(x1114))) -> a(b(b(x1114))) a(b(c(x1114))) -> a(b(a(x1114))) a(b(a(x1114))) -> a(b(b(x1114))) c(b(a(x1114))) -> c(a(b(x1114))) c(a(b(x1114))) -> a(b(b(x1114))) a(b(c(x1114))) -> a(c(c(x1114))) a(c(c(x1114))) -> a(b(b(x1114))) c(b(a(x1114))) -> c(c(a(x1114))) c(c(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> c(c(a(x1114))) c(c(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(c(c(x1114))) a(c(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> c(a(a(x1114))) c(a(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> c(a(a(x1114))) c(a(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(c(c(x1114))) a(c(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> b(b(a(x1114))) b(b(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> b(b(a(x1114))) b(b(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(c(c(x1114))) a(c(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> b(a(a(x1114))) b(a(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(b(a(x1114))) c(b(a(x1114))) -> b(a(a(x1114))) b(a(a(x1114))) -> a(b(a(x1114))) a(b(c(x1114))) -> a(c(c(x1114))) a(c(c(x1114))) -> a(b(a(x1114))) c(a(x)) -> a(b(x)) c(a(x)) -> b(a(x)) b(a(x)) -> a(b(x)) b(c(a(x1116))) -> b(a(b(x1116))) b(c(a(x1116))) -> b(a(a(x1116))) b(a(a(x1116))) -> b(b(a(x1116))) b(b(a(x1116))) -> b(a(b(x1116))) b(a(b(x1116))) -> a(b(b(x1116))) b(a(a(x1116))) -> a(b(a(x1116))) a(b(a(x1116))) -> a(b(b(x1116))) b(a(b(x1116))) -> b(b(b(x1116))) b(b(b(x1116))) -> a(b(b(x1116))) b(a(a(x1116))) -> a(b(a(x1116))) a(b(a(x1116))) -> a(b(b(x1116))) b(a(b(x1116))) -> b(b(b(x1116))) b(a(a(x1116))) -> b(b(a(x1116))) b(b(a(x1116))) -> b(b(b(x1116))) b(a(b(x1116))) -> a(b(b(x1116))) a(b(b(x1116))) -> a(a(b(x1116))) b(a(a(x1116))) -> a(b(a(x1116))) a(b(a(x1116))) -> a(a(b(x1116))) c(c(a(x1117))) -> c(a(b(x1117))) c(c(a(x1117))) -> b(b(a(x1117))) c(a(b(x1117))) -> b(a(b(x1117))) b(b(a(x1117))) -> b(a(b(x1117))) c(a(b(x1117))) -> b(b(b(x1117))) b(b(a(x1117))) -> b(b(b(x1117))) c(a(x)) -> a(b(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(b(x)) b(c(a(x1119))) -> b(a(b(x1119))) b(c(a(x1119))) -> c(c(a(x1119))) c(c(a(x1119))) -> b(b(a(x1119))) b(b(a(x1119))) -> b(a(b(x1119))) c(c(a(x1119))) -> c(a(b(x1119))) c(a(b(x1119))) -> b(a(b(x1119))) c(c(a(x1119))) -> c(b(b(x1119))) c(b(b(x1119))) -> b(a(b(x1119))) b(a(b(x1119))) -> a(b(b(x1119))) c(c(a(x1119))) -> c(a(b(x1119))) c(a(b(x1119))) -> a(b(b(x1119))) b(a(b(x1119))) -> a(b(b(x1119))) c(c(a(x1119))) -> a(b(a(x1119))) a(b(a(x1119))) -> a(b(b(x1119))) b(a(b(x1119))) -> b(b(b(x1119))) b(b(b(x1119))) -> a(b(b(x1119))) c(c(a(x1119))) -> c(a(b(x1119))) c(a(b(x1119))) -> a(b(b(x1119))) b(a(b(x1119))) -> b(b(b(x1119))) b(b(b(x1119))) -> a(b(b(x1119))) c(c(a(x1119))) -> a(b(a(x1119))) a(b(a(x1119))) -> a(b(b(x1119))) b(a(b(x1119))) -> b(b(b(x1119))) c(c(a(x1119))) -> b(b(a(x1119))) b(b(a(x1119))) -> b(b(b(x1119))) b(a(b(x1119))) -> b(b(b(x1119))) c(c(a(x1119))) -> c(a(b(x1119))) c(a(b(x1119))) -> b(b(b(x1119))) b(a(b(x1119))) -> b(b(b(x1119))) c(c(a(x1119))) -> c(b(b(x1119))) c(b(b(x1119))) -> b(b(b(x1119))) b(a(b(x1119))) -> a(b(b(x1119))) a(b(b(x1119))) -> a(a(b(x1119))) c(c(a(x1119))) -> a(b(a(x1119))) a(b(a(x1119))) -> a(a(b(x1119))) c(c(a(x1120))) -> c(a(b(x1120))) c(c(a(x1120))) -> b(a(a(x1120))) c(a(b(x1120))) -> b(a(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(a(b(x1120))) c(a(b(x1120))) -> c(c(b(x1120))) c(c(b(x1120))) -> b(a(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(a(b(x1120))) c(a(b(x1120))) -> b(b(b(x1120))) b(b(b(x1120))) -> b(a(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(a(b(x1120))) c(a(b(x1120))) -> a(b(b(x1120))) b(a(a(x1120))) -> a(b(a(x1120))) a(b(a(x1120))) -> a(b(b(x1120))) c(a(b(x1120))) -> b(a(b(x1120))) b(a(b(x1120))) -> a(b(b(x1120))) b(a(a(x1120))) -> a(b(a(x1120))) a(b(a(x1120))) -> a(b(b(x1120))) c(a(b(x1120))) -> c(c(b(x1120))) c(c(b(x1120))) -> a(b(b(x1120))) b(a(a(x1120))) -> a(b(a(x1120))) a(b(a(x1120))) -> a(b(b(x1120))) c(a(b(x1120))) -> b(b(b(x1120))) b(b(b(x1120))) -> a(b(b(x1120))) b(a(a(x1120))) -> a(b(a(x1120))) a(b(a(x1120))) -> a(b(b(x1120))) c(a(b(x1120))) -> b(b(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(b(b(x1120))) c(a(b(x1120))) -> b(a(b(x1120))) b(a(b(x1120))) -> b(b(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(b(b(x1120))) c(a(b(x1120))) -> c(c(b(x1120))) c(c(b(x1120))) -> b(b(b(x1120))) b(a(a(x1120))) -> b(b(a(x1120))) b(b(a(x1120))) -> b(b(b(x1120))) c(a(b(x1120))) -> a(b(b(x1120))) a(b(b(x1120))) -> a(a(b(x1120))) b(a(a(x1120))) -> a(b(a(x1120))) a(b(a(x1120))) -> a(a(b(x1120))) c(a(x)) -> a(b(x)) c(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(c(a(x1122))) -> b(a(b(x1122))) b(c(a(x1122))) -> a(b(a(x1122))) b(a(b(x1122))) -> a(b(b(x1122))) a(b(a(x1122))) -> a(b(b(x1122))) b(c(a(x1123))) -> b(a(b(x1123))) b(c(a(x1123))) -> b(b(a(x1123))) b(b(a(x1123))) -> b(a(b(x1123))) b(a(b(x1123))) -> b(b(b(x1123))) b(b(a(x1123))) -> b(b(b(x1123))) c(c(a(x1124))) -> c(a(b(x1124))) c(c(a(x1124))) -> a(b(a(x1124))) c(a(b(x1124))) -> a(b(b(x1124))) a(b(a(x1124))) -> a(b(b(x1124))) c(a(x)) -> b(b(x)) c(a(x)) -> b(a(x)) b(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) b(c(a(x1126))) -> b(b(b(x1126))) b(c(a(x1126))) -> b(a(a(x1126))) b(a(a(x1126))) -> b(b(a(x1126))) b(b(a(x1126))) -> b(b(b(x1126))) b(b(b(x1126))) -> b(a(b(x1126))) b(a(a(x1126))) -> b(b(a(x1126))) b(b(a(x1126))) -> b(a(b(x1126))) b(b(b(x1126))) -> a(b(b(x1126))) b(a(a(x1126))) -> a(b(a(x1126))) a(b(a(x1126))) -> a(b(b(x1126))) b(b(b(x1126))) -> b(a(b(x1126))) b(a(b(x1126))) -> a(b(b(x1126))) b(a(a(x1126))) -> a(b(a(x1126))) a(b(a(x1126))) -> a(b(b(x1126))) b(b(b(x1126))) -> a(b(b(x1126))) a(b(b(x1126))) -> a(a(b(x1126))) b(a(a(x1126))) -> a(b(a(x1126))) a(b(a(x1126))) -> a(a(b(x1126))) c(c(a(x1127))) -> c(b(b(x1127))) c(c(a(x1127))) -> b(b(a(x1127))) c(b(b(x1127))) -> b(b(b(x1127))) b(b(a(x1127))) -> b(b(b(x1127))) c(b(b(x1127))) -> b(a(b(x1127))) b(b(a(x1127))) -> b(a(b(x1127))) c(a(x)) -> b(b(x)) c(a(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(c(a(x1129))) -> b(b(b(x1129))) b(c(a(x1129))) -> c(c(a(x1129))) c(c(a(x1129))) -> b(b(a(x1129))) b(b(a(x1129))) -> b(b(b(x1129))) c(c(a(x1129))) -> c(a(b(x1129))) c(a(b(x1129))) -> b(b(b(x1129))) c(c(a(x1129))) -> c(b(b(x1129))) c(b(b(x1129))) -> b(b(b(x1129))) b(b(b(x1129))) -> b(a(b(x1129))) c(c(a(x1129))) -> b(b(a(x1129))) b(b(a(x1129))) -> b(a(b(x1129))) b(b(b(x1129))) -> b(a(b(x1129))) c(c(a(x1129))) -> c(a(b(x1129))) c(a(b(x1129))) -> b(a(b(x1129))) b(b(b(x1129))) -> b(a(b(x1129))) c(c(a(x1129))) -> c(b(b(x1129))) c(b(b(x1129))) -> b(a(b(x1129))) b(b(b(x1129))) -> a(b(b(x1129))) c(c(a(x1129))) -> c(a(b(x1129))) c(a(b(x1129))) -> a(b(b(x1129))) b(b(b(x1129))) -> a(b(b(x1129))) c(c(a(x1129))) -> a(b(a(x1129))) a(b(a(x1129))) -> a(b(b(x1129))) b(b(b(x1129))) -> b(a(b(x1129))) b(a(b(x1129))) -> a(b(b(x1129))) c(c(a(x1129))) -> c(a(b(x1129))) c(a(b(x1129))) -> a(b(b(x1129))) b(b(b(x1129))) -> b(a(b(x1129))) b(a(b(x1129))) -> a(b(b(x1129))) c(c(a(x1129))) -> a(b(a(x1129))) a(b(a(x1129))) -> a(b(b(x1129))) b(b(b(x1129))) -> a(b(b(x1129))) a(b(b(x1129))) -> a(a(b(x1129))) c(c(a(x1129))) -> a(b(a(x1129))) a(b(a(x1129))) -> a(a(b(x1129))) c(c(a(x1130))) -> c(b(b(x1130))) c(c(a(x1130))) -> b(a(a(x1130))) c(b(b(x1130))) -> b(b(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(b(b(x1130))) c(b(b(x1130))) -> c(c(b(x1130))) c(c(b(x1130))) -> b(b(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(b(b(x1130))) c(b(b(x1130))) -> c(a(b(x1130))) c(a(b(x1130))) -> b(b(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(b(b(x1130))) c(b(b(x1130))) -> b(a(b(x1130))) b(a(b(x1130))) -> b(b(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(b(b(x1130))) c(b(b(x1130))) -> b(a(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(a(b(x1130))) c(b(b(x1130))) -> c(c(b(x1130))) c(c(b(x1130))) -> b(a(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(a(b(x1130))) c(b(b(x1130))) -> c(a(b(x1130))) c(a(b(x1130))) -> b(a(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(a(b(x1130))) c(b(b(x1130))) -> b(b(b(x1130))) b(b(b(x1130))) -> b(a(b(x1130))) b(a(a(x1130))) -> b(b(a(x1130))) b(b(a(x1130))) -> b(a(b(x1130))) c(b(b(x1130))) -> c(c(b(x1130))) c(c(b(x1130))) -> a(b(b(x1130))) b(a(a(x1130))) -> a(b(a(x1130))) a(b(a(x1130))) -> a(b(b(x1130))) c(b(b(x1130))) -> c(a(b(x1130))) c(a(b(x1130))) -> a(b(b(x1130))) b(a(a(x1130))) -> a(b(a(x1130))) a(b(a(x1130))) -> a(b(b(x1130))) c(b(b(x1130))) -> b(b(b(x1130))) b(b(b(x1130))) -> a(b(b(x1130))) b(a(a(x1130))) -> a(b(a(x1130))) a(b(a(x1130))) -> a(b(b(x1130))) c(b(b(x1130))) -> b(a(b(x1130))) b(a(b(x1130))) -> a(b(b(x1130))) b(a(a(x1130))) -> a(b(a(x1130))) a(b(a(x1130))) -> a(b(b(x1130))) c(a(x)) -> b(b(x)) c(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(c(a(x1132))) -> b(b(b(x1132))) b(c(a(x1132))) -> a(b(a(x1132))) b(b(b(x1132))) -> a(b(b(x1132))) a(b(a(x1132))) -> a(b(b(x1132))) b(c(a(x1133))) -> b(b(b(x1133))) b(c(a(x1133))) -> b(b(a(x1133))) b(b(a(x1133))) -> b(b(b(x1133))) b(b(b(x1133))) -> b(a(b(x1133))) b(b(a(x1133))) -> b(a(b(x1133))) c(c(a(x1134))) -> c(b(b(x1134))) c(c(a(x1134))) -> a(b(a(x1134))) c(b(b(x1134))) -> c(c(b(x1134))) c(c(b(x1134))) -> a(b(b(x1134))) a(b(a(x1134))) -> a(b(b(x1134))) c(b(b(x1134))) -> c(a(b(x1134))) c(a(b(x1134))) -> a(b(b(x1134))) a(b(a(x1134))) -> a(b(b(x1134))) c(b(b(x1134))) -> b(b(b(x1134))) b(b(b(x1134))) -> a(b(b(x1134))) a(b(a(x1134))) -> a(b(b(x1134))) c(b(b(x1134))) -> b(a(b(x1134))) b(a(b(x1134))) -> a(b(b(x1134))) a(b(a(x1134))) -> a(b(b(x1134))) b(c(x)) -> a(b(x)) b(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(b(c(x1136))) -> c(a(b(x1136))) c(b(c(x1136))) -> c(c(c(x1136))) c(c(c(x1136))) -> c(a(b(x1136))) b(b(c(x1137))) -> b(a(b(x1137))) b(b(c(x1137))) -> a(b(c(x1137))) b(a(b(x1137))) -> a(b(b(x1137))) a(b(c(x1137))) -> a(b(b(x1137))) b(c(x)) -> a(b(x)) b(c(x)) -> c(c(x)) c(c(x)) -> a(b(x)) c(b(c(x1139))) -> c(a(b(x1139))) c(b(c(x1139))) -> c(a(c(x1139))) c(a(c(x1139))) -> c(c(c(x1139))) c(c(c(x1139))) -> c(a(b(x1139))) c(a(b(x1139))) -> b(a(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(a(b(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> b(a(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(a(b(x1139))) c(a(b(x1139))) -> b(b(b(x1139))) b(b(b(x1139))) -> b(a(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(a(b(x1139))) c(a(b(x1139))) -> a(b(b(x1139))) c(a(c(x1139))) -> a(b(c(x1139))) a(b(c(x1139))) -> a(b(b(x1139))) c(a(b(x1139))) -> b(a(b(x1139))) b(a(b(x1139))) -> a(b(b(x1139))) c(a(c(x1139))) -> a(b(c(x1139))) a(b(c(x1139))) -> a(b(b(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> a(b(b(x1139))) c(a(c(x1139))) -> a(b(c(x1139))) a(b(c(x1139))) -> a(b(b(x1139))) c(a(b(x1139))) -> b(b(b(x1139))) b(b(b(x1139))) -> a(b(b(x1139))) c(a(c(x1139))) -> a(b(c(x1139))) a(b(c(x1139))) -> a(b(b(x1139))) c(a(b(x1139))) -> b(b(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(b(b(x1139))) c(a(b(x1139))) -> b(a(b(x1139))) b(a(b(x1139))) -> b(b(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(b(b(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> b(b(b(x1139))) c(a(c(x1139))) -> b(b(c(x1139))) b(b(c(x1139))) -> b(b(b(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> c(c(c(x1139))) c(a(c(x1139))) -> c(c(c(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> c(b(b(x1139))) c(a(c(x1139))) -> c(c(c(x1139))) c(c(c(x1139))) -> c(b(b(x1139))) c(a(b(x1139))) -> c(c(b(x1139))) c(c(b(x1139))) -> c(b(a(x1139))) c(a(c(x1139))) -> c(c(c(x1139))) c(c(c(x1139))) -> c(b(a(x1139))) c(a(b(x1139))) -> a(b(b(x1139))) a(b(b(x1139))) -> a(a(b(x1139))) c(a(c(x1139))) -> a(b(c(x1139))) a(b(c(x1139))) -> a(a(b(x1139))) b(c(x)) -> a(b(x)) b(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(b(c(x1141))) -> c(a(b(x1141))) c(b(c(x1141))) -> b(b(c(x1141))) c(a(b(x1141))) -> b(a(b(x1141))) b(b(c(x1141))) -> b(a(b(x1141))) c(a(b(x1141))) -> b(b(b(x1141))) b(b(c(x1141))) -> b(b(b(x1141))) c(b(c(x1142))) -> c(a(b(x1142))) c(b(c(x1142))) -> b(a(c(x1142))) c(a(b(x1142))) -> b(a(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(a(b(x1142))) c(a(b(x1142))) -> c(c(b(x1142))) c(c(b(x1142))) -> b(a(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(a(b(x1142))) c(a(b(x1142))) -> b(b(b(x1142))) b(b(b(x1142))) -> b(a(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(a(b(x1142))) c(a(b(x1142))) -> a(b(b(x1142))) b(a(c(x1142))) -> a(b(c(x1142))) a(b(c(x1142))) -> a(b(b(x1142))) c(a(b(x1142))) -> b(a(b(x1142))) b(a(b(x1142))) -> a(b(b(x1142))) b(a(c(x1142))) -> a(b(c(x1142))) a(b(c(x1142))) -> a(b(b(x1142))) c(a(b(x1142))) -> c(c(b(x1142))) c(c(b(x1142))) -> a(b(b(x1142))) b(a(c(x1142))) -> a(b(c(x1142))) a(b(c(x1142))) -> a(b(b(x1142))) c(a(b(x1142))) -> b(b(b(x1142))) b(b(b(x1142))) -> a(b(b(x1142))) b(a(c(x1142))) -> a(b(c(x1142))) a(b(c(x1142))) -> a(b(b(x1142))) c(a(b(x1142))) -> b(b(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(b(b(x1142))) c(a(b(x1142))) -> b(a(b(x1142))) b(a(b(x1142))) -> b(b(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(b(b(x1142))) c(a(b(x1142))) -> c(c(b(x1142))) c(c(b(x1142))) -> b(b(b(x1142))) b(a(c(x1142))) -> b(b(c(x1142))) b(b(c(x1142))) -> b(b(b(x1142))) c(a(b(x1142))) -> a(b(b(x1142))) a(b(b(x1142))) -> a(a(b(x1142))) b(a(c(x1142))) -> a(b(c(x1142))) a(b(c(x1142))) -> a(a(b(x1142))) b(c(x)) -> b(b(x)) b(c(x)) -> b(a(x)) b(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(b(c(x1144))) -> c(b(b(x1144))) c(b(c(x1144))) -> c(c(c(x1144))) c(c(c(x1144))) -> c(b(b(x1144))) c(b(b(x1144))) -> c(a(b(x1144))) c(c(c(x1144))) -> c(a(b(x1144))) b(b(c(x1145))) -> b(b(b(x1145))) b(b(c(x1145))) -> a(b(c(x1145))) b(b(b(x1145))) -> a(b(b(x1145))) a(b(c(x1145))) -> a(b(b(x1145))) b(c(x)) -> b(b(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(b(c(x1147))) -> c(b(b(x1147))) c(b(c(x1147))) -> c(a(c(x1147))) c(a(c(x1147))) -> c(c(c(x1147))) c(c(c(x1147))) -> c(b(b(x1147))) c(b(b(x1147))) -> c(a(b(x1147))) c(a(c(x1147))) -> c(c(c(x1147))) c(c(c(x1147))) -> c(a(b(x1147))) c(b(b(x1147))) -> b(b(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(b(b(x1147))) c(b(b(x1147))) -> c(c(b(x1147))) c(c(b(x1147))) -> b(b(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(b(b(x1147))) c(b(b(x1147))) -> c(a(b(x1147))) c(a(b(x1147))) -> b(b(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(b(b(x1147))) c(b(b(x1147))) -> b(a(b(x1147))) b(a(b(x1147))) -> b(b(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(b(b(x1147))) c(b(b(x1147))) -> b(a(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(a(b(x1147))) c(b(b(x1147))) -> c(c(b(x1147))) c(c(b(x1147))) -> b(a(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(a(b(x1147))) c(b(b(x1147))) -> c(a(b(x1147))) c(a(b(x1147))) -> b(a(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(a(b(x1147))) c(b(b(x1147))) -> b(b(b(x1147))) b(b(b(x1147))) -> b(a(b(x1147))) c(a(c(x1147))) -> b(b(c(x1147))) b(b(c(x1147))) -> b(a(b(x1147))) c(b(b(x1147))) -> c(c(b(x1147))) c(c(b(x1147))) -> c(c(c(x1147))) c(a(c(x1147))) -> c(c(c(x1147))) c(b(b(x1147))) -> c(c(b(x1147))) c(c(b(x1147))) -> c(b(a(x1147))) c(a(c(x1147))) -> c(c(c(x1147))) c(c(c(x1147))) -> c(b(a(x1147))) c(b(b(x1147))) -> c(c(b(x1147))) c(c(b(x1147))) -> a(b(b(x1147))) c(a(c(x1147))) -> a(b(c(x1147))) a(b(c(x1147))) -> a(b(b(x1147))) c(b(b(x1147))) -> c(a(b(x1147))) c(a(b(x1147))) -> a(b(b(x1147))) c(a(c(x1147))) -> a(b(c(x1147))) a(b(c(x1147))) -> a(b(b(x1147))) c(b(b(x1147))) -> b(b(b(x1147))) b(b(b(x1147))) -> a(b(b(x1147))) c(a(c(x1147))) -> a(b(c(x1147))) a(b(c(x1147))) -> a(b(b(x1147))) c(b(b(x1147))) -> b(a(b(x1147))) b(a(b(x1147))) -> a(b(b(x1147))) c(a(c(x1147))) -> a(b(c(x1147))) a(b(c(x1147))) -> a(b(b(x1147))) b(c(x)) -> b(b(x)) b(c(x)) -> a(b(x)) b(b(x)) -> a(b(x)) c(b(c(x1149))) -> c(b(b(x1149))) c(b(c(x1149))) -> b(b(c(x1149))) c(b(b(x1149))) -> b(b(b(x1149))) b(b(c(x1149))) -> b(b(b(x1149))) c(b(b(x1149))) -> b(a(b(x1149))) b(b(c(x1149))) -> b(a(b(x1149))) c(b(c(x1150))) -> c(b(b(x1150))) c(b(c(x1150))) -> b(a(c(x1150))) c(b(b(x1150))) -> b(b(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(b(b(x1150))) c(b(b(x1150))) -> c(c(b(x1150))) c(c(b(x1150))) -> b(b(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(b(b(x1150))) c(b(b(x1150))) -> c(a(b(x1150))) c(a(b(x1150))) -> b(b(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(b(b(x1150))) c(b(b(x1150))) -> b(a(b(x1150))) b(a(b(x1150))) -> b(b(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(b(b(x1150))) c(b(b(x1150))) -> b(a(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(a(b(x1150))) c(b(b(x1150))) -> c(c(b(x1150))) c(c(b(x1150))) -> b(a(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(a(b(x1150))) c(b(b(x1150))) -> c(a(b(x1150))) c(a(b(x1150))) -> b(a(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(a(b(x1150))) c(b(b(x1150))) -> b(b(b(x1150))) b(b(b(x1150))) -> b(a(b(x1150))) b(a(c(x1150))) -> b(b(c(x1150))) b(b(c(x1150))) -> b(a(b(x1150))) c(b(b(x1150))) -> c(c(b(x1150))) c(c(b(x1150))) -> a(b(b(x1150))) b(a(c(x1150))) -> a(b(c(x1150))) a(b(c(x1150))) -> a(b(b(x1150))) c(b(b(x1150))) -> c(a(b(x1150))) c(a(b(x1150))) -> a(b(b(x1150))) b(a(c(x1150))) -> a(b(c(x1150))) a(b(c(x1150))) -> a(b(b(x1150))) c(b(b(x1150))) -> b(b(b(x1150))) b(b(b(x1150))) -> a(b(b(x1150))) b(a(c(x1150))) -> a(b(c(x1150))) a(b(c(x1150))) -> a(b(b(x1150))) c(b(b(x1150))) -> b(a(b(x1150))) b(a(b(x1150))) -> a(b(b(x1150))) b(a(c(x1150))) -> a(b(c(x1150))) a(b(c(x1150))) -> a(b(b(x1150))) b(c(b(x1151))) -> b(b(b(x1151))) b(c(b(x1151))) -> b(a(b(x1151))) b(a(b(x1151))) -> b(b(b(x1151))) b(b(b(x1151))) -> b(a(b(x1151))) b(b(b(x1151))) -> a(b(b(x1151))) b(a(b(x1151))) -> a(b(b(x1151))) c(b(x)) -> b(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(c(x)) -> a(b(x)) c(c(b(x1153))) -> c(b(b(x1153))) c(c(b(x1153))) -> b(b(b(x1153))) c(b(b(x1153))) -> b(b(b(x1153))) c(b(b(x1153))) -> b(a(b(x1153))) b(b(b(x1153))) -> b(a(b(x1153))) b(c(b(x1154))) -> b(b(b(x1154))) b(c(b(x1154))) -> c(c(b(x1154))) c(c(b(x1154))) -> b(b(b(x1154))) b(b(b(x1154))) -> b(a(b(x1154))) c(c(b(x1154))) -> b(a(b(x1154))) b(b(b(x1154))) -> a(b(b(x1154))) c(c(b(x1154))) -> a(b(b(x1154))) c(b(x)) -> b(b(x)) c(b(x)) -> c(a(x)) c(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(a(x)) -> a(b(x)) c(c(b(x1156))) -> c(b(b(x1156))) c(c(b(x1156))) -> b(a(b(x1156))) c(b(b(x1156))) -> b(b(b(x1156))) b(a(b(x1156))) -> b(b(b(x1156))) c(b(b(x1156))) -> b(a(b(x1156))) b(c(b(x1157))) -> b(b(b(x1157))) b(c(b(x1157))) -> a(b(b(x1157))) b(b(b(x1157))) -> a(b(b(x1157))) b(c(b(x1158))) -> b(b(b(x1158))) b(c(b(x1158))) -> b(b(b(x1158))) c(b(x)) -> b(b(x)) c(b(x)) -> b(a(x)) b(a(x)) -> b(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(c(b(x1160))) -> c(b(b(x1160))) c(c(b(x1160))) -> a(b(b(x1160))) c(b(b(x1160))) -> c(c(b(x1160))) c(c(b(x1160))) -> a(b(b(x1160))) c(b(b(x1160))) -> c(a(b(x1160))) c(a(b(x1160))) -> a(b(b(x1160))) c(b(b(x1160))) -> b(b(b(x1160))) b(b(b(x1160))) -> a(b(b(x1160))) c(b(b(x1160))) -> b(a(b(x1160))) b(a(b(x1160))) -> a(b(b(x1160))) b(c(b(x1161))) -> b(b(a(x1161))) b(c(b(x1161))) -> b(a(b(x1161))) b(b(a(x1161))) -> b(a(b(x1161))) b(b(a(x1161))) -> b(b(b(x1161))) b(a(b(x1161))) -> b(b(b(x1161))) c(b(x)) -> b(a(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(c(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(c(x)) -> b(b(x)) c(c(b(x1163))) -> c(b(a(x1163))) c(c(b(x1163))) -> b(b(b(x1163))) c(b(a(x1163))) -> c(a(b(x1163))) c(a(b(x1163))) -> b(a(b(x1163))) b(b(b(x1163))) -> b(a(b(x1163))) c(b(a(x1163))) -> c(b(b(x1163))) c(b(b(x1163))) -> b(a(b(x1163))) b(b(b(x1163))) -> b(a(b(x1163))) c(b(a(x1163))) -> b(b(a(x1163))) b(b(a(x1163))) -> b(a(b(x1163))) b(b(b(x1163))) -> b(a(b(x1163))) c(b(a(x1163))) -> c(a(b(x1163))) c(a(b(x1163))) -> a(b(b(x1163))) b(b(b(x1163))) -> a(b(b(x1163))) c(b(a(x1163))) -> c(a(b(x1163))) c(a(b(x1163))) -> a(b(b(x1163))) b(b(b(x1163))) -> b(a(b(x1163))) b(a(b(x1163))) -> a(b(b(x1163))) c(b(a(x1163))) -> c(a(b(x1163))) c(a(b(x1163))) -> b(b(b(x1163))) c(b(a(x1163))) -> c(b(b(x1163))) c(b(b(x1163))) -> b(b(b(x1163))) c(b(a(x1163))) -> b(b(a(x1163))) b(b(a(x1163))) -> b(b(b(x1163))) b(c(b(x1164))) -> b(b(a(x1164))) b(c(b(x1164))) -> c(c(b(x1164))) b(b(a(x1164))) -> b(a(b(x1164))) c(c(b(x1164))) -> b(a(b(x1164))) b(b(a(x1164))) -> b(b(b(x1164))) c(c(b(x1164))) -> b(b(b(x1164))) c(b(x)) -> b(a(x)) c(b(x)) -> c(a(x)) c(a(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(a(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(a(x)) -> b(b(x)) c(c(b(x1166))) -> c(b(a(x1166))) c(c(b(x1166))) -> b(a(b(x1166))) c(b(a(x1166))) -> c(a(b(x1166))) c(a(b(x1166))) -> b(a(b(x1166))) c(b(a(x1166))) -> c(b(b(x1166))) c(b(b(x1166))) -> b(a(b(x1166))) c(b(a(x1166))) -> b(b(a(x1166))) b(b(a(x1166))) -> b(a(b(x1166))) c(b(a(x1166))) -> c(a(b(x1166))) c(a(b(x1166))) -> a(b(b(x1166))) b(a(b(x1166))) -> a(b(b(x1166))) c(b(a(x1166))) -> c(a(b(x1166))) c(a(b(x1166))) -> a(b(b(x1166))) b(a(b(x1166))) -> b(b(b(x1166))) b(b(b(x1166))) -> a(b(b(x1166))) c(b(a(x1166))) -> c(a(b(x1166))) c(a(b(x1166))) -> b(b(b(x1166))) b(a(b(x1166))) -> b(b(b(x1166))) c(b(a(x1166))) -> c(b(b(x1166))) c(b(b(x1166))) -> b(b(b(x1166))) b(a(b(x1166))) -> b(b(b(x1166))) c(b(a(x1166))) -> b(b(a(x1166))) b(b(a(x1166))) -> b(b(b(x1166))) b(a(b(x1166))) -> b(b(b(x1166))) b(c(b(x1167))) -> b(b(a(x1167))) b(c(b(x1167))) -> a(b(b(x1167))) b(b(a(x1167))) -> b(a(b(x1167))) b(a(b(x1167))) -> a(b(b(x1167))) b(b(a(x1167))) -> a(b(a(x1167))) a(b(a(x1167))) -> a(b(b(x1167))) b(b(a(x1167))) -> b(b(b(x1167))) b(b(b(x1167))) -> a(b(b(x1167))) b(b(a(x1167))) -> a(b(a(x1167))) a(b(a(x1167))) -> a(a(b(x1167))) a(b(b(x1167))) -> a(a(b(x1167))) b(c(b(x1168))) -> b(b(a(x1168))) b(c(b(x1168))) -> b(b(b(x1168))) b(b(a(x1168))) -> b(a(b(x1168))) b(b(b(x1168))) -> b(a(b(x1168))) b(b(a(x1168))) -> b(b(b(x1168))) c(b(x)) -> b(a(x)) c(b(x)) -> b(b(x)) b(a(x)) -> a(b(x)) b(b(x)) -> a(b(x)) b(a(x)) -> b(b(x)) c(c(b(x1170))) -> c(b(a(x1170))) c(c(b(x1170))) -> a(b(b(x1170))) c(b(a(x1170))) -> c(a(b(x1170))) c(a(b(x1170))) -> a(b(b(x1170))) b(c(c(x1171))) -> b(a(b(x1171))) b(c(c(x1171))) -> b(a(c(x1171))) b(a(c(x1171))) -> b(b(c(x1171))) b(b(c(x1171))) -> b(a(b(x1171))) b(a(b(x1171))) -> a(b(b(x1171))) b(a(c(x1171))) -> a(b(c(x1171))) a(b(c(x1171))) -> a(b(b(x1171))) b(a(b(x1171))) -> b(b(b(x1171))) b(b(b(x1171))) -> a(b(b(x1171))) b(a(c(x1171))) -> a(b(c(x1171))) a(b(c(x1171))) -> a(b(b(x1171))) b(a(b(x1171))) -> b(b(b(x1171))) b(a(c(x1171))) -> b(b(c(x1171))) b(b(c(x1171))) -> b(b(b(x1171))) b(a(b(x1171))) -> a(b(b(x1171))) a(b(b(x1171))) -> a(a(b(x1171))) b(a(c(x1171))) -> a(b(c(x1171))) a(b(c(x1171))) -> a(a(b(x1171))) c(c(x)) -> a(b(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(c(c(x1173))) -> c(a(b(x1173))) c(c(c(x1173))) -> b(b(c(x1173))) c(a(b(x1173))) -> b(a(b(x1173))) b(b(c(x1173))) -> b(a(b(x1173))) c(a(b(x1173))) -> b(b(b(x1173))) b(b(c(x1173))) -> b(b(b(x1173))) b(c(c(x1174))) -> b(a(b(x1174))) b(c(c(x1174))) -> c(c(c(x1174))) c(c(c(x1174))) -> c(b(b(x1174))) c(b(b(x1174))) -> b(a(b(x1174))) c(c(c(x1174))) -> b(b(c(x1174))) b(b(c(x1174))) -> b(a(b(x1174))) c(c(c(x1174))) -> c(a(b(x1174))) c(a(b(x1174))) -> b(a(b(x1174))) b(a(b(x1174))) -> a(b(b(x1174))) c(c(c(x1174))) -> c(a(b(x1174))) c(a(b(x1174))) -> a(b(b(x1174))) b(a(b(x1174))) -> a(b(b(x1174))) c(c(c(x1174))) -> a(b(c(x1174))) a(b(c(x1174))) -> a(b(b(x1174))) b(a(b(x1174))) -> b(b(b(x1174))) b(b(b(x1174))) -> a(b(b(x1174))) c(c(c(x1174))) -> c(a(b(x1174))) c(a(b(x1174))) -> a(b(b(x1174))) b(a(b(x1174))) -> b(b(b(x1174))) b(b(b(x1174))) -> a(b(b(x1174))) c(c(c(x1174))) -> a(b(c(x1174))) a(b(c(x1174))) -> a(b(b(x1174))) b(a(b(x1174))) -> b(b(b(x1174))) c(c(c(x1174))) -> c(b(b(x1174))) c(b(b(x1174))) -> b(b(b(x1174))) b(a(b(x1174))) -> b(b(b(x1174))) c(c(c(x1174))) -> b(b(c(x1174))) b(b(c(x1174))) -> b(b(b(x1174))) b(a(b(x1174))) -> b(b(b(x1174))) c(c(c(x1174))) -> c(a(b(x1174))) c(a(b(x1174))) -> b(b(b(x1174))) b(a(b(x1174))) -> a(b(b(x1174))) a(b(b(x1174))) -> a(a(b(x1174))) c(c(c(x1174))) -> a(b(c(x1174))) a(b(c(x1174))) -> a(a(b(x1174))) c(c(x)) -> a(b(x)) c(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(c(c(x1176))) -> c(a(b(x1176))) c(c(c(x1176))) -> b(a(c(x1176))) c(a(b(x1176))) -> b(a(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(a(b(x1176))) c(a(b(x1176))) -> c(c(b(x1176))) c(c(b(x1176))) -> b(a(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(a(b(x1176))) c(a(b(x1176))) -> b(b(b(x1176))) b(b(b(x1176))) -> b(a(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(a(b(x1176))) c(a(b(x1176))) -> a(b(b(x1176))) b(a(c(x1176))) -> a(b(c(x1176))) a(b(c(x1176))) -> a(b(b(x1176))) c(a(b(x1176))) -> b(a(b(x1176))) b(a(b(x1176))) -> a(b(b(x1176))) b(a(c(x1176))) -> a(b(c(x1176))) a(b(c(x1176))) -> a(b(b(x1176))) c(a(b(x1176))) -> c(c(b(x1176))) c(c(b(x1176))) -> a(b(b(x1176))) b(a(c(x1176))) -> a(b(c(x1176))) a(b(c(x1176))) -> a(b(b(x1176))) c(a(b(x1176))) -> b(b(b(x1176))) b(b(b(x1176))) -> a(b(b(x1176))) b(a(c(x1176))) -> a(b(c(x1176))) a(b(c(x1176))) -> a(b(b(x1176))) c(a(b(x1176))) -> b(b(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(b(b(x1176))) c(a(b(x1176))) -> b(a(b(x1176))) b(a(b(x1176))) -> b(b(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(b(b(x1176))) c(a(b(x1176))) -> c(c(b(x1176))) c(c(b(x1176))) -> b(b(b(x1176))) b(a(c(x1176))) -> b(b(c(x1176))) b(b(c(x1176))) -> b(b(b(x1176))) c(a(b(x1176))) -> a(b(b(x1176))) a(b(b(x1176))) -> a(a(b(x1176))) b(a(c(x1176))) -> a(b(c(x1176))) a(b(c(x1176))) -> a(a(b(x1176))) b(c(c(x1177))) -> b(a(b(x1177))) b(c(c(x1177))) -> a(b(c(x1177))) b(a(b(x1177))) -> a(b(b(x1177))) a(b(c(x1177))) -> a(b(b(x1177))) b(c(c(x1178))) -> b(a(b(x1178))) b(c(c(x1178))) -> b(b(c(x1178))) b(b(c(x1178))) -> b(a(b(x1178))) b(a(b(x1178))) -> b(b(b(x1178))) b(b(c(x1178))) -> b(b(b(x1178))) c(c(c(x1179))) -> c(a(b(x1179))) c(c(c(x1179))) -> a(b(c(x1179))) c(a(b(x1179))) -> a(b(b(x1179))) a(b(c(x1179))) -> a(b(b(x1179))) weak: c(a(x)) -> b(a(x)) b(c(x)) -> b(a(x)) b(a(x)) -> a(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(b(x)) b(b(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> c(c(x)) b(a(x)) -> b(b(x)) c(b(x)) -> c(a(x)) c(c(x)) -> b(a(x)) c(a(x)) -> a(b(x)) c(a(x)) -> b(b(x)) b(c(x)) -> a(b(x)) b(c(x)) -> b(b(x)) c(b(x)) -> b(b(x)) c(b(x)) -> b(a(x)) c(c(x)) -> a(b(x)) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): c(a(x)) -> b(a(x)): 17 b(c(x)) -> b(a(x)): 16 b(a(x)) -> a(b(x)): 0 c(b(x)) -> c(c(x)): 17 c(c(x)) -> b(b(x)): 16 b(b(x)) -> a(b(x)): 0 c(a(x)) -> c(c(x)): 4 b(c(x)) -> c(c(x)): 27 b(a(x)) -> b(b(x)): 0 c(b(x)) -> c(a(x)): 17 c(c(x)) -> b(a(x)): 16 c(a(x)) -> a(b(x)): 0 c(a(x)) -> b(b(x)): 16 b(c(x)) -> a(b(x)): 0 b(c(x)) -> b(b(x)): 0 c(b(x)) -> b(b(x)): 16 c(b(x)) -> b(a(x)): 1 c(c(x)) -> a(b(x)): 0 Decreasing Processor: The following diagrams are decreasing: peak: b(b(a(x1024))) <-0|0[==1,=?17]- b(c(a(x1024))) -1|[==1,>=16]-> b(a(a(x1024))) joins (1): b(a(a(x1024))) -8|[==1,>>0]-> b(b(a(x1024))) peak: c(b(a(x1025))) <-0|0[==1,=?17]- c(c(a(x1025))) -4|[==1,>=16]-> b(b(a(x1025))) joins (1): c(b(a(x1025))) -15|[==1,>=16]-> b(b(a(x1025))) peak: b(a(x)) <-0|[==1,=?17]- c(a(x)) -6|[==1,>=4]-> c(c(x)) joins (1): c(c(x)) -10|[==1,>?16]-> b(a(x)) peak: b(b(a(x1027))) <-0|0[==1,=>17]- b(c(a(x1027))) -7|[==1,?=27]-> c(c(a(x1027))) joins (1): c(c(a(x1027))) -4|[==1,>>16]-> b(b(a(x1027))) peak: c(b(a(x1028))) <-0|0[==1,=?17]- c(c(a(x1028))) -10|[==1,>=16]-> b(a(a(x1028))) joins (1): c(b(a(x1028))) -16|[==1,>>1]-> b(a(a(x1028))) peak: b(a(x)) <-0|[==1,=?17]- c(a(x)) -11|[==1,>=0]-> a(b(x)) joins (1): b(a(x)) -2|[==1,>=0]-> a(b(x)) peak: b(a(x)) <-0|[==1,=?17]- c(a(x)) -12|[==1,>=16]-> b(b(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: b(b(a(x1031))) <-0|0[==1,=?17]- b(c(a(x1031))) -13|[==1,>=0]-> a(b(a(x1031))) joins (1): b(b(a(x1031))) -5|[==1,>=0]-> a(b(a(x1031))) peak: b(b(a(x1032))) <-0|0[==1,=?17]- b(c(a(x1032))) -14|[==1,>=0]-> b(b(a(x1032))) joins (1): peak: c(b(a(x1033))) <-0|0[==1,=?17]- c(c(a(x1033))) -17|[==1,>=0]-> a(b(a(x1033))) joins (1): c(b(a(x1033))) -15|[==1,>?16]-> b(b(a(x1033))) -5|[==1,>=0]-> a(b(a(x1033))) peak: c(b(a(x1034))) <-1|0[==1,=>16]- c(b(c(x1034))) -3|[==1,?=17]-> c(c(c(x1034))) joins (1): c(c(c(x1034))) -10|0[==1,=>16]-> c(b(a(x1034))) peak: b(b(a(x1035))) <-1|0[==1,=?16]- b(b(c(x1035))) -5|[==1,>=0]-> a(b(c(x1035))) joins (1): b(b(a(x1035))) -5|[==1,>=0]-> a(b(a(x1035))) a(b(c(x1035))) -1|0[==1,=?16]-> a(b(a(x1035))) peak: b(a(x)) <-1|[==1,=>16]- b(c(x)) -7|[==1,?=27]-> c(c(x)) joins (1): c(c(x)) -10|[==1,=>16]-> b(a(x)) peak: c(b(a(x1037))) <-1|0[==1,=>16]- c(b(c(x1037))) -9|[==1,?=17]-> c(a(c(x1037))) joins (1): c(a(c(x1037))) -6|[==1,>>4]-> c(c(c(x1037))) -10|0[==1,=>16]-> c(b(a(x1037))) peak: b(a(x)) <-1|[==1,=?16]- b(c(x)) -13|[==1,>=0]-> a(b(x)) joins (1): b(a(x)) -2|[==1,>=0]-> a(b(x)) peak: b(a(x)) <-1|[==1,=?16]- b(c(x)) -14|[==1,>=0]-> b(b(x)) joins (1): b(a(x)) -8|[==1,>=0]-> b(b(x)) peak: c(b(a(x1040))) <-1|0[==1,==16]- c(b(c(x1040))) -15|[==1,==16]-> b(b(c(x1040))) joins (1): c(b(a(x1040))) -15|[==1,==16]-> b(b(a(x1040))) b(b(c(x1040))) -1|0[==1,==16]-> b(b(a(x1040))) peak: c(b(a(x1041))) <-1|0[==1,=?16]- c(b(c(x1041))) -16|[==1,>=1]-> b(a(c(x1041))) joins (1): c(b(a(x1041))) -16|[==1,>=1]-> b(a(a(x1041))) -8|[==1,>>0]-> b(b(a(x1041))) b(a(c(x1041))) -8|[==1,>>0]-> b(b(c(x1041))) -1|0[==1,=?16]-> b(b(a(x1041))) peak: c(a(b(x1042))) <-2|0[==1,=>0]- c(b(a(x1042))) -3|[==1,?=17]-> c(c(a(x1042))) joins (1): c(c(a(x1042))) -11|0[==1,=>0]-> c(a(b(x1042))) peak: b(a(b(x1043))) <-2|0[==1,==0]- b(b(a(x1043))) -5|[==1,==0]-> a(b(a(x1043))) joins (1): b(a(b(x1043))) -2|[==1,==0]-> a(b(b(x1043))) a(b(a(x1043))) -8|0[==1,==0]-> a(b(b(x1043))) peak: a(b(x)) <-2|[==1,==0]- b(a(x)) -8|[==1,==0]-> b(b(x)) joins (1): b(b(x)) -5|[==1,==0]-> a(b(x)) peak: c(a(b(x1045))) <-2|0[==1,=>0]- c(b(a(x1045))) -9|[==1,?=17]-> c(a(a(x1045))) joins (1): c(a(a(x1045))) -6|[==1,?>4]-> c(c(a(x1045))) -11|0[==1,=>0]-> c(a(b(x1045))) peak: c(a(b(x1046))) <-2|0[==1,=>0]- c(b(a(x1046))) -15|[==1,?=16]-> b(b(a(x1046))) joins (1): c(a(b(x1046))) -12|[==1,?=16]-> b(b(b(x1046))) b(b(a(x1046))) -8|0[==1,=>0]-> b(b(b(x1046))) peak: c(a(b(x1047))) <-2|0[==1,=>0]- c(b(a(x1047))) -16|[==1,?=1]-> b(a(a(x1047))) joins (1): c(a(b(x1047))) -11|[==1,=>0]-> a(b(b(x1047))) b(a(a(x1047))) -2|[==1,=>0]-> a(b(a(x1047))) -8|0[==1,=>0]-> a(b(b(x1047))) peak: b(c(c(x1048))) <-3|0[==1,=?17]- b(c(b(x1048))) -1|[==1,>=16]-> b(a(b(x1048))) joins (1): b(c(c(x1048))) -17|0[==1,>>0]-> b(a(b(x1048))) peak: c(c(c(x1049))) <-3|0[==1,=?17]- c(c(b(x1049))) -4|[==1,>=16]-> b(b(b(x1049))) joins (1): c(c(c(x1049))) -4|0[==1,>=16]-> c(b(b(x1049))) -15|[==1,>=16]-> b(b(b(x1049))) peak: b(c(c(x1050))) <-3|0[==1,=>17]- b(c(b(x1050))) -7|[==1,?=27]-> c(c(b(x1050))) joins (1): b(c(c(x1050))) -4|0[==1,>>16]-> b(b(b(x1050))) c(c(b(x1050))) -4|[==1,>>16]-> b(b(b(x1050))) peak: c(c(x)) <-3|[==1,==17]- c(b(x)) -9|[==1,==17]-> c(a(x)) joins (1): c(a(x)) -6|[==1,>>4]-> c(c(x)) peak: c(c(c(x1052))) <-3|0[==1,=?17]- c(c(b(x1052))) -10|[==1,>=16]-> b(a(b(x1052))) joins (1): c(c(c(x1052))) -4|0[==1,>=16]-> c(b(b(x1052))) -16|[==1,>>1]-> b(a(b(x1052))) peak: b(c(c(x1053))) <-3|0[==1,=?17]- b(c(b(x1053))) -13|[==1,>=0]-> a(b(b(x1053))) joins (1): b(c(c(x1053))) -4|0[==1,>?16]-> b(b(b(x1053))) -5|[==1,>=0]-> a(b(b(x1053))) peak: b(c(c(x1054))) <-3|0[==1,=?17]- b(c(b(x1054))) -14|[==1,>=0]-> b(b(b(x1054))) joins (1): b(c(c(x1054))) -4|0[==1,>?16]-> b(b(b(x1054))) peak: c(c(x)) <-3|[==1,=?17]- c(b(x)) -15|[==1,>=16]-> b(b(x)) joins (1): c(c(x)) -4|[==1,>=16]-> b(b(x)) peak: c(c(x)) <-3|[==1,=?17]- c(b(x)) -16|[==1,>=1]-> b(a(x)) joins (1): c(c(x)) -10|[==1,>?16]-> b(a(x)) peak: c(c(c(x1057))) <-3|0[==1,=?17]- c(c(b(x1057))) -17|[==1,>=0]-> a(b(b(x1057))) joins (1): c(c(c(x1057))) -17|0[==1,>=0]-> c(a(b(x1057))) -11|[==1,>=0]-> a(b(b(x1057))) peak: b(b(b(x1058))) <-4|0[==1,==16]- b(c(c(x1058))) -1|[==1,==16]-> b(a(c(x1058))) joins (1): b(a(c(x1058))) -8|[==1,>>0]-> b(b(c(x1058))) -14|0[==1,>>0]-> b(b(b(x1058))) peak: c(b(b(x1059))) <-4|0[==1,==16]- c(c(c(x1059))) -4|[==1,==16]-> b(b(c(x1059))) joins (1): c(b(b(x1059))) -15|[==1,==16]-> b(b(b(x1059))) b(b(c(x1059))) -14|0[==1,>>0]-> b(b(b(x1059))) peak: b(b(b(x1060))) <-4|0[==1,=>16]- b(c(c(x1060))) -7|[==1,?=27]-> c(c(c(x1060))) joins (1): c(c(c(x1060))) -4|0[==1,=>16]-> c(b(b(x1060))) -15|[==1,=>16]-> b(b(b(x1060))) peak: b(b(x)) <-4|[==1,==16]- c(c(x)) -10|[==1,==16]-> b(a(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: c(b(b(x1062))) <-4|0[==1,==16]- c(c(c(x1062))) -10|[==1,==16]-> b(a(c(x1062))) joins (1): c(b(b(x1062))) -15|[==1,==16]-> b(b(b(x1062))) b(a(c(x1062))) -8|[==1,>>0]-> b(b(c(x1062))) -14|0[==1,>>0]-> b(b(b(x1062))) peak: b(b(b(x1063))) <-4|0[==1,=?16]- b(c(c(x1063))) -13|[==1,>=0]-> a(b(c(x1063))) joins (1): b(b(b(x1063))) -5|[==1,>=0]-> a(b(b(x1063))) a(b(c(x1063))) -14|0[==1,>=0]-> a(b(b(x1063))) peak: b(b(b(x1064))) <-4|0[==1,=?16]- b(c(c(x1064))) -14|[==1,>=0]-> b(b(c(x1064))) joins (1): b(b(c(x1064))) -14|0[==1,>=0]-> b(b(b(x1064))) peak: b(b(x)) <-4|[==1,=?16]- c(c(x)) -17|[==1,>=0]-> a(b(x)) joins (1): b(b(x)) -5|[==1,>=0]-> a(b(x)) peak: c(b(b(x1066))) <-4|0[==1,=?16]- c(c(c(x1066))) -17|[==1,>=0]-> a(b(c(x1066))) joins (1): c(b(b(x1066))) -16|[==1,>?1]-> b(a(b(x1066))) -2|[==1,>=0]-> a(b(b(x1066))) a(b(c(x1066))) -14|0[==1,>=0]-> a(b(b(x1066))) peak: c(a(b(x1067))) <-5|0[==1,=>0]- c(b(b(x1067))) -3|[==1,?=17]-> c(c(b(x1067))) joins (1): c(a(b(x1067))) -6|[==1,?>4]-> c(c(b(x1067))) peak: b(a(b(x1068))) <-5|0[==1,==0]- b(b(b(x1068))) -5|[==1,==0]-> a(b(b(x1068))) joins (1): b(a(b(x1068))) -2|[==1,==0]-> a(b(b(x1068))) peak: c(a(b(x1069))) <-5|0[==1,=>0]- c(b(b(x1069))) -9|[==1,?=17]-> c(a(b(x1069))) joins (1): peak: c(a(b(x1070))) <-5|0[==1,=>0]- c(b(b(x1070))) -15|[==1,?=16]-> b(b(b(x1070))) joins (1): c(a(b(x1070))) -12|[==1,?=16]-> b(b(b(x1070))) peak: c(a(b(x1071))) <-5|0[==1,=>0]- c(b(b(x1071))) -16|[==1,?=1]-> b(a(b(x1071))) joins (1): c(a(b(x1071))) -11|[==1,=>0]-> a(b(b(x1071))) b(a(b(x1071))) -2|[==1,=>0]-> a(b(b(x1071))) peak: c(c(x)) <-6|[==1,=>4]- c(a(x)) -0|[==1,?=17]-> b(a(x)) joins (1): c(c(x)) -10|[==1,?>16]-> b(a(x)) peak: b(c(c(x1073))) <-6|0[==1,=>4]- b(c(a(x1073))) -1|[==1,?=16]-> b(a(a(x1073))) joins (1): b(c(c(x1073))) -10|0[==1,?=16]-> b(b(a(x1073))) b(a(a(x1073))) -8|[==1,>>0]-> b(b(a(x1073))) peak: c(c(c(x1074))) <-6|0[==1,=>4]- c(c(a(x1074))) -4|[==1,?=16]-> b(b(a(x1074))) joins (1): c(c(c(x1074))) -4|[==1,?=16]-> b(b(c(x1074))) -14|0[==1,>>0]-> b(b(b(x1074))) b(b(a(x1074))) -8|0[==1,>>0]-> b(b(b(x1074))) peak: b(c(c(x1075))) <-6|0[==1,=>4]- b(c(a(x1075))) -7|[==1,?=27]-> c(c(a(x1075))) joins (1): b(c(c(x1075))) -7|[==1,?=27]-> c(c(c(x1075))) c(c(a(x1075))) -6|0[==1,=>4]-> c(c(c(x1075))) peak: c(c(c(x1076))) <-6|0[==1,=>4]- c(c(a(x1076))) -10|[==1,?=16]-> b(a(a(x1076))) joins (1): c(c(c(x1076))) -10|0[==1,?=16]-> c(b(a(x1076))) -16|[==1,>>1]-> b(a(a(x1076))) peak: c(c(x)) <-6|[==1,=?4]- c(a(x)) -11|[==1,>=0]-> a(b(x)) joins (1): c(c(x)) -17|[==1,>=0]-> a(b(x)) peak: c(c(x)) <-6|[==1,=>4]- c(a(x)) -12|[==1,?=16]-> b(b(x)) joins (1): c(c(x)) -4|[==1,?=16]-> b(b(x)) peak: b(c(c(x1079))) <-6|0[==1,=?4]- b(c(a(x1079))) -13|[==1,>=0]-> a(b(a(x1079))) joins (1): b(c(c(x1079))) -13|[==1,>=0]-> a(b(c(x1079))) -14|0[==1,>=0]-> a(b(b(x1079))) a(b(a(x1079))) -8|0[==1,>=0]-> a(b(b(x1079))) peak: b(c(c(x1080))) <-6|0[==1,=?4]- b(c(a(x1080))) -14|[==1,>=0]-> b(b(a(x1080))) joins (1): b(c(c(x1080))) -17|0[==1,>=0]-> b(a(b(x1080))) b(b(a(x1080))) -2|0[==1,>=0]-> b(a(b(x1080))) peak: c(c(c(x1081))) <-6|0[==1,=?4]- c(c(a(x1081))) -17|[==1,>=0]-> a(b(a(x1081))) joins (1): c(c(c(x1081))) -17|0[==1,>=0]-> c(a(b(x1081))) -11|[==1,>=0]-> a(b(b(x1081))) a(b(a(x1081))) -8|0[==1,>=0]-> a(b(b(x1081))) peak: c(c(x)) <-7|[==1,=?27]- b(c(x)) -1|[==1,>=16]-> b(a(x)) joins (1): c(c(x)) -10|[==1,>=16]-> b(a(x)) peak: c(c(c(x1083))) <-7|0[==1,=?27]- c(b(c(x1083))) -3|[==1,>=17]-> c(c(c(x1083))) joins (1): peak: b(c(c(x1084))) <-7|0[==1,=?27]- b(b(c(x1084))) -5|[==1,>=0]-> a(b(c(x1084))) joins (1): b(c(c(x1084))) -13|[==1,>=0]-> a(b(c(x1084))) peak: c(c(c(x1085))) <-7|0[==1,=?27]- c(b(c(x1085))) -9|[==1,>=17]-> c(a(c(x1085))) joins (1): c(a(c(x1085))) -6|[==1,>>4]-> c(c(c(x1085))) peak: c(c(x)) <-7|[==1,=?27]- b(c(x)) -13|[==1,>=0]-> a(b(x)) joins (1): c(c(x)) -17|[==1,>=0]-> a(b(x)) peak: c(c(x)) <-7|[==1,=?27]- b(c(x)) -14|[==1,>=0]-> b(b(x)) joins (1): c(c(x)) -4|[==1,>?16]-> b(b(x)) peak: c(c(c(x1088))) <-7|0[==1,=?27]- c(b(c(x1088))) -15|[==1,>=16]-> b(b(c(x1088))) joins (1): c(c(c(x1088))) -4|[==1,>=16]-> b(b(c(x1088))) peak: c(c(c(x1089))) <-7|0[==1,=?27]- c(b(c(x1089))) -16|[==1,>=1]-> b(a(c(x1089))) joins (1): c(c(c(x1089))) -10|[==1,>?16]-> b(a(c(x1089))) peak: b(b(x)) <-8|[==1,==0]- b(a(x)) -2|[==1,==0]-> a(b(x)) joins (1): b(b(x)) -5|[==1,==0]-> a(b(x)) peak: c(b(b(x1091))) <-8|0[==1,=>0]- c(b(a(x1091))) -3|[==1,?=17]-> c(c(a(x1091))) joins (1): c(c(a(x1091))) -12|0[==1,?>16]-> c(b(b(x1091))) peak: b(b(b(x1092))) <-8|0[==1,==0]- b(b(a(x1092))) -5|[==1,==0]-> a(b(a(x1092))) joins (1): b(b(b(x1092))) -5|[==1,==0]-> a(b(b(x1092))) a(b(a(x1092))) -8|0[==1,==0]-> a(b(b(x1092))) peak: c(b(b(x1093))) <-8|0[==1,=>0]- c(b(a(x1093))) -9|[==1,?=17]-> c(a(a(x1093))) joins (1): c(a(a(x1093))) -6|[==1,?>4]-> c(c(a(x1093))) -12|0[==1,?>16]-> c(b(b(x1093))) peak: c(b(b(x1094))) <-8|0[==1,=>0]- c(b(a(x1094))) -15|[==1,?=16]-> b(b(a(x1094))) joins (1): c(b(b(x1094))) -15|[==1,?=16]-> b(b(b(x1094))) b(b(a(x1094))) -8|0[==1,=>0]-> b(b(b(x1094))) peak: c(b(b(x1095))) <-8|0[==1,=>0]- c(b(a(x1095))) -16|[==1,?=1]-> b(a(a(x1095))) joins (1): c(b(b(x1095))) -16|[==1,?=1]-> b(a(b(x1095))) b(a(a(x1095))) -8|[==1,=>0]-> b(b(a(x1095))) -2|0[==1,=>0]-> b(a(b(x1095))) peak: b(c(a(x1096))) <-9|0[==1,=?17]- b(c(b(x1096))) -1|[==1,>=16]-> b(a(b(x1096))) joins (1): b(c(a(x1096))) -11|0[==1,>>0]-> b(a(b(x1096))) peak: c(a(x)) <-9|[==1,==17]- c(b(x)) -3|[==1,==17]-> c(c(x)) joins (1): c(a(x)) -6|[==1,>>4]-> c(c(x)) peak: c(c(a(x1098))) <-9|0[==1,=?17]- c(c(b(x1098))) -4|[==1,>=16]-> b(b(b(x1098))) joins (1): c(c(a(x1098))) -4|[==1,>=16]-> b(b(a(x1098))) -8|0[==1,>>0]-> b(b(b(x1098))) peak: b(c(a(x1099))) <-9|0[==1,=>17]- b(c(b(x1099))) -7|[==1,?=27]-> c(c(b(x1099))) joins (1): b(c(a(x1099))) -7|[==1,?=27]-> c(c(a(x1099))) c(c(b(x1099))) -9|0[==1,=>17]-> c(c(a(x1099))) peak: c(c(a(x1100))) <-9|0[==1,=?17]- c(c(b(x1100))) -10|[==1,>=16]-> b(a(b(x1100))) joins (1): c(c(a(x1100))) -4|[==1,>=16]-> b(b(a(x1100))) -2|0[==1,>>0]-> b(a(b(x1100))) peak: b(c(a(x1101))) <-9|0[==1,=?17]- b(c(b(x1101))) -13|[==1,>=0]-> a(b(b(x1101))) joins (1): b(c(a(x1101))) -11|0[==1,>=0]-> b(a(b(x1101))) -2|[==1,>=0]-> a(b(b(x1101))) peak: b(c(a(x1102))) <-9|0[==1,=?17]- b(c(b(x1102))) -14|[==1,>=0]-> b(b(b(x1102))) joins (1): b(c(a(x1102))) -12|0[==1,>?16]-> b(b(b(x1102))) peak: c(a(x)) <-9|[==1,=?17]- c(b(x)) -15|[==1,>=16]-> b(b(x)) joins (1): c(a(x)) -12|[==1,>=16]-> b(b(x)) peak: c(a(x)) <-9|[==1,=?17]- c(b(x)) -16|[==1,>=1]-> b(a(x)) joins (1): c(a(x)) -11|[==1,>>0]-> a(b(x)) b(a(x)) -2|[==1,>>0]-> a(b(x)) peak: c(c(a(x1105))) <-9|0[==1,=?17]- c(c(b(x1105))) -17|[==1,>=0]-> a(b(b(x1105))) joins (1): c(c(a(x1105))) -11|0[==1,>=0]-> c(a(b(x1105))) -11|[==1,>=0]-> a(b(b(x1105))) peak: b(b(a(x1106))) <-10|0[==1,==16]- b(c(c(x1106))) -1|[==1,==16]-> b(a(c(x1106))) joins (1): b(a(c(x1106))) -8|[==1,>>0]-> b(b(c(x1106))) -1|0[==1,==16]-> b(b(a(x1106))) peak: b(a(x)) <-10|[==1,==16]- c(c(x)) -4|[==1,==16]-> b(b(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: c(b(a(x1108))) <-10|0[==1,==16]- c(c(c(x1108))) -4|[==1,==16]-> b(b(c(x1108))) joins (1): c(b(a(x1108))) -15|[==1,==16]-> b(b(a(x1108))) b(b(c(x1108))) -1|0[==1,==16]-> b(b(a(x1108))) peak: b(b(a(x1109))) <-10|0[==1,=>16]- b(c(c(x1109))) -7|[==1,?=27]-> c(c(c(x1109))) joins (1): c(c(c(x1109))) -4|[==1,=>16]-> b(b(c(x1109))) -1|0[==1,=>16]-> b(b(a(x1109))) peak: c(b(a(x1110))) <-10|0[==1,==16]- c(c(c(x1110))) -10|[==1,==16]-> b(a(c(x1110))) joins (1): c(b(a(x1110))) -15|[==1,==16]-> b(b(a(x1110))) b(a(c(x1110))) -8|[==1,>>0]-> b(b(c(x1110))) -1|0[==1,==16]-> b(b(a(x1110))) peak: b(b(a(x1111))) <-10|0[==1,=?16]- b(c(c(x1111))) -13|[==1,>=0]-> a(b(c(x1111))) joins (1): b(b(a(x1111))) -5|[==1,>=0]-> a(b(a(x1111))) a(b(c(x1111))) -1|0[==1,=?16]-> a(b(a(x1111))) peak: b(b(a(x1112))) <-10|0[==1,=?16]- b(c(c(x1112))) -14|[==1,>=0]-> b(b(c(x1112))) joins (1): b(b(c(x1112))) -1|0[==1,=?16]-> b(b(a(x1112))) peak: b(a(x)) <-10|[==1,=?16]- c(c(x)) -17|[==1,>=0]-> a(b(x)) joins (1): b(a(x)) -2|[==1,>=0]-> a(b(x)) peak: c(b(a(x1114))) <-10|0[==1,=?16]- c(c(c(x1114))) -17|[==1,>=0]-> a(b(c(x1114))) joins (1): c(b(a(x1114))) -2|0[==1,>=0]-> c(a(b(x1114))) -11|[==1,>=0]-> a(b(b(x1114))) a(b(c(x1114))) -14|0[==1,>=0]-> a(b(b(x1114))) peak: a(b(x)) <-11|[==1,=>0]- c(a(x)) -0|[==1,?=17]-> b(a(x)) joins (1): b(a(x)) -2|[==1,=>0]-> a(b(x)) peak: b(a(b(x1116))) <-11|0[==1,=>0]- b(c(a(x1116))) -1|[==1,?=16]-> b(a(a(x1116))) joins (1): b(a(a(x1116))) -8|[==1,=>0]-> b(b(a(x1116))) -2|0[==1,=>0]-> b(a(b(x1116))) peak: c(a(b(x1117))) <-11|0[==1,=>0]- c(c(a(x1117))) -4|[==1,?=16]-> b(b(a(x1117))) joins (1): c(a(b(x1117))) -12|[==1,?=16]-> b(b(b(x1117))) b(b(a(x1117))) -8|0[==1,=>0]-> b(b(b(x1117))) peak: a(b(x)) <-11|[==1,=>0]- c(a(x)) -6|[==1,?=4]-> c(c(x)) joins (1): c(c(x)) -17|[==1,=>0]-> a(b(x)) peak: b(a(b(x1119))) <-11|0[==1,=>0]- b(c(a(x1119))) -7|[==1,?=27]-> c(c(a(x1119))) joins (1): c(c(a(x1119))) -4|[==1,?>16]-> b(b(a(x1119))) -2|0[==1,=>0]-> b(a(b(x1119))) peak: c(a(b(x1120))) <-11|0[==1,=>0]- c(c(a(x1120))) -10|[==1,?=16]-> b(a(a(x1120))) joins (1): c(a(b(x1120))) -11|[==1,=>0]-> a(b(b(x1120))) b(a(a(x1120))) -2|[==1,=>0]-> a(b(a(x1120))) -8|0[==1,=>0]-> a(b(b(x1120))) peak: a(b(x)) <-11|[==1,=>0]- c(a(x)) -12|[==1,?=16]-> b(b(x)) joins (1): b(b(x)) -5|[==1,=>0]-> a(b(x)) peak: b(a(b(x1122))) <-11|0[==1,==0]- b(c(a(x1122))) -13|[==1,==0]-> a(b(a(x1122))) joins (1): b(a(b(x1122))) -2|[==1,==0]-> a(b(b(x1122))) a(b(a(x1122))) -8|0[==1,==0]-> a(b(b(x1122))) peak: b(a(b(x1123))) <-11|0[==1,==0]- b(c(a(x1123))) -14|[==1,==0]-> b(b(a(x1123))) joins (1): b(b(a(x1123))) -2|0[==1,==0]-> b(a(b(x1123))) peak: c(a(b(x1124))) <-11|0[==1,==0]- c(c(a(x1124))) -17|[==1,==0]-> a(b(a(x1124))) joins (1): c(a(b(x1124))) -11|[==1,==0]-> a(b(b(x1124))) a(b(a(x1124))) -8|0[==1,==0]-> a(b(b(x1124))) peak: b(b(x)) <-12|[==1,=>16]- c(a(x)) -0|[==1,?=17]-> b(a(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: b(b(b(x1126))) <-12|0[==1,==16]- b(c(a(x1126))) -1|[==1,==16]-> b(a(a(x1126))) joins (1): b(a(a(x1126))) -8|[==1,>>0]-> b(b(a(x1126))) -8|0[==1,>>0]-> b(b(b(x1126))) peak: c(b(b(x1127))) <-12|0[==1,==16]- c(c(a(x1127))) -4|[==1,==16]-> b(b(a(x1127))) joins (1): c(b(b(x1127))) -15|[==1,==16]-> b(b(b(x1127))) b(b(a(x1127))) -8|0[==1,>>0]-> b(b(b(x1127))) peak: b(b(x)) <-12|[==1,=?16]- c(a(x)) -6|[==1,>=4]-> c(c(x)) joins (1): c(c(x)) -4|[==1,=?16]-> b(b(x)) peak: b(b(b(x1129))) <-12|0[==1,=>16]- b(c(a(x1129))) -7|[==1,?=27]-> c(c(a(x1129))) joins (1): c(c(a(x1129))) -4|[==1,=>16]-> b(b(a(x1129))) -8|0[==1,>>0]-> b(b(b(x1129))) peak: c(b(b(x1130))) <-12|0[==1,==16]- c(c(a(x1130))) -10|[==1,==16]-> b(a(a(x1130))) joins (1): c(b(b(x1130))) -15|[==1,==16]-> b(b(b(x1130))) b(a(a(x1130))) -8|[==1,>>0]-> b(b(a(x1130))) -8|0[==1,>>0]-> b(b(b(x1130))) peak: b(b(x)) <-12|[==1,=?16]- c(a(x)) -11|[==1,>=0]-> a(b(x)) joins (1): b(b(x)) -5|[==1,>=0]-> a(b(x)) peak: b(b(b(x1132))) <-12|0[==1,=?16]- b(c(a(x1132))) -13|[==1,>=0]-> a(b(a(x1132))) joins (1): b(b(b(x1132))) -5|[==1,>=0]-> a(b(b(x1132))) a(b(a(x1132))) -8|0[==1,>=0]-> a(b(b(x1132))) peak: b(b(b(x1133))) <-12|0[==1,=?16]- b(c(a(x1133))) -14|[==1,>=0]-> b(b(a(x1133))) joins (1): b(b(a(x1133))) -8|0[==1,>=0]-> b(b(b(x1133))) peak: c(b(b(x1134))) <-12|0[==1,=?16]- c(c(a(x1134))) -17|[==1,>=0]-> a(b(a(x1134))) joins (1): c(b(b(x1134))) -16|[==1,>?1]-> b(a(b(x1134))) -2|[==1,>=0]-> a(b(b(x1134))) a(b(a(x1134))) -8|0[==1,>=0]-> a(b(b(x1134))) peak: a(b(x)) <-13|[==1,=>0]- b(c(x)) -1|[==1,?=16]-> b(a(x)) joins (1): b(a(x)) -2|[==1,=>0]-> a(b(x)) peak: c(a(b(x1136))) <-13|0[==1,=>0]- c(b(c(x1136))) -3|[==1,?=17]-> c(c(c(x1136))) joins (1): c(c(c(x1136))) -17|0[==1,=>0]-> c(a(b(x1136))) peak: b(a(b(x1137))) <-13|0[==1,==0]- b(b(c(x1137))) -5|[==1,==0]-> a(b(c(x1137))) joins (1): b(a(b(x1137))) -2|[==1,==0]-> a(b(b(x1137))) a(b(c(x1137))) -14|0[==1,==0]-> a(b(b(x1137))) peak: a(b(x)) <-13|[==1,=>0]- b(c(x)) -7|[==1,?=27]-> c(c(x)) joins (1): c(c(x)) -17|[==1,=>0]-> a(b(x)) peak: c(a(b(x1139))) <-13|0[==1,=>0]- c(b(c(x1139))) -9|[==1,?=17]-> c(a(c(x1139))) joins (1): c(a(c(x1139))) -6|[==1,?>4]-> c(c(c(x1139))) -17|0[==1,=>0]-> c(a(b(x1139))) peak: a(b(x)) <-13|[==1,==0]- b(c(x)) -14|[==1,==0]-> b(b(x)) joins (1): b(b(x)) -5|[==1,==0]-> a(b(x)) peak: c(a(b(x1141))) <-13|0[==1,=>0]- c(b(c(x1141))) -15|[==1,?=16]-> b(b(c(x1141))) joins (1): c(a(b(x1141))) -12|[==1,?=16]-> b(b(b(x1141))) b(b(c(x1141))) -14|0[==1,=>0]-> b(b(b(x1141))) peak: c(a(b(x1142))) <-13|0[==1,=>0]- c(b(c(x1142))) -16|[==1,?=1]-> b(a(c(x1142))) joins (1): c(a(b(x1142))) -11|[==1,=>0]-> a(b(b(x1142))) b(a(c(x1142))) -2|[==1,=>0]-> a(b(c(x1142))) -14|0[==1,=>0]-> a(b(b(x1142))) peak: b(b(x)) <-14|[==1,=>0]- b(c(x)) -1|[==1,?=16]-> b(a(x)) joins (1): b(a(x)) -8|[==1,=>0]-> b(b(x)) peak: c(b(b(x1144))) <-14|0[==1,=>0]- c(b(c(x1144))) -3|[==1,?=17]-> c(c(c(x1144))) joins (1): c(c(c(x1144))) -4|0[==1,?>16]-> c(b(b(x1144))) peak: b(b(b(x1145))) <-14|0[==1,==0]- b(b(c(x1145))) -5|[==1,==0]-> a(b(c(x1145))) joins (1): b(b(b(x1145))) -5|[==1,==0]-> a(b(b(x1145))) a(b(c(x1145))) -14|0[==1,==0]-> a(b(b(x1145))) peak: b(b(x)) <-14|[==1,=>0]- b(c(x)) -7|[==1,?=27]-> c(c(x)) joins (1): c(c(x)) -4|[==1,?>16]-> b(b(x)) peak: c(b(b(x1147))) <-14|0[==1,=>0]- c(b(c(x1147))) -9|[==1,?=17]-> c(a(c(x1147))) joins (1): c(a(c(x1147))) -6|[==1,?>4]-> c(c(c(x1147))) -4|0[==1,?>16]-> c(b(b(x1147))) peak: b(b(x)) <-14|[==1,==0]- b(c(x)) -13|[==1,==0]-> a(b(x)) joins (1): b(b(x)) -5|[==1,==0]-> a(b(x)) peak: c(b(b(x1149))) <-14|0[==1,=>0]- c(b(c(x1149))) -15|[==1,?=16]-> b(b(c(x1149))) joins (1): c(b(b(x1149))) -15|[==1,?=16]-> b(b(b(x1149))) b(b(c(x1149))) -14|0[==1,=>0]-> b(b(b(x1149))) peak: c(b(b(x1150))) <-14|0[==1,=>0]- c(b(c(x1150))) -16|[==1,?=1]-> b(a(c(x1150))) joins (1): c(b(b(x1150))) -16|[==1,?=1]-> b(a(b(x1150))) b(a(c(x1150))) -8|[==1,=>0]-> b(b(c(x1150))) -13|0[==1,=>0]-> b(a(b(x1150))) peak: b(b(b(x1151))) <-15|0[==1,==16]- b(c(b(x1151))) -1|[==1,==16]-> b(a(b(x1151))) joins (1): b(a(b(x1151))) -8|[==1,>>0]-> b(b(b(x1151))) peak: b(b(x)) <-15|[==1,=>16]- c(b(x)) -3|[==1,?=17]-> c(c(x)) joins (1): c(c(x)) -4|[==1,=>16]-> b(b(x)) peak: c(b(b(x1153))) <-15|0[==1,==16]- c(c(b(x1153))) -4|[==1,==16]-> b(b(b(x1153))) joins (1): c(b(b(x1153))) -15|[==1,==16]-> b(b(b(x1153))) peak: b(b(b(x1154))) <-15|0[==1,=>16]- b(c(b(x1154))) -7|[==1,?=27]-> c(c(b(x1154))) joins (1): c(c(b(x1154))) -4|[==1,=>16]-> b(b(b(x1154))) peak: b(b(x)) <-15|[==1,=>16]- c(b(x)) -9|[==1,?=17]-> c(a(x)) joins (1): c(a(x)) -12|[==1,=>16]-> b(b(x)) peak: c(b(b(x1156))) <-15|0[==1,==16]- c(c(b(x1156))) -10|[==1,==16]-> b(a(b(x1156))) joins (1): c(b(b(x1156))) -16|[==1,>>1]-> b(a(b(x1156))) peak: b(b(b(x1157))) <-15|0[==1,=?16]- b(c(b(x1157))) -13|[==1,>=0]-> a(b(b(x1157))) joins (1): b(b(b(x1157))) -5|[==1,>=0]-> a(b(b(x1157))) peak: b(b(b(x1158))) <-15|0[==1,=?16]- b(c(b(x1158))) -14|[==1,>=0]-> b(b(b(x1158))) joins (1): peak: b(b(x)) <-15|[==1,=?16]- c(b(x)) -16|[==1,>=1]-> b(a(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: c(b(b(x1160))) <-15|0[==1,=?16]- c(c(b(x1160))) -17|[==1,>=0]-> a(b(b(x1160))) joins (1): c(b(b(x1160))) -16|[==1,>?1]-> b(a(b(x1160))) -2|[==1,>=0]-> a(b(b(x1160))) peak: b(b(a(x1161))) <-16|0[==1,=>1]- b(c(b(x1161))) -1|[==1,?=16]-> b(a(b(x1161))) joins (1): b(b(a(x1161))) -2|0[==1,>>0]-> b(a(b(x1161))) peak: b(a(x)) <-16|[==1,=>1]- c(b(x)) -3|[==1,?=17]-> c(c(x)) joins (1): c(c(x)) -10|[==1,?>16]-> b(a(x)) peak: c(b(a(x1163))) <-16|0[==1,=>1]- c(c(b(x1163))) -4|[==1,?=16]-> b(b(b(x1163))) joins (1): c(b(a(x1163))) -2|0[==1,>>0]-> c(a(b(x1163))) -12|[==1,?=16]-> b(b(b(x1163))) peak: b(b(a(x1164))) <-16|0[==1,=>1]- b(c(b(x1164))) -7|[==1,?=27]-> c(c(b(x1164))) joins (1): b(b(a(x1164))) -2|0[==1,>>0]-> b(a(b(x1164))) c(c(b(x1164))) -10|[==1,?>16]-> b(a(b(x1164))) peak: b(a(x)) <-16|[==1,=>1]- c(b(x)) -9|[==1,?=17]-> c(a(x)) joins (1): b(a(x)) -2|[==1,>>0]-> a(b(x)) c(a(x)) -11|[==1,>>0]-> a(b(x)) peak: c(b(a(x1166))) <-16|0[==1,=>1]- c(c(b(x1166))) -10|[==1,?=16]-> b(a(b(x1166))) joins (1): c(b(a(x1166))) -8|0[==1,>>0]-> c(b(b(x1166))) -16|[==1,=>1]-> b(a(b(x1166))) peak: b(b(a(x1167))) <-16|0[==1,=?1]- b(c(b(x1167))) -13|[==1,>=0]-> a(b(b(x1167))) joins (1): b(b(a(x1167))) -2|0[==1,>=0]-> b(a(b(x1167))) -2|[==1,>=0]-> a(b(b(x1167))) peak: b(b(a(x1168))) <-16|0[==1,=?1]- b(c(b(x1168))) -14|[==1,>=0]-> b(b(b(x1168))) joins (1): b(b(a(x1168))) -8|0[==1,>=0]-> b(b(b(x1168))) peak: b(a(x)) <-16|[==1,=>1]- c(b(x)) -15|[==1,?=16]-> b(b(x)) joins (1): b(a(x)) -8|[==1,>>0]-> b(b(x)) peak: c(b(a(x1170))) <-16|0[==1,=?1]- c(c(b(x1170))) -17|[==1,>=0]-> a(b(b(x1170))) joins (1): c(b(a(x1170))) -2|0[==1,>=0]-> c(a(b(x1170))) -11|[==1,>=0]-> a(b(b(x1170))) peak: b(a(b(x1171))) <-17|0[==1,=>0]- b(c(c(x1171))) -1|[==1,?=16]-> b(a(c(x1171))) joins (1): b(a(c(x1171))) -8|[==1,=>0]-> b(b(c(x1171))) -13|0[==1,=>0]-> b(a(b(x1171))) peak: a(b(x)) <-17|[==1,=>0]- c(c(x)) -4|[==1,?=16]-> b(b(x)) joins (1): b(b(x)) -5|[==1,=>0]-> a(b(x)) peak: c(a(b(x1173))) <-17|0[==1,=>0]- c(c(c(x1173))) -4|[==1,?=16]-> b(b(c(x1173))) joins (1): c(a(b(x1173))) -12|[==1,?=16]-> b(b(b(x1173))) b(b(c(x1173))) -14|0[==1,=>0]-> b(b(b(x1173))) peak: b(a(b(x1174))) <-17|0[==1,=>0]- b(c(c(x1174))) -7|[==1,?=27]-> c(c(c(x1174))) joins (1): c(c(c(x1174))) -4|0[==1,?>16]-> c(b(b(x1174))) -16|[==1,?>1]-> b(a(b(x1174))) peak: a(b(x)) <-17|[==1,=>0]- c(c(x)) -10|[==1,?=16]-> b(a(x)) joins (1): b(a(x)) -2|[==1,=>0]-> a(b(x)) peak: c(a(b(x1176))) <-17|0[==1,=>0]- c(c(c(x1176))) -10|[==1,?=16]-> b(a(c(x1176))) joins (1): c(a(b(x1176))) -11|[==1,=>0]-> a(b(b(x1176))) b(a(c(x1176))) -2|[==1,=>0]-> a(b(c(x1176))) -14|0[==1,=>0]-> a(b(b(x1176))) peak: b(a(b(x1177))) <-17|0[==1,==0]- b(c(c(x1177))) -13|[==1,==0]-> a(b(c(x1177))) joins (1): b(a(b(x1177))) -2|[==1,==0]-> a(b(b(x1177))) a(b(c(x1177))) -14|0[==1,==0]-> a(b(b(x1177))) peak: b(a(b(x1178))) <-17|0[==1,==0]- b(c(c(x1178))) -14|[==1,==0]-> b(b(c(x1178))) joins (1): b(b(c(x1178))) -13|0[==1,==0]-> b(a(b(x1178))) peak: c(a(b(x1179))) <-17|0[==1,==0]- c(c(c(x1179))) -17|[==1,==0]-> a(b(c(x1179))) joins (1): c(a(b(x1179))) -11|[==1,==0]-> a(b(b(x1179))) a(b(c(x1179))) -14|0[==1,==0]-> a(b(b(x1179))) Qed