%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP075-1 : TPTP v9.0.0. Released v2.4.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 : n016.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 07:48:07 PM UTC 2025 % Result : Satisfiable 61.90s 51.92s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP075-1 : TPTP v9.0.0. Released v2.4.0. % 0.06/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.13/0.33 % Computer : n016.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:24:38 EDT 2025 % 0.13/0.34 % CPUTime : % 61.90/51.92 % 61.90/51.92 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 61.90/51.92 % 61.90/51.92 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 61.90/51.93 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf25 > skf24 > skf22 > skf20 > skf18 > skf16 > skf14 > #nlpp > skf12 > skf11 > skf10 > skc5 > skc4 > skc3 % 61.90/51.93 % 61.90/51.93 %Foreground sorts: % 61.90/51.93 % 61.90/51.93 % 61.90/51.93 %Background operators: % 61.90/51.93 % 61.90/51.93 % 61.90/51.93 %Foreground operators: % 61.90/51.93 tff(nonliving, type, nonliving: ($i * $i) > $o). % 61.90/51.93 tff(member, type, member: ($i * $i * $i) > $o). % 61.90/51.93 tff(living, type, living: ($i * $i) > $o). % 61.90/51.93 tff(fire, type, fire: ($i * $i) > $o). % 61.90/51.93 tff(human_person, type, human_person: ($i * $i) > $o). % 61.90/51.93 tff(action, type, action: ($i * $i) > $o). % 61.90/51.93 tff(present, type, present: ($i * $i) > $o). % 61.90/51.93 tff(shot, type, shot: ($i * $i) > $o). % 61.90/51.93 tff(skf22, type, skf22: ($i * $i) > $i). % 61.90/51.93 tff(entity, type, entity: ($i * $i) > $o). % 61.90/51.93 tff(skf12, type, skf12: $i > $i). % 61.90/51.93 tff(eventuality, type, eventuality: ($i * $i) > $o). % 61.90/51.93 tff(weapon, type, weapon: ($i * $i) > $o). % 61.90/51.93 tff(existent, type, existent: ($i * $i) > $o). % 61.90/51.93 tff(singleton, type, singleton: ($i * $i) > $o). % 61.90/51.93 tff(male, type, male: ($i * $i) > $o). % 61.90/51.93 tff(multiple, type, multiple: ($i * $i) > $o). % 61.90/51.93 tff(organism, type, organism: ($i * $i) > $o). % 61.90/51.93 tff(animate, type, animate: ($i * $i) > $o). % 61.90/51.93 tff(of, type, of: ($i * $i * $i) > $o). % 61.90/51.93 tff(skf14, type, skf14: ($i * $i) > $i). % 61.90/51.93 tff(actual_world, type, actual_world: $i > $o). % 61.90/51.93 tff(agent, type, agent: ($i * $i * $i) > $o). % 61.90/51.93 tff(skf10, type, skf10: $i > $i). % 61.90/51.93 tff(skf24, type, skf24: ($i * $i) > $i). % 61.90/51.93 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 61.90/51.93 tff(group, type, group: ($i * $i) > $o). % 61.90/51.93 tff(artifact, type, artifact: ($i * $i) > $o). % 61.90/51.93 tff(cannon, type, cannon: ($i * $i) > $o). % 61.90/51.93 tff(event, type, event: ($i * $i) > $o). % 61.90/51.93 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 61.90/51.93 tff(patient, type, patient: ($i * $i * $i) > $o). % 61.90/51.93 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 61.90/51.93 tff(skc4, type, skc4: $i). % 61.90/51.93 tff(skf25, type, skf25: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 61.90/51.93 tff(skc3, type, skc3: $i). % 61.90/51.93 tff(thing, type, thing: ($i * $i) > $o). % 61.90/51.93 tff(human, type, human: ($i * $i) > $o). % 61.90/51.93 tff(six, type, six: ($i * $i) > $o). % 61.90/51.93 tff(skf18, type, skf18: ($i * $i) > $i). % 61.90/51.93 tff(man, type, man: ($i * $i) > $o). % 61.90/51.93 tff(skf11, type, skf11: $i > $i). % 61.90/51.93 tff(skc5, type, skc5: $i). % 61.90/51.93 tff(weaponry, type, weaponry: ($i * $i) > $o). % 61.90/51.93 tff(unisex, type, unisex: ($i * $i) > $o). % 61.90/51.93 tff(skf16, type, skf16: ($i * $i) > $i). % 61.90/51.93 tff(set, type, set: ($i * $i) > $o). % 61.90/51.93 tff(impartial, type, impartial: ($i * $i) > $o). % 61.90/51.93 tff(object, type, object: ($i * $i) > $o). % 61.90/51.93 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 61.90/51.93 tff(specific, type, specific: ($i * $i) > $o). % 61.90/51.93 tff(skf20, type, skf20: ($i * $i) > $i). % 61.90/51.93 tff(act, type, act: ($i * $i) > $o). % 61.90/51.93 % 61.90/51.93 %Saturated clause set: % 61.90/51.94 tff(c_1718, plain, (![X_1207, V_1209, W_1173, X2_1178, Z_194, V_199, V_1187, Y_1198, Z_1201, X_1176, X1_1181, X2_196, X2_1186, Z_1185, X1_1179, X1_1192, X_1206, V_1203, Y_1210, X_1212, V_1197, X2_1175, X_1191, Z_1193, W_192, Z_1190, X1_195, X1_1204, X1_1199, V_1174, Y_1200, Y_1202, V_1211, X2_1205, X_197, Y_198, X1_1188, Z_1208, U_193, X_1184, X2_1183, X2_1195, Y_1189, Z_1182, Y_1177]: (skf25(V_1203, X_1191, Y_1202, Z_1208, X1_1179, X2_1186, W_192, U_193)=skf25(V_1174, X_1207, Y_1200, Z_1201, X1_1199, X2_1195, W_192, U_193) | skf25(V_1209, X_1206, Y_1177, Z_1182, X1_1204, X2_1183, W_192, U_193)=skf25(V_1174, X_1207, Y_1200, Z_1201, X1_1199, X2_1195, W_192, U_193) | skf25(V_1209, X_1206, Y_1177, Z_1182, X1_1204, X2_1183, W_192, U_193)=skf25(V_1203, X_1191, Y_1202, Z_1208, X1_1179, X2_1186, W_192, U_193) | skf25(V_1211, X_1184, Y_1189, Z_1185, X1_1192, X2_1178, W_192, U_193)=skf25(V_1209, X_1206, Y_1177, Z_1182, X1_1204, X2_1183, W_192, U_193) | skf25(V_1211, X_1184, Y_1189, Z_1185, X1_1192, X2_1178, W_192, U_193)=skf25(V_1174, X_1207, Y_1200, Z_1201, X1_1199, X2_1195, W_192, U_193) | skf25(V_1211, X_1184, Y_1189, Z_1185, X1_1192, X2_1178, W_192, U_193)=skf25(V_1203, X_1191, Y_1202, Z_1208, X1_1179, X2_1186, W_192, U_193) | skf25(V_1211, X_1184, Y_1189, Z_1185, X1_1192, X2_1178, W_192, U_193)=skf25(V_1197, X_1212, Y_1198, Z_1193, X1_1181, X2_1175, W_192, U_193) | skf25(V_1209, X_1206, Y_1177, Z_1182, X1_1204, X2_1183, W_192, U_193)=skf25(V_1197, X_1212, Y_1198, Z_1193, X1_1181, X2_1175, W_192, U_193) | skf25(V_1197, X_1212, Y_1198, Z_1193, X1_1181, X2_1175, W_192, U_193)=skf25(V_1174, X_1207, Y_1200, Z_1201, X1_1199, X2_1195, W_192, U_193) | skf25(V_1203, X_1191, Y_1202, Z_1208, X1_1179, X2_1186, W_192, U_193)=skf25(V_1197, X_1212, Y_1198, Z_1193, X1_1181, X2_1175, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1197, X_1212, Y_1198, Z_1193, X1_1181, X2_1175, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1211, X_1184, Y_1189, Z_1185, X1_1192, X2_1178, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1209, X_1206, Y_1177, Z_1182, X1_1204, X2_1183, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1174, X_1207, Y_1200, Z_1201, X1_1199, X2_1195, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1203, X_1191, Y_1202, Z_1208, X1_1179, X2_1186, W_192, U_193) | skf25(skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), V_1187, W_1173, X_1176, Y_1210, Z_1190, X1_1188, X2_1205)!=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_1186=X1_1179 | Z_1208=X1_1179 | Z_1208=X2_1186 | Z_1208=Y_1202 | Y_1202=X1_1179 | Y_1202=X2_1186 | Y_1202=X_1191 | Z_1208=X_1191 | X_1191=X1_1179 | X_1191=X2_1186 | X_1191=V_1203 | Y_1202=V_1203 | Z_1208=V_1203 | X1_1179=V_1203 | X2_1186=V_1203 | ~member(U_193, X2_1186, W_192) | ~member(U_193, X1_1179, W_192) | ~member(U_193, Z_1208, W_192) | ~member(U_193, Y_1202, W_192) | ~member(U_193, X_1191, W_192) | ~member(U_193, V_1203, W_192) | X2_1195=X1_1199 | Z_1201=X1_1199 | Z_1201=X2_1195 | Z_1201=Y_1200 | Y_1200=X1_1199 | Y_1200=X2_1195 | Y_1200=X_1207 | Z_1201=X_1207 | X_1207=X1_1199 | X_1207=X2_1195 | X_1207=V_1174 | Y_1200=V_1174 | Z_1201=V_1174 | X1_1199=V_1174 | X2_1195=V_1174 | ~member(U_193, X2_1195, W_192) | ~member(U_193, X1_1199, W_192) | ~member(U_193, Z_1201, W_192) | ~member(U_193, Y_1200, W_192) | ~member(U_193, X_1207, W_192) | ~member(U_193, V_1174, W_192) | X2_1183=X1_1204 | Z_1182=X1_1204 | Z_1182=X2_1183 | Z_1182=Y_1177 | Y_1177=X1_1204 | Y_1177=X2_1183 | Y_1177=X_1206 | Z_1182=X_1206 | X_1206=X1_1204 | X_1206=X2_1183 | X_1206=V_1209 | Y_1177=V_1209 | Z_1182=V_1209 | X1_1204=V_1209 | X2_1183=V_1209 | ~member(U_193, X2_1183, W_192) | ~member(U_193, X1_1204, W_192) | ~member(U_193, Z_1182, W_192) | ~member(U_193, Y_1177, W_192) | ~member(U_193, X_1206, W_192) | ~member(U_193, V_1209, W_192) | X2_1178=X1_1192 | Z_1185=X1_1192 | Z_1185=X2_1178 | Z_1185=Y_1189 | Y_1189=X1_1192 | Y_1189=X2_1178 | Y_1189=X_1184 | Z_1185=X_1184 | X_1184=X1_1192 | X_1184=X2_1178 | X_1184=V_1211 | Y_1189=V_1211 | Z_1185=V_1211 | X1_1192=V_1211 | X2_1178=V_1211 | ~member(U_193, X2_1178, W_192) | ~member(U_193, X1_1192, W_192) | ~member(U_193, Z_1185, W_192) | ~member(U_193, Y_1189, W_192) | ~member(U_193, X_1184, W_192) | ~member(U_193, V_1211, W_192) | X2_1175=X1_1181 | Z_1193=X1_1181 | Z_1193=X2_1175 | Z_1193=Y_1198 | Y_1198=X1_1181 | Y_1198=X2_1175 | Y_1198=X_1212 | Z_1193=X_1212 | X_1212=X1_1181 | X_1212=X2_1175 | X_1212=V_1197 | Y_1198=V_1197 | Z_1193=V_1197 | X1_1181=V_1197 | X2_1175=V_1197 | ~member(U_193, X2_1175, W_192) | ~member(U_193, X1_1181, W_192) | ~member(U_193, Z_1193, W_192) | ~member(U_193, Y_1198, W_192) | ~member(U_193, X_1212, W_192) | ~member(U_193, V_1197, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.94 tff(c_1673, plain, (![Y_1086, X1_1074, X2_1097, Y_1075, Z_194, Z_1090, Z_1078, V_199, V_1102, X2_1083, X_1071, V_1081, X2_196, X2_1073, Y_1094, X_1089, Z_1085, V_1096, X1_1100, X1_1099, X_1101, X2_1079, X_1088, W_192, X1_195, X_1104, Y_1098, X1_1103, X_197, Y_198, Z_1080, W_1077, X1_1082, Z_1091, U_193, Y_1072, U_1084, V_1076, X2_1087]: (skf25(V_1102, X_1089, Y_1072, Z_1078, X1_1082, X2_1097, W_192, U_193)=skf25(V_1076, X_1088, Y_1094, Z_1090, X1_1100, X2_1079, W_192, U_193) | skf25(V_1102, X_1089, Y_1072, Z_1078, X1_1082, X2_1097, W_192, U_193)=skf25(V_1081, X_1071, Y_1075, Z_1085, X1_1103, X2_1087, W_192, U_193) | skf25(V_1081, X_1071, Y_1075, Z_1085, X1_1103, X2_1087, W_192, U_193)=skf25(V_1076, X_1088, Y_1094, Z_1090, X1_1100, X2_1079, W_192, U_193) | skf25(V_1096, X_1104, Y_1098, Z_1091, X1_1074, X2_1073, W_192, U_193)=skf25(V_1081, X_1071, Y_1075, Z_1085, X1_1103, X2_1087, W_192, U_193) | skf25(V_1102, X_1089, Y_1072, Z_1078, X1_1082, X2_1097, W_192, U_193)=skf25(V_1096, X_1104, Y_1098, Z_1091, X1_1074, X2_1073, W_192, U_193) | skf25(V_1096, X_1104, Y_1098, Z_1091, X1_1074, X2_1073, W_192, U_193)=skf25(V_1076, X_1088, Y_1094, Z_1090, X1_1100, X2_1079, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1096, X_1104, Y_1098, Z_1091, X1_1074, X2_1073, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1081, X_1071, Y_1075, Z_1085, X1_1103, X2_1087, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1102, X_1089, Y_1072, Z_1078, X1_1082, X2_1097, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1076, X_1088, Y_1094, Z_1090, X1_1100, X2_1079, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_1084 | skf25(V_1096, X_1104, Y_1098, Z_1091, X1_1074, X2_1073, W_192, U_193)=U_1084 | skf25(V_1081, X_1071, Y_1075, Z_1085, X1_1103, X2_1087, W_192, U_193)=U_1084 | skf25(V_1102, X_1089, Y_1072, Z_1078, X1_1082, X2_1097, W_192, U_193)=U_1084 | skf25(V_1076, X_1088, Y_1094, Z_1090, X1_1100, X2_1079, W_192, U_193)=U_1084 | ~member(U_193, U_1084, W_192) | skf25(U_1084, skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_1077, X_1101, Y_1086, Z_1080, X1_1099, X2_1083)!=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_1079=X1_1100 | Z_1090=X1_1100 | Z_1090=X2_1079 | Z_1090=Y_1094 | Y_1094=X1_1100 | Y_1094=X2_1079 | Y_1094=X_1088 | Z_1090=X_1088 | X_1088=X1_1100 | X_1088=X2_1079 | X_1088=V_1076 | Y_1094=V_1076 | Z_1090=V_1076 | X1_1100=V_1076 | X2_1079=V_1076 | ~member(U_193, X2_1079, W_192) | ~member(U_193, X1_1100, W_192) | ~member(U_193, Z_1090, W_192) | ~member(U_193, Y_1094, W_192) | ~member(U_193, X_1088, W_192) | ~member(U_193, V_1076, W_192) | X2_1097=X1_1082 | Z_1078=X1_1082 | Z_1078=X2_1097 | Z_1078=Y_1072 | Y_1072=X1_1082 | Y_1072=X2_1097 | Y_1072=X_1089 | Z_1078=X_1089 | X_1089=X1_1082 | X_1089=X2_1097 | X_1089=V_1102 | Y_1072=V_1102 | Z_1078=V_1102 | X1_1082=V_1102 | X2_1097=V_1102 | ~member(U_193, X2_1097, W_192) | ~member(U_193, X1_1082, W_192) | ~member(U_193, Z_1078, W_192) | ~member(U_193, Y_1072, W_192) | ~member(U_193, X_1089, W_192) | ~member(U_193, V_1102, W_192) | X2_1087=X1_1103 | Z_1085=X1_1103 | Z_1085=X2_1087 | Z_1085=Y_1075 | Y_1075=X1_1103 | Y_1075=X2_1087 | Y_1075=X_1071 | Z_1085=X_1071 | X_1071=X1_1103 | X_1071=X2_1087 | X_1071=V_1081 | Y_1075=V_1081 | Z_1085=V_1081 | X1_1103=V_1081 | X2_1087=V_1081 | ~member(U_193, X2_1087, W_192) | ~member(U_193, X1_1103, W_192) | ~member(U_193, Z_1085, W_192) | ~member(U_193, Y_1075, W_192) | ~member(U_193, X_1071, W_192) | ~member(U_193, V_1081, W_192) | X2_1073=X1_1074 | Z_1091=X1_1074 | Z_1091=X2_1073 | Z_1091=Y_1098 | Y_1098=X1_1074 | Y_1098=X2_1073 | Y_1098=X_1104 | Z_1091=X_1104 | X_1104=X1_1074 | X_1104=X2_1073 | X_1104=V_1096 | Y_1098=V_1096 | Z_1091=V_1096 | X1_1074=V_1096 | X2_1073=V_1096 | ~member(U_193, X2_1073, W_192) | ~member(U_193, X1_1074, W_192) | ~member(U_193, Z_1091, W_192) | ~member(U_193, Y_1098, W_192) | ~member(U_193, X_1104, W_192) | ~member(U_193, V_1096, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1695, plain, (![Z_1136, Z_1106, Z_1118, X2_1105, X_1139, Z_194, V_199, U_1115, X1_1131, X2_1127, X2_196, V_1138, X1_1110, V_1109, X1_1129, V_1116, Z_1120, W_192, V_1137, X1_1117, V_1126, Y_1121, X1_195, X_1108, X2_1133, X2_1111, X2_1135, X_1114, Y_1134, X_197, Y_198, X1_1125, Z_1107, Y_1112, Y_1130, U_193, X_1113, Y_1128, X_1132, W_1119]: (skf25(V_1138, X_1132, Y_1112, Z_1136, X1_1117, X2_1135, W_192, U_193)=skf25(V_1116, X_1108, Y_1121, Z_1107, X1_1125, X2_1111, W_192, U_193) | skf25(V_1138, X_1132, Y_1112, Z_1136, X1_1117, X2_1135, W_192, U_193)=skf25(V_1137, X_1114, Y_1130, Z_1118, X1_1129, X2_1127, W_192, U_193) | skf25(V_1137, X_1114, Y_1130, Z_1118, X1_1129, X2_1127, W_192, U_193)=skf25(V_1116, X_1108, Y_1121, Z_1107, X1_1125, X2_1111, W_192, U_193) | skf25(V_1137, X_1114, Y_1130, Z_1118, X1_1129, X2_1127, W_192, U_193)=skf25(V_1126, X_1139, Y_1128, Z_1120, X1_1110, X2_1105, W_192, U_193) | skf25(V_1138, X_1132, Y_1112, Z_1136, X1_1117, X2_1135, W_192, U_193)=skf25(V_1126, X_1139, Y_1128, Z_1120, X1_1110, X2_1105, W_192, U_193) | skf25(V_1126, X_1139, Y_1128, Z_1120, X1_1110, X2_1105, W_192, U_193)=skf25(V_1116, X_1108, Y_1121, Z_1107, X1_1125, X2_1111, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1126, X_1139, Y_1128, Z_1120, X1_1110, X2_1105, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1137, X_1114, Y_1130, Z_1118, X1_1129, X2_1127, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1138, X_1132, Y_1112, Z_1136, X1_1117, X2_1135, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1116, X_1108, Y_1121, Z_1107, X1_1125, X2_1111, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_1115 | skf25(V_1126, X_1139, Y_1128, Z_1120, X1_1110, X2_1105, W_192, U_193)=U_1115 | skf25(V_1137, X_1114, Y_1130, Z_1118, X1_1129, X2_1127, W_192, U_193)=U_1115 | skf25(V_1138, X_1132, Y_1112, Z_1136, X1_1117, X2_1135, W_192, U_193)=U_1115 | skf25(V_1116, X_1108, Y_1121, Z_1107, X1_1125, X2_1111, W_192, U_193)=U_1115 | ~member(U_193, U_1115, W_192) | skf25(U_1115, V_1109, W_1119, X_1113, Y_1134, Z_1106, X1_1131, X2_1133)!=U_1115 | X2_1111=X1_1125 | Z_1107=X1_1125 | Z_1107=X2_1111 | Z_1107=Y_1121 | Y_1121=X1_1125 | Y_1121=X2_1111 | Y_1121=X_1108 | Z_1107=X_1108 | X_1108=X1_1125 | X_1108=X2_1111 | X_1108=V_1116 | Y_1121=V_1116 | Z_1107=V_1116 | X1_1125=V_1116 | X2_1111=V_1116 | ~member(U_193, X2_1111, W_192) | ~member(U_193, X1_1125, W_192) | ~member(U_193, Z_1107, W_192) | ~member(U_193, Y_1121, W_192) | ~member(U_193, X_1108, W_192) | ~member(U_193, V_1116, W_192) | X2_1135=X1_1117 | Z_1136=X1_1117 | Z_1136=X2_1135 | Z_1136=Y_1112 | Y_1112=X1_1117 | Y_1112=X2_1135 | Y_1112=X_1132 | Z_1136=X_1132 | X_1132=X1_1117 | X_1132=X2_1135 | X_1132=V_1138 | Y_1112=V_1138 | Z_1136=V_1138 | X1_1117=V_1138 | X2_1135=V_1138 | ~member(U_193, X2_1135, W_192) | ~member(U_193, X1_1117, W_192) | ~member(U_193, Z_1136, W_192) | ~member(U_193, Y_1112, W_192) | ~member(U_193, X_1132, W_192) | ~member(U_193, V_1138, W_192) | X2_1127=X1_1129 | Z_1118=X1_1129 | Z_1118=X2_1127 | Z_1118=Y_1130 | Y_1130=X1_1129 | Y_1130=X2_1127 | Y_1130=X_1114 | Z_1118=X_1114 | X_1114=X1_1129 | X_1114=X2_1127 | X_1114=V_1137 | Y_1130=V_1137 | Z_1118=V_1137 | X1_1129=V_1137 | X2_1127=V_1137 | ~member(U_193, X2_1127, W_192) | ~member(U_193, X1_1129, W_192) | ~member(U_193, Z_1118, W_192) | ~member(U_193, Y_1130, W_192) | ~member(U_193, X_1114, W_192) | ~member(U_193, V_1137, W_192) | X2_1105=X1_1110 | Z_1120=X1_1110 | Z_1120=X2_1105 | Z_1120=Y_1128 | Y_1128=X1_1110 | Y_1128=X2_1105 | Y_1128=X_1139 | Z_1120=X_1139 | X_1139=X1_1110 | X_1139=X2_1105 | X_1139=V_1126 | Y_1128=V_1126 | Z_1120=V_1126 | X1_1110=V_1126 | X2_1105=V_1126 | ~member(U_193, X2_1105, W_192) | ~member(U_193, X1_1110, W_192) | ~member(U_193, Z_1120, W_192) | ~member(U_193, Y_1128, W_192) | ~member(U_193, X_1139, W_192) | ~member(U_193, V_1126, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1650, plain, (![V_1033, Z_1031, Y_1032, V_1034, Z_194, Z_1027, V_199, Y_1022, X2_196, X1_1025, X_1036, V_1026, Y_1041, X1_1020, X2_1039, W_192, X2_1017, X1_1035, X_1037, X1_195, X_1040, U_1042, Z_1018, V_1030, X2_1038, X_197, Y_198, X_1043, U_193, Z_1021, X2_1024, X1_1019, Y_1023]: (skf25(V_1033, X_1040, Y_1022, Z_1021, X1_1019, X2_1024, W_192, U_193)=skf25(V_1026, X_1036, Y_1041, Z_1031, X1_1025, X2_1039, W_192, U_193) | skf25(V_1033, X_1040, Y_1022, Z_1021, X1_1019, X2_1024, W_192, U_193)=skf25(V_1030, X_1043, Y_1032, Z_1027, X1_1020, X2_1017, W_192, U_193) | skf25(V_1030, X_1043, Y_1032, Z_1027, X1_1020, X2_1017, W_192, U_193)=skf25(V_1026, X_1036, Y_1041, Z_1031, X1_1025, X2_1039, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1030, X_1043, Y_1032, Z_1027, X1_1020, X2_1017, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1033, X_1040, Y_1022, Z_1021, X1_1019, X2_1024, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1026, X_1036, Y_1041, Z_1031, X1_1025, X2_1039, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_1034 | skf25(V_1030, X_1043, Y_1032, Z_1027, X1_1020, X2_1017, W_192, U_193)=V_1034 | skf25(V_1033, X_1040, Y_1022, Z_1021, X1_1019, X2_1024, W_192, U_193)=V_1034 | skf25(V_1026, X_1036, Y_1041, Z_1031, X1_1025, X2_1039, W_192, U_193)=V_1034 | V_1034=U_1042 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_1042 | skf25(V_1030, X_1043, Y_1032, Z_1027, X1_1020, X2_1017, W_192, U_193)=U_1042 | skf25(V_1033, X_1040, Y_1022, Z_1021, X1_1019, X2_1024, W_192, U_193)=U_1042 | skf25(V_1026, X_1036, Y_1041, Z_1031, X1_1025, X2_1039, W_192, U_193)=U_1042 | ~member(U_193, V_1034, W_192) | ~member(U_193, U_1042, W_192) | skf25(U_1042, V_1034, skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_1037, Y_1023, Z_1018, X1_1035, X2_1038)!=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_1039=X1_1025 | Z_1031=X1_1025 | Z_1031=X2_1039 | Z_1031=Y_1041 | Y_1041=X1_1025 | Y_1041=X2_1039 | Y_1041=X_1036 | Z_1031=X_1036 | X_1036=X1_1025 | X_1036=X2_1039 | X_1036=V_1026 | Y_1041=V_1026 | Z_1031=V_1026 | X1_1025=V_1026 | X2_1039=V_1026 | ~member(U_193, X2_1039, W_192) | ~member(U_193, X1_1025, W_192) | ~member(U_193, Z_1031, W_192) | ~member(U_193, Y_1041, W_192) | ~member(U_193, X_1036, W_192) | ~member(U_193, V_1026, W_192) | X2_1024=X1_1019 | Z_1021=X1_1019 | Z_1021=X2_1024 | Z_1021=Y_1022 | Y_1022=X1_1019 | Y_1022=X2_1024 | Y_1022=X_1040 | Z_1021=X_1040 | X_1040=X1_1019 | X_1040=X2_1024 | X_1040=V_1033 | Y_1022=V_1033 | Z_1021=V_1033 | X1_1019=V_1033 | X2_1024=V_1033 | ~member(U_193, X2_1024, W_192) | ~member(U_193, X1_1019, W_192) | ~member(U_193, Z_1021, W_192) | ~member(U_193, Y_1022, W_192) | ~member(U_193, X_1040, W_192) | ~member(U_193, V_1033, W_192) | X2_1017=X1_1020 | Z_1027=X1_1020 | Z_1027=X2_1017 | Z_1027=Y_1032 | Y_1032=X1_1020 | Y_1032=X2_1017 | Y_1032=X_1043 | Z_1027=X_1043 | X_1043=X1_1020 | X_1043=X2_1017 | X_1043=V_1030 | Y_1032=V_1030 | Z_1027=V_1030 | X1_1020=V_1030 | X2_1017=V_1030 | ~member(U_193, X2_1017, W_192) | ~member(U_193, X1_1020, W_192) | ~member(U_193, Z_1027, W_192) | ~member(U_193, Y_1032, W_192) | ~member(U_193, X_1043, W_192) | ~member(U_193, V_1030, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1628, plain, (![X2_994, U_996, X_1009, X1_1007, Z_194, V_199, V_999, V_1005, Y_1006, X2_196, Y_1013, X1_991, X2_989, V_998, X_1015, Z_1001, W_192, Z_1000, Z_1008, W_1010, X1_195, X_1014, V_986, X1_1011, X_197, Y_198, Z_995, X2_1002, U_193, Y_988, Y_1012, X1_993, X5_992, X_997, X2_987]: (skf25(V_999, X_1014, Y_988, Z_995, X1_1011, X2_1002, W_192, U_193)=skf25(V_998, X_1009, Y_1012, Z_1008, X1_1007, X2_989, W_192, U_193) | skf25(V_999, X_1014, Y_988, Z_995, X1_1011, X2_1002, W_192, U_193)=skf25(V_1005, X_1015, Y_1006, Z_1001, X1_991, X2_987, W_192, U_193) | skf25(V_998, X_1009, Y_1012, Z_1008, X1_1007, X2_989, W_192, U_193)=skf25(V_1005, X_1015, Y_1006, Z_1001, X1_991, X2_987, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=skf25(V_1005, X_1015, Y_1006, Z_1001, X1_991, X2_987, W_192, U_193) | skf25(V_999, X_1014, Y_988, Z_995, X1_1011, X2_1002, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_998, X_1009, Y_1012, Z_1008, X1_1007, X2_989, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_992 | skf25(V_1005, X_1015, Y_1006, Z_1001, X1_991, X2_987, W_192, U_193)=X5_992 | skf25(V_999, X_1014, Y_988, Z_995, X1_1011, X2_1002, W_192, U_193)=X5_992 | skf25(V_998, X_1009, Y_1012, Z_1008, X1_1007, X2_989, W_192, U_193)=X5_992 | X5_992=U_996 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_996 | skf25(V_1005, X_1015, Y_1006, Z_1001, X1_991, X2_987, W_192, U_193)=U_996 | skf25(V_999, X_1014, Y_988, Z_995, X1_1011, X2_1002, W_192, U_193)=U_996 | skf25(V_998, X_1009, Y_1012, Z_1008, X1_1007, X2_989, W_192, U_193)=U_996 | ~member(U_193, X5_992, W_192) | ~member(U_193, U_996, W_192) | skf25(U_996, V_986, W_1010, X_997, Y_1013, Z_1000, X1_993, X2_994)!=U_996 | X2_989=X1_1007 | Z_1008=X1_1007 | Z_1008=X2_989 | Z_1008=Y_1012 | Y_1012=X1_1007 | Y_1012=X2_989 | Y_1012=X_1009 | Z_1008=X_1009 | X_1009=X1_1007 | X_1009=X2_989 | X_1009=V_998 | Y_1012=V_998 | Z_1008=V_998 | X1_1007=V_998 | X2_989=V_998 | ~member(U_193, X2_989, W_192) | ~member(U_193, X1_1007, W_192) | ~member(U_193, Z_1008, W_192) | ~member(U_193, Y_1012, W_192) | ~member(U_193, X_1009, W_192) | ~member(U_193, V_998, W_192) | X2_1002=X1_1011 | Z_995=X1_1011 | Z_995=X2_1002 | Z_995=Y_988 | Y_988=X1_1011 | Y_988=X2_1002 | Y_988=X_1014 | Z_995=X_1014 | X_1014=X1_1011 | X_1014=X2_1002 | X_1014=V_999 | Y_988=V_999 | Z_995=V_999 | X1_1011=V_999 | X2_1002=V_999 | ~member(U_193, X2_1002, W_192) | ~member(U_193, X1_1011, W_192) | ~member(U_193, Z_995, W_192) | ~member(U_193, Y_988, W_192) | ~member(U_193, X_1014, W_192) | ~member(U_193, V_999, W_192) | X2_987=X1_991 | Z_1001=X1_991 | Z_1001=X2_987 | Z_1001=Y_1006 | Y_1006=X1_991 | Y_1006=X2_987 | Y_1006=X_1015 | Z_1001=X_1015 | X_1015=X1_991 | X_1015=X2_987 | X_1015=V_1005 | Y_1006=V_1005 | Z_1001=V_1005 | X1_991=V_1005 | X2_987=V_1005 | ~member(U_193, X2_987, W_192) | ~member(U_193, X1_991, W_192) | ~member(U_193, Z_1001, W_192) | ~member(U_193, Y_1006, W_192) | ~member(U_193, X_1015, W_192) | ~member(U_193, V_1005, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1606, plain, (![X2_959, X_985, Y_981, X_963, X1_971, Z_194, V_199, W_975, X2_196, X_967, Y_958, X1_980, V_957, Y_984, X2_960, V_961, V_979, X_968, Z_970, X1_962, W_192, X1_195, Y_983, V_976, U_972, Z_982, Z_974, X2_965, X_197, Y_198, U_193, X2_966, X1_969, Z_973]: (skf25(V_961, X_967, Y_984, Z_974, X1_980, X2_965, W_192, U_193)=skf25(V_957, X_968, Y_983, Z_970, X1_969, X2_966, W_192, U_193) | skf25(V_979, X_985, Y_981, Z_973, X1_962, X2_960, W_192, U_193)=skf25(V_961, X_967, Y_984, Z_974, X1_980, X2_965, W_192, U_193) | skf25(V_979, X_985, Y_981, Z_973, X1_962, X2_960, W_192, U_193)=skf25(V_957, X_968, Y_983, Z_970, X1_969, X2_966, W_192, U_193) | skf25(V_979, X_985, Y_981, Z_973, X1_962, X2_960, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_961, X_967, Y_984, Z_974, X1_980, X2_965, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_957, X_968, Y_983, Z_970, X1_969, X2_966, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_976 | skf25(V_979, X_985, Y_981, Z_973, X1_962, X2_960, W_192, U_193)=V_976 | skf25(V_961, X_967, Y_984, Z_974, X1_980, X2_965, W_192, U_193)=V_976 | skf25(V_957, X_968, Y_983, Z_970, X1_969, X2_966, W_192, U_193)=V_976 | V_976=U_972 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_972 | skf25(V_979, X_985, Y_981, Z_973, X1_962, X2_960, W_192, U_193)=U_972 | skf25(V_961, X_967, Y_984, Z_974, X1_980, X2_965, W_192, U_193)=U_972 | skf25(V_957, X_968, Y_983, Z_970, X1_969, X2_966, W_192, U_193)=U_972 | ~member(U_193, V_976, W_192) | ~member(U_193, U_972, W_192) | skf25(U_972, V_976, W_975, X_963, Y_958, Z_982, X1_971, X2_959)!=V_976 | X2_966=X1_969 | Z_970=X1_969 | Z_970=X2_966 | Z_970=Y_983 | Y_983=X1_969 | Y_983=X2_966 | Y_983=X_968 | Z_970=X_968 | X_968=X1_969 | X_968=X2_966 | X_968=V_957 | Y_983=V_957 | Z_970=V_957 | X1_969=V_957 | X2_966=V_957 | ~member(U_193, X2_966, W_192) | ~member(U_193, X1_969, W_192) | ~member(U_193, Z_970, W_192) | ~member(U_193, Y_983, W_192) | ~member(U_193, X_968, W_192) | ~member(U_193, V_957, W_192) | X2_965=X1_980 | Z_974=X1_980 | Z_974=X2_965 | Z_974=Y_984 | Y_984=X1_980 | Y_984=X2_965 | Y_984=X_967 | Z_974=X_967 | X_967=X1_980 | X_967=X2_965 | X_967=V_961 | Y_984=V_961 | Z_974=V_961 | X1_980=V_961 | X2_965=V_961 | ~member(U_193, X2_965, W_192) | ~member(U_193, X1_980, W_192) | ~member(U_193, Z_974, W_192) | ~member(U_193, Y_984, W_192) | ~member(U_193, X_967, W_192) | ~member(U_193, V_961, W_192) | X2_960=X1_962 | Z_973=X1_962 | Z_973=X2_960 | Z_973=Y_981 | Y_981=X1_962 | Y_981=X2_960 | Y_981=X_985 | Z_973=X_985 | X_985=X1_962 | X_985=X2_960 | X_985=V_979 | Y_981=V_979 | Z_973=V_979 | X1_962=V_979 | X2_960=V_979 | ~member(U_193, X2_960, W_192) | ~member(U_193, X1_962, W_192) | ~member(U_193, Z_973, W_192) | ~member(U_193, Y_981, W_192) | ~member(U_193, X_985, W_192) | ~member(U_193, V_979, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1561, plain, (![Z_194, Y_910, V_199, X_911, X2_196, V_906, X1_890, Z_909, X_897, X2_892, W_905, W_192, X1_894, X1_195, X2_908, Z_893, Y_904, V_903, X_197, Y_198, X2_891, U_193, X1_895, V_896, U_898, Z_899, Y_907]: (skf25(V_906, X_897, Y_907, Z_893, X1_895, X2_892, W_192, U_193)=skf25(V_903, X_911, Y_904, Z_899, X1_894, X2_891, W_192, U_193) | skf25(V_903, X_911, Y_904, Z_899, X1_894, X2_891, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_906, X_897, Y_907, Z_893, X1_895, X2_892, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_905 | skf25(V_903, X_911, Y_904, Z_899, X1_894, X2_891, W_192, U_193)=W_905 | skf25(V_906, X_897, Y_907, Z_893, X1_895, X2_892, W_192, U_193)=W_905 | W_905=V_896 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_896 | skf25(V_903, X_911, Y_904, Z_899, X1_894, X2_891, W_192, U_193)=V_896 | skf25(V_906, X_897, Y_907, Z_893, X1_895, X2_892, W_192, U_193)=V_896 | V_896=U_898 | W_905=U_898 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_898 | skf25(V_903, X_911, Y_904, Z_899, X1_894, X2_891, W_192, U_193)=U_898 | skf25(V_906, X_897, Y_907, Z_893, X1_895, X2_892, W_192, U_193)=U_898 | ~member(U_193, W_905, W_192) | ~member(U_193, V_896, W_192) | ~member(U_193, U_898, W_192) | skf25(U_898, V_896, W_905, skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_910, Z_909, X1_890, X2_908)!=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_892=X1_895 | Z_893=X1_895 | Z_893=X2_892 | Z_893=Y_907 | Y_907=X1_895 | Y_907=X2_892 | Y_907=X_897 | Z_893=X_897 | X_897=X1_895 | X_897=X2_892 | X_897=V_906 | Y_907=V_906 | Z_893=V_906 | X1_895=V_906 | X2_892=V_906 | ~member(U_193, X2_892, W_192) | ~member(U_193, X1_895, W_192) | ~member(U_193, Z_893, W_192) | ~member(U_193, Y_907, W_192) | ~member(U_193, X_897, W_192) | ~member(U_193, V_906, W_192) | X2_891=X1_894 | Z_899=X1_894 | Z_899=X2_891 | Z_899=Y_904 | Y_904=X1_894 | Y_904=X2_891 | Y_904=X_911 | Z_899=X_911 | X_911=X1_894 | X_911=X2_891 | X_911=V_903 | Y_904=V_903 | Z_899=V_903 | X1_894=V_903 | X2_891=V_903 | ~member(U_193, X2_891, W_192) | ~member(U_193, X1_894, W_192) | ~member(U_193, Z_899, W_192) | ~member(U_193, Y_904, W_192) | ~member(U_193, X_911, W_192) | ~member(U_193, V_903, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1539, plain, (![X1_879, X1_874, Z_880, V_883, Z_194, X2_871, V_199, X_887, U_886, Y_875, V_873, X2_196, V_876, X2_885, X2_869, Y_884, X_889, Y_867, X_868, W_192, X1_872, X1_195, Z_870, X_197, Y_198, U_193, Z_877, W_888]: (skf25(V_883, X_889, Y_884, Z_880, X1_872, X2_869, W_192, U_193)=skf25(V_876, X_868, Y_875, Z_877, X1_874, X2_871, W_192, U_193) | skf25(V_883, X_889, Y_884, Z_880, X1_872, X2_869, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_876, X_868, Y_875, Z_877, X1_874, X2_871, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_888 | skf25(V_883, X_889, Y_884, Z_880, X1_872, X2_869, W_192, U_193)=W_888 | skf25(V_876, X_868, Y_875, Z_877, X1_874, X2_871, W_192, U_193)=W_888 | W_888=V_873 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_873 | skf25(V_883, X_889, Y_884, Z_880, X1_872, X2_869, W_192, U_193)=V_873 | skf25(V_876, X_868, Y_875, Z_877, X1_874, X2_871, W_192, U_193)=V_873 | V_873=U_886 | W_888=U_886 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_886 | skf25(V_883, X_889, Y_884, Z_880, X1_872, X2_869, W_192, U_193)=U_886 | skf25(V_876, X_868, Y_875, Z_877, X1_874, X2_871, W_192, U_193)=U_886 | ~member(U_193, W_888, W_192) | ~member(U_193, V_873, W_192) | ~member(U_193, U_886, W_192) | skf25(U_886, V_873, W_888, X_887, Y_867, Z_870, X1_879, X2_885)!=W_888 | X2_871=X1_874 | Z_877=X1_874 | Z_877=X2_871 | Z_877=Y_875 | Y_875=X1_874 | Y_875=X2_871 | Y_875=X_868 | Z_877=X_868 | X_868=X1_874 | X_868=X2_871 | X_868=V_876 | Y_875=V_876 | Z_877=V_876 | X1_874=V_876 | X2_871=V_876 | ~member(U_193, X2_871, W_192) | ~member(U_193, X1_874, W_192) | ~member(U_193, Z_877, W_192) | ~member(U_193, Y_875, W_192) | ~member(U_193, X_868, W_192) | ~member(U_193, V_876, W_192) | X2_869=X1_872 | Z_880=X1_872 | Z_880=X2_869 | Z_880=Y_884 | Y_884=X1_872 | Y_884=X2_869 | Y_884=X_889 | Z_880=X_889 | X_889=X1_872 | X_889=X2_869 | X_889=V_883 | Y_884=V_883 | Z_880=V_883 | X1_872=V_883 | X2_869=V_883 | ~member(U_193, X2_869, W_192) | ~member(U_193, X1_872, W_192) | ~member(U_193, Z_880, W_192) | ~member(U_193, Y_884, W_192) | ~member(U_193, X_889, W_192) | ~member(U_193, V_883, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1517, plain, (![X6_848, X_866, X2_860, Y_862, Z_194, V_199, V_850, Y_852, X1_847, V_865, Z_851, X2_196, Z_853, X5_861, X_842, Y_858, X2_859, U_844, V_856, W_192, X1_195, X_849, Z_845, W_863, X1_857, X_197, Y_198, U_193, X2_843, X1_846]: (skf25(V_865, X_849, Y_862, Z_845, X1_857, X2_860, W_192, U_193)=skf25(V_856, X_866, Y_858, Z_853, X1_846, X2_843, W_192, U_193) | skf25(V_856, X_866, Y_858, Z_853, X1_846, X2_843, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_865, X_849, Y_862, Z_845, X1_857, X2_860, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_848 | skf25(V_856, X_866, Y_858, Z_853, X1_846, X2_843, W_192, U_193)=X6_848 | skf25(V_865, X_849, Y_862, Z_845, X1_857, X2_860, W_192, U_193)=X6_848 | X6_848=X5_861 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_861 | skf25(V_856, X_866, Y_858, Z_853, X1_846, X2_843, W_192, U_193)=X5_861 | skf25(V_865, X_849, Y_862, Z_845, X1_857, X2_860, W_192, U_193)=X5_861 | X5_861=U_844 | X6_848=U_844 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_844 | skf25(V_856, X_866, Y_858, Z_853, X1_846, X2_843, W_192, U_193)=U_844 | skf25(V_865, X_849, Y_862, Z_845, X1_857, X2_860, W_192, U_193)=U_844 | ~member(U_193, X6_848, W_192) | ~member(U_193, X5_861, W_192) | ~member(U_193, U_844, W_192) | skf25(U_844, V_850, W_863, X_842, Y_852, Z_851, X1_847, X2_859)!=U_844 | X2_860=X1_857 | Z_845=X1_857 | Z_845=X2_860 | Z_845=Y_862 | Y_862=X1_857 | Y_862=X2_860 | Y_862=X_849 | Z_845=X_849 | X_849=X1_857 | X_849=X2_860 | X_849=V_865 | Y_862=V_865 | Z_845=V_865 | X1_857=V_865 | X2_860=V_865 | ~member(U_193, X2_860, W_192) | ~member(U_193, X1_857, W_192) | ~member(U_193, Z_845, W_192) | ~member(U_193, Y_862, W_192) | ~member(U_193, X_849, W_192) | ~member(U_193, V_865, W_192) | X2_843=X1_846 | Z_853=X1_846 | Z_853=X2_843 | Z_853=Y_858 | Y_858=X1_846 | Y_858=X2_843 | Y_858=X_866 | Z_853=X_866 | X_866=X1_846 | X_866=X2_843 | X_866=V_856 | Y_858=V_856 | Z_853=V_856 | X1_846=V_856 | X2_843=V_856 | ~member(U_193, X2_843, W_192) | ~member(U_193, X1_846, W_192) | ~member(U_193, Z_853, W_192) | ~member(U_193, Y_858, W_192) | ~member(U_193, X_866, W_192) | ~member(U_193, V_856, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1583, plain, (![X2_933, X1_915, X5_921, Z_194, W_917, V_199, X2_914, X2_196, Y_922, V_912, Z_927, X1_930, X_932, V_926, W_192, X1_913, X1_195, Y_928, V_920, X_935, Z_923, X_918, X_197, Y_198, U_931, Y_919, U_193, Z_929, X2_916]: (skf25(V_926, X_935, Y_928, Z_923, X1_915, X2_914, W_192, U_193)=skf25(V_920, X_918, Y_922, Z_927, X1_930, X2_916, W_192, U_193) | skf25(V_926, X_935, Y_928, Z_923, X1_915, X2_914, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_920, X_918, Y_922, Z_927, X1_930, X2_916, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_921 | skf25(V_926, X_935, Y_928, Z_923, X1_915, X2_914, W_192, U_193)=X5_921 | skf25(V_920, X_918, Y_922, Z_927, X1_930, X2_916, W_192, U_193)=X5_921 | X5_921=V_912 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_912 | skf25(V_926, X_935, Y_928, Z_923, X1_915, X2_914, W_192, U_193)=V_912 | skf25(V_920, X_918, Y_922, Z_927, X1_930, X2_916, W_192, U_193)=V_912 | V_912=U_931 | X5_921=U_931 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_931 | skf25(V_926, X_935, Y_928, Z_923, X1_915, X2_914, W_192, U_193)=U_931 | skf25(V_920, X_918, Y_922, Z_927, X1_930, X2_916, W_192, U_193)=U_931 | ~member(U_193, X5_921, W_192) | ~member(U_193, V_912, W_192) | ~member(U_193, U_931, W_192) | skf25(U_931, V_912, W_917, X_932, Y_919, Z_929, X1_913, X2_933)!=V_912 | X2_916=X1_930 | Z_927=X1_930 | Z_927=X2_916 | Z_927=Y_922 | Y_922=X1_930 | Y_922=X2_916 | Y_922=X_918 | Z_927=X_918 | X_918=X1_930 | X_918=X2_916 | X_918=V_920 | Y_922=V_920 | Z_927=V_920 | X1_930=V_920 | X2_916=V_920 | ~member(U_193, X2_916, W_192) | ~member(U_193, X1_930, W_192) | ~member(U_193, Z_927, W_192) | ~member(U_193, Y_922, W_192) | ~member(U_193, X_918, W_192) | ~member(U_193, V_920, W_192) | X2_914=X1_915 | Z_923=X1_915 | Z_923=X2_914 | Z_923=Y_928 | Y_928=X1_915 | Y_928=X2_914 | Y_928=X_935 | Z_923=X_935 | X_935=X1_915 | X_935=X2_914 | X_935=V_926 | Y_928=V_926 | Z_923=V_926 | X1_915=V_926 | X2_914=V_926 | ~member(U_193, X2_914, W_192) | ~member(U_193, X1_915, W_192) | ~member(U_193, Z_923, W_192) | ~member(U_193, Y_928, W_192) | ~member(U_193, X_935, W_192) | ~member(U_193, V_926, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.95 tff(c_1472, plain, (![X1_797, X2_791, Z_194, V_199, Y_799, X2_196, X_793, Z_805, W_796, X2_792, W_192, X1_195, X1_801, Z_803, X_197, Y_198, U_795, V_802, U_193, V_806, X_800]: (skf25(V_802, X_800, Y_799, Z_803, X1_797, X2_792, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_793 | skf25(V_802, X_800, Y_799, Z_803, X1_797, X2_792, W_192, U_193)=X_793 | X_793=W_796 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_796 | skf25(V_802, X_800, Y_799, Z_803, X1_797, X2_792, W_192, U_193)=W_796 | W_796=V_806 | X_793=V_806 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_806 | skf25(V_802, X_800, Y_799, Z_803, X1_797, X2_792, W_192, U_193)=V_806 | V_806=U_795 | W_796=U_795 | X_793=U_795 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_795 | skf25(V_802, X_800, Y_799, Z_803, X1_797, X2_792, W_192, U_193)=U_795 | ~member(U_193, X_793, W_192) | ~member(U_193, W_796, W_192) | ~member(U_193, V_806, W_192) | ~member(U_193, U_795, W_192) | skf25(U_795, V_806, W_796, X_793, skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_805, X1_801, X2_791)!=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_792=X1_797 | Z_803=X1_797 | Z_803=X2_792 | Z_803=Y_799 | Y_799=X1_797 | Y_799=X2_792 | Y_799=X_800 | Z_803=X_800 | X_800=X1_797 | X_800=X2_792 | X_800=V_802 | Y_799=V_802 | Z_803=V_802 | X1_797=V_802 | X2_792=V_802 | ~member(U_193, X2_792, W_192) | ~member(U_193, X1_797, W_192) | ~member(U_193, Z_803, W_192) | ~member(U_193, Y_799, W_192) | ~member(U_193, X_800, W_192) | ~member(U_193, V_802, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_1406, plain, (![Z_750, X2_739, Z_194, V_199, U_752, Y_754, X2_196, Z_748, X1_755, W_746, X_747, X5_742, W_192, X6_738, X1_195, V_744, X_745, V_749, X2_737, Y_743, X_197, Y_198, X1_741, U_193]: (skf25(V_749, X_747, Y_743, Z_750, X1_741, X2_739, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_738 | skf25(V_749, X_747, Y_743, Z_750, X1_741, X2_739, W_192, U_193)=X6_738 | X6_738=X5_742 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_742 | skf25(V_749, X_747, Y_743, Z_750, X1_741, X2_739, W_192, U_193)=X5_742 | X5_742=V_744 | X6_738=V_744 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_744 | skf25(V_749, X_747, Y_743, Z_750, X1_741, X2_739, W_192, U_193)=V_744 | V_744=U_752 | X5_742=U_752 | X6_738=U_752 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_752 | skf25(V_749, X_747, Y_743, Z_750, X1_741, X2_739, W_192, U_193)=U_752 | ~member(U_193, X6_738, W_192) | ~member(U_193, X5_742, W_192) | ~member(U_193, V_744, W_192) | ~member(U_193, U_752, W_192) | skf25(U_752, V_744, W_746, X_745, Y_754, Z_748, X1_755, X2_737)!=V_744 | X2_739=X1_741 | Z_750=X1_741 | Z_750=X2_739 | Z_750=Y_743 | Y_743=X1_741 | Y_743=X2_739 | Y_743=X_747 | Z_750=X_747 | X_747=X1_741 | X_747=X2_739 | X_747=V_749 | Y_743=V_749 | Z_750=V_749 | X1_741=V_749 | X2_739=V_749 | ~member(U_193, X2_739, W_192) | ~member(U_193, X1_741, W_192) | ~member(U_193, Z_750, W_192) | ~member(U_193, Y_743, W_192) | ~member(U_193, X_747, W_192) | ~member(U_193, V_749, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_1428, plain, (![X1_764, Z_194, V_770, V_199, X2_196, W_767, X_759, X_769, Z_756, X2_758, V_766, W_192, Y_757, X1_195, Y_765, X2_760, X_197, Y_198, X1_763, U_193, Z_771, U_762]: (skf25(V_770, X_769, Y_765, Z_771, X1_763, X2_758, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_759 | skf25(V_770, X_769, Y_765, Z_771, X1_763, X2_758, W_192, U_193)=X_759 | X_759=W_767 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_767 | skf25(V_770, X_769, Y_765, Z_771, X1_763, X2_758, W_192, U_193)=W_767 | W_767=V_766 | X_759=V_766 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_766 | skf25(V_770, X_769, Y_765, Z_771, X1_763, X2_758, W_192, U_193)=V_766 | V_766=U_762 | W_767=U_762 | X_759=U_762 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_762 | skf25(V_770, X_769, Y_765, Z_771, X1_763, X2_758, W_192, U_193)=U_762 | ~member(U_193, X_759, W_192) | ~member(U_193, W_767, W_192) | ~member(U_193, V_766, W_192) | ~member(U_193, U_762, W_192) | skf25(U_762, V_766, W_767, X_759, Y_757, Z_756, X1_764, X2_760)!=X_759 | X2_758=X1_763 | Z_771=X1_763 | Z_771=X2_758 | Z_771=Y_765 | Y_765=X1_763 | Y_765=X2_758 | Y_765=X_769 | Z_771=X_769 | X_769=X1_763 | X_769=X2_758 | X_769=V_770 | Y_765=V_770 | Z_771=V_770 | X1_763=V_770 | X2_758=V_770 | ~member(U_193, X2_758, W_192) | ~member(U_193, X1_763, W_192) | ~member(U_193, Z_771, W_192) | ~member(U_193, Y_765, W_192) | ~member(U_193, X_769, W_192) | ~member(U_193, V_770, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_1450, plain, (![X1_773, X5_789, X_788, Z_194, V_199, Y_790, X1_777, X2_196, W_778, Z_786, X2_779, V_784, W_192, Z_774, X1_195, V_785, Y_780, X_197, Y_198, X2_775, U_193, X_783, U_781]: (skf25(V_785, X_783, Y_780, Z_786, X1_777, X2_775, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_789 | skf25(V_785, X_783, Y_780, Z_786, X1_777, X2_775, W_192, U_193)=X5_789 | X5_789=W_778 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_778 | skf25(V_785, X_783, Y_780, Z_786, X1_777, X2_775, W_192, U_193)=W_778 | W_778=V_784 | X5_789=V_784 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_784 | skf25(V_785, X_783, Y_780, Z_786, X1_777, X2_775, W_192, U_193)=V_784 | V_784=U_781 | W_778=U_781 | X5_789=U_781 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_781 | skf25(V_785, X_783, Y_780, Z_786, X1_777, X2_775, W_192, U_193)=U_781 | ~member(U_193, X5_789, W_192) | ~member(U_193, W_778, W_192) | ~member(U_193, V_784, W_192) | ~member(U_193, U_781, W_192) | skf25(U_781, V_784, W_778, X_788, Y_790, Z_774, X1_773, X2_779)!=W_778 | X2_775=X1_777 | Z_786=X1_777 | Z_786=X2_775 | Z_786=Y_780 | Y_780=X1_777 | Y_780=X2_775 | Y_780=X_783 | Z_786=X_783 | X_783=X1_777 | X_783=X2_775 | X_783=V_785 | Y_780=V_785 | Z_786=V_785 | X1_777=V_785 | X2_775=V_785 | ~member(U_193, X2_775, W_192) | ~member(U_193, X1_777, W_192) | ~member(U_193, Z_786, W_192) | ~member(U_193, Y_780, W_192) | ~member(U_193, X_783, W_192) | ~member(U_193, V_785, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_1494, plain, (![X_814, X5_825, X6_824, Z_194, Y_818, V_199, X1_820, Y_813, X2_196, X_819, W_809, U_826, X2_808, V_816, V_821, X2_815, Z_822, W_192, X1_195, X1_812, X7_807, X_197, Y_198, U_193, Z_817]: (skf25(V_821, X_819, Y_813, Z_822, X1_812, X2_808, W_192, U_193)=skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X7_807 | skf25(V_821, X_819, Y_813, Z_822, X1_812, X2_808, W_192, U_193)=X7_807 | X7_807=X6_824 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_824 | skf25(V_821, X_819, Y_813, Z_822, X1_812, X2_808, W_192, U_193)=X6_824 | X6_824=X5_825 | X7_807=X5_825 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_825 | skf25(V_821, X_819, Y_813, Z_822, X1_812, X2_808, W_192, U_193)=X5_825 | X5_825=U_826 | X6_824=U_826 | X7_807=U_826 | skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_826 | skf25(V_821, X_819, Y_813, Z_822, X1_812, X2_808, W_192, U_193)=U_826 | ~member(U_193, X7_807, W_192) | ~member(U_193, X6_824, W_192) | ~member(U_193, X5_825, W_192) | ~member(U_193, U_826, W_192) | skf25(U_826, V_816, W_809, X_814, Y_818, Z_817, X1_820, X2_815)!=U_826 | X2_808=X1_812 | Z_822=X1_812 | Z_822=X2_808 | Z_822=Y_813 | Y_813=X1_812 | Y_813=X2_808 | Y_813=X_819 | Z_822=X_819 | X_819=X1_812 | X_819=X2_808 | X_819=V_821 | Y_813=V_821 | Z_822=V_821 | X1_812=V_821 | X2_808=V_821 | ~member(U_193, X2_808, W_192) | ~member(U_193, X1_812, W_192) | ~member(U_193, Z_822, W_192) | ~member(U_193, Y_813, W_192) | ~member(U_193, X_819, W_192) | ~member(U_193, V_821, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_1386, plain, (![X_206, X1_204, X1_730, W_200, V_208, X2_729, X_736, W_733, X2_205, V_734, U_202, Y_735, Y_207, U_732, Z_731]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=Y_207 | Y_207=X_206 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X_206 | X_206=W_200 | Y_207=W_200 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_202 | ~member(U_732, Y_207, W_733) | ~member(U_732, X_206, W_733) | ~member(U_732, W_200, W_733) | ~member(U_732, V_208, W_733) | ~member(U_732, U_202, W_733) | skf25(U_202, V_208, W_200, X_206, Y_207, skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732), X1_204, X2_205)!=skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732) | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_1384, plain, (![Z_183, X8_190, X1_730, X5_177, X2_729, X1_185, X_736, W_733, V_189, X_187, Y_188, V_734, U_181, X2_186, X7_184, X6_178, Y_735, W_179, U_732, Z_731]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X8_190 | X8_190=X7_184 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_181 | ~member(U_732, X8_190, W_733) | ~member(U_732, X7_184, W_733) | ~member(U_732, X6_178, W_733) | ~member(U_732, X5_177, W_733) | ~member(U_732, U_181, W_733) | skf25(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_1385, plain, (![U_130, X1_730, X2_729, X_736, W_733, X1_132, V_734, V_136, Y_135, Y_735, W_128, X2_133, U_732, Z_731, Z_131, X_134]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=Y_135 | Y_135=X_134 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X_134 | X_134=W_128 | Y_135=W_128 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_130 | ~member(U_732, Y_135, W_733) | ~member(U_732, X_134, W_733) | ~member(U_732, W_128, W_733) | ~member(U_732, V_136, W_733) | ~member(U_732, U_130, W_733) | skf25(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_1383, plain, (![X6_151, X2_158, X1_730, X2_729, Y_160, X_736, W_733, X1_157, V_734, X_159, W_152, V_161, Y_735, U_732, X5_150, Z_731, Z_155, U_154]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X6_151 | X6_151=X5_150 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_154 | ~member(U_732, X6_151, W_733) | ~member(U_732, X5_150, W_733) | ~member(U_732, W_152, W_733) | ~member(U_732, V_161, W_733) | ~member(U_732, U_154, W_733) | skf25(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_1387, plain, (![U_142, X1_730, W_140, X2_729, X2_145, X5_138, X_736, W_733, Y_147, V_148, V_734, Y_735, U_732, Z_143, X1_144, X_146, Z_731]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X5_138 | X_146=X5_138 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X_146 | X_146=W_140 | X5_138=W_140 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_142 | ~member(U_732, X5_138, W_733) | ~member(U_732, X_146, W_733) | ~member(U_732, W_140, W_733) | ~member(U_732, V_148, W_733) | ~member(U_732, U_142, W_733) | skf25(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_1382, plain, (![X1_730, X2_171, X6_164, V_174, X2_729, U_167, X_736, Z_168, W_733, V_734, W_165, Y_735, X5_163, X1_170, X7_169, U_732, X_172, Y_173, Z_731]: (skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X7_169 | X7_169=X6_164 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf25(V_734, X_736, Y_735, Z_731, X1_730, X2_729, W_733, U_732)=U_167 | ~member(U_732, X7_169, W_733) | ~member(U_732, X6_164, W_733) | ~member(U_732, X5_163, W_733) | ~member(U_732, V_174, W_733) | ~member(U_732, U_167, W_733) | skf25(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_729=X1_730 | Z_731=X1_730 | Z_731=X2_729 | Z_731=Y_735 | Y_735=X1_730 | Y_735=X2_729 | Y_735=X_736 | Z_731=X_736 | X_736=X1_730 | X_736=X2_729 | X_736=V_734 | Y_735=V_734 | Z_731=V_734 | X1_730=V_734 | X2_729=V_734 | six(U_732, W_733) | ~member(U_732, X2_729, W_733) | ~member(U_732, X1_730, W_733) | ~member(U_732, Z_731, W_733) | ~member(U_732, Y_735, W_733) | ~member(U_732, X_736, W_733) | ~member(U_732, V_734, W_733)))). % 61.90/51.96 tff(c_136, plain, (![Z_194, V_199, X2_196, W_192, X1_195, X_197, Y_198, U_193]: (X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | member(U_193, skf25(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_192) | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 61.90/51.96 tff(c_132, plain, (![X2_171, X6_164, V_174, U_167, Z_168, W_165, X5_163, X1_170, X7_169, X8_175, X_172, Y_173, X4_176, X3_166]: (X8_175=X7_169 | X7_169=X6_164 | X8_175=X6_164 | X6_164=X5_163 | X7_169=X5_163 | X8_175=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | X8_175=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | X8_175=U_167 | six(X3_166, X4_176) | ~member(X3_166, X8_175, X4_176) | ~member(X3_166, X7_169, X4_176) | ~member(X3_166, X6_164, X4_176) | ~member(X3_166, X5_163, X4_176) | ~member(X3_166, V_174, X4_176) | ~member(X3_166, U_167, X4_176) | skf25(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174))). % 61.90/51.96 tff(c_130, plain, (![X4_162, X6_151, X2_158, Y_160, X1_157, X3_153, X_159, W_152, V_161, X5_150, X7_156, Z_155, U_154]: (X7_156=X6_151 | X6_151=X5_150 | X7_156=X5_150 | X5_150=W_152 | X6_151=W_152 | X7_156=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | X7_156=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | X7_156=U_154 | six(X3_153, X4_162) | ~member(X3_153, X7_156, X4_162) | ~member(X3_153, X6_151, X4_162) | ~member(X3_153, X5_150, X4_162) | ~member(X3_153, W_152, X4_162) | ~member(X3_153, V_161, X4_162) | ~member(X3_153, U_154, X4_162) | skf25(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152))). % 61.90/51.96 tff(c_134, plain, (![Z_183, X4_191, X8_190, X5_177, X3_180, X1_185, V_189, X_187, Y_188, X9_182, U_181, X2_186, X7_184, X6_178, W_179]: (X9_182=X8_190 | X8_190=X7_184 | X9_182=X7_184 | X7_184=X6_178 | X8_190=X6_178 | X9_182=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | X9_182=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | X9_182=U_181 | six(X3_180, X4_191) | ~member(X3_180, X9_182, X4_191) | ~member(X3_180, X8_190, X4_191) | ~member(X3_180, X7_184, X4_191) | ~member(X3_180, X6_178, X4_191) | ~member(X3_180, X5_177, X4_191) | ~member(X3_180, U_181, X4_191) | skf25(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181))). % 61.90/51.96 tff(c_126, plain, (![U_130, X5_127, X1_132, V_136, Y_135, W_128, X3_129, X2_133, Z_131, X_134, X4_137]: (Y_135=X5_127 | Y_135=X_134 | X_134=X5_127 | X_134=W_128 | Y_135=W_128 | X5_127=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | X5_127=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | X5_127=U_130 | six(X3_129, X4_137) | ~member(X3_129, X5_127, X4_137) | ~member(X3_129, Y_135, X4_137) | ~member(X3_129, X_134, X4_137) | ~member(X3_129, W_128, X4_137) | ~member(X3_129, V_136, X4_137) | ~member(X3_129, U_130, X4_137) | skf25(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135))). % 61.90/51.96 tff(c_138, plain, (![X3_201, X_206, X1_204, W_200, V_208, X2_205, X4_209, U_202, Y_207, Z_203]: (Z_203=Y_207 | Y_207=X_206 | Z_203=X_206 | X_206=W_200 | Y_207=W_200 | Z_203=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | Z_203=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | Z_203=U_202 | six(X3_201, X4_209) | ~member(X3_201, Z_203, X4_209) | ~member(X3_201, Y_207, X4_209) | ~member(X3_201, X_206, X4_209) | ~member(X3_201, W_200, X4_209) | ~member(X3_201, V_208, X4_209) | ~member(X3_201, U_202, X4_209) | skf25(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Z_203))). % 61.90/51.96 tff(c_128, plain, (![U_142, W_140, X2_145, X5_138, Y_147, V_148, X3_141, Z_143, X4_149, X6_139, X1_144, X_146]: (X6_139=X5_138 | X_146=X5_138 | X_146=X6_139 | X_146=W_140 | X5_138=W_140 | X6_139=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | X6_139=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | X6_139=U_142 | six(X3_141, X4_149) | ~member(X3_141, X6_139, X4_149) | ~member(X3_141, X5_138, X4_149) | ~member(X3_141, X_146, X4_149) | ~member(X3_141, W_140, X4_149) | ~member(X3_141, V_148, X4_149) | ~member(X3_141, U_142, X4_149) | skf25(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146))). % 61.90/51.96 tff(c_124, plain, (![W_126, U_124, V_125]: (skf24(W_126, U_124)=V_125 | skf22(W_126, U_124)=V_125 | skf20(W_126, U_124)=V_125 | skf18(W_126, U_124)=V_125 | skf16(W_126, U_124)=V_125 | skf14(W_126, U_124)=V_125 | ~six(U_124, W_126) | ~member(U_124, V_125, W_126)))). % 61.90/51.96 tff(c_1215, plain, (![U_223]: (~agent(skc3, skf10(U_223), U_223) | ~member(skc3, U_223, skc4)))). % 61.90/51.96 tff(c_122, plain, (![U_121, V_122, W_123]: (~agent(U_121, V_122, W_123) | ~patient(U_121, V_122, W_123) | ~nonreflexive(U_121, V_122)))). % 61.90/51.96 tff(c_1207, plain, (![V_227]: (agent(skc3, skf10(V_227), skf12(V_227))))). % 61.90/51.96 tff(c_1175, plain, (![V_229]: (from_loc(skc3, skf10(V_229), skf11(V_229))))). % 61.90/51.96 tff(c_1144, plain, (act(skc3, skf20(skc4, skc3)))). % 61.90/51.96 tff(c_1140, plain, (action(skc3, skf20(skc4, skc3)))). % 61.90/51.96 tff(c_1136, plain, (shot(skc3, skf20(skc4, skc3)))). % 61.90/51.96 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf20(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 61.90/51.96 tff(c_1128, plain, (skf24(skc4, skc3)!=skf14(skc4, skc3))). % 61.90/51.96 tff(c_1123, plain, (skf22(skc4, skc3)!=skf14(skc4, skc3))). % 61.90/51.96 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf24(U_91, V_92)!=skf14(U_91, V_92)))). % 61.90/51.96 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf22(U_101, V_102)!=skf14(U_101, V_102)))). % 61.90/51.96 tff(c_1118, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 61.90/51.96 tff(c_1113, plain, (act(skc3, skf16(skc4, skc3)))). % 61.90/51.96 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf18(U_115, V_116)!=skf14(U_115, V_116)))). % 61.90/51.96 tff(c_1109, plain, (action(skc3, skf16(skc4, skc3)))). % 61.90/51.96 tff(c_1105, plain, (shot(skc3, skf16(skc4, skc3)))). % 61.90/51.96 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf16(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 61.90/51.96 tff(c_1097, plain, (skf22(skc4, skc3)!=skf20(skc4, skc3))). % 61.90/51.96 tff(c_1092, plain, (skf22(skc4, skc3)!=skf16(skc4, skc3))). % 61.90/51.96 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf22(U_107, V_108)!=skf20(U_107, V_108)))). % 61.90/51.96 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf22(U_103, V_104)!=skf16(U_103, V_104)))). % 61.90/51.96 tff(c_1087, plain, (skf24(skc4, skc3)!=skf22(skc4, skc3))). % 61.90/51.96 tff(c_1082, plain, (skf24(skc4, skc3)!=skf20(skc4, skc3))). % 61.90/51.96 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf24(U_99, V_100)!=skf22(U_99, V_100)))). % 61.90/51.96 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf24(U_97, V_98)!=skf20(U_97, V_98)))). % 61.90/51.96 tff(c_1069, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 61.90/51.96 tff(c_1077, plain, (act(skc3, skf24(skc4, skc3)))). % 61.90/51.96 tff(c_1073, plain, (action(skc3, skf24(skc4, skc3)))). % 61.90/51.96 tff(c_1064, plain, (shot(skc3, skf24(skc4, skc3)))). % 61.90/51.96 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf20(U_113, V_114)!=skf18(U_113, V_114)))). % 61.90/51.96 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf24(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 61.90/51.96 tff(c_1055, plain, (skf24(skc4, skc3)!=skf18(skc4, skc3))). % 61.90/51.97 tff(c_1050, plain, (![V_222]: (~act(skc3, skf11(V_222))))). % 61.90/51.97 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf24(U_95, V_96)!=skf18(U_95, V_96)))). % 61.90/51.97 tff(c_1045, plain, (![U_250, V_251]: (~act(U_250, V_251) | ~artifact(U_250, V_251)))). % 61.90/51.97 tff(c_1002, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 61.90/51.97 tff(c_1032, plain, (skf24(skc4, skc3)!=skf16(skc4, skc3))). % 61.90/51.97 tff(c_1036, plain, (~act(skc3, skc4))). % 61.90/51.97 tff(c_1027, plain, (~event(skc3, skc4))). % 61.90/51.97 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf24(U_93, V_94)!=skf16(U_93, V_94)))). % 61.90/51.97 tff(c_1023, plain, (~eventuality(skc3, skc4))). % 61.90/51.97 tff(c_910, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 61.90/51.97 tff(c_1018, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 61.90/51.97 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf18(U_117, V_118)!=skf16(U_117, V_118)))). % 61.90/51.97 tff(c_905, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 61.90/51.97 tff(c_1007, plain, (![V_604]: (~artifact(skc3, skf10(V_604))))). % 61.90/51.97 tff(c_1001, plain, (![V_220]: (~entity(skc3, skf10(V_220))))). % 61.90/51.97 tff(c_958, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 61.90/51.97 tff(c_993, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 61.90/51.97 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf20(U_111, V_112)!=skf16(U_111, V_112)))). % 61.90/51.97 tff(c_982, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 61.90/51.97 tff(c_987, plain, (![V_598]: (~animate(skc3, skf11(V_598))))). % 61.90/51.97 tff(c_977, plain, (![V_222]: (artifact(skc3, skf11(V_222))))). % 61.90/51.97 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf20(U_109, V_110)!=skf14(U_109, V_110)))). % 61.90/51.97 tff(c_933, plain, (![U_579, V_580]: (artifact(U_579, V_580) | ~cannon(U_579, V_580)))). % 61.90/51.97 tff(c_972, plain, (~artifact(skc3, skc4))). % 61.90/51.97 tff(c_968, plain, (~entity(skc3, skc4))). % 61.90/51.97 tff(c_953, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 61.90/51.97 tff(c_963, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 61.90/51.97 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf16(U_119, V_120)!=skf14(U_119, V_120)))). % 61.90/51.97 tff(c_712, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 61.90/51.97 tff(c_865, plain, (![U_558, V_559]: (~multiple(U_558, V_559) | ~entity(U_558, V_559)))). % 61.90/51.97 tff(c_948, plain, (skf22(skc4, skc3)!=skf18(skc4, skc3))). % 61.90/51.97 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf22(U_105, V_106)!=skf18(U_105, V_106)))). % 61.90/51.97 tff(c_941, plain, (![V_416]: (~artifact(skc3, skf12(V_416))))). % 61.90/51.97 tff(c_942, plain, (~artifact(skc3, skc5))). % 61.90/51.97 tff(c_830, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 61.90/51.97 tff(c_775, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 61.90/51.97 tff(c_784, plain, (![U_524, V_525]: (~animate(U_524, V_525) | ~artifact(U_524, V_525)))). % 61.90/51.97 tff(c_162, plain, (![U_223]: (patient(skc3, skf10(U_223), U_223) | ~member(skc3, U_223, skc4)))). % 61.90/51.97 tff(c_926, plain, (act(skc3, skf18(skc4, skc3)))). % 61.90/51.97 tff(c_922, plain, (action(skc3, skf18(skc4, skc3)))). % 61.90/51.97 tff(c_918, plain, (shot(skc3, skf18(skc4, skc3)))). % 61.90/51.97 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf18(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 61.90/51.97 tff(c_841, plain, (![U_548, V_549]: (~multiple(U_548, V_549) | ~eventuality(U_548, V_549)))). % 61.90/51.97 tff(c_783, plain, (![U_524, V_525]: (~living(U_524, V_525) | ~artifact(U_524, V_525)))). % 61.90/51.97 tff(c_900, plain, (act(skc3, skf22(skc4, skc3)))). % 61.90/51.97 tff(c_896, plain, (action(skc3, skf22(skc4, skc3)))). % 61.90/51.97 tff(c_892, plain, (shot(skc3, skf22(skc4, skc3)))). % 61.90/51.97 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf22(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 61.90/51.97 tff(c_884, plain, (act(skc3, skf14(skc4, skc3)))). % 61.90/51.97 tff(c_880, plain, (action(skc3, skf14(skc4, skc3)))). % 61.90/51.97 tff(c_876, plain, (shot(skc3, skf14(skc4, skc3)))). % 61.90/51.97 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf14(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 61.90/51.97 tff(c_232, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 61.90/51.97 tff(c_184, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 61.90/51.97 tff(c_261, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 61.90/51.97 tff(c_175, plain, (![U_41, V_42]: (singleton(U_41, V_42) | ~entity(U_41, V_42)))). % 61.90/51.97 tff(c_859, plain, (![V_225]: (of(skc3, skf11(V_225), skc5)))). % 61.90/51.97 tff(c_189, plain, (![U_246, V_247]: (singleton(U_246, V_247) | ~eventuality(U_246, V_247)))). % 61.90/51.97 tff(c_835, plain, (![V_416]: (entity(skc3, skf12(V_416))))). % 61.90/51.97 tff(c_239, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 61.90/51.97 tff(c_255, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 61.90/51.97 tff(c_819, plain, (![V_214]: (fire(skc3, skf10(V_214))))). % 61.90/51.97 tff(c_224, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 61.90/51.97 tff(c_210, plain, (![U_31, V_32]: (instrumentality(U_31, V_32) | ~weapon(U_31, V_32)))). % 61.90/51.97 tff(c_769, plain, (![V_216]: (nonreflexive(skc3, skf10(V_216))))). % 61.90/51.97 tff(c_195, plain, (![U_250, V_251]: (entity(U_250, V_251) | ~artifact(U_250, V_251)))). % 61.90/51.97 tff(c_202, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 61.90/51.97 tff(c_706, plain, (![V_220]: (event(skc3, skf10(V_220))))). % 61.90/51.97 tff(c_635, plain, (![V_458]: (~act(skc3, skf12(V_458))))). % 61.90/51.97 tff(c_553, plain, (![V_420]: (~event(skc3, skf12(V_420))))). % 61.90/51.97 tff(c_548, plain, (![V_419]: (animate(skc3, skf12(V_419))))). % 61.90/51.97 tff(c_547, plain, (![V_419]: (human(skc3, skf12(V_419))))). % 61.90/51.97 tff(c_627, plain, (![V_222]: (cannon(skc3, skf11(V_222))))). % 61.90/51.97 tff(c_539, plain, (![V_418]: (~eventuality(skc3, skf12(V_418))))). % 61.90/51.97 tff(c_533, plain, (![V_416]: (human_person(skc3, skf12(V_416))))). % 61.90/51.97 tff(c_532, plain, (![V_416]: (male(skc3, skf12(V_416))))). % 61.90/51.97 tff(c_524, plain, (![V_218]: (present(skc3, skf10(V_218))))). % 61.90/51.97 tff(c_421, plain, (![V_212]: (man(skc3, skf12(V_212))))). % 61.90/51.97 tff(c_279, plain, (~act(skc3, skc5))). % 61.90/51.97 tff(c_275, plain, (~event(skc3, skc5))). % 61.90/51.97 tff(c_270, plain, (~eventuality(skc3, skc5))). % 61.90/51.97 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 61.90/51.97 tff(c_256, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 61.90/51.97 tff(c_247, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 61.90/51.98 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 61.90/51.98 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 61.90/51.98 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 61.90/51.98 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 61.90/51.98 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 61.90/51.98 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 61.90/51.98 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 61.90/51.98 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 61.90/51.98 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 62.15/51.98 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 62.15/51.98 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.15/51.98 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 62.15/51.98 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 62.15/51.98 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 62.15/51.98 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 62.15/51.98 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 62.15/51.98 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 62.15/51.98 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 62.15/51.98 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 62.15/51.98 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 62.15/51.98 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 62.15/51.98 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 62.15/51.98 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 62.15/51.98 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 62.15/51.98 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 62.15/51.98 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 62.15/51.98 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 62.15/51.98 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 62.15/51.98 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.15/51.98 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 62.15/51.98 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 62.15/51.98 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 62.15/51.98 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 62.15/51.98 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 62.15/51.98 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 62.15/51.98 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 62.15/51.98 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 62.15/51.98 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 62.15/51.98 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 62.15/51.98 tff(c_142, plain, (male(skc3, skc5))). % 62.15/51.98 tff(c_144, plain, (group(skc3, skc4))). % 62.15/51.98 tff(c_146, plain, (six(skc3, skc4))). % 62.15/51.98 tff(c_140, plain, (actual_world(skc3))). % 62.15/51.98 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 62.15/51.98 %------------------------------------------------------------------------------