%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP085-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 : n008.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:09 PM UTC 2025 % Result : Satisfiable 67.00s 56.90s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP085-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:26:47 EDT 2025 % 0.12/0.34 % CPUTime : % 67.00/56.89 % 67.00/56.90 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 67.00/56.90 % 67.00/56.90 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 67.00/56.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 % 67.00/56.91 % 67.00/56.91 %Foreground sorts: % 67.00/56.91 % 67.00/56.91 % 67.00/56.91 %Background operators: % 67.00/56.91 % 67.00/56.91 % 67.00/56.91 %Foreground operators: % 67.00/56.91 tff(nonliving, type, nonliving: ($i * $i) > $o). % 67.00/56.91 tff(skf10, type, skf10: ($i * $i) > $i). % 67.00/56.91 tff(member, type, member: ($i * $i * $i) > $o). % 67.00/56.91 tff(skc7, type, skc7: $i). % 67.00/56.91 tff(living, type, living: ($i * $i) > $o). % 67.00/56.91 tff(fire, type, fire: ($i * $i) > $o). % 67.00/56.91 tff(human_person, type, human_person: ($i * $i) > $o). % 67.00/56.91 tff(action, type, action: ($i * $i) > $o). % 67.00/56.91 tff(present, type, present: ($i * $i) > $o). % 67.00/56.91 tff(shot, type, shot: ($i * $i) > $o). % 67.00/56.91 tff(skc11, type, skc11: $i). % 67.00/56.91 tff(entity, type, entity: ($i * $i) > $o). % 67.00/56.91 tff(skc9, type, skc9: $i). % 67.00/56.91 tff(eventuality, type, eventuality: ($i * $i) > $o). % 67.00/56.91 tff(weapon, type, weapon: ($i * $i) > $o). % 67.00/56.91 tff(existent, type, existent: ($i * $i) > $o). % 67.00/56.91 tff(skc8, type, skc8: $i). % 67.00/56.91 tff(scream, type, scream: ($i * $i) > $o). % 67.00/56.91 tff(skc14, type, skc14: $i). % 67.00/56.91 tff(singleton, type, singleton: ($i * $i) > $o). % 67.00/56.91 tff(male, type, male: ($i * $i) > $o). % 67.00/56.91 tff(skf8, type, skf8: $i > $i). % 67.00/56.91 tff(multiple, type, multiple: ($i * $i) > $o). % 67.00/56.91 tff(organism, type, organism: ($i * $i) > $o). % 67.00/56.91 tff(animate, type, animate: ($i * $i) > $o). % 67.00/56.91 tff(of, type, of: ($i * $i * $i) > $o). % 67.00/56.91 tff(skf14, type, skf14: ($i * $i) > $i). % 67.00/56.91 tff(actual_world, type, actual_world: $i > $o). % 67.00/56.91 tff(agent, type, agent: ($i * $i * $i) > $o). % 67.00/56.91 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 67.00/56.91 tff(group, type, group: ($i * $i) > $o). % 67.00/56.91 tff(revenge, type, revenge: ($i * $i) > $o). % 67.00/56.91 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 67.00/56.91 tff(artifact, type, artifact: ($i * $i) > $o). % 67.00/56.91 tff(cannon, type, cannon: ($i * $i) > $o). % 67.00/56.91 tff(cry, type, cry: ($i * $i) > $o). % 67.00/56.91 tff(event, type, event: ($i * $i) > $o). % 67.00/56.91 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 67.00/56.91 tff(patient, type, patient: ($i * $i * $i) > $o). % 67.00/56.91 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 67.00/56.91 tff(thing, type, thing: ($i * $i) > $o). % 67.00/56.91 tff(human, type, human: ($i * $i) > $o). % 67.00/56.91 tff(six, type, six: ($i * $i) > $o). % 67.00/56.91 tff(skf18, type, skf18: ($i * $i) > $i). % 67.00/56.91 tff(man, type, man: ($i * $i) > $o). % 67.00/56.91 tff(sound, type, sound: ($i * $i) > $o). % 67.00/56.91 tff(weaponry, type, weaponry: ($i * $i) > $o). % 67.00/56.91 tff(unisex, type, unisex: ($i * $i) > $o). % 67.00/56.91 tff(skf16, type, skf16: ($i * $i) > $i). % 67.00/56.91 tff(set, type, set: ($i * $i) > $o). % 67.00/56.91 tff(skf12, type, skf12: ($i * $i) > $i). % 67.00/56.91 tff(impartial, type, impartial: ($i * $i) > $o). % 67.00/56.91 tff(object, type, object: ($i * $i) > $o). % 67.00/56.91 tff(skc12, type, skc12: $i). % 67.00/56.91 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 67.00/56.91 tff(specific, type, specific: ($i * $i) > $o). % 67.00/56.91 tff(skf20, type, skf20: ($i * $i) > $i). % 67.00/56.91 tff(skc10, type, skc10: $i). % 67.00/56.91 tff(act, type, act: ($i * $i) > $o). % 67.00/56.91 % 67.00/56.91 %Saturated clause set: % 67.00/56.91 tff(c_1552, plain, (![Y_1080, Y_1064, Y_1086, X_1068, X1_1066, X1_1085, X1_1069, Y_1091, X2_1075, Z_1089, X2_1077, X_1060, Z_1057, U_203, X1_1058, X_1078, V_1096, V_1074, Z_204, X_1090, W_1070, Y_208, Z_1082, W_202, Z_1081, X1_1076, V_1059, X2_1092, V_1088, X1_205, X_1095, X2_206, X_1061, Y_1087, V_209, Z_1065, V_1083, X_207, V_1072, X2_1067, X1_1079, X2_1071, X2_1093, Y_1062, Z_1084]: (skf21(V_1096, X_1095, Y_1087, Z_1065, X1_1066, X2_1067, W_202, U_203)=skf21(V_1088, X_1060, Y_1062, Z_1089, X1_1085, X2_1077, W_202, U_203) | skf21(V_1096, X_1095, Y_1087, Z_1065, X1_1066, X2_1067, W_202, U_203)=skf21(V_1074, X_1090, Y_1080, Z_1082, X1_1058, X2_1093, W_202, U_203) | skf21(V_1088, X_1060, Y_1062, Z_1089, X1_1085, X2_1077, W_202, U_203)=skf21(V_1074, X_1090, Y_1080, Z_1082, X1_1058, X2_1093, W_202, U_203) | skf21(V_1083, X_1061, Y_1086, Z_1081, X1_1069, X2_1092, W_202, U_203)=skf21(V_1074, X_1090, Y_1080, Z_1082, X1_1058, X2_1093, W_202, U_203) | skf21(V_1096, X_1095, Y_1087, Z_1065, X1_1066, X2_1067, W_202, U_203)=skf21(V_1083, X_1061, Y_1086, Z_1081, X1_1069, X2_1092, W_202, U_203) | skf21(V_1088, X_1060, Y_1062, Z_1089, X1_1085, X2_1077, W_202, U_203)=skf21(V_1083, X_1061, Y_1086, Z_1081, X1_1069, X2_1092, W_202, U_203) | skf21(V_1083, X_1061, Y_1086, Z_1081, X1_1069, X2_1092, W_202, U_203)=skf21(V_1072, X_1068, Y_1091, Z_1057, X1_1076, X2_1075, W_202, U_203) | skf21(V_1074, X_1090, Y_1080, Z_1082, X1_1058, X2_1093, W_202, U_203)=skf21(V_1072, X_1068, Y_1091, Z_1057, X1_1076, X2_1075, W_202, U_203) | skf21(V_1096, X_1095, Y_1087, Z_1065, X1_1066, X2_1067, W_202, U_203)=skf21(V_1072, X_1068, Y_1091, Z_1057, X1_1076, X2_1075, W_202, U_203) | skf21(V_1088, X_1060, Y_1062, Z_1089, X1_1085, X2_1077, W_202, U_203)=skf21(V_1072, X_1068, Y_1091, Z_1057, X1_1076, X2_1075, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1072, X_1068, Y_1091, Z_1057, X1_1076, X2_1075, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1083, X_1061, Y_1086, Z_1081, X1_1069, X2_1092, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1074, X_1090, Y_1080, Z_1082, X1_1058, X2_1093, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1096, X_1095, Y_1087, Z_1065, X1_1066, X2_1067, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1088, X_1060, Y_1062, Z_1089, X1_1085, X2_1077, W_202, U_203) | skf21(skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), V_1059, W_1070, X_1078, Y_1064, Z_1084, X1_1079, X2_1071)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_1077=X1_1085 | Z_1089=X1_1085 | Z_1089=X2_1077 | Z_1089=Y_1062 | Y_1062=X1_1085 | Y_1062=X2_1077 | Y_1062=X_1060 | Z_1089=X_1060 | X_1060=X1_1085 | X_1060=X2_1077 | X_1060=V_1088 | Y_1062=V_1088 | Z_1089=V_1088 | X1_1085=V_1088 | X2_1077=V_1088 | ~member(U_203, X2_1077, W_202) | ~member(U_203, X1_1085, W_202) | ~member(U_203, Z_1089, W_202) | ~member(U_203, Y_1062, W_202) | ~member(U_203, X_1060, W_202) | ~member(U_203, V_1088, W_202) | X2_1067=X1_1066 | Z_1065=X1_1066 | Z_1065=X2_1067 | Z_1065=Y_1087 | Y_1087=X1_1066 | Y_1087=X2_1067 | Y_1087=X_1095 | Z_1065=X_1095 | X_1095=X1_1066 | X_1095=X2_1067 | X_1095=V_1096 | Y_1087=V_1096 | Z_1065=V_1096 | X1_1066=V_1096 | X2_1067=V_1096 | ~member(U_203, X2_1067, W_202) | ~member(U_203, X1_1066, W_202) | ~member(U_203, Z_1065, W_202) | ~member(U_203, Y_1087, W_202) | ~member(U_203, X_1095, W_202) | ~member(U_203, V_1096, W_202) | X2_1093=X1_1058 | Z_1082=X1_1058 | Z_1082=X2_1093 | Z_1082=Y_1080 | Y_1080=X1_1058 | Y_1080=X2_1093 | Y_1080=X_1090 | Z_1082=X_1090 | X_1090=X1_1058 | X_1090=X2_1093 | X_1090=V_1074 | Y_1080=V_1074 | Z_1082=V_1074 | X1_1058=V_1074 | X2_1093=V_1074 | ~member(U_203, X2_1093, W_202) | ~member(U_203, X1_1058, W_202) | ~member(U_203, Z_1082, W_202) | ~member(U_203, Y_1080, W_202) | ~member(U_203, X_1090, W_202) | ~member(U_203, V_1074, W_202) | X2_1092=X1_1069 | Z_1081=X1_1069 | Z_1081=X2_1092 | Z_1081=Y_1086 | Y_1086=X1_1069 | Y_1086=X2_1092 | Y_1086=X_1061 | Z_1081=X_1061 | X_1061=X1_1069 | X_1061=X2_1092 | X_1061=V_1083 | Y_1086=V_1083 | Z_1081=V_1083 | X1_1069=V_1083 | X2_1092=V_1083 | ~member(U_203, X2_1092, W_202) | ~member(U_203, X1_1069, W_202) | ~member(U_203, Z_1081, W_202) | ~member(U_203, Y_1086, W_202) | ~member(U_203, X_1061, W_202) | ~member(U_203, V_1083, W_202) | X2_1075=X1_1076 | Z_1057=X1_1076 | Z_1057=X2_1075 | Z_1057=Y_1091 | Y_1091=X1_1076 | Y_1091=X2_1075 | Y_1091=X_1068 | Z_1057=X_1068 | X_1068=X1_1076 | X_1068=X2_1075 | X_1068=V_1072 | Y_1091=V_1072 | Z_1057=V_1072 | X1_1076=V_1072 | X2_1075=V_1072 | ~member(U_203, X2_1075, W_202) | ~member(U_203, X1_1076, W_202) | ~member(U_203, Z_1057, W_202) | ~member(U_203, Y_1091, W_202) | ~member(U_203, X_1068, W_202) | ~member(U_203, V_1072, 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)))). % 67.00/56.92 tff(c_1507, plain, (![X1_975, X2_988, X1_959, U_203, Z_958, Y_955, X1_980, V_977, Z_204, X2_982, Y_208, Y_984, X2_971, V_979, V_968, W_202, Y_967, Z_986, X_957, Y_973, Y_983, X1_205, X1_972, X_965, X_976, U_961, X2_970, X2_206, X2_981, V_209, Z_956, Z_985, X_207, Z_963, W_974, V_964, X_966, X_960, X1_969]: (skf21(V_979, X_976, Y_967, Z_985, X1_969, X2_970, W_202, U_203)=skf21(V_977, X_960, Y_984, Z_963, X1_959, X2_988, W_202, U_203) | skf21(V_979, X_976, Y_967, Z_985, X1_969, X2_970, W_202, U_203)=skf21(V_964, X_965, Y_955, Z_956, X1_975, X2_982, W_202, U_203) | skf21(V_977, X_960, Y_984, Z_963, X1_959, X2_988, W_202, U_203)=skf21(V_964, X_965, Y_955, Z_956, X1_975, X2_982, W_202, U_203) | skf21(V_968, X_966, Y_983, Z_958, X1_972, X2_971, W_202, U_203)=skf21(V_964, X_965, Y_955, Z_956, X1_975, X2_982, W_202, U_203) | skf21(V_979, X_976, Y_967, Z_985, X1_969, X2_970, W_202, U_203)=skf21(V_968, X_966, Y_983, Z_958, X1_972, X2_971, W_202, U_203) | skf21(V_977, X_960, Y_984, Z_963, X1_959, X2_988, W_202, U_203)=skf21(V_968, X_966, Y_983, Z_958, X1_972, X2_971, W_202, U_203) | skf21(V_968, X_966, Y_983, Z_958, X1_972, X2_971, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_964, X_965, Y_955, Z_956, X1_975, X2_982, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_979, X_976, Y_967, Z_985, X1_969, X2_970, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_977, X_960, Y_984, Z_963, X1_959, X2_988, 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)=U_961 | skf21(V_968, X_966, Y_983, Z_958, X1_972, X2_971, W_202, U_203)=U_961 | skf21(V_964, X_965, Y_955, Z_956, X1_975, X2_982, W_202, U_203)=U_961 | skf21(V_979, X_976, Y_967, Z_985, X1_969, X2_970, W_202, U_203)=U_961 | skf21(V_977, X_960, Y_984, Z_963, X1_959, X2_988, W_202, U_203)=U_961 | ~member(U_203, U_961, W_202) | skf21(U_961, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), W_974, X_957, Y_973, Z_986, X1_980, X2_981)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_988=X1_959 | Z_963=X1_959 | Z_963=X2_988 | Z_963=Y_984 | Y_984=X1_959 | Y_984=X2_988 | Y_984=X_960 | Z_963=X_960 | X_960=X1_959 | X_960=X2_988 | X_960=V_977 | Y_984=V_977 | Z_963=V_977 | X1_959=V_977 | X2_988=V_977 | ~member(U_203, X2_988, W_202) | ~member(U_203, X1_959, W_202) | ~member(U_203, Z_963, W_202) | ~member(U_203, Y_984, W_202) | ~member(U_203, X_960, W_202) | ~member(U_203, V_977, W_202) | X2_970=X1_969 | Z_985=X1_969 | Z_985=X2_970 | Z_985=Y_967 | Y_967=X1_969 | Y_967=X2_970 | Y_967=X_976 | Z_985=X_976 | X_976=X1_969 | X_976=X2_970 | X_976=V_979 | Y_967=V_979 | Z_985=V_979 | X1_969=V_979 | X2_970=V_979 | ~member(U_203, X2_970, W_202) | ~member(U_203, X1_969, W_202) | ~member(U_203, Z_985, W_202) | ~member(U_203, Y_967, W_202) | ~member(U_203, X_976, W_202) | ~member(U_203, V_979, W_202) | X2_982=X1_975 | Z_956=X1_975 | Z_956=X2_982 | Z_956=Y_955 | Y_955=X1_975 | Y_955=X2_982 | Y_955=X_965 | Z_956=X_965 | X_965=X1_975 | X_965=X2_982 | X_965=V_964 | Y_955=V_964 | Z_956=V_964 | X1_975=V_964 | X2_982=V_964 | ~member(U_203, X2_982, W_202) | ~member(U_203, X1_975, W_202) | ~member(U_203, Z_956, W_202) | ~member(U_203, Y_955, W_202) | ~member(U_203, X_965, W_202) | ~member(U_203, V_964, W_202) | X2_971=X1_972 | Z_958=X1_972 | Z_958=X2_971 | Z_958=Y_983 | Y_983=X1_972 | Y_983=X2_971 | Y_983=X_966 | Z_958=X_966 | X_966=X1_972 | X_966=X2_971 | X_966=V_968 | Y_983=V_968 | Z_958=V_968 | X1_972=V_968 | X2_971=V_968 | ~member(U_203, X2_971, W_202) | ~member(U_203, X1_972, W_202) | ~member(U_203, Z_958, W_202) | ~member(U_203, Y_983, W_202) | ~member(U_203, X_966, W_202) | ~member(U_203, V_968, 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)))). % 67.00/56.92 tff(c_1529, plain, (![V_1012, X1_1007, V_1016, V_999, X2_1014, Y_998, U_203, Y_1002, V_1004, X_995, X1_994, Y_1020, X2_1000, V_1008, X_1018, X_991, Z_204, X1_1003, X2_1015, Y_208, Z_1023, Y_992, W_202, Z_993, X1_1005, Z_1022, X1_205, X2_1010, X2_997, W_1019, X2_206, X1_1011, V_209, Y_990, X_207, X_1017, Z_989, Z_996, X_1006, U_1013]: (skf21(V_999, X_1018, Y_1002, Z_1023, X1_994, X2_1014, W_202, U_203)=skf21(V_1004, X_1017, Y_998, Z_1022, X1_1005, X2_1000, W_202, U_203) | skf21(V_999, X_1018, Y_1002, Z_1023, X1_994, X2_1014, W_202, U_203)=skf21(V_1012, X_991, Y_992, Z_989, X1_1003, X2_1015, W_202, U_203) | skf21(V_1012, X_991, Y_992, Z_989, X1_1003, X2_1015, W_202, U_203)=skf21(V_1004, X_1017, Y_998, Z_1022, X1_1005, X2_1000, W_202, U_203) | skf21(V_1012, X_991, Y_992, Z_989, X1_1003, X2_1015, W_202, U_203)=skf21(V_1008, X_1006, Y_1020, Z_993, X1_1011, X2_1010, W_202, U_203) | skf21(V_999, X_1018, Y_1002, Z_1023, X1_994, X2_1014, W_202, U_203)=skf21(V_1008, X_1006, Y_1020, Z_993, X1_1011, X2_1010, W_202, U_203) | skf21(V_1008, X_1006, Y_1020, Z_993, X1_1011, X2_1010, W_202, U_203)=skf21(V_1004, X_1017, Y_998, Z_1022, X1_1005, X2_1000, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1008, X_1006, Y_1020, Z_993, X1_1011, X2_1010, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1012, X_991, Y_992, Z_989, X1_1003, X2_1015, W_202, U_203) | skf21(V_999, X_1018, Y_1002, Z_1023, X1_994, X2_1014, 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)=skf21(V_1004, X_1017, Y_998, Z_1022, X1_1005, X2_1000, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_1013 | skf21(V_1008, X_1006, Y_1020, Z_993, X1_1011, X2_1010, W_202, U_203)=U_1013 | skf21(V_1012, X_991, Y_992, Z_989, X1_1003, X2_1015, W_202, U_203)=U_1013 | skf21(V_999, X_1018, Y_1002, Z_1023, X1_994, X2_1014, W_202, U_203)=U_1013 | skf21(V_1004, X_1017, Y_998, Z_1022, X1_1005, X2_1000, W_202, U_203)=U_1013 | ~member(U_203, U_1013, W_202) | skf21(U_1013, V_1016, W_1019, X_995, Y_990, Z_996, X1_1007, X2_997)!=U_1013 | X2_1000=X1_1005 | Z_1022=X1_1005 | Z_1022=X2_1000 | Z_1022=Y_998 | Y_998=X1_1005 | Y_998=X2_1000 | Y_998=X_1017 | Z_1022=X_1017 | X_1017=X1_1005 | X_1017=X2_1000 | X_1017=V_1004 | Y_998=V_1004 | Z_1022=V_1004 | X1_1005=V_1004 | X2_1000=V_1004 | ~member(U_203, X2_1000, W_202) | ~member(U_203, X1_1005, W_202) | ~member(U_203, Z_1022, W_202) | ~member(U_203, Y_998, W_202) | ~member(U_203, X_1017, W_202) | ~member(U_203, V_1004, W_202) | X2_1014=X1_994 | Z_1023=X1_994 | Z_1023=X2_1014 | Z_1023=Y_1002 | Y_1002=X1_994 | Y_1002=X2_1014 | Y_1002=X_1018 | Z_1023=X_1018 | X_1018=X1_994 | X_1018=X2_1014 | X_1018=V_999 | Y_1002=V_999 | Z_1023=V_999 | X1_994=V_999 | X2_1014=V_999 | ~member(U_203, X2_1014, W_202) | ~member(U_203, X1_994, W_202) | ~member(U_203, Z_1023, W_202) | ~member(U_203, Y_1002, W_202) | ~member(U_203, X_1018, W_202) | ~member(U_203, V_999, W_202) | X2_1015=X1_1003 | Z_989=X1_1003 | Z_989=X2_1015 | Z_989=Y_992 | Y_992=X1_1003 | Y_992=X2_1015 | Y_992=X_991 | Z_989=X_991 | X_991=X1_1003 | X_991=X2_1015 | X_991=V_1012 | Y_992=V_1012 | Z_989=V_1012 | X1_1003=V_1012 | X2_1015=V_1012 | ~member(U_203, X2_1015, W_202) | ~member(U_203, X1_1003, W_202) | ~member(U_203, Z_989, W_202) | ~member(U_203, Y_992, W_202) | ~member(U_203, X_991, W_202) | ~member(U_203, V_1012, W_202) | X2_1010=X1_1011 | Z_993=X1_1011 | Z_993=X2_1010 | Z_993=Y_1020 | Y_1020=X1_1011 | Y_1020=X2_1010 | Y_1020=X_1006 | Z_993=X_1006 | X_1006=X1_1011 | X_1006=X2_1010 | X_1006=V_1008 | Y_1020=V_1008 | Z_993=V_1008 | X1_1011=V_1008 | X2_1010=V_1008 | ~member(U_203, X2_1010, W_202) | ~member(U_203, X1_1011, W_202) | ~member(U_203, Z_993, W_202) | ~member(U_203, Y_1020, W_202) | ~member(U_203, X_1006, W_202) | ~member(U_203, V_1008, 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)))). % 67.00/56.92 tff(c_1440, plain, (![X2_858, V_848, V_862, U_203, Z_846, X1_867, U_843, X_853, X1_844, Y_854, Z_868, X_842, Z_204, X_845, X1_860, Y_857, Y_208, W_202, V_856, Y_863, Z_859, X2_841, X1_205, X2_206, V_209, X_852, Z_847, X2_851, X_207, X1_864, X2_861, V_855, Y_865]: (skf21(V_862, X_845, Y_854, Z_859, X1_844, X2_861, W_202, U_203)=skf21(V_848, X_853, Y_863, Z_868, X1_867, X2_841, W_202, U_203) | skf21(V_856, X_852, Y_865, Z_846, X1_860, X2_858, W_202, U_203)=skf21(V_848, X_853, Y_863, Z_868, X1_867, X2_841, W_202, U_203) | skf21(V_862, X_845, Y_854, Z_859, X1_844, X2_861, W_202, U_203)=skf21(V_856, X_852, Y_865, Z_846, X1_860, X2_858, W_202, U_203) | skf21(V_856, X_852, Y_865, Z_846, X1_860, X2_858, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_848, X_853, Y_863, Z_868, X1_867, X2_841, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_862, X_845, Y_854, Z_859, X1_844, X2_861, 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_855 | skf21(V_856, X_852, Y_865, Z_846, X1_860, X2_858, W_202, U_203)=V_855 | skf21(V_848, X_853, Y_863, Z_868, X1_867, X2_841, W_202, U_203)=V_855 | skf21(V_862, X_845, Y_854, Z_859, X1_844, X2_861, W_202, U_203)=V_855 | V_855=U_843 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_843 | skf21(V_856, X_852, Y_865, Z_846, X1_860, X2_858, W_202, U_203)=U_843 | skf21(V_848, X_853, Y_863, Z_868, X1_867, X2_841, W_202, U_203)=U_843 | skf21(V_862, X_845, Y_854, Z_859, X1_844, X2_861, W_202, U_203)=U_843 | ~member(U_203, V_855, W_202) | ~member(U_203, U_843, W_202) | skf21(U_843, V_855, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), X_842, Y_857, Z_847, X1_864, X2_851)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_861=X1_844 | Z_859=X1_844 | Z_859=X2_861 | Z_859=Y_854 | Y_854=X1_844 | Y_854=X2_861 | Y_854=X_845 | Z_859=X_845 | X_845=X1_844 | X_845=X2_861 | X_845=V_862 | Y_854=V_862 | Z_859=V_862 | X1_844=V_862 | X2_861=V_862 | ~member(U_203, X2_861, W_202) | ~member(U_203, X1_844, W_202) | ~member(U_203, Z_859, W_202) | ~member(U_203, Y_854, W_202) | ~member(U_203, X_845, W_202) | ~member(U_203, V_862, W_202) | X2_841=X1_867 | Z_868=X1_867 | Z_868=X2_841 | Z_868=Y_863 | Y_863=X1_867 | Y_863=X2_841 | Y_863=X_853 | Z_868=X_853 | X_853=X1_867 | X_853=X2_841 | X_853=V_848 | Y_863=V_848 | Z_868=V_848 | X1_867=V_848 | X2_841=V_848 | ~member(U_203, X2_841, W_202) | ~member(U_203, X1_867, W_202) | ~member(U_203, Z_868, W_202) | ~member(U_203, Y_863, W_202) | ~member(U_203, X_853, W_202) | ~member(U_203, V_848, W_202) | X2_858=X1_860 | Z_846=X1_860 | Z_846=X2_858 | Z_846=Y_865 | Y_865=X1_860 | Y_865=X2_858 | Y_865=X_852 | Z_846=X_852 | X_852=X1_860 | X_852=X2_858 | X_852=V_856 | Y_865=V_856 | Z_846=V_856 | X1_860=V_856 | X2_858=V_856 | ~member(U_203, X2_858, W_202) | ~member(U_203, X1_860, W_202) | ~member(U_203, Z_846, W_202) | ~member(U_203, Y_865, W_202) | ~member(U_203, X_852, W_202) | ~member(U_203, V_856, 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)))). % 67.00/56.92 tff(c_1462, plain, (![X1_885, V_872, Y_883, X_876, X_887, V_873, Y_877, U_203, X2_874, W_871, Y_895, Y_884, X1_890, Z_204, V_886, X2_888, Y_208, Z_875, X_894, U_891, W_202, V_878, X2_889, X1_205, Z_893, Z_892, Z_882, X2_206, V_209, X2_880, X5_870, X_207, X_881, X1_869, X1_898]: (skf21(V_878, X_876, Y_883, Z_893, X1_898, X2_880, W_202, U_203)=skf21(V_872, X_887, Y_884, Z_892, X1_885, X2_888, W_202, U_203) | skf21(V_886, X_881, Y_895, Z_875, X1_890, X2_889, W_202, U_203)=skf21(V_878, X_876, Y_883, Z_893, X1_898, X2_880, W_202, U_203) | skf21(V_886, X_881, Y_895, Z_875, X1_890, X2_889, W_202, U_203)=skf21(V_872, X_887, Y_884, Z_892, X1_885, X2_888, W_202, U_203) | skf21(V_886, X_881, Y_895, Z_875, X1_890, X2_889, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_878, X_876, Y_883, Z_893, X1_898, X2_880, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_872, X_887, Y_884, Z_892, X1_885, X2_888, 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_870 | skf21(V_886, X_881, Y_895, Z_875, X1_890, X2_889, W_202, U_203)=X5_870 | skf21(V_878, X_876, Y_883, Z_893, X1_898, X2_880, W_202, U_203)=X5_870 | skf21(V_872, X_887, Y_884, Z_892, X1_885, X2_888, W_202, U_203)=X5_870 | X5_870=U_891 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_891 | skf21(V_886, X_881, Y_895, Z_875, X1_890, X2_889, W_202, U_203)=U_891 | skf21(V_878, X_876, Y_883, Z_893, X1_898, X2_880, W_202, U_203)=U_891 | skf21(V_872, X_887, Y_884, Z_892, X1_885, X2_888, W_202, U_203)=U_891 | ~member(U_203, X5_870, W_202) | ~member(U_203, U_891, W_202) | skf21(U_891, V_873, W_871, X_894, Y_877, Z_882, X1_869, X2_874)!=U_891 | X2_888=X1_885 | Z_892=X1_885 | Z_892=X2_888 | Z_892=Y_884 | Y_884=X1_885 | Y_884=X2_888 | Y_884=X_887 | Z_892=X_887 | X_887=X1_885 | X_887=X2_888 | X_887=V_872 | Y_884=V_872 | Z_892=V_872 | X1_885=V_872 | X2_888=V_872 | ~member(U_203, X2_888, W_202) | ~member(U_203, X1_885, W_202) | ~member(U_203, Z_892, W_202) | ~member(U_203, Y_884, W_202) | ~member(U_203, X_887, W_202) | ~member(U_203, V_872, W_202) | X2_880=X1_898 | Z_893=X1_898 | Z_893=X2_880 | Z_893=Y_883 | Y_883=X1_898 | Y_883=X2_880 | Y_883=X_876 | Z_893=X_876 | X_876=X1_898 | X_876=X2_880 | X_876=V_878 | Y_883=V_878 | Z_893=V_878 | X1_898=V_878 | X2_880=V_878 | ~member(U_203, X2_880, W_202) | ~member(U_203, X1_898, W_202) | ~member(U_203, Z_893, W_202) | ~member(U_203, Y_883, W_202) | ~member(U_203, X_876, W_202) | ~member(U_203, V_878, W_202) | X2_889=X1_890 | Z_875=X1_890 | Z_875=X2_889 | Z_875=Y_895 | Y_895=X1_890 | Y_895=X2_889 | Y_895=X_881 | Z_875=X_881 | X_881=X1_890 | X_881=X2_889 | X_881=V_886 | Y_895=V_886 | Z_875=V_886 | X1_890=V_886 | X2_889=V_886 | ~member(U_203, X2_889, W_202) | ~member(U_203, X1_890, W_202) | ~member(U_203, Z_875, W_202) | ~member(U_203, Y_895, W_202) | ~member(U_203, X_881, W_202) | ~member(U_203, V_886, 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)))). % 67.00/56.92 tff(c_1484, plain, (![V_902, X1_915, V_909, X1_922, U_203, X_920, X2_910, X2_921, Z_914, X2_913, V_901, Z_204, Y_208, Y_911, W_202, W_924, V_916, Z_908, X1_205, X1_907, Y_904, X2_206, Y_923, V_209, U_918, Y_919, X1_900, Z_926, X_207, X_917, X_906, Z_899, X2_927, X_905]: (skf21(V_916, X_920, Y_911, Z_914, X1_900, X2_921, W_202, U_203)=skf21(V_901, X_917, Y_904, Z_908, X1_907, X2_910, W_202, U_203) | skf21(V_909, X_905, Y_919, Z_899, X1_915, X2_913, W_202, U_203)=skf21(V_901, X_917, Y_904, Z_908, X1_907, X2_910, W_202, U_203) | skf21(V_916, X_920, Y_911, Z_914, X1_900, X2_921, W_202, U_203)=skf21(V_909, X_905, Y_919, Z_899, X1_915, X2_913, W_202, U_203) | skf21(V_909, X_905, Y_919, Z_899, X1_915, X2_913, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_901, X_917, Y_904, Z_908, X1_907, X2_910, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_916, X_920, Y_911, Z_914, X1_900, X2_921, 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_902 | skf21(V_909, X_905, Y_919, Z_899, X1_915, X2_913, W_202, U_203)=V_902 | skf21(V_901, X_917, Y_904, Z_908, X1_907, X2_910, W_202, U_203)=V_902 | skf21(V_916, X_920, Y_911, Z_914, X1_900, X2_921, W_202, U_203)=V_902 | V_902=U_918 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_918 | skf21(V_909, X_905, Y_919, Z_899, X1_915, X2_913, W_202, U_203)=U_918 | skf21(V_901, X_917, Y_904, Z_908, X1_907, X2_910, W_202, U_203)=U_918 | skf21(V_916, X_920, Y_911, Z_914, X1_900, X2_921, W_202, U_203)=U_918 | ~member(U_203, V_902, W_202) | ~member(U_203, U_918, W_202) | skf21(U_918, V_902, W_924, X_906, Y_923, Z_926, X1_922, X2_927)!=V_902 | X2_921=X1_900 | Z_914=X1_900 | Z_914=X2_921 | Z_914=Y_911 | Y_911=X1_900 | Y_911=X2_921 | Y_911=X_920 | Z_914=X_920 | X_920=X1_900 | X_920=X2_921 | X_920=V_916 | Y_911=V_916 | Z_914=V_916 | X1_900=V_916 | X2_921=V_916 | ~member(U_203, X2_921, W_202) | ~member(U_203, X1_900, W_202) | ~member(U_203, Z_914, W_202) | ~member(U_203, Y_911, W_202) | ~member(U_203, X_920, W_202) | ~member(U_203, V_916, W_202) | X2_910=X1_907 | Z_908=X1_907 | Z_908=X2_910 | Z_908=Y_904 | Y_904=X1_907 | Y_904=X2_910 | Y_904=X_917 | Z_908=X_917 | X_917=X1_907 | X_917=X2_910 | X_917=V_901 | Y_904=V_901 | Z_908=V_901 | X1_907=V_901 | X2_910=V_901 | ~member(U_203, X2_910, W_202) | ~member(U_203, X1_907, W_202) | ~member(U_203, Z_908, W_202) | ~member(U_203, Y_904, W_202) | ~member(U_203, X_917, W_202) | ~member(U_203, V_901, W_202) | X2_913=X1_915 | Z_899=X1_915 | Z_899=X2_913 | Z_899=Y_919 | Y_919=X1_915 | Y_919=X2_913 | Y_919=X_905 | Z_899=X_905 | X_905=X1_915 | X_905=X2_913 | X_905=V_909 | Y_919=V_909 | Z_899=V_909 | X1_915=V_909 | X2_913=V_909 | ~member(U_203, X2_913, W_202) | ~member(U_203, X1_915, W_202) | ~member(U_203, Z_899, W_202) | ~member(U_203, Y_919, W_202) | ~member(U_203, X_905, W_202) | ~member(U_203, V_909, 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)))). % 67.00/56.92 tff(c_1373, plain, (![X_758, U_771, Z_761, W_764, Y_766, Z_751, U_203, X2_762, Z_204, X1_754, X_752, Y_208, Y_753, V_759, W_202, Y_768, V_755, X2_750, X1_205, Z_769, X2_206, X1_760, V_765, V_209, X2_756, X1_763, X_207]: (skf21(V_759, X_758, Y_768, Z_751, X1_763, X2_762, W_202, U_203)=skf21(V_755, X_752, Y_753, Z_761, X1_754, X2_750, W_202, U_203) | skf21(V_759, X_758, Y_768, Z_751, X1_763, X2_762, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_755, X_752, Y_753, Z_761, X1_754, X2_750, 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_764 | skf21(V_759, X_758, Y_768, Z_751, X1_763, X2_762, W_202, U_203)=W_764 | skf21(V_755, X_752, Y_753, Z_761, X1_754, X2_750, W_202, U_203)=W_764 | W_764=V_765 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_765 | skf21(V_759, X_758, Y_768, Z_751, X1_763, X2_762, W_202, U_203)=V_765 | skf21(V_755, X_752, Y_753, Z_761, X1_754, X2_750, W_202, U_203)=V_765 | V_765=U_771 | W_764=U_771 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_771 | skf21(V_759, X_758, Y_768, Z_751, X1_763, X2_762, W_202, U_203)=U_771 | skf21(V_755, X_752, Y_753, Z_761, X1_754, X2_750, W_202, U_203)=U_771 | ~member(U_203, W_764, W_202) | ~member(U_203, V_765, W_202) | ~member(U_203, U_771, W_202) | skf21(U_771, V_765, W_764, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Y_766, Z_769, X1_760, X2_756)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_750=X1_754 | Z_761=X1_754 | Z_761=X2_750 | Z_761=Y_753 | Y_753=X1_754 | Y_753=X2_750 | Y_753=X_752 | Z_761=X_752 | X_752=X1_754 | X_752=X2_750 | X_752=V_755 | Y_753=V_755 | Z_761=V_755 | X1_754=V_755 | X2_750=V_755 | ~member(U_203, X2_750, W_202) | ~member(U_203, X1_754, W_202) | ~member(U_203, Z_761, W_202) | ~member(U_203, Y_753, W_202) | ~member(U_203, X_752, W_202) | ~member(U_203, V_755, W_202) | X2_762=X1_763 | Z_751=X1_763 | Z_751=X2_762 | Z_751=Y_768 | Y_768=X1_763 | Y_768=X2_762 | Y_768=X_758 | Z_751=X_758 | X_758=X1_763 | X_758=X2_762 | X_758=V_759 | Y_768=V_759 | Z_751=V_759 | X1_763=V_759 | X2_762=V_759 | ~member(U_203, X2_762, W_202) | ~member(U_203, X1_763, W_202) | ~member(U_203, Z_751, W_202) | ~member(U_203, Y_768, W_202) | ~member(U_203, X_758, W_202) | ~member(U_203, V_759, 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)))). % 67.00/56.92 tff(c_1351, plain, (![X_731, X1_742, X_735, W_732, Z_726, U_741, U_203, X2_740, Y_748, X1_744, Z_204, Y_729, X2_743, Y_208, W_202, V_730, Z_736, V_738, Z_739, X1_205, V_749, X2_737, X2_206, X1_727, V_209, X_207, X5_745, X_728, Y_746]: (skf21(V_738, X_735, Y_746, Z_726, X1_742, X2_740, W_202, U_203)=skf21(V_730, X_728, Y_729, Z_736, X1_744, X2_737, W_202, U_203) | skf21(V_738, X_735, Y_746, Z_726, X1_742, X2_740, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_730, X_728, Y_729, Z_736, X1_744, X2_737, 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_745 | skf21(V_738, X_735, Y_746, Z_726, X1_742, X2_740, W_202, U_203)=X5_745 | skf21(V_730, X_728, Y_729, Z_736, X1_744, X2_737, W_202, U_203)=X5_745 | X5_745=V_749 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_749 | skf21(V_738, X_735, Y_746, Z_726, X1_742, X2_740, W_202, U_203)=V_749 | skf21(V_730, X_728, Y_729, Z_736, X1_744, X2_737, W_202, U_203)=V_749 | V_749=U_741 | X5_745=U_741 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_741 | skf21(V_738, X_735, Y_746, Z_726, X1_742, X2_740, W_202, U_203)=U_741 | skf21(V_730, X_728, Y_729, Z_736, X1_744, X2_737, W_202, U_203)=U_741 | ~member(U_203, X5_745, W_202) | ~member(U_203, V_749, W_202) | ~member(U_203, U_741, W_202) | skf21(U_741, V_749, W_732, X_731, Y_748, Z_739, X1_727, X2_743)!=V_749 | X2_737=X1_744 | Z_736=X1_744 | Z_736=X2_737 | Z_736=Y_729 | Y_729=X1_744 | Y_729=X2_737 | Y_729=X_728 | Z_736=X_728 | X_728=X1_744 | X_728=X2_737 | X_728=V_730 | Y_729=V_730 | Z_736=V_730 | X1_744=V_730 | X2_737=V_730 | ~member(U_203, X2_737, W_202) | ~member(U_203, X1_744, W_202) | ~member(U_203, Z_736, W_202) | ~member(U_203, Y_729, W_202) | ~member(U_203, X_728, W_202) | ~member(U_203, V_730, W_202) | X2_740=X1_742 | Z_726=X1_742 | Z_726=X2_740 | Z_726=Y_746 | Y_746=X1_742 | Y_746=X2_740 | Y_746=X_735 | Z_726=X_735 | X_735=X1_742 | X_735=X2_740 | X_735=V_738 | Y_746=V_738 | Z_726=V_738 | X1_742=V_738 | X2_740=V_738 | ~member(U_203, X2_740, W_202) | ~member(U_203, X1_742, W_202) | ~member(U_203, Z_726, W_202) | ~member(U_203, Y_746, W_202) | ~member(U_203, X_735, W_202) | ~member(U_203, V_738, 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)))). % 67.00/56.92 tff(c_1395, plain, (![X1_780, W_781, X1_773, Z_772, U_785, X5_783, Z_791, X_775, U_203, X1_787, V_774, Z_204, X6_777, Y_208, Y_793, W_202, X2_788, X2_786, X1_205, V_782, Z_784, V_789, X2_206, X2_790, V_209, X_779, X_795, Y_778, X_207, Y_792]: (skf21(V_782, X_779, Y_792, Z_772, X1_787, X2_786, W_202, U_203)=skf21(V_774, X_795, Y_793, Z_791, X1_773, X2_788, W_202, U_203) | skf21(V_782, X_779, Y_792, Z_772, X1_787, X2_786, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_774, X_795, Y_793, Z_791, X1_773, X2_788, 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_777 | skf21(V_782, X_779, Y_792, Z_772, X1_787, X2_786, W_202, U_203)=X6_777 | skf21(V_774, X_795, Y_793, Z_791, X1_773, X2_788, W_202, U_203)=X6_777 | X6_777=X5_783 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_783 | skf21(V_782, X_779, Y_792, Z_772, X1_787, X2_786, W_202, U_203)=X5_783 | skf21(V_774, X_795, Y_793, Z_791, X1_773, X2_788, W_202, U_203)=X5_783 | X5_783=U_785 | X6_777=U_785 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_785 | skf21(V_782, X_779, Y_792, Z_772, X1_787, X2_786, W_202, U_203)=U_785 | skf21(V_774, X_795, Y_793, Z_791, X1_773, X2_788, W_202, U_203)=U_785 | ~member(U_203, X6_777, W_202) | ~member(U_203, X5_783, W_202) | ~member(U_203, U_785, W_202) | skf21(U_785, V_789, W_781, X_775, Y_778, Z_784, X1_780, X2_790)!=U_785 | X2_788=X1_773 | Z_791=X1_773 | Z_791=X2_788 | Z_791=Y_793 | Y_793=X1_773 | Y_793=X2_788 | Y_793=X_795 | Z_791=X_795 | X_795=X1_773 | X_795=X2_788 | X_795=V_774 | Y_793=V_774 | Z_791=V_774 | X1_773=V_774 | X2_788=V_774 | ~member(U_203, X2_788, W_202) | ~member(U_203, X1_773, W_202) | ~member(U_203, Z_791, W_202) | ~member(U_203, Y_793, W_202) | ~member(U_203, X_795, W_202) | ~member(U_203, V_774, W_202) | X2_786=X1_787 | Z_772=X1_787 | Z_772=X2_786 | Z_772=Y_792 | Y_792=X1_787 | Y_792=X2_786 | Y_792=X_779 | Z_772=X_779 | X_779=X1_787 | X_779=X2_786 | X_779=V_782 | Y_792=V_782 | Z_772=V_782 | X1_787=V_782 | X2_786=V_782 | ~member(U_203, X2_786, W_202) | ~member(U_203, X1_787, W_202) | ~member(U_203, Z_772, W_202) | ~member(U_203, Y_792, W_202) | ~member(U_203, X_779, W_202) | ~member(U_203, V_782, 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)))). % 67.00/56.92 tff(c_1417, plain, (![X_814, X2_810, Y_819, U_816, U_203, V_808, X1_804, Z_204, X1_811, Y_817, Y_208, X2_812, W_202, X2_799, Y_798, X1_205, X_806, V_815, Z_797, W_807, X2_206, Z_803, V_209, Z_801, X1_809, V_802, X_207, X_805]: (skf21(V_815, X_806, Y_798, Z_803, X1_804, X2_812, W_202, U_203)=skf21(V_808, X_805, Y_817, Z_797, X1_811, X2_810, W_202, U_203) | skf21(V_808, X_805, Y_817, Z_797, X1_811, X2_810, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_815, X_806, Y_798, Z_803, X1_804, X2_812, 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_807 | skf21(V_808, X_805, Y_817, Z_797, X1_811, X2_810, W_202, U_203)=W_807 | skf21(V_815, X_806, Y_798, Z_803, X1_804, X2_812, W_202, U_203)=W_807 | W_807=V_802 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_802 | skf21(V_808, X_805, Y_817, Z_797, X1_811, X2_810, W_202, U_203)=V_802 | skf21(V_815, X_806, Y_798, Z_803, X1_804, X2_812, W_202, U_203)=V_802 | V_802=U_816 | W_807=U_816 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_816 | skf21(V_808, X_805, Y_817, Z_797, X1_811, X2_810, W_202, U_203)=U_816 | skf21(V_815, X_806, Y_798, Z_803, X1_804, X2_812, W_202, U_203)=U_816 | ~member(U_203, W_807, W_202) | ~member(U_203, V_802, W_202) | ~member(U_203, U_816, W_202) | skf21(U_816, V_802, W_807, X_814, Y_819, Z_801, X1_809, X2_799)!=W_807 | X2_812=X1_804 | Z_803=X1_804 | Z_803=X2_812 | Z_803=Y_798 | Y_798=X1_804 | Y_798=X2_812 | Y_798=X_806 | Z_803=X_806 | X_806=X1_804 | X_806=X2_812 | X_806=V_815 | Y_798=V_815 | Z_803=V_815 | X1_804=V_815 | X2_812=V_815 | ~member(U_203, X2_812, W_202) | ~member(U_203, X1_804, W_202) | ~member(U_203, Z_803, W_202) | ~member(U_203, Y_798, W_202) | ~member(U_203, X_806, W_202) | ~member(U_203, V_815, W_202) | X2_810=X1_811 | Z_797=X1_811 | Z_797=X2_810 | Z_797=Y_817 | Y_817=X1_811 | Y_817=X2_810 | Y_817=X_805 | Z_797=X_805 | X_805=X1_811 | X_805=X2_810 | X_805=V_808 | Y_817=V_808 | Z_797=V_808 | X1_811=V_808 | X2_810=V_808 | ~member(U_203, X2_810, W_202) | ~member(U_203, X1_811, W_202) | ~member(U_203, Z_797, W_202) | ~member(U_203, Y_817, W_202) | ~member(U_203, X_805, W_202) | ~member(U_203, V_808, 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)))). % 67.00/56.92 tff(c_1328, plain, (![U_701, V_697, U_203, X_708, Z_204, Y_208, Z_705, X2_698, W_703, Y_702, W_202, X1_704, X2_696, X1_205, X1_709, V_699, X2_206, X_710, Z_700, V_209, X_207]: (skf21(V_697, X_710, Y_702, Z_700, X1_704, X2_696, 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_708 | skf21(V_697, X_710, Y_702, Z_700, X1_704, X2_696, W_202, U_203)=X_708 | X_708=W_703 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_703 | skf21(V_697, X_710, Y_702, Z_700, X1_704, X2_696, W_202, U_203)=W_703 | W_703=V_699 | X_708=V_699 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_699 | skf21(V_697, X_710, Y_702, Z_700, X1_704, X2_696, W_202, U_203)=V_699 | V_699=U_701 | W_703=U_701 | X_708=U_701 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_701 | skf21(V_697, X_710, Y_702, Z_700, X1_704, X2_696, W_202, U_203)=U_701 | ~member(U_203, X_708, W_202) | ~member(U_203, W_703, W_202) | ~member(U_203, V_699, W_202) | ~member(U_203, U_701, W_202) | skf21(U_701, V_699, W_703, X_708, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Z_705, X1_709, X2_698)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_696=X1_704 | Z_700=X1_704 | Z_700=X2_696 | Z_700=Y_702 | Y_702=X1_704 | Y_702=X2_696 | Y_702=X_710 | Z_700=X_710 | X_710=X1_704 | X_710=X2_696 | X_710=V_697 | Y_702=V_697 | Z_700=V_697 | X1_704=V_697 | X2_696=V_697 | ~member(U_203, X2_696, W_202) | ~member(U_203, X1_704, W_202) | ~member(U_203, Z_700, W_202) | ~member(U_203, Y_702, W_202) | ~member(U_203, X_710, 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)))). % 67.00/56.92 tff(c_1284, plain, (![V_672, X1_674, U_203, W_670, X_673, Z_204, V_660, Y_663, Y_208, X2_662, U_666, X5_668, W_202, Z_661, X1_665, Y_675, X1_205, Z_671, X2_206, V_209, X_207, X_669, X2_659]: (skf21(V_660, X_673, Y_663, Z_661, X1_665, X2_659, 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_668 | skf21(V_660, X_673, Y_663, Z_661, X1_665, X2_659, W_202, U_203)=X5_668 | X5_668=W_670 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_670 | skf21(V_660, X_673, Y_663, Z_661, X1_665, X2_659, W_202, U_203)=W_670 | W_670=V_672 | X5_668=V_672 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_672 | skf21(V_660, X_673, Y_663, Z_661, X1_665, X2_659, W_202, U_203)=V_672 | V_672=U_666 | W_670=U_666 | X5_668=U_666 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_666 | skf21(V_660, X_673, Y_663, Z_661, X1_665, X2_659, W_202, U_203)=U_666 | ~member(U_203, X5_668, W_202) | ~member(U_203, W_670, W_202) | ~member(U_203, V_672, W_202) | ~member(U_203, U_666, W_202) | skf21(U_666, V_672, W_670, X_669, Y_675, Z_671, X1_674, X2_662)!=W_670 | X2_659=X1_665 | Z_661=X1_665 | Z_661=X2_659 | Z_661=Y_663 | Y_663=X1_665 | Y_663=X2_659 | Y_663=X_673 | Z_661=X_673 | X_673=X1_665 | X_673=X2_659 | X_673=V_660 | Y_663=V_660 | Z_661=V_660 | X1_665=V_660 | X2_659=V_660 | ~member(U_203, X2_659, W_202) | ~member(U_203, X1_665, W_202) | ~member(U_203, Z_661, W_202) | ~member(U_203, Y_663, W_202) | ~member(U_203, X_673, W_202) | ~member(U_203, V_660, 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)))). % 67.00/56.92 tff(c_1262, plain, (![V_641, X6_648, X2_640, X5_649, U_203, X1_647, W_655, Z_204, Y_208, Z_643, X_657, W_202, U_650, X7_638, X2_642, Y_645, X1_205, X2_206, X_656, V_209, X_207, Y_654, Z_652, V_653, X1_644]: (skf21(V_641, X_656, Y_645, Z_643, X1_647, X2_640, 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_638 | skf21(V_641, X_656, Y_645, Z_643, X1_647, X2_640, W_202, U_203)=X7_638 | X7_638=X6_648 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_648 | skf21(V_641, X_656, Y_645, Z_643, X1_647, X2_640, W_202, U_203)=X6_648 | X6_648=X5_649 | X7_638=X5_649 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_649 | skf21(V_641, X_656, Y_645, Z_643, X1_647, X2_640, W_202, U_203)=X5_649 | X5_649=U_650 | X6_648=U_650 | X7_638=U_650 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_650 | skf21(V_641, X_656, Y_645, Z_643, X1_647, X2_640, W_202, U_203)=U_650 | ~member(U_203, X7_638, W_202) | ~member(U_203, X6_648, W_202) | ~member(U_203, X5_649, W_202) | ~member(U_203, U_650, W_202) | skf21(U_650, V_653, W_655, X_657, Y_654, Z_652, X1_644, X2_642)!=U_650 | X2_640=X1_647 | Z_643=X1_647 | Z_643=X2_640 | Z_643=Y_645 | Y_645=X1_647 | Y_645=X2_640 | Y_645=X_656 | Z_643=X_656 | X_656=X1_647 | X_656=X2_640 | X_656=V_641 | Y_645=V_641 | Z_643=V_641 | X1_647=V_641 | X2_640=V_641 | ~member(U_203, X2_640, W_202) | ~member(U_203, X1_647, W_202) | ~member(U_203, Z_643, W_202) | ~member(U_203, Y_645, W_202) | ~member(U_203, X_656, W_202) | ~member(U_203, V_641, 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)))). % 67.00/56.92 tff(c_1240, plain, (![X1_629, V_623, Z_626, U_203, W_633, Z_636, V_628, Z_204, X_635, Y_208, Y_625, X1_631, W_202, U_624, X1_205, X_632, X2_206, Y_627, V_209, X2_622, X_207, X2_637]: (skf21(V_623, X_635, Y_627, Z_626, X1_629, X2_622, 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_632 | skf21(V_623, X_635, Y_627, Z_626, X1_629, X2_622, W_202, U_203)=X_632 | X_632=W_633 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_633 | skf21(V_623, X_635, Y_627, Z_626, X1_629, X2_622, W_202, U_203)=W_633 | W_633=V_628 | X_632=V_628 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_628 | skf21(V_623, X_635, Y_627, Z_626, X1_629, X2_622, W_202, U_203)=V_628 | V_628=U_624 | W_633=U_624 | X_632=U_624 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_624 | skf21(V_623, X_635, Y_627, Z_626, X1_629, X2_622, W_202, U_203)=U_624 | ~member(U_203, X_632, W_202) | ~member(U_203, W_633, W_202) | ~member(U_203, V_628, W_202) | ~member(U_203, U_624, W_202) | skf21(U_624, V_628, W_633, X_632, Y_625, Z_636, X1_631, X2_637)!=X_632 | X2_622=X1_629 | Z_626=X1_629 | Z_626=X2_622 | Z_626=Y_627 | Y_627=X1_629 | Y_627=X2_622 | Y_627=X_635 | Z_626=X_635 | X_635=X1_629 | X_635=X2_622 | X_635=V_623 | Y_627=V_623 | Z_626=V_623 | X1_629=V_623 | X2_622=V_623 | ~member(U_203, X2_622, W_202) | ~member(U_203, X1_629, W_202) | ~member(U_203, Z_626, W_202) | ~member(U_203, Y_627, W_202) | ~member(U_203, X_635, W_202) | ~member(U_203, V_623, 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)))). % 67.00/56.92 tff(c_1306, plain, (![X1_685, W_680, V_683, V_678, X2_694, U_203, X2_677, X_688, Z_204, Y_208, Y_692, W_202, X_693, X6_686, X1_205, Y_682, Z_681, X2_206, V_209, Z_679, X_207, U_691, X5_684, X1_689]: (skf21(V_678, X_693, Y_682, Z_679, X1_685, X2_677, 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_686 | skf21(V_678, X_693, Y_682, Z_679, X1_685, X2_677, W_202, U_203)=X6_686 | X6_686=X5_684 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_684 | skf21(V_678, X_693, Y_682, Z_679, X1_685, X2_677, W_202, U_203)=X5_684 | X5_684=V_683 | X6_686=V_683 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_683 | skf21(V_678, X_693, Y_682, Z_679, X1_685, X2_677, W_202, U_203)=V_683 | V_683=U_691 | X5_684=U_691 | X6_686=U_691 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_691 | skf21(V_678, X_693, Y_682, Z_679, X1_685, X2_677, W_202, U_203)=U_691 | ~member(U_203, X6_686, W_202) | ~member(U_203, X5_684, W_202) | ~member(U_203, V_683, W_202) | ~member(U_203, U_691, W_202) | skf21(U_691, V_683, W_680, X_688, Y_692, Z_681, X1_689, X2_694)!=V_683 | X2_677=X1_685 | Z_679=X1_685 | Z_679=X2_677 | Z_679=Y_682 | Y_682=X1_685 | Y_682=X2_677 | Y_682=X_693 | Z_679=X_693 | X_693=X1_685 | X_693=X2_677 | X_693=V_678 | Y_682=V_678 | Z_679=V_678 | X1_685=V_678 | X2_677=V_678 | ~member(U_203, X2_677, W_202) | ~member(U_203, X1_685, W_202) | ~member(U_203, Z_679, W_202) | ~member(U_203, Y_682, W_202) | ~member(U_203, X_693, W_202) | ~member(U_203, V_678, 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)))). % 67.00/56.93 tff(c_1216, plain, (![W_614, U_212, X2_617, X1_618, X_216, U_620, X_615, V_218, Z_613, X2_215, Y_217, V_616, Y_619, W_210, X1_214]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=Y_217 | Y_217=X_216 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X_216 | X_216=W_210 | Y_217=W_210 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=W_210 | W_210=V_218 | X_216=V_218 | Y_217=V_218 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=V_218 | V_218=U_212 | W_210=U_212 | X_216=U_212 | Y_217=U_212 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_212 | ~member(U_620, Y_217, W_614) | ~member(U_620, X_216, W_614) | ~member(U_620, W_210, W_614) | ~member(U_620, V_218, W_614) | ~member(U_620, U_212, W_614) | skf21(U_212, V_218, W_210, X_216, Y_217, skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620), X1_214, X2_215)!=skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620) | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.93 tff(c_1218, plain, (![W_614, X2_617, X_144, Y_145, Z_141, X1_618, U_140, X1_142, U_620, X_615, Z_613, V_616, V_146, Y_619, X2_143, W_138]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=Y_145 | Y_145=X_144 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X_144 | X_144=W_138 | Y_145=W_138 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=W_138 | W_138=V_146 | X_144=V_146 | Y_145=V_146 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=V_146 | V_146=U_140 | W_138=U_140 | X_144=U_140 | Y_145=U_140 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_140 | ~member(U_620, Y_145, W_614) | ~member(U_620, X_144, W_614) | ~member(U_620, W_138, W_614) | ~member(U_620, V_146, W_614) | ~member(U_620, U_140, W_614) | skf21(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143)!=Y_145 | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.93 tff(c_1219, plain, (![V_184, W_614, X5_173, X2_617, X6_174, Z_178, X_182, X1_618, Y_183, U_620, X_615, X1_180, Z_613, W_175, U_177, V_616, Y_619, X2_181, X7_179]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X7_179 | X7_179=X6_174 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X6_174 | X6_174=X5_173 | X7_179=X5_173 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X5_173 | X5_173=V_184 | X6_174=V_184 | X7_179=V_184 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=V_184 | V_184=U_177 | X5_173=U_177 | X6_174=U_177 | X7_179=U_177 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_177 | ~member(U_620, X7_179, W_614) | ~member(U_620, X6_174, W_614) | ~member(U_620, X5_173, W_614) | ~member(U_620, V_184, W_614) | ~member(U_620, U_177, W_614) | skf21(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181)!=V_184 | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.93 tff(c_1220, plain, (![W_614, U_164, X6_161, Y_170, W_162, X2_617, X1_167, X1_618, U_620, X_169, Z_165, X_615, V_171, Z_613, X2_168, V_616, Y_619, X5_160]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X6_161 | X6_161=X5_160 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X5_160 | X5_160=W_162 | X6_161=W_162 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=W_162 | W_162=V_171 | X5_160=V_171 | X6_161=V_171 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=V_171 | V_171=U_164 | W_162=U_164 | X5_160=U_164 | X6_161=U_164 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_164 | ~member(U_620, X6_161, W_614) | ~member(U_620, X5_160, W_614) | ~member(U_620, W_162, W_614) | ~member(U_620, V_171, W_614) | ~member(U_620, U_164, W_614) | skf21(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168)!=W_162 | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.93 tff(c_1221, plain, (![X8_200, W_614, V_199, X6_188, X2_617, X2_196, X7_194, W_189, Z_193, X1_195, X1_618, U_620, X_615, U_191, Z_613, X_197, Y_198, X5_187, V_616, Y_619]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X8_200 | X8_200=X7_194 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X7_194 | X7_194=X6_188 | X8_200=X6_188 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X6_188 | X6_188=X5_187 | X7_194=X5_187 | X8_200=X5_187 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X5_187 | X5_187=U_191 | X6_188=U_191 | X7_194=U_191 | X8_200=U_191 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_191 | ~member(U_620, X8_200, W_614) | ~member(U_620, X7_194, W_614) | ~member(U_620, X6_188, W_614) | ~member(U_620, X5_187, W_614) | ~member(U_620, U_191, W_614) | skf21(U_191, V_199, W_189, X_197, Y_198, Z_193, X1_195, X2_196)!=U_191 | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.93 tff(c_1217, plain, (![W_614, X_156, X2_155, X2_617, X5_148, X1_154, U_152, Z_153, X1_618, U_620, Y_157, V_158, X_615, Z_613, W_150, V_616, Y_619]: (skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X5_148 | X_156=X5_148 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=X_156 | X_156=W_150 | X5_148=W_150 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=W_150 | W_150=V_158 | X_156=V_158 | X5_148=V_158 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=V_158 | V_158=U_152 | W_150=U_152 | X_156=U_152 | X5_148=U_152 | skf21(V_616, X_615, Y_619, Z_613, X1_618, X2_617, W_614, U_620)=U_152 | ~member(U_620, X5_148, W_614) | ~member(U_620, X_156, W_614) | ~member(U_620, W_150, W_614) | ~member(U_620, V_158, W_614) | ~member(U_620, U_152, W_614) | skf21(U_152, V_158, W_150, X_156, Y_157, Z_153, X1_154, X2_155)!=X_156 | X2_617=X1_618 | Z_613=X1_618 | Z_613=X2_617 | Z_613=Y_619 | Y_619=X1_618 | Y_619=X2_617 | Y_619=X_615 | Z_613=X_615 | X_615=X1_618 | X_615=X2_617 | X_615=V_616 | Y_619=V_616 | Z_613=V_616 | X1_618=V_616 | X2_617=V_616 | six(U_620, W_614) | ~member(U_620, X2_617, W_614) | ~member(U_620, X1_618, W_614) | ~member(U_620, Z_613, W_614) | ~member(U_620, Y_619, W_614) | ~member(U_620, X_615, W_614) | ~member(U_620, V_616, W_614)))). % 67.00/56.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)))). % 67.00/56.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))). % 67.00/56.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))). % 67.00/56.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))). % 67.00/56.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))). % 67.00/56.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))). % 67.00/56.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))). % 67.00/56.93 tff(c_1050, plain, (~member(skc7, skc12, skc10))). % 67.00/56.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)))). % 67.00/56.93 tff(c_1041, plain, (![U_231]: (~agent(skc7, skf8(U_231), U_231) | ~member(skc7, U_231, skc10)))). % 67.00/56.93 tff(c_1031, plain, (act(skc7, skf18(skc10, skc7)))). % 67.00/56.93 tff(c_1044, plain, (~agent(skc7, skc8, skc9))). % 67.00/56.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)))). % 67.00/56.93 tff(c_1027, plain, (act(skc7, skf12(skc10, skc7)))). % 67.00/56.93 tff(c_1023, plain, (action(skc7, skf18(skc10, skc7)))). % 67.00/56.93 tff(c_1019, plain, (action(skc7, skf12(skc10, skc7)))). % 67.00/56.93 tff(c_1015, plain, (shot(skc7, skf18(skc10, skc7)))). % 67.00/56.93 tff(c_1007, plain, (shot(skc7, skf12(skc10, skc7)))). % 67.00/56.93 tff(c_92, plain, (![U_91, V_92]: (member(U_91, skf18(V_92, U_91), V_92) | ~six(U_91, V_92)))). % 67.00/56.93 tff(c_98, plain, (![U_97, V_98]: (member(U_97, skf12(V_98, U_97), V_98) | ~six(U_97, V_98)))). % 67.00/56.93 tff(c_999, plain, (skf16(skc10, skc7)!=skf12(skc10, skc7))). % 67.00/56.93 tff(c_994, plain, (skf20(skc10, skc7)!=skf16(skc10, skc7))). % 67.00/56.93 tff(c_122, plain, (![V_122, U_121]: (~six(V_122, U_121) | skf16(U_121, V_122)!=skf12(U_121, V_122)))). % 67.00/56.93 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf16(U_107, V_108)))). % 67.00/56.93 tff(c_988, plain, (![V_230]: (from_loc(skc7, skf8(V_230), skc11)))). % 67.00/56.93 tff(c_965, plain, (skf20(skc10, skc7)!=skf18(skc10, skc7))). % 67.00/56.93 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf20(U_109, V_110)!=skf18(U_109, V_110)))). % 67.00/56.93 tff(c_960, plain, (act(skc7, skf10(skc10, skc7)))). % 67.00/56.93 tff(c_956, plain, (action(skc7, skf10(skc10, skc7)))). % 67.00/56.93 tff(c_951, plain, (shot(skc7, skf10(skc10, skc7)))). % 67.00/56.93 tff(c_196, plain, (![U_231]: (patient(skc7, skf8(U_231), U_231) | ~member(skc7, U_231, skc10)))). % 67.00/56.93 tff(c_100, plain, (![U_99, V_100]: (member(U_99, skf10(V_100, U_99), V_100) | ~six(U_99, V_100)))). % 67.00/56.93 tff(c_943, plain, (skf12(skc10, skc7)!=skf10(skc10, skc7))). % 67.00/56.93 tff(c_130, plain, (![V_130, U_129]: (~six(V_130, U_129) | skf12(U_129, V_130)!=skf10(U_129, V_130)))). % 67.00/56.93 tff(c_938, plain, (skf18(skc10, skc7)!=skf12(skc10, skc7))). % 67.00/56.93 tff(c_933, plain, (skf14(skc10, skc7)!=skf10(skc10, skc7))). % 67.00/56.93 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf12(U_113, V_114)))). % 67.00/56.93 tff(c_126, plain, (![V_126, U_125]: (~six(V_126, U_125) | skf14(U_125, V_126)!=skf10(U_125, V_126)))). % 67.00/56.93 tff(c_928, plain, (skf16(skc10, skc7)!=skf14(skc10, skc7))). % 67.00/56.93 tff(c_923, plain, (skf20(skc10, skc7)!=skf12(skc10, skc7))). % 67.00/56.93 tff(c_124, plain, (![V_124, U_123]: (~six(V_124, U_123) | skf16(U_123, V_124)!=skf14(U_123, V_124)))). % 67.00/56.93 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf12(U_103, V_104)))). % 67.00/56.93 tff(c_918, plain, (~artifact(skc7, skc9))). % 67.00/56.93 tff(c_882, plain, (![U_47, V_48]: (~cry(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.00/56.93 tff(c_912, plain, (![V_233]: (agent(skc7, skf8(V_233), skc12)))). % 67.00/56.93 tff(c_893, plain, (~act(skc7, skc11))). % 67.00/56.93 tff(c_873, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.00/56.93 tff(c_888, plain, (skf18(skc10, skc7)!=skf10(skc10, skc7))). % 67.00/56.93 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf10(U_111, V_112)))). % 67.00/56.93 tff(c_844, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~cry(U_21, V_22)))). % 67.00/56.93 tff(c_843, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~act(U_27, V_28)))). % 67.00/56.93 tff(c_864, plain, (skf14(skc10, skc7)!=skf12(skc10, skc7))). % 67.00/56.93 tff(c_850, plain, (skf18(skc10, skc7)!=skf14(skc10, skc7))). % 67.00/56.93 tff(c_859, plain, (![V_490]: (~artifact(skc7, skf8(V_490))))). % 67.00/56.93 tff(c_128, plain, (![V_128, U_127]: (~six(V_128, U_127) | skf14(U_127, V_128)!=skf12(U_127, V_128)))). % 67.00/56.93 tff(c_842, plain, (![V_390]: (~entity(skc7, skf8(V_390))))). % 67.00/56.94 tff(c_854, plain, (~artifact(skc7, skc8))). % 67.00/56.94 tff(c_845, plain, (~entity(skc7, skc8))). % 67.00/56.94 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf18(U_115, V_116)!=skf14(U_115, V_116)))). % 67.00/56.94 tff(c_723, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~event(U_7, V_8)))). % 67.00/56.94 tff(c_728, plain, (![U_244, V_245]: (~artifact(U_244, V_245) | ~human_person(U_244, V_245)))). % 67.00/56.94 tff(c_819, plain, (skf20(skc10, skc7)!=skf14(skc10, skc7))). % 67.00/56.94 tff(c_823, plain, (~animate(skc7, skc11))). % 67.00/56.94 tff(c_814, plain, (artifact(skc7, skc11))). % 67.22/56.94 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf14(U_105, V_106)))). % 67.22/56.94 tff(c_789, plain, (![U_470, V_471]: (artifact(U_470, V_471) | ~cannon(U_470, V_471)))). % 67.22/56.94 tff(c_805, plain, (skf16(skc10, skc7)!=skf10(skc10, skc7))). % 67.22/56.94 tff(c_800, plain, (~entity(skc7, skc10))). % 67.22/56.94 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf16(U_119, V_120)!=skf10(U_119, V_120)))). % 67.22/56.94 tff(c_738, plain, (![U_31, V_32]: (~entity(U_31, V_32) | ~group(U_31, V_32)))). % 67.22/56.94 tff(c_702, plain, (![U_31, V_32]: (~eventuality(U_31, V_32) | ~group(U_31, V_32)))). % 67.22/56.94 tff(c_581, plain, (![U_398, V_399]: (~animate(U_398, V_399) | ~artifact(U_398, V_399)))). % 67.22/56.94 tff(c_566, plain, (![U_39, V_40]: (instrumentality(U_39, V_40) | ~cannon(U_39, V_40)))). % 67.22/56.94 tff(c_784, plain, (skf18(skc10, skc7)!=skf16(skc10, skc7))). % 67.22/56.94 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf18(U_117, V_118)!=skf16(U_117, V_118)))). % 67.22/56.94 tff(c_779, plain, (act(skc7, skf20(skc10, skc7)))). % 67.22/56.94 tff(c_775, plain, (action(skc7, skf20(skc10, skc7)))). % 67.22/56.94 tff(c_771, plain, (shot(skc7, skf20(skc10, skc7)))). % 67.22/56.94 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf20(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 67.22/56.94 tff(c_763, plain, (act(skc7, skf14(skc10, skc7)))). % 67.22/56.94 tff(c_759, plain, (action(skc7, skf14(skc10, skc7)))). % 67.22/56.94 tff(c_755, plain, (shot(skc7, skf14(skc10, skc7)))). % 67.22/56.94 tff(c_746, plain, (~artifact(skc7, skc12))). % 67.22/56.94 tff(c_747, plain, (~artifact(skc7, skc10))). % 67.22/56.94 tff(c_96, plain, (![U_95, V_96]: (member(U_95, skf14(V_96, U_95), V_96) | ~six(U_95, V_96)))). % 67.22/56.94 tff(c_573, plain, (![U_47, V_48]: (~male(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.22/56.94 tff(c_338, plain, (![U_322, V_323]: (~multiple(U_322, V_323) | ~entity(U_322, V_323)))). % 67.22/56.94 tff(c_733, plain, (skf20(skc10, skc7)!=skf10(skc10, skc7))). % 67.22/56.94 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf10(U_101, V_102)))). % 67.22/56.94 tff(c_582, plain, (![U_398, V_399]: (~living(U_398, V_399) | ~artifact(U_398, V_399)))). % 67.22/56.94 tff(c_348, plain, (![U_55, V_56]: (~eventuality(U_55, V_56) | ~entity(U_55, V_56)))). % 67.22/56.94 tff(c_718, plain, (act(skc7, skf16(skc10, skc7)))). % 67.22/56.94 tff(c_714, plain, (action(skc7, skf16(skc10, skc7)))). % 67.22/56.94 tff(c_710, plain, (shot(skc7, skf16(skc10, skc7)))). % 67.22/56.94 tff(c_94, plain, (![U_93, V_94]: (member(U_93, skf16(V_94, U_93), V_94) | ~six(U_93, V_94)))). % 67.22/56.94 tff(c_343, plain, (![U_324, V_325]: (~multiple(U_324, V_325) | ~eventuality(U_324, V_325)))). % 67.22/56.94 tff(c_243, plain, (![U_47, V_48]: (impartial(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.22/56.94 tff(c_695, plain, (![V_226]: (present(skc7, skf8(V_226))))). % 67.22/56.94 tff(c_222, plain, (![U_65, V_66]: (impartial(U_65, V_66) | ~human_person(U_65, V_66)))). % 67.22/56.94 tff(c_261, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.22/56.94 tff(c_664, plain, (![V_224]: (nonreflexive(skc7, skf8(V_224))))). % 67.22/56.94 tff(c_587, plain, (entity(skc7, skc12))). % 67.22/56.94 tff(c_214, plain, (![U_65, V_66]: (entity(U_65, V_66) | ~human_person(U_65, V_66)))). % 67.22/56.94 tff(c_254, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.22/56.94 tff(c_283, plain, (![U_61, V_62]: (~male(U_61, V_62) | ~object(U_61, V_62)))). % 67.22/56.94 tff(c_208, plain, (![U_244, V_245]: (living(U_244, V_245) | ~human_person(U_244, V_245)))). % 67.22/56.94 tff(c_228, plain, (![U_41, V_42]: (instrumentality(U_41, V_42) | ~weapon(U_41, V_42)))). % 67.22/56.94 tff(c_560, plain, (![V_390]: (event(skc7, skf8(V_390))))). % 67.22/56.94 tff(c_547, plain, (![V_222]: (fire(skc7, skf8(V_222))))). % 67.22/56.94 tff(c_555, plain, (~cry(skc7, skc10))). % 67.22/56.94 tff(c_554, plain, (~act(skc7, skc10))). % 67.22/56.94 tff(c_374, plain, (~act(skc7, skc12))). % 67.22/56.94 tff(c_375, plain, (~cry(skc7, skc12))). % 67.22/56.94 tff(c_367, plain, (~event(skc7, skc10))). % 67.22/56.94 tff(c_363, plain, (~event(skc7, skc12))). % 67.22/56.94 tff(c_359, plain, (~eventuality(skc7, skc10))). % 67.22/56.94 tff(c_358, plain, (~eventuality(skc7, skc12))). % 67.22/56.94 tff(c_333, plain, (![U_320, V_321]: (~male(U_320, V_321) | ~eventuality(U_320, V_321)))). % 67.22/56.94 tff(c_312, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~group(U_31, V_32)))). % 67.22/56.94 tff(c_184, plain, (![U_220]: (shot(skc7, U_220) | ~member(skc7, U_220, skc10)))). % 67.22/56.94 tff(c_317, plain, (![U_314, V_315]: (~existent(U_314, V_315) | ~eventuality(U_314, V_315)))). % 67.22/56.94 tff(c_322, plain, (![U_316, V_317]: (singleton(U_316, V_317) | ~eventuality(U_316, V_317)))). % 67.22/56.94 tff(c_307, plain, (![U_51, V_52]: (singleton(U_51, V_52) | ~entity(U_51, V_52)))). % 67.22/56.94 tff(c_18, plain, (![U_17, V_18]: (unisex(U_17, V_18) | ~eventuality(U_17, V_18)))). % 67.22/56.94 tff(c_20, plain, (![U_19, V_20]: (event(U_19, V_20) | ~scream(U_19, V_20)))). % 67.22/56.94 tff(c_10, plain, (![U_9, V_10]: (thing(U_9, V_10) | ~eventuality(U_9, V_10)))). % 67.22/56.94 tff(c_16, plain, (![U_15, V_16]: (nonexistent(U_15, V_16) | ~eventuality(U_15, V_16)))). % 67.22/56.94 tff(c_34, plain, (![U_33, V_34]: (multiple(U_33, V_34) | ~set(U_33, V_34)))). % 67.22/56.94 tff(c_302, plain, (act(skc7, skc14))). % 67.22/56.94 tff(c_12, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~thing(U_11, V_12)))). % 67.22/56.94 tff(c_298, plain, (action(skc7, skc14))). % 67.22/56.94 tff(c_24, plain, (![U_23, V_24]: (action(U_23, V_24) | ~revenge(U_23, V_24)))). % 67.22/56.94 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~act(U_27, V_28)))). % 67.22/56.94 tff(c_6, plain, (![U_5, V_6]: (event(U_5, V_6) | ~sound(U_5, V_6)))). % 67.22/56.94 tff(c_88, plain, (![U_87, V_88]: (~animate(U_87, V_88) | ~nonliving(U_87, V_88)))). % 67.22/56.94 tff(c_22, plain, (![U_21, V_22]: (event(U_21, V_22) | ~cry(U_21, V_22)))). % 67.22/56.94 tff(c_86, plain, (![U_85, V_86]: (~existent(U_85, V_86) | ~nonexistent(U_85, V_86)))). % 67.22/56.94 tff(c_8, plain, (![U_7, V_8]: (eventuality(U_7, V_8) | ~event(U_7, V_8)))). % 67.22/56.94 tff(c_80, plain, (![U_79, V_80]: (~unisex(U_79, V_80) | ~male(U_79, V_80)))). % 67.22/56.94 tff(c_30, plain, (![U_29, V_30]: (action(U_29, V_30) | ~shot(U_29, V_30)))). % 67.22/56.94 tff(c_82, plain, (![U_81, V_82]: (~singleton(U_81, V_82) | ~multiple(U_81, V_82)))). % 67.22/56.95 tff(c_36, plain, (![U_35, V_36]: (group(U_35, V_36) | ~six(U_35, V_36)))). % 67.22/56.95 tff(c_84, plain, (![U_83, V_84]: (~nonliving(U_83, V_84) | ~living(U_83, V_84)))). % 67.22/56.95 tff(c_32, plain, (![U_31, V_32]: (set(U_31, V_32) | ~group(U_31, V_32)))). % 67.22/56.95 tff(c_78, plain, (![U_77, V_78]: (male(U_77, V_78) | ~man(U_77, V_78)))). % 67.22/56.95 tff(c_56, plain, (![U_55, V_56]: (existent(U_55, V_56) | ~entity(U_55, V_56)))). % 67.22/56.95 tff(c_50, plain, (![U_49, V_50]: (entity(U_49, V_50) | ~object(U_49, V_50)))). % 67.22/56.95 tff(c_54, plain, (![U_53, V_54]: (specific(U_53, V_54) | ~entity(U_53, V_54)))). % 67.22/56.95 tff(c_38, plain, (![U_37, V_38]: (event(U_37, V_38) | ~fire(U_37, V_38)))). % 67.22/56.95 tff(c_58, plain, (![U_57, V_58]: (nonliving(U_57, V_58) | ~object(U_57, V_58)))). % 67.22/56.95 tff(c_4, plain, (![U_3, V_4]: (sound(U_3, V_4) | ~scream(U_3, V_4)))). % 67.22/56.95 tff(c_248, plain, (animate(skc7, skc12))). % 67.22/56.95 tff(c_76, plain, (![U_75, V_76]: (animate(U_75, V_76) | ~human_person(U_75, V_76)))). % 67.22/56.95 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~object(U_59, V_60)))). % 67.22/56.95 tff(c_62, plain, (![U_61, V_62]: (unisex(U_61, V_62) | ~object(U_61, V_62)))). % 67.22/56.95 tff(c_237, plain, (human(skc7, skc12))). % 67.22/56.95 tff(c_233, plain, (human_person(skc7, skc12))). % 67.22/56.95 tff(c_64, plain, (![U_63, V_64]: (human_person(U_63, V_64) | ~man(U_63, V_64)))). % 67.22/56.95 tff(c_44, plain, (![U_43, V_44]: (instrumentality(U_43, V_44) | ~weaponry(U_43, V_44)))). % 67.22/56.95 tff(c_48, plain, (![U_47, V_48]: (object(U_47, V_48) | ~artifact(U_47, V_48)))). % 67.22/56.95 tff(c_70, plain, (![U_69, V_70]: (impartial(U_69, V_70) | ~organism(U_69, V_70)))). % 67.22/56.95 tff(c_52, plain, (![U_51, V_52]: (thing(U_51, V_52) | ~entity(U_51, V_52)))). % 67.22/56.95 tff(c_26, plain, (![U_25, V_26]: (act(U_25, V_26) | ~action(U_25, V_26)))). % 67.22/56.95 tff(c_46, plain, (![U_45, V_46]: (artifact(U_45, V_46) | ~instrumentality(U_45, V_46)))). % 67.22/56.95 tff(c_68, plain, (![U_67, V_68]: (entity(U_67, V_68) | ~organism(U_67, V_68)))). % 67.22/56.95 tff(c_14, plain, (![U_13, V_14]: (specific(U_13, V_14) | ~eventuality(U_13, V_14)))). % 67.22/56.95 tff(c_66, plain, (![U_65, V_66]: (organism(U_65, V_66) | ~human_person(U_65, V_66)))). % 67.22/56.95 tff(c_42, plain, (![U_41, V_42]: (weaponry(U_41, V_42) | ~weapon(U_41, V_42)))). % 67.22/56.95 tff(c_72, plain, (![U_71, V_72]: (living(U_71, V_72) | ~organism(U_71, V_72)))). % 67.22/56.95 tff(c_74, plain, (![U_73, V_74]: (human(U_73, V_74) | ~human_person(U_73, V_74)))). % 67.22/56.95 tff(c_40, plain, (![U_39, V_40]: (weapon(U_39, V_40) | ~cannon(U_39, V_40)))). % 67.22/56.95 tff(c_176, plain, (of(skc7, skc8, skc14))). % 67.22/56.95 tff(c_182, plain, (agent(skc7, skc8, skc10))). % 67.22/56.95 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 67.22/56.95 tff(c_178, plain, (of(skc7, skc11, skc12))). % 67.22/56.95 tff(c_180, plain, (patient(skc7, skc8, skc9))). % 67.22/56.95 tff(c_154, plain, (man(skc7, skc12))). % 67.22/56.95 tff(c_156, plain, (cannon(skc7, skc11))). % 67.22/56.95 tff(c_158, plain, (cry(skc7, skc9))). % 67.22/56.95 tff(c_174, plain, (revenge(skc7, skc14))). % 67.22/56.95 tff(c_172, plain, (event(skc7, skc8))). % 67.22/56.95 tff(c_152, plain, (male(skc7, skc12))). % 67.22/56.95 tff(c_170, plain, (present(skc7, skc8))). % 67.22/56.95 tff(c_160, plain, (male(skc7, skc10))). % 67.22/56.95 tff(c_162, plain, (six(skc7, skc10))). % 67.22/56.95 tff(c_164, plain, (group(skc7, skc10))). % 67.22/56.95 tff(c_166, plain, (scream(skc7, skc8))). % 67.22/56.95 tff(c_168, plain, (nonreflexive(skc7, skc8))). % 67.22/56.95 tff(c_150, plain, (actual_world(skc7))). % 67.22/56.95 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 67.22/56.95 %------------------------------------------------------------------------------