%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP058-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 : n027.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:04 PM UTC 2025 % Result : Satisfiable 21.89s 13.41s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP058-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/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.32 % Computer : n027.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Tue Apr 8 08:20:05 EDT 2025 % 0.12/0.32 % CPUTime : % 21.89/13.41 % 21.89/13.41 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.89/13.41 % 21.89/13.41 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.89/13.42 %$ patient > of > member > agent > woman > unisex > thing > substance_matter > ssSkP0 > specific > singleton > shake_beverage > set > relname > relation > present > possession > past > organism > order > object > nonreflexive > nonliving > nonhuman > nonexistent > multiple > mia_forename > living > impartial > human_person > human > group > general > forename > food > five > female > existent > eventuality > event > entity > dollar > currency > cost > cash > beverage > animate > act > abstraction > actual_world > skf21 > skf8 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc9 > skc8 > skc7 > skc6 > skc5 % 21.89/13.42 % 21.89/13.42 %Foreground sorts: % 21.89/13.42 % 21.89/13.42 % 21.89/13.42 %Background operators: % 21.89/13.42 % 21.89/13.42 % 21.89/13.42 %Foreground operators: % 21.89/13.42 tff(nonliving, type, nonliving: ($i * $i) > $o). % 21.89/13.42 tff(skf10, type, skf10: ($i * $i) > $i). % 21.89/13.42 tff(relation, type, relation: ($i * $i) > $o). % 21.89/13.42 tff(member, type, member: ($i * $i * $i) > $o). % 21.89/13.42 tff(forename, type, forename: ($i * $i) > $o). % 21.89/13.42 tff(skc7, type, skc7: $i). % 21.89/13.42 tff(female, type, female: ($i * $i) > $o). % 21.89/13.42 tff(living, type, living: ($i * $i) > $o). % 21.89/13.42 tff(cost, type, cost: ($i * $i) > $o). % 21.89/13.42 tff(human_person, type, human_person: ($i * $i) > $o). % 21.89/13.42 tff(present, type, present: ($i * $i) > $o). % 21.89/13.42 tff(entity, type, entity: ($i * $i) > $o). % 21.89/13.42 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 21.89/13.42 tff(skc9, type, skc9: $i). % 21.89/13.42 tff(ssSkP0, type, ssSkP0: ($i * $i) > $o). % 21.89/13.42 tff(past, type, past: ($i * $i) > $o). % 21.89/13.42 tff(beverage, type, beverage: ($i * $i) > $o). % 21.89/13.42 tff(eventuality, type, eventuality: ($i * $i) > $o). % 21.89/13.42 tff(existent, type, existent: ($i * $i) > $o). % 21.89/13.42 tff(abstraction, type, abstraction: ($i * $i) > $o). % 21.89/13.42 tff(skc8, type, skc8: $i). % 21.89/13.42 tff(relname, type, relname: ($i * $i) > $o). % 21.89/13.42 tff(possession, type, possession: ($i * $i) > $o). % 21.89/13.42 tff(singleton, type, singleton: ($i * $i) > $o). % 21.89/13.42 tff(multiple, type, multiple: ($i * $i) > $o). % 21.89/13.42 tff(organism, type, organism: ($i * $i) > $o). % 21.89/13.42 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 21.89/13.42 tff(animate, type, animate: ($i * $i) > $o). % 21.89/13.42 tff(of, type, of: ($i * $i * $i) > $o). % 21.89/13.42 tff(skf14, type, skf14: ($i * $i) > $i). % 21.89/13.42 tff(actual_world, type, actual_world: $i > $o). % 21.89/13.42 tff(dollar, type, dollar: ($i * $i) > $o). % 21.89/13.42 tff(agent, type, agent: ($i * $i * $i) > $o). % 21.89/13.42 tff(group, type, group: ($i * $i) > $o). % 21.89/13.42 tff(five, type, five: ($i * $i) > $o). % 21.89/13.42 tff(general, type, general: ($i * $i) > $o). % 21.89/13.42 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 21.89/13.42 tff(food, type, food: ($i * $i) > $o). % 21.89/13.42 tff(event, type, event: ($i * $i) > $o). % 21.89/13.42 tff(woman, type, woman: ($i * $i) > $o). % 21.89/13.42 tff(currency, type, currency: ($i * $i) > $o). % 21.89/13.42 tff(patient, type, patient: ($i * $i * $i) > $o). % 21.89/13.42 tff(skf8, type, skf8: ($i * $i) > $i). % 21.89/13.42 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 21.89/13.42 tff(cash, type, cash: ($i * $i) > $o). % 21.89/13.42 tff(thing, type, thing: ($i * $i) > $o). % 21.89/13.42 tff(human, type, human: ($i * $i) > $o). % 21.89/13.42 tff(skf18, type, skf18: ($i * $i) > $i). % 21.89/13.42 tff(skc5, type, skc5: $i). % 21.89/13.42 tff(unisex, type, unisex: ($i * $i) > $o). % 21.89/13.42 tff(skf16, type, skf16: ($i * $i) > $i). % 21.89/13.42 tff(set, type, set: ($i * $i) > $o). % 21.89/13.42 tff(skf12, type, skf12: ($i * $i) > $i). % 21.89/13.42 tff(skc6, type, skc6: $i). % 21.89/13.42 tff(impartial, type, impartial: ($i * $i) > $o). % 21.89/13.42 tff(object, type, object: ($i * $i) > $o). % 21.89/13.42 tff(order, type, order: ($i * $i) > $o). % 21.89/13.42 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 21.89/13.42 tff(specific, type, specific: ($i * $i) > $o). % 21.89/13.42 tff(skf20, type, skf20: ($i * $i) > $i). % 21.89/13.42 tff(act, type, act: ($i * $i) > $o). % 21.89/13.42 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 21.89/13.42 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i) > $i). % 21.89/13.42 % 21.89/13.42 %Saturated clause set: % 21.89/13.42 tff(c_1361, plain, (![X1_1074, Z_1078, U_178, V_1064, X_181, Z_179, Z_1086, X_1085, X1_1084, Y_1079, X1_1083, Y_182, Z_1061, X_1073, Z_1081, V_1059, Y_1060, Y_1082, X_1066, Y_1063, Y_1067, V_1062, X1_180, W_177, W_1077, V_183, X1_1071, X1_1075, V_1072, V_1065, X_1076, Z_1069, X_1070]: (skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, W_177, U_178)=skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, W_177, U_178) | skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, W_177, U_178)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, W_177, U_178) | skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, W_177, U_178)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, W_177, U_178) | skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, W_177, U_178)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, W_177, U_178) | skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, W_177, U_178)=skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, W_177, U_178) | skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, W_177, U_178)=skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1062, W_1077, X_1070, Y_1067, Z_1081, X1_1071)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1061=X1_1075 | Z_1061=Y_1079 | Y_1079=X1_1075 | Y_1079=X_1073 | Z_1061=X_1073 | X_1073=X1_1075 | X_1073=V_1072 | Y_1079=V_1072 | Z_1061=V_1072 | X1_1075=V_1072 | ~member(U_178, X1_1075, W_177) | ~member(U_178, Z_1061, W_177) | ~member(U_178, Y_1079, W_177) | ~member(U_178, X_1073, W_177) | ~member(U_178, V_1072, W_177) | Z_1069=X1_1074 | Z_1069=Y_1082 | Y_1082=X1_1074 | Y_1082=X_1066 | Z_1069=X_1066 | X_1066=X1_1074 | X_1066=V_1065 | Y_1082=V_1065 | Z_1069=V_1065 | X1_1074=V_1065 | ~member(U_178, X1_1074, W_177) | ~member(U_178, Z_1069, W_177) | ~member(U_178, Y_1082, W_177) | ~member(U_178, X_1066, W_177) | ~member(U_178, V_1065, W_177) | Z_1086=X1_1084 | Z_1086=Y_1060 | Y_1060=X1_1084 | Y_1060=X_1076 | Z_1086=X_1076 | X_1076=X1_1084 | X_1076=V_1059 | Y_1060=V_1059 | Z_1086=V_1059 | X1_1084=V_1059 | ~member(U_178, X1_1084, W_177) | ~member(U_178, Z_1086, W_177) | ~member(U_178, Y_1060, W_177) | ~member(U_178, X_1076, W_177) | ~member(U_178, V_1059, W_177) | Z_1078=X1_1083 | Z_1078=Y_1063 | Y_1063=X1_1083 | Y_1063=X_1085 | Z_1078=X_1085 | X_1085=X1_1083 | X_1085=V_1064 | Y_1063=V_1064 | Z_1078=V_1064 | X1_1083=V_1064 | ~member(U_178, X1_1083, W_177) | ~member(U_178, Z_1078, W_177) | ~member(U_178, Y_1063, W_177) | ~member(U_178, X_1085, W_177) | ~member(U_178, V_1064, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.42 tff(c_1332, plain, (![V_978, X1_977, Z_988, U_178, X1_987, X_181, Z_179, W_983, X1_980, V_966, Y_984, Y_182, X_979, Y_986, Z_975, Y_967, Z_968, V_969, X_972, Y_973, X1_981, V_971, X_976, X1_180, W_177, V_183, Z_985, X_982]: (skf21(V_978, X_979, Y_984, Z_968, X1_981, W_177, U_178)=skf21(V_971, X_972, Y_986, Z_975, X1_980, W_177, U_178) | skf21(V_971, X_972, Y_986, Z_975, X1_980, W_177, U_178)=skf21(V_966, X_982, Y_967, Z_988, X1_987, W_177, U_178) | skf21(V_978, X_979, Y_984, Z_968, X1_981, W_177, U_178)=skf21(V_966, X_982, Y_967, Z_988, X1_987, W_177, U_178) | skf21(V_966, X_982, Y_967, Z_988, X1_987, W_177, U_178)=skf10(W_177, U_178) | skf21(V_971, X_972, Y_986, Z_975, X1_980, W_177, U_178)=skf10(W_177, U_178) | skf21(V_978, X_979, Y_984, Z_968, X1_981, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_966, X_982, Y_967, Z_988, X1_987, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_971, X_972, Y_986, Z_975, X1_980, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_978, X_979, Y_984, Z_968, X1_981, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_969, W_983, X_976, Y_973, Z_985, X1_977)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_968=X1_981 | Z_968=Y_984 | Y_984=X1_981 | Y_984=X_979 | Z_968=X_979 | X_979=X1_981 | X_979=V_978 | Y_984=V_978 | Z_968=V_978 | X1_981=V_978 | ~member(U_178, X1_981, W_177) | ~member(U_178, Z_968, W_177) | ~member(U_178, Y_984, W_177) | ~member(U_178, X_979, W_177) | ~member(U_178, V_978, W_177) | Z_975=X1_980 | Z_975=Y_986 | Y_986=X1_980 | Y_986=X_972 | Z_975=X_972 | X_972=X1_980 | X_972=V_971 | Y_986=V_971 | Z_975=V_971 | X1_980=V_971 | ~member(U_178, X1_980, W_177) | ~member(U_178, Z_975, W_177) | ~member(U_178, Y_986, W_177) | ~member(U_178, X_972, W_177) | ~member(U_178, V_971, W_177) | Z_988=X1_987 | Z_988=Y_967 | Y_967=X1_987 | Y_967=X_982 | Z_988=X_982 | X_982=X1_987 | X_982=V_966 | Y_967=V_966 | Z_988=V_966 | X1_987=V_966 | ~member(U_178, X1_987, W_177) | ~member(U_178, Z_988, W_177) | ~member(U_178, Y_967, W_177) | ~member(U_178, X_982, W_177) | ~member(U_178, V_966, W_177) | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.42 tff(c_1307, plain, (![X_963, Y_960, U_178, V_945, X_942, X1_959, Z_947, X_181, Z_179, Z_965, X_962, X1_956, Y_952, Y_182, V_961, Y_944, Z_949, Z_953, X_954, X1_946, W_951, X1_180, V_943, W_177, U_958, X1_950, V_183, Y_957]: (skf21(V_961, X_942, Y_957, Z_947, X1_946, W_177, U_178)=skf21(V_943, X_963, Y_960, Z_965, X1_959, W_177, U_178) | skf21(V_961, X_942, Y_957, Z_947, X1_946, W_177, U_178)=skf21(V_945, X_962, Y_944, Z_953, X1_956, W_177, U_178) | skf21(V_945, X_962, Y_944, Z_953, X1_956, W_177, U_178)=skf21(V_943, X_963, Y_960, Z_965, X1_959, W_177, U_178) | skf21(V_945, X_962, Y_944, Z_953, X1_956, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_961, X_942, Y_957, Z_947, X1_946, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_943, X_963, Y_960, Z_965, X1_959, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_958 | skf21(V_945, X_962, Y_944, Z_953, X1_956, W_177, U_178)=U_958 | skf21(V_961, X_942, Y_957, Z_947, X1_946, W_177, U_178)=U_958 | skf21(V_943, X_963, Y_960, Z_965, X1_959, W_177, U_178)=U_958 | ~member(U_178, U_958, W_177) | skf21(U_958, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_951, X_954, Y_952, Z_949, X1_950)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_965=X1_959 | Z_965=Y_960 | Y_960=X1_959 | Y_960=X_963 | Z_965=X_963 | X_963=X1_959 | X_963=V_943 | Y_960=V_943 | Z_965=V_943 | X1_959=V_943 | ~member(U_178, X1_959, W_177) | ~member(U_178, Z_965, W_177) | ~member(U_178, Y_960, W_177) | ~member(U_178, X_963, W_177) | ~member(U_178, V_943, W_177) | Z_947=X1_946 | Z_947=Y_957 | Y_957=X1_946 | Y_957=X_942 | Z_947=X_942 | X_942=X1_946 | X_942=V_961 | Y_957=V_961 | Z_947=V_961 | X1_946=V_961 | ~member(U_178, X1_946, W_177) | ~member(U_178, Z_947, W_177) | ~member(U_178, Y_957, W_177) | ~member(U_178, X_942, W_177) | ~member(U_178, V_961, W_177) | Z_953=X1_956 | Z_953=Y_944 | Y_944=X1_956 | Y_944=X_962 | Z_953=X_962 | X_962=X1_956 | X_962=V_945 | Y_944=V_945 | Z_953=V_945 | X1_956=V_945 | ~member(U_178, X1_956, W_177) | ~member(U_178, Z_953, W_177) | ~member(U_178, Y_944, W_177) | ~member(U_178, X_962, W_177) | ~member(U_178, V_945, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1364, plain, (![X1_1074, Z_1078, V_210, V_1064, Z_1086, X_1085, X1_1084, Y_1079, X1_1083, Z_1061, X_1073, Z_1081, V_1059, Y_1060, Y_1082, X_1066, Y_1063, Y_1067, V_1062, W_1077, X1_1071, X1_1075, V_1072, V_1065, X_1076, Z_1069, U_209, X_1070]: (skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, U_209, V_210)=skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, U_209, V_210) | skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, U_209, V_210)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, U_209, V_210) | skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, U_209, V_210)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, U_209, V_210) | skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, U_209, V_210)=skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, U_209, V_210) | skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, U_209, V_210)=skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, U_209, V_210) | skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, U_209, V_210)=skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, U_209, V_210) | skf21(V_1064, X_1085, Y_1063, Z_1078, X1_1083, U_209, V_210)=skf10(U_209, V_210) | skf21(V_1059, X_1076, Y_1060, Z_1086, X1_1084, U_209, V_210)=skf10(U_209, V_210) | skf21(V_1065, X_1066, Y_1082, Z_1069, X1_1074, U_209, V_210)=skf10(U_209, V_210) | skf21(V_1072, X_1073, Y_1079, Z_1061, X1_1075, U_209, V_210)=skf10(U_209, V_210) | skf21(skf10(U_209, V_210), V_1062, W_1077, X_1070, Y_1067, Z_1081, X1_1071)!=skf10(U_209, V_210) | Z_1061=X1_1075 | Z_1061=Y_1079 | Y_1079=X1_1075 | Y_1079=X_1073 | Z_1061=X_1073 | X_1073=X1_1075 | X_1073=V_1072 | Y_1079=V_1072 | Z_1061=V_1072 | X1_1075=V_1072 | ~member(V_210, X1_1075, U_209) | ~member(V_210, Z_1061, U_209) | ~member(V_210, Y_1079, U_209) | ~member(V_210, X_1073, U_209) | ~member(V_210, V_1072, U_209) | Z_1069=X1_1074 | Z_1069=Y_1082 | Y_1082=X1_1074 | Y_1082=X_1066 | Z_1069=X_1066 | X_1066=X1_1074 | X_1066=V_1065 | Y_1082=V_1065 | Z_1069=V_1065 | X1_1074=V_1065 | ~member(V_210, X1_1074, U_209) | ~member(V_210, Z_1069, U_209) | ~member(V_210, Y_1082, U_209) | ~member(V_210, X_1066, U_209) | ~member(V_210, V_1065, U_209) | Z_1086=X1_1084 | Z_1086=Y_1060 | Y_1060=X1_1084 | Y_1060=X_1076 | Z_1086=X_1076 | X_1076=X1_1084 | X_1076=V_1059 | Y_1060=V_1059 | Z_1086=V_1059 | X1_1084=V_1059 | ~member(V_210, X1_1084, U_209) | ~member(V_210, Z_1086, U_209) | ~member(V_210, Y_1060, U_209) | ~member(V_210, X_1076, U_209) | ~member(V_210, V_1059, U_209) | Z_1078=X1_1083 | Z_1078=Y_1063 | Y_1063=X1_1083 | Y_1063=X_1085 | Z_1078=X_1085 | X_1085=X1_1083 | X_1085=V_1064 | Y_1063=V_1064 | Z_1078=V_1064 | X1_1083=V_1064 | five(V_210, U_209) | ~member(V_210, X1_1083, U_209) | ~member(V_210, Z_1078, U_209) | ~member(V_210, Y_1063, U_209) | ~member(V_210, X_1085, U_209) | ~member(V_210, V_1064, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_1282, plain, (![Y_929, U_924, X1_937, U_178, X_181, Z_179, X_925, V_917, V_939, Z_933, Y_182, V_926, Z_930, X1_921, Z_940, X1_180, V_920, Y_923, Y_931, W_177, X1_936, V_183, X_938, Y_919, X_927, W_918, X_928, Z_935, X1_932]: (skf21(V_939, X_925, Y_929, Z_935, X1_921, W_177, U_178)=skf21(V_917, X_928, Y_923, Z_940, X1_937, W_177, U_178) | skf21(V_939, X_925, Y_929, Z_935, X1_921, W_177, U_178)=skf21(V_920, X_938, Y_919, Z_933, X1_936, W_177, U_178) | skf21(V_920, X_938, Y_919, Z_933, X1_936, W_177, U_178)=skf21(V_917, X_928, Y_923, Z_940, X1_937, W_177, U_178) | skf21(V_920, X_938, Y_919, Z_933, X1_936, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_939, X_925, Y_929, Z_935, X1_921, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_917, X_928, Y_923, Z_940, X1_937, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_924 | skf21(V_920, X_938, Y_919, Z_933, X1_936, W_177, U_178)=U_924 | skf21(V_939, X_925, Y_929, Z_935, X1_921, W_177, U_178)=U_924 | skf21(V_917, X_928, Y_923, Z_940, X1_937, W_177, U_178)=U_924 | ~member(U_178, U_924, W_177) | skf21(U_924, V_926, W_918, X_927, Y_931, Z_930, X1_932)!=U_924 | Z_940=X1_937 | Z_940=Y_923 | Y_923=X1_937 | Y_923=X_928 | Z_940=X_928 | X_928=X1_937 | X_928=V_917 | Y_923=V_917 | Z_940=V_917 | X1_937=V_917 | ~member(U_178, X1_937, W_177) | ~member(U_178, Z_940, W_177) | ~member(U_178, Y_923, W_177) | ~member(U_178, X_928, W_177) | ~member(U_178, V_917, W_177) | Z_935=X1_921 | Z_935=Y_929 | Y_929=X1_921 | Y_929=X_925 | Z_935=X_925 | X_925=X1_921 | X_925=V_939 | Y_929=V_939 | Z_935=V_939 | X1_921=V_939 | ~member(U_178, X1_921, W_177) | ~member(U_178, Z_935, W_177) | ~member(U_178, Y_929, W_177) | ~member(U_178, X_925, W_177) | ~member(U_178, V_939, W_177) | Z_933=X1_936 | Z_933=Y_919 | Y_919=X1_936 | Y_919=X_938 | Z_933=X_938 | X_938=X1_936 | X_938=V_920 | Y_919=V_920 | Z_933=V_920 | X1_936=V_920 | ~member(U_178, X1_936, W_177) | ~member(U_178, Z_933, W_177) | ~member(U_178, Y_919, W_177) | ~member(U_178, X_938, W_177) | ~member(U_178, V_920, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1227, plain, (![X_840, Y_838, X1_831, U_178, X_181, Z_179, Z_830, Z_842, X1_837, Y_835, Y_182, X_834, U_836, V_839, X1_827, X1_180, W_177, W_832, V_183, X_824, V_825, Y_833, Z_828]: (skf21(V_839, X_824, Y_835, Z_828, X1_827, W_177, U_178)=skf21(V_825, X_840, Y_838, Z_842, X1_837, W_177, U_178) | skf21(V_839, X_824, Y_835, Z_828, X1_827, W_177, U_178)=skf10(W_177, U_178) | skf21(V_825, X_840, Y_838, Z_842, X1_837, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_839, X_824, Y_835, Z_828, X1_827, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_825, X_840, Y_838, Z_842, X1_837, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_836 | skf10(W_177, U_178)=U_836 | skf21(V_839, X_824, Y_835, Z_828, X1_827, W_177, U_178)=U_836 | skf21(V_825, X_840, Y_838, Z_842, X1_837, W_177, U_178)=U_836 | ~member(U_178, U_836, W_177) | skf21(U_836, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_832, X_834, Y_833, Z_830, X1_831)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_842=X1_837 | Z_842=Y_838 | Y_838=X1_837 | Y_838=X_840 | Z_842=X_840 | X_840=X1_837 | X_840=V_825 | Y_838=V_825 | Z_842=V_825 | X1_837=V_825 | ~member(U_178, X1_837, W_177) | ~member(U_178, Z_842, W_177) | ~member(U_178, Y_838, W_177) | ~member(U_178, X_840, W_177) | ~member(U_178, V_825, W_177) | Z_828=X1_827 | Z_828=Y_835 | Y_835=X1_827 | Y_835=X_824 | Z_828=X_824 | X_824=X1_827 | X_824=V_839 | Y_835=V_839 | Z_828=V_839 | X1_827=V_839 | ~member(U_178, X1_827, W_177) | ~member(U_178, Z_828, W_177) | ~member(U_178, Y_835, W_177) | ~member(U_178, X_824, W_177) | ~member(U_178, V_839, W_177) | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1310, plain, (![X_963, Y_960, V_210, V_945, X_942, X1_959, Z_947, Z_965, X_962, X1_956, Y_952, V_961, Y_944, Z_949, Z_953, X_954, X1_946, W_951, V_943, U_958, X1_950, U_209, Y_957]: (skf21(V_961, X_942, Y_957, Z_947, X1_946, U_209, V_210)=skf21(V_943, X_963, Y_960, Z_965, X1_959, U_209, V_210) | skf21(V_961, X_942, Y_957, Z_947, X1_946, U_209, V_210)=skf21(V_945, X_962, Y_944, Z_953, X1_956, U_209, V_210) | skf21(V_945, X_962, Y_944, Z_953, X1_956, U_209, V_210)=skf21(V_943, X_963, Y_960, Z_965, X1_959, U_209, V_210) | skf21(V_945, X_962, Y_944, Z_953, X1_956, U_209, V_210)=skf10(U_209, V_210) | skf21(V_961, X_942, Y_957, Z_947, X1_946, U_209, V_210)=skf10(U_209, V_210) | skf21(V_943, X_963, Y_960, Z_965, X1_959, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=U_958 | skf21(V_945, X_962, Y_944, Z_953, X1_956, U_209, V_210)=U_958 | skf21(V_961, X_942, Y_957, Z_947, X1_946, U_209, V_210)=U_958 | skf21(V_943, X_963, Y_960, Z_965, X1_959, U_209, V_210)=U_958 | ~member(V_210, U_958, U_209) | skf21(U_958, skf10(U_209, V_210), W_951, X_954, Y_952, Z_949, X1_950)!=skf10(U_209, V_210) | Z_965=X1_959 | Z_965=Y_960 | Y_960=X1_959 | Y_960=X_963 | Z_965=X_963 | X_963=X1_959 | X_963=V_943 | Y_960=V_943 | Z_965=V_943 | X1_959=V_943 | ~member(V_210, X1_959, U_209) | ~member(V_210, Z_965, U_209) | ~member(V_210, Y_960, U_209) | ~member(V_210, X_963, U_209) | ~member(V_210, V_943, U_209) | Z_947=X1_946 | Z_947=Y_957 | Y_957=X1_946 | Y_957=X_942 | Z_947=X_942 | X_942=X1_946 | X_942=V_961 | Y_957=V_961 | Z_947=V_961 | X1_946=V_961 | ~member(V_210, X1_946, U_209) | ~member(V_210, Z_947, U_209) | ~member(V_210, Y_957, U_209) | ~member(V_210, X_942, U_209) | ~member(V_210, V_961, U_209) | Z_953=X1_956 | Z_953=Y_944 | Y_944=X1_956 | Y_944=X_962 | Z_953=X_962 | X_962=X1_956 | X_962=V_945 | Y_944=V_945 | Z_953=V_945 | X1_956=V_945 | five(V_210, U_209) | ~member(V_210, X1_956, U_209) | ~member(V_210, Z_953, U_209) | ~member(V_210, Y_944, U_209) | ~member(V_210, X_962, U_209) | ~member(V_210, V_945, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_1202, plain, (![X_821, V_810, X1_808, Z_820, V_819, Z_809, Z_812, U_178, Y_813, X_181, Z_179, X1_815, X_818, Y_182, X1_816, X_817, Y_822, X1_180, W_177, V_183, Y_805, V_806, U_823]: (skf21(V_810, X_817, Y_822, Z_809, X1_808, W_177, U_178)=skf21(V_806, X_818, Y_805, Z_812, X1_815, W_177, U_178) | skf21(V_806, X_818, Y_805, Z_812, X1_815, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_810, X_817, Y_822, Z_809, X1_808, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_819 | skf21(V_806, X_818, Y_805, Z_812, X1_815, W_177, U_178)=V_819 | skf21(V_810, X_817, Y_822, Z_809, X1_808, W_177, U_178)=V_819 | V_819=U_823 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_823 | skf21(V_806, X_818, Y_805, Z_812, X1_815, W_177, U_178)=U_823 | skf21(V_810, X_817, Y_822, Z_809, X1_808, W_177, U_178)=U_823 | ~member(U_178, V_819, W_177) | ~member(U_178, U_823, W_177) | skf21(U_823, V_819, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_821, Y_813, Z_820, X1_816)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_809=X1_808 | Z_809=Y_822 | Y_822=X1_808 | Y_822=X_817 | Z_809=X_817 | X_817=X1_808 | X_817=V_810 | Y_822=V_810 | Z_809=V_810 | X1_808=V_810 | ~member(U_178, X1_808, W_177) | ~member(U_178, Z_809, W_177) | ~member(U_178, Y_822, W_177) | ~member(U_178, X_817, W_177) | ~member(U_178, V_810, W_177) | Z_812=X1_815 | Z_812=Y_805 | Y_805=X1_815 | Y_805=X_818 | Z_812=X_818 | X_818=X1_815 | X_818=V_806 | Y_805=V_806 | Z_812=V_806 | X1_815=V_806 | ~member(U_178, X1_815, W_177) | ~member(U_178, Z_812, W_177) | ~member(U_178, Y_805, W_177) | ~member(U_178, X_818, W_177) | ~member(U_178, V_806, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1285, plain, (![Y_929, U_924, X1_937, V_210, X_925, V_917, V_939, Z_933, V_926, Z_930, X1_921, Z_940, V_920, Y_923, Y_931, X1_936, X_938, Y_919, X_927, W_918, X_928, Z_935, U_209, X1_932]: (skf21(V_939, X_925, Y_929, Z_935, X1_921, U_209, V_210)=skf21(V_917, X_928, Y_923, Z_940, X1_937, U_209, V_210) | skf21(V_939, X_925, Y_929, Z_935, X1_921, U_209, V_210)=skf21(V_920, X_938, Y_919, Z_933, X1_936, U_209, V_210) | skf21(V_920, X_938, Y_919, Z_933, X1_936, U_209, V_210)=skf21(V_917, X_928, Y_923, Z_940, X1_937, U_209, V_210) | skf21(V_920, X_938, Y_919, Z_933, X1_936, U_209, V_210)=skf10(U_209, V_210) | skf21(V_939, X_925, Y_929, Z_935, X1_921, U_209, V_210)=skf10(U_209, V_210) | skf21(V_917, X_928, Y_923, Z_940, X1_937, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=U_924 | skf21(V_920, X_938, Y_919, Z_933, X1_936, U_209, V_210)=U_924 | skf21(V_939, X_925, Y_929, Z_935, X1_921, U_209, V_210)=U_924 | skf21(V_917, X_928, Y_923, Z_940, X1_937, U_209, V_210)=U_924 | ~member(V_210, U_924, U_209) | skf21(U_924, V_926, W_918, X_927, Y_931, Z_930, X1_932)!=U_924 | Z_940=X1_937 | Z_940=Y_923 | Y_923=X1_937 | Y_923=X_928 | Z_940=X_928 | X_928=X1_937 | X_928=V_917 | Y_923=V_917 | Z_940=V_917 | X1_937=V_917 | ~member(V_210, X1_937, U_209) | ~member(V_210, Z_940, U_209) | ~member(V_210, Y_923, U_209) | ~member(V_210, X_928, U_209) | ~member(V_210, V_917, U_209) | Z_935=X1_921 | Z_935=Y_929 | Y_929=X1_921 | Y_929=X_925 | Z_935=X_925 | X_925=X1_921 | X_925=V_939 | Y_929=V_939 | Z_935=V_939 | X1_921=V_939 | ~member(V_210, X1_921, U_209) | ~member(V_210, Z_935, U_209) | ~member(V_210, Y_929, U_209) | ~member(V_210, X_925, U_209) | ~member(V_210, V_939, U_209) | Z_933=X1_936 | Z_933=Y_919 | Y_919=X1_936 | Y_919=X_938 | Z_933=X_938 | X_938=X1_936 | X_938=V_920 | Y_919=V_920 | Z_933=V_920 | X1_936=V_920 | five(V_210, U_209) | ~member(V_210, X1_936, U_209) | ~member(V_210, Z_933, U_209) | ~member(V_210, Y_919, U_209) | ~member(V_210, X_938, U_209) | ~member(V_210, V_920, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_1177, plain, (![V_787, X1_797, X1_803, X_788, Z_795, U_178, Y_802, X_181, Z_179, U_804, Z_794, X1_799, Y_182, X_785, Y_786, Y_791, Z_793, X_801, V_789, X1_180, W_177, V_183, W_800, V_792]: (skf21(V_789, X_788, Y_802, Z_795, X1_803, W_177, U_178)=skf21(V_787, X_801, Y_786, Z_794, X1_799, W_177, U_178) | skf21(V_787, X_801, Y_786, Z_794, X1_799, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_789, X_788, Y_802, Z_795, X1_803, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_792 | skf21(V_787, X_801, Y_786, Z_794, X1_799, W_177, U_178)=V_792 | skf21(V_789, X_788, Y_802, Z_795, X1_803, W_177, U_178)=V_792 | V_792=U_804 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_804 | skf21(V_787, X_801, Y_786, Z_794, X1_799, W_177, U_178)=U_804 | skf21(V_789, X_788, Y_802, Z_795, X1_803, W_177, U_178)=U_804 | ~member(U_178, V_792, W_177) | ~member(U_178, U_804, W_177) | skf21(U_804, V_792, W_800, X_785, Y_791, Z_793, X1_797)!=V_792 | Z_795=X1_803 | Z_795=Y_802 | Y_802=X1_803 | Y_802=X_788 | Z_795=X_788 | X_788=X1_803 | X_788=V_789 | Y_802=V_789 | Z_795=V_789 | X1_803=V_789 | ~member(U_178, X1_803, W_177) | ~member(U_178, Z_795, W_177) | ~member(U_178, Y_802, W_177) | ~member(U_178, X_788, W_177) | ~member(U_178, V_789, W_177) | Z_794=X1_799 | Z_794=Y_786 | Y_786=X1_799 | Y_786=X_801 | Z_794=X_801 | X_801=X1_799 | X_801=V_787 | Y_786=V_787 | Z_794=V_787 | X1_799=V_787 | ~member(U_178, X1_799, W_177) | ~member(U_178, Z_794, W_177) | ~member(U_178, Y_786, W_177) | ~member(U_178, X_801, W_177) | ~member(U_178, V_787, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1152, plain, (![Z_772, U_178, Y_771, X1_777, X_181, Z_179, U_778, V_774, Y_764, Y_182, V_766, X1_769, X4_779, X1_782, X_784, X1_180, W_177, V_765, X_780, X_768, V_183, Z_775, Z_770, Y_781, W_783]: (skf21(V_774, X_784, Y_781, Z_772, X1_782, W_177, U_178)=skf21(V_765, X_780, Y_764, Z_775, X1_777, W_177, U_178) | skf21(V_765, X_780, Y_764, Z_775, X1_777, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_774, X_784, Y_781, Z_772, X1_782, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_779 | skf21(V_765, X_780, Y_764, Z_775, X1_777, W_177, U_178)=X4_779 | skf21(V_774, X_784, Y_781, Z_772, X1_782, W_177, U_178)=X4_779 | X4_779=U_778 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_778 | skf21(V_765, X_780, Y_764, Z_775, X1_777, W_177, U_178)=U_778 | skf21(V_774, X_784, Y_781, Z_772, X1_782, W_177, U_178)=U_778 | ~member(U_178, X4_779, W_177) | ~member(U_178, U_778, W_177) | skf21(U_778, V_766, W_783, X_768, Y_771, Z_770, X1_769)!=U_778 | Z_772=X1_782 | Z_772=Y_781 | Y_781=X1_782 | Y_781=X_784 | Z_772=X_784 | X_784=X1_782 | X_784=V_774 | Y_781=V_774 | Z_772=V_774 | X1_782=V_774 | ~member(U_178, X1_782, W_177) | ~member(U_178, Z_772, W_177) | ~member(U_178, Y_781, W_177) | ~member(U_178, X_784, W_177) | ~member(U_178, V_774, W_177) | Z_775=X1_777 | Z_775=Y_764 | Y_764=X1_777 | Y_764=X_780 | Z_775=X_780 | X_780=X1_777 | X_780=V_765 | Y_764=V_765 | Z_775=V_765 | X1_777=V_765 | ~member(U_178, X1_777, W_177) | ~member(U_178, Z_775, W_177) | ~member(U_178, Y_764, W_177) | ~member(U_178, X_780, W_177) | ~member(U_178, V_765, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1071, plain, (![V_689, Z_683, U_178, X_181, Z_179, Z_690, X_688, U_693, X_691, Y_182, Y_692, X1_687, Y_686, V_684, X1_180, W_177, V_183, X1_682]: (skf21(V_684, X_688, Y_692, Z_683, X1_682, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_684, X_688, Y_692, Z_683, X1_682, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_689 | skf10(W_177, U_178)=V_689 | skf21(V_684, X_688, Y_692, Z_683, X1_682, W_177, U_178)=V_689 | V_689=U_693 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_693 | skf10(W_177, U_178)=U_693 | skf21(V_684, X_688, Y_692, Z_683, X1_682, W_177, U_178)=U_693 | ~member(U_178, V_689, W_177) | ~member(U_178, U_693, W_177) | skf21(U_693, V_689, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_691, Y_686, Z_690, X1_687)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_683=X1_682 | Z_683=Y_692 | Y_692=X1_682 | Y_692=X_688 | Z_683=X_688 | X_688=X1_682 | X_688=V_684 | Y_692=V_684 | Z_683=V_684 | X1_682=V_684 | ~member(U_178, X1_682, W_177) | ~member(U_178, Z_683, W_177) | ~member(U_178, Y_692, W_177) | ~member(U_178, X_688, W_177) | ~member(U_178, V_684, W_177) | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1205, plain, (![X_821, V_810, X1_808, Z_820, V_819, Z_809, V_210, Z_812, Y_813, X1_815, X_818, X1_816, X_817, Y_822, Y_805, U_209, V_806, U_823]: (skf21(V_810, X_817, Y_822, Z_809, X1_808, U_209, V_210)=skf21(V_806, X_818, Y_805, Z_812, X1_815, U_209, V_210) | skf21(V_806, X_818, Y_805, Z_812, X1_815, U_209, V_210)=skf10(U_209, V_210) | skf21(V_810, X_817, Y_822, Z_809, X1_808, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=V_819 | skf21(V_806, X_818, Y_805, Z_812, X1_815, U_209, V_210)=V_819 | skf21(V_810, X_817, Y_822, Z_809, X1_808, U_209, V_210)=V_819 | V_819=U_823 | skf10(U_209, V_210)=U_823 | skf21(V_806, X_818, Y_805, Z_812, X1_815, U_209, V_210)=U_823 | skf21(V_810, X_817, Y_822, Z_809, X1_808, U_209, V_210)=U_823 | ~member(V_210, V_819, U_209) | ~member(V_210, U_823, U_209) | skf21(U_823, V_819, skf10(U_209, V_210), X_821, Y_813, Z_820, X1_816)!=skf10(U_209, V_210) | Z_809=X1_808 | Z_809=Y_822 | Y_822=X1_808 | Y_822=X_817 | Z_809=X_817 | X_817=X1_808 | X_817=V_810 | Y_822=V_810 | Z_809=V_810 | X1_808=V_810 | ~member(V_210, X1_808, U_209) | ~member(V_210, Z_809, U_209) | ~member(V_210, Y_822, U_209) | ~member(V_210, X_817, U_209) | ~member(V_210, V_810, U_209) | Z_812=X1_815 | Z_812=Y_805 | Y_805=X1_815 | Y_805=X_818 | Z_812=X_818 | X_818=X1_815 | X_818=V_806 | Y_805=V_806 | Z_812=V_806 | X1_815=V_806 | five(V_210, U_209) | ~member(V_210, X1_815, U_209) | ~member(V_210, Z_812, U_209) | ~member(V_210, Y_805, U_209) | ~member(V_210, X_818, U_209) | ~member(V_210, V_806, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_1155, plain, (![Z_772, V_210, Y_771, X1_777, U_778, V_774, Y_764, V_766, X1_769, X4_779, X1_782, X_784, V_765, X_780, X_768, Z_775, Z_770, U_209, Y_781, W_783]: (skf21(V_774, X_784, Y_781, Z_772, X1_782, U_209, V_210)=skf21(V_765, X_780, Y_764, Z_775, X1_777, U_209, V_210) | skf21(V_765, X_780, Y_764, Z_775, X1_777, U_209, V_210)=skf10(U_209, V_210) | skf21(V_774, X_784, Y_781, Z_772, X1_782, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=X4_779 | skf21(V_765, X_780, Y_764, Z_775, X1_777, U_209, V_210)=X4_779 | skf21(V_774, X_784, Y_781, Z_772, X1_782, U_209, V_210)=X4_779 | X4_779=U_778 | skf10(U_209, V_210)=U_778 | skf21(V_765, X_780, Y_764, Z_775, X1_777, U_209, V_210)=U_778 | skf21(V_774, X_784, Y_781, Z_772, X1_782, U_209, V_210)=U_778 | ~member(V_210, X4_779, U_209) | ~member(V_210, U_778, U_209) | skf21(U_778, V_766, W_783, X_768, Y_771, Z_770, X1_769)!=U_778 | Z_772=X1_782 | Z_772=Y_781 | Y_781=X1_782 | Y_781=X_784 | Z_772=X_784 | X_784=X1_782 | X_784=V_774 | Y_781=V_774 | Z_772=V_774 | X1_782=V_774 | ~member(V_210, X1_782, U_209) | ~member(V_210, Z_772, U_209) | ~member(V_210, Y_781, U_209) | ~member(V_210, X_784, U_209) | ~member(V_210, V_774, U_209) | Z_775=X1_777 | Z_775=Y_764 | Y_764=X1_777 | Y_764=X_780 | Z_775=X_780 | X_780=X1_777 | X_780=V_765 | Y_764=V_765 | Z_775=V_765 | X1_777=V_765 | five(V_210, U_209) | ~member(V_210, X1_777, U_209) | ~member(V_210, Z_775, U_209) | ~member(V_210, Y_764, U_209) | ~member(V_210, X_780, U_209) | ~member(V_210, V_765, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_1046, plain, (![U_178, X_668, U_674, Y_673, X_181, Z_179, Y_182, X1_676, V_666, V_677, Z_671, X1_180, W_177, V_183, Z_679, W_669, X1_678, Y_672]: (skf21(V_666, X_668, Y_673, Z_671, X1_676, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_669 | skf21(V_666, X_668, Y_673, Z_671, X1_676, W_177, U_178)=W_669 | W_669=V_677 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_677 | skf21(V_666, X_668, Y_673, Z_671, X1_676, W_177, U_178)=V_677 | V_677=U_674 | W_669=U_674 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_674 | skf21(V_666, X_668, Y_673, Z_671, X1_676, W_177, U_178)=U_674 | ~member(U_178, W_669, W_177) | ~member(U_178, V_677, W_177) | ~member(U_178, U_674, W_177) | skf21(U_674, V_677, W_669, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_672, Z_679, X1_678)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_671=X1_676 | Z_671=Y_673 | Y_673=X1_676 | Y_673=X_668 | Z_671=X_668 | X_668=X1_676 | X_668=V_666 | Y_673=V_666 | Z_671=V_666 | X1_676=V_666 | ~member(U_178, X1_676, W_177) | ~member(U_178, Z_671, W_177) | ~member(U_178, Y_673, W_177) | ~member(U_178, X_668, W_177) | ~member(U_178, V_666, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1180, plain, (![V_787, X1_797, X1_803, X_788, Z_795, V_210, Y_802, U_804, Z_794, X1_799, X_785, Y_786, Y_791, Z_793, X_801, V_789, W_800, V_792, U_209]: (skf21(V_789, X_788, Y_802, Z_795, X1_803, U_209, V_210)=skf21(V_787, X_801, Y_786, Z_794, X1_799, U_209, V_210) | skf21(V_787, X_801, Y_786, Z_794, X1_799, U_209, V_210)=skf10(U_209, V_210) | skf21(V_789, X_788, Y_802, Z_795, X1_803, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=V_792 | skf21(V_787, X_801, Y_786, Z_794, X1_799, U_209, V_210)=V_792 | skf21(V_789, X_788, Y_802, Z_795, X1_803, U_209, V_210)=V_792 | V_792=U_804 | skf10(U_209, V_210)=U_804 | skf21(V_787, X_801, Y_786, Z_794, X1_799, U_209, V_210)=U_804 | skf21(V_789, X_788, Y_802, Z_795, X1_803, U_209, V_210)=U_804 | ~member(V_210, V_792, U_209) | ~member(V_210, U_804, U_209) | skf21(U_804, V_792, W_800, X_785, Y_791, Z_793, X1_797)!=V_792 | Z_795=X1_803 | Z_795=Y_802 | Y_802=X1_803 | Y_802=X_788 | Z_795=X_788 | X_788=X1_803 | X_788=V_789 | Y_802=V_789 | Z_795=V_789 | X1_803=V_789 | ~member(V_210, X1_803, U_209) | ~member(V_210, Z_795, U_209) | ~member(V_210, Y_802, U_209) | ~member(V_210, X_788, U_209) | ~member(V_210, V_789, U_209) | Z_794=X1_799 | Z_794=Y_786 | Y_786=X1_799 | Y_786=X_801 | Z_794=X_801 | X_801=X1_799 | X_801=V_787 | Y_786=V_787 | Z_794=V_787 | X1_799=V_787 | five(V_210, U_209) | ~member(V_210, X1_799, U_209) | ~member(V_210, Z_794, U_209) | ~member(V_210, Y_786, U_209) | ~member(V_210, X_801, U_209) | ~member(V_210, V_787, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_996, plain, (![X1_648, X_639, U_178, X_181, Z_179, W_640, U_647, Z_643, Y_182, Y_645, Y_642, V_637, X1_180, W_177, V_635, V_183, Z_641, X_638, X1_649]: (skf21(V_635, X_638, Y_645, Z_641, X1_648, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_640 | skf21(V_635, X_638, Y_645, Z_641, X1_648, W_177, U_178)=W_640 | W_640=V_637 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_637 | skf21(V_635, X_638, Y_645, Z_641, X1_648, W_177, U_178)=V_637 | V_637=U_647 | W_640=U_647 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_647 | skf21(V_635, X_638, Y_645, Z_641, X1_648, W_177, U_178)=U_647 | ~member(U_178, W_640, W_177) | ~member(U_178, V_637, W_177) | ~member(U_178, U_647, W_177) | skf21(U_647, V_637, W_640, X_639, Y_642, Z_643, X1_649)!=W_640 | Z_641=X1_648 | Z_641=Y_645 | Y_645=X1_648 | Y_645=X_638 | Z_641=X_638 | X_638=X1_648 | X_638=V_635 | Y_645=V_635 | Z_641=V_635 | X1_648=V_635 | ~member(U_178, X1_648, W_177) | ~member(U_178, Z_641, W_177) | ~member(U_178, Y_645, W_177) | ~member(U_178, X_638, W_177) | ~member(U_178, V_635, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1021, plain, (![X1_659, X1_663, U_178, U_665, X_181, Z_179, Y_657, Z_655, Y_182, W_661, V_650, X4_656, V_662, Y_664, X1_180, W_177, V_183, X_653, X_660, Z_652]: (skf21(V_650, X_653, Y_657, Z_655, X1_663, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_656 | skf21(V_650, X_653, Y_657, Z_655, X1_663, W_177, U_178)=X4_656 | X4_656=V_662 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_662 | skf21(V_650, X_653, Y_657, Z_655, X1_663, W_177, U_178)=V_662 | V_662=U_665 | X4_656=U_665 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_665 | skf21(V_650, X_653, Y_657, Z_655, X1_663, W_177, U_178)=U_665 | ~member(U_178, X4_656, W_177) | ~member(U_178, V_662, W_177) | ~member(U_178, U_665, W_177) | skf21(U_665, V_662, W_661, X_660, Y_664, Z_652, X1_659)!=V_662 | Z_655=X1_663 | Z_655=Y_657 | Y_657=X1_663 | Y_657=X_653 | Z_655=X_653 | X_653=X1_663 | X_653=V_650 | Y_657=V_650 | Z_655=V_650 | X1_663=V_650 | ~member(U_178, X1_663, W_177) | ~member(U_178, Z_655, W_177) | ~member(U_178, Y_657, W_177) | ~member(U_178, X_653, W_177) | ~member(U_178, V_650, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_971, plain, (![X5_628, U_178, Y_624, X_181, U_619, Z_179, X4_630, X_633, X_622, Y_182, V_618, Y_625, W_634, X1_632, X1_621, X1_180, W_177, Z_627, V_183, V_631, Z_623]: (skf21(V_618, X_622, Y_625, Z_623, X1_632, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X5_628 | skf21(V_618, X_622, Y_625, Z_623, X1_632, W_177, U_178)=X5_628 | X5_628=X4_630 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_630 | skf21(V_618, X_622, Y_625, Z_623, X1_632, W_177, U_178)=X4_630 | X4_630=U_619 | X5_628=U_619 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_619 | skf21(V_618, X_622, Y_625, Z_623, X1_632, W_177, U_178)=U_619 | ~member(U_178, X5_628, W_177) | ~member(U_178, X4_630, W_177) | ~member(U_178, U_619, W_177) | skf21(U_619, V_631, W_634, X_633, Y_624, Z_627, X1_621)!=U_619 | Z_623=X1_632 | Z_623=Y_625 | Y_625=X1_632 | Y_625=X_622 | Z_623=X_622 | X_622=X1_632 | X_622=V_618 | Y_625=V_618 | Z_623=V_618 | X1_632=V_618 | ~member(U_178, X1_632, W_177) | ~member(U_178, Z_623, W_177) | ~member(U_178, Y_625, W_177) | ~member(U_178, X_622, W_177) | ~member(U_178, V_618, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_827, plain, (![X1_562, U_178, W_563, X_181, Z_179, Y_182, Z_560, X1_180, W_177, V_561, U_566, V_183, Y_565]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_563 | skf10(W_177, U_178)=W_563 | W_563=V_561 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_561 | skf10(W_177, U_178)=V_561 | V_561=U_566 | W_563=U_566 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_566 | skf10(W_177, U_178)=U_566 | ~member(U_178, W_563, W_177) | ~member(U_178, V_561, W_177) | ~member(U_178, U_566, W_177) | skf21(U_566, V_561, W_563, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_565, Z_560, X1_562)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_1049, plain, (![V_210, X_668, U_674, Y_673, X1_676, V_666, V_677, Z_671, Z_679, W_669, U_209, X1_678, Y_672]: (skf21(V_666, X_668, Y_673, Z_671, X1_676, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=W_669 | skf21(V_666, X_668, Y_673, Z_671, X1_676, U_209, V_210)=W_669 | W_669=V_677 | skf10(U_209, V_210)=V_677 | skf21(V_666, X_668, Y_673, Z_671, X1_676, U_209, V_210)=V_677 | V_677=U_674 | W_669=U_674 | skf10(U_209, V_210)=U_674 | skf21(V_666, X_668, Y_673, Z_671, X1_676, U_209, V_210)=U_674 | ~member(V_210, W_669, U_209) | ~member(V_210, V_677, U_209) | ~member(V_210, U_674, U_209) | skf21(U_674, V_677, W_669, skf10(U_209, V_210), Y_672, Z_679, X1_678)!=skf10(U_209, V_210) | Z_671=X1_676 | Z_671=Y_673 | Y_673=X1_676 | Y_673=X_668 | Z_671=X_668 | X_668=X1_676 | X_668=V_666 | Y_673=V_666 | Z_671=V_666 | X1_676=V_666 | five(V_210, U_209) | ~member(V_210, X1_676, U_209) | ~member(V_210, Z_671, U_209) | ~member(V_210, Y_673, U_209) | ~member(V_210, X_668, U_209) | ~member(V_210, V_666, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_934, plain, (![U_178, X_181, Z_179, V_600, Y_182, X4_594, X_593, X1_598, Y_601, U_595, X1_180, Z_596, W_177, V_183, W_597]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_594 | skf10(W_177, U_178)=X4_594 | X4_594=V_600 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_600 | skf10(W_177, U_178)=V_600 | V_600=U_595 | X4_594=U_595 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_595 | skf10(W_177, U_178)=U_595 | ~member(U_178, X4_594, W_177) | ~member(U_178, V_600, W_177) | ~member(U_178, U_595, W_177) | skf21(U_595, V_600, W_597, X_593, Y_601, Z_596, X1_598)!=V_600 | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_789, plain, (![X_542, Z_539, X1_172, V_537, X_174, Z_171, X1_541, U_170, U_538, W_168, V_176, Y_536, W_540]: (skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X_174 | X_174=W_168 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=W_168 | W_168=V_176 | X_174=V_176 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=V_176 | V_176=U_170 | W_168=U_170 | X_174=U_170 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=U_170 | ~member(U_538, X_174, W_540) | ~member(U_538, W_168, W_540) | ~member(U_538, V_176, W_540) | ~member(U_538, U_170, W_540) | skf21(U_170, V_176, W_168, X_174, skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538), Z_171, X1_172)!=skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538) | Z_539=X1_541 | Z_539=Y_536 | Y_536=X1_541 | Y_536=X_542 | Z_539=X_542 | X_542=X1_541 | X_542=V_537 | Y_536=V_537 | Z_539=V_537 | X1_541=V_537 | five(U_538, W_540) | ~member(U_538, X1_541, W_540) | ~member(U_538, Z_539, W_540) | ~member(U_538, Y_536, W_540) | ~member(U_538, X_542, W_540) | ~member(U_538, V_537, W_540)))). % 21.89/13.43 tff(c_908, plain, (![U_178, W_585, X_181, Z_179, X1_584, V_586, X_587, X5_588, Z_582, Y_182, Y_589, X1_180, W_177, V_183, X4_579, U_580]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X5_588 | skf10(W_177, U_178)=X5_588 | X5_588=X4_579 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_579 | skf10(W_177, U_178)=X4_579 | X4_579=U_580 | X5_588=U_580 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_580 | skf10(W_177, U_178)=U_580 | ~member(U_178, X5_588, W_177) | ~member(U_178, X4_579, W_177) | ~member(U_178, U_580, W_177) | skf21(U_580, V_586, W_585, X_587, Y_589, Z_582, X1_584)!=U_580 | ssSkP0(W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.43 tff(c_999, plain, (![X1_648, X_639, V_210, W_640, U_647, Z_643, Y_645, Y_642, V_637, V_635, Z_641, U_209, X_638, X1_649]: (skf21(V_635, X_638, Y_645, Z_641, X1_648, U_209, V_210)=skf10(U_209, V_210) | skf10(U_209, V_210)=W_640 | skf21(V_635, X_638, Y_645, Z_641, X1_648, U_209, V_210)=W_640 | W_640=V_637 | skf10(U_209, V_210)=V_637 | skf21(V_635, X_638, Y_645, Z_641, X1_648, U_209, V_210)=V_637 | V_637=U_647 | W_640=U_647 | skf10(U_209, V_210)=U_647 | skf21(V_635, X_638, Y_645, Z_641, X1_648, U_209, V_210)=U_647 | ~member(V_210, W_640, U_209) | ~member(V_210, V_637, U_209) | ~member(V_210, U_647, U_209) | skf21(U_647, V_637, W_640, X_639, Y_642, Z_643, X1_649)!=W_640 | Z_641=X1_648 | Z_641=Y_645 | Y_645=X1_648 | Y_645=X_638 | Z_641=X_638 | X_638=X1_648 | X_638=V_635 | Y_645=V_635 | Z_641=V_635 | X1_648=V_635 | five(V_210, U_209) | ~member(V_210, X1_648, U_209) | ~member(V_210, Z_641, U_209) | ~member(V_210, Y_645, U_209) | ~member(V_210, X_638, U_209) | ~member(V_210, V_635, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.43 tff(c_788, plain, (![X_542, Z_539, Z_161, V_537, X1_162, W_158, X1_541, U_538, U_160, Y_536, V_166, X_164, W_540, Y_165]: (skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X_164 | X_164=W_158 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=W_158 | W_158=V_166 | X_164=V_166 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=V_166 | V_166=U_160 | W_158=U_160 | X_164=U_160 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=U_160 | ~member(U_538, X_164, W_540) | ~member(U_538, W_158, W_540) | ~member(U_538, V_166, W_540) | ~member(U_538, U_160, W_540) | skf21(U_160, V_166, W_158, X_164, Y_165, Z_161, X1_162)!=X_164 | Z_539=X1_541 | Z_539=Y_536 | Y_536=X1_541 | Y_536=X_542 | Z_539=X_542 | X_542=X1_541 | X_542=V_537 | Y_536=V_537 | Z_539=V_537 | X1_541=V_537 | five(U_538, W_540) | ~member(U_538, X1_541, W_540) | ~member(U_538, Z_539, W_540) | ~member(U_538, Y_536, W_540) | ~member(U_538, X_542, W_540) | ~member(U_538, V_537, W_540)))). % 21.89/13.43 tff(c_787, plain, (![X_542, W_199, Z_539, Z_202, X4_208, V_537, X5_197, X_205, X1_541, V_207, U_538, U_201, Y_536, X1_203, Y_206, W_540]: (skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X5_197 | X5_197=X4_208 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X4_208 | X4_208=V_207 | X5_197=V_207 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=V_207 | V_207=U_201 | X4_208=U_201 | X5_197=U_201 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=U_201 | ~member(U_538, X5_197, W_540) | ~member(U_538, X4_208, W_540) | ~member(U_538, V_207, W_540) | ~member(U_538, U_201, W_540) | skf21(U_201, V_207, W_199, X_205, Y_206, Z_202, X1_203)!=V_207 | Z_539=X1_541 | Z_539=Y_536 | Y_536=X1_541 | Y_536=X_542 | Z_539=X_542 | X_542=X1_541 | X_542=V_537 | Y_536=V_537 | Z_539=V_537 | X1_541=V_537 | five(U_538, W_540) | ~member(U_538, X1_541, W_540) | ~member(U_538, Z_539, W_540) | ~member(U_538, Y_536, W_540) | ~member(U_538, X_542, W_540) | ~member(U_538, V_537, W_540)))). % 21.89/13.43 tff(c_786, plain, (![X_542, Z_539, W_148, V_537, V_156, X1_541, Y_155, X1_152, U_538, X_154, Y_536, Z_151, W_540, U_150, X4_157]: (skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X4_157 | X4_157=W_148 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=W_148 | W_148=V_156 | X4_157=V_156 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=V_156 | V_156=U_150 | W_148=U_150 | X4_157=U_150 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=U_150 | ~member(U_538, X4_157, W_540) | ~member(U_538, W_148, W_540) | ~member(U_538, V_156, W_540) | ~member(U_538, U_150, W_540) | skf21(U_150, V_156, W_148, X_154, Y_155, Z_151, X1_152)!=W_148 | Z_539=X1_541 | Z_539=Y_536 | Y_536=X1_541 | Y_536=X_542 | Z_539=X_542 | X_542=X1_541 | X_542=V_537 | Y_536=V_537 | Z_539=V_537 | X1_541=V_537 | five(U_538, W_540) | ~member(U_538, X1_541, W_540) | ~member(U_538, Z_539, W_540) | ~member(U_538, Y_536, W_540) | ~member(U_538, X_542, W_540) | ~member(U_538, V_537, W_540)))). % 21.89/13.44 tff(c_790, plain, (![X_542, Z_539, V_195, V_537, X6_185, U_188, X4_196, X5_184, X1_541, Z_189, U_538, X1_191, Y_194, Y_536, W_540, W_186, X_193]: (skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X6_185 | X6_185=X5_184 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X5_184 | X5_184=X4_196 | X6_185=X4_196 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=X4_196 | X4_196=U_188 | X5_184=U_188 | X6_185=U_188 | skf21(V_537, X_542, Y_536, Z_539, X1_541, W_540, U_538)=U_188 | ~member(U_538, X6_185, W_540) | ~member(U_538, X5_184, W_540) | ~member(U_538, X4_196, W_540) | ~member(U_538, U_188, W_540) | skf21(U_188, V_195, W_186, X_193, Y_194, Z_189, X1_191)!=U_188 | Z_539=X1_541 | Z_539=Y_536 | Y_536=X1_541 | Y_536=X_542 | Z_539=X_542 | X_542=X1_541 | X_542=V_537 | Y_536=V_537 | Z_539=V_537 | X1_541=V_537 | five(U_538, W_540) | ~member(U_538, X1_541, W_540) | ~member(U_538, Z_539, W_540) | ~member(U_538, Y_536, W_540) | ~member(U_538, X_542, W_540) | ~member(U_538, V_537, W_540)))). % 21.89/13.44 tff(c_795, plain, (![Y_546, V_210, V_544, W_549, Z_548, U_209, X_547]: (~actual_world(V_210) | ~nonhuman(V_210, U_209) | ~group(V_210, U_209) | ~dollar(V_210, skf8(V_210, Z_548)) | ~shake_beverage(V_210, Y_546) | ~patient(V_210, W_549, Y_546) | ~order(V_210, W_549) | ~nonreflexive(V_210, W_549) | ~past(V_210, W_549) | ~event(V_210, W_549) | ~of(V_210, V_544, X_547) | ~woman(V_210, X_547) | ~agent(V_210, W_549, X_547) | ~forename(V_210, V_544) | ~mia_forename(V_210, V_544) | skf20(U_209, V_210)=skf10(U_209, V_210) | skf18(U_209, V_210)=skf10(U_209, V_210) | skf16(U_209, V_210)=skf10(U_209, V_210) | skf14(U_209, V_210)=skf10(U_209, V_210) | skf12(U_209, V_210)=skf10(U_209, V_210) | ~five(V_210, U_209)))). % 21.89/13.44 tff(c_863, plain, (![U_209]: (skf8(skc5, U_209)=skf20(U_209, skc5) | skf8(skc5, U_209)=skf18(U_209, skc5) | skf8(skc5, U_209)=skf16(U_209, skc5) | skf8(skc5, U_209)=skf14(U_209, skc5) | skf8(skc5, U_209)=skf12(U_209, skc5) | ~nonhuman(skc5, U_209) | ~group(skc5, U_209) | skf20(U_209, skc5)=skf10(U_209, skc5) | skf18(U_209, skc5)=skf10(U_209, skc5) | skf16(U_209, skc5)=skf10(U_209, skc5) | skf14(U_209, skc5)=skf10(U_209, skc5) | skf12(U_209, skc5)=skf10(U_209, skc5) | ~five(skc5, U_209)))). % 21.89/13.44 tff(c_711, plain, (![V_210, Z_496, U_495, X1_494, W_500, X_501, V_502, U_209]: (skf10(U_209, V_210)=X_501 | X_501=W_500 | skf10(U_209, V_210)=W_500 | W_500=V_502 | X_501=V_502 | skf10(U_209, V_210)=V_502 | V_502=U_495 | W_500=U_495 | X_501=U_495 | skf10(U_209, V_210)=U_495 | five(V_210, U_209) | ~member(V_210, X_501, U_209) | ~member(V_210, W_500, U_209) | ~member(V_210, V_502, U_209) | ~member(V_210, U_495, U_209) | skf21(U_495, V_502, W_500, X_501, skf10(U_209, V_210), Z_496, X1_494)!=skf10(U_209, V_210) | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_749, plain, (![X5_514, Z_513, V_210, V_522, W_520, U_524, X4_515, X1_517, Y_523, U_209, X_519]: (skf10(U_209, V_210)=X5_514 | X5_514=X4_515 | skf10(U_209, V_210)=X4_515 | X4_515=V_522 | X5_514=V_522 | skf10(U_209, V_210)=V_522 | V_522=U_524 | X4_515=U_524 | X5_514=U_524 | skf10(U_209, V_210)=U_524 | five(V_210, U_209) | ~member(V_210, X5_514, U_209) | ~member(V_210, X4_515, U_209) | ~member(V_210, V_522, U_209) | ~member(V_210, U_524, U_209) | skf21(U_524, V_522, W_520, X_519, Y_523, Z_513, X1_517)!=V_522 | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_692, plain, (![Y_485, X6_489, V_210, U_481, V_491, X_492, Z_487, X1_482, U_209, W_493, X5_488, X4_490]: (skf10(U_209, V_210)=X6_489 | X6_489=X5_488 | skf10(U_209, V_210)=X5_488 | X5_488=X4_490 | X6_489=X4_490 | skf10(U_209, V_210)=X4_490 | X4_490=U_481 | X5_488=U_481 | X6_489=U_481 | skf10(U_209, V_210)=U_481 | five(V_210, U_209) | ~member(V_210, X6_489, U_209) | ~member(V_210, X5_488, U_209) | ~member(V_210, X4_490, U_209) | ~member(V_210, U_481, U_209) | skf21(U_481, V_491, W_493, X_492, Y_485, Z_487, X1_482)!=U_481 | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_768, plain, (![V_210, Y_530, V_525, X1_534, X_528, Z_531, X4_532, U_533, W_529, U_209]: (skf10(U_209, V_210)=X4_532 | X4_532=W_529 | skf10(U_209, V_210)=W_529 | W_529=V_525 | X4_532=V_525 | skf10(U_209, V_210)=V_525 | V_525=U_533 | W_529=U_533 | X4_532=U_533 | skf10(U_209, V_210)=U_533 | five(V_210, U_209) | ~member(V_210, X4_532, U_209) | ~member(V_210, W_529, U_209) | ~member(V_210, V_525, U_209) | ~member(V_210, U_533, U_209) | skf21(U_533, V_525, W_529, X_528, Y_530, Z_531, X1_534)!=W_529 | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_857, plain, (![Z_567]: (skf8(skc5, Z_567)=skf20(Z_567, skc5) | skf8(skc5, Z_567)=skf18(Z_567, skc5) | skf8(skc5, Z_567)=skf16(Z_567, skc5) | skf8(skc5, Z_567)=skf14(Z_567, skc5) | skf8(skc5, Z_567)=skf12(Z_567, skc5) | ~nonhuman(skc5, Z_567) | ~ssSkP0(Z_567, skc5) | ~five(skc5, Z_567) | ~group(skc5, Z_567)))). % 21.89/13.44 tff(c_811, plain, (![Z_552]: (member(skc5, skf8(skc5, Z_552), Z_552) | ~nonhuman(skc5, Z_552) | ~ssSkP0(Z_552, skc5) | ~five(skc5, Z_552) | ~group(skc5, Z_552)))). % 21.89/13.44 tff(c_730, plain, (![U_509, X1_511, Y_508, V_210, V_510, W_505, Z_512, X_507, U_209]: (skf10(U_209, V_210)=X_507 | X_507=W_505 | skf10(U_209, V_210)=W_505 | W_505=V_510 | X_507=V_510 | skf10(U_209, V_210)=V_510 | V_510=U_509 | W_505=U_509 | X_507=U_509 | skf10(U_209, V_210)=U_509 | five(V_210, U_209) | ~member(V_210, X_507, U_209) | ~member(V_210, W_505, U_209) | ~member(V_210, V_510, U_209) | ~member(V_210, U_509, U_209) | skf21(U_509, V_510, W_505, X_507, Y_508, Z_512, X1_511)!=X_507 | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_184, plain, (![V_219, X_217, Y_218, U_215, Z_216, W_214]: (member(U_215, skf8(U_215, Z_216), Z_216) | ~actual_world(U_215) | ~nonhuman(U_215, Z_216) | ~ssSkP0(Z_216, U_215) | ~five(U_215, Z_216) | ~group(U_215, Z_216) | ~shake_beverage(U_215, Y_218) | ~patient(U_215, W_214, Y_218) | ~order(U_215, W_214) | ~nonreflexive(U_215, W_214) | ~past(U_215, W_214) | ~event(U_215, W_214) | ~of(U_215, V_219, X_217) | ~woman(U_215, X_217) | ~agent(U_215, W_214, X_217) | ~forename(U_215, V_219) | ~mia_forename(U_215, V_219)))). % 21.89/13.44 tff(c_186, plain, (![X1_223, U_221, Y_225, Z_222, X_224, W_220, V_226]: (~actual_world(U_221) | ~nonhuman(U_221, X1_223) | ~ssSkP0(X1_223, U_221) | ~five(U_221, X1_223) | ~group(U_221, X1_223) | ~dollar(U_221, skf8(U_221, Z_222)) | ~shake_beverage(U_221, Y_225) | ~patient(U_221, W_220, Y_225) | ~order(U_221, W_220) | ~nonreflexive(U_221, W_220) | ~past(U_221, W_220) | ~event(U_221, W_220) | ~of(U_221, V_226, X_224) | ~woman(U_221, X_224) | ~agent(U_221, W_220, X_224) | ~forename(U_221, V_226) | ~mia_forename(U_221, V_226)))). % 21.89/13.44 tff(c_150, plain, (![U_178, X_181, Z_179, Y_182, X1_180, W_177, V_183]: (Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | member(U_178, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_177) | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 21.89/13.44 tff(c_144, plain, (![X3_149, W_148, V_156, X5_147, Y_155, X1_152, X2_153, X_154, Z_151, U_150, X4_157]: (X5_147=X4_157 | X4_157=W_148 | X5_147=W_148 | W_148=V_156 | X4_157=V_156 | X5_147=V_156 | V_156=U_150 | W_148=U_150 | X4_157=U_150 | X5_147=U_150 | five(X2_153, X3_149) | ~member(X2_153, X5_147, X3_149) | ~member(X2_153, X4_157, X3_149) | ~member(X2_153, W_148, X3_149) | ~member(X2_153, V_156, X3_149) | ~member(X2_153, U_150, X3_149) | skf21(U_150, V_156, W_148, X_154, Y_155, Z_151, X1_152)!=W_148))). % 21.89/13.44 tff(c_154, plain, (![W_199, Z_202, X4_208, X5_197, X_205, X6_198, V_207, U_201, X2_204, X3_200, X1_203, Y_206]: (X6_198=X5_197 | X5_197=X4_208 | X6_198=X4_208 | X4_208=V_207 | X5_197=V_207 | X6_198=V_207 | V_207=U_201 | X4_208=U_201 | X5_197=U_201 | X6_198=U_201 | five(X2_204, X3_200) | ~member(X2_204, X6_198, X3_200) | ~member(X2_204, X5_197, X3_200) | ~member(X2_204, X4_208, X3_200) | ~member(X2_204, V_207, X3_200) | ~member(X2_204, U_201, X3_200) | skf21(U_201, V_207, W_199, X_205, Y_206, Z_202, X1_203)!=V_207))). % 21.89/13.44 tff(c_146, plain, (![Z_161, X3_159, X1_162, X4_167, X2_163, W_158, U_160, V_166, X_164, Y_165]: (X_164=X4_167 | X_164=W_158 | X4_167=W_158 | W_158=V_166 | X_164=V_166 | X4_167=V_166 | V_166=U_160 | W_158=U_160 | X_164=U_160 | X4_167=U_160 | five(X2_163, X3_159) | ~member(X2_163, X4_167, X3_159) | ~member(X2_163, X_164, X3_159) | ~member(X2_163, W_158, X3_159) | ~member(X2_163, V_166, X3_159) | ~member(X2_163, U_160, X3_159) | skf21(U_160, V_166, W_158, X_164, Y_165, Z_161, X1_162)!=X_164))). % 21.89/13.44 tff(c_148, plain, (![Y_175, X3_169, X1_172, X_174, X2_173, Z_171, U_170, W_168, V_176]: (Y_175=X_174 | X_174=W_168 | Y_175=W_168 | W_168=V_176 | X_174=V_176 | Y_175=V_176 | V_176=U_170 | W_168=U_170 | X_174=U_170 | Y_175=U_170 | five(X2_173, X3_169) | ~member(X2_173, Y_175, X3_169) | ~member(X2_173, X_174, X3_169) | ~member(X2_173, W_168, X3_169) | ~member(X2_173, V_176, X3_169) | ~member(X2_173, U_170, X3_169) | skf21(U_170, V_176, W_168, X_174, Y_175, Z_171, X1_172)!=Y_175))). % 21.89/13.44 tff(c_152, plain, (![V_195, X6_185, U_188, X7_190, X4_196, X5_184, X3_187, Z_189, X1_191, Y_194, W_186, X_193, X2_192]: (X7_190=X6_185 | X6_185=X5_184 | X7_190=X5_184 | X5_184=X4_196 | X6_185=X4_196 | X7_190=X4_196 | X4_196=U_188 | X5_184=U_188 | X6_185=U_188 | X7_190=U_188 | five(X2_192, X3_187) | ~member(X2_192, X7_190, X3_187) | ~member(X2_192, X6_185, X3_187) | ~member(X2_192, X5_184, X3_187) | ~member(X2_192, X4_196, X3_187) | ~member(X2_192, U_188, X3_187) | skf21(U_188, V_195, W_186, X_193, Y_194, Z_189, X1_191)!=U_188))). % 21.89/13.44 tff(c_669, plain, (![U_209, V_210]: (skf20(U_209, V_210)=skf10(U_209, V_210) | skf18(U_209, V_210)=skf10(U_209, V_210) | skf16(U_209, V_210)=skf10(U_209, V_210) | skf14(U_209, V_210)=skf10(U_209, V_210) | skf12(U_209, V_210)=skf10(U_209, V_210) | ~five(V_210, U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_142, plain, (![W_146, U_144, V_145]: (skf20(W_146, U_144)=V_145 | skf18(W_146, U_144)=V_145 | skf16(W_146, U_144)=V_145 | skf14(W_146, U_144)=V_145 | skf12(W_146, U_144)=V_145 | ~five(U_144, W_146) | ~member(U_144, V_145, W_146)))). % 21.89/13.44 tff(c_636, plain, (![W_468]: (skc8=W_468 | ~forename(skc5, W_468) | ~of(skc5, W_468, skc9)))). % 21.89/13.44 tff(c_182, plain, (![U_211, V_212, W_213]: (~event(U_211, V_212) | ~agent(U_211, V_212, W_213) | ~patient(U_211, V_212, skf10(W_213, U_211)) | ~present(U_211, V_212) | ~nonreflexive(U_211, V_212) | ~cost(U_211, V_212)))). % 21.89/13.44 tff(c_140, plain, (![W_142, V_141, U_140, X_143]: (W_142=V_141 | ~entity(U_140, X_143) | ~of(U_140, V_141, X_143) | ~forename(U_140, W_142) | ~of(U_140, W_142, X_143) | ~forename(U_140, V_141)))). % 21.89/13.44 tff(c_630, plain, (~agent(skc5, skc6, skc7))). % 21.89/13.44 tff(c_138, plain, (![U_137, V_138, W_139]: (~agent(U_137, V_138, W_139) | ~patient(U_137, V_138, W_139) | ~nonreflexive(U_137, V_138)))). % 21.89/13.44 tff(c_623, plain, (~act(skc5, skc7))). % 21.89/13.44 tff(c_615, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 21.89/13.44 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf18(U_127, V_128)!=skf14(U_127, V_128)))). % 21.89/13.44 tff(c_591, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 21.89/13.44 tff(c_515, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 21.89/13.44 tff(c_602, plain, (~food(skc5, skc9))). % 21.89/13.44 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf16(U_131, V_132)!=skf12(U_131, V_132)))). % 21.89/13.44 tff(c_537, plain, (![U_77, V_78]: (~food(U_77, V_78) | ~human_person(U_77, V_78)))). % 21.89/13.44 tff(c_597, plain, (~abstraction(skc5, skc7))). % 21.89/13.44 tff(c_532, plain, (![U_417, V_418]: (~abstraction(U_417, V_418) | ~beverage(U_417, V_418)))). % 21.89/13.44 tff(c_516, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 21.89/13.44 tff(c_504, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 21.89/13.44 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf14(U_135, V_136)!=skf12(U_135, V_136)))). % 21.89/13.44 tff(c_581, plain, (~animate(skc5, skc7))). % 21.89/13.44 tff(c_562, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 21.89/13.44 tff(c_556, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 21.89/13.44 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf20(U_119, V_120)!=skf14(U_119, V_120)))). % 21.89/13.44 tff(c_549, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 21.89/13.44 tff(c_567, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 21.89/13.44 tff(c_550, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 21.89/13.44 tff(c_486, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 21.89/13.44 tff(c_464, plain, (![U_385, V_386]: (~animate(U_385, V_386) | ~food(U_385, V_386)))). % 21.89/13.44 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf18(U_129, V_130)!=skf16(U_129, V_130)))). % 21.89/13.44 tff(c_498, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 21.89/13.44 tff(c_551, plain, (~abstraction(skc5, skc6))). % 21.89/13.44 tff(c_469, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 21.89/13.44 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf18(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 21.89/13.44 tff(c_463, plain, (![U_385, V_386]: (~living(U_385, V_386) | ~food(U_385, V_386)))). % 21.89/13.44 tff(c_531, plain, (~beverage(skc5, skc6))). % 21.89/13.44 tff(c_455, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 21.89/13.44 tff(c_523, plain, (~beverage(skc5, skc9))). % 21.89/13.44 tff(c_450, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 21.89/13.44 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf16(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 21.89/13.44 tff(c_517, plain, (~entity(skc5, skc6))). % 21.89/13.44 tff(c_492, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 21.89/13.44 tff(c_445, plain, (![U_21, V_22]: (~abstraction(U_21, V_22) | ~group(U_21, V_22)))). % 21.89/13.44 tff(c_180, plain, (![V_210, U_209]: (member(V_210, skf10(U_209, V_210), U_209) | ssSkP0(U_209, V_210)))). % 21.89/13.44 tff(c_403, plain, (![U_367, V_368]: (~multiple(U_367, V_368) | ~eventuality(U_367, V_368)))). % 21.89/13.44 tff(c_420, plain, (![U_369, V_370]: (impartial(U_369, V_370) | ~food(U_369, V_370)))). % 21.89/13.44 tff(c_375, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 21.89/13.44 tff(c_381, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 21.89/13.44 tff(c_353, plain, (![U_339, V_340]: (~multiple(U_339, V_340) | ~entity(U_339, V_340)))). % 21.89/13.44 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf16(U_133, V_134)!=skf14(U_133, V_134)))). % 21.89/13.44 tff(c_347, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 21.89/13.44 tff(c_475, plain, (abstraction(skc5, skc8))). % 21.89/13.44 tff(c_359, plain, (![U_343, V_344]: (abstraction(U_343, V_344) | ~forename(U_343, V_344)))). % 21.89/13.44 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf20(U_117, V_118)!=skf12(U_117, V_118)))). % 21.89/13.44 tff(c_387, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 21.89/13.44 tff(c_419, plain, (![U_369, V_370]: (nonliving(U_369, V_370) | ~food(U_369, V_370)))). % 21.89/13.44 tff(c_418, plain, (![U_369, V_370]: (entity(U_369, V_370) | ~food(U_369, V_370)))). % 21.89/13.44 tff(c_417, plain, (![U_369, V_370]: (~female(U_369, V_370) | ~food(U_369, V_370)))). % 21.89/13.44 tff(c_392, plain, (![U_361, V_362]: (~multiple(U_361, V_362) | ~abstraction(U_361, V_362)))). % 21.89/13.44 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf20(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 21.89/13.45 tff(c_248, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 21.89/13.45 tff(c_437, plain, (~cost(skc5, skc9))). % 21.89/13.45 tff(c_436, plain, (~act(skc5, skc9))). % 21.89/13.45 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf18(U_125, V_126)!=skf12(U_125, V_126)))). % 21.89/13.45 tff(c_429, plain, (~event(skc5, skc9))). % 21.89/13.45 tff(c_425, plain, (~eventuality(skc5, skc9))). % 21.89/13.45 tff(c_319, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 21.89/13.45 tff(c_258, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 21.89/13.45 tff(c_240, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 21.89/13.45 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf20(U_123, V_124)!=skf18(U_123, V_124)))). % 21.89/13.45 tff(c_341, plain, (![U_331, V_332]: (~female(U_331, V_332) | ~abstraction(U_331, V_332)))). % 21.89/13.45 tff(c_294, plain, (![U_309, V_310]: (singleton(U_309, V_310) | ~abstraction(U_309, V_310)))). % 21.89/13.45 tff(c_329, plain, (![U_33, V_34]: (~general(U_33, V_34) | ~eventuality(U_33, V_34)))). % 21.89/13.45 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf14(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 21.89/13.45 tff(c_304, plain, (![U_313, V_314]: (abstraction(U_313, V_314) | ~currency(U_313, V_314)))). % 21.89/13.45 tff(c_320, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 21.89/13.45 tff(c_274, plain, (![U_293, V_294]: (~existent(U_293, V_294) | ~eventuality(U_293, V_294)))). % 21.89/13.45 tff(c_370, plain, (entity(skc5, skc9))). % 21.89/13.45 tff(c_253, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 21.89/13.45 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf20(U_121, V_122)!=skf16(U_121, V_122)))). % 21.89/13.45 tff(c_364, plain, (~abstraction(skc5, skc9))). % 21.89/13.45 tff(c_309, plain, (![U_315, V_316]: (~human(U_315, V_316) | ~abstraction(U_315, V_316)))). % 21.89/13.45 tff(c_206, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 21.89/13.45 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf12(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 21.89/13.45 tff(c_289, plain, (![U_307, V_308]: (singleton(U_307, V_308) | ~entity(U_307, V_308)))). % 21.89/13.45 tff(c_234, plain, (![U_77, V_78]: (living(U_77, V_78) | ~human_person(U_77, V_78)))). % 21.89/13.45 tff(c_328, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 21.89/13.45 tff(c_268, plain, (![U_77, V_78]: (impartial(U_77, V_78) | ~human_person(U_77, V_78)))). % 21.89/13.45 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 21.89/13.45 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 21.89/13.45 tff(c_335, plain, (human(skc5, skc9))). % 21.89/13.45 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 21.89/13.45 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 21.89/13.45 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 21.89/13.45 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 21.89/13.45 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 21.89/13.45 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 21.89/13.45 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 21.89/13.45 tff(c_299, plain, (female(skc5, skc9))). % 21.89/13.45 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 21.89/13.45 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 22.19/13.45 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 22.19/13.45 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 22.19/13.45 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 22.19/13.45 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 22.19/13.45 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 22.19/13.45 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 22.19/13.45 tff(c_280, plain, (animate(skc5, skc9))). % 22.19/13.45 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 22.19/13.45 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 22.19/13.45 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 22.19/13.45 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 22.19/13.45 tff(c_263, plain, (human_person(skc5, skc9))). % 22.19/13.45 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 22.19/13.45 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 22.19/13.45 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 22.19/13.45 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 22.19/13.45 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 22.19/13.45 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 22.19/13.45 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 22.19/13.45 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 22.19/13.45 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 22.19/13.45 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 22.19/13.45 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 22.19/13.45 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 22.19/13.45 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 22.19/13.45 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 22.19/13.45 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 22.19/13.45 tff(c_219, plain, (act(skc5, skc6))). % 22.19/13.45 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 22.19/13.45 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 22.19/13.45 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 22.19/13.45 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 22.19/13.45 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 22.19/13.45 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 22.19/13.45 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 22.19/13.45 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 22.19/13.45 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 22.19/13.45 tff(c_198, plain, (beverage(skc5, skc7))). % 22.19/13.45 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 22.19/13.45 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 22.19/13.45 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 22.19/13.45 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 22.19/13.45 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 22.19/13.45 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 22.19/13.45 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 22.19/13.45 tff(c_176, plain, (agent(skc5, skc6, skc9))). % 22.19/13.45 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 22.19/13.45 tff(c_178, plain, (patient(skc5, skc6, skc7))). % 22.19/13.45 tff(c_174, plain, (of(skc5, skc8, skc9))). % 22.19/13.45 tff(c_162, plain, (order(skc5, skc6))). % 22.19/13.45 tff(c_160, plain, (shake_beverage(skc5, skc7))). % 22.19/13.45 tff(c_158, plain, (woman(skc5, skc9))). % 22.19/13.45 tff(c_164, plain, (nonreflexive(skc5, skc6))). % 22.19/13.45 tff(c_166, plain, (past(skc5, skc6))). % 22.19/13.45 tff(c_168, plain, (event(skc5, skc6))). % 22.19/13.45 tff(c_170, plain, (forename(skc5, skc8))). % 22.19/13.45 tff(c_172, plain, (mia_forename(skc5, skc8))). % 22.19/13.46 tff(c_156, plain, (actual_world(skc5))). % 22.19/13.46 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.19/13.46 %------------------------------------------------------------------------------