%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN424+1 : TPTP v9.0.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:03:32 PM UTC 2025 % Result : CounterSatisfiable 40.77s 22.15s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN424+1 : TPTP v9.0.0. Released v2.1.0. % 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n007.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 07:24:39 EDT 2025 % 0.12/0.34 % CPUTime : % 40.77/22.15 % 40.77/22.15 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.77/22.15 % 40.77/22.15 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.77/22.17 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a999 > a998 > a997 > a996 > a995 > a994 > a993 > a992 > a991 > a990 > a989 > a988 > a987 > a986 > a985 > a984 > a983 > a982 > a981 > a980 > a979 > a978 > a977 > a976 > a975 > a974 > a973 > a972 > a971 > a970 > a969 > a968 > a967 > a966 > a965 > a964 > a963 > a962 > a961 > a960 > a1189 > a1188 > a1187 > a1186 > a1185 > a1184 > a1183 > a1182 > a1181 > a1180 > a1179 > a1178 > a1177 > a1176 > a1175 > a1174 > a1173 > a1172 > a1171 > a1170 > a1169 > a1168 > a1167 > a1166 > a1165 > a1164 > a1163 > a1162 > a1161 > a1160 > a1159 > a1158 > a1157 > a1156 > a1155 > a1154 > a1153 > a1152 > a1151 > a1150 > a1149 > a1148 > a1147 > a1146 > a1145 > a1144 > a1143 > a1142 > a1141 > a1140 > a1139 > a1138 > a1137 > a1136 > a1135 > a1134 > a1133 > a1132 > a1131 > a1130 > a1129 > a1128 > a1127 > a1126 > a1125 > a1124 > a1123 > a1122 > a1121 > a1120 > a1119 > a1118 > a1117 > a1116 > a1115 > a1114 > a1113 > a1112 > a1111 > a1110 > a1109 > a1108 > a1107 > a1106 > a1105 > a1104 > a1103 > a1102 > a1101 > a1100 > a1099 > a1098 > a1097 > a1096 > a1095 > a1094 > a1093 > a1092 > a1091 > a1090 > a1089 > a1088 > a1087 > a1086 > a1085 > a1084 > a1083 > a1082 > a1081 > a1080 > a1079 > a1078 > a1077 > a1076 > a1075 > a1074 > a1073 > a1072 > a1071 > a1070 > a1069 > a1068 > a1067 > a1066 > a1065 > a1064 > a1063 > a1062 > a1061 > a1060 > a1059 > a1058 > a1057 > a1056 > a1055 > a1054 > a1053 > a1052 > a1051 > a1050 > a1049 > a1048 > a1047 > a1046 > a1045 > a1044 > a1043 > a1042 > a1041 > a1040 > a1039 > a1038 > a1037 > a1036 > a1035 > a1034 > a1033 > a1032 > a1031 > a1030 > a1029 > a1028 > a1027 > a1026 > a1025 > a1024 > a1023 > a1022 > a1021 > a1020 > a1019 > a1018 > a1017 > a1016 > a1015 > a1014 > a1013 > a1012 > a1011 > a1010 > a1009 > a1008 > a1007 > a1006 > a1005 > a1004 > a1003 > a1002 > a1001 > a1000 % 40.77/22.17 % 40.77/22.17 %Foreground sorts: % 40.77/22.17 % 40.77/22.17 % 40.77/22.17 %Background operators: % 40.77/22.17 % 40.77/22.17 % 40.77/22.17 %Foreground operators: % 40.77/22.17 tff(a988, type, a988: $i). % 40.77/22.17 tff(c7_0, type, c7_0: $o). % 40.77/22.17 tff(a1005, type, a1005: $i). % 40.77/22.17 tff(a1027, type, a1027: $i). % 40.77/22.17 tff(a1152, type, a1152: $i). % 40.77/22.17 tff(a1135, type, a1135: $i). % 40.77/22.17 tff(a1126, type, a1126: $i). % 40.77/22.17 tff(a1188, type, a1188: $i). % 40.77/22.17 tff(a1162, type, a1162: $i). % 40.77/22.17 tff(a980, type, a980: $i). % 40.77/22.17 tff(a1171, type, a1171: $i). % 40.77/22.17 tff(a1023, type, a1023: $i). % 40.77/22.17 tff(a1097, type, a1097: $i). % 40.77/22.17 tff(a1133, type, a1133: $i). % 40.77/22.17 tff(a975, type, a975: $i). % 40.77/22.17 tff(c4_0, type, c4_0: $o). % 40.77/22.17 tff(a970, type, a970: $i). % 40.77/22.17 tff(a1108, type, a1108: $i). % 40.77/22.17 tff(a1189, type, a1189: $i). % 40.77/22.17 tff(a1172, type, a1172: $i). % 40.77/22.17 tff(a1128, type, a1128: $i). % 40.77/22.17 tff(a1000, type, a1000: $i). % 40.77/22.17 tff(a1163, type, a1163: $i). % 40.77/22.17 tff(a1018, type, a1018: $i). % 40.77/22.17 tff(c3_0, type, c3_0: $o). % 40.77/22.17 tff(a989, type, a989: $i). % 40.77/22.17 tff(a1003, type, a1003: $i). % 40.77/22.17 tff(a1081, type, a1081: $i). % 40.77/22.17 tff(a1100, type, a1100: $i). % 40.77/22.17 tff(c1_2, type, c1_2: ($i * $i) > $o). % 40.77/22.17 tff(a1119, type, a1119: $i). % 40.77/22.17 tff(a1168, type, a1168: $i). % 40.77/22.17 tff(a1071, type, a1071: $i). % 40.77/22.17 tff(a1054, type, a1054: $i). % 40.77/22.17 tff(a977, type, a977: $i). % 40.77/22.17 tff(a1109, type, a1109: $i). % 40.77/22.17 tff(a1145, type, a1145: $i). % 40.77/22.17 tff(a1117, type, a1117: $i). % 40.77/22.17 tff(a1028, type, a1028: $i). % 40.77/22.17 tff(a991, type, a991: $i). % 40.77/22.17 tff(a987, type, a987: $i). % 40.77/22.17 tff(a1006, type, a1006: $i). % 40.77/22.17 tff(a1138, type, a1138: $i). % 40.77/22.17 tff(a1139, type, a1139: $i). % 40.77/22.17 tff(a985, type, a985: $i). % 40.77/22.17 tff(a968, type, a968: $i). % 40.77/22.17 tff(a1129, type, a1129: $i). % 40.77/22.17 tff(a983, type, a983: $i). % 40.77/22.17 tff(a1157, type, a1157: $i). % 40.77/22.17 tff(a1053, type, a1053: $i). % 40.77/22.17 tff(a990, type, a990: $i). % 40.77/22.17 tff(a1025, type, a1025: $i). % 40.77/22.17 tff(a1021, type, a1021: $i). % 40.77/22.17 tff(a1038, type, a1038: $i). % 40.77/22.17 tff(a1074, type, a1074: $i). % 40.77/22.17 tff(a1079, type, a1079: $i). % 40.77/22.17 tff(a1086, type, a1086: $i). % 40.77/22.17 tff(a1046, type, a1046: $i). % 40.77/22.17 tff(a1147, type, a1147: $i). % 40.77/22.17 tff(a1116, type, a1116: $i). % 40.77/22.17 tff(a1174, type, a1174: $i). % 40.77/22.17 tff(a972, type, a972: $i). % 40.77/22.17 tff(a1013, type, a1013: $i). % 40.77/22.17 tff(a1164, type, a1164: $i). % 40.77/22.17 tff(a1182, type, a1182: $i). % 40.77/22.17 tff(c8_0, type, c8_0: $o). % 40.77/22.17 tff(a1080, type, a1080: $i). % 40.77/22.17 tff(a960, type, a960: $i). % 40.77/22.17 tff(a1065, type, a1065: $i). % 40.77/22.17 tff(a1137, type, a1137: $i). % 40.77/22.17 tff(a1106, type, a1106: $i). % 40.77/22.17 tff(a1165, type, a1165: $i). % 40.77/22.17 tff(a1031, type, a1031: $i). % 40.77/22.17 tff(a1173, type, a1173: $i). % 40.77/22.17 tff(a981, type, a981: $i). % 40.77/22.17 tff(a1177, type, a1177: $i). % 40.77/22.17 tff(a1069, type, a1069: $i). % 40.77/22.17 tff(a1186, type, a1186: $i). % 40.77/22.17 tff(a1076, type, a1076: $i). % 40.77/22.17 tff(a976, type, a976: $i). % 40.77/22.17 tff(a1007, type, a1007: $i). % 40.77/22.17 tff(a1166, type, a1166: $i). % 40.77/22.17 tff(a1030, type, a1030: $i). % 40.77/22.17 tff(a1161, type, a1161: $i). % 40.77/22.17 tff(a1078, type, a1078: $i). % 40.77/22.17 tff(a1015, type, a1015: $i). % 40.77/22.17 tff(a994, type, a994: $i). % 40.77/22.17 tff(c5_0, type, c5_0: $o). % 40.77/22.17 tff(a1082, type, a1082: $i). % 40.77/22.17 tff(a1049, type, a1049: $i). % 40.77/22.17 tff(a965, type, a965: $i). % 40.77/22.17 tff(a1037, type, a1037: $i). % 40.77/22.17 tff(a1052, type, a1052: $i). % 40.77/22.17 tff(a1167, type, a1167: $i). % 40.77/22.17 tff(a1083, type, a1083: $i). % 40.77/22.17 tff(a1012, type, a1012: $i). % 40.77/22.17 tff(a1061, type, a1061: $i). % 40.77/22.17 tff(a974, type, a974: $i). % 40.77/22.17 tff(a1091, type, a1091: $i). % 40.77/22.17 tff(a969, type, a969: $i). % 40.77/22.17 tff(a1160, type, a1160: $i). % 40.77/22.17 tff(c6_0, type, c6_0: $o). % 40.77/22.17 tff(a1099, type, a1099: $i). % 40.77/22.17 tff(c8_2, type, c8_2: ($i * $i) > $o). % 40.77/22.17 tff(a966, type, a966: $i). % 40.77/22.17 tff(a1121, type, a1121: $i). % 40.77/22.17 tff(a1009, type, a1009: $i). % 40.77/22.17 tff(a1087, type, a1087: $i). % 40.77/22.17 tff(a1035, type, a1035: $i). % 40.77/22.17 tff(a1017, type, a1017: $i). % 40.77/22.17 tff(a1048, type, a1048: $i). % 40.77/22.17 tff(a1185, type, a1185: $i). % 40.77/22.17 tff(a1151, type, a1151: $i). % 40.77/22.17 tff(a1008, type, a1008: $i). % 40.77/22.17 tff(a1134, type, a1134: $i). % 40.77/22.17 tff(a1102, type, a1102: $i). % 40.77/22.17 tff(a1010, type, a1010: $i). % 40.77/22.17 tff(a1002, type, a1002: $i). % 40.77/22.17 tff(a1047, type, a1047: $i). % 40.77/22.17 tff(a978, type, a978: $i). % 40.77/22.17 tff(a1104, type, a1104: $i). % 40.77/22.17 tff(a1144, type, a1144: $i). % 40.77/22.17 tff(a1036, type, a1036: $i). % 40.77/22.17 tff(a1111, type, a1111: $i). % 40.77/22.17 tff(a1175, type, a1175: $i). % 40.77/22.17 tff(a1088, type, a1088: $i). % 40.77/22.17 tff(a1149, type, a1149: $i). % 40.77/22.17 tff(a1067, type, a1067: $i). % 40.77/22.17 tff(a1155, type, a1155: $i). % 40.77/22.17 tff(a1084, type, a1084: $i). % 40.77/22.17 tff(a1001, type, a1001: $i). % 40.77/22.17 tff(a1055, type, a1055: $i). % 40.77/22.17 tff(a1178, type, a1178: $i). % 40.77/22.17 tff(a1060, type, a1060: $i). % 40.77/22.17 tff(a982, type, a982: $i). % 40.77/22.17 tff(a1143, type, a1143: $i). % 40.77/22.17 tff(a998, type, a998: $i). % 40.77/22.17 tff(c1_0, type, c1_0: $o). % 40.77/22.17 tff(a1132, type, a1132: $i). % 40.77/22.17 tff(c8_1, type, c8_1: $i > $o). % 40.77/22.17 tff(a971, type, a971: $i). % 40.77/22.17 tff(a1064, type, a1064: $i). % 40.77/22.17 tff(a1085, type, a1085: $i). % 40.77/22.17 tff(a1105, type, a1105: $i). % 40.77/22.17 tff(a1051, type, a1051: $i). % 40.77/22.17 tff(c2_1, type, c2_1: $i > $o). % 40.77/22.17 tff(a967, type, a967: $i). % 40.77/22.17 tff(a1101, type, a1101: $i). % 40.77/22.17 tff(a1033, type, a1033: $i). % 40.77/22.17 tff(a992, type, a992: $i). % 40.77/22.17 tff(a963, type, a963: $i). % 40.77/22.17 tff(a1004, type, a1004: $i). % 40.77/22.17 tff(a1169, type, a1169: $i). % 40.77/22.17 tff(ndr1_1, type, ndr1_1: $i > $o). % 40.77/22.17 tff(c2_0, type, c2_0: $o). % 40.77/22.17 tff(c4_1, type, c4_1: $i > $o). % 40.77/22.17 tff(a1041, type, a1041: $i). % 40.77/22.17 tff(a1058, type, a1058: $i). % 40.77/22.17 tff(a1112, type, a1112: $i). % 40.77/22.17 tff(a1063, type, a1063: $i). % 40.77/22.17 tff(a1039, type, a1039: $i). % 40.77/22.17 tff(a1096, type, a1096: $i). % 40.77/22.17 tff(a1141, type, a1141: $i). % 40.77/22.17 tff(a986, type, a986: $i). % 40.77/22.17 tff(a1090, type, a1090: $i). % 40.77/22.17 tff(a1020, type, a1020: $i). % 40.77/22.17 tff(c9_1, type, c9_1: $i > $o). % 40.77/22.17 tff(a1044, type, a1044: $i). % 40.77/22.17 tff(c10_1, type, c10_1: $i > $o). % 40.77/22.17 tff(c10_0, type, c10_0: $o). % 40.77/22.17 tff(a1184, type, a1184: $i). % 40.77/22.17 tff(a1094, type, a1094: $i). % 40.77/22.17 tff(a1026, type, a1026: $i). % 40.77/22.17 tff(a1120, type, a1120: $i). % 40.77/22.17 tff(a1107, type, a1107: $i). % 40.77/22.17 tff(a1131, type, a1131: $i). % 40.77/22.17 tff(c6_2, type, c6_2: ($i * $i) > $o). % 40.77/22.17 tff(a1114, type, a1114: $i). % 40.77/22.17 tff(a1098, type, a1098: $i). % 40.77/22.17 tff(a1179, type, a1179: $i). % 40.77/22.17 tff(a1016, type, a1016: $i). % 40.77/22.17 tff(a1158, type, a1158: $i). % 40.77/22.17 tff(a1170, type, a1170: $i). % 40.77/22.17 tff(a1183, type, a1183: $i). % 40.77/22.17 tff(a1073, type, a1073: $i). % 40.77/22.17 tff(a1136, type, a1136: $i). % 40.77/22.17 tff(a1014, type, a1014: $i). % 40.77/22.17 tff(a1153, type, a1153: $i). % 40.77/22.17 tff(a1045, type, a1045: $i). % 40.77/22.17 tff(a1075, type, a1075: $i). % 40.77/22.17 tff(ndr1_0, type, ndr1_0: $o). % 40.77/22.17 tff(a1125, type, a1125: $i). % 40.77/22.17 tff(a1187, type, a1187: $i). % 40.77/22.17 tff(a1050, type, a1050: $i). % 40.77/22.17 tff(a1159, type, a1159: $i). % 40.77/22.17 tff(a1043, type, a1043: $i). % 40.77/22.17 tff(a1019, type, a1019: $i). % 40.77/22.17 tff(a1029, type, a1029: $i). % 40.77/22.17 tff(a1057, type, a1057: $i). % 40.77/22.17 tff(c9_2, type, c9_2: ($i * $i) > $o). % 40.77/22.17 tff(c10_2, type, c10_2: ($i * $i) > $o). % 40.77/22.17 tff(a1092, type, a1092: $i). % 40.77/22.17 tff(a1130, type, a1130: $i). % 40.77/22.17 tff(a993, type, a993: $i). % 40.77/22.17 tff(a1115, type, a1115: $i). % 40.77/22.17 tff(a1056, type, a1056: $i). % 40.77/22.17 tff(a1059, type, a1059: $i). % 40.77/22.17 tff(a1022, type, a1022: $i). % 40.77/22.17 tff(a1140, type, a1140: $i). % 40.77/22.17 tff(a1024, type, a1024: $i). % 40.77/22.17 tff(c1_1, type, c1_1: $i > $o). % 40.77/22.17 tff(a1113, type, a1113: $i). % 40.77/22.17 tff(a999, type, a999: $i). % 40.77/22.17 tff(a1103, type, a1103: $i). % 40.77/22.17 tff(a1176, type, a1176: $i). % 40.77/22.17 tff(a1095, type, a1095: $i). % 40.77/22.17 tff(a1156, type, a1156: $i). % 40.77/22.17 tff(c5_2, type, c5_2: ($i * $i) > $o). % 40.77/22.17 tff(a1110, type, a1110: $i). % 40.77/22.17 tff(a1032, type, a1032: $i). % 40.77/22.17 tff(a1089, type, a1089: $i). % 40.77/22.17 tff(c9_0, type, c9_0: $o). % 40.77/22.17 tff(a1062, type, a1062: $i). % 40.77/22.17 tff(c7_1, type, c7_1: $i > $o). % 40.77/22.17 tff(c6_1, type, c6_1: $i > $o). % 40.77/22.17 tff(a1180, type, a1180: $i). % 40.77/22.17 tff(a961, type, a961: $i). % 40.77/22.17 tff(a997, type, a997: $i). % 40.77/22.17 tff(a1124, type, a1124: $i). % 40.77/22.17 tff(a1034, type, a1034: $i). % 40.77/22.17 tff(c4_2, type, c4_2: ($i * $i) > $o). % 40.77/22.17 tff(a1070, type, a1070: $i). % 40.77/22.17 tff(a1181, type, a1181: $i). % 40.77/22.17 tff(a1154, type, a1154: $i). % 40.77/22.17 tff(a1123, type, a1123: $i). % 40.77/22.17 tff(a1072, type, a1072: $i). % 40.77/22.17 tff(a1042, type, a1042: $i). % 40.77/22.17 tff(a962, type, a962: $i). % 40.77/22.17 tff(a1040, type, a1040: $i). % 40.77/22.17 tff(a1142, type, a1142: $i). % 40.77/22.17 tff(a1093, type, a1093: $i). % 40.77/22.17 tff(c5_1, type, c5_1: $i > $o). % 40.77/22.17 tff(c7_2, type, c7_2: ($i * $i) > $o). % 40.77/22.17 tff(c3_2, type, c3_2: ($i * $i) > $o). % 40.77/22.17 tff(a964, type, a964: $i). % 40.77/22.17 tff(a1150, type, a1150: $i). % 40.77/22.17 tff(c2_2, type, c2_2: ($i * $i) > $o). % 40.77/22.17 tff(a1118, type, a1118: $i). % 40.77/22.17 tff(a973, type, a973: $i). % 40.77/22.17 tff(a984, type, a984: $i). % 40.77/22.17 tff(a1127, type, a1127: $i). % 40.77/22.17 tff(a1077, type, a1077: $i). % 40.77/22.17 tff(a995, type, a995: $i). % 40.77/22.17 tff(a1068, type, a1068: $i). % 40.77/22.17 tff(a996, type, a996: $i). % 40.77/22.17 tff(a1011, type, a1011: $i). % 40.77/22.17 tff(a1066, type, a1066: $i). % 40.77/22.17 tff(a1146, type, a1146: $i). % 40.77/22.17 tff(a1122, type, a1122: $i). % 40.77/22.17 tff(a979, type, a979: $i). % 40.77/22.17 tff(a1148, type, a1148: $i). % 40.77/22.17 tff(c3_1, type, c3_1: $i > $o). % 40.77/22.17 % 40.77/22.17 %Saturated clause set: % 40.77/22.17 tff(c_24819, plain, (![X20_30]: (~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | ~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.77/22.17 tff(c_23674, plain, (![X217_287]: (~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.77/22.17 tff(c_23068, plain, (![X58_743]: (~c1_1(X58_743) | ~c2_2(X58_743, a969) | c3_2(X58_743, a969) | ~c1_2(X58_743, a1176) | c4_2(X58_743, a990) | c3_2(X58_743, a990) | ~c10_2(X58_743, a1149) | ~c10_2(X58_743, a969) | ~c10_1(X58_743) | c6_2(X58_743, a969) | ~c5_1(X58_743) | ~c3_1(X58_743) | c9_1(X58_743) | c7_1(X58_743) | ~c6_2(X58_743, a1149) | c2_2(X58_743, a1149) | ~c3_2(X58_743, a1002) | c10_2(X58_743, a1073) | ~c1_2(X58_743, a1002) | c10_2(X58_743, a1002) | ~ndr1_1(X58_743) | ~c4_1(X58_743) | ~c6_1(X58_743) | ~c2_1(X58_743)))). % 40.77/22.17 tff(c_23065, plain, (![X58_743]: (~c1_1(X58_743) | ~c2_2(X58_743, a969) | c3_2(X58_743, a969) | c6_2(X58_743, a1176) | c4_2(X58_743, a990) | c3_2(X58_743, a990) | ~c10_2(X58_743, a1149) | ~c10_2(X58_743, a969) | ~c10_1(X58_743) | c6_2(X58_743, a969) | ~c5_1(X58_743) | ~c3_1(X58_743) | c9_1(X58_743) | c7_1(X58_743) | ~c6_2(X58_743, a1149) | c2_2(X58_743, a1149) | ~c3_2(X58_743, a1002) | c10_2(X58_743, a1073) | ~c1_2(X58_743, a1002) | c10_2(X58_743, a1002) | ~ndr1_1(X58_743) | ~c4_1(X58_743) | ~c6_1(X58_743) | ~c2_1(X58_743)))). % 40.77/22.17 tff(c_24738, plain, (![X20_30]: (~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | ~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.77/22.17 tff(c_23067, plain, (![X58_743]: (~c1_1(X58_743) | ~c2_2(X58_743, a969) | c3_2(X58_743, a969) | c7_2(X58_743, a1176) | c4_2(X58_743, a990) | c3_2(X58_743, a990) | ~c10_2(X58_743, a1149) | ~c10_2(X58_743, a969) | ~c10_1(X58_743) | c6_2(X58_743, a969) | ~c5_1(X58_743) | ~c3_1(X58_743) | c9_1(X58_743) | c7_1(X58_743) | ~c6_2(X58_743, a1149) | c2_2(X58_743, a1149) | ~c3_2(X58_743, a1002) | c10_2(X58_743, a1073) | ~c1_2(X58_743, a1002) | c10_2(X58_743, a1002) | ~ndr1_1(X58_743) | ~c4_1(X58_743) | ~c6_1(X58_743) | ~c2_1(X58_743)))). % 40.77/22.18 tff(c_23706, plain, (![X217_287]: (~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.77/22.18 tff(c_22998, plain, (![X58_742]: (~c1_1(X58_742) | ~c2_2(X58_742, a969) | c3_2(X58_742, a969) | c6_2(X58_742, a1176) | c4_2(X58_742, a990) | c3_2(X58_742, a990) | ~c10_2(X58_742, a1149) | ~c10_2(X58_742, a969) | ~c10_1(X58_742) | c6_2(X58_742, a969) | ~c5_1(X58_742) | ~c3_1(X58_742) | c9_1(X58_742) | c7_1(X58_742) | ~c6_2(X58_742, a1149) | c2_2(X58_742, a1149) | ~c3_2(X58_742, a1002) | c3_2(X58_742, a1073) | ~c1_2(X58_742, a1002) | c10_2(X58_742, a1002) | ~ndr1_1(X58_742) | ~c4_1(X58_742) | ~c6_1(X58_742) | ~c2_1(X58_742)))). % 40.77/22.18 tff(c_23001, plain, (![X58_742]: (~c1_1(X58_742) | ~c2_2(X58_742, a969) | c3_2(X58_742, a969) | ~c1_2(X58_742, a1176) | c4_2(X58_742, a990) | c3_2(X58_742, a990) | ~c10_2(X58_742, a1149) | ~c10_2(X58_742, a969) | ~c10_1(X58_742) | c6_2(X58_742, a969) | ~c5_1(X58_742) | ~c3_1(X58_742) | c9_1(X58_742) | c7_1(X58_742) | ~c6_2(X58_742, a1149) | c2_2(X58_742, a1149) | ~c3_2(X58_742, a1002) | c3_2(X58_742, a1073) | ~c1_2(X58_742, a1002) | c10_2(X58_742, a1002) | ~ndr1_1(X58_742) | ~c4_1(X58_742) | ~c6_1(X58_742) | ~c2_1(X58_742)))). % 40.77/22.18 tff(c_24702, plain, (![X217_822]: (c1_2(X217_822, a988) | c10_2(X217_822, a989) | c7_1(X217_822) | c2_2(X217_822, a990) | ~c3_2(X217_822, a1002) | c10_2(X217_822, a1073) | ~c1_2(X217_822, a1002) | c10_2(X217_822, a1002) | ~c4_1(X217_822) | ~c6_1(X217_822) | ~c2_1(X217_822) | c10_2(X217_822, a990) | c8_1(X217_822) | c5_1(X217_822) | ~c1_1(X217_822) | ~c2_2(X217_822, a989) | c3_2(X217_822, a990) | ~c1_2(X217_822, a1176) | c9_1(X217_822) | c3_2(X217_822, a989) | ~ndr1_1(X217_822)))). % 40.77/22.18 tff(c_24701, plain, (![X217_822]: (c10_2(X217_822, a988) | c10_2(X217_822, a989) | c7_1(X217_822) | c2_2(X217_822, a990) | ~c3_2(X217_822, a1002) | c10_2(X217_822, a1073) | ~c1_2(X217_822, a1002) | c10_2(X217_822, a1002) | ~c4_1(X217_822) | ~c6_1(X217_822) | ~c2_1(X217_822) | c10_2(X217_822, a990) | c8_1(X217_822) | c5_1(X217_822) | ~c1_1(X217_822) | ~c2_2(X217_822, a989) | c3_2(X217_822, a990) | ~c1_2(X217_822, a1176) | c9_1(X217_822) | c3_2(X217_822, a989) | ~ndr1_1(X217_822)))). % 40.77/22.18 tff(c_24439, plain, (![X217_287, X218_760]: (c7_1(X217_287) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c10_2(X217_287, a990) | c8_1(X217_287) | c5_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_760) | c3_2(X217_287, a990) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c3_2(X217_287, X218_760) | ~ndr1_1(X217_287) | c4_2(X217_287, X218_760)))). % 40.77/22.18 tff(c_23000, plain, (![X58_742]: (~c1_1(X58_742) | ~c2_2(X58_742, a969) | c3_2(X58_742, a969) | c7_2(X58_742, a1176) | c4_2(X58_742, a990) | c3_2(X58_742, a990) | ~c10_2(X58_742, a1149) | ~c10_2(X58_742, a969) | ~c10_1(X58_742) | c6_2(X58_742, a969) | ~c5_1(X58_742) | ~c3_1(X58_742) | c9_1(X58_742) | c7_1(X58_742) | ~c6_2(X58_742, a1149) | c2_2(X58_742, a1149) | ~c3_2(X58_742, a1002) | c3_2(X58_742, a1073) | ~c1_2(X58_742, a1002) | c10_2(X58_742, a1002) | ~ndr1_1(X58_742) | ~c4_1(X58_742) | ~c6_1(X58_742) | ~c2_1(X58_742)))). % 40.77/22.18 tff(c_24336, plain, (![X217_814]: (c1_2(X217_814, a988) | c10_2(X217_814, a989) | c7_1(X217_814) | c2_2(X217_814, a990) | ~c3_2(X217_814, a1002) | c3_2(X217_814, a1073) | ~c1_2(X217_814, a1002) | c10_2(X217_814, a1002) | ~c4_1(X217_814) | ~c6_1(X217_814) | ~c2_1(X217_814) | c10_2(X217_814, a990) | c8_1(X217_814) | c5_1(X217_814) | ~c1_1(X217_814) | ~c2_2(X217_814, a989) | c3_2(X217_814, a990) | ~c1_2(X217_814, a1176) | c9_1(X217_814) | c3_2(X217_814, a989) | ~ndr1_1(X217_814)))). % 40.77/22.18 tff(c_24335, plain, (![X217_814]: (c10_2(X217_814, a988) | c10_2(X217_814, a989) | c7_1(X217_814) | c2_2(X217_814, a990) | ~c3_2(X217_814, a1002) | c3_2(X217_814, a1073) | ~c1_2(X217_814, a1002) | c10_2(X217_814, a1002) | ~c4_1(X217_814) | ~c6_1(X217_814) | ~c2_1(X217_814) | c10_2(X217_814, a990) | c8_1(X217_814) | c5_1(X217_814) | ~c1_1(X217_814) | ~c2_2(X217_814, a989) | c3_2(X217_814, a990) | ~c1_2(X217_814, a1176) | c9_1(X217_814) | c3_2(X217_814, a989) | ~ndr1_1(X217_814)))). % 40.77/22.18 tff(c_24073, plain, (![X217_287, X218_754]: (c7_1(X217_287) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c10_2(X217_287, a990) | c8_1(X217_287) | c5_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_754) | c3_2(X217_287, a990) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c3_2(X217_287, X218_754) | ~ndr1_1(X217_287) | c4_2(X217_287, X218_754)))). % 40.77/22.18 tff(c_23949, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.77/22.18 tff(c_23938, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_23927, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_24055, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a1149) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | c9_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1149) | c2_2(X20_30, a1149) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_24044, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a1149) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | c9_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1149) | c2_2(X20_30, a1149) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_22994, plain, (![X58_742]: (~c1_1(X58_742) | ~c2_2(X58_742, a969) | c3_2(X58_742, a969) | ~c6_2(X58_742, a990) | c2_2(X58_742, a990) | ~c10_2(X58_742, a1149) | ~c10_2(X58_742, a969) | ~c10_1(X58_742) | c6_2(X58_742, a969) | ~c5_1(X58_742) | ~c3_1(X58_742) | c9_1(X58_742) | c7_1(X58_742) | ~c6_2(X58_742, a1149) | c2_2(X58_742, a1149) | ~c3_2(X58_742, a1002) | c3_2(X58_742, a1073) | ~c1_2(X58_742, a1002) | c10_2(X58_742, a1002) | ~ndr1_1(X58_742) | ~c4_1(X58_742) | ~c6_1(X58_742) | ~c2_1(X58_742)))). % 40.91/22.18 tff(c_23062, plain, (![X58_743]: (~c1_1(X58_743) | ~c2_2(X58_743, a969) | c3_2(X58_743, a969) | ~c6_2(X58_743, a990) | c2_2(X58_743, a990) | ~c10_2(X58_743, a1149) | ~c10_2(X58_743, a969) | ~c10_1(X58_743) | c6_2(X58_743, a969) | ~c5_1(X58_743) | ~c3_1(X58_743) | c9_1(X58_743) | c7_1(X58_743) | ~c6_2(X58_743, a1149) | c2_2(X58_743, a1149) | ~c3_2(X58_743, a1002) | c10_2(X58_743, a1073) | ~c1_2(X58_743, a1002) | c10_2(X58_743, a1002) | ~ndr1_1(X58_743) | ~c4_1(X58_743) | ~c6_1(X58_743) | ~c2_1(X58_743)))). % 40.91/22.18 tff(c_23916, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_23962, plain, (![X20_30]: (~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c3_1(X20_30) | ~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.18 tff(c_20908, plain, (![X58_667]: (~c1_1(X58_667) | ~c2_2(X58_667, a969) | c3_2(X58_667, a969) | c7_2(X58_667, a1176) | c4_2(X58_667, a990) | c3_2(X58_667, a990) | ~c10_2(X58_667, a1149) | ~c10_2(X58_667, a969) | ~c10_1(X58_667) | c6_2(X58_667, a969) | ~c3_1(X58_667) | c9_1(X58_667) | c7_1(X58_667) | ~c6_2(X58_667, a1149) | c2_2(X58_667, a1149) | ~c3_2(X58_667, a1002) | c6_2(X58_667, a1002) | ~c4_2(X58_667, a1002) | ~ndr1_1(X58_667) | ~c5_1(X58_667) | ~c6_1(X58_667) | ~c2_1(X58_667)))). % 40.91/22.18 tff(c_20906, plain, (![X58_667]: (~c1_1(X58_667) | ~c2_2(X58_667, a969) | c3_2(X58_667, a969) | c6_2(X58_667, a1176) | c4_2(X58_667, a990) | c3_2(X58_667, a990) | ~c10_2(X58_667, a1149) | ~c10_2(X58_667, a969) | ~c10_1(X58_667) | c6_2(X58_667, a969) | ~c3_1(X58_667) | c9_1(X58_667) | c7_1(X58_667) | ~c6_2(X58_667, a1149) | c2_2(X58_667, a1149) | ~c3_2(X58_667, a1002) | c6_2(X58_667, a1002) | ~c4_2(X58_667, a1002) | ~ndr1_1(X58_667) | ~c5_1(X58_667) | ~c6_1(X58_667) | ~c2_1(X58_667)))). % 40.91/22.18 tff(c_20909, plain, (![X58_667]: (~c1_1(X58_667) | ~c2_2(X58_667, a969) | c3_2(X58_667, a969) | ~c1_2(X58_667, a1176) | c4_2(X58_667, a990) | c3_2(X58_667, a990) | ~c10_2(X58_667, a1149) | ~c10_2(X58_667, a969) | ~c10_1(X58_667) | c6_2(X58_667, a969) | ~c3_1(X58_667) | c9_1(X58_667) | c7_1(X58_667) | ~c6_2(X58_667, a1149) | c2_2(X58_667, a1149) | ~c3_2(X58_667, a1002) | c6_2(X58_667, a1002) | ~c4_2(X58_667, a1002) | ~ndr1_1(X58_667) | ~c5_1(X58_667) | ~c6_1(X58_667) | ~c2_1(X58_667)))). % 40.91/22.19 tff(c_23109, plain, (![X217_287]: (~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c3_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_22999, plain, (![X58_742]: (~c10_2(X58_742, a990) | ~c1_1(X58_742) | ~c2_2(X58_742, a969) | c3_2(X58_742, a969) | ~c10_2(X58_742, a1149) | ~c10_2(X58_742, a969) | ~c10_1(X58_742) | c6_2(X58_742, a969) | ~c5_1(X58_742) | ~c3_1(X58_742) | c9_1(X58_742) | c7_1(X58_742) | ~c6_2(X58_742, a1149) | c2_2(X58_742, a1149) | ~c3_2(X58_742, a1002) | c3_2(X58_742, a1073) | ~c1_2(X58_742, a1002) | c10_2(X58_742, a1002) | ~ndr1_1(X58_742) | ~c4_1(X58_742) | ~c6_1(X58_742) | ~c2_1(X58_742)))). % 40.91/22.19 tff(c_23066, plain, (![X58_743]: (~c10_2(X58_743, a990) | ~c1_1(X58_743) | ~c2_2(X58_743, a969) | c3_2(X58_743, a969) | ~c10_2(X58_743, a1149) | ~c10_2(X58_743, a969) | ~c10_1(X58_743) | c6_2(X58_743, a969) | ~c5_1(X58_743) | ~c3_1(X58_743) | c9_1(X58_743) | c7_1(X58_743) | ~c6_2(X58_743, a1149) | c2_2(X58_743, a1149) | ~c3_2(X58_743, a1002) | c10_2(X58_743, a1073) | ~c1_2(X58_743, a1002) | c10_2(X58_743, a1002) | ~ndr1_1(X58_743) | ~c4_1(X58_743) | ~c6_1(X58_743) | ~c2_1(X58_743)))). % 40.91/22.19 tff(c_23677, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_23678, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_23711, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_23710, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_23543, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_23734, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c2_2(X20_30, a990) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c4_2(X20_30, a990) | c10_2(X20_30, a990) | c8_1(X20_30) | c5_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_23745, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | ~c10_2(X20_30, a1149) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c3_1(X20_30) | c9_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1149) | c2_2(X20_30, a1149) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_23723, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c2_2(X20_30, a990) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c4_2(X20_30, a990) | c10_2(X20_30, a990) | c8_1(X20_30) | c5_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_22918, plain, (![X75_106, X218_728]: (~c2_2(X75_106, a1176) | c3_2(X75_106, a1176) | ~c1_1(X75_106) | ~c2_2(X75_106, X218_728) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c9_1(X75_106) | c4_2(X75_106, X218_728) | c3_2(X75_106, X218_728) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.19 tff(c_22927, plain, (![X75_106, X218_730]: (~c2_2(X75_106, a1176) | c3_2(X75_106, a1176) | ~c1_1(X75_106) | ~c2_2(X75_106, X218_730) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c9_1(X75_106) | c4_2(X75_106, X218_730) | c3_2(X75_106, X218_730) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.19 tff(c_20904, plain, (![X58_667]: (~c1_1(X58_667) | ~c2_2(X58_667, a969) | c3_2(X58_667, a969) | ~c6_2(X58_667, a990) | c2_2(X58_667, a990) | ~c10_2(X58_667, a1149) | ~c10_2(X58_667, a969) | ~c10_1(X58_667) | c6_2(X58_667, a969) | ~c3_1(X58_667) | c9_1(X58_667) | c7_1(X58_667) | ~c6_2(X58_667, a1149) | c2_2(X58_667, a1149) | ~c3_2(X58_667, a1002) | c6_2(X58_667, a1002) | ~c4_2(X58_667, a1002) | ~ndr1_1(X58_667) | ~c5_1(X58_667) | ~c6_1(X58_667) | ~c2_1(X58_667)))). % 40.91/22.19 tff(c_22880, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c2_2(X75_106, a990) | ~c10_2(X75_106, a1111) | ~c10_1(X75_106) | c7_1(X75_106) | ~c6_2(X75_106, a1111) | c2_2(X75_106, a1111) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.19 tff(c_22869, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c2_2(X75_106, a990) | ~c10_2(X75_106, a1111) | ~c10_1(X75_106) | c7_1(X75_106) | ~c6_2(X75_106, a1111) | c2_2(X75_106, a1111) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.19 tff(c_23645, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a969) | c3_2(X20_30, a969) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c2_1(X20_30) | ~c10_2(X20_30, a969) | ~c10_1(X20_30) | c6_2(X20_30, a969) | ~c5_1(X20_30) | ~c3_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a1149) | c3_2(X20_30, a1149) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_20407, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c3_2(X2_10, a1002) | c10_2(X2_10, a1073) | ~c1_2(X2_10, a1002) | c10_2(X2_10, a1002) | ~c4_1(X2_10) | ~c6_1(X2_10) | ~c2_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.19 tff(c_20484, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c3_2(X2_10, a1002) | c3_2(X2_10, a1073) | ~c1_2(X2_10, a1002) | c10_2(X2_10, a1002) | ~c4_1(X2_10) | ~c6_1(X2_10) | ~c2_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.19 tff(c_23111, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.19 tff(c_19703, plain, (![X58_579]: (~c1_1(X58_579) | ~c2_2(X58_579, a1112) | c3_2(X58_579, a1112) | c6_2(X58_579, a1176) | c9_1(X58_579) | c4_2(X58_579, a990) | c3_2(X58_579, a990) | ~c10_2(X58_579, a1111) | ~c10_1(X58_579) | c7_1(X58_579) | ~c6_2(X58_579, a1111) | c2_2(X58_579, a1111) | ~c3_2(X58_579, a1002) | c3_2(X58_579, a1073) | ~c1_2(X58_579, a1002) | c10_2(X58_579, a1002) | ~ndr1_1(X58_579) | ~c4_1(X58_579) | ~c6_1(X58_579) | ~c2_1(X58_579)))). % 40.91/22.19 tff(c_23564, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a990) | c3_2(X20_30, a990) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.19 tff(c_19836, plain, (![X58_586]: (~c1_1(X58_586) | ~c2_2(X58_586, a1112) | c3_2(X58_586, a1112) | c6_2(X58_586, a1176) | c9_1(X58_586) | c4_2(X58_586, a990) | c3_2(X58_586, a990) | ~c10_2(X58_586, a1111) | ~c10_1(X58_586) | c7_1(X58_586) | ~c6_2(X58_586, a1111) | c2_2(X58_586, a1111) | ~c3_2(X58_586, a1002) | c10_2(X58_586, a1073) | ~c1_2(X58_586, a1002) | c10_2(X58_586, a1002) | ~ndr1_1(X58_586) | ~c4_1(X58_586) | ~c6_1(X58_586) | ~c2_1(X58_586)))). % 40.91/22.19 tff(c_19705, plain, (![X58_579]: (~c1_1(X58_579) | ~c2_2(X58_579, a1112) | c3_2(X58_579, a1112) | c7_2(X58_579, a1176) | c9_1(X58_579) | c4_2(X58_579, a990) | c3_2(X58_579, a990) | ~c10_2(X58_579, a1111) | ~c10_1(X58_579) | c7_1(X58_579) | ~c6_2(X58_579, a1111) | c2_2(X58_579, a1111) | ~c3_2(X58_579, a1002) | c3_2(X58_579, a1073) | ~c1_2(X58_579, a1002) | c10_2(X58_579, a1002) | ~ndr1_1(X58_579) | ~c4_1(X58_579) | ~c6_1(X58_579) | ~c2_1(X58_579)))). % 40.91/22.19 tff(c_19839, plain, (![X58_586]: (~c1_1(X58_586) | ~c2_2(X58_586, a1112) | c3_2(X58_586, a1112) | ~c1_2(X58_586, a1176) | c9_1(X58_586) | c4_2(X58_586, a990) | c3_2(X58_586, a990) | ~c10_2(X58_586, a1111) | ~c10_1(X58_586) | c7_1(X58_586) | ~c6_2(X58_586, a1111) | c2_2(X58_586, a1111) | ~c3_2(X58_586, a1002) | c10_2(X58_586, a1073) | ~c1_2(X58_586, a1002) | c10_2(X58_586, a1002) | ~ndr1_1(X58_586) | ~c4_1(X58_586) | ~c6_1(X58_586) | ~c2_1(X58_586)))). % 40.91/22.19 tff(c_22317, plain, (![X159_214]: (c7_1(X159_214) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a990) | c8_1(X159_214) | c5_1(X159_214) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.19 tff(c_22260, plain, (![X159_214]: (c7_1(X159_214) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a990) | c8_1(X159_214) | c5_1(X159_214) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.20 tff(c_23112, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.20 tff(c_22796, plain, (![X159_214]: (c7_1(X159_214) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a990) | c8_1(X159_214) | c5_1(X159_214) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.20 tff(c_22853, plain, (![X159_214]: (c7_1(X159_214) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a990) | c8_1(X159_214) | c5_1(X159_214) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.20 tff(c_20907, plain, (![X58_667]: (~c10_2(X58_667, a990) | ~c1_1(X58_667) | ~c2_2(X58_667, a969) | c3_2(X58_667, a969) | ~c10_2(X58_667, a1149) | ~c10_2(X58_667, a969) | ~c10_1(X58_667) | c6_2(X58_667, a969) | ~c3_1(X58_667) | c9_1(X58_667) | c7_1(X58_667) | ~c6_2(X58_667, a1149) | c2_2(X58_667, a1149) | ~c3_2(X58_667, a1002) | c6_2(X58_667, a1002) | ~c4_2(X58_667, a1002) | ~ndr1_1(X58_667) | ~c5_1(X58_667) | ~c6_1(X58_667) | ~c2_1(X58_667)))). % 40.91/22.20 tff(c_19838, plain, (![X58_586]: (~c1_1(X58_586) | ~c2_2(X58_586, a1112) | c3_2(X58_586, a1112) | c7_2(X58_586, a1176) | c9_1(X58_586) | c4_2(X58_586, a990) | c3_2(X58_586, a990) | ~c10_2(X58_586, a1111) | ~c10_1(X58_586) | c7_1(X58_586) | ~c6_2(X58_586, a1111) | c2_2(X58_586, a1111) | ~c3_2(X58_586, a1002) | c10_2(X58_586, a1073) | ~c1_2(X58_586, a1002) | c10_2(X58_586, a1002) | ~ndr1_1(X58_586) | ~c4_1(X58_586) | ~c6_1(X58_586) | ~c2_1(X58_586)))). % 40.91/22.20 tff(c_21500, plain, (![X75_106, X218_679]: (~c1_1(X75_106) | ~c2_2(X75_106, X218_679) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c1_2(X75_106, a1176) | c9_1(X75_106) | c4_2(X75_106, X218_679) | c3_2(X75_106, X218_679) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_21007, plain, (![X75_106, X218_671]: (~c1_1(X75_106) | ~c2_2(X75_106, X218_671) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c6_2(X75_106, a1176) | c9_1(X75_106) | c4_2(X75_106, X218_671) | c3_2(X75_106, X218_671) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_21491, plain, (![X75_106, X218_677]: (~c1_1(X75_106) | ~c2_2(X75_106, X218_677) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c6_2(X75_106, a1176) | c9_1(X75_106) | c4_2(X75_106, X218_677) | c3_2(X75_106, X218_677) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_20852, plain, (![X75_106, X218_666]: (~c1_1(X75_106) | ~c2_2(X75_106, X218_666) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c1_2(X75_106, a1176) | c9_1(X75_106) | c4_2(X75_106, X218_666) | c3_2(X75_106, X218_666) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_23325, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a990) | c3_2(X20_30, a990) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_19706, plain, (![X58_579]: (~c1_1(X58_579) | ~c2_2(X58_579, a1112) | c3_2(X58_579, a1112) | ~c1_2(X58_579, a1176) | c9_1(X58_579) | c4_2(X58_579, a990) | c3_2(X58_579, a990) | ~c10_2(X58_579, a1111) | ~c10_1(X58_579) | c7_1(X58_579) | ~c6_2(X58_579, a1111) | c2_2(X58_579, a1111) | ~c3_2(X58_579, a1002) | c3_2(X58_579, a1073) | ~c1_2(X58_579, a1002) | c10_2(X58_579, a1002) | ~ndr1_1(X58_579) | ~c4_1(X58_579) | ~c6_1(X58_579) | ~c2_1(X58_579)))). % 40.91/22.20 tff(c_23238, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, a990) | c3_2(X20_30, a990) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_18336, plain, (![X58_448]: (~c1_1(X58_448) | ~c2_2(X58_448, a1112) | c3_2(X58_448, a1112) | c7_2(X58_448, a1176) | c9_1(X58_448) | c4_2(X58_448, a990) | c3_2(X58_448, a990) | ~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.20 tff(c_18305, plain, (![X58_448]: (~c1_1(X58_448) | ~c2_2(X58_448, a1112) | c3_2(X58_448, a1112) | ~c1_2(X58_448, a1176) | c9_1(X58_448) | c4_2(X58_448, a990) | c3_2(X58_448, a990) | ~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.20 tff(c_20737, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1176) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c9_1(X75_106) | c4_2(X75_106, a1176) | c3_2(X75_106, a1176) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_18546, plain, (![X58_448]: (~c1_1(X58_448) | ~c2_2(X58_448, a1112) | c3_2(X58_448, a1112) | c6_2(X58_448, a1176) | c9_1(X58_448) | c4_2(X58_448, a990) | c3_2(X58_448, a990) | ~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.20 tff(c_20726, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1176) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | c9_1(X75_106) | c4_2(X75_106, a1176) | c3_2(X75_106, a1176) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_19655, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c3_2(X2_10, a1002) | c6_2(X2_10, a1002) | ~c4_2(X2_10, a1002) | ~c6_1(X2_10) | ~c2_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.20 tff(c_17831, plain, (![X58_474]: (~c10_2(X58_474, a1149) | ~c10_2(X58_474, a969) | ~c10_1(X58_474) | c6_2(X58_474, a969) | c7_2(X58_474, a969) | ~c5_1(X58_474) | ~c3_1(X58_474) | c9_1(X58_474) | c7_1(X58_474) | ~c6_2(X58_474, a1149) | c2_2(X58_474, a1149) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.20 tff(c_17635, plain, (![X58_462]: (~c10_2(X58_462, a1149) | ~c10_2(X58_462, a969) | ~c10_1(X58_462) | c6_2(X58_462, a969) | c7_2(X58_462, a969) | ~c5_1(X58_462) | ~c3_1(X58_462) | c9_1(X58_462) | c7_1(X58_462) | ~c6_2(X58_462, a1149) | c2_2(X58_462, a1149) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.20 tff(c_22901, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_22939, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_22919, plain, (![X20_30, X218_728]: (~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c1_1(X20_30) | ~c2_2(X20_30, X218_728) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, X218_728) | c3_2(X20_30, X218_728) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_22928, plain, (![X20_30, X218_730]: (~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c1_1(X20_30) | ~c2_2(X20_30, X218_730) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, X218_730) | c3_2(X20_30, X218_730) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_22881, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21069, plain, (![X217_672, X218_673]: (~c2_2(X217_672, a1176) | c3_2(X217_672, a1176) | ~c1_1(X217_672) | ~c2_2(X217_672, X218_673) | c7_1(X217_672) | ~c6_2(X217_672, a990) | c2_2(X217_672, a990) | ~c3_2(X217_672, a1002) | c3_2(X217_672, a1073) | ~c1_2(X217_672, a1002) | c10_2(X217_672, a1002) | ~c4_1(X217_672) | ~c6_1(X217_672) | ~c2_1(X217_672) | c9_1(X217_672) | c4_2(X217_672, X218_673) | c3_2(X217_672, X218_673) | ~ndr1_1(X217_672)))). % 40.91/22.20 tff(c_20982, plain, (![X217_668, X218_669]: (~c2_2(X217_668, a1176) | c3_2(X217_668, a1176) | ~c1_1(X217_668) | ~c2_2(X217_668, X218_669) | c7_1(X217_668) | ~c6_2(X217_668, a990) | c2_2(X217_668, a990) | ~c3_2(X217_668, a1002) | c10_2(X217_668, a1073) | ~c1_2(X217_668, a1002) | c10_2(X217_668, a1002) | ~c4_1(X217_668) | ~c6_1(X217_668) | ~c2_1(X217_668) | c9_1(X217_668) | c4_2(X217_668, X218_669) | c3_2(X217_668, X218_669) | ~ndr1_1(X217_668)))). % 40.91/22.20 tff(c_22870, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_20471, plain, (![X58_462]: (~c1_1(X58_462) | ~c2_2(X58_462, a1112) | c3_2(X58_462, a1112) | ~c6_2(X58_462, a990) | c2_2(X58_462, a990) | ~c10_2(X58_462, a1111) | ~c10_1(X58_462) | c7_1(X58_462) | ~c6_2(X58_462, a1111) | c2_2(X58_462, a1111) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.20 tff(c_20393, plain, (![X58_474]: (~c1_1(X58_474) | ~c2_2(X58_474, a1112) | c3_2(X58_474, a1112) | ~c6_2(X58_474, a990) | c2_2(X58_474, a990) | ~c10_2(X58_474, a1111) | ~c10_1(X58_474) | c7_1(X58_474) | ~c6_2(X58_474, a1111) | c2_2(X58_474, a1111) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.20 tff(c_20531, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c2_1(X75_106) | c10_2(X75_106, a1111) | ~c6_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_20508, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c2_1(X75_106) | c10_2(X75_106, a1111) | ~c6_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_20404, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.20 tff(c_20497, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c2_1(X75_106) | ~c3_2(X75_106, a1111) | ~c6_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_20520, plain, (![X75_106]: (~c1_1(X75_106) | ~c2_2(X75_106, a1112) | c3_2(X75_106, a1112) | c7_1(X75_106) | c2_2(X75_106, a990) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~c4_1(X75_106) | ~c2_1(X75_106) | ~c3_2(X75_106, a1111) | ~c6_1(X75_106) | ~c4_2(X75_106, a990) | c10_2(X75_106, a990) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.20 tff(c_18238, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c7_2(X2_10, a989) | ~c3_2(X2_10, a989) | ~c5_2(X2_10, a988) | ~c6_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.20 tff(c_19198, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c7_2(X2_10, a989) | ~c3_2(X2_10, a989) | c1_2(X2_10, a988) | ~c6_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.20 tff(c_18191, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_1(X2_10) | ~c6_2(X2_10, a990) | c2_2(X2_10, a990) | ~c7_2(X2_10, a989) | ~c3_2(X2_10, a989) | c10_2(X2_10, a988) | ~c6_1(X2_10) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.20 tff(c_20481, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.20 tff(c_19189, plain, (![X217_287, X218_289]: (~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.20 tff(c_18848, plain, (![X217_527, X218_528]: (~c2_2(X217_527, a1176) | c3_2(X217_527, a1176) | c7_1(X217_527) | ~c6_2(X217_527, a990) | c2_2(X217_527, a990) | ~c7_2(X217_527, a989) | ~c3_2(X217_527, a989) | ~c5_2(X217_527, a988) | ~c6_1(X217_527) | ~c1_1(X217_527) | ~c2_2(X217_527, X218_528) | c4_2(X217_527, a990) | c3_2(X217_527, a990) | c9_1(X217_527) | c4_2(X217_527, X218_528) | c3_2(X217_527, X218_528) | ~ndr1_1(X217_527)))). % 40.91/22.20 tff(c_21612, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21565, plain, (![X20_30, X218_688]: (~c2_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c1_1(X20_30) | ~c2_2(X20_30, X218_688) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, X218_688) | c3_2(X20_30, X218_688) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21536, plain, (![X20_30]: (~c10_2(X20_30, a990) | ~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21525, plain, (![X20_30]: (~c10_2(X20_30, a990) | ~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21547, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c6_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21492, plain, (![X20_30, X218_677]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_677) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_677) | c3_2(X20_30, X218_677) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_20853, plain, (![X20_30, X218_666]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_666) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_666) | c3_2(X20_30, X218_666) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_21501, plain, (![X20_30, X218_679]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_679) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_679) | c3_2(X20_30, X218_679) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_18849, plain, (![X217_527, X218_528]: (~c2_2(X217_527, a1176) | c3_2(X217_527, a1176) | c7_1(X217_527) | ~c6_2(X217_527, a990) | c2_2(X217_527, a990) | ~c7_2(X217_527, a989) | ~c3_2(X217_527, a989) | c10_2(X217_527, a988) | ~c6_1(X217_527) | ~c1_1(X217_527) | ~c2_2(X217_527, X218_528) | c4_2(X217_527, a990) | c3_2(X217_527, a990) | c9_1(X217_527) | c4_2(X217_527, X218_528) | c3_2(X217_527, X218_528) | ~ndr1_1(X217_527)))). % 40.91/22.20 tff(c_20678, plain, (![X217_648, X218_649]: (~c2_2(X217_648, a1176) | c3_2(X217_648, a1176) | ~c1_1(X217_648) | ~c2_2(X217_648, X218_649) | c7_1(X217_648) | ~c6_2(X217_648, a990) | c2_2(X217_648, a990) | ~c3_2(X217_648, a1002) | c6_2(X217_648, a1002) | ~c4_2(X217_648, a1002) | ~c5_1(X217_648) | ~c6_1(X217_648) | ~c2_1(X217_648) | c9_1(X217_648) | c4_2(X217_648, X218_649) | c3_2(X217_648, X218_649) | ~ndr1_1(X217_648)))). % 40.91/22.20 tff(c_19649, plain, (![X58_448]: (~c1_1(X58_448) | ~c2_2(X58_448, a1112) | c3_2(X58_448, a1112) | ~c6_2(X58_448, a990) | c2_2(X58_448, a990) | ~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.20 tff(c_19704, plain, (![X58_579]: (~c10_2(X58_579, a990) | ~c1_1(X58_579) | ~c2_2(X58_579, a1112) | c3_2(X58_579, a1112) | ~c10_2(X58_579, a1111) | ~c10_1(X58_579) | c7_1(X58_579) | ~c6_2(X58_579, a1111) | c2_2(X58_579, a1111) | ~c3_2(X58_579, a1002) | c3_2(X58_579, a1073) | ~c1_2(X58_579, a1002) | c10_2(X58_579, a1002) | ~ndr1_1(X58_579) | ~c4_1(X58_579) | ~c6_1(X58_579) | ~c2_1(X58_579)))). % 40.91/22.20 tff(c_19837, plain, (![X58_586]: (~c10_2(X58_586, a990) | ~c1_1(X58_586) | ~c2_2(X58_586, a1112) | c3_2(X58_586, a1112) | ~c10_2(X58_586, a1111) | ~c10_1(X58_586) | c7_1(X58_586) | ~c6_2(X58_586, a1111) | c2_2(X58_586, a1111) | ~c3_2(X58_586, a1002) | c10_2(X58_586, a1073) | ~c1_2(X58_586, a1002) | c10_2(X58_586, a1002) | ~ndr1_1(X58_586) | ~c4_1(X58_586) | ~c6_1(X58_586) | ~c2_1(X58_586)))). % 40.91/22.20 tff(c_21008, plain, (![X20_30, X218_671]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_671) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_671) | c3_2(X20_30, X218_671) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.20 tff(c_20402, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20406, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19652, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20482, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20483, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20405, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_17439, plain, (![X58_448]: (~c10_2(X58_448, a1149) | ~c10_2(X58_448, a969) | ~c10_1(X58_448) | c6_2(X58_448, a969) | c7_2(X58_448, a969) | ~c3_1(X58_448) | c9_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1149) | c2_2(X58_448, a1149) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.21 tff(c_20479, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20812, plain, (![X20_30]: (~c10_2(X20_30, a990) | ~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | ~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_20703, plain, (![X20_30, X218_651]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_651) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c1_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_651) | c3_2(X20_30, X218_651) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_20727, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_20738, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_18380, plain, (![X58_448]: (~c10_2(X58_448, a990) | ~c1_1(X58_448) | ~c2_2(X58_448, a1112) | c3_2(X58_448, a1112) | ~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.21 tff(c_16579, plain, (![X26_39]: (~c10_2(X26_39, a1149) | ~c10_2(X26_39, a969) | ~c10_1(X26_39) | c6_2(X26_39, a969) | c7_2(X26_39, a969) | ~c5_1(X26_39) | ~c3_1(X26_39) | c9_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1149) | c2_2(X26_39, a1149) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_16577, plain, (![X26_39]: (~c10_2(X26_39, a1149) | ~c10_2(X26_39, a969) | ~c10_1(X26_39) | c6_2(X26_39, a969) | c7_2(X26_39, a969) | ~c5_1(X26_39) | ~c3_1(X26_39) | c9_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1149) | c2_2(X26_39, a1149) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_16578, plain, (![X26_39]: (~c10_2(X26_39, a1149) | ~c10_2(X26_39, a969) | ~c10_1(X26_39) | c6_2(X26_39, a969) | c7_2(X26_39, a969) | ~c5_1(X26_39) | ~c3_1(X26_39) | c9_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1149) | c2_2(X26_39, a1149) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_20480, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c3_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20403, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c10_2(X217_287, a1073) | ~c1_2(X217_287, a1002) | c10_2(X217_287, a1002) | ~c4_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20615, plain, (![X20_30, X218_647]: (~c1_1(X20_30) | ~c2_2(X20_30, X218_647) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c6_2(X20_30, a1176) | c9_1(X20_30) | c4_2(X20_30, X218_647) | c3_2(X20_30, X218_647) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19650, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19653, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19654, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_17633, plain, (![X58_462]: (~c10_2(X58_462, a1111) | ~c10_1(X58_462) | c6_2(X58_462, a1112) | ~c4_2(X58_462, a1112) | ~c5_1(X58_462) | c7_1(X58_462) | ~c6_2(X58_462, a1111) | c2_2(X58_462, a1111) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.21 tff(c_17829, plain, (![X58_474]: (~c10_2(X58_474, a1111) | ~c10_1(X58_474) | c6_2(X58_474, a1112) | ~c4_2(X58_474, a1112) | ~c5_1(X58_474) | c7_1(X58_474) | ~c6_2(X58_474, a1111) | c2_2(X58_474, a1111) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.21 tff(c_19195, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_18188, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c10_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20532, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c10_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_20521, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c3_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_18235, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | ~c5_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20498, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c3_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_20509, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | c10_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19150, plain, (![X217_287]: (~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20486, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_20485, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c4_1(X159_214) | ~c2_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_19966, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_20409, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c4_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_20408, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c4_1(X159_214) | ~c2_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_18159, plain, (![X58_85, X28_494]: (~c1_1(X58_85) | ~c2_2(X58_85, X28_494) | c3_2(X58_85, X28_494) | ~c7_2(X58_85, X28_494) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c3_2(X58_85, a1002) | c3_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.21 tff(c_18158, plain, (![X58_85, X28_494]: (~c1_1(X58_85) | ~c2_2(X58_85, X28_494) | c3_2(X58_85, X28_494) | ~c7_2(X58_85, X28_494) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c3_2(X58_85, a1002) | c10_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.21 tff(c_20324, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1176) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c9_1(X20_30) | c4_2(X20_30, a1176) | c3_2(X20_30, a1176) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19651, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c3_2(X217_287, a1002) | c6_2(X217_287, a1002) | ~c4_2(X217_287, a1002) | ~c5_1(X217_287) | ~c6_1(X217_287) | ~c2_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19563, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | c10_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~c4_1(X58_85) | c2_2(X58_85, a1112) | c10_2(X58_85, a1111) | ~c10_2(X58_85, a990) | ~c1_1(X58_85) | ~c2_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.21 tff(c_19888, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_17545, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c3_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17543, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c3_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17737, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c10_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17735, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c10_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17544, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c3_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17736, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | c10_2(X26_39, a1073) | ~c1_2(X26_39, a1112) | c10_2(X26_39, a1112) | ~c4_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_18189, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c10_2(X217_287, a988) | ~c6_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19196, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_18186, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c10_2(X217_287, a988) | ~c6_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_18190, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c10_2(X217_287, a988) | ~c6_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19193, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_18236, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | ~c5_2(X217_287, a988) | ~c6_1(X217_287) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19197, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_18233, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | ~c5_2(X217_287, a988) | ~c6_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.21 tff(c_19988, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c3_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19379, plain, (![X75_106]: (c3_1(X75_106) | ~c9_1(X75_106) | c7_1(X75_106) | c2_2(X75_106, a1002) | ~c3_2(X75_106, a1002) | c3_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c4_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.21 tff(c_18093, plain, (![X75_106]: (c3_1(X75_106) | ~c9_1(X75_106) | c7_1(X75_106) | c2_2(X75_106, a1002) | ~c3_2(X75_106, a1002) | c10_2(X75_106, a1073) | ~c1_2(X75_106, a1002) | ~c4_1(X75_106) | ~c6_1(X75_106) | ~c2_1(X75_106) | ~c4_2(X75_106, a1002) | c10_2(X75_106, a1002) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.21 tff(c_19977, plain, (![X20_30]: (~c1_1(X20_30) | ~c2_2(X20_30, a1112) | c3_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c10_2(X20_30, a1111) | ~c5_2(X20_30, a990) | c2_2(X20_30, a990) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19791, plain, (![X20_30]: (~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c5_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c10_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.21 tff(c_19656, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c6_2(X159_214, a1002) | ~c4_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c5_1(X159_214) | ~c2_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_19657, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c3_2(X159_214, a1002) | c6_2(X159_214, a1002) | ~c4_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c5_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.21 tff(c_18552, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c6_2(X2_10, a1176) | c4_2(X2_10, a990) | c3_2(X2_10, a990) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.21 tff(c_18342, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | c7_2(X2_10, a1176) | c4_2(X2_10, a990) | c3_2(X2_10, a990) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.21 tff(c_18311, plain, (![X2_10]: (~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | ~c1_2(X2_10, a1176) | c4_2(X2_10, a990) | c3_2(X2_10, a990) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.21 tff(c_17354, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | ~c2_1(X26_39) | c6_2(X26_39, a1112) | ~c4_2(X26_39, a1112) | ~c5_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.21 tff(c_17838, plain, (![X58_474]: (~c10_2(X58_474, a1111) | ~c10_1(X58_474) | c7_2(X58_474, a1112) | c7_1(X58_474) | ~c6_2(X58_474, a1111) | c2_2(X58_474, a1111) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.22 tff(c_17837, plain, (![X58_474]: (~c10_2(X58_474, a1111) | ~c10_1(X58_474) | c5_2(X58_474, a1112) | c7_1(X58_474) | ~c6_2(X58_474, a1111) | c2_2(X58_474, a1111) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.22 tff(c_19728, plain, (![X20_30]: (~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c5_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c3_2(X20_30, a1073) | ~c1_2(X20_30, a1002) | c10_2(X20_30, a1002) | ~c4_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.22 tff(c_17355, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | ~c2_1(X26_39) | c6_2(X26_39, a1112) | ~c4_2(X26_39, a1112) | ~c5_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.22 tff(c_17437, plain, (![X58_448]: (~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c6_2(X58_448, a1112) | ~c4_2(X58_448, a1112) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.22 tff(c_17353, plain, (![X26_39]: (~c10_2(X26_39, a1111) | ~c10_1(X26_39) | ~c2_1(X26_39) | c6_2(X26_39, a1112) | ~c4_2(X26_39, a1112) | ~c5_1(X26_39) | c7_1(X26_39) | ~c6_2(X26_39, a1111) | c2_2(X26_39, a1111) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.22 tff(c_17641, plain, (![X58_462]: (~c10_2(X58_462, a1111) | ~c10_1(X58_462) | c5_2(X58_462, a1112) | c7_1(X58_462) | ~c6_2(X58_462, a1111) | c2_2(X58_462, a1111) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.22 tff(c_17642, plain, (![X58_462]: (~c10_2(X58_462, a1111) | ~c10_1(X58_462) | c7_2(X58_462, a1112) | c7_1(X58_462) | ~c6_2(X58_462, a1111) | c2_2(X58_462, a1111) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.22 tff(c_18160, plain, (![X58_85, X28_494]: (~c1_1(X58_85) | ~c2_2(X58_85, X28_494) | c3_2(X58_85, X28_494) | ~c7_2(X58_85, X28_494) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c3_2(X58_85, a1002) | c6_2(X58_85, a1002) | ~c4_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c5_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_19587, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c2_2(X159_214, a1112) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19572, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c2_2(X159_214, a1112) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19553, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c3_2(X159_214, a1002) | c10_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c2_2(X159_214, a1112) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19520, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c3_2(X159_214, a1002) | c3_2(X159_214, a1073) | ~c1_2(X159_214, a1002) | c10_2(X159_214, a1002) | ~c4_1(X159_214) | ~c2_1(X159_214) | c2_2(X159_214, a1112) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19194, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c1_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18187, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | c10_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18234, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | ~c5_2(X217_287, a988) | ~c6_1(X217_287) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18881, plain, (![X217_530]: (c10_2(X217_530, a988) | ~c6_1(X217_530) | c10_2(X217_530, a989) | c8_1(X217_530) | c5_1(X217_530) | ~c2_2(X217_530, a989) | ~c10_2(X217_530, a990) | ~c1_1(X217_530) | ~c2_2(X217_530, a1176) | c3_2(X217_530, a1176) | c9_1(X217_530) | c3_2(X217_530, a989) | ~ndr1_1(X217_530)))). % 40.91/22.22 tff(c_19151, plain, (![X217_287]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18925, plain, (![X217_532]: (c1_2(X217_532, a988) | ~c6_1(X217_532) | c10_2(X217_532, a989) | c8_1(X217_532) | c5_1(X217_532) | ~c2_2(X217_532, a1176) | c3_2(X217_532, a1176) | ~c10_2(X217_532, a990) | ~c1_1(X217_532) | ~c2_2(X217_532, a989) | c9_1(X217_532) | c3_2(X217_532, a989) | ~ndr1_1(X217_532)))). % 40.91/22.22 tff(c_18135, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | ~c6_2(X58_85, a1002) | c2_2(X58_85, a1002) | ~c3_2(X58_85, a1002) | c3_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18192, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c10_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18239, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | ~c5_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18193, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c10_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18240, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | ~c5_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19199, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c1_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19152, plain, (![X217_287]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, a969) | c3_2(X217_287, a969) | ~c10_2(X217_287, a969) | ~c10_1(X217_287) | c6_2(X217_287, a969) | ~c5_1(X217_287) | ~c3_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1149) | c3_2(X217_287, a1149) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_19200, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_1(X159_214) | ~c6_2(X159_214, a990) | c2_2(X159_214, a990) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c1_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_19201, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | c1_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18162, plain, (![X26_39, X28_494]: (~c1_1(X26_39) | ~c2_2(X26_39, X28_494) | c3_2(X26_39, X28_494) | ~c7_2(X26_39, X28_494) | c7_1(X26_39) | ~c6_2(X26_39, a990) | c2_2(X26_39, a990) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.22 tff(c_18386, plain, (![X2_10]: (~c10_2(X2_10, a990) | ~c1_1(X2_10) | ~c2_2(X2_10, a969) | c3_2(X2_10, a969) | ~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.22 tff(c_18237, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_1(X217_287) | ~c6_2(X217_287, a990) | c2_2(X217_287, a990) | ~c7_2(X217_287, a989) | ~c3_2(X217_287, a989) | ~c5_2(X217_287, a988) | ~c6_1(X217_287) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18485, plain, (![X217_515]: (c1_2(X217_515, a988) | ~c6_1(X217_515) | c10_2(X217_515, a989) | c8_1(X217_515) | c5_1(X217_515) | ~c10_2(X217_515, a990) | ~c1_1(X217_515) | ~c2_2(X217_515, a989) | ~c1_2(X217_515, a1176) | c9_1(X217_515) | c3_2(X217_515, a989) | ~ndr1_1(X217_515)))). % 40.91/22.22 tff(c_18484, plain, (![X217_515]: (c10_2(X217_515, a988) | ~c6_1(X217_515) | c10_2(X217_515, a989) | c8_1(X217_515) | c5_1(X217_515) | ~c10_2(X217_515, a990) | ~c1_1(X217_515) | ~c2_2(X217_515, a989) | ~c1_2(X217_515, a1176) | c9_1(X217_515) | c3_2(X217_515, a989) | ~ndr1_1(X217_515)))). % 40.91/22.22 tff(c_18344, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18313, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18554, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c6_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18312, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~c1_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18553, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c6_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18343, plain, (![X159_214]: (~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | c7_2(X159_214, a1176) | c9_1(X159_214) | c4_2(X159_214, a990) | c3_2(X159_214, a990) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18555, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | c6_2(X58_85, a1176) | c9_1(X58_85) | c4_2(X58_85, a990) | c3_2(X58_85, a990) | ~ndr1_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18314, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | ~c1_2(X58_85, a1176) | c9_1(X58_85) | c4_2(X58_85, a990) | c3_2(X58_85, a990) | ~ndr1_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18345, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | c7_2(X58_85, a1176) | c9_1(X58_85) | c4_2(X58_85, a990) | c3_2(X58_85, a990) | ~ndr1_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18939, plain, (~c2_2(a1087, a1176))). % 40.91/22.22 tff(c_18449, plain, (![X217_513, X218_514]: (~c2_2(X217_513, a1176) | c3_2(X217_513, a1176) | ~c10_2(X217_513, a990) | ~c1_1(X217_513) | ~c2_2(X217_513, X218_514) | c9_1(X217_513) | c4_2(X217_513, X218_514) | c3_2(X217_513, X218_514) | ~ndr1_1(X217_513)))). % 40.91/22.22 tff(c_18896, plain, (~c2_2(a1026, a1176))). % 40.91/22.22 tff(c_18787, plain, (![X217_287]: (~c1_1(X217_287) | ~c2_2(X217_287, a990) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c3_2(X217_287, a990) | ~ndr1_1(X217_287) | c4_2(X217_287, a990)))). % 40.91/22.22 tff(c_18340, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18306, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18551, plain, (![X217_287, X218_289]: (~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18383, plain, (![X217_287, X218_289]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c3_2(X217_287, a1176) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18273, plain, (![X217_287, X28_502]: (~c1_1(X217_287) | ~c2_2(X217_287, X28_502) | c3_2(X217_287, X28_502) | ~c7_2(X217_287, X28_502) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18385, plain, (![X217_287, X218_289]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c6_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18501, plain, (~c1_2(a1087, a1176))). % 40.91/22.22 tff(c_18499, plain, (~c1_2(a1026, a1176))). % 40.91/22.22 tff(c_18381, plain, (![X217_287, X218_289]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18384, plain, (![X217_287, X218_289]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, X218_289) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18382, plain, (![X217_287]: (~c10_2(X217_287, a990) | ~c1_1(X217_287) | ~c2_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18388, plain, (![X159_214]: (~c10_2(X159_214, a990) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~ndr1_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18387, plain, (![X159_214]: (~c10_2(X159_214, a990) | ~c1_1(X159_214) | ~c2_2(X159_214, a1112) | c3_2(X159_214, a1112) | ~ndr1_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_18389, plain, (![X58_85]: (~c10_2(X58_85, a990) | ~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18348, plain, (![X27_40, X28_42]: (~c10_2(X27_40, a990) | ~c1_1(X27_40) | ~c2_2(X27_40, X28_42) | c3_2(X27_40, X28_42) | ~c7_2(X27_40, X28_42) | ~ndr1_1(X27_40)))). % 40.91/22.22 tff(c_18272, plain, (![X217_287, X28_502]: (~c1_1(X217_287) | ~c2_2(X217_287, X28_502) | c3_2(X217_287, X28_502) | ~c7_2(X217_287, X28_502) | c7_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18271, plain, (![X217_287, X28_502]: (~c1_1(X217_287) | ~c2_2(X217_287, X28_502) | c3_2(X217_287, X28_502) | ~c7_2(X217_287, X28_502) | ~c1_2(X217_287, a1176) | c9_1(X217_287) | c4_2(X217_287, a990) | c3_2(X217_287, a990) | ~ndr1_1(X217_287)))). % 40.91/22.22 tff(c_18260, plain, (![X27_40, X28_42]: (~c7_2(X27_40, a990) | ~c1_1(X27_40) | ~c2_2(X27_40, X28_42) | c3_2(X27_40, X28_42) | ~c7_2(X27_40, X28_42) | ~ndr1_1(X27_40)))). % 40.91/22.22 tff(c_18241, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | ~c5_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18163, plain, (![X26_39, X28_494]: (~c1_1(X26_39) | ~c2_2(X26_39, X28_494) | c3_2(X26_39, X28_494) | ~c7_2(X26_39, X28_494) | c7_1(X26_39) | ~c6_2(X26_39, a990) | c2_2(X26_39, a990) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.22 tff(c_18194, plain, (![X58_85]: (~c1_1(X58_85) | ~c2_2(X58_85, a1002) | c3_2(X58_85, a1002) | c7_1(X58_85) | ~c6_2(X58_85, a990) | c2_2(X58_85, a990) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | c10_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_18161, plain, (![X26_39, X28_494]: (~c1_1(X26_39) | ~c2_2(X26_39, X28_494) | c3_2(X26_39, X28_494) | ~c7_2(X26_39, X28_494) | c7_1(X26_39) | ~c6_2(X26_39, a990) | c2_2(X26_39, a990) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.22 tff(c_18138, plain, (![X27_40, X28_42]: (~c8_2(X27_40, a990) | ~c1_1(X27_40) | ~c2_2(X27_40, X28_42) | c3_2(X27_40, X28_42) | ~c7_2(X27_40, X28_42) | ~ndr1_1(X27_40)))). % 40.91/22.22 tff(c_17640, plain, (![X58_462, X205_463]: (c3_1(X58_462) | ~c9_1(X58_462) | ~c7_2(X58_462, X205_463) | c7_1(X58_462) | ~c6_2(X58_462, X205_463) | c2_2(X58_462, X205_463) | ~c3_2(X58_462, a1002) | c3_2(X58_462, a1073) | ~c1_2(X58_462, a1002) | c10_2(X58_462, a1002) | ~ndr1_1(X58_462) | ~c4_1(X58_462) | ~c6_1(X58_462) | ~c2_1(X58_462)))). % 40.91/22.22 tff(c_18063, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | ~c6_2(X58_85, a1002) | c2_2(X58_85, a1002) | ~c3_2(X58_85, a1002) | c10_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.22 tff(c_17836, plain, (![X58_474, X205_475]: (c3_1(X58_474) | ~c9_1(X58_474) | ~c7_2(X58_474, X205_475) | c7_1(X58_474) | ~c6_2(X58_474, X205_475) | c2_2(X58_474, X205_475) | ~c3_2(X58_474, a1002) | c10_2(X58_474, a1073) | ~c1_2(X58_474, a1002) | c10_2(X58_474, a1002) | ~ndr1_1(X58_474) | ~c4_1(X58_474) | ~c6_1(X58_474) | ~c2_1(X58_474)))). % 40.91/22.22 tff(c_18022, plain, (~c2_1(a1080))). % 40.91/22.22 tff(c_18020, plain, (c1_1(a1080))). % 40.91/22.22 tff(c_18021, plain, (~c8_1(a1080))). % 40.91/22.22 tff(c_18011, plain, (~c7_1(a1080))). % 40.91/22.22 tff(c_18009, plain, (c9_1(a1080))). % 40.91/22.22 tff(c_18010, plain, (~c6_1(a1080))). % 40.91/22.22 tff(c_17983, plain, (~ndr1_1(a1080))). % 40.91/22.22 tff(c_17981, plain, (![X20_30]: (~c10_2(X20_30, a1111) | ~c10_1(X20_30) | c5_2(X20_30, a1112) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c5_2(X20_30, a1111) | c2_2(X20_30, a1111) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.22 tff(c_17445, plain, (![X58_448]: (~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c5_2(X58_448, a1112) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.22 tff(c_17446, plain, (![X58_448]: (~c10_2(X58_448, a1111) | ~c10_1(X58_448) | c7_2(X58_448, a1112) | c7_1(X58_448) | ~c6_2(X58_448, a1111) | c2_2(X58_448, a1111) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.22 tff(c_17941, plain, (![X20_30]: (c3_1(X20_30) | ~c9_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | c10_2(X20_30, a1111) | ~c5_2(X20_30, a1112) | c2_2(X20_30, a1112) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.22 tff(c_17905, plain, (![X20_30]: (c3_1(X20_30) | ~c9_1(X20_30) | c7_1(X20_30) | ~c3_2(X20_30, a1002) | c6_2(X20_30, a1002) | ~c4_2(X20_30, a1002) | ~c5_1(X20_30) | ~c2_1(X20_30) | ~c3_2(X20_30, a1111) | ~c5_2(X20_30, a1112) | c2_2(X20_30, a1112) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.22 tff(c_17939, plain, (![X64_436]: (c3_1(X64_436) | ~c9_1(X64_436) | c7_1(X64_436) | c2_2(X64_436, a1112) | ~c3_2(X64_436, a1002) | c6_2(X64_436, a1002) | ~c4_2(X64_436, a1002) | c10_2(X64_436, a1111) | ~c6_1(X64_436) | ~c2_1(X64_436) | ~c4_2(X64_436, a1112) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.22 tff(c_17902, plain, (![X64_436]: (c3_1(X64_436) | ~c9_1(X64_436) | c7_1(X64_436) | c2_2(X64_436, a1112) | ~c3_2(X64_436, a1002) | c6_2(X64_436, a1002) | ~c4_2(X64_436, a1002) | ~c3_2(X64_436, a1111) | ~c6_1(X64_436) | ~c2_1(X64_436) | ~c4_2(X64_436, a1112) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.22 tff(c_17885, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c3_2(X159_214, a1002) | c6_2(X159_214, a1002) | ~c4_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c5_1(X159_214) | ~c2_1(X159_214) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_17908, plain, (![X50_74]: (~c7_1(X50_74) | ~c2_1(X50_74) | c4_1(X50_74)))). % 40.91/22.22 tff(c_17884, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c3_2(X159_214, a1002) | c6_2(X159_214, a1002) | ~c4_2(X159_214, a1002) | ~ndr1_1(X159_214) | ~c5_1(X159_214) | ~c2_1(X159_214) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.22 tff(c_17444, plain, (![X58_448, X205_449]: (c3_1(X58_448) | ~c9_1(X58_448) | ~c7_2(X58_448, X205_449) | c7_1(X58_448) | ~c6_2(X58_448, X205_449) | c2_2(X58_448, X205_449) | ~c3_2(X58_448, a1002) | c6_2(X58_448, a1002) | ~c4_2(X58_448, a1002) | ~ndr1_1(X58_448) | ~c5_1(X58_448) | ~c6_1(X58_448) | ~c2_1(X58_448)))). % 40.91/22.22 tff(c_17765, plain, (![X58_85, X205_472]: (c7_1(X58_85) | ~c6_2(X58_85, X205_472) | c8_2(X58_85, X205_472) | c2_2(X58_85, X205_472) | ~c3_2(X58_85, a1002) | c10_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_17684, plain, (![X109_464, X205_271, X110_465]: (c7_1(X109_464) | ~c6_2(X109_464, X205_271) | c8_2(X109_464, X205_271) | c2_2(X109_464, X205_271) | ~c7_2(X109_464, X110_465) | ~c3_2(X109_464, X110_465) | c10_2(X109_464, a1073) | ~c1_2(X109_464, X110_465) | c10_2(X109_464, X110_465) | ~ndr1_1(X109_464) | ~c4_1(X109_464)))). % 40.91/22.23 tff(c_17704, plain, (![X109_467]: (~c8_2(X109_467, a1111) | ~c10_2(X109_467, a1111) | ~c10_1(X109_467) | ~c6_1(X109_467) | c10_2(X109_467, a1073) | ~c1_2(X109_467, a1112) | c10_2(X109_467, a1112) | ~ndr1_1(X109_467) | ~c4_1(X109_467)))). % 40.91/22.23 tff(c_17710, plain, (![X146_197]: (~c6_1(X146_197) | c10_2(X146_197, a1073) | ~c1_2(X146_197, a1112) | c10_2(X146_197, a1112) | ~c4_1(X146_197) | c2_2(X146_197, a1111) | ~ndr1_1(X146_197) | ~c2_1(X146_197) | ~c10_1(X146_197)))). % 40.91/22.23 tff(c_17693, plain, (![X109_464]: (~c3_2(X109_464, a1111) | ~c6_1(X109_464) | c10_2(X109_464, a1073) | ~c1_2(X109_464, a1112) | c10_2(X109_464, a1112) | ~ndr1_1(X109_464) | ~c4_1(X109_464)))). % 40.91/22.23 tff(c_17694, plain, (![X109_464]: (c9_2(X109_464, a1111) | ~c6_1(X109_464) | c10_2(X109_464, a1073) | ~c1_2(X109_464, a1112) | c10_2(X109_464, a1112) | ~ndr1_1(X109_464) | ~c4_1(X109_464)))). % 40.91/22.23 tff(c_17692, plain, (![X109_464]: (c10_2(X109_464, a1111) | ~c6_1(X109_464) | c10_2(X109_464, a1073) | ~c1_2(X109_464, a1112) | c10_2(X109_464, a1112) | ~ndr1_1(X109_464) | ~c4_1(X109_464)))). % 40.91/22.23 tff(c_17653, plain, (![X109_149, X110_151]: (c10_2(X109_149, a1073) | ~c1_2(X109_149, X110_151) | c10_2(X109_149, X110_151) | c9_2(X109_149, X110_151) | ~ndr1_1(X109_149) | ~c4_1(X109_149)))). % 40.91/22.23 tff(c_17574, plain, (![X58_85, X205_460]: (c7_1(X58_85) | ~c6_2(X58_85, X205_460) | c8_2(X58_85, X205_460) | c2_2(X58_85, X205_460) | ~c3_2(X58_85, a1002) | c3_2(X58_85, a1073) | ~c1_2(X58_85, a1002) | c10_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c4_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_17488, plain, (![X109_450, X205_271, X110_451]: (c7_1(X109_450) | ~c6_2(X109_450, X205_271) | c8_2(X109_450, X205_271) | c2_2(X109_450, X205_271) | ~c7_2(X109_450, X110_451) | ~c3_2(X109_450, X110_451) | c3_2(X109_450, a1073) | ~c1_2(X109_450, X110_451) | c10_2(X109_450, X110_451) | ~ndr1_1(X109_450) | ~c4_1(X109_450)))). % 40.91/22.23 tff(c_17523, plain, (![X146_455]: (~c1_2(X146_455, a1073) | c1_1(X146_455) | c5_1(X146_455) | ~c6_1(X146_455) | ~c1_2(X146_455, a1112) | c10_2(X146_455, a1112) | ~c4_1(X146_455) | c2_2(X146_455, a1111) | ~ndr1_1(X146_455) | ~c2_1(X146_455) | ~c10_1(X146_455)))). % 40.91/22.23 tff(c_17513, plain, (![X109_453]: (~c8_2(X109_453, a1111) | ~c10_2(X109_453, a1111) | ~c10_1(X109_453) | ~c6_1(X109_453) | c3_2(X109_453, a1073) | ~c1_2(X109_453, a1112) | c10_2(X109_453, a1112) | ~ndr1_1(X109_453) | ~c4_1(X109_453)))). % 40.91/22.23 tff(c_17518, plain, (![X109_454]: (~c1_2(X109_454, a1073) | c1_1(X109_454) | c5_1(X109_454) | c10_2(X109_454, a1111) | ~c6_1(X109_454) | ~c1_2(X109_454, a1112) | c10_2(X109_454, a1112) | ~ndr1_1(X109_454) | ~c4_1(X109_454)))). % 40.91/22.23 tff(c_17505, plain, (![X146_197]: (~c6_1(X146_197) | c3_2(X146_197, a1073) | ~c1_2(X146_197, a1112) | c10_2(X146_197, a1112) | ~c4_1(X146_197) | c2_2(X146_197, a1111) | ~ndr1_1(X146_197) | ~c2_1(X146_197) | ~c10_1(X146_197)))). % 40.91/22.23 tff(c_17496, plain, (![X109_450]: (c10_2(X109_450, a1111) | ~c6_1(X109_450) | c3_2(X109_450, a1073) | ~c1_2(X109_450, a1112) | c10_2(X109_450, a1112) | ~ndr1_1(X109_450) | ~c4_1(X109_450)))). % 40.91/22.23 tff(c_17498, plain, (![X109_450]: (c9_2(X109_450, a1111) | ~c6_1(X109_450) | c3_2(X109_450, a1073) | ~c1_2(X109_450, a1112) | c10_2(X109_450, a1112) | ~ndr1_1(X109_450) | ~c4_1(X109_450)))). % 40.91/22.23 tff(c_17497, plain, (![X109_450]: (~c3_2(X109_450, a1111) | ~c6_1(X109_450) | c3_2(X109_450, a1073) | ~c1_2(X109_450, a1112) | c10_2(X109_450, a1112) | ~ndr1_1(X109_450) | ~c4_1(X109_450)))). % 40.91/22.23 tff(c_17457, plain, (![X109_149, X110_151]: (c3_2(X109_149, a1073) | ~c1_2(X109_149, X110_151) | c10_2(X109_149, X110_151) | c9_2(X109_149, X110_151) | ~ndr1_1(X109_149) | ~c4_1(X109_149)))). % 40.91/22.23 tff(c_17383, plain, (![X58_85, X205_446]: (c7_1(X58_85) | ~c6_2(X58_85, X205_446) | c8_2(X58_85, X205_446) | c2_2(X58_85, X205_446) | ~c3_2(X58_85, a1002) | c6_2(X58_85, a1002) | ~c4_2(X58_85, a1002) | ~ndr1_1(X58_85) | ~c5_1(X58_85) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_17273, plain, (![X64_436, X205_271, X65_437]: (c7_1(X64_436) | ~c6_2(X64_436, X205_271) | c8_2(X64_436, X205_271) | c2_2(X64_436, X205_271) | ~c7_2(X64_436, X65_437) | ~c3_2(X64_436, X65_437) | ~c2_1(X64_436) | c6_2(X64_436, X65_437) | ~c4_2(X64_436, X65_437) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.23 tff(c_17293, plain, (![X64_440]: (~c8_2(X64_440, a1111) | ~c10_2(X64_440, a1111) | ~c10_1(X64_440) | ~c6_1(X64_440) | ~c2_1(X64_440) | c6_2(X64_440, a1112) | ~c4_2(X64_440, a1112) | ~ndr1_1(X64_440) | ~c5_1(X64_440)))). % 40.91/22.23 tff(c_17331, plain, (![X2_10]: (~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c2_1(X2_10) | c6_2(X2_10, a969) | ~c4_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.23 tff(c_17283, plain, (![X64_436, X65_437]: (~c8_2(X64_436, X65_437) | ~c10_2(X64_436, X65_437) | ~c10_1(X64_436) | ~c2_1(X64_436) | c6_2(X64_436, X65_437) | ~c4_2(X64_436, X65_437) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.23 tff(c_17282, plain, (![X64_436]: (c9_2(X64_436, a1111) | ~c6_1(X64_436) | ~c2_1(X64_436) | c6_2(X64_436, a1112) | ~c4_2(X64_436, a1112) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.23 tff(c_17281, plain, (![X64_436]: (~c3_2(X64_436, a1111) | ~c6_1(X64_436) | ~c2_1(X64_436) | c6_2(X64_436, a1112) | ~c4_2(X64_436, a1112) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.23 tff(c_17280, plain, (![X64_436]: (c10_2(X64_436, a1111) | ~c6_1(X64_436) | ~c2_1(X64_436) | c6_2(X64_436, a1112) | ~c4_2(X64_436, a1112) | ~ndr1_1(X64_436) | ~c5_1(X64_436)))). % 40.91/22.23 tff(c_17242, plain, (![X64_93, X65_95]: (~c2_1(X64_93) | c6_2(X64_93, X65_95) | c9_2(X64_93, X65_95) | ~c4_2(X64_93, X65_95) | ~ndr1_1(X64_93) | ~c5_1(X64_93)))). % 40.91/22.23 tff(c_17208, plain, (c5_2(a1183, a1185))). % 40.91/22.23 tff(c_17205, plain, (~c1_2(a1183, a1184))). % 40.91/22.23 tff(c_17197, plain, (c3_2(a1183, a1184))). % 40.91/22.23 tff(c_17178, plain, (~c7_2(a1183, a1184))). % 40.91/22.23 tff(c_17155, plain, (c8_2(a1183, a1184))). % 40.91/22.23 tff(c_17153, plain, (~c1_2(a1183, a1185))). % 40.91/22.23 tff(c_17145, plain, (c3_2(a1183, a1185))). % 40.91/22.23 tff(c_17144, plain, (~c1_2(a1183, a1176))). % 40.91/22.23 tff(c_17125, plain, (~c7_2(a1183, a1185))). % 40.91/22.23 tff(c_17124, plain, (~c5_1(a1183))). % 40.91/22.23 tff(c_17123, plain, (c10_2(a1183, a1185))). % 40.91/22.23 tff(c_17104, plain, (~c9_2(a1183, a1184))). % 40.91/22.23 tff(c_16326, plain, (![X26_401]: (~c10_2(X26_401, a1111) | ~c10_1(X26_401) | c7_2(X26_401, a1112) | c7_1(X26_401) | ~c6_2(X26_401, a1111) | c2_2(X26_401, a1111) | ~c7_2(X26_401, a989) | ~c3_2(X26_401, a989) | ~ndr1_1(X26_401) | ~c5_2(X26_401, a988) | ~c6_1(X26_401)))). % 40.91/22.23 tff(c_16325, plain, (![X26_401]: (~c10_2(X26_401, a1111) | ~c10_1(X26_401) | c5_2(X26_401, a1112) | c7_1(X26_401) | ~c6_2(X26_401, a1111) | c2_2(X26_401, a1111) | ~c7_2(X26_401, a989) | ~c3_2(X26_401, a989) | ~ndr1_1(X26_401) | ~c5_2(X26_401, a988) | ~c6_1(X26_401)))). % 40.91/22.23 tff(c_16444, plain, (![X26_405]: (~c10_2(X26_405, a1111) | ~c10_1(X26_405) | c7_2(X26_405, a1112) | c7_1(X26_405) | ~c6_2(X26_405, a1111) | c2_2(X26_405, a1111) | ~c7_2(X26_405, a989) | ~c3_2(X26_405, a989) | ~ndr1_1(X26_405) | c10_2(X26_405, a988) | ~c6_1(X26_405)))). % 40.91/22.23 tff(c_16443, plain, (![X26_405]: (~c10_2(X26_405, a1111) | ~c10_1(X26_405) | c5_2(X26_405, a1112) | c7_1(X26_405) | ~c6_2(X26_405, a1111) | c2_2(X26_405, a1111) | ~c7_2(X26_405, a989) | ~c3_2(X26_405, a989) | ~ndr1_1(X26_405) | c10_2(X26_405, a988) | ~c6_1(X26_405)))). % 40.91/22.23 tff(c_16381, plain, (![X26_403]: (~c10_2(X26_403, a1111) | ~c10_1(X26_403) | c5_2(X26_403, a1112) | c7_1(X26_403) | ~c6_2(X26_403, a1111) | c2_2(X26_403, a1111) | ~c7_2(X26_403, a989) | ~c3_2(X26_403, a989) | ~ndr1_1(X26_403) | c1_2(X26_403, a988) | ~c6_1(X26_403)))). % 40.91/22.23 tff(c_16382, plain, (![X26_403]: (~c10_2(X26_403, a1111) | ~c10_1(X26_403) | c7_2(X26_403, a1112) | c7_1(X26_403) | ~c6_2(X26_403, a1111) | c2_2(X26_403, a1111) | ~c7_2(X26_403, a989) | ~c3_2(X26_403, a989) | ~ndr1_1(X26_403) | c1_2(X26_403, a988) | ~c6_1(X26_403)))). % 40.91/22.23 tff(c_16718, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c10_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16762, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c1_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16717, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c10_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16806, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | ~c5_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16929, plain, (~c7_1(a1050))). % 40.91/22.23 tff(c_16930, plain, (ndr1_1(a1183))). % 40.91/22.23 tff(c_16923, plain, (~c3_1(a1050))). % 40.91/22.23 tff(c_16919, plain, (c8_1(a1050))). % 40.91/22.23 tff(c_16916, plain, (~c2_1(a1050))). % 40.91/22.23 tff(c_16918, plain, (~c6_1(a1050))). % 40.91/22.23 tff(c_16892, plain, (~ndr1_1(a1050))). % 40.91/22.23 tff(c_16807, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | ~c5_2(X159_214, a988) | c10_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16761, plain, (![X159_214]: (c3_1(X159_214) | ~c9_1(X159_214) | c7_1(X159_214) | ~c6_2(X159_214, a1112) | c2_2(X159_214, a1112) | ~c7_2(X159_214, a989) | ~c3_2(X159_214, a989) | ~ndr1_1(X159_214) | c1_2(X159_214, a988) | ~c3_2(X159_214, a1111) | ~c6_1(X159_214)))). % 40.91/22.23 tff(c_16808, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | ~c6_2(X58_85, a1002) | c2_2(X58_85, a1002) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | ~c5_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_16839, plain, (~c3_1(a1130))). % 40.91/22.23 tff(c_16838, plain, (~c2_1(a1130))). % 40.91/22.23 tff(c_16837, plain, (~c7_1(a1130))). % 40.91/22.23 tff(c_16836, plain, (~c6_1(a1130))). % 40.91/22.23 tff(c_16831, plain, (c1_1(a1130))). % 40.91/22.23 tff(c_16810, plain, (~ndr1_1(a1130))). % 40.91/22.23 tff(c_16324, plain, (![X26_401, X205_402]: (c3_1(X26_401) | ~c9_1(X26_401) | ~c7_2(X26_401, X205_402) | c7_1(X26_401) | ~c6_2(X26_401, X205_402) | c2_2(X26_401, X205_402) | ~c7_2(X26_401, a989) | ~c3_2(X26_401, a989) | ~ndr1_1(X26_401) | ~c5_2(X26_401, a988) | ~c6_1(X26_401)))). % 40.91/22.23 tff(c_16763, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | ~c6_2(X58_85, a1002) | c2_2(X58_85, a1002) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | c1_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_16764, plain, (~c10_1(a1183))). % 40.91/22.23 tff(c_16380, plain, (![X26_403, X205_404]: (c3_1(X26_403) | ~c9_1(X26_403) | ~c7_2(X26_403, X205_404) | c7_1(X26_403) | ~c6_2(X26_403, X205_404) | c2_2(X26_403, X205_404) | ~c7_2(X26_403, a989) | ~c3_2(X26_403, a989) | ~ndr1_1(X26_403) | c1_2(X26_403, a988) | ~c6_1(X26_403)))). % 40.91/22.23 tff(c_16719, plain, (![X58_85]: (c3_1(X58_85) | ~c9_1(X58_85) | c7_1(X58_85) | ~c6_2(X58_85, a1002) | c2_2(X58_85, a1002) | ~c7_2(X58_85, a989) | ~c3_2(X58_85, a989) | ~ndr1_1(X58_85) | c10_2(X58_85, a988) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.23 tff(c_16442, plain, (![X26_405, X205_406]: (c3_1(X26_405) | ~c9_1(X26_405) | ~c7_2(X26_405, X205_406) | c7_1(X26_405) | ~c6_2(X26_405, X205_406) | c2_2(X26_405, X205_406) | ~c7_2(X26_405, a989) | ~c3_2(X26_405, a989) | ~ndr1_1(X26_405) | c10_2(X26_405, a988) | ~c6_1(X26_405)))). % 40.91/22.23 tff(c_16684, plain, (![X75_410]: (~c5_2(X75_410, a988) | ~c6_1(X75_410) | ~c4_2(X75_410, a989) | c10_2(X75_410, a989) | ~ndr1_1(X75_410) | c8_1(X75_410) | c5_1(X75_410)))). % 40.91/22.23 tff(c_16683, plain, (![X75_410]: (c10_2(X75_410, a988) | ~c6_1(X75_410) | ~c4_2(X75_410, a989) | c10_2(X75_410, a989) | ~ndr1_1(X75_410) | c8_1(X75_410) | c5_1(X75_410)))). % 40.91/22.23 tff(c_16682, plain, (![X75_410]: (c1_2(X75_410, a988) | ~c6_1(X75_410) | ~c4_2(X75_410, a989) | c10_2(X75_410, a989) | ~ndr1_1(X75_410) | c8_1(X75_410) | c5_1(X75_410)))). % 40.91/22.23 tff(c_16688, plain, (~c4_2(a1133, a1134))). % 40.91/22.23 tff(c_16659, plain, (![X75_106, X76_108]: (c6_2(X75_106, X76_108) | ~c4_2(X75_106, X76_108) | c10_2(X75_106, X76_108) | ~ndr1_1(X75_106) | c8_1(X75_106) | c5_1(X75_106)))). % 40.91/22.23 tff(c_16651, plain, (~c3_1(a1098))). % 40.91/22.23 tff(c_16650, plain, (~c7_1(a1098))). % 40.91/22.23 tff(c_16648, plain, (~c2_1(a1098))). % 40.91/22.23 tff(c_16647, plain, (~c2_1(a971))). % 40.91/22.23 tff(c_16646, plain, (c3_1(a1080))). % 40.91/22.23 tff(c_16641, plain, (c8_1(a971))). % 40.91/22.23 tff(c_16640, plain, (~c6_1(a1098))). % 40.91/22.23 tff(c_16635, plain, (c1_1(a1098))). % 40.91/22.23 tff(c_16614, plain, (~ndr1_1(a1098))). % 40.91/22.23 tff(c_16608, plain, (~c3_1(a971))). % 40.91/22.23 tff(c_16609, plain, (~c6_1(a971))). % 40.91/22.23 tff(c_16603, plain, (~c7_1(a971))). % 40.91/22.23 tff(c_16581, plain, (~ndr1_1(a971))). % 40.91/22.23 tff(c_16580, plain, (~c9_1(a1079))). % 40.91/22.23 tff(c_16036, plain, (![X2_385]: (~c8_2(X2_385, a1149) | ~c10_2(X2_385, a1149) | ~c10_2(X2_385, a969) | ~c10_1(X2_385) | c6_2(X2_385, a969) | c7_2(X2_385, a969) | ~ndr1_1(X2_385) | ~c5_1(X2_385) | ~c3_1(X2_385) | c9_1(X2_385)))). % 40.91/22.23 tff(c_16560, plain, (~c7_1(a1046))). % 40.91/22.23 tff(c_16559, plain, (~c2_1(a1046))). % 40.91/22.23 tff(c_16553, plain, (c8_1(a1046))). % 40.91/22.23 tff(c_16502, plain, (~c7_2(a997, a998))). % 40.91/22.23 tff(c_16529, plain, (~c3_1(a1046))). % 40.91/22.23 tff(c_16530, plain, (~c6_1(a1046))). % 40.91/22.23 tff(c_16504, plain, (~ndr1_1(a1046))). % 40.91/22.23 tff(c_16501, plain, (~c5_2(a997, a998))). % 40.91/22.23 tff(c_16500, plain, (~c10_1(a997))). % 40.91/22.23 tff(c_16488, plain, (c9_2(a997, a998))). % 40.91/22.23 tff(c_15881, plain, (![X188_378, X189_379]: (~c8_2(X188_378, X189_379) | ~c10_2(X188_378, X189_379) | ~c8_2(X188_378, a1149) | ~c10_2(X188_378, a1149) | ~c10_1(X188_378) | c6_2(X188_378, X189_379) | c7_2(X188_378, X189_379) | ~ndr1_1(X188_378) | ~c5_1(X188_378)))). % 40.91/22.23 tff(c_15975, plain, (![X26_39, X205_382]: (c7_1(X26_39) | ~c6_2(X26_39, X205_382) | c8_2(X26_39, X205_382) | c2_2(X26_39, X205_382) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c10_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.23 tff(c_16392, plain, (c3_2(a997, a998))). % 40.91/22.23 tff(c_15976, plain, (![X26_39, X205_382]: (c7_1(X26_39) | ~c6_2(X26_39, X205_382) | c8_2(X26_39, X205_382) | c2_2(X26_39, X205_382) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | c1_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.23 tff(c_16336, plain, (~c6_1(a967))). % 40.91/22.23 tff(c_15971, plain, (![X26_39, X205_382]: (c7_1(X26_39) | ~c6_2(X26_39, X205_382) | c8_2(X26_39, X205_382) | c2_2(X26_39, X205_382) | ~c7_2(X26_39, a989) | ~c3_2(X26_39, a989) | ~ndr1_1(X26_39) | ~c5_2(X26_39, a988) | ~c6_1(X26_39)))). % 40.91/22.23 tff(c_16184, plain, (![X146_197, X147_199]: (~c1_2(X146_197, X147_199) | c1_1(X146_197) | c5_1(X146_197) | c2_2(X146_197, X147_199) | ~ndr1_1(X146_197) | ~c2_1(X146_197) | ~c10_1(X146_197)))). % 40.91/22.23 tff(c_16176, plain, (![X148_200]: (~c1_2(X148_200, a1101) | ~ndr1_1(X148_200) | c5_1(X148_200) | c1_1(X148_200) | c8_1(X148_200)))). % 40.91/22.23 tff(c_16197, plain, (~c1_2(a1092, a1093))). % 40.91/22.23 tff(c_16194, plain, (![X217_287, X218_289]: (~c1_2(X217_287, a1176) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.23 tff(c_16196, plain, (~c1_2(a1015, a1016))). % 40.91/22.23 tff(c_16195, plain, (~c1_2(a1035, a1036))). % 40.91/22.23 tff(c_16193, plain, (~c1_2(a1035, a1037))). % 40.91/22.23 tff(c_16191, plain, (c5_1(a1068))). % 40.91/22.23 tff(c_16137, plain, (![X97_133, X98_135]: (~c3_2(X97_133, X98_135) | ~c1_2(X97_133, X98_135) | ~ndr1_1(X97_133) | c1_1(X97_133) | c5_1(X97_133)))). % 40.91/22.24 tff(c_16119, plain, (![X217_287]: (c9_1(X217_287) | c4_2(X217_287, a1176) | c3_2(X217_287, a1176) | ~ndr1_1(X217_287) | c7_2(X217_287, a1176)))). % 40.91/22.24 tff(c_16106, plain, (![X217_287, X218_289]: (c7_2(X217_287, a1176) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.24 tff(c_16104, plain, (c3_2(a1035, a1036))). % 40.91/22.24 tff(c_16103, plain, (c3_2(a1068, a1070))). % 40.91/22.24 tff(c_16101, plain, (c4_2(a1125, a1126))). % 40.91/22.24 tff(c_16100, plain, (c3_2(a1092, a1093))). % 40.91/22.24 tff(c_16049, plain, (![X217_287, X218_289]: (c6_2(X217_287, a1176) | c9_1(X217_287) | c7_2(X217_287, X218_289) | c4_2(X217_287, X218_289) | c3_2(X217_287, X218_289) | ~ndr1_1(X217_287)))). % 40.91/22.24 tff(c_16046, plain, (![X148_200]: (c3_2(X148_200, a1101) | c1_1(X148_200) | c8_1(X148_200)))). % 40.91/22.24 tff(c_16043, plain, (![X148_200]: (c5_2(X148_200, a1101) | c1_1(X148_200) | c8_1(X148_200)))). % 40.91/22.24 tff(c_16040, plain, (![X148_200]: (c4_2(X148_200, a1101) | c1_1(X148_200) | c8_1(X148_200)))). % 40.91/22.24 tff(c_16038, plain, (c5_1(a997))). % 40.91/22.24 tff(c_16037, plain, (c7_1(a1087))). % 40.91/22.24 tff(c_15839, plain, (![X2_10]: (~c10_2(X2_10, a969) | ~c10_1(X2_10) | c9_2(X2_10, a1149) | c6_2(X2_10, a969) | c7_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.24 tff(c_15812, plain, (![X2_10]: (~c10_2(X2_10, a969) | ~c10_1(X2_10) | ~c7_2(X2_10, a1149) | c6_2(X2_10, a969) | c7_2(X2_10, a969) | ~ndr1_1(X2_10) | ~c5_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.24 tff(c_16020, plain, (~c3_2(a1120, a1121))). % 40.91/22.24 tff(c_16018, plain, (~c7_2(a1015, a1017))). % 40.91/22.24 tff(c_16019, plain, (ndr1_1(a997))). % 40.91/22.24 tff(c_16013, plain, (~c3_1(a1154))). % 40.91/22.24 tff(c_16009, plain, (c8_1(a1154))). % 40.91/22.24 tff(c_16003, plain, (c8_1(a1124))). % 40.91/22.24 tff(c_15998, plain, (c8_1(a1042))). % 40.91/22.24 tff(c_15992, plain, (c8_1(a1078))). % 40.91/22.24 tff(c_15987, plain, (c8_1(a995))). % 40.91/22.24 tff(c_15927, plain, (c8_1(a1041))). % 40.91/22.24 tff(c_15928, plain, (![X203_267, X205_271, X204_270]: (c7_1(X203_267) | ~c6_2(X203_267, X205_271) | c8_2(X203_267, X205_271) | c2_2(X203_267, X205_271) | ~c9_2(X203_267, X204_270) | ~c7_2(X203_267, X204_270) | ~c3_2(X203_267, X204_270) | ~ndr1_1(X203_267)))). % 40.91/22.24 tff(c_15919, plain, (c8_1(a1139))). % 40.91/22.24 tff(c_15891, plain, (![X148_200]: (ndr1_1(X148_200) | c1_1(X148_200) | c8_1(X148_200)))). % 40.91/22.24 tff(c_15524, plain, (![X188_361, X189_362]: (~c8_2(X188_361, a1149) | ~c10_2(X188_361, a1149) | ~c10_1(X188_361) | c6_2(X188_361, X189_362) | c9_2(X188_361, X189_362) | c7_2(X188_361, X189_362) | ~ndr1_1(X188_361) | ~c5_1(X188_361)))). % 40.91/22.24 tff(c_15525, plain, (![X188_361, X189_362]: (~c8_2(X188_361, X189_362) | ~c10_2(X188_361, X189_362) | ~c10_1(X188_361) | c9_2(X188_361, a1149) | c6_2(X188_361, X189_362) | c7_2(X188_361, X189_362) | ~ndr1_1(X188_361) | ~c5_1(X188_361)))). % 40.91/22.24 tff(c_15461, plain, (![X188_358, X189_359]: (~c8_2(X188_358, X189_359) | ~c10_2(X188_358, X189_359) | ~c10_1(X188_358) | ~c7_2(X188_358, a1149) | c6_2(X188_358, X189_359) | c7_2(X188_358, X189_359) | ~ndr1_1(X188_358) | ~c5_1(X188_358)))). % 40.91/22.24 tff(c_15763, plain, (~c7_2(a1035, a1037))). % 40.91/22.24 tff(c_15755, plain, (~c10_2(a1035, a1038))). % 40.91/22.24 tff(c_15752, plain, (c2_2(a1035, a1036))). % 40.91/22.24 tff(c_15736, plain, (~c9_2(a1035, a1036))). % 40.91/22.24 tff(c_15738, plain, (~c8_1(a1130))). % 40.91/22.24 tff(c_15730, plain, (~c1_2(a1035, a1038))). % 40.91/22.24 tff(c_15721, plain, (~c10_1(a1130))). % 40.91/22.24 tff(c_15718, plain, (~c5_1(a1035))). % 40.91/22.24 tff(c_15710, plain, (~c9_2(a1035, a1038))). % 40.91/22.24 tff(c_15706, plain, (c5_1(a1050))). % 40.91/22.24 tff(c_15705, plain, (~c7_2(a1035, a1036))). % 40.91/22.24 tff(c_15698, plain, (c8_2(a1035, a1036))). % 40.91/22.24 tff(c_15696, plain, (c3_2(a1035, a1037))). % 40.91/22.24 tff(c_15694, plain, (~c1_1(a1047))). % 40.91/22.24 tff(c_15693, plain, (c4_2(a1035, a1037))). % 40.91/22.24 tff(c_15690, plain, (~c10_1(a1026))). % 40.91/22.24 tff(c_15683, plain, (~c3_2(a1026, a1027))). % 40.91/22.24 tff(c_15681, plain, (~c4_2(a1026, a1027))). % 40.91/22.24 tff(c_15675, plain, (![X213_282]: (c10_2(X213_282, a1172) | c4_1(X213_282) | ~c7_1(X213_282)))). % 40.91/22.24 tff(c_15664, plain, (![X213_282]: (c1_2(X213_282, a1172) | c4_1(X213_282) | ~c7_1(X213_282)))). % 40.91/22.24 tff(c_15661, plain, (~c7_1(a1041))). % 40.91/22.24 tff(c_15660, plain, (~c6_1(a1041))). % 40.91/22.24 tff(c_15639, plain, (~ndr1_1(a1041))). % 40.91/22.24 tff(c_15629, plain, (![X20_367]: (c10_2(X20_367, a988) | ~c5_2(X20_367, a989) | c2_2(X20_367, a989) | ~ndr1_1(X20_367) | ~c6_1(X20_367)))). % 40.91/22.24 tff(c_15630, plain, (![X20_367]: (~c5_2(X20_367, a988) | ~c5_2(X20_367, a989) | c2_2(X20_367, a989) | ~ndr1_1(X20_367) | ~c6_1(X20_367)))). % 40.91/22.24 tff(c_15628, plain, (![X20_367]: (c1_2(X20_367, a988) | ~c5_2(X20_367, a989) | c2_2(X20_367, a989) | ~ndr1_1(X20_367) | ~c6_1(X20_367)))). % 40.91/22.24 tff(c_15635, plain, (~c6_1(a1043))). % 40.91/22.24 tff(c_15634, plain, (~c6_1(a1133))). % 40.91/22.24 tff(c_15605, plain, (![X20_30, X21_32]: (c6_2(X20_30, X21_32) | ~c5_2(X20_30, X21_32) | c2_2(X20_30, X21_32) | ~ndr1_1(X20_30) | ~c6_1(X20_30)))). % 40.91/22.24 tff(c_15579, plain, (~c5_2(a1026, a1027))). % 40.91/22.24 tff(c_15577, plain, (ndr1_1(a1035))). % 40.91/22.24 tff(c_15574, plain, (![X213_282]: (c4_2(X213_282, a1172) | c4_1(X213_282) | ~c7_1(X213_282)))). % 40.91/22.24 tff(c_15530, plain, (![X188_363]: (~c8_2(X188_363, a1149) | ~c10_2(X188_363, a1149) | ~c10_1(X188_363) | c6_2(X188_363, a1149) | c7_2(X188_363, a1149) | ~ndr1_1(X188_363) | ~c5_1(X188_363)))). % 40.91/22.24 tff(c_15561, plain, (~c3_1(a1124))). % 40.91/22.24 tff(c_15560, plain, (~c6_1(a1124))). % 40.91/22.24 tff(c_15556, plain, (c4_1(a1124))). % 40.91/22.24 tff(c_15538, plain, (~ndr1_1(a1124))). % 40.91/22.24 tff(c_15535, plain, (ndr1_1(a1026))). % 40.91/22.24 tff(c_15533, plain, (c5_1(a1026))). % 40.91/22.24 tff(c_15509, plain, (![X188_248]: (c6_2(X188_248, a1149) | c7_2(X188_248, a1149) | ~ndr1_1(X188_248) | ~c5_1(X188_248) | c9_2(X188_248, a1149)))). % 40.91/22.24 tff(c_15496, plain, (![X188_248, X189_250]: (c9_2(X188_248, a1149) | c6_2(X188_248, X189_250) | c9_2(X188_248, X189_250) | c7_2(X188_248, X189_250) | ~ndr1_1(X188_248) | ~c5_1(X188_248)))). % 40.91/22.24 tff(c_15490, plain, (~c7_1(a1154))). % 40.91/22.24 tff(c_15489, plain, (~c7_1(a1042))). % 40.91/22.24 tff(c_15488, plain, (~c7_1(a1139))). % 40.91/22.24 tff(c_15487, plain, (~c7_1(a995))). % 40.91/22.24 tff(c_15486, plain, (~c7_1(a1078))). % 40.91/22.24 tff(c_15464, plain, (![X213_282]: (ndr1_1(X213_282) | c4_1(X213_282) | ~c7_1(X213_282)))). % 40.91/22.24 tff(c_15441, plain, (![X188_248, X189_250]: (~c7_2(X188_248, a1149) | c6_2(X188_248, X189_250) | c9_2(X188_248, X189_250) | c7_2(X188_248, X189_250) | ~ndr1_1(X188_248) | ~c5_1(X188_248)))). % 40.91/22.24 tff(c_15435, plain, (~c4_1(a971))). % 40.91/22.24 tff(c_15431, plain, (~c5_1(a1098))). % 40.91/22.24 tff(c_15430, plain, (c10_1(a1062))). % 40.91/22.24 tff(c_15426, plain, (~c8_1(a1098))). % 40.91/22.24 tff(c_15421, plain, (~c5_1(a1062))). % 40.91/22.24 tff(c_15418, plain, (~c9_1(a971))). % 40.91/22.24 tff(c_15403, plain, (![X145_196]: (c3_1(X145_196) | ~c9_1(X145_196) | c2_2(X145_196, a1100) | ~c7_2(X145_196, a1100) | ~ndr1_1(X145_196) | ~c5_1(X145_196) | ~c2_1(X145_196)))). % 40.91/22.24 tff(c_15412, plain, (~c7_2(a1125, a1126))). % 40.91/22.24 tff(c_15411, plain, (~c7_2(a1068, a1070))). % 40.91/22.24 tff(c_15388, plain, (![X34_51, X35_53]: (c3_1(X34_51) | ~c9_1(X34_51) | c2_2(X34_51, X35_53) | ~c7_2(X34_51, X35_53) | ~c8_2(X34_51, X35_53) | ~ndr1_1(X34_51)))). % 40.91/22.24 tff(c_15373, plain, (![X159_214]: (c10_2(X159_214, a1111) | ~c9_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15349, plain, (![X159_214]: (~c3_2(X159_214, a1111) | c7_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15325, plain, (![X159_214]: (c10_2(X159_214, a1111) | c5_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15300, plain, (![X159_214]: (~c3_2(X159_214, a1111) | c5_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15266, plain, (![X159_214]: (~c3_2(X159_214, a1111) | ~c9_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15265, plain, (c3_2(a1053, a1054))). % 40.91/22.24 tff(c_15262, plain, (![X159_344]: (~c8_2(X159_344, a1111) | ~c10_2(X159_344, a1111) | ~ndr1_1(X159_344) | ~c10_1(X159_344) | c5_2(X159_344, a1112) | ~c6_1(X159_344)))). % 40.91/22.24 tff(c_15257, plain, (![X159_214]: (c9_2(X159_214, a1111) | c5_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15234, plain, (~c1_2(a1043, a1044))). % 40.91/22.24 tff(c_15231, plain, (c10_2(a1053, a1054))). % 40.91/22.24 tff(c_15229, plain, (~c6_2(a1043, a1044))). % 40.91/22.24 tff(c_15226, plain, (~c6_1(a1087))). % 40.91/22.24 tff(c_15214, plain, (![X159_214]: (c9_2(X159_214, a1111) | ~c9_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15190, plain, (![X159_339]: (~c8_2(X159_339, a1111) | ~c10_2(X159_339, a1111) | ~ndr1_1(X159_339) | ~c10_1(X159_339) | c7_2(X159_339, a1112) | ~c6_1(X159_339)))). % 40.91/22.24 tff(c_15185, plain, (![X159_214]: (c9_2(X159_214, a1111) | c7_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15162, plain, (c4_2(a1043, a1044))). % 40.91/22.24 tff(c_15159, plain, (~c2_2(a1053, a1054))). % 40.91/22.24 tff(c_15156, plain, (![X159_214]: (c10_2(X159_214, a1111) | c7_2(X159_214, a1112) | ~c6_1(X159_214)))). % 40.91/22.24 tff(c_15133, plain, (~c9_1(a1046))). % 40.91/22.24 tff(c_15131, plain, (c1_1(a1053))). % 40.91/22.24 tff(c_15127, plain, (ndr1_1(a1053))). % 40.91/22.24 tff(c_15122, plain, (c5_1(a1043))). % 40.91/22.24 tff(c_15109, plain, (~c3_1(a1078))). % 40.91/22.24 tff(c_15108, plain, (~c2_1(a1078))). % 40.91/22.24 tff(c_15106, plain, (~c6_1(a1078))). % 40.91/22.24 tff(c_15090, plain, (~ndr1_1(a1078))). % 40.91/22.24 tff(c_15084, plain, (ndr1_1(a1043))). % 40.91/22.24 tff(c_15075, plain, (~c10_1(a1087))). % 40.91/22.24 tff(c_15073, plain, (~c10_1(a1015))). % 40.91/22.24 tff(c_15031, plain, (![X176_232, X177_234]: (~c8_2(X176_232, X177_234) | ~c9_2(X176_232, X177_234) | ~c10_2(X176_232, X177_234) | ~ndr1_1(X176_232) | ~c10_1(X176_232)))). % 40.91/22.24 tff(c_15020, plain, (~c2_1(a1043))). % 40.91/22.24 tff(c_15013, plain, (~c3_1(a1043))). % 40.91/22.24 tff(c_15009, plain, (c8_1(a1043))). % 40.91/22.24 tff(c_14924, plain, (~c3_1(a1139))). % 40.91/22.24 tff(c_14923, plain, (~c2_1(a1139))). % 40.91/22.24 tff(c_14922, plain, (~c6_1(a1139))). % 40.91/22.24 tff(c_14906, plain, (~ndr1_1(a1139))). % 40.91/22.24 tff(c_14886, plain, (~c2_1(a1154))). % 40.91/22.24 tff(c_14868, plain, (~ndr1_1(a1154))). % 40.91/22.24 tff(c_14799, plain, (~c2_1(a1041))). % 40.91/22.24 tff(c_14751, plain, (![X152_205]: (~c10_1(X152_205) | c3_1(X152_205) | ~c2_1(X152_205)))). % 40.91/22.24 tff(c_14773, plain, (~c10_1(a1120))). % 40.91/22.24 tff(c_14772, plain, (~c10_1(a1068))). % 40.91/22.24 tff(c_14771, plain, (~c10_1(a967))). % 40.91/22.24 tff(c_14702, plain, (![X152_205]: (~c2_2(X152_205, a1104) | c3_1(X152_205) | ~c2_1(X152_205)))). % 40.91/22.24 tff(c_14685, plain, (~c2_1(a1042))). % 40.91/22.24 tff(c_14683, plain, (~c3_1(a1042))). % 40.91/22.24 tff(c_14684, plain, (~c6_1(a1042))). % 40.91/22.24 tff(c_14666, plain, (~ndr1_1(a1042))). % 40.91/22.24 tff(c_14644, plain, (![X152_205]: (~c3_2(X152_205, a1104) | c3_1(X152_205) | ~c2_1(X152_205)))). % 40.91/22.25 tff(c_14640, plain, (![X152_205]: (c9_2(X152_205, a1104) | c3_1(X152_205) | ~c2_1(X152_205)))). % 40.91/22.25 tff(c_14637, plain, (![X58_85]: (~c5_2(X58_85, a1002) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.25 tff(c_14634, plain, (![X58_85]: (c7_2(X58_85, a1002) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.25 tff(c_14629, plain, (![X58_85]: (c1_2(X58_85, a1002) | ~c6_1(X58_85) | ~c2_1(X58_85)))). % 40.91/22.25 tff(c_14622, plain, (~c10_1(a1125))). % 40.91/22.25 tff(c_13800, plain, (![X146_197, X147_199]: (c2_2(X146_197, X147_199) | c3_2(X146_197, X147_199) | ~ndr1_1(X146_197) | ~c2_1(X146_197) | ~c10_1(X146_197)))). % 40.91/22.25 tff(c_14591, plain, (![X152_205]: (ndr1_1(X152_205) | c3_1(X152_205) | ~c2_1(X152_205)))). % 40.91/22.25 tff(c_14573, plain, (~c4_2(a1092, a1093))). % 40.91/22.25 tff(c_14568, plain, (~c10_2(a1092, a1093))). % 40.91/22.25 tff(c_14562, plain, (~c5_2(a1092, a1094))). % 40.91/22.25 tff(c_14553, plain, (~c7_2(a1092, a1093))). % 40.91/22.25 tff(c_14552, plain, (~c3_2(a1092, a1094))). % 40.91/22.25 tff(c_14549, plain, (c10_2(a1092, a1094))). % 40.91/22.25 tff(c_14548, plain, (~c3_1(a1087))). % 40.91/22.25 tff(c_14547, plain, (~c2_1(a1087))). % 40.91/22.25 tff(c_14542, plain, (~c5_2(a1173, a1174))). % 40.91/22.25 tff(c_14537, plain, (![X26_39]: (c1_2(X26_39, a988) | ~c6_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14534, plain, (c4_2(a1173, a1174))). % 40.91/22.25 tff(c_14522, plain, (![X_4]: (c3_2(a963, X_4) | c10_2(a963, X_4) | c9_2(a963, X_4)))). % 40.91/22.25 tff(c_14514, plain, (![X26_39]: (~c5_2(X26_39, a988) | c9_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14512, plain, (![X129_175]: (c6_2(a1087, X129_175) | c5_2(a1087, X129_175) | c9_2(a1087, X129_175)))). % 40.91/22.25 tff(c_14510, plain, (~c3_1(a1041))). % 40.91/22.25 tff(c_14498, plain, (![X128_174]: (~c3_2(a1087, X128_174) | ~c8_2(a1087, X128_174) | c6_2(a1087, X128_174)))). % 40.91/22.25 tff(c_14493, plain, (![X26_39]: (c1_2(X26_39, a988) | ~c8_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14487, plain, (![X26_39]: (c10_2(X26_39, a988) | c9_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14485, plain, (![X26_39]: (c1_2(X26_39, a988) | c9_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14483, plain, (![X26_39]: (c10_2(X26_39, a988) | ~c6_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14480, plain, (![X26_39]: (~c5_2(X26_39, a988) | ~c6_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14479, plain, (ndr1_1(a1092))). % 40.91/22.25 tff(c_14478, plain, (~c10_1(a1092))). % 40.91/22.25 tff(c_14476, plain, (![X26_39]: (~c5_2(X26_39, a988) | ~c8_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14474, plain, (![X26_39]: (c10_2(X26_39, a988) | ~c8_2(X26_39, a989) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14471, plain, (~c2_1(a995))). % 40.91/22.25 tff(c_14470, plain, (~c3_1(a995))). % 40.91/22.25 tff(c_14469, plain, (~c6_1(a995))). % 40.91/22.25 tff(c_14457, plain, (~ndr1_1(a995))). % 40.91/22.25 tff(c_14447, plain, (ndr1_1(a1173))). % 40.91/22.25 tff(c_14443, plain, (![X2_10]: (~c5_2(X2_10, a969) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.25 tff(c_14439, plain, (~c7_2(a1015, a1016))). % 40.91/22.25 tff(c_14435, plain, (~c2_1(a1124))). % 40.91/22.25 tff(c_14432, plain, (c7_1(a1124))). % 40.91/22.25 tff(c_14429, plain, (c3_1(a1173))). % 40.91/22.25 tff(c_14415, plain, (c9_2(a1015, a1017))). % 40.91/22.25 tff(c_14413, plain, (c3_2(a1015, a1017))). % 40.91/22.25 tff(c_14411, plain, (![X2_10]: (c8_2(X2_10, a969) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.25 tff(c_14403, plain, (![X2_10]: (c10_2(X2_10, a969) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.25 tff(c_14400, plain, (c3_2(a1015, a1016))). % 40.91/22.25 tff(c_14399, plain, (~c1_2(a1015, a1017))). % 40.91/22.25 tff(c_14395, plain, (![X145_196]: (~c10_2(X145_196, a1100) | ~c5_1(X145_196) | ~c2_1(X145_196)))). % 40.91/22.25 tff(c_14388, plain, (![X145_196]: (c8_2(X145_196, a1100) | ~c5_1(X145_196) | ~c2_1(X145_196)))). % 40.91/22.25 tff(c_14380, plain, (![X145_196]: (ndr1_1(X145_196) | ~c5_1(X145_196) | ~c2_1(X145_196)))). % 40.91/22.25 tff(c_14372, plain, (![X2_10]: (ndr1_1(X2_10) | ~c3_1(X2_10) | c9_1(X2_10)))). % 40.91/22.25 tff(c_14350, plain, (ndr1_1(a1015))). % 40.91/22.25 tff(c_14242, plain, (![X154_207]: (~c8_1(X154_207) | ~c3_1(X154_207)))). % 40.91/22.25 tff(c_14231, plain, (~c10_1(a1058))). % 40.91/22.25 tff(c_14216, plain, (~c10_1(a1078))). % 40.91/22.25 tff(c_14212, plain, (~c9_1(a1061))). % 40.91/22.25 tff(c_14188, plain, (~c2_2(a1068, a1069))). % 40.91/22.25 tff(c_14179, plain, (~c6_2(a1133, a1134))). % 40.91/22.25 tff(c_14180, plain, (~c1_1(a1058))). % 40.91/22.25 tff(c_14169, plain, (~c5_1(a1058))). % 40.91/22.25 tff(c_14164, plain, (~c5_2(a1068, a1069))). % 40.91/22.25 tff(c_14149, plain, (~c2_2(a1133, a1134))). % 40.91/22.25 tff(c_14146, plain, (c9_2(a1120, a1121))). % 40.91/22.25 tff(c_14144, plain, (c5_2(a1133, a1134))). % 40.91/22.25 tff(c_14128, plain, (c2_2(a1120, a1121))). % 40.91/22.25 tff(c_14122, plain, (c10_1(a1007))). % 40.91/22.25 tff(c_14120, plain, (~c9_1(a1059))). % 40.91/22.25 tff(c_14111, plain, (~c1_1(a1005))). % 40.91/22.25 tff(c_14107, plain, (c8_2(a1068, a1070))). % 40.91/22.25 tff(c_14104, plain, (c1_2(a1120, a1121))). % 40.91/22.25 tff(c_14095, plain, (~c8_1(a1066))). % 40.91/22.25 tff(c_14092, plain, (~c1_1(a1003))). % 40.91/22.25 tff(c_14080, plain, (~c2_2(a1068, a1070))). % 40.91/22.25 tff(c_14072, plain, (c1_2(a967, a968))). % 40.91/22.25 tff(c_14070, plain, (c1_2(a1068, a1070))). % 40.91/22.25 tff(c_14058, plain, (![X26_39]: (ndr1_1(X26_39) | ~c6_1(X26_39)))). % 40.91/22.25 tff(c_14056, plain, (c6_2(a967, a968))). % 40.91/22.25 tff(c_14054, plain, (~c8_2(a967, a968))). % 40.91/22.25 tff(c_14031, plain, (c9_1(a1154))). % 40.91/22.25 tff(c_14024, plain, (ndr1_1(a967))). % 40.91/22.25 tff(c_14020, plain, (~c4_1(a966))). % 40.91/22.25 tff(c_14013, plain, (~c6_1(a1154))). % 40.91/22.25 tff(c_14011, plain, (c4_1(a967))). % 40.91/22.25 tff(c_14007, plain, (~c1_1(a1139))). % 40.91/22.25 tff(c_14000, plain, (~c10_1(a1139))). % 40.91/22.25 tff(c_13996, plain, (~c2_1(a1133))). % 40.91/22.25 tff(c_13993, plain, (c7_1(a1133))). % 40.91/22.25 tff(c_13988, plain, (~c1_2(a1125, a1127))). % 40.91/22.25 tff(c_13977, plain, (c4_2(a1125, a1127))). % 40.91/22.25 tff(c_13966, plain, (c5_2(a1125, a1127))). % 40.91/22.25 tff(c_13961, plain, (~c3_2(a1125, a1126))). % 40.91/22.25 tff(c_13958, plain, (ndr1_1(a1133))). % 40.91/22.25 tff(c_13951, plain, (c8_2(a1125, a1126))). % 40.91/22.25 tff(c_13948, plain, (~c3_1(a1068))). % 40.91/22.25 tff(c_13945, plain, (~c3_1(a967))). % 40.91/22.25 tff(c_13941, plain, (ndr1_1(a1068))). % 40.91/22.25 tff(c_13933, plain, (ndr1_1(a1120))). % 40.91/22.25 tff(c_13930, plain, (~c10_2(a1125, a1126))). % 40.91/22.25 tff(c_13924, plain, (~c9_1(a966))). % 40.91/22.25 tff(c_13922, plain, (~c1_1(a1120))). % 40.91/22.25 tff(c_13908, plain, (c4_1(a1120))). % 40.91/22.25 tff(c_13889, plain, (~c5_2(a1087, a1088))). % 40.91/22.25 tff(c_13885, plain, (~c10_2(a1087, a1088))). % 40.91/22.25 tff(c_13879, plain, (~c9_1(a1042))). % 40.91/22.26 tff(c_13876, plain, (~c4_2(a1087, a1088))). % 40.91/22.26 tff(c_13872, plain, (~c4_1(a1125))). % 40.91/22.26 tff(c_13866, plain, (c9_0)). % 40.91/22.26 tff(c_13863, plain, (c4_2(a963, a964))). % 40.91/22.26 tff(c_13861, plain, (ndr1_1(a1125))). % 40.91/22.26 tff(c_13856, plain, (c1_2(a963, a964))). % 40.91/22.26 tff(c_13853, plain, (~c5_2(a963, a964))). % 40.91/22.26 tff(c_13835, plain, (~c6_1(a963))). % 40.91/22.26 tff(c_13831, plain, (c1_0)). % 40.91/22.26 tff(c_13828, plain, (c6_0)). % 40.91/22.26 tff(c_13825, plain, (ndr1_1(a963))). % 40.91/22.26 tff(c_13822, plain, (ndr1_1(a1087))). % 40.91/22.26 tff(c_13823, plain, (c2_0)). % 40.91/22.26 tff(c_13817, plain, (~c5_0)). % 40.91/22.26 tff(c_13816, plain, (c4_0)). % 40.91/22.26 tff(c_13814, plain, (~c10_0)). % 40.91/22.26 tff(c_13813, plain, (~c7_0)). % 40.91/22.26 tff(c_13812, plain, (~c3_0)). % 40.91/22.26 tff(c_13811, plain, (~c8_0)). % 40.91/22.26 tff(c_8152, plain, (ndr1_0)). % 40.91/22.26 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.91/22.26 %------------------------------------------------------------------------------