%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP087-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n021.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:10 PM UTC 2025 % Result : Satisfiable 68.75s 58.90s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP087-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 08:27:58 EDT 2025 % 0.14/0.34 % CPUTime : % 68.75/58.90 % 68.75/58.90 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.75/58.90 % 68.75/58.90 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.75/58.91 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > sound > six > singleton > shot > set > scream > revenge > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cry > cannon > artifact > animate > action > act > actual_world > skf21 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skf8 > skc9 > skc8 > skc7 > skc14 > skc12 > skc11 > skc10 % 68.75/58.91 % 68.75/58.91 %Foreground sorts: % 68.75/58.91 % 68.75/58.91 % 68.75/58.91 %Background operators: % 68.75/58.91 % 68.75/58.91 % 68.75/58.91 %Foreground operators: % 68.75/58.91 tff(nonliving, type, nonliving: ($i * $i) > $o). % 68.75/58.91 tff(skf10, type, skf10: ($i * $i) > $i). % 68.75/58.91 tff(member, type, member: ($i * $i * $i) > $o). % 68.75/58.91 tff(skc7, type, skc7: $i). % 68.75/58.91 tff(living, type, living: ($i * $i) > $o). % 68.75/58.91 tff(fire, type, fire: ($i * $i) > $o). % 68.75/58.91 tff(human_person, type, human_person: ($i * $i) > $o). % 68.75/58.91 tff(action, type, action: ($i * $i) > $o). % 68.75/58.91 tff(present, type, present: ($i * $i) > $o). % 68.75/58.91 tff(shot, type, shot: ($i * $i) > $o). % 68.75/58.91 tff(skc11, type, skc11: $i). % 68.75/58.91 tff(entity, type, entity: ($i * $i) > $o). % 68.75/58.91 tff(skc9, type, skc9: $i). % 68.75/58.91 tff(eventuality, type, eventuality: ($i * $i) > $o). % 68.75/58.91 tff(weapon, type, weapon: ($i * $i) > $o). % 68.75/58.91 tff(existent, type, existent: ($i * $i) > $o). % 68.75/58.91 tff(skc8, type, skc8: $i). % 68.75/58.91 tff(scream, type, scream: ($i * $i) > $o). % 68.75/58.91 tff(skc14, type, skc14: $i). % 68.75/58.91 tff(singleton, type, singleton: ($i * $i) > $o). % 68.75/58.91 tff(male, type, male: ($i * $i) > $o). % 68.75/58.91 tff(skf8, type, skf8: $i > $i). % 68.75/58.91 tff(multiple, type, multiple: ($i * $i) > $o). % 68.75/58.91 tff(organism, type, organism: ($i * $i) > $o). % 68.75/58.91 tff(animate, type, animate: ($i * $i) > $o). % 68.75/58.91 tff(of, type, of: ($i * $i * $i) > $o). % 68.75/58.91 tff(skf14, type, skf14: ($i * $i) > $i). % 68.75/58.91 tff(actual_world, type, actual_world: $i > $o). % 68.75/58.91 tff(agent, type, agent: ($i * $i * $i) > $o). % 68.75/58.91 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 68.75/58.91 tff(group, type, group: ($i * $i) > $o). % 68.75/58.91 tff(revenge, type, revenge: ($i * $i) > $o). % 68.75/58.91 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 68.75/58.91 tff(artifact, type, artifact: ($i * $i) > $o). % 68.75/58.91 tff(cannon, type, cannon: ($i * $i) > $o). % 68.75/58.91 tff(cry, type, cry: ($i * $i) > $o). % 68.75/58.91 tff(event, type, event: ($i * $i) > $o). % 68.75/58.91 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 68.75/58.91 tff(patient, type, patient: ($i * $i * $i) > $o). % 68.75/58.91 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 68.75/58.91 tff(thing, type, thing: ($i * $i) > $o). % 68.75/58.91 tff(human, type, human: ($i * $i) > $o). % 68.75/58.91 tff(six, type, six: ($i * $i) > $o). % 68.75/58.91 tff(skf18, type, skf18: ($i * $i) > $i). % 68.75/58.91 tff(man, type, man: ($i * $i) > $o). % 68.75/58.91 tff(sound, type, sound: ($i * $i) > $o). % 68.75/58.91 tff(weaponry, type, weaponry: ($i * $i) > $o). % 68.75/58.91 tff(unisex, type, unisex: ($i * $i) > $o). % 68.75/58.91 tff(skf16, type, skf16: ($i * $i) > $i). % 68.75/58.91 tff(set, type, set: ($i * $i) > $o). % 68.75/58.91 tff(skf12, type, skf12: ($i * $i) > $i). % 68.75/58.91 tff(impartial, type, impartial: ($i * $i) > $o). % 68.75/58.91 tff(object, type, object: ($i * $i) > $o). % 68.75/58.91 tff(skc12, type, skc12: $i). % 68.75/58.91 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 68.75/58.91 tff(specific, type, specific: ($i * $i) > $o). % 68.75/58.91 tff(skf20, type, skf20: ($i * $i) > $i). % 68.75/58.91 tff(skc10, type, skc10: $i). % 68.75/58.91 tff(act, type, act: ($i * $i) > $o). % 68.75/58.91 % 68.75/58.91 %Saturated clause set: % 68.81/58.92 tff(c_1643, plain, (![Z_1136, Y_1113, Y_1148, V_1146, Y_1145, Z_1132, Z_1143, U_203, V_1133, X2_1137, X2_1121, X1_1129, X1_1135, W_1142, Z_204, X2_1134, Y_1117, V_1116, Y_208, Y_1126, X_1138, X1_1144, W_202, Z_1112, X2_1150, X_1115, X1_1139, X1_1128, X1_205, V_1131, X2_206, X1_1123, Z_1122, V_209, X_1118, V_1114, Y_1147, Z_1127, X_1124, X_207, V_1125, X_1151, X2_1141, X_1140, X2_1130]: (skf21(V_1125, X_1138, Y_1147, Z_1136, X1_1123, X2_1130, W_202, U_203)=skf21(V_1114, X_1140, Y_1117, Z_1122, X1_1129, X2_1150, W_202, U_203) | skf21(V_1125, X_1138, Y_1147, Z_1136, X1_1123, X2_1130, W_202, U_203)=skf21(V_1116, X_1115, Y_1113, Z_1127, X1_1128, X2_1121, W_202, U_203) | skf21(V_1116, X_1115, Y_1113, Z_1127, X1_1128, X2_1121, W_202, U_203)=skf21(V_1114, X_1140, Y_1117, Z_1122, X1_1129, X2_1150, W_202, U_203) | skf21(V_1146, X_1118, Y_1126, Z_1143, X1_1144, X2_1134, W_202, U_203)=skf21(V_1116, X_1115, Y_1113, Z_1127, X1_1128, X2_1121, W_202, U_203) | skf21(V_1146, X_1118, Y_1126, Z_1143, X1_1144, X2_1134, W_202, U_203)=skf21(V_1125, X_1138, Y_1147, Z_1136, X1_1123, X2_1130, W_202, U_203) | skf21(V_1146, X_1118, Y_1126, Z_1143, X1_1144, X2_1134, W_202, U_203)=skf21(V_1114, X_1140, Y_1117, Z_1122, X1_1129, X2_1150, W_202, U_203) | skf21(V_1146, X_1118, Y_1126, Z_1143, X1_1144, X2_1134, W_202, U_203)=skf21(V_1131, X_1124, Y_1148, Z_1112, X1_1139, X2_1137, W_202, U_203) | skf21(V_1131, X_1124, Y_1148, Z_1112, X1_1139, X2_1137, W_202, U_203)=skf21(V_1116, X_1115, Y_1113, Z_1127, X1_1128, X2_1121, W_202, U_203) | skf21(V_1131, X_1124, Y_1148, Z_1112, X1_1139, X2_1137, W_202, U_203)=skf21(V_1125, X_1138, Y_1147, Z_1136, X1_1123, X2_1130, W_202, U_203) | skf21(V_1131, X_1124, Y_1148, Z_1112, X1_1139, X2_1137, W_202, U_203)=skf21(V_1114, X_1140, Y_1117, Z_1122, X1_1129, X2_1150, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1131, X_1124, Y_1148, Z_1112, X1_1139, X2_1137, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1146, X_1118, Y_1126, Z_1143, X1_1144, X2_1134, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1116, X_1115, Y_1113, Z_1127, X1_1128, X2_1121, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1125, X_1138, Y_1147, Z_1136, X1_1123, X2_1130, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1114, X_1140, Y_1117, Z_1122, X1_1129, X2_1150, W_202, U_203) | skf21(skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), V_1133, W_1142, X_1151, Y_1145, Z_1132, X1_1135, X2_1141)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_1150=X1_1129 | Z_1122=X1_1129 | Z_1122=X2_1150 | Z_1122=Y_1117 | Y_1117=X1_1129 | Y_1117=X2_1150 | Y_1117=X_1140 | Z_1122=X_1140 | X_1140=X1_1129 | X_1140=X2_1150 | X_1140=V_1114 | Y_1117=V_1114 | Z_1122=V_1114 | X1_1129=V_1114 | X2_1150=V_1114 | ~member(U_203, X2_1150, W_202) | ~member(U_203, X1_1129, W_202) | ~member(U_203, Z_1122, W_202) | ~member(U_203, Y_1117, W_202) | ~member(U_203, X_1140, W_202) | ~member(U_203, V_1114, W_202) | X2_1130=X1_1123 | Z_1136=X1_1123 | Z_1136=X2_1130 | Z_1136=Y_1147 | Y_1147=X1_1123 | Y_1147=X2_1130 | Y_1147=X_1138 | Z_1136=X_1138 | X_1138=X1_1123 | X_1138=X2_1130 | X_1138=V_1125 | Y_1147=V_1125 | Z_1136=V_1125 | X1_1123=V_1125 | X2_1130=V_1125 | ~member(U_203, X2_1130, W_202) | ~member(U_203, X1_1123, W_202) | ~member(U_203, Z_1136, W_202) | ~member(U_203, Y_1147, W_202) | ~member(U_203, X_1138, W_202) | ~member(U_203, V_1125, W_202) | X2_1121=X1_1128 | Z_1127=X1_1128 | Z_1127=X2_1121 | Z_1127=Y_1113 | Y_1113=X1_1128 | Y_1113=X2_1121 | Y_1113=X_1115 | Z_1127=X_1115 | X_1115=X1_1128 | X_1115=X2_1121 | X_1115=V_1116 | Y_1113=V_1116 | Z_1127=V_1116 | X1_1128=V_1116 | X2_1121=V_1116 | ~member(U_203, X2_1121, W_202) | ~member(U_203, X1_1128, W_202) | ~member(U_203, Z_1127, W_202) | ~member(U_203, Y_1113, W_202) | ~member(U_203, X_1115, W_202) | ~member(U_203, V_1116, W_202) | X2_1134=X1_1144 | Z_1143=X1_1144 | Z_1143=X2_1134 | Z_1143=Y_1126 | Y_1126=X1_1144 | Y_1126=X2_1134 | Y_1126=X_1118 | Z_1143=X_1118 | X_1118=X1_1144 | X_1118=X2_1134 | X_1118=V_1146 | Y_1126=V_1146 | Z_1143=V_1146 | X1_1144=V_1146 | X2_1134=V_1146 | ~member(U_203, X2_1134, W_202) | ~member(U_203, X1_1144, W_202) | ~member(U_203, Z_1143, W_202) | ~member(U_203, Y_1126, W_202) | ~member(U_203, X_1118, W_202) | ~member(U_203, V_1146, W_202) | X2_1137=X1_1139 | Z_1112=X1_1139 | Z_1112=X2_1137 | Z_1112=Y_1148 | Y_1148=X1_1139 | Y_1148=X2_1137 | Y_1148=X_1124 | Z_1112=X_1124 | X_1124=X1_1139 | X_1124=X2_1137 | X_1124=V_1131 | Y_1148=V_1131 | Z_1112=V_1131 | X1_1139=V_1131 | X2_1137=V_1131 | ~member(U_203, X2_1137, W_202) | ~member(U_203, X1_1139, W_202) | ~member(U_203, Z_1112, W_202) | ~member(U_203, Y_1148, W_202) | ~member(U_203, X_1124, W_202) | ~member(U_203, V_1131, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1620, plain, (![V_1068, X1_1055, Y_1075, X_1053, W_1071, X2_1064, X2_1072, U_203, X2_1069, U_1066, X1_1067, X2_1052, Z_204, Y_208, Y_1046, X1_1063, W_202, X1_1057, V_1059, Y_1060, Z_1070, Z_1076, X_1058, X1_205, Z_1048, Y_1074, X_1051, V_1062, X2_206, X2_1049, X_1061, Z_1047, V_209, Z_1073, X_207, V_1050, Y_1077, X_1054, X1_1065]: (skf21(V_1059, X_1058, Y_1046, Z_1047, X1_1057, X2_1052, W_202, U_203)=skf21(V_1050, X_1051, Y_1077, Z_1070, X1_1063, X2_1069, W_202, U_203) | skf21(V_1068, X_1053, Y_1060, Z_1073, X1_1055, X2_1049, W_202, U_203)=skf21(V_1059, X_1058, Y_1046, Z_1047, X1_1057, X2_1052, W_202, U_203) | skf21(V_1068, X_1053, Y_1060, Z_1073, X1_1055, X2_1049, W_202, U_203)=skf21(V_1050, X_1051, Y_1077, Z_1070, X1_1063, X2_1069, W_202, U_203) | skf21(V_1068, X_1053, Y_1060, Z_1073, X1_1055, X2_1049, W_202, U_203)=skf21(V_1062, X_1061, Y_1074, Z_1048, X1_1065, X2_1064, W_202, U_203) | skf21(V_1062, X_1061, Y_1074, Z_1048, X1_1065, X2_1064, W_202, U_203)=skf21(V_1059, X_1058, Y_1046, Z_1047, X1_1057, X2_1052, W_202, U_203) | skf21(V_1062, X_1061, Y_1074, Z_1048, X1_1065, X2_1064, W_202, U_203)=skf21(V_1050, X_1051, Y_1077, Z_1070, X1_1063, X2_1069, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1062, X_1061, Y_1074, Z_1048, X1_1065, X2_1064, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1068, X_1053, Y_1060, Z_1073, X1_1055, X2_1049, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1059, X_1058, Y_1046, Z_1047, X1_1057, X2_1052, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1050, X_1051, Y_1077, Z_1070, X1_1063, X2_1069, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_1066 | skf21(V_1062, X_1061, Y_1074, Z_1048, X1_1065, X2_1064, W_202, U_203)=U_1066 | skf21(V_1068, X_1053, Y_1060, Z_1073, X1_1055, X2_1049, W_202, U_203)=U_1066 | skf21(V_1059, X_1058, Y_1046, Z_1047, X1_1057, X2_1052, W_202, U_203)=U_1066 | skf21(V_1050, X_1051, Y_1077, Z_1070, X1_1063, X2_1069, W_202, U_203)=U_1066 | ~member(U_203, U_1066, W_202) | skf21(U_1066, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), W_1071, X_1054, Y_1075, Z_1076, X1_1067, X2_1072)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_1069=X1_1063 | Z_1070=X1_1063 | Z_1070=X2_1069 | Z_1070=Y_1077 | Y_1077=X1_1063 | Y_1077=X2_1069 | Y_1077=X_1051 | Z_1070=X_1051 | X_1051=X1_1063 | X_1051=X2_1069 | X_1051=V_1050 | Y_1077=V_1050 | Z_1070=V_1050 | X1_1063=V_1050 | X2_1069=V_1050 | ~member(U_203, X2_1069, W_202) | ~member(U_203, X1_1063, W_202) | ~member(U_203, Z_1070, W_202) | ~member(U_203, Y_1077, W_202) | ~member(U_203, X_1051, W_202) | ~member(U_203, V_1050, W_202) | X2_1052=X1_1057 | Z_1047=X1_1057 | Z_1047=X2_1052 | Z_1047=Y_1046 | Y_1046=X1_1057 | Y_1046=X2_1052 | Y_1046=X_1058 | Z_1047=X_1058 | X_1058=X1_1057 | X_1058=X2_1052 | X_1058=V_1059 | Y_1046=V_1059 | Z_1047=V_1059 | X1_1057=V_1059 | X2_1052=V_1059 | ~member(U_203, X2_1052, W_202) | ~member(U_203, X1_1057, W_202) | ~member(U_203, Z_1047, W_202) | ~member(U_203, Y_1046, W_202) | ~member(U_203, X_1058, W_202) | ~member(U_203, V_1059, W_202) | X2_1049=X1_1055 | Z_1073=X1_1055 | Z_1073=X2_1049 | Z_1073=Y_1060 | Y_1060=X1_1055 | Y_1060=X2_1049 | Y_1060=X_1053 | Z_1073=X_1053 | X_1053=X1_1055 | X_1053=X2_1049 | X_1053=V_1068 | Y_1060=V_1068 | Z_1073=V_1068 | X1_1055=V_1068 | X2_1049=V_1068 | ~member(U_203, X2_1049, W_202) | ~member(U_203, X1_1055, W_202) | ~member(U_203, Z_1073, W_202) | ~member(U_203, Y_1060, W_202) | ~member(U_203, X_1053, W_202) | ~member(U_203, V_1068, W_202) | X2_1064=X1_1065 | Z_1048=X1_1065 | Z_1048=X2_1064 | Z_1048=Y_1074 | Y_1074=X1_1065 | Y_1074=X2_1064 | Y_1074=X_1061 | Z_1048=X_1061 | X_1061=X1_1065 | X_1061=X2_1064 | X_1061=V_1062 | Y_1074=V_1062 | Z_1048=V_1062 | X1_1065=V_1062 | X2_1064=V_1062 | ~member(U_203, X2_1064, W_202) | ~member(U_203, X1_1065, W_202) | ~member(U_203, Z_1048, W_202) | ~member(U_203, Y_1074, W_202) | ~member(U_203, X_1061, W_202) | ~member(U_203, V_1062, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1598, plain, (![V_1033, X1_1044, X2_1040, V_1027, V_1016, X1_1030, X_1031, V_1010, X_1019, Y_1039, Z_1024, U_203, X2_1029, Y_1020, X1_1014, Z_204, Z_1028, X_1023, Y_208, X_1041, W_202, W_1038, X_1022, X1_1035, Z_1011, X2_1012, Y_1026, X2_1021, Y_1015, X1_205, V_1025, Z_1018, X2_1032, X2_206, Z_1037, V_209, U_1036, X_207, Y_1034, X1_1043]: (skf21(V_1033, X_1031, Y_1034, Z_1028, X1_1014, X2_1021, W_202, U_203)=skf21(V_1016, X_1019, Y_1026, Z_1037, X1_1035, X2_1040, W_202, U_203) | skf21(V_1033, X_1031, Y_1034, Z_1028, X1_1014, X2_1021, W_202, U_203)=skf21(V_1010, X_1022, Y_1015, Z_1024, X1_1044, X2_1012, W_202, U_203) | skf21(V_1016, X_1019, Y_1026, Z_1037, X1_1035, X2_1040, W_202, U_203)=skf21(V_1010, X_1022, Y_1015, Z_1024, X1_1044, X2_1012, W_202, U_203) | skf21(V_1025, X_1023, Y_1039, Z_1011, X1_1030, X2_1029, W_202, U_203)=skf21(V_1010, X_1022, Y_1015, Z_1024, X1_1044, X2_1012, W_202, U_203) | skf21(V_1033, X_1031, Y_1034, Z_1028, X1_1014, X2_1021, W_202, U_203)=skf21(V_1025, X_1023, Y_1039, Z_1011, X1_1030, X2_1029, W_202, U_203) | skf21(V_1025, X_1023, Y_1039, Z_1011, X1_1030, X2_1029, W_202, U_203)=skf21(V_1016, X_1019, Y_1026, Z_1037, X1_1035, X2_1040, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1025, X_1023, Y_1039, Z_1011, X1_1030, X2_1029, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1010, X_1022, Y_1015, Z_1024, X1_1044, X2_1012, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1033, X_1031, Y_1034, Z_1028, X1_1014, X2_1021, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1016, X_1019, Y_1026, Z_1037, X1_1035, X2_1040, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_1036 | skf21(V_1025, X_1023, Y_1039, Z_1011, X1_1030, X2_1029, W_202, U_203)=U_1036 | skf21(V_1010, X_1022, Y_1015, Z_1024, X1_1044, X2_1012, W_202, U_203)=U_1036 | skf21(V_1033, X_1031, Y_1034, Z_1028, X1_1014, X2_1021, W_202, U_203)=U_1036 | skf21(V_1016, X_1019, Y_1026, Z_1037, X1_1035, X2_1040, W_202, U_203)=U_1036 | ~member(U_203, U_1036, W_202) | skf21(U_1036, V_1027, W_1038, X_1041, Y_1020, Z_1018, X1_1043, X2_1032)!=U_1036 | X2_1040=X1_1035 | Z_1037=X1_1035 | Z_1037=X2_1040 | Z_1037=Y_1026 | Y_1026=X1_1035 | Y_1026=X2_1040 | Y_1026=X_1019 | Z_1037=X_1019 | X_1019=X1_1035 | X_1019=X2_1040 | X_1019=V_1016 | Y_1026=V_1016 | Z_1037=V_1016 | X1_1035=V_1016 | X2_1040=V_1016 | ~member(U_203, X2_1040, W_202) | ~member(U_203, X1_1035, W_202) | ~member(U_203, Z_1037, W_202) | ~member(U_203, Y_1026, W_202) | ~member(U_203, X_1019, W_202) | ~member(U_203, V_1016, W_202) | X2_1021=X1_1014 | Z_1028=X1_1014 | Z_1028=X2_1021 | Z_1028=Y_1034 | Y_1034=X1_1014 | Y_1034=X2_1021 | Y_1034=X_1031 | Z_1028=X_1031 | X_1031=X1_1014 | X_1031=X2_1021 | X_1031=V_1033 | Y_1034=V_1033 | Z_1028=V_1033 | X1_1014=V_1033 | X2_1021=V_1033 | ~member(U_203, X2_1021, W_202) | ~member(U_203, X1_1014, W_202) | ~member(U_203, Z_1028, W_202) | ~member(U_203, Y_1034, W_202) | ~member(U_203, X_1031, W_202) | ~member(U_203, V_1033, W_202) | X2_1012=X1_1044 | Z_1024=X1_1044 | Z_1024=X2_1012 | Z_1024=Y_1015 | Y_1015=X1_1044 | Y_1015=X2_1012 | Y_1015=X_1022 | Z_1024=X_1022 | X_1022=X1_1044 | X_1022=X2_1012 | X_1022=V_1010 | Y_1015=V_1010 | Z_1024=V_1010 | X1_1044=V_1010 | X2_1012=V_1010 | ~member(U_203, X2_1012, W_202) | ~member(U_203, X1_1044, W_202) | ~member(U_203, Z_1024, W_202) | ~member(U_203, Y_1015, W_202) | ~member(U_203, X_1022, W_202) | ~member(U_203, V_1010, W_202) | X2_1029=X1_1030 | Z_1011=X1_1030 | Z_1011=X2_1029 | Z_1011=Y_1039 | Y_1039=X1_1030 | Y_1039=X2_1029 | Y_1039=X_1023 | Z_1011=X_1023 | X_1023=X1_1030 | X_1023=X2_1029 | X_1023=V_1025 | Y_1039=V_1025 | Z_1011=V_1025 | X1_1030=V_1025 | X2_1029=V_1025 | ~member(U_203, X2_1029, W_202) | ~member(U_203, X1_1030, W_202) | ~member(U_203, Z_1011, W_202) | ~member(U_203, Y_1039, W_202) | ~member(U_203, X_1023, W_202) | ~member(U_203, V_1025, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1553, plain, (![X1_937, X2_933, U_928, V_949, X2_950, Z_925, U_203, V_930, X_936, Z_944, V_940, Z_204, Y_952, Y_208, W_202, X2_942, V_927, Y_939, X1_205, X1_931, Y_948, Z_945, X_935, X2_206, Y_946, V_209, X2_947, X_938, X1_943, Z_926, X_207, X1_932, X_941]: (skf21(V_949, X_941, Y_946, Z_944, X1_931, X2_950, W_202, U_203)=skf21(V_927, X_935, Y_952, Z_925, X1_937, X2_947, W_202, U_203) | skf21(V_940, X_936, Y_948, Z_926, X1_943, X2_942, W_202, U_203)=skf21(V_927, X_935, Y_952, Z_925, X1_937, X2_947, W_202, U_203) | skf21(V_949, X_941, Y_946, Z_944, X1_931, X2_950, W_202, U_203)=skf21(V_940, X_936, Y_948, Z_926, X1_943, X2_942, W_202, U_203) | skf21(V_940, X_936, Y_948, Z_926, X1_943, X2_942, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_927, X_935, Y_952, Z_925, X1_937, X2_947, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_949, X_941, Y_946, Z_944, X1_931, X2_950, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_930 | skf21(V_940, X_936, Y_948, Z_926, X1_943, X2_942, W_202, U_203)=V_930 | skf21(V_927, X_935, Y_952, Z_925, X1_937, X2_947, W_202, U_203)=V_930 | skf21(V_949, X_941, Y_946, Z_944, X1_931, X2_950, W_202, U_203)=V_930 | V_930=U_928 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_928 | skf21(V_940, X_936, Y_948, Z_926, X1_943, X2_942, W_202, U_203)=U_928 | skf21(V_927, X_935, Y_952, Z_925, X1_937, X2_947, W_202, U_203)=U_928 | skf21(V_949, X_941, Y_946, Z_944, X1_931, X2_950, W_202, U_203)=U_928 | ~member(U_203, V_930, W_202) | ~member(U_203, U_928, W_202) | skf21(U_928, V_930, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), X_938, Y_939, Z_945, X1_932, X2_933)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_950=X1_931 | Z_944=X1_931 | Z_944=X2_950 | Z_944=Y_946 | Y_946=X1_931 | Y_946=X2_950 | Y_946=X_941 | Z_944=X_941 | X_941=X1_931 | X_941=X2_950 | X_941=V_949 | Y_946=V_949 | Z_944=V_949 | X1_931=V_949 | X2_950=V_949 | ~member(U_203, X2_950, W_202) | ~member(U_203, X1_931, W_202) | ~member(U_203, Z_944, W_202) | ~member(U_203, Y_946, W_202) | ~member(U_203, X_941, W_202) | ~member(U_203, V_949, W_202) | X2_947=X1_937 | Z_925=X1_937 | Z_925=X2_947 | Z_925=Y_952 | Y_952=X1_937 | Y_952=X2_947 | Y_952=X_935 | Z_925=X_935 | X_935=X1_937 | X_935=X2_947 | X_935=V_927 | Y_952=V_927 | Z_925=V_927 | X1_937=V_927 | X2_947=V_927 | ~member(U_203, X2_947, W_202) | ~member(U_203, X1_937, W_202) | ~member(U_203, Z_925, W_202) | ~member(U_203, Y_952, W_202) | ~member(U_203, X_935, W_202) | ~member(U_203, V_927, W_202) | X2_942=X1_943 | Z_926=X1_943 | Z_926=X2_942 | Z_926=Y_948 | Y_948=X1_943 | Y_948=X2_942 | Y_948=X_936 | Z_926=X_936 | X_936=X1_943 | X_936=X2_942 | X_936=V_940 | Y_948=V_940 | Z_926=V_940 | X1_943=V_940 | X2_942=V_940 | ~member(U_203, X2_942, W_202) | ~member(U_203, X1_943, W_202) | ~member(U_203, Z_926, W_202) | ~member(U_203, Y_948, W_202) | ~member(U_203, X_936, W_202) | ~member(U_203, V_940, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1531, plain, (![Z_906, X_904, Y_921, U_203, V_917, X_914, Z_896, Z_204, W_922, X2_907, Y_208, Y_911, Z_897, W_202, X2_909, X1_899, X1_910, V_905, X1_913, X1_902, X1_205, X2_206, V_903, V_209, Y_924, Y_919, V_908, X_207, Z_918, X_912, X_901, U_898, X2_915, X2_916]: (skf21(V_917, X_912, Y_919, Z_906, X1_899, X2_916, W_202, U_203)=skf21(V_908, X_914, Y_911, Z_896, X1_913, X2_907, W_202, U_203) | skf21(V_917, X_912, Y_919, Z_906, X1_899, X2_916, W_202, U_203)=skf21(V_905, X_901, Y_921, Z_897, X1_910, X2_909, W_202, U_203) | skf21(V_908, X_914, Y_911, Z_896, X1_913, X2_907, W_202, U_203)=skf21(V_905, X_901, Y_921, Z_897, X1_910, X2_909, W_202, U_203) | skf21(V_905, X_901, Y_921, Z_897, X1_910, X2_909, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_917, X_912, Y_919, Z_906, X1_899, X2_916, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_908, X_914, Y_911, Z_896, X1_913, X2_907, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_903 | skf21(V_905, X_901, Y_921, Z_897, X1_910, X2_909, W_202, U_203)=V_903 | skf21(V_917, X_912, Y_919, Z_906, X1_899, X2_916, W_202, U_203)=V_903 | skf21(V_908, X_914, Y_911, Z_896, X1_913, X2_907, W_202, U_203)=V_903 | V_903=U_898 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_898 | skf21(V_905, X_901, Y_921, Z_897, X1_910, X2_909, W_202, U_203)=U_898 | skf21(V_917, X_912, Y_919, Z_906, X1_899, X2_916, W_202, U_203)=U_898 | skf21(V_908, X_914, Y_911, Z_896, X1_913, X2_907, W_202, U_203)=U_898 | ~member(U_203, V_903, W_202) | ~member(U_203, U_898, W_202) | skf21(U_898, V_903, W_922, X_904, Y_924, Z_918, X1_902, X2_915)!=V_903 | X2_907=X1_913 | Z_896=X1_913 | Z_896=X2_907 | Z_896=Y_911 | Y_911=X1_913 | Y_911=X2_907 | Y_911=X_914 | Z_896=X_914 | X_914=X1_913 | X_914=X2_907 | X_914=V_908 | Y_911=V_908 | Z_896=V_908 | X1_913=V_908 | X2_907=V_908 | ~member(U_203, X2_907, W_202) | ~member(U_203, X1_913, W_202) | ~member(U_203, Z_896, W_202) | ~member(U_203, Y_911, W_202) | ~member(U_203, X_914, W_202) | ~member(U_203, V_908, W_202) | X2_916=X1_899 | Z_906=X1_899 | Z_906=X2_916 | Z_906=Y_919 | Y_919=X1_899 | Y_919=X2_916 | Y_919=X_912 | Z_906=X_912 | X_912=X1_899 | X_912=X2_916 | X_912=V_917 | Y_919=V_917 | Z_906=V_917 | X1_899=V_917 | X2_916=V_917 | ~member(U_203, X2_916, W_202) | ~member(U_203, X1_899, W_202) | ~member(U_203, Z_906, W_202) | ~member(U_203, Y_919, W_202) | ~member(U_203, X_912, W_202) | ~member(U_203, V_917, W_202) | X2_909=X1_910 | Z_897=X1_910 | Z_897=X2_909 | Z_897=Y_921 | Y_921=X1_910 | Y_921=X2_909 | Y_921=X_901 | Z_897=X_901 | X_901=X1_910 | X_901=X2_909 | X_901=V_905 | Y_921=V_905 | Z_897=V_905 | X1_910=V_905 | X2_909=V_905 | ~member(U_203, X2_909, W_202) | ~member(U_203, X1_910, W_202) | ~member(U_203, Z_897, W_202) | ~member(U_203, Y_921, W_202) | ~member(U_203, X_901, W_202) | ~member(U_203, V_905, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1575, plain, (![X_974, X2_955, Y_976, Y_965, Z_977, V_963, U_203, Y_969, X2_967, X_973, X1_970, X2_975, Z_204, Y_208, U_971, Z_954, X5_966, X2_953, W_202, X_961, X1_962, V_958, Y_978, X1_205, Z_960, X1_979, X1_968, X2_206, V_980, X_964, V_209, V_981, X_207, Z_972, W_956]: (skf21(V_981, X_973, Y_969, Z_977, X1_979, X2_955, W_202, U_203)=skf21(V_980, X_974, Y_965, Z_960, X1_970, X2_975, W_202, U_203) | skf21(V_980, X_974, Y_965, Z_960, X1_970, X2_975, W_202, U_203)=skf21(V_963, X_961, Y_978, Z_954, X1_968, X2_967, W_202, U_203) | skf21(V_981, X_973, Y_969, Z_977, X1_979, X2_955, W_202, U_203)=skf21(V_963, X_961, Y_978, Z_954, X1_968, X2_967, W_202, U_203) | skf21(V_963, X_961, Y_978, Z_954, X1_968, X2_967, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_980, X_974, Y_965, Z_960, X1_970, X2_975, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_981, X_973, Y_969, Z_977, X1_979, X2_955, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_966 | skf21(V_963, X_961, Y_978, Z_954, X1_968, X2_967, W_202, U_203)=X5_966 | skf21(V_980, X_974, Y_965, Z_960, X1_970, X2_975, W_202, U_203)=X5_966 | skf21(V_981, X_973, Y_969, Z_977, X1_979, X2_955, W_202, U_203)=X5_966 | X5_966=U_971 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_971 | skf21(V_963, X_961, Y_978, Z_954, X1_968, X2_967, W_202, U_203)=U_971 | skf21(V_980, X_974, Y_965, Z_960, X1_970, X2_975, W_202, U_203)=U_971 | skf21(V_981, X_973, Y_969, Z_977, X1_979, X2_955, W_202, U_203)=U_971 | ~member(U_203, X5_966, W_202) | ~member(U_203, U_971, W_202) | skf21(U_971, V_958, W_956, X_964, Y_976, Z_972, X1_962, X2_953)!=U_971 | X2_955=X1_979 | Z_977=X1_979 | Z_977=X2_955 | Z_977=Y_969 | Y_969=X1_979 | Y_969=X2_955 | Y_969=X_973 | Z_977=X_973 | X_973=X1_979 | X_973=X2_955 | X_973=V_981 | Y_969=V_981 | Z_977=V_981 | X1_979=V_981 | X2_955=V_981 | ~member(U_203, X2_955, W_202) | ~member(U_203, X1_979, W_202) | ~member(U_203, Z_977, W_202) | ~member(U_203, Y_969, W_202) | ~member(U_203, X_973, W_202) | ~member(U_203, V_981, W_202) | X2_975=X1_970 | Z_960=X1_970 | Z_960=X2_975 | Z_960=Y_965 | Y_965=X1_970 | Y_965=X2_975 | Y_965=X_974 | Z_960=X_974 | X_974=X1_970 | X_974=X2_975 | X_974=V_980 | Y_965=V_980 | Z_960=V_980 | X1_970=V_980 | X2_975=V_980 | ~member(U_203, X2_975, W_202) | ~member(U_203, X1_970, W_202) | ~member(U_203, Z_960, W_202) | ~member(U_203, Y_965, W_202) | ~member(U_203, X_974, W_202) | ~member(U_203, V_980, W_202) | X2_967=X1_968 | Z_954=X1_968 | Z_954=X2_967 | Z_954=Y_978 | Y_978=X1_968 | Y_978=X2_967 | Y_978=X_961 | Z_954=X_961 | X_961=X1_968 | X_961=X2_967 | X_961=V_963 | Y_978=V_963 | Z_954=V_963 | X1_968=V_963 | X2_967=V_963 | ~member(U_203, X2_967, W_202) | ~member(U_203, X1_968, W_202) | ~member(U_203, Z_954, W_202) | ~member(U_203, Y_978, W_202) | ~member(U_203, X_961, W_202) | ~member(U_203, V_963, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1486, plain, (![Y_849, X_836, X1_842, V_837, U_846, X1_840, X_831, U_203, Z_841, Z_835, Z_830, X1_833, Z_204, V_838, Y_208, W_202, Y_844, X2_834, X1_205, X2_839, X2_206, W_847, V_209, Y_845, V_829, X_207, X2_843]: (skf21(V_838, X_836, Y_849, Z_830, X1_840, X2_839, W_202, U_203)=skf21(V_829, X_831, Y_845, Z_841, X1_833, X2_843, W_202, U_203) | skf21(V_838, X_836, Y_849, Z_830, X1_840, X2_839, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_829, X_831, Y_845, Z_841, X1_833, X2_843, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_847 | skf21(V_838, X_836, Y_849, Z_830, X1_840, X2_839, W_202, U_203)=W_847 | skf21(V_829, X_831, Y_845, Z_841, X1_833, X2_843, W_202, U_203)=W_847 | W_847=V_837 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_837 | skf21(V_838, X_836, Y_849, Z_830, X1_840, X2_839, W_202, U_203)=V_837 | skf21(V_829, X_831, Y_845, Z_841, X1_833, X2_843, W_202, U_203)=V_837 | V_837=U_846 | W_847=U_846 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_846 | skf21(V_838, X_836, Y_849, Z_830, X1_840, X2_839, W_202, U_203)=U_846 | skf21(V_829, X_831, Y_845, Z_841, X1_833, X2_843, W_202, U_203)=U_846 | ~member(U_203, W_847, W_202) | ~member(U_203, V_837, W_202) | ~member(U_203, U_846, W_202) | skf21(U_846, V_837, W_847, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Y_844, Z_835, X1_842, X2_834)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_843=X1_833 | Z_841=X1_833 | Z_841=X2_843 | Z_841=Y_845 | Y_845=X1_833 | Y_845=X2_843 | Y_845=X_831 | Z_841=X_831 | X_831=X1_833 | X_831=X2_843 | X_831=V_829 | Y_845=V_829 | Z_841=V_829 | X1_833=V_829 | X2_843=V_829 | ~member(U_203, X2_843, W_202) | ~member(U_203, X1_833, W_202) | ~member(U_203, Z_841, W_202) | ~member(U_203, Y_845, W_202) | ~member(U_203, X_831, W_202) | ~member(U_203, V_829, W_202) | X2_839=X1_840 | Z_830=X1_840 | Z_830=X2_839 | Z_830=Y_849 | Y_849=X1_840 | Y_849=X2_839 | Y_849=X_836 | Z_830=X_836 | X_836=X1_840 | X_836=X2_839 | X_836=V_838 | Y_849=V_838 | Z_830=V_838 | X1_840=V_838 | X2_839=V_838 | ~member(U_203, X2_839, W_202) | ~member(U_203, X1_840, W_202) | ~member(U_203, Z_830, W_202) | ~member(U_203, Y_849, W_202) | ~member(U_203, X_836, W_202) | ~member(U_203, V_838, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1442, plain, (![X1_791, V_798, X1_795, Z_804, X_788, X5_784, X2_802, Y_785, W_782, U_203, X6_805, X2_789, Z_783, Z_204, Y_208, W_202, X1_205, V_796, Y_787, X_797, X2_793, X2_206, V_209, X_207, Z_799, V_792, X1_794, U_781, Y_801, X_800]: (skf21(V_796, X_800, Y_785, Z_799, X1_791, X2_789, W_202, U_203)=skf21(V_792, X_788, Y_801, Z_783, X1_794, X2_793, W_202, U_203) | skf21(V_792, X_788, Y_801, Z_783, X1_794, X2_793, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_796, X_800, Y_785, Z_799, X1_791, X2_789, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_805 | skf21(V_792, X_788, Y_801, Z_783, X1_794, X2_793, W_202, U_203)=X6_805 | skf21(V_796, X_800, Y_785, Z_799, X1_791, X2_789, W_202, U_203)=X6_805 | X6_805=X5_784 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_784 | skf21(V_792, X_788, Y_801, Z_783, X1_794, X2_793, W_202, U_203)=X5_784 | skf21(V_796, X_800, Y_785, Z_799, X1_791, X2_789, W_202, U_203)=X5_784 | X5_784=U_781 | X6_805=U_781 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_781 | skf21(V_792, X_788, Y_801, Z_783, X1_794, X2_793, W_202, U_203)=U_781 | skf21(V_796, X_800, Y_785, Z_799, X1_791, X2_789, W_202, U_203)=U_781 | ~member(U_203, X6_805, W_202) | ~member(U_203, X5_784, W_202) | ~member(U_203, U_781, W_202) | skf21(U_781, V_798, W_782, X_797, Y_787, Z_804, X1_795, X2_802)!=U_781 | X2_789=X1_791 | Z_799=X1_791 | Z_799=X2_789 | Z_799=Y_785 | Y_785=X1_791 | Y_785=X2_789 | Y_785=X_800 | Z_799=X_800 | X_800=X1_791 | X_800=X2_789 | X_800=V_796 | Y_785=V_796 | Z_799=V_796 | X1_791=V_796 | X2_789=V_796 | ~member(U_203, X2_789, W_202) | ~member(U_203, X1_791, W_202) | ~member(U_203, Z_799, W_202) | ~member(U_203, Y_785, W_202) | ~member(U_203, X_800, W_202) | ~member(U_203, V_796, W_202) | X2_793=X1_794 | Z_783=X1_794 | Z_783=X2_793 | Z_783=Y_801 | Y_801=X1_794 | Y_801=X2_793 | Y_801=X_788 | Z_783=X_788 | X_788=X1_794 | X_788=X2_793 | X_788=V_792 | Y_801=V_792 | Z_783=V_792 | X1_794=V_792 | X2_793=V_792 | ~member(U_203, X2_793, W_202) | ~member(U_203, X1_794, W_202) | ~member(U_203, Z_783, W_202) | ~member(U_203, Y_801, W_202) | ~member(U_203, X_788, W_202) | ~member(U_203, V_792, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.92 tff(c_1464, plain, (![V_810, X1_808, X2_821, X_825, Y_818, U_203, X1_822, Z_827, X2_819, X1_815, Z_204, Y_817, Y_208, W_202, V_824, X1_205, V_820, X_812, Z_807, X2_811, X2_206, V_209, Z_814, X_207, U_823, W_806, Y_826, X_816]: (skf21(V_824, X_825, Y_817, Z_814, X1_808, X2_811, W_202, U_203)=skf21(V_820, X_816, Y_826, Z_807, X1_822, X2_821, W_202, U_203) | skf21(V_820, X_816, Y_826, Z_807, X1_822, X2_821, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_824, X_825, Y_817, Z_814, X1_808, X2_811, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_806 | skf21(V_820, X_816, Y_826, Z_807, X1_822, X2_821, W_202, U_203)=W_806 | skf21(V_824, X_825, Y_817, Z_814, X1_808, X2_811, W_202, U_203)=W_806 | W_806=V_810 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_810 | skf21(V_820, X_816, Y_826, Z_807, X1_822, X2_821, W_202, U_203)=V_810 | skf21(V_824, X_825, Y_817, Z_814, X1_808, X2_811, W_202, U_203)=V_810 | V_810=U_823 | W_806=U_823 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_823 | skf21(V_820, X_816, Y_826, Z_807, X1_822, X2_821, W_202, U_203)=U_823 | skf21(V_824, X_825, Y_817, Z_814, X1_808, X2_811, W_202, U_203)=U_823 | ~member(U_203, W_806, W_202) | ~member(U_203, V_810, W_202) | ~member(U_203, U_823, W_202) | skf21(U_823, V_810, W_806, X_812, Y_818, Z_827, X1_815, X2_819)!=W_806 | X2_811=X1_808 | Z_814=X1_808 | Z_814=X2_811 | Z_814=Y_817 | Y_817=X1_808 | Y_817=X2_811 | Y_817=X_825 | Z_814=X_825 | X_825=X1_808 | X_825=X2_811 | X_825=V_824 | Y_817=V_824 | Z_814=V_824 | X1_808=V_824 | X2_811=V_824 | ~member(U_203, X2_811, W_202) | ~member(U_203, X1_808, W_202) | ~member(U_203, Z_814, W_202) | ~member(U_203, Y_817, W_202) | ~member(U_203, X_825, W_202) | ~member(U_203, V_824, W_202) | X2_821=X1_822 | Z_807=X1_822 | Z_807=X2_821 | Z_807=Y_826 | Y_826=X1_822 | Y_826=X2_821 | Y_826=X_816 | Z_807=X_816 | X_816=X1_822 | X_816=X2_821 | X_816=V_820 | Y_826=V_820 | Z_807=V_820 | X1_822=V_820 | X2_821=V_820 | ~member(U_203, X2_821, W_202) | ~member(U_203, X1_822, W_202) | ~member(U_203, Z_807, W_202) | ~member(U_203, Y_826, W_202) | ~member(U_203, X_816, W_202) | ~member(U_203, V_820, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1508, plain, (![Z_873, Y_872, V_865, Z_851, U_203, X1_859, X2_863, X2_870, X_861, X_855, Z_204, Y_208, X5_854, W_202, X_860, X1_205, W_868, X2_862, X2_206, X1_857, V_209, Y_869, V_858, Z_866, Y_856, V_852, X_207, U_871, X1_864]: (skf21(V_858, X_855, Y_872, Z_851, X1_864, X2_862, W_202, U_203)=skf21(V_852, X_861, Y_869, Z_873, X1_857, X2_863, W_202, U_203) | skf21(V_858, X_855, Y_872, Z_851, X1_864, X2_862, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_852, X_861, Y_869, Z_873, X1_857, X2_863, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_854 | skf21(V_858, X_855, Y_872, Z_851, X1_864, X2_862, W_202, U_203)=X5_854 | skf21(V_852, X_861, Y_869, Z_873, X1_857, X2_863, W_202, U_203)=X5_854 | X5_854=V_865 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_865 | skf21(V_858, X_855, Y_872, Z_851, X1_864, X2_862, W_202, U_203)=V_865 | skf21(V_852, X_861, Y_869, Z_873, X1_857, X2_863, W_202, U_203)=V_865 | V_865=U_871 | X5_854=U_871 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_871 | skf21(V_858, X_855, Y_872, Z_851, X1_864, X2_862, W_202, U_203)=U_871 | skf21(V_852, X_861, Y_869, Z_873, X1_857, X2_863, W_202, U_203)=U_871 | ~member(U_203, X5_854, W_202) | ~member(U_203, V_865, W_202) | ~member(U_203, U_871, W_202) | skf21(U_871, V_865, W_868, X_860, Y_856, Z_866, X1_859, X2_870)!=V_865 | X2_863=X1_857 | Z_873=X1_857 | Z_873=X2_863 | Z_873=Y_869 | Y_869=X1_857 | Y_869=X2_863 | Y_869=X_861 | Z_873=X_861 | X_861=X1_857 | X_861=X2_863 | X_861=V_852 | Y_869=V_852 | Z_873=V_852 | X1_857=V_852 | X2_863=V_852 | ~member(U_203, X2_863, W_202) | ~member(U_203, X1_857, W_202) | ~member(U_203, Z_873, W_202) | ~member(U_203, Y_869, W_202) | ~member(U_203, X_861, W_202) | ~member(U_203, V_852, W_202) | X2_862=X1_864 | Z_851=X1_864 | Z_851=X2_862 | Z_851=Y_872 | Y_872=X1_864 | Y_872=X2_862 | Y_872=X_855 | Z_851=X_855 | X_855=X1_864 | X_855=X2_862 | X_855=V_858 | Y_872=V_858 | Z_851=V_858 | X1_864=V_858 | X2_862=V_858 | ~member(U_203, X2_862, W_202) | ~member(U_203, X1_864, W_202) | ~member(U_203, Z_851, W_202) | ~member(U_203, Y_872, W_202) | ~member(U_203, X_855, W_202) | ~member(U_203, V_858, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1331, plain, (![X_676, W_680, V_683, X_687, V_678, U_203, X2_677, Z_682, X2_688, Y_681, Z_204, Y_208, X1_690, W_202, X1_205, X2_206, V_209, U_679, X_207, Z_684, X1_689]: (skf21(V_683, X_676, Y_681, Z_684, X1_690, X2_688, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X_687 | skf21(V_683, X_676, Y_681, Z_684, X1_690, X2_688, W_202, U_203)=X_687 | X_687=W_680 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_680 | skf21(V_683, X_676, Y_681, Z_684, X1_690, X2_688, W_202, U_203)=W_680 | W_680=V_678 | X_687=V_678 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_678 | skf21(V_683, X_676, Y_681, Z_684, X1_690, X2_688, W_202, U_203)=V_678 | V_678=U_679 | W_680=U_679 | X_687=U_679 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_679 | skf21(V_683, X_676, Y_681, Z_684, X1_690, X2_688, W_202, U_203)=U_679 | ~member(U_203, X_687, W_202) | ~member(U_203, W_680, W_202) | ~member(U_203, V_678, W_202) | ~member(U_203, U_679, W_202) | skf21(U_679, V_678, W_680, X_687, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Z_682, X1_689, X2_677)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_688=X1_690 | Z_684=X1_690 | Z_684=X2_688 | Z_684=Y_681 | Y_681=X1_690 | Y_681=X2_688 | Y_681=X_676 | Z_684=X_676 | X_676=X1_690 | X_676=X2_688 | X_676=V_683 | Y_681=V_683 | Z_684=V_683 | X1_690=V_683 | X2_688=V_683 | ~member(U_203, X2_688, W_202) | ~member(U_203, X1_690, W_202) | ~member(U_203, Z_684, W_202) | ~member(U_203, Y_681, W_202) | ~member(U_203, X_676, W_202) | ~member(U_203, V_683, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1397, plain, (![Z_729, X5_732, X1_739, X1_742, U_741, U_203, Z_204, Y_208, W_202, V_730, X_737, V_733, X_727, X2_744, X6_734, W_728, X1_205, Y_731, X2_206, X2_738, Y_743, V_209, X_207, Z_735]: (skf21(V_733, X_727, Y_731, Z_735, X1_742, X2_738, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_734 | skf21(V_733, X_727, Y_731, Z_735, X1_742, X2_738, W_202, U_203)=X6_734 | X6_734=X5_732 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_732 | skf21(V_733, X_727, Y_731, Z_735, X1_742, X2_738, W_202, U_203)=X5_732 | X5_732=V_730 | X6_734=V_730 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_730 | skf21(V_733, X_727, Y_731, Z_735, X1_742, X2_738, W_202, U_203)=V_730 | V_730=U_741 | X5_732=U_741 | X6_734=U_741 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_741 | skf21(V_733, X_727, Y_731, Z_735, X1_742, X2_738, W_202, U_203)=U_741 | ~member(U_203, X6_734, W_202) | ~member(U_203, X5_732, W_202) | ~member(U_203, V_730, W_202) | ~member(U_203, U_741, W_202) | skf21(U_741, V_730, W_728, X_737, Y_743, Z_729, X1_739, X2_744)!=V_730 | X2_738=X1_742 | Z_735=X1_742 | Z_735=X2_738 | Z_735=Y_731 | Y_731=X1_742 | Y_731=X2_738 | Y_731=X_727 | Z_735=X_727 | X_727=X1_742 | X_727=X2_738 | X_727=V_733 | Y_731=V_733 | Z_735=V_733 | X1_742=V_733 | X2_738=V_733 | ~member(U_203, X2_738, W_202) | ~member(U_203, X1_742, W_202) | ~member(U_203, Z_735, W_202) | ~member(U_203, Y_731, W_202) | ~member(U_203, X_727, W_202) | ~member(U_203, V_733, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1353, plain, (![X2_708, U_692, Z_698, V_697, U_203, Y_696, Z_204, Y_208, X2_703, W_202, X1_700, X_693, X1_704, V_695, X1_205, W_702, X2_206, V_209, Z_706, X_701, X_207, Y_694]: (skf21(V_697, X_693, Y_696, Z_698, X1_704, X2_703, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X_701 | skf21(V_697, X_693, Y_696, Z_698, X1_704, X2_703, W_202, U_203)=X_701 | X_701=W_702 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_702 | skf21(V_697, X_693, Y_696, Z_698, X1_704, X2_703, W_202, U_203)=W_702 | W_702=V_695 | X_701=V_695 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_695 | skf21(V_697, X_693, Y_696, Z_698, X1_704, X2_703, W_202, U_203)=V_695 | V_695=U_692 | W_702=U_692 | X_701=U_692 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_692 | skf21(V_697, X_693, Y_696, Z_698, X1_704, X2_703, W_202, U_203)=U_692 | ~member(U_203, X_701, W_202) | ~member(U_203, W_702, W_202) | ~member(U_203, V_695, W_202) | ~member(U_203, U_692, W_202) | skf21(U_692, V_695, W_702, X_701, Y_694, Z_706, X1_700, X2_708)!=X_701 | X2_703=X1_704 | Z_698=X1_704 | Z_698=X2_703 | Z_698=Y_696 | Y_696=X1_704 | Y_696=X2_703 | Y_696=X_693 | Z_698=X_693 | X_693=X1_704 | X_693=X2_703 | X_693=V_697 | Y_696=V_697 | Z_698=V_697 | X1_704=V_697 | X2_703=V_697 | ~member(U_203, X2_703, W_202) | ~member(U_203, X1_704, W_202) | ~member(U_203, Z_698, W_202) | ~member(U_203, Y_696, W_202) | ~member(U_203, X_693, W_202) | ~member(U_203, V_697, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1375, plain, (![Y_726, Y_712, X_718, V_713, W_719, U_203, X1_725, Z_715, X2_721, Z_204, X2_710, Y_208, W_202, V_722, X1_205, U_714, X2_206, Z_720, V_209, X5_717, X1_723, X_207, X_709]: (skf21(V_713, X_709, Y_712, Z_715, X1_723, X2_721, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_717 | skf21(V_713, X_709, Y_712, Z_715, X1_723, X2_721, W_202, U_203)=X5_717 | X5_717=W_719 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_719 | skf21(V_713, X_709, Y_712, Z_715, X1_723, X2_721, W_202, U_203)=W_719 | W_719=V_722 | X5_717=V_722 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_722 | skf21(V_713, X_709, Y_712, Z_715, X1_723, X2_721, W_202, U_203)=V_722 | V_722=U_714 | W_719=U_714 | X5_717=U_714 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_714 | skf21(V_713, X_709, Y_712, Z_715, X1_723, X2_721, W_202, U_203)=U_714 | ~member(U_203, X5_717, W_202) | ~member(U_203, W_719, W_202) | ~member(U_203, V_722, W_202) | ~member(U_203, U_714, W_202) | skf21(U_714, V_722, W_719, X_718, Y_726, Z_720, X1_725, X2_710)!=W_719 | X2_721=X1_723 | Z_715=X1_723 | Z_715=X2_721 | Z_715=Y_712 | Y_712=X1_723 | Y_712=X2_721 | Y_712=X_709 | Z_715=X_709 | X_709=X1_723 | X_709=X2_721 | X_709=V_713 | Y_712=V_713 | Z_715=V_713 | X1_723=V_713 | X2_721=V_713 | ~member(U_203, X2_721, W_202) | ~member(U_203, X1_723, W_202) | ~member(U_203, Z_715, W_202) | ~member(U_203, Y_712, W_202) | ~member(U_203, X_709, W_202) | ~member(U_203, V_713, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1419, plain, (![X1_762, X6_753, Y_760, U_203, X_748, V_752, W_763, X7_746, Z_204, X5_756, Y_208, X2_747, V_759, W_202, Y_751, X1_205, Z_758, X2_206, X2_761, V_209, X1_749, X_207, U_757, Z_754, X_765]: (skf21(V_752, X_748, Y_751, Z_754, X1_762, X2_761, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X7_746 | skf21(V_752, X_748, Y_751, Z_754, X1_762, X2_761, W_202, U_203)=X7_746 | X7_746=X6_753 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_753 | skf21(V_752, X_748, Y_751, Z_754, X1_762, X2_761, W_202, U_203)=X6_753 | X6_753=X5_756 | X7_746=X5_756 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_756 | skf21(V_752, X_748, Y_751, Z_754, X1_762, X2_761, W_202, U_203)=X5_756 | X5_756=U_757 | X6_753=U_757 | X7_746=U_757 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_757 | skf21(V_752, X_748, Y_751, Z_754, X1_762, X2_761, W_202, U_203)=U_757 | ~member(U_203, X7_746, W_202) | ~member(U_203, X6_753, W_202) | ~member(U_203, X5_756, W_202) | ~member(U_203, U_757, W_202) | skf21(U_757, V_759, W_763, X_765, Y_760, Z_758, X1_749, X2_747)!=U_757 | X2_761=X1_762 | Z_754=X1_762 | Z_754=X2_761 | Z_754=Y_751 | Y_751=X1_762 | Y_751=X2_761 | Y_751=X_748 | Z_754=X_748 | X_748=X1_762 | X_748=X2_761 | X_748=V_752 | Y_751=V_752 | Z_754=V_752 | X1_762=V_752 | X2_761=V_752 | ~member(U_203, X2_761, W_202) | ~member(U_203, X1_762, W_202) | ~member(U_203, Z_754, W_202) | ~member(U_203, Y_751, W_202) | ~member(U_203, X_748, W_202) | ~member(U_203, V_752, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_1311, plain, (![X2_672, X_670, Z_668, U_212, Y_674, V_671, U_675, X_216, V_218, X2_215, W_669, Y_217, X1_673, W_210, X1_214]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=Y_217 | Y_217=X_216 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X_216 | X_216=W_210 | Y_217=W_210 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=W_210 | W_210=V_218 | X_216=V_218 | Y_217=V_218 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=V_218 | V_218=U_212 | W_210=U_212 | X_216=U_212 | Y_217=U_212 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_212 | ~member(U_675, Y_217, W_669) | ~member(U_675, X_216, W_669) | ~member(U_675, W_210, W_669) | ~member(U_675, V_218, W_669) | ~member(U_675, U_212, W_669) | skf21(U_212, V_218, W_210, X_216, Y_217, skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675), X1_214, X2_215)!=skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675) | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_1310, plain, (![X8_200, X2_672, V_199, X_670, Z_668, X6_188, X2_196, Y_674, X7_194, W_189, V_671, Z_193, U_675, X1_195, U_191, X_197, Y_198, W_669, X5_187, X1_673]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X8_200 | X8_200=X7_194 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X7_194 | X7_194=X6_188 | X8_200=X6_188 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X6_188 | X6_188=X5_187 | X7_194=X5_187 | X8_200=X5_187 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X5_187 | X5_187=U_191 | X6_188=U_191 | X7_194=U_191 | X8_200=U_191 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_191 | ~member(U_675, X8_200, W_669) | ~member(U_675, X7_194, W_669) | ~member(U_675, X6_188, W_669) | ~member(U_675, X5_187, W_669) | ~member(U_675, U_191, W_669) | skf21(U_191, V_199, W_189, X_197, Y_198, Z_193, X1_195, X2_196)!=U_191 | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_1309, plain, (![X2_672, V_184, X5_173, X_670, Z_668, Y_674, X6_174, V_671, Z_178, X_182, U_675, Y_183, X1_180, W_175, U_177, W_669, X1_673, X2_181, X7_179]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X7_179 | X7_179=X6_174 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X6_174 | X6_174=X5_173 | X7_179=X5_173 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X5_173 | X5_173=V_184 | X6_174=V_184 | X7_179=V_184 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=V_184 | V_184=U_177 | X5_173=U_177 | X6_174=U_177 | X7_179=U_177 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_177 | ~member(U_675, X7_179, W_669) | ~member(U_675, X6_174, W_669) | ~member(U_675, X5_173, W_669) | ~member(U_675, V_184, W_669) | ~member(U_675, U_177, W_669) | skf21(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181)!=V_184 | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_1308, plain, (![X2_672, U_164, X6_161, Y_170, X_670, Z_668, W_162, Y_674, V_671, U_675, X1_167, X_169, Z_165, V_171, X2_168, W_669, X1_673, X5_160]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X6_161 | X6_161=X5_160 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X5_160 | X5_160=W_162 | X6_161=W_162 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=W_162 | W_162=V_171 | X5_160=V_171 | X6_161=V_171 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=V_171 | V_171=U_164 | W_162=U_164 | X5_160=U_164 | X6_161=U_164 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_164 | ~member(U_675, X6_161, W_669) | ~member(U_675, X5_160, W_669) | ~member(U_675, W_162, W_669) | ~member(U_675, V_171, W_669) | ~member(U_675, U_164, W_669) | skf21(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168)!=W_162 | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_1312, plain, (![X2_672, X_156, X_670, Z_668, X2_155, Y_674, X5_148, V_671, X1_154, U_152, Z_153, U_675, Y_157, V_158, W_669, W_150, X1_673]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X5_148 | X_156=X5_148 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X_156 | X_156=W_150 | X5_148=W_150 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=W_150 | W_150=V_158 | X_156=V_158 | X5_148=V_158 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=V_158 | V_158=U_152 | W_150=U_152 | X_156=U_152 | X5_148=U_152 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_152 | ~member(U_675, X5_148, W_669) | ~member(U_675, X_156, W_669) | ~member(U_675, W_150, W_669) | ~member(U_675, V_158, W_669) | ~member(U_675, U_152, W_669) | skf21(U_152, V_158, W_150, X_156, Y_157, Z_153, X1_154, X2_155)!=X_156 | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_1307, plain, (![X2_672, X_670, Z_668, X_144, Y_674, Y_145, Z_141, V_671, U_675, U_140, X1_142, W_669, X1_673, V_146, X2_143, W_138]: (skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=Y_145 | Y_145=X_144 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=X_144 | X_144=W_138 | Y_145=W_138 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=W_138 | W_138=V_146 | X_144=V_146 | Y_145=V_146 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=V_146 | V_146=U_140 | W_138=U_140 | X_144=U_140 | Y_145=U_140 | skf21(V_671, X_670, Y_674, Z_668, X1_673, X2_672, W_669, U_675)=U_140 | ~member(U_675, Y_145, W_669) | ~member(U_675, X_144, W_669) | ~member(U_675, W_138, W_669) | ~member(U_675, V_146, W_669) | ~member(U_675, U_140, W_669) | skf21(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143)!=Y_145 | X2_672=X1_673 | Z_668=X1_673 | Z_668=X2_672 | Z_668=Y_674 | Y_674=X1_673 | Y_674=X2_672 | Y_674=X_670 | Z_668=X_670 | X_670=X1_673 | X_670=X2_672 | X_670=V_671 | Y_674=V_671 | Z_668=V_671 | X1_673=V_671 | X2_672=V_671 | six(U_675, W_669) | ~member(U_675, X2_672, W_669) | ~member(U_675, X1_673, W_669) | ~member(U_675, Z_668, W_669) | ~member(U_675, Y_674, W_669) | ~member(U_675, X_670, W_669) | ~member(U_675, V_671, W_669)))). % 68.81/58.93 tff(c_146, plain, (![U_203, Z_204, Y_208, W_202, X1_205, X2_206, V_209, X_207]: (X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | member(U_203, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), W_202) | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 68.81/58.93 tff(c_136, plain, (![X4_147, X_144, Y_145, Z_141, X3_139, X5_137, U_140, X1_142, V_146, X2_143, W_138]: (Y_145=X5_137 | Y_145=X_144 | X_144=X5_137 | X_144=W_138 | Y_145=W_138 | X5_137=W_138 | W_138=V_146 | X_144=V_146 | Y_145=V_146 | X5_137=V_146 | V_146=U_140 | W_138=U_140 | X_144=U_140 | Y_145=U_140 | X5_137=U_140 | six(X3_139, X4_147) | ~member(X3_139, X5_137, X4_147) | ~member(X3_139, Y_145, X4_147) | ~member(X3_139, X_144, X4_147) | ~member(X3_139, W_138, X4_147) | ~member(X3_139, V_146, X4_147) | ~member(X3_139, U_140, X4_147) | skf21(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143)!=Y_145))). % 68.81/58.93 tff(c_140, plain, (![U_164, X7_166, X6_161, Y_170, W_162, X1_167, X3_163, X_169, Z_165, V_171, X2_168, X4_172, X5_160]: (X7_166=X6_161 | X6_161=X5_160 | X7_166=X5_160 | X5_160=W_162 | X6_161=W_162 | X7_166=W_162 | W_162=V_171 | X5_160=V_171 | X6_161=V_171 | X7_166=V_171 | V_171=U_164 | W_162=U_164 | X5_160=U_164 | X6_161=U_164 | X7_166=U_164 | six(X3_163, X4_172) | ~member(X3_163, X7_166, X4_172) | ~member(X3_163, X6_161, X4_172) | ~member(X3_163, X5_160, X4_172) | ~member(X3_163, W_162, X4_172) | ~member(X3_163, V_171, X4_172) | ~member(X3_163, U_164, X4_172) | skf21(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168)!=W_162))). % 68.81/58.93 tff(c_142, plain, (![X3_176, V_184, X5_173, X6_174, Z_178, X_182, Y_183, X1_180, X4_186, X8_185, W_175, U_177, X2_181, X7_179]: (X8_185=X7_179 | X7_179=X6_174 | X8_185=X6_174 | X6_174=X5_173 | X7_179=X5_173 | X8_185=X5_173 | X5_173=V_184 | X6_174=V_184 | X7_179=V_184 | X8_185=V_184 | V_184=U_177 | X5_173=U_177 | X6_174=U_177 | X7_179=U_177 | X8_185=U_177 | six(X3_176, X4_186) | ~member(X3_176, X8_185, X4_186) | ~member(X3_176, X7_179, X4_186) | ~member(X3_176, X6_174, X4_186) | ~member(X3_176, X5_173, X4_186) | ~member(X3_176, V_184, X4_186) | ~member(X3_176, U_177, X4_186) | skf21(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181)!=V_184))). % 68.81/58.93 tff(c_144, plain, (![X8_200, V_199, X6_188, X2_196, X3_190, X4_201, X7_194, W_189, Z_193, X1_195, U_191, X_197, Y_198, X5_187, X9_192]: (X9_192=X8_200 | X8_200=X7_194 | X9_192=X7_194 | X7_194=X6_188 | X8_200=X6_188 | X9_192=X6_188 | X6_188=X5_187 | X7_194=X5_187 | X8_200=X5_187 | X9_192=X5_187 | X5_187=U_191 | X6_188=U_191 | X7_194=U_191 | X8_200=U_191 | X9_192=U_191 | six(X3_190, X4_201) | ~member(X3_190, X9_192, X4_201) | ~member(X3_190, X8_200, X4_201) | ~member(X3_190, X7_194, X4_201) | ~member(X3_190, X6_188, X4_201) | ~member(X3_190, X5_187, X4_201) | ~member(X3_190, U_191, X4_201) | skf21(U_191, V_199, W_189, X_197, Y_198, Z_193, X1_195, X2_196)!=U_191))). % 68.81/58.93 tff(c_148, plain, (![Z_213, X4_219, U_212, X_216, V_218, X2_215, X3_211, Y_217, W_210, X1_214]: (Z_213=Y_217 | Y_217=X_216 | Z_213=X_216 | X_216=W_210 | Y_217=W_210 | Z_213=W_210 | W_210=V_218 | X_216=V_218 | Y_217=V_218 | Z_213=V_218 | V_218=U_212 | W_210=U_212 | X_216=U_212 | Y_217=U_212 | Z_213=U_212 | six(X3_211, X4_219) | ~member(X3_211, Z_213, X4_219) | ~member(X3_211, Y_217, X4_219) | ~member(X3_211, X_216, X4_219) | ~member(X3_211, W_210, X4_219) | ~member(X3_211, V_218, X4_219) | ~member(X3_211, U_212, X4_219) | skf21(U_212, V_218, W_210, X_216, Y_217, Z_213, X1_214, X2_215)!=Z_213))). % 68.81/58.93 tff(c_138, plain, (![X_156, X2_155, X3_151, X5_148, X1_154, U_152, X6_149, Z_153, Y_157, V_158, W_150, X4_159]: (X6_149=X5_148 | X_156=X5_148 | X_156=X6_149 | X_156=W_150 | X5_148=W_150 | X6_149=W_150 | W_150=V_158 | X_156=V_158 | X5_148=V_158 | X6_149=V_158 | V_158=U_152 | W_150=U_152 | X_156=U_152 | X5_148=U_152 | X6_149=U_152 | six(X3_151, X4_159) | ~member(X3_151, X6_149, X4_159) | ~member(X3_151, X5_148, X4_159) | ~member(X3_151, X_156, X4_159) | ~member(X3_151, W_150, X4_159) | ~member(X3_151, V_158, X4_159) | ~member(X3_151, U_152, X4_159) | skf21(U_152, V_158, W_150, X_156, Y_157, Z_153, X1_154, X2_155)!=X_156))). % 68.90/58.93 tff(c_134, plain, (![W_136, U_134, V_135]: (skf20(W_136, U_134)=V_135 | skf18(W_136, U_134)=V_135 | skf16(W_136, U_134)=V_135 | skf14(W_136, U_134)=V_135 | skf12(W_136, U_134)=V_135 | skf10(W_136, U_134)=V_135 | ~six(U_134, W_136) | ~member(U_134, V_135, W_136)))). % 68.90/58.93 tff(c_1141, plain, (~member(skc7, skc12, skc10))). % 68.90/58.93 tff(c_1132, plain, (![U_231]: (~agent(skc7, skf8(U_231), U_231) | ~member(skc7, U_231, skc10)))). % 68.90/58.93 tff(c_1135, plain, (~agent(skc7, skc8, skc9))). % 68.90/58.93 tff(c_132, plain, (![U_131, V_132, W_133]: (~agent(U_131, V_132, W_133) | ~patient(U_131, V_132, W_133) | ~nonreflexive(U_131, V_132)))). % 68.90/58.93 tff(c_1122, plain, (skf16(skc10, skc7)!=skf10(skc10, skc7))). % 68.90/58.93 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf16(U_119, V_120)!=skf10(U_119, V_120)))). % 68.90/58.93 tff(c_1113, plain, (skf20(skc10, skc7)!=skf14(skc10, skc7))). % 68.90/58.93 tff(c_1117, plain, (act(skc7, skf10(skc10, skc7)))). % 68.90/58.93 tff(c_1108, plain, (action(skc7, skf10(skc10, skc7)))). % 68.90/58.93 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf14(U_105, V_106)))). % 68.90/58.93 tff(c_1104, plain, (shot(skc7, skf10(skc10, skc7)))). % 68.90/58.93 tff(c_100, plain, (![U_99, V_100]: (member(U_99, skf10(V_100, U_99), V_100) | ~six(U_99, V_100)))). % 68.90/58.93 tff(c_1095, plain, (skf20(skc10, skc7)!=skf10(skc10, skc7))). % 68.90/58.93 tff(c_194, plain, (![U_231]: (patient(skc7, skf8(U_231), U_231) | ~member(skc7, U_231, skc10)))). % 68.90/58.93 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf10(U_101, V_102)))). % 68.90/58.93 tff(c_1090, plain, (skf12(skc10, skc7)!=skf10(skc10, skc7))). % 68.90/58.93 tff(c_130, plain, (![V_130, U_129]: (~six(V_130, U_129) | skf12(U_129, V_130)!=skf10(U_129, V_130)))). % 68.90/58.93 tff(c_1085, plain, (skf14(skc10, skc7)!=skf10(skc10, skc7))). % 68.90/58.93 tff(c_1080, plain, (skf18(skc10, skc7)!=skf16(skc10, skc7))). % 68.90/58.93 tff(c_126, plain, (![V_126, U_125]: (~six(V_126, U_125) | skf14(U_125, V_126)!=skf10(U_125, V_126)))). % 68.90/58.94 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf18(U_117, V_118)!=skf16(U_117, V_118)))). % 68.90/58.94 tff(c_1074, plain, (![V_230]: (from_loc(skc7, skf8(V_230), skc11)))). % 68.90/58.94 tff(c_1047, plain, (~act(skc7, skc11))). % 68.90/58.94 tff(c_1031, plain, (![U_272, V_273]: (~act(U_272, V_273) | ~artifact(U_272, V_273)))). % 68.90/58.94 tff(c_1042, plain, (~artifact(skc7, skc9))). % 68.90/58.94 tff(c_994, plain, (![U_272, V_273]: (~cry(U_272, V_273) | ~artifact(U_272, V_273)))). % 68.90/58.94 tff(c_1037, plain, (skf16(skc10, skc7)!=skf14(skc10, skc7))). % 68.90/58.94 tff(c_124, plain, (![V_124, U_123]: (~six(V_124, U_123) | skf16(U_123, V_124)!=skf14(U_123, V_124)))). % 68.90/58.94 tff(c_886, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~act(U_27, V_28)))). % 68.90/58.94 tff(c_1022, plain, (![V_233]: (agent(skc7, skf8(V_233), skc12)))). % 68.90/58.94 tff(c_885, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~cry(U_21, V_22)))). % 68.90/58.94 tff(c_978, plain, (skf16(skc10, skc7)!=skf12(skc10, skc7))). % 68.90/58.94 tff(c_986, plain, (~act(skc7, skc10))). % 68.90/58.94 tff(c_985, plain, (~cry(skc7, skc10))). % 68.90/58.94 tff(c_973, plain, (~event(skc7, skc10))). % 68.90/58.94 tff(c_122, plain, (![V_122, U_121]: (~six(V_122, U_121) | skf16(U_121, V_122)!=skf12(U_121, V_122)))). % 68.90/58.94 tff(c_969, plain, (~eventuality(skc7, skc10))). % 68.90/58.94 tff(c_810, plain, (![U_320, V_321]: (~eventuality(U_320, V_321) | ~group(U_320, V_321)))). % 68.90/58.94 tff(c_964, plain, (skf18(skc10, skc7)!=skf14(skc10, skc7))). % 68.90/58.94 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf18(U_115, V_116)!=skf14(U_115, V_116)))). % 68.90/58.94 tff(c_959, plain, (act(skc7, skf18(skc10, skc7)))). % 68.90/58.94 tff(c_955, plain, (act(skc7, skf20(skc10, skc7)))). % 68.90/58.94 tff(c_951, plain, (action(skc7, skf18(skc10, skc7)))). % 68.90/58.94 tff(c_939, plain, (action(skc7, skf20(skc10, skc7)))). % 68.90/58.94 tff(c_947, plain, (shot(skc7, skf18(skc10, skc7)))). % 68.90/58.94 tff(c_92, plain, (![U_91, V_92]: (member(U_91, skf18(V_92, U_91), V_92) | ~six(U_91, V_92)))). % 68.90/58.94 tff(c_931, plain, (shot(skc7, skf20(skc10, skc7)))). % 68.90/58.94 tff(c_935, plain, (~artifact(skc7, skc10))). % 68.90/58.94 tff(c_923, plain, (~entity(skc7, skc10))). % 68.90/58.94 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf20(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 68.90/58.94 tff(c_805, plain, (![U_320, V_321]: (~entity(U_320, V_321) | ~group(U_320, V_321)))). % 68.90/58.94 tff(c_896, plain, (skf20(skc10, skc7)!=skf18(skc10, skc7))). % 68.90/58.94 tff(c_918, plain, (act(skc7, skf12(skc10, skc7)))). % 68.90/58.94 tff(c_914, plain, (action(skc7, skf12(skc10, skc7)))). % 68.90/58.94 tff(c_910, plain, (shot(skc7, skf12(skc10, skc7)))). % 68.90/58.94 tff(c_98, plain, (![U_97, V_98]: (member(U_97, skf12(V_98, U_97), V_98) | ~six(U_97, V_98)))). % 68.90/58.94 tff(c_901, plain, (![V_541]: (~artifact(skc7, skf8(V_541))))). % 68.90/58.94 tff(c_884, plain, (![V_228]: (~entity(skc7, skf8(V_228))))). % 68.90/58.94 tff(c_891, plain, (~artifact(skc7, skc8))). % 68.90/58.94 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf20(U_109, V_110)!=skf18(U_109, V_110)))). % 68.90/58.94 tff(c_887, plain, (~entity(skc7, skc8))). % 68.90/58.94 tff(c_846, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~event(U_7, V_8)))). % 68.90/58.94 tff(c_784, plain, (![U_244, V_245]: (~artifact(U_244, V_245) | ~human_person(U_244, V_245)))). % 68.90/58.94 tff(c_865, plain, (skf18(skc10, skc7)!=skf12(skc10, skc7))). % 68.90/58.94 tff(c_860, plain, (~animate(skc7, skc11))). % 68.90/58.94 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf12(U_113, V_114)))). % 68.90/58.94 tff(c_856, plain, (artifact(skc7, skc11))). % 68.90/58.94 tff(c_841, plain, (![U_525, V_526]: (artifact(U_525, V_526) | ~cannon(U_525, V_526)))). % 68.90/58.94 tff(c_851, plain, (skf14(skc10, skc7)!=skf12(skc10, skc7))). % 68.90/58.94 tff(c_128, plain, (![V_128, U_127]: (~six(V_128, U_127) | skf14(U_127, V_128)!=skf12(U_127, V_128)))). % 68.90/58.94 tff(c_443, plain, (![U_55, V_56]: (~eventuality(U_55, V_56) | ~entity(U_55, V_56)))). % 68.90/58.94 tff(c_766, plain, (![U_39, V_40]: (instrumentality(U_39, V_40) | ~cannon(U_39, V_40)))). % 68.90/58.94 tff(c_836, plain, (act(skc7, skf16(skc10, skc7)))). % 68.90/58.94 tff(c_832, plain, (action(skc7, skf16(skc10, skc7)))). % 68.90/58.94 tff(c_828, plain, (shot(skc7, skf16(skc10, skc7)))). % 68.90/58.94 tff(c_94, plain, (![U_93, V_94]: (member(U_93, skf16(V_94, U_93), V_94) | ~six(U_93, V_94)))). % 68.90/58.94 tff(c_820, plain, (~artifact(skc7, skc12))). % 68.90/58.94 tff(c_773, plain, (![U_47, V_48]: (~male(U_47, V_48) | ~artifact(U_47, V_48)))). % 68.90/58.94 tff(c_815, plain, (skf20(skc10, skc7)!=skf12(skc10, skc7))). % 68.90/58.94 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf12(U_103, V_104)))). % 68.90/58.94 tff(c_525, plain, (![U_407, V_408]: (~multiple(U_407, V_408) | ~eventuality(U_407, V_408)))). % 68.90/58.94 tff(c_530, plain, (![U_409, V_410]: (~multiple(U_409, V_410) | ~entity(U_409, V_410)))). % 68.90/58.94 tff(c_800, plain, (act(skc7, skf14(skc10, skc7)))). % 68.90/58.94 tff(c_796, plain, (action(skc7, skf14(skc10, skc7)))). % 68.90/58.94 tff(c_792, plain, (shot(skc7, skf14(skc10, skc7)))). % 68.90/58.94 tff(c_96, plain, (![U_95, V_96]: (member(U_95, skf14(V_96, U_95), V_96) | ~six(U_95, V_96)))). % 68.90/58.94 tff(c_756, plain, (![U_495, V_496]: (~living(U_495, V_496) | ~artifact(U_495, V_496)))). % 68.90/58.94 tff(c_755, plain, (![U_495, V_496]: (~animate(U_495, V_496) | ~artifact(U_495, V_496)))). % 68.90/58.94 tff(c_778, plain, (skf20(skc10, skc7)!=skf16(skc10, skc7))). % 68.90/58.94 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf16(U_107, V_108)))). % 68.90/58.94 tff(c_761, plain, (skf18(skc10, skc7)!=skf10(skc10, skc7))). % 68.90/58.94 tff(c_308, plain, (![U_61, V_62]: (~male(U_61, V_62) | ~object(U_61, V_62)))). % 68.90/58.95 tff(c_252, plain, (![U_272, V_273]: (impartial(U_272, V_273) | ~artifact(U_272, V_273)))). % 68.90/58.95 tff(c_253, plain, (![U_272, V_273]: (entity(U_272, V_273) | ~artifact(U_272, V_273)))). % 68.90/58.95 tff(c_276, plain, (![U_284, V_285]: (instrumentality(U_284, V_285) | ~weapon(U_284, V_285)))). % 68.90/58.95 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf10(U_111, V_112)))). % 68.90/58.95 tff(c_251, plain, (![U_272, V_273]: (nonliving(U_272, V_273) | ~artifact(U_272, V_273)))). % 68.90/58.95 tff(c_746, plain, (![V_226]: (present(skc7, skf8(V_226))))). % 68.90/58.95 tff(c_641, plain, (entity(skc7, skc12))). % 68.90/58.95 tff(c_217, plain, (![U_65, V_66]: (entity(U_65, V_66) | ~human_person(U_65, V_66)))). % 68.90/58.95 tff(c_240, plain, (![U_65, V_66]: (impartial(U_65, V_66) | ~human_person(U_65, V_66)))). % 68.90/58.95 tff(c_629, plain, (![V_222]: (fire(skc7, skf8(V_222))))). % 68.90/58.95 tff(c_321, plain, (![U_51, V_52]: (singleton(U_51, V_52) | ~entity(U_51, V_52)))). % 68.90/58.95 tff(c_326, plain, (![U_318, V_319]: (singleton(U_318, V_319) | ~eventuality(U_318, V_319)))). % 68.90/58.95 tff(c_211, plain, (![U_244, V_245]: (living(U_244, V_245) | ~human_person(U_244, V_245)))). % 68.90/58.95 tff(c_518, plain, (![V_224]: (nonreflexive(skc7, skf8(V_224))))). % 68.90/58.95 tff(c_298, plain, (![U_15, V_16]: (~existent(U_15, V_16) | ~eventuality(U_15, V_16)))). % 68.90/58.95 tff(c_331, plain, (![U_320, V_321]: (multiple(U_320, V_321) | ~group(U_320, V_321)))). % 68.90/58.95 tff(c_436, plain, (![V_228]: (event(skc7, skf8(V_228))))). % 68.90/58.95 tff(c_349, plain, (~act(skc7, skc12))). % 68.90/58.95 tff(c_348, plain, (~cry(skc7, skc12))). % 68.90/58.95 tff(c_341, plain, (~event(skc7, skc12))). % 68.90/58.95 tff(c_337, plain, (~eventuality(skc7, skc12))). % 68.90/58.95 tff(c_307, plain, (![U_17, V_18]: (~male(U_17, V_18) | ~eventuality(U_17, V_18)))). % 68.90/58.95 tff(c_182, plain, (![U_220]: (shot(skc7, U_220) | ~member(skc7, U_220, skc10)))). % 68.90/58.95 tff(c_32, plain, (![U_31, V_32]: (set(U_31, V_32) | ~group(U_31, V_32)))). % 68.90/58.95 tff(c_10, plain, (![U_9, V_10]: (thing(U_9, V_10) | ~eventuality(U_9, V_10)))). % 68.90/58.95 tff(c_12, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~thing(U_11, V_12)))). % 68.90/58.95 tff(c_20, plain, (![U_19, V_20]: (event(U_19, V_20) | ~scream(U_19, V_20)))). % 68.90/58.95 tff(c_22, plain, (![U_21, V_22]: (event(U_21, V_22) | ~cry(U_21, V_22)))). % 68.90/58.95 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~act(U_27, V_28)))). % 68.90/58.95 tff(c_80, plain, (![U_79, V_80]: (~unisex(U_79, V_80) | ~male(U_79, V_80)))). % 68.90/58.95 tff(c_8, plain, (![U_7, V_8]: (eventuality(U_7, V_8) | ~event(U_7, V_8)))). % 68.90/58.95 tff(c_86, plain, (![U_85, V_86]: (~existent(U_85, V_86) | ~nonexistent(U_85, V_86)))). % 68.90/58.95 tff(c_88, plain, (![U_87, V_88]: (~animate(U_87, V_88) | ~nonliving(U_87, V_88)))). % 68.90/58.95 tff(c_6, plain, (![U_5, V_6]: (event(U_5, V_6) | ~sound(U_5, V_6)))). % 68.90/58.95 tff(c_18, plain, (![U_17, V_18]: (unisex(U_17, V_18) | ~eventuality(U_17, V_18)))). % 68.90/58.95 tff(c_4, plain, (![U_3, V_4]: (sound(U_3, V_4) | ~scream(U_3, V_4)))). % 68.90/58.95 tff(c_82, plain, (![U_81, V_82]: (~singleton(U_81, V_82) | ~multiple(U_81, V_82)))). % 68.90/58.95 tff(c_30, plain, (![U_29, V_30]: (action(U_29, V_30) | ~shot(U_29, V_30)))). % 68.90/58.95 tff(c_14, plain, (![U_13, V_14]: (specific(U_13, V_14) | ~eventuality(U_13, V_14)))). % 68.90/58.95 tff(c_84, plain, (![U_83, V_84]: (~nonliving(U_83, V_84) | ~living(U_83, V_84)))). % 68.90/58.95 tff(c_281, plain, (human(skc7, skc12))). % 68.90/58.95 tff(c_74, plain, (![U_73, V_74]: (human(U_73, V_74) | ~human_person(U_73, V_74)))). % 68.90/58.95 tff(c_42, plain, (![U_41, V_42]: (weaponry(U_41, V_42) | ~weapon(U_41, V_42)))). % 68.90/58.95 tff(c_271, plain, (animate(skc7, skc12))). % 68.90/58.95 tff(c_76, plain, (![U_75, V_76]: (animate(U_75, V_76) | ~human_person(U_75, V_76)))). % 68.90/58.95 tff(c_78, plain, (![U_77, V_78]: (male(U_77, V_78) | ~man(U_77, V_78)))). % 68.90/58.95 tff(c_260, plain, (act(skc7, skc14))). % 68.90/58.95 tff(c_26, plain, (![U_25, V_26]: (act(U_25, V_26) | ~action(U_25, V_26)))). % 68.90/58.95 tff(c_34, plain, (![U_33, V_34]: (multiple(U_33, V_34) | ~set(U_33, V_34)))). % 68.90/58.95 tff(c_52, plain, (![U_51, V_52]: (thing(U_51, V_52) | ~entity(U_51, V_52)))). % 68.90/58.95 tff(c_48, plain, (![U_47, V_48]: (object(U_47, V_48) | ~artifact(U_47, V_48)))). % 68.90/58.95 tff(c_70, plain, (![U_69, V_70]: (impartial(U_69, V_70) | ~organism(U_69, V_70)))). % 68.90/58.95 tff(c_58, plain, (![U_57, V_58]: (nonliving(U_57, V_58) | ~object(U_57, V_58)))). % 68.90/58.95 tff(c_56, plain, (![U_55, V_56]: (existent(U_55, V_56) | ~entity(U_55, V_56)))). % 68.90/58.95 tff(c_54, plain, (![U_53, V_54]: (specific(U_53, V_54) | ~entity(U_53, V_54)))). % 68.90/58.95 tff(c_46, plain, (![U_45, V_46]: (artifact(U_45, V_46) | ~instrumentality(U_45, V_46)))). % 68.90/58.95 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~object(U_59, V_60)))). % 68.90/58.95 tff(c_50, plain, (![U_49, V_50]: (entity(U_49, V_50) | ~object(U_49, V_50)))). % 68.90/58.95 tff(c_62, plain, (![U_61, V_62]: (unisex(U_61, V_62) | ~object(U_61, V_62)))). % 68.90/58.95 tff(c_228, plain, (action(skc7, skc14))). % 68.90/58.95 tff(c_24, plain, (![U_23, V_24]: (action(U_23, V_24) | ~revenge(U_23, V_24)))). % 68.90/58.95 tff(c_222, plain, (human_person(skc7, skc12))). % 68.90/58.95 tff(c_44, plain, (![U_43, V_44]: (instrumentality(U_43, V_44) | ~weaponry(U_43, V_44)))). % 68.90/58.95 tff(c_64, plain, (![U_63, V_64]: (human_person(U_63, V_64) | ~man(U_63, V_64)))). % 68.90/58.95 tff(c_68, plain, (![U_67, V_68]: (entity(U_67, V_68) | ~organism(U_67, V_68)))). % 68.90/58.95 tff(c_38, plain, (![U_37, V_38]: (event(U_37, V_38) | ~fire(U_37, V_38)))). % 68.90/58.95 tff(c_66, plain, (![U_65, V_66]: (organism(U_65, V_66) | ~human_person(U_65, V_66)))). % 68.90/58.95 tff(c_16, plain, (![U_15, V_16]: (nonexistent(U_15, V_16) | ~eventuality(U_15, V_16)))). % 68.90/58.95 tff(c_40, plain, (![U_39, V_40]: (weapon(U_39, V_40) | ~cannon(U_39, V_40)))). % 68.90/58.95 tff(c_72, plain, (![U_71, V_72]: (living(U_71, V_72) | ~organism(U_71, V_72)))). % 68.90/58.95 tff(c_36, plain, (![U_35, V_36]: (group(U_35, V_36) | ~six(U_35, V_36)))). % 68.90/58.95 tff(c_180, plain, (patient(skc7, skc8, skc9))). % 68.90/58.95 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 68.90/58.95 tff(c_174, plain, (of(skc7, skc8, skc14))). % 68.90/58.95 tff(c_176, plain, (of(skc7, skc11, skc12))). % 68.90/58.96 tff(c_178, plain, (agent(skc7, skc8, skc12))). % 68.90/58.96 tff(c_154, plain, (man(skc7, skc12))). % 68.90/58.96 tff(c_156, plain, (cannon(skc7, skc11))). % 68.90/58.96 tff(c_152, plain, (male(skc7, skc12))). % 68.90/58.96 tff(c_172, plain, (revenge(skc7, skc14))). % 68.90/58.96 tff(c_170, plain, (event(skc7, skc8))). % 68.90/58.96 tff(c_168, plain, (present(skc7, skc8))). % 68.90/58.96 tff(c_158, plain, (cry(skc7, skc9))). % 68.90/58.96 tff(c_160, plain, (six(skc7, skc10))). % 68.90/58.96 tff(c_162, plain, (group(skc7, skc10))). % 68.90/58.96 tff(c_164, plain, (scream(skc7, skc8))). % 68.90/58.96 tff(c_166, plain, (nonreflexive(skc7, skc8))). % 68.90/58.96 tff(c_150, plain, (actual_world(skc7))). % 68.90/58.96 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.90/58.96 %------------------------------------------------------------------------------