%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP076-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:07 PM UTC 2025 % Result : Satisfiable 71.29s 61.30s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP076-1 : TPTP v9.0.0. Released v2.4.0. % 0.08/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.14/0.34 % Computer : n008.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 08:23:32 EDT 2025 % 0.14/0.34 % CPUTime : % 71.29/61.30 % 71.29/61.30 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 71.29/61.30 % 71.29/61.30 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 71.29/61.31 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf21 > skf8 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc3 > skc2 % 71.29/61.31 % 71.29/61.31 %Foreground sorts: % 71.29/61.31 % 71.29/61.31 % 71.29/61.31 %Background operators: % 71.29/61.31 % 71.29/61.31 % 71.29/61.31 %Foreground operators: % 71.29/61.31 tff(nonliving, type, nonliving: ($i * $i) > $o). % 71.29/61.31 tff(skf10, type, skf10: ($i * $i) > $i). % 71.29/61.31 tff(member, type, member: ($i * $i * $i) > $o). % 71.29/61.31 tff(living, type, living: ($i * $i) > $o). % 71.29/61.31 tff(fire, type, fire: ($i * $i) > $o). % 71.29/61.31 tff(human_person, type, human_person: ($i * $i) > $o). % 71.29/61.31 tff(action, type, action: ($i * $i) > $o). % 71.29/61.31 tff(present, type, present: ($i * $i) > $o). % 71.29/61.31 tff(shot, type, shot: ($i * $i) > $o). % 71.29/61.31 tff(entity, type, entity: ($i * $i) > $o). % 71.29/61.31 tff(eventuality, type, eventuality: ($i * $i) > $o). % 71.29/61.31 tff(weapon, type, weapon: ($i * $i) > $o). % 71.29/61.31 tff(existent, type, existent: ($i * $i) > $o). % 71.29/61.31 tff(singleton, type, singleton: ($i * $i) > $o). % 71.29/61.31 tff(male, type, male: ($i * $i) > $o). % 71.29/61.31 tff(multiple, type, multiple: ($i * $i) > $o). % 71.29/61.31 tff(organism, type, organism: ($i * $i) > $o). % 71.29/61.31 tff(animate, type, animate: ($i * $i) > $o). % 71.29/61.31 tff(of, type, of: ($i * $i * $i) > $o). % 71.29/61.31 tff(skf14, type, skf14: ($i * $i) > $i). % 71.29/61.31 tff(actual_world, type, actual_world: $i > $o). % 71.29/61.31 tff(agent, type, agent: ($i * $i * $i) > $o). % 71.29/61.31 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 71.29/61.31 tff(group, type, group: ($i * $i) > $o). % 71.29/61.31 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 71.29/61.31 tff(artifact, type, artifact: ($i * $i) > $o). % 71.29/61.31 tff(cannon, type, cannon: ($i * $i) > $o). % 71.29/61.31 tff(event, type, event: ($i * $i) > $o). % 71.29/61.31 tff(skc2, type, skc2: $i). % 71.29/61.31 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 71.29/61.31 tff(patient, type, patient: ($i * $i * $i) > $o). % 71.29/61.31 tff(skf8, type, skf8: ($i * $i) > $i). % 71.29/61.31 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 71.29/61.31 tff(skc3, type, skc3: $i). % 71.29/61.31 tff(thing, type, thing: ($i * $i) > $o). % 71.29/61.31 tff(human, type, human: ($i * $i) > $o). % 71.29/61.31 tff(six, type, six: ($i * $i) > $o). % 71.29/61.31 tff(skf18, type, skf18: ($i * $i) > $i). % 71.29/61.31 tff(man, type, man: ($i * $i) > $o). % 71.29/61.31 tff(weaponry, type, weaponry: ($i * $i) > $o). % 71.29/61.31 tff(unisex, type, unisex: ($i * $i) > $o). % 71.29/61.31 tff(skf16, type, skf16: ($i * $i) > $i). % 71.29/61.31 tff(set, type, set: ($i * $i) > $o). % 71.29/61.31 tff(skf12, type, skf12: ($i * $i) > $i). % 71.29/61.31 tff(impartial, type, impartial: ($i * $i) > $o). % 71.29/61.31 tff(object, type, object: ($i * $i) > $o). % 71.29/61.31 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 71.29/61.31 tff(specific, type, specific: ($i * $i) > $o). % 71.29/61.31 tff(skf20, type, skf20: ($i * $i) > $i). % 71.29/61.31 tff(act, type, act: ($i * $i) > $o). % 71.29/61.31 % 71.29/61.31 %Saturated clause set: % 71.29/61.31 tff(c_1046, plain, (![X_974, Y_936, X2_955, Y_960, X_970, Z_194, V_199, X1_952, X2_939, X2_196, X1_967, Z_969, X_956, X1_941, X_945, V_940, V_946, V_966, X2_964, W_949, V_944, X1_973, X_961, X2_942, W_192, X1_195, Y_938, Z_971, V_954, X1_968, Y_962, X2_965, X_197, Y_198, Z_959, U_193, X2_937, Z_963, X_958, Z_950, Z_935, X1_947, Y_972, V_948, Y_957]: (skf21(V_948, X_945, Y_960, Z_959, X1_947, X2_964, W_192, U_193)=skf21(V_946, X_961, Y_936, Z_969, X1_968, X2_942, W_192, U_193) | skf21(V_948, X_945, Y_960, Z_959, X1_947, X2_964, W_192, U_193)=skf21(V_940, X_956, Y_962, Z_935, X1_952, X2_965, W_192, U_193) | skf21(V_946, X_961, Y_936, Z_969, X1_968, X2_942, W_192, U_193)=skf21(V_940, X_956, Y_962, Z_935, X1_952, X2_965, W_192, U_193) | skf21(V_944, X_970, Y_972, Z_971, X1_973, X2_955, W_192, U_193)=skf21(V_940, X_956, Y_962, Z_935, X1_952, X2_965, W_192, U_193) | skf21(V_948, X_945, Y_960, Z_959, X1_947, X2_964, W_192, U_193)=skf21(V_944, X_970, Y_972, Z_971, X1_973, X2_955, W_192, U_193) | skf21(V_946, X_961, Y_936, Z_969, X1_968, X2_942, W_192, U_193)=skf21(V_944, X_970, Y_972, Z_971, X1_973, X2_955, W_192, U_193) | skf21(V_954, X_974, Y_957, Z_950, X1_941, X2_937, W_192, U_193)=skf21(V_944, X_970, Y_972, Z_971, X1_973, X2_955, W_192, U_193) | skf21(V_954, X_974, Y_957, Z_950, X1_941, X2_937, W_192, U_193)=skf21(V_940, X_956, Y_962, Z_935, X1_952, X2_965, W_192, U_193) | skf21(V_954, X_974, Y_957, Z_950, X1_941, X2_937, W_192, U_193)=skf21(V_948, X_945, Y_960, Z_959, X1_947, X2_964, W_192, U_193) | skf21(V_954, X_974, Y_957, Z_950, X1_941, X2_937, W_192, U_193)=skf21(V_946, X_961, Y_936, Z_969, X1_968, X2_942, W_192, U_193) | skf21(V_954, X_974, Y_957, Z_950, X1_941, X2_937, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_944, X_970, Y_972, Z_971, X1_973, X2_955, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_940, X_956, Y_962, Z_935, X1_952, X2_965, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_948, X_945, Y_960, Z_959, X1_947, X2_964, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_946, X_961, Y_936, Z_969, X1_968, X2_942, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), V_966, W_949, X_958, Y_938, Z_963, X1_967, X2_939)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_942=X1_968 | Z_969=X1_968 | Z_969=X2_942 | Z_969=Y_936 | Y_936=X1_968 | Y_936=X2_942 | Y_936=X_961 | Z_969=X_961 | X_961=X1_968 | X_961=X2_942 | X_961=V_946 | Y_936=V_946 | Z_969=V_946 | X1_968=V_946 | X2_942=V_946 | ~member(U_193, X2_942, W_192) | ~member(U_193, X1_968, W_192) | ~member(U_193, Z_969, W_192) | ~member(U_193, Y_936, W_192) | ~member(U_193, X_961, W_192) | ~member(U_193, V_946, W_192) | X2_964=X1_947 | Z_959=X1_947 | Z_959=X2_964 | Z_959=Y_960 | Y_960=X1_947 | Y_960=X2_964 | Y_960=X_945 | Z_959=X_945 | X_945=X1_947 | X_945=X2_964 | X_945=V_948 | Y_960=V_948 | Z_959=V_948 | X1_947=V_948 | X2_964=V_948 | ~member(U_193, X2_964, W_192) | ~member(U_193, X1_947, W_192) | ~member(U_193, Z_959, W_192) | ~member(U_193, Y_960, W_192) | ~member(U_193, X_945, W_192) | ~member(U_193, V_948, W_192) | X2_965=X1_952 | Z_935=X1_952 | Z_935=X2_965 | Z_935=Y_962 | Y_962=X1_952 | Y_962=X2_965 | Y_962=X_956 | Z_935=X_956 | X_956=X1_952 | X_956=X2_965 | X_956=V_940 | Y_962=V_940 | Z_935=V_940 | X1_952=V_940 | X2_965=V_940 | ~member(U_193, X2_965, W_192) | ~member(U_193, X1_952, W_192) | ~member(U_193, Z_935, W_192) | ~member(U_193, Y_962, W_192) | ~member(U_193, X_956, W_192) | ~member(U_193, V_940, W_192) | X2_955=X1_973 | Z_971=X1_973 | Z_971=X2_955 | Z_971=Y_972 | Y_972=X1_973 | Y_972=X2_955 | Y_972=X_970 | Z_971=X_970 | X_970=X1_973 | X_970=X2_955 | X_970=V_944 | Y_972=V_944 | Z_971=V_944 | X1_973=V_944 | X2_955=V_944 | ~member(U_193, X2_955, W_192) | ~member(U_193, X1_973, W_192) | ~member(U_193, Z_971, W_192) | ~member(U_193, Y_972, W_192) | ~member(U_193, X_970, W_192) | ~member(U_193, V_944, W_192) | X2_937=X1_941 | Z_950=X1_941 | Z_950=X2_937 | Z_950=Y_957 | Y_957=X1_941 | Y_957=X2_937 | Y_957=X_974 | Z_950=X_974 | X_974=X1_941 | X_974=X2_937 | X_974=V_954 | Y_957=V_954 | Z_950=V_954 | X1_941=V_954 | X2_937=V_954 | ~member(U_193, X2_937, W_192) | ~member(U_193, X1_941, W_192) | ~member(U_193, Z_950, W_192) | ~member(U_193, Y_957, W_192) | ~member(U_193, X_974, W_192) | ~member(U_193, V_954, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_1023, plain, (![X1_879, Y_878, X_884, V_894, Z_194, Z_898, X2_871, V_199, X_895, X2_196, X2_869, X2_870, Z_885, Z_868, Z_896, Y_880, Z_886, X2_877, X_875, X2_881, X1_883, W_192, X1_872, X1_195, V_891, W_873, V_899, X_197, Y_198, V_888, X1_900, U_193, Y_893, X1_876, X_892, X_901, Y_887, Y_882, U_874]: (skf21(V_894, X_884, Y_880, Z_885, X1_879, X2_881, W_192, U_193)=skf21(V_888, X_892, Y_882, Z_868, X1_900, X2_871, W_192, U_193) | skf21(V_899, X_875, Y_878, Z_898, X1_876, X2_877, W_192, U_193)=skf21(V_894, X_884, Y_880, Z_885, X1_879, X2_881, W_192, U_193) | skf21(V_899, X_875, Y_878, Z_898, X1_876, X2_877, W_192, U_193)=skf21(V_888, X_892, Y_882, Z_868, X1_900, X2_871, W_192, U_193) | skf21(V_899, X_875, Y_878, Z_898, X1_876, X2_877, W_192, U_193)=skf21(V_891, X_901, Y_893, Z_886, X1_872, X2_869, W_192, U_193) | skf21(V_894, X_884, Y_880, Z_885, X1_879, X2_881, W_192, U_193)=skf21(V_891, X_901, Y_893, Z_886, X1_872, X2_869, W_192, U_193) | skf21(V_891, X_901, Y_893, Z_886, X1_872, X2_869, W_192, U_193)=skf21(V_888, X_892, Y_882, Z_868, X1_900, X2_871, W_192, U_193) | skf21(V_891, X_901, Y_893, Z_886, X1_872, X2_869, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_899, X_875, Y_878, Z_898, X1_876, X2_877, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_894, X_884, Y_880, Z_885, X1_879, X2_881, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_888, X_892, Y_882, Z_868, X1_900, X2_871, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_874 | skf21(V_891, X_901, Y_893, Z_886, X1_872, X2_869, W_192, U_193)=U_874 | skf21(V_899, X_875, Y_878, Z_898, X1_876, X2_877, W_192, U_193)=U_874 | skf21(V_894, X_884, Y_880, Z_885, X1_879, X2_881, W_192, U_193)=U_874 | skf21(V_888, X_892, Y_882, Z_868, X1_900, X2_871, W_192, U_193)=U_874 | ~member(U_193, U_874, W_192) | skf21(U_874, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_873, X_895, Y_887, Z_896, X1_883, X2_870)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_871=X1_900 | Z_868=X1_900 | Z_868=X2_871 | Z_868=Y_882 | Y_882=X1_900 | Y_882=X2_871 | Y_882=X_892 | Z_868=X_892 | X_892=X1_900 | X_892=X2_871 | X_892=V_888 | Y_882=V_888 | Z_868=V_888 | X1_900=V_888 | X2_871=V_888 | ~member(U_193, X2_871, W_192) | ~member(U_193, X1_900, W_192) | ~member(U_193, Z_868, W_192) | ~member(U_193, Y_882, W_192) | ~member(U_193, X_892, W_192) | ~member(U_193, V_888, W_192) | X2_881=X1_879 | Z_885=X1_879 | Z_885=X2_881 | Z_885=Y_880 | Y_880=X1_879 | Y_880=X2_881 | Y_880=X_884 | Z_885=X_884 | X_884=X1_879 | X_884=X2_881 | X_884=V_894 | Y_880=V_894 | Z_885=V_894 | X1_879=V_894 | X2_881=V_894 | ~member(U_193, X2_881, W_192) | ~member(U_193, X1_879, W_192) | ~member(U_193, Z_885, W_192) | ~member(U_193, Y_880, W_192) | ~member(U_193, X_884, W_192) | ~member(U_193, V_894, W_192) | X2_877=X1_876 | Z_898=X1_876 | Z_898=X2_877 | Z_898=Y_878 | Y_878=X1_876 | Y_878=X2_877 | Y_878=X_875 | Z_898=X_875 | X_875=X1_876 | X_875=X2_877 | X_875=V_899 | Y_878=V_899 | Z_898=V_899 | X1_876=V_899 | X2_877=V_899 | ~member(U_193, X2_877, W_192) | ~member(U_193, X1_876, W_192) | ~member(U_193, Z_898, W_192) | ~member(U_193, Y_878, W_192) | ~member(U_193, X_875, W_192) | ~member(U_193, V_899, W_192) | X2_869=X1_872 | Z_886=X1_872 | Z_886=X2_869 | Z_886=Y_893 | Y_893=X1_872 | Y_893=X2_869 | Y_893=X_901 | Z_886=X_901 | X_901=X1_872 | X_901=X2_869 | X_901=V_891 | Y_893=V_891 | Z_886=V_891 | X1_872=V_891 | X2_869=V_891 | ~member(U_193, X2_869, W_192) | ~member(U_193, X1_872, W_192) | ~member(U_193, Z_886, W_192) | ~member(U_193, Y_893, W_192) | ~member(U_193, X_901, W_192) | ~member(U_193, V_891, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_1001, plain, (![X2_847, X_862, X_866, X_836, X1_851, Z_194, Z_843, X_844, V_199, Z_838, V_859, Y_841, X2_196, V_860, U_857, X_861, Y_854, X1_855, X1_837, Y_858, Y_840, X2_833, W_864, Z_839, V_867, Z_848, Y_863, W_192, X1_195, Z_834, X2_856, X2_842, V_845, V_853, X_197, Y_198, X2_835, U_193, X1_865, X1_846]: (skf21(V_867, X_862, Y_841, Z_839, X1_865, X2_847, W_192, U_193)=skf21(V_859, X_836, Y_863, Z_843, X1_851, X2_842, W_192, U_193) | skf21(V_867, X_862, Y_841, Z_839, X1_865, X2_847, W_192, U_193)=skf21(V_845, X_844, Y_840, Z_838, X1_855, X2_856, W_192, U_193) | skf21(V_859, X_836, Y_863, Z_843, X1_851, X2_842, W_192, U_193)=skf21(V_845, X_844, Y_840, Z_838, X1_855, X2_856, W_192, U_193) | skf21(V_853, X_866, Y_854, Z_848, X1_837, X2_835, W_192, U_193)=skf21(V_845, X_844, Y_840, Z_838, X1_855, X2_856, W_192, U_193) | skf21(V_867, X_862, Y_841, Z_839, X1_865, X2_847, W_192, U_193)=skf21(V_853, X_866, Y_854, Z_848, X1_837, X2_835, W_192, U_193) | skf21(V_859, X_836, Y_863, Z_843, X1_851, X2_842, W_192, U_193)=skf21(V_853, X_866, Y_854, Z_848, X1_837, X2_835, W_192, U_193) | skf21(V_853, X_866, Y_854, Z_848, X1_837, X2_835, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_845, X_844, Y_840, Z_838, X1_855, X2_856, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_867, X_862, Y_841, Z_839, X1_865, X2_847, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_859, X_836, Y_863, Z_843, X1_851, X2_842, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_857 | skf21(V_853, X_866, Y_854, Z_848, X1_837, X2_835, W_192, U_193)=U_857 | skf21(V_845, X_844, Y_840, Z_838, X1_855, X2_856, W_192, U_193)=U_857 | skf21(V_867, X_862, Y_841, Z_839, X1_865, X2_847, W_192, U_193)=U_857 | skf21(V_859, X_836, Y_863, Z_843, X1_851, X2_842, W_192, U_193)=U_857 | ~member(U_193, U_857, W_192) | skf21(U_857, V_860, W_864, X_861, Y_858, Z_834, X1_846, X2_833)!=U_857 | X2_842=X1_851 | Z_843=X1_851 | Z_843=X2_842 | Z_843=Y_863 | Y_863=X1_851 | Y_863=X2_842 | Y_863=X_836 | Z_843=X_836 | X_836=X1_851 | X_836=X2_842 | X_836=V_859 | Y_863=V_859 | Z_843=V_859 | X1_851=V_859 | X2_842=V_859 | ~member(U_193, X2_842, W_192) | ~member(U_193, X1_851, W_192) | ~member(U_193, Z_843, W_192) | ~member(U_193, Y_863, W_192) | ~member(U_193, X_836, W_192) | ~member(U_193, V_859, W_192) | X2_847=X1_865 | Z_839=X1_865 | Z_839=X2_847 | Z_839=Y_841 | Y_841=X1_865 | Y_841=X2_847 | Y_841=X_862 | Z_839=X_862 | X_862=X1_865 | X_862=X2_847 | X_862=V_867 | Y_841=V_867 | Z_839=V_867 | X1_865=V_867 | X2_847=V_867 | ~member(U_193, X2_847, W_192) | ~member(U_193, X1_865, W_192) | ~member(U_193, Z_839, W_192) | ~member(U_193, Y_841, W_192) | ~member(U_193, X_862, W_192) | ~member(U_193, V_867, W_192) | X2_856=X1_855 | Z_838=X1_855 | Z_838=X2_856 | Z_838=Y_840 | Y_840=X1_855 | Y_840=X2_856 | Y_840=X_844 | Z_838=X_844 | X_844=X1_855 | X_844=X2_856 | X_844=V_845 | Y_840=V_845 | Z_838=V_845 | X1_855=V_845 | X2_856=V_845 | ~member(U_193, X2_856, W_192) | ~member(U_193, X1_855, W_192) | ~member(U_193, Z_838, W_192) | ~member(U_193, Y_840, W_192) | ~member(U_193, X_844, W_192) | ~member(U_193, V_845, W_192) | X2_835=X1_837 | Z_848=X1_837 | Z_848=X2_835 | Z_848=Y_854 | Y_854=X1_837 | Y_854=X2_835 | Y_854=X_866 | Z_848=X_866 | X_866=X1_837 | X_866=X2_835 | X_866=V_853 | Y_854=V_853 | Z_848=V_853 | X1_837=V_853 | X2_835=V_853 | ~member(U_193, X2_835, W_192) | ~member(U_193, X1_837, W_192) | ~member(U_193, Z_848, W_192) | ~member(U_193, Y_854, W_192) | ~member(U_193, X_866, W_192) | ~member(U_193, V_853, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_956, plain, (![X1_773, X1_753, V_768, Z_194, V_199, V_758, Y_759, X_775, X2_196, X2_751, Y_769, X2_754, X_763, X1_748, U_772, Z_766, V_755, W_192, X_770, X2_750, X1_195, V_749, X1_760, X2_761, Y_774, X_197, Y_198, Y_756, Z_757, U_193, X_762, Z_771, Z_764]: (skf21(V_755, X_763, Y_774, Z_766, X1_760, X2_761, W_192, U_193)=skf21(V_749, X_770, Y_756, Z_771, X1_773, X2_750, W_192, U_193) | skf21(V_768, X_775, Y_769, Z_764, X1_753, X2_751, W_192, U_193)=skf21(V_749, X_770, Y_756, Z_771, X1_773, X2_750, W_192, U_193) | skf21(V_768, X_775, Y_769, Z_764, X1_753, X2_751, W_192, U_193)=skf21(V_755, X_763, Y_774, Z_766, X1_760, X2_761, W_192, U_193) | skf21(V_768, X_775, Y_769, Z_764, X1_753, X2_751, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_749, X_770, Y_756, Z_771, X1_773, X2_750, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_755, X_763, Y_774, Z_766, X1_760, X2_761, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_758 | skf21(V_768, X_775, Y_769, Z_764, X1_753, X2_751, W_192, U_193)=V_758 | skf21(V_749, X_770, Y_756, Z_771, X1_773, X2_750, W_192, U_193)=V_758 | skf21(V_755, X_763, Y_774, Z_766, X1_760, X2_761, W_192, U_193)=V_758 | V_758=U_772 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_772 | skf21(V_768, X_775, Y_769, Z_764, X1_753, X2_751, W_192, U_193)=U_772 | skf21(V_749, X_770, Y_756, Z_771, X1_773, X2_750, W_192, U_193)=U_772 | skf21(V_755, X_763, Y_774, Z_766, X1_760, X2_761, W_192, U_193)=U_772 | ~member(U_193, V_758, W_192) | ~member(U_193, U_772, W_192) | skf21(U_772, V_758, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_762, Y_759, Z_757, X1_748, X2_754)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_761=X1_760 | Z_766=X1_760 | Z_766=X2_761 | Z_766=Y_774 | Y_774=X1_760 | Y_774=X2_761 | Y_774=X_763 | Z_766=X_763 | X_763=X1_760 | X_763=X2_761 | X_763=V_755 | Y_774=V_755 | Z_766=V_755 | X1_760=V_755 | X2_761=V_755 | ~member(U_193, X2_761, W_192) | ~member(U_193, X1_760, W_192) | ~member(U_193, Z_766, W_192) | ~member(U_193, Y_774, W_192) | ~member(U_193, X_763, W_192) | ~member(U_193, V_755, W_192) | X2_750=X1_773 | Z_771=X1_773 | Z_771=X2_750 | Z_771=Y_756 | Y_756=X1_773 | Y_756=X2_750 | Y_756=X_770 | Z_771=X_770 | X_770=X1_773 | X_770=X2_750 | X_770=V_749 | Y_756=V_749 | Z_771=V_749 | X1_773=V_749 | X2_750=V_749 | ~member(U_193, X2_750, W_192) | ~member(U_193, X1_773, W_192) | ~member(U_193, Z_771, W_192) | ~member(U_193, Y_756, W_192) | ~member(U_193, X_770, W_192) | ~member(U_193, V_749, W_192) | X2_751=X1_753 | Z_764=X1_753 | Z_764=X2_751 | Z_764=Y_769 | Y_769=X1_753 | Y_769=X2_751 | Y_769=X_775 | Z_764=X_775 | X_775=X1_753 | X_775=X2_751 | X_775=V_768 | Y_769=V_768 | Z_764=V_768 | X1_753=V_768 | X2_751=V_768 | ~member(U_193, X2_751, W_192) | ~member(U_193, X1_753, W_192) | ~member(U_193, Z_764, W_192) | ~member(U_193, Y_769, W_192) | ~member(U_193, X_775, W_192) | ~member(U_193, V_768, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_934, plain, (![Z_729, V_742, Y_737, U_745, Z_194, X1_730, V_199, X2_724, V_735, X2_196, X2_736, X1_743, X2_721, W_746, Y_744, X_747, V_719, X1_722, W_192, Y_739, X1_195, Z_728, X_738, Y_741, V_727, X1_726, X_723, X_197, Y_198, X_740, U_193, Z_731, X2_720, Z_732]: (skf21(V_742, X_723, Y_741, Z_728, X1_743, X2_720, W_192, U_193)=skf21(V_719, X_740, Y_744, Z_732, X1_730, X2_724, W_192, U_193) | skf21(V_735, X_747, Y_739, Z_731, X1_722, X2_721, W_192, U_193)=skf21(V_719, X_740, Y_744, Z_732, X1_730, X2_724, W_192, U_193) | skf21(V_742, X_723, Y_741, Z_728, X1_743, X2_720, W_192, U_193)=skf21(V_735, X_747, Y_739, Z_731, X1_722, X2_721, W_192, U_193) | skf21(V_735, X_747, Y_739, Z_731, X1_722, X2_721, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_719, X_740, Y_744, Z_732, X1_730, X2_724, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_742, X_723, Y_741, Z_728, X1_743, X2_720, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_727 | skf21(V_735, X_747, Y_739, Z_731, X1_722, X2_721, W_192, U_193)=V_727 | skf21(V_719, X_740, Y_744, Z_732, X1_730, X2_724, W_192, U_193)=V_727 | skf21(V_742, X_723, Y_741, Z_728, X1_743, X2_720, W_192, U_193)=V_727 | V_727=U_745 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_745 | skf21(V_735, X_747, Y_739, Z_731, X1_722, X2_721, W_192, U_193)=U_745 | skf21(V_719, X_740, Y_744, Z_732, X1_730, X2_724, W_192, U_193)=U_745 | skf21(V_742, X_723, Y_741, Z_728, X1_743, X2_720, W_192, U_193)=U_745 | ~member(U_193, V_727, W_192) | ~member(U_193, U_745, W_192) | skf21(U_745, V_727, W_746, X_738, Y_737, Z_729, X1_726, X2_736)!=V_727 | X2_720=X1_743 | Z_728=X1_743 | Z_728=X2_720 | Z_728=Y_741 | Y_741=X1_743 | Y_741=X2_720 | Y_741=X_723 | Z_728=X_723 | X_723=X1_743 | X_723=X2_720 | X_723=V_742 | Y_741=V_742 | Z_728=V_742 | X1_743=V_742 | X2_720=V_742 | ~member(U_193, X2_720, W_192) | ~member(U_193, X1_743, W_192) | ~member(U_193, Z_728, W_192) | ~member(U_193, Y_741, W_192) | ~member(U_193, X_723, W_192) | ~member(U_193, V_742, W_192) | X2_724=X1_730 | Z_732=X1_730 | Z_732=X2_724 | Z_732=Y_744 | Y_744=X1_730 | Y_744=X2_724 | Y_744=X_740 | Z_732=X_740 | X_740=X1_730 | X_740=X2_724 | X_740=V_719 | Y_744=V_719 | Z_732=V_719 | X1_730=V_719 | X2_724=V_719 | ~member(U_193, X2_724, W_192) | ~member(U_193, X1_730, W_192) | ~member(U_193, Z_732, W_192) | ~member(U_193, Y_744, W_192) | ~member(U_193, X_740, W_192) | ~member(U_193, V_719, W_192) | X2_721=X1_722 | Z_731=X1_722 | Z_731=X2_721 | Z_731=Y_739 | Y_739=X1_722 | Y_739=X2_721 | Y_739=X_747 | Z_731=X_747 | X_747=X1_722 | X_747=X2_721 | X_747=V_735 | Y_739=V_735 | Z_731=V_735 | X1_722=V_735 | X2_721=V_735 | ~member(U_193, X2_721, W_192) | ~member(U_193, X1_722, W_192) | ~member(U_193, Z_731, W_192) | ~member(U_193, Y_739, W_192) | ~member(U_193, X_747, W_192) | ~member(U_193, V_735, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_978, plain, (![Z_785, V_780, Y_796, X1_795, V_783, X_788, Z_194, V_199, X2_802, V_791, X2_196, Y_794, X1_787, Z_782, X2_776, Y_786, X_778, W_192, X2_777, X1_195, V_793, W_799, Z_784, X1_801, X2_803, X_197, Y_198, X_804, Y_805, X1_779, U_193, X5_798, U_781, Z_789, X_800]: (skf21(V_791, X_788, Y_805, Z_785, X1_787, X2_803, W_192, U_193)=skf21(V_783, X_778, Y_796, Z_784, X1_801, X2_776, W_192, U_193) | skf21(V_793, X_804, Y_794, Z_789, X1_779, X2_777, W_192, U_193)=skf21(V_791, X_788, Y_805, Z_785, X1_787, X2_803, W_192, U_193) | skf21(V_793, X_804, Y_794, Z_789, X1_779, X2_777, W_192, U_193)=skf21(V_783, X_778, Y_796, Z_784, X1_801, X2_776, W_192, U_193) | skf21(V_793, X_804, Y_794, Z_789, X1_779, X2_777, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_791, X_788, Y_805, Z_785, X1_787, X2_803, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_783, X_778, Y_796, Z_784, X1_801, X2_776, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_798 | skf21(V_793, X_804, Y_794, Z_789, X1_779, X2_777, W_192, U_193)=X5_798 | skf21(V_791, X_788, Y_805, Z_785, X1_787, X2_803, W_192, U_193)=X5_798 | skf21(V_783, X_778, Y_796, Z_784, X1_801, X2_776, W_192, U_193)=X5_798 | X5_798=U_781 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_781 | skf21(V_793, X_804, Y_794, Z_789, X1_779, X2_777, W_192, U_193)=U_781 | skf21(V_791, X_788, Y_805, Z_785, X1_787, X2_803, W_192, U_193)=U_781 | skf21(V_783, X_778, Y_796, Z_784, X1_801, X2_776, W_192, U_193)=U_781 | ~member(U_193, X5_798, W_192) | ~member(U_193, U_781, W_192) | skf21(U_781, V_780, W_799, X_800, Y_786, Z_782, X1_795, X2_802)!=U_781 | X2_776=X1_801 | Z_784=X1_801 | Z_784=X2_776 | Z_784=Y_796 | Y_796=X1_801 | Y_796=X2_776 | Y_796=X_778 | Z_784=X_778 | X_778=X1_801 | X_778=X2_776 | X_778=V_783 | Y_796=V_783 | Z_784=V_783 | X1_801=V_783 | X2_776=V_783 | ~member(U_193, X2_776, W_192) | ~member(U_193, X1_801, W_192) | ~member(U_193, Z_784, W_192) | ~member(U_193, Y_796, W_192) | ~member(U_193, X_778, W_192) | ~member(U_193, V_783, W_192) | X2_803=X1_787 | Z_785=X1_787 | Z_785=X2_803 | Z_785=Y_805 | Y_805=X1_787 | Y_805=X2_803 | Y_805=X_788 | Z_785=X_788 | X_788=X1_787 | X_788=X2_803 | X_788=V_791 | Y_805=V_791 | Z_785=V_791 | X1_787=V_791 | X2_803=V_791 | ~member(U_193, X2_803, W_192) | ~member(U_193, X1_787, W_192) | ~member(U_193, Z_785, W_192) | ~member(U_193, Y_805, W_192) | ~member(U_193, X_788, W_192) | ~member(U_193, V_791, W_192) | X2_777=X1_779 | Z_789=X1_779 | Z_789=X2_777 | Z_789=Y_794 | Y_794=X1_779 | Y_794=X2_777 | Y_794=X_804 | Z_789=X_804 | X_804=X1_779 | X_804=X2_777 | X_804=V_793 | Y_794=V_793 | Z_789=V_793 | X1_779=V_793 | X2_777=V_793 | ~member(U_193, X2_777, W_192) | ~member(U_193, X1_779, W_192) | ~member(U_193, Z_789, W_192) | ~member(U_193, Y_794, W_192) | ~member(U_193, X_804, W_192) | ~member(U_193, V_793, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_867, plain, (![X1_629, X1_630, Y_628, Z_194, X2_627, V_199, X2_196, Z_647, V_633, V_639, U_636, Y_641, X1_631, W_192, Z_635, X1_195, Y_645, Z_640, X2_646, X_648, X_632, V_643, X_197, Y_198, X2_644, W_642, U_193]: (skf21(V_643, X_632, Y_628, Z_647, X1_630, X2_646, W_192, U_193)=skf21(V_639, X_648, Y_641, Z_635, X1_629, X2_627, W_192, U_193) | skf21(V_639, X_648, Y_641, Z_635, X1_629, X2_627, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_643, X_632, Y_628, Z_647, X1_630, X2_646, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_642 | skf21(V_639, X_648, Y_641, Z_635, X1_629, X2_627, W_192, U_193)=W_642 | skf21(V_643, X_632, Y_628, Z_647, X1_630, X2_646, W_192, U_193)=W_642 | W_642=V_633 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_633 | skf21(V_639, X_648, Y_641, Z_635, X1_629, X2_627, W_192, U_193)=V_633 | skf21(V_643, X_632, Y_628, Z_647, X1_630, X2_646, W_192, U_193)=V_633 | V_633=U_636 | W_642=U_636 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_636 | skf21(V_639, X_648, Y_641, Z_635, X1_629, X2_627, W_192, U_193)=U_636 | skf21(V_643, X_632, Y_628, Z_647, X1_630, X2_646, W_192, U_193)=U_636 | ~member(U_193, W_642, W_192) | ~member(U_193, V_633, W_192) | ~member(U_193, U_636, W_192) | skf21(U_636, V_633, W_642, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_645, Z_640, X1_631, X2_644)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_646=X1_630 | Z_647=X1_630 | Z_647=X2_646 | Z_647=Y_628 | Y_628=X1_630 | Y_628=X2_646 | Y_628=X_632 | Z_647=X_632 | X_632=X1_630 | X_632=X2_646 | X_632=V_643 | Y_628=V_643 | Z_647=V_643 | X1_630=V_643 | X2_646=V_643 | ~member(U_193, X2_646, W_192) | ~member(U_193, X1_630, W_192) | ~member(U_193, Z_647, W_192) | ~member(U_193, Y_628, W_192) | ~member(U_193, X_632, W_192) | ~member(U_193, V_643, W_192) | X2_627=X1_629 | Z_635=X1_629 | Z_635=X2_627 | Z_635=Y_641 | Y_641=X1_629 | Y_641=X2_627 | Y_641=X_648 | Z_635=X_648 | X_648=X1_629 | X_648=X2_627 | X_648=V_639 | Y_641=V_639 | Z_635=V_639 | X1_629=V_639 | X2_627=V_639 | ~member(U_193, X2_627, W_192) | ~member(U_193, X1_629, W_192) | ~member(U_193, Z_635, W_192) | ~member(U_193, Y_641, W_192) | ~member(U_193, X_648, W_192) | ~member(U_193, V_639, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_889, plain, (![V_672, X1_659, X5_671, Z_194, V_199, X2_649, Z_668, Y_666, Y_655, X2_196, X_673, X1_658, U_662, Y_656, Z_657, V_650, W_192, Z_661, W_654, X1_195, X_667, V_665, X6_669, X2_670, X_197, Y_198, U_193, X_653, X1_651, X2_660]: (skf21(V_672, X_653, Y_655, Z_668, X1_658, X2_660, W_192, U_193)=skf21(V_665, X_673, Y_666, Z_661, X1_651, X2_649, W_192, U_193) | skf21(V_665, X_673, Y_666, Z_661, X1_651, X2_649, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_672, X_653, Y_655, Z_668, X1_658, X2_660, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_669 | skf21(V_665, X_673, Y_666, Z_661, X1_651, X2_649, W_192, U_193)=X6_669 | skf21(V_672, X_653, Y_655, Z_668, X1_658, X2_660, W_192, U_193)=X6_669 | X6_669=X5_671 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_671 | skf21(V_665, X_673, Y_666, Z_661, X1_651, X2_649, W_192, U_193)=X5_671 | skf21(V_672, X_653, Y_655, Z_668, X1_658, X2_660, W_192, U_193)=X5_671 | X5_671=U_662 | X6_669=U_662 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_662 | skf21(V_665, X_673, Y_666, Z_661, X1_651, X2_649, W_192, U_193)=U_662 | skf21(V_672, X_653, Y_655, Z_668, X1_658, X2_660, W_192, U_193)=U_662 | ~member(U_193, X6_669, W_192) | ~member(U_193, X5_671, W_192) | ~member(U_193, U_662, W_192) | skf21(U_662, V_650, W_654, X_667, Y_656, Z_657, X1_659, X2_670)!=U_662 | X2_660=X1_658 | Z_668=X1_658 | Z_668=X2_660 | Z_668=Y_655 | Y_655=X1_658 | Y_655=X2_660 | Y_655=X_653 | Z_668=X_653 | X_653=X1_658 | X_653=X2_660 | X_653=V_672 | Y_655=V_672 | Z_668=V_672 | X1_658=V_672 | X2_660=V_672 | ~member(U_193, X2_660, W_192) | ~member(U_193, X1_658, W_192) | ~member(U_193, Z_668, W_192) | ~member(U_193, Y_655, W_192) | ~member(U_193, X_653, W_192) | ~member(U_193, V_672, W_192) | X2_649=X1_651 | Z_661=X1_651 | Z_661=X2_649 | Z_661=Y_666 | Y_666=X1_651 | Y_666=X2_649 | Y_666=X_673 | Z_661=X_673 | X_673=X1_651 | X_673=X2_649 | X_673=V_665 | Y_666=V_665 | Z_661=V_665 | X1_651=V_665 | X2_649=V_665 | ~member(U_193, X2_649, W_192) | ~member(U_193, X1_651, W_192) | ~member(U_193, Z_661, W_192) | ~member(U_193, Y_666, W_192) | ~member(U_193, X_673, W_192) | ~member(U_193, V_665, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_845, plain, (![V_623, X_624, Z_194, X1_611, V_199, V_622, X2_196, X1_625, X2_607, Z_617, Z_606, W_621, W_192, Y_618, Z_612, X1_195, X2_620, X_626, X_609, Y_610, X_197, Y_198, X1_608, U_193, X2_604, V_616, Y_619, U_614]: (skf21(V_623, X_609, Y_618, Z_617, X1_611, X2_620, W_192, U_193)=skf21(V_616, X_626, Y_619, Z_612, X1_608, X2_604, W_192, U_193) | skf21(V_616, X_626, Y_619, Z_612, X1_608, X2_604, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_623, X_609, Y_618, Z_617, X1_611, X2_620, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_621 | skf21(V_616, X_626, Y_619, Z_612, X1_608, X2_604, W_192, U_193)=W_621 | skf21(V_623, X_609, Y_618, Z_617, X1_611, X2_620, W_192, U_193)=W_621 | W_621=V_622 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_622 | skf21(V_616, X_626, Y_619, Z_612, X1_608, X2_604, W_192, U_193)=V_622 | skf21(V_623, X_609, Y_618, Z_617, X1_611, X2_620, W_192, U_193)=V_622 | V_622=U_614 | W_621=U_614 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_614 | skf21(V_616, X_626, Y_619, Z_612, X1_608, X2_604, W_192, U_193)=U_614 | skf21(V_623, X_609, Y_618, Z_617, X1_611, X2_620, W_192, U_193)=U_614 | ~member(U_193, W_621, W_192) | ~member(U_193, V_622, W_192) | ~member(U_193, U_614, W_192) | skf21(U_614, V_622, W_621, X_624, Y_610, Z_606, X1_625, X2_607)!=W_621 | X2_620=X1_611 | Z_617=X1_611 | Z_617=X2_620 | Z_617=Y_618 | Y_618=X1_611 | Y_618=X2_620 | Y_618=X_609 | Z_617=X_609 | X_609=X1_611 | X_609=X2_620 | X_609=V_623 | Y_618=V_623 | Z_617=V_623 | X1_611=V_623 | X2_620=V_623 | ~member(U_193, X2_620, W_192) | ~member(U_193, X1_611, W_192) | ~member(U_193, Z_617, W_192) | ~member(U_193, Y_618, W_192) | ~member(U_193, X_609, W_192) | ~member(U_193, V_623, W_192) | X2_604=X1_608 | Z_612=X1_608 | Z_612=X2_604 | Z_612=Y_619 | Y_619=X1_608 | Y_619=X2_604 | Y_619=X_626 | Z_612=X_626 | X_626=X1_608 | X_626=X2_604 | X_626=V_616 | Y_619=V_616 | Z_612=V_616 | X1_608=V_616 | X2_604=V_616 | ~member(U_193, X2_604, W_192) | ~member(U_193, X1_608, W_192) | ~member(U_193, Z_612, W_192) | ~member(U_193, Y_619, W_192) | ~member(U_193, X_626, W_192) | ~member(U_193, V_616, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_911, plain, (![W_691, Y_688, X5_682, Z_194, X2_694, V_199, V_675, X2_196, Z_693, Y_679, V_687, X2_690, X2_676, X_689, W_192, X_678, X1_195, X1_681, X_197, Y_198, U_696, Z_674, X_697, X1_677, U_193, V_680, Z_684, Y_683, X1_695]: (skf21(V_687, X_697, Y_688, Z_684, X1_677, X2_676, W_192, U_193)=skf21(V_680, X_689, Y_683, Z_674, X1_695, X2_690, W_192, U_193) | skf21(V_687, X_697, Y_688, Z_684, X1_677, X2_676, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_680, X_689, Y_683, Z_674, X1_695, X2_690, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_682 | skf21(V_687, X_697, Y_688, Z_684, X1_677, X2_676, W_192, U_193)=X5_682 | skf21(V_680, X_689, Y_683, Z_674, X1_695, X2_690, W_192, U_193)=X5_682 | X5_682=V_675 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_675 | skf21(V_687, X_697, Y_688, Z_684, X1_677, X2_676, W_192, U_193)=V_675 | skf21(V_680, X_689, Y_683, Z_674, X1_695, X2_690, W_192, U_193)=V_675 | V_675=U_696 | X5_682=U_696 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_696 | skf21(V_687, X_697, Y_688, Z_684, X1_677, X2_676, W_192, U_193)=U_696 | skf21(V_680, X_689, Y_683, Z_674, X1_695, X2_690, W_192, U_193)=U_696 | ~member(U_193, X5_682, W_192) | ~member(U_193, V_675, W_192) | ~member(U_193, U_696, W_192) | skf21(U_696, V_675, W_691, X_678, Y_679, Z_693, X1_681, X2_694)!=V_675 | X2_690=X1_695 | Z_674=X1_695 | Z_674=X2_690 | Z_674=Y_683 | Y_683=X1_695 | Y_683=X2_690 | Y_683=X_689 | Z_674=X_689 | X_689=X1_695 | X_689=X2_690 | X_689=V_680 | Y_683=V_680 | Z_674=V_680 | X1_695=V_680 | X2_690=V_680 | ~member(U_193, X2_690, W_192) | ~member(U_193, X1_695, W_192) | ~member(U_193, Z_674, W_192) | ~member(U_193, Y_683, W_192) | ~member(U_193, X_689, W_192) | ~member(U_193, V_680, W_192) | X2_676=X1_677 | Z_684=X1_677 | Z_684=X2_676 | Z_684=Y_688 | Y_688=X1_677 | Y_688=X2_676 | Y_688=X_697 | Z_684=X_697 | X_697=X1_677 | X_697=X2_676 | X_697=V_687 | Y_688=V_687 | Z_684=V_687 | X1_677=V_687 | X2_676=V_687 | ~member(U_193, X2_676, W_192) | ~member(U_193, X1_677, W_192) | ~member(U_193, Z_684, W_192) | ~member(U_193, Y_688, W_192) | ~member(U_193, X_697, W_192) | ~member(U_193, V_687, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_800, plain, (![X_557, Z_568, Z_194, X2_555, V_199, U_558, X1_565, X2_196, X2_554, V_556, W_192, W_559, X_562, X1_563, X1_195, Y_564, V_569, X_197, Y_198, Z_561, U_193]: (skf21(V_556, X_562, Y_564, Z_561, X1_563, X2_555, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_557 | skf21(V_556, X_562, Y_564, Z_561, X1_563, X2_555, W_192, U_193)=X_557 | X_557=W_559 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_559 | skf21(V_556, X_562, Y_564, Z_561, X1_563, X2_555, W_192, U_193)=W_559 | W_559=V_569 | X_557=V_569 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_569 | skf21(V_556, X_562, Y_564, Z_561, X1_563, X2_555, W_192, U_193)=V_569 | V_569=U_558 | W_559=U_558 | X_557=U_558 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_558 | skf21(V_556, X_562, Y_564, Z_561, X1_563, X2_555, W_192, U_193)=U_558 | ~member(U_193, X_557, W_192) | ~member(U_193, W_559, W_192) | ~member(U_193, V_569, W_192) | ~member(U_193, U_558, W_192) | skf21(U_558, V_569, W_559, X_557, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_568, X1_565, X2_554)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_555=X1_563 | Z_561=X1_563 | Z_561=X2_555 | Z_561=Y_564 | Y_564=X1_563 | Y_564=X2_555 | Y_564=X_562 | Z_561=X_562 | X_562=X1_563 | X_562=X2_555 | X_562=V_556 | Y_564=V_556 | Z_561=V_556 | X1_563=V_556 | X2_555=V_556 | ~member(U_193, X2_555, W_192) | ~member(U_193, X1_563, W_192) | ~member(U_193, Z_561, W_192) | ~member(U_193, Y_564, W_192) | ~member(U_193, X_562, W_192) | ~member(U_193, V_556, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_822, plain, (![Z_194, V_199, Y_587, X6_571, X2_572, X2_196, Z_574, U_585, X1_588, W_192, X1_580, X1_195, X2_570, X_577, V_573, Z_581, X5_575, X_197, Y_198, X_578, W_579, U_193, Y_582, V_576]: (skf21(V_573, X_577, Y_582, Z_574, X1_580, X2_572, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_571 | skf21(V_573, X_577, Y_582, Z_574, X1_580, X2_572, W_192, U_193)=X6_571 | X6_571=X5_575 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_575 | skf21(V_573, X_577, Y_582, Z_574, X1_580, X2_572, W_192, U_193)=X5_575 | X5_575=V_576 | X6_571=V_576 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_576 | skf21(V_573, X_577, Y_582, Z_574, X1_580, X2_572, W_192, U_193)=V_576 | V_576=U_585 | X5_575=U_585 | X6_571=U_585 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_585 | skf21(V_573, X_577, Y_582, Z_574, X1_580, X2_572, W_192, U_193)=U_585 | ~member(U_193, X6_571, W_192) | ~member(U_193, X5_575, W_192) | ~member(U_193, V_576, W_192) | ~member(U_193, U_585, W_192) | skf21(U_585, V_576, W_579, X_578, Y_587, Z_581, X1_588, X2_570)!=V_576 | X2_572=X1_580 | Z_574=X1_580 | Z_574=X2_572 | Z_574=Y_582 | Y_582=X1_580 | Y_582=X2_572 | Y_582=X_577 | Z_574=X_577 | X_577=X1_580 | X_577=X2_572 | X_577=V_573 | Y_582=V_573 | Z_574=V_573 | X1_580=V_573 | X2_572=V_573 | ~member(U_193, X2_572, W_192) | ~member(U_193, X1_580, W_192) | ~member(U_193, Z_574, W_192) | ~member(U_193, Y_582, W_192) | ~member(U_193, X_577, W_192) | ~member(U_193, V_573, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_734, plain, (![Y_513, X1_511, X5_517, X_505, Z_194, V_199, X2_196, X_506, X1_512, X2_500, W_501, U_518, X2_507, W_192, Z_504, X1_195, X6_516, V_502, Z_509, X_197, Y_198, Y_510, U_193, X7_499, V_508]: (skf21(V_502, X_505, Y_513, Z_504, X1_511, X2_500, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X7_499 | skf21(V_502, X_505, Y_513, Z_504, X1_511, X2_500, W_192, U_193)=X7_499 | X7_499=X6_516 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_516 | skf21(V_502, X_505, Y_513, Z_504, X1_511, X2_500, W_192, U_193)=X6_516 | X6_516=X5_517 | X7_499=X5_517 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_517 | skf21(V_502, X_505, Y_513, Z_504, X1_511, X2_500, W_192, U_193)=X5_517 | X5_517=U_518 | X6_516=U_518 | X7_499=U_518 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_518 | skf21(V_502, X_505, Y_513, Z_504, X1_511, X2_500, W_192, U_193)=U_518 | ~member(U_193, X7_499, W_192) | ~member(U_193, X6_516, W_192) | ~member(U_193, X5_517, W_192) | ~member(U_193, U_518, W_192) | skf21(U_518, V_508, W_501, X_506, Y_510, Z_509, X1_512, X2_507)!=U_518 | X2_500=X1_511 | Z_504=X1_511 | Z_504=X2_500 | Z_504=Y_513 | Y_513=X1_511 | Y_513=X2_500 | Y_513=X_505 | Z_504=X_505 | X_505=X1_511 | X_505=X2_500 | X_505=V_502 | Y_513=V_502 | Z_504=V_502 | X1_511=V_502 | X2_500=V_502 | ~member(U_193, X2_500, W_192) | ~member(U_193, X1_511, W_192) | ~member(U_193, Z_504, W_192) | ~member(U_193, Y_513, W_192) | ~member(U_193, X_505, W_192) | ~member(U_193, V_502, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_756, plain, (![W_530, U_525, X2_524, Y_533, Z_194, V_199, V_522, X2_196, Z_527, X2_519, Z_520, X_528, W_192, X_523, X1_195, X_197, Y_198, V_529, X1_526, U_193, Y_521, X1_532]: (skf21(V_522, X_528, Y_533, Z_527, X1_532, X2_519, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_523 | skf21(V_522, X_528, Y_533, Z_527, X1_532, X2_519, W_192, U_193)=X_523 | X_523=W_530 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_530 | skf21(V_522, X_528, Y_533, Z_527, X1_532, X2_519, W_192, U_193)=W_530 | W_530=V_529 | X_523=V_529 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_529 | skf21(V_522, X_528, Y_533, Z_527, X1_532, X2_519, W_192, U_193)=V_529 | V_529=U_525 | W_530=U_525 | X_523=U_525 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_525 | skf21(V_522, X_528, Y_533, Z_527, X1_532, X2_519, W_192, U_193)=U_525 | ~member(U_193, X_523, W_192) | ~member(U_193, W_530, W_192) | ~member(U_193, V_529, W_192) | ~member(U_193, U_525, W_192) | skf21(U_525, V_529, W_530, X_523, Y_521, Z_520, X1_526, X2_524)!=X_523 | X2_519=X1_532 | Z_527=X1_532 | Z_527=X2_519 | Z_527=Y_533 | Y_533=X1_532 | Y_533=X2_519 | Y_533=X_528 | Z_527=X_528 | X_528=X1_532 | X_528=X2_519 | X_528=V_522 | Y_533=V_522 | Z_527=V_522 | X1_532=V_522 | X2_519=V_522 | ~member(U_193, X2_519, W_192) | ~member(U_193, X1_532, W_192) | ~member(U_193, Z_527, W_192) | ~member(U_193, Y_533, W_192) | ~member(U_193, X_528, W_192) | ~member(U_193, V_522, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_778, plain, (![X1_546, X1_536, Z_194, V_199, Y_547, X2_196, X_543, Z_538, X5_552, V_539, X_551, W_192, X2_541, X1_195, Y_553, X2_537, X_197, Y_198, U_544, Z_542, U_193, W_540, V_548]: (skf21(V_539, X_543, Y_547, Z_542, X1_546, X2_537, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_552 | skf21(V_539, X_543, Y_547, Z_542, X1_546, X2_537, W_192, U_193)=X5_552 | X5_552=W_540 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_540 | skf21(V_539, X_543, Y_547, Z_542, X1_546, X2_537, W_192, U_193)=W_540 | W_540=V_548 | X5_552=V_548 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_548 | skf21(V_539, X_543, Y_547, Z_542, X1_546, X2_537, W_192, U_193)=V_548 | V_548=U_544 | W_540=U_544 | X5_552=U_544 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_544 | skf21(V_539, X_543, Y_547, Z_542, X1_546, X2_537, W_192, U_193)=U_544 | ~member(U_193, X5_552, W_192) | ~member(U_193, W_540, W_192) | ~member(U_193, V_548, W_192) | ~member(U_193, U_544, W_192) | skf21(U_544, V_548, W_540, X_551, Y_553, Z_538, X1_536, X2_541)!=W_540 | X2_537=X1_546 | Z_542=X1_546 | Z_542=X2_537 | Z_542=Y_547 | Y_547=X1_546 | Y_547=X2_537 | Y_547=X_543 | Z_542=X_543 | X_543=X1_546 | X_543=X2_537 | X_543=V_539 | Y_547=V_539 | Z_542=V_539 | X1_546=V_539 | X2_537=V_539 | ~member(U_193, X2_537, W_192) | ~member(U_193, X1_546, W_192) | ~member(U_193, Z_542, W_192) | ~member(U_193, Y_547, W_192) | ~member(U_193, X_543, W_192) | ~member(U_193, V_539, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.32 tff(c_715, plain, (![V_496, X_206, X1_204, W_200, X1_492, V_208, W_495, X2_205, U_494, X_498, U_202, Y_207, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=Y_207 | Y_207=X_206 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_206 | X_206=W_200 | Y_207=W_200 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_202 | ~member(U_494, Y_207, W_495) | ~member(U_494, X_206, W_495) | ~member(U_494, W_200, W_495) | ~member(U_494, V_208, W_495) | ~member(U_494, U_202, W_495) | skf21(U_202, V_208, W_200, X_206, Y_207, skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494), X1_204, X2_205)!=skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494) | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.32 tff(c_714, plain, (![V_496, X2_171, X1_492, X6_164, V_174, W_495, U_167, Z_168, W_165, U_494, X_498, X5_163, X1_170, X7_169, X_172, Y_173, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X7_169 | X7_169=X6_164 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_167 | ~member(U_494, X7_169, W_495) | ~member(U_494, X6_164, W_495) | ~member(U_494, X5_163, W_495) | ~member(U_494, V_174, W_495) | ~member(U_494, U_167, W_495) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.32 tff(c_712, plain, (![V_496, U_130, X1_492, W_495, X1_132, V_136, Y_135, U_494, X_498, W_128, X2_133, Y_497, Z_131, X2_491, X_134, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=Y_135 | Y_135=X_134 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_134 | X_134=W_128 | Y_135=W_128 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_130 | ~member(U_494, Y_135, W_495) | ~member(U_494, X_134, W_495) | ~member(U_494, W_128, W_495) | ~member(U_494, V_136, W_495) | ~member(U_494, U_130, W_495) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.32 tff(c_713, plain, (![V_496, X6_151, X2_158, X1_492, Y_160, W_495, X1_157, X_159, W_152, U_494, V_161, X_498, X5_150, Y_497, X2_491, Z_493, Z_155, U_154]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_151 | X6_151=X5_150 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_154 | ~member(U_494, X6_151, W_495) | ~member(U_494, X5_150, W_495) | ~member(U_494, W_152, W_495) | ~member(U_494, V_161, W_495) | ~member(U_494, U_154, W_495) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.32 tff(c_711, plain, (![V_496, U_142, W_140, X1_492, X2_145, X5_138, W_495, Y_147, V_148, U_494, X_498, Z_143, X1_144, X_146, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_138 | X_146=X5_138 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_146 | X_146=W_140 | X5_138=W_140 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_142 | ~member(U_494, X5_138, W_495) | ~member(U_494, X_146, W_495) | ~member(U_494, W_140, W_495) | ~member(U_494, V_148, W_495) | ~member(U_494, U_142, W_495) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.33 tff(c_710, plain, (![Z_183, V_496, X8_190, X5_177, X1_492, W_495, X1_185, V_189, X_187, Y_188, U_494, U_181, X2_186, X7_184, X6_178, X_498, W_179, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X8_190 | X8_190=X7_184 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_181 | ~member(U_494, X8_190, W_495) | ~member(U_494, X7_184, W_495) | ~member(U_494, X6_178, W_495) | ~member(U_494, X5_177, W_495) | ~member(U_494, U_181, W_495) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 71.29/61.33 tff(c_136, plain, (![Z_194, V_199, X2_196, W_192, X1_195, X_197, Y_198, U_193]: (X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | member(U_193, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_192) | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 71.29/61.33 tff(c_134, plain, (![Z_183, X4_191, X8_190, X5_177, X3_180, X1_185, V_189, X_187, Y_188, X9_182, U_181, X2_186, X7_184, X6_178, W_179]: (X9_182=X8_190 | X8_190=X7_184 | X9_182=X7_184 | X7_184=X6_178 | X8_190=X6_178 | X9_182=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | X9_182=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | X9_182=U_181 | six(X3_180, X4_191) | ~member(X3_180, X9_182, X4_191) | ~member(X3_180, X8_190, X4_191) | ~member(X3_180, X7_184, X4_191) | ~member(X3_180, X6_178, X4_191) | ~member(X3_180, X5_177, X4_191) | ~member(X3_180, U_181, X4_191) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181))). % 71.29/61.33 tff(c_128, plain, (![U_142, W_140, X2_145, X5_138, Y_147, V_148, X3_141, Z_143, X4_149, X6_139, X1_144, X_146]: (X6_139=X5_138 | X_146=X5_138 | X_146=X6_139 | X_146=W_140 | X5_138=W_140 | X6_139=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | X6_139=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | X6_139=U_142 | six(X3_141, X4_149) | ~member(X3_141, X6_139, X4_149) | ~member(X3_141, X5_138, X4_149) | ~member(X3_141, X_146, X4_149) | ~member(X3_141, W_140, X4_149) | ~member(X3_141, V_148, X4_149) | ~member(X3_141, U_142, X4_149) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146))). % 71.29/61.33 tff(c_126, plain, (![U_130, X5_127, X1_132, V_136, Y_135, W_128, X3_129, X2_133, Z_131, X_134, X4_137]: (Y_135=X5_127 | Y_135=X_134 | X_134=X5_127 | X_134=W_128 | Y_135=W_128 | X5_127=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | X5_127=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | X5_127=U_130 | six(X3_129, X4_137) | ~member(X3_129, X5_127, X4_137) | ~member(X3_129, Y_135, X4_137) | ~member(X3_129, X_134, X4_137) | ~member(X3_129, W_128, X4_137) | ~member(X3_129, V_136, X4_137) | ~member(X3_129, U_130, X4_137) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135))). % 71.29/61.33 tff(c_130, plain, (![X4_162, X6_151, X2_158, Y_160, X1_157, X3_153, X_159, W_152, V_161, X5_150, X7_156, Z_155, U_154]: (X7_156=X6_151 | X6_151=X5_150 | X7_156=X5_150 | X5_150=W_152 | X6_151=W_152 | X7_156=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | X7_156=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | X7_156=U_154 | six(X3_153, X4_162) | ~member(X3_153, X7_156, X4_162) | ~member(X3_153, X6_151, X4_162) | ~member(X3_153, X5_150, X4_162) | ~member(X3_153, W_152, X4_162) | ~member(X3_153, V_161, X4_162) | ~member(X3_153, U_154, X4_162) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152))). % 71.29/61.33 tff(c_132, plain, (![X2_171, X6_164, V_174, U_167, Z_168, W_165, X5_163, X1_170, X7_169, X8_175, X_172, Y_173, X4_176, X3_166]: (X8_175=X7_169 | X7_169=X6_164 | X8_175=X6_164 | X6_164=X5_163 | X7_169=X5_163 | X8_175=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | X8_175=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | X8_175=U_167 | six(X3_166, X4_176) | ~member(X3_166, X8_175, X4_176) | ~member(X3_166, X7_169, X4_176) | ~member(X3_166, X6_164, X4_176) | ~member(X3_166, X5_163, X4_176) | ~member(X3_166, V_174, X4_176) | ~member(X3_166, U_167, X4_176) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174))). % 71.29/61.33 tff(c_138, plain, (![X3_201, X_206, X1_204, W_200, V_208, X2_205, X4_209, U_202, Y_207, Z_203]: (Z_203=Y_207 | Y_207=X_206 | Z_203=X_206 | X_206=W_200 | Y_207=W_200 | Z_203=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | Z_203=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | Z_203=U_202 | six(X3_201, X4_209) | ~member(X3_201, Z_203, X4_209) | ~member(X3_201, Y_207, X4_209) | ~member(X3_201, X_206, X4_209) | ~member(X3_201, W_200, X4_209) | ~member(X3_201, V_208, X4_209) | ~member(X3_201, U_202, X4_209) | skf21(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Z_203))). % 71.29/61.33 tff(c_124, plain, (![W_126, U_124, V_125]: (skf20(W_126, U_124)=V_125 | skf18(W_126, U_124)=V_125 | skf16(W_126, U_124)=V_125 | skf14(W_126, U_124)=V_125 | skf12(W_126, U_124)=V_125 | skf10(W_126, U_124)=V_125 | ~six(U_124, W_126) | ~member(U_124, V_125, W_126)))). % 71.29/61.33 tff(c_543, plain, (![U_223]: (~member(skc2, U_223, skc3) | ~cannon(skc2, U_223) | ~of(skc2, U_223, skc3)))). % 71.29/61.33 tff(c_541, plain, (skf14(skc3, skc2)!=skf10(skc3, skc2))). % 71.29/61.33 tff(c_122, plain, (![U_121, V_122, W_123]: (~agent(U_121, V_122, W_123) | ~patient(U_121, V_122, W_123) | ~nonreflexive(U_121, V_122)))). % 71.29/61.33 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf14(U_115, V_116)!=skf10(U_115, V_116)))). % 71.29/61.33 tff(c_536, plain, (skf20(skc3, skc2)!=skf10(skc3, skc2))). % 71.29/61.33 tff(c_531, plain, (skf16(skc3, skc2)!=skf10(skc3, skc2))). % 71.29/61.33 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf20(U_91, V_92)!=skf10(U_91, V_92)))). % 71.29/61.33 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf16(U_109, V_110)!=skf10(U_109, V_110)))). % 71.29/61.33 tff(c_522, plain, (skf14(skc3, skc2)!=skf12(skc3, skc2))). % 71.29/61.33 tff(c_526, plain, (act(skc2, skf10(skc3, skc2)))). % 71.29/61.33 tff(c_517, plain, (act(skc2, skf12(skc3, skc2)))). % 71.29/61.33 tff(c_513, plain, (action(skc2, skf10(skc3, skc2)))). % 71.29/61.33 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf14(U_117, V_118)!=skf12(U_117, V_118)))). % 71.29/61.33 tff(c_509, plain, (action(skc2, skf12(skc3, skc2)))). % 71.29/61.33 tff(c_505, plain, (shot(skc2, skf10(skc3, skc2)))). % 71.29/61.33 tff(c_497, plain, (shot(skc2, skf12(skc3, skc2)))). % 71.29/61.33 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf10(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 71.29/61.33 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf12(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 71.29/61.33 tff(c_489, plain, (skf18(skc3, skc2)!=skf16(skc3, skc2))). % 71.29/61.33 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf18(U_107, V_108)!=skf16(U_107, V_108)))). % 71.29/61.33 tff(c_484, plain, (skf16(skc3, skc2)!=skf12(skc3, skc2))). % 71.29/61.33 tff(c_463, plain, (skf18(skc3, skc2)!=skf10(skc3, skc2))). % 71.29/61.33 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf16(U_111, V_112)!=skf12(U_111, V_112)))). % 71.29/61.33 tff(c_479, plain, (act(skc2, skf16(skc3, skc2)))). % 71.29/61.33 tff(c_475, plain, (action(skc2, skf16(skc3, skc2)))). % 71.29/61.33 tff(c_471, plain, (shot(skc2, skf16(skc3, skc2)))). % 71.29/61.33 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf16(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 71.29/61.33 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf18(U_101, V_102)!=skf10(U_101, V_102)))). % 71.29/61.33 tff(c_441, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.33 tff(c_457, plain, (act(skc2, skf20(skc3, skc2)))). % 71.29/61.33 tff(c_453, plain, (action(skc2, skf20(skc3, skc2)))). % 71.29/61.33 tff(c_449, plain, (shot(skc2, skf20(skc3, skc2)))). % 71.29/61.33 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf20(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 71.29/61.33 tff(c_394, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 71.29/61.33 tff(c_359, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 71.29/61.33 tff(c_431, plain, (skf18(skc3, skc2)!=skf12(skc3, skc2))). % 71.29/61.33 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf18(U_103, V_104)!=skf12(U_103, V_104)))). % 71.29/61.33 tff(c_389, plain, (![U_365, V_366]: (artifact(U_365, V_366) | ~cannon(U_365, V_366)))). % 71.29/61.33 tff(c_421, plain, (~entity(skc2, skc3))). % 71.29/61.33 tff(c_369, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 71.29/61.33 tff(c_354, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 71.29/61.33 tff(c_415, plain, (skf20(skc3, skc2)!=skf16(skc3, skc2))). % 71.29/61.33 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf20(U_97, V_98)!=skf16(U_97, V_98)))). % 71.29/61.33 tff(c_410, plain, (act(skc2, skf14(skc3, skc2)))). % 71.29/61.33 tff(c_406, plain, (action(skc2, skf14(skc3, skc2)))). % 71.29/61.33 tff(c_402, plain, (shot(skc2, skf14(skc3, skc2)))). % 71.29/61.33 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf14(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 71.29/61.33 tff(c_374, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 71.29/61.33 tff(c_342, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 71.29/61.33 tff(c_384, plain, (~artifact(skc2, skc3))). % 71.29/61.33 tff(c_264, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.33 tff(c_379, plain, (skf20(skc3, skc2)!=skf14(skc3, skc2))). % 71.29/61.33 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf20(U_95, V_96)!=skf14(U_95, V_96)))). % 71.29/61.33 tff(c_294, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 71.29/61.33 tff(c_270, plain, (![U_317, V_318]: (~multiple(U_317, V_318) | ~entity(U_317, V_318)))). % 71.29/61.33 tff(c_364, plain, (skf20(skc3, skc2)!=skf12(skc3, skc2))). % 71.29/61.33 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf20(U_93, V_94)!=skf12(U_93, V_94)))). % 71.29/61.33 tff(c_305, plain, (![U_333, V_334]: (~multiple(U_333, V_334) | ~eventuality(U_333, V_334)))). % 71.29/61.33 tff(c_336, plain, (![U_341, V_342]: (~living(U_341, V_342) | ~artifact(U_341, V_342)))). % 71.29/61.33 tff(c_337, plain, (![U_341, V_342]: (~animate(U_341, V_342) | ~artifact(U_341, V_342)))). % 71.29/61.33 tff(c_348, plain, (skf16(skc3, skc2)!=skf14(skc3, skc2))). % 71.29/61.33 tff(c_328, plain, (skf20(skc3, skc2)!=skf18(skc3, skc2))). % 71.29/61.33 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf16(U_113, V_114)!=skf14(U_113, V_114)))). % 71.29/61.33 tff(c_248, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 71.29/61.33 tff(c_179, plain, (![U_250, V_251]: (instrumentality(U_250, V_251) | ~weapon(U_250, V_251)))). % 71.29/61.33 tff(c_212, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.33 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf20(U_99, V_100)!=skf18(U_99, V_100)))). % 71.29/61.33 tff(c_299, plain, (skf12(skc3, skc2)!=skf10(skc3, skc2))). % 71.29/61.34 tff(c_315, plain, (skf18(skc3, skc2)!=skf14(skc3, skc2))). % 71.29/61.34 tff(c_323, plain, (~act(skc2, skc3))). % 71.29/61.34 tff(c_319, plain, (~event(skc2, skc3))). % 71.29/61.34 tff(c_310, plain, (~eventuality(skc2, skc3))). % 71.29/61.34 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf18(U_105, V_106)!=skf14(U_105, V_106)))). % 71.29/61.34 tff(c_226, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 71.29/61.34 tff(c_173, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~eventuality(U_11, V_12)))). % 71.29/61.34 tff(c_200, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.34 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf12(U_119, V_120)!=skf10(U_119, V_120)))). % 71.29/61.34 tff(c_206, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 71.29/61.34 tff(c_195, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 71.29/61.34 tff(c_288, plain, (act(skc2, skf18(skc3, skc2)))). % 71.29/61.34 tff(c_284, plain, (action(skc2, skf18(skc3, skc2)))). % 71.29/61.34 tff(c_280, plain, (shot(skc2, skf18(skc3, skc2)))). % 71.29/61.34 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf18(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 71.29/61.34 tff(c_253, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 71.29/61.34 tff(c_258, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 71.29/61.34 tff(c_219, plain, (![U_280, V_281]: (singleton(U_280, V_281) | ~entity(U_280, V_281)))). % 71.29/61.34 tff(c_148, plain, (![U_210]: (shot(skc2, U_210) | ~member(skc2, U_210, skc3)))). % 71.29/61.34 tff(c_242, plain, (![U_302, V_303]: (~male(U_302, V_303) | ~object(U_302, V_303)))). % 71.29/61.34 tff(c_237, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.34 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 71.29/61.34 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 71.29/61.34 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 71.29/61.34 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 71.29/61.34 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 71.29/61.34 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 71.29/61.34 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 71.29/61.34 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 71.29/61.34 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 71.29/61.34 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 71.29/61.34 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 71.29/61.34 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 71.29/61.34 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 71.29/61.34 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 71.29/61.34 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 71.29/61.34 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 71.29/61.34 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 71.29/61.34 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 71.29/61.34 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 71.29/61.34 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 71.29/61.34 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 71.29/61.34 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 71.29/61.34 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 71.29/61.34 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 71.29/61.34 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 71.29/61.34 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 71.29/61.34 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 71.29/61.34 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 71.29/61.34 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 71.29/61.34 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 71.48/61.34 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 71.48/61.34 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 71.48/61.34 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 71.48/61.34 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 71.48/61.34 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 71.48/61.34 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 71.48/61.34 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 71.48/61.34 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 71.48/61.34 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 71.48/61.34 tff(c_146, plain, (group(skc2, skc3))). % 71.48/61.34 tff(c_142, plain, (male(skc2, skc3))). % 71.48/61.34 tff(c_144, plain, (six(skc2, skc3))). % 71.48/61.34 tff(c_140, plain, (actual_world(skc2))). % 71.48/61.34 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 71.48/61.34 %------------------------------------------------------------------------------