%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP071-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 : n011.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:06 PM UTC 2025 % Result : Satisfiable 74.51s 65.49s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP071-1 : TPTP v9.0.0. Released v2.4.0. % 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:23:18 EDT 2025 % 0.19/0.34 % CPUTime : % 74.51/65.49 % 74.51/65.49 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 74.51/65.49 % 74.51/65.49 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 74.51/65.50 %$ 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 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skf8 > skc7 > skc6 > skc5 > skc4 % 74.51/65.50 % 74.51/65.50 %Foreground sorts: % 74.51/65.50 % 74.51/65.50 % 74.51/65.50 %Background operators: % 74.51/65.50 % 74.51/65.50 % 74.51/65.50 %Foreground operators: % 74.51/65.50 tff(nonliving, type, nonliving: ($i * $i) > $o). % 74.51/65.50 tff(skf10, type, skf10: ($i * $i) > $i). % 74.51/65.50 tff(member, type, member: ($i * $i * $i) > $o). % 74.51/65.50 tff(skc7, type, skc7: $i). % 74.51/65.50 tff(living, type, living: ($i * $i) > $o). % 74.51/65.50 tff(fire, type, fire: ($i * $i) > $o). % 74.51/65.50 tff(human_person, type, human_person: ($i * $i) > $o). % 74.51/65.50 tff(action, type, action: ($i * $i) > $o). % 74.51/65.50 tff(present, type, present: ($i * $i) > $o). % 74.51/65.50 tff(shot, type, shot: ($i * $i) > $o). % 74.51/65.50 tff(entity, type, entity: ($i * $i) > $o). % 74.51/65.50 tff(eventuality, type, eventuality: ($i * $i) > $o). % 74.51/65.50 tff(weapon, type, weapon: ($i * $i) > $o). % 74.51/65.50 tff(existent, type, existent: ($i * $i) > $o). % 74.51/65.50 tff(singleton, type, singleton: ($i * $i) > $o). % 74.51/65.50 tff(male, type, male: ($i * $i) > $o). % 74.51/65.50 tff(skf8, type, skf8: $i > $i). % 74.51/65.50 tff(multiple, type, multiple: ($i * $i) > $o). % 74.51/65.50 tff(organism, type, organism: ($i * $i) > $o). % 74.51/65.50 tff(animate, type, animate: ($i * $i) > $o). % 74.51/65.50 tff(of, type, of: ($i * $i * $i) > $o). % 74.51/65.50 tff(skf14, type, skf14: ($i * $i) > $i). % 74.51/65.50 tff(actual_world, type, actual_world: $i > $o). % 74.51/65.50 tff(agent, type, agent: ($i * $i * $i) > $o). % 74.51/65.50 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 74.51/65.50 tff(group, type, group: ($i * $i) > $o). % 74.51/65.50 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 74.51/65.50 tff(artifact, type, artifact: ($i * $i) > $o). % 74.51/65.50 tff(cannon, type, cannon: ($i * $i) > $o). % 74.51/65.50 tff(event, type, event: ($i * $i) > $o). % 74.51/65.50 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 74.51/65.50 tff(patient, type, patient: ($i * $i * $i) > $o). % 74.51/65.50 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 74.51/65.50 tff(skc4, type, skc4: $i). % 74.51/65.50 tff(thing, type, thing: ($i * $i) > $o). % 74.51/65.50 tff(human, type, human: ($i * $i) > $o). % 74.51/65.50 tff(six, type, six: ($i * $i) > $o). % 74.51/65.50 tff(skf18, type, skf18: ($i * $i) > $i). % 74.51/65.50 tff(man, type, man: ($i * $i) > $o). % 74.51/65.50 tff(skc5, type, skc5: $i). % 74.51/65.50 tff(weaponry, type, weaponry: ($i * $i) > $o). % 74.51/65.50 tff(unisex, type, unisex: ($i * $i) > $o). % 74.51/65.50 tff(skf16, type, skf16: ($i * $i) > $i). % 74.51/65.50 tff(set, type, set: ($i * $i) > $o). % 74.51/65.50 tff(skf12, type, skf12: ($i * $i) > $i). % 74.51/65.50 tff(skc6, type, skc6: $i). % 74.51/65.50 tff(impartial, type, impartial: ($i * $i) > $o). % 74.51/65.50 tff(object, type, object: ($i * $i) > $o). % 74.51/65.50 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 74.51/65.50 tff(specific, type, specific: ($i * $i) > $o). % 74.51/65.50 tff(skf20, type, skf20: ($i * $i) > $i). % 74.51/65.50 tff(act, type, act: ($i * $i) > $o). % 74.51/65.50 % 74.51/65.50 %Saturated clause set: % 74.51/65.51 tff(c_1100, plain, (![X2_948, X_963, X_952, V_933, Y_954, X2_949, Z_194, V_199, V_945, X2_939, Z_936, X2_196, Z_958, X2_924, Y_941, V_928, X1_956, X1_934, V_961, Y_947, V_955, W_192, X1_951, X_950, X1_195, Y_938, Z_940, X1_931, W_962, X_930, Y_946, X_197, Y_198, X_953, X1_925, U_193, Z_942, Z_935, Z_929, X1_932, X2_926, X_960, V_959, X2_927, Y_957]: (skf21(V_959, X_930, Y_954, Z_936, X1_932, X2_939, W_192, U_193)=skf21(V_955, X_953, Y_941, Z_958, X1_934, X2_926, W_192, U_193) | skf21(V_959, X_930, Y_954, Z_936, X1_932, X2_939, W_192, U_193)=skf21(V_933, X_950, Y_946, Z_929, X1_925, X2_948, W_192, U_193) | skf21(V_955, X_953, Y_941, Z_958, X1_934, X2_926, W_192, U_193)=skf21(V_933, X_950, Y_946, Z_929, X1_925, X2_948, W_192, U_193) | skf21(V_933, X_950, Y_946, Z_929, X1_925, X2_948, W_192, U_193)=skf21(V_928, X_960, Y_938, Z_935, X1_951, X2_949, W_192, U_193) | skf21(V_959, X_930, Y_954, Z_936, X1_932, X2_939, W_192, U_193)=skf21(V_928, X_960, Y_938, Z_935, X1_951, X2_949, W_192, U_193) | skf21(V_955, X_953, Y_941, Z_958, X1_934, X2_926, W_192, U_193)=skf21(V_928, X_960, Y_938, Z_935, X1_951, X2_949, W_192, U_193) | skf21(V_945, X_963, Y_947, Z_942, X1_931, X2_927, W_192, U_193)=skf21(V_928, X_960, Y_938, Z_935, X1_951, X2_949, W_192, U_193) | skf21(V_945, X_963, Y_947, Z_942, X1_931, X2_927, W_192, U_193)=skf21(V_933, X_950, Y_946, Z_929, X1_925, X2_948, W_192, U_193) | skf21(V_959, X_930, Y_954, Z_936, X1_932, X2_939, W_192, U_193)=skf21(V_945, X_963, Y_947, Z_942, X1_931, X2_927, W_192, U_193) | skf21(V_955, X_953, Y_941, Z_958, X1_934, X2_926, W_192, U_193)=skf21(V_945, X_963, Y_947, Z_942, X1_931, X2_927, W_192, U_193) | skf21(V_945, X_963, Y_947, Z_942, X1_931, X2_927, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_928, X_960, Y_938, Z_935, X1_951, X2_949, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_933, X_950, Y_946, Z_929, X1_925, X2_948, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_959, X_930, Y_954, Z_936, X1_932, X2_939, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_955, X_953, Y_941, Z_958, X1_934, X2_926, 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_961, W_962, X_952, Y_957, Z_940, X1_956, X2_924)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_926=X1_934 | Z_958=X1_934 | Z_958=X2_926 | Z_958=Y_941 | Y_941=X1_934 | Y_941=X2_926 | Y_941=X_953 | Z_958=X_953 | X_953=X1_934 | X_953=X2_926 | X_953=V_955 | Y_941=V_955 | Z_958=V_955 | X1_934=V_955 | X2_926=V_955 | ~member(U_193, X2_926, W_192) | ~member(U_193, X1_934, W_192) | ~member(U_193, Z_958, W_192) | ~member(U_193, Y_941, W_192) | ~member(U_193, X_953, W_192) | ~member(U_193, V_955, W_192) | X2_939=X1_932 | Z_936=X1_932 | Z_936=X2_939 | Z_936=Y_954 | Y_954=X1_932 | Y_954=X2_939 | Y_954=X_930 | Z_936=X_930 | X_930=X1_932 | X_930=X2_939 | X_930=V_959 | Y_954=V_959 | Z_936=V_959 | X1_932=V_959 | X2_939=V_959 | ~member(U_193, X2_939, W_192) | ~member(U_193, X1_932, W_192) | ~member(U_193, Z_936, W_192) | ~member(U_193, Y_954, W_192) | ~member(U_193, X_930, W_192) | ~member(U_193, V_959, W_192) | X2_948=X1_925 | Z_929=X1_925 | Z_929=X2_948 | Z_929=Y_946 | Y_946=X1_925 | Y_946=X2_948 | Y_946=X_950 | Z_929=X_950 | X_950=X1_925 | X_950=X2_948 | X_950=V_933 | Y_946=V_933 | Z_929=V_933 | X1_925=V_933 | X2_948=V_933 | ~member(U_193, X2_948, W_192) | ~member(U_193, X1_925, W_192) | ~member(U_193, Z_929, W_192) | ~member(U_193, Y_946, W_192) | ~member(U_193, X_950, W_192) | ~member(U_193, V_933, W_192) | X2_949=X1_951 | Z_935=X1_951 | Z_935=X2_949 | Z_935=Y_938 | Y_938=X1_951 | Y_938=X2_949 | Y_938=X_960 | Z_935=X_960 | X_960=X1_951 | X_960=X2_949 | X_960=V_928 | Y_938=V_928 | Z_935=V_928 | X1_951=V_928 | X2_949=V_928 | ~member(U_193, X2_949, W_192) | ~member(U_193, X1_951, W_192) | ~member(U_193, Z_935, W_192) | ~member(U_193, Y_938, W_192) | ~member(U_193, X_960, W_192) | ~member(U_193, V_928, W_192) | X2_927=X1_931 | Z_942=X1_931 | Z_942=X2_927 | Z_942=Y_947 | Y_947=X1_931 | Y_947=X2_927 | Y_947=X_963 | Z_942=X_963 | X_963=X1_931 | X_963=X2_927 | X_963=V_945 | Y_947=V_945 | Z_942=V_945 | X1_931=V_945 | X2_927=V_945 | ~member(U_193, X2_927, W_192) | ~member(U_193, X1_931, W_192) | ~member(U_193, Z_942, W_192) | ~member(U_193, Y_947, W_192) | ~member(U_193, X_963, W_192) | ~member(U_193, V_945, 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)))). % 74.51/65.51 tff(c_1077, plain, (![X2_882, X_890, X_884, V_872, Z_194, V_199, X_873, X_865, X2_876, X2_196, V_871, Z_881, X1_889, Z_868, Y_867, V_886, Y_858, X2_877, Z_863, W_864, X1_878, X1_883, Y_860, W_192, Z_859, X1_861, X1_195, X1_862, X_197, Y_198, X2_857, V_888, Z_866, X2_880, U_885, U_193, Y_887, Y_874, X_879]: (skf21(V_888, X_873, Y_887, Z_881, X1_878, X2_876, W_192, U_193)=skf21(V_872, X_884, Y_867, Z_863, X1_862, X2_882, W_192, U_193) | skf21(V_886, X_865, Y_858, Z_859, X1_889, X2_880, W_192, U_193)=skf21(V_872, X_884, Y_867, Z_863, X1_862, X2_882, W_192, U_193) | skf21(V_888, X_873, Y_887, Z_881, X1_878, X2_876, W_192, U_193)=skf21(V_886, X_865, Y_858, Z_859, X1_889, X2_880, W_192, U_193) | skf21(V_886, X_865, Y_858, Z_859, X1_889, X2_880, W_192, U_193)=skf21(V_871, X_890, Y_874, Z_868, X1_861, X2_857, W_192, U_193) | skf21(V_872, X_884, Y_867, Z_863, X1_862, X2_882, W_192, U_193)=skf21(V_871, X_890, Y_874, Z_868, X1_861, X2_857, W_192, U_193) | skf21(V_888, X_873, Y_887, Z_881, X1_878, X2_876, W_192, U_193)=skf21(V_871, X_890, Y_874, Z_868, X1_861, X2_857, W_192, U_193) | skf21(V_871, X_890, Y_874, Z_868, X1_861, X2_857, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_886, X_865, Y_858, Z_859, X1_889, X2_880, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_872, X_884, Y_867, Z_863, X1_862, X2_882, 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_873, Y_887, Z_881, X1_878, X2_876, 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_885 | skf21(V_871, X_890, Y_874, Z_868, X1_861, X2_857, W_192, U_193)=U_885 | skf21(V_886, X_865, Y_858, Z_859, X1_889, X2_880, W_192, U_193)=U_885 | skf21(V_872, X_884, Y_867, Z_863, X1_862, X2_882, W_192, U_193)=U_885 | skf21(V_888, X_873, Y_887, Z_881, X1_878, X2_876, W_192, U_193)=U_885 | ~member(U_193, U_885, W_192) | skf21(U_885, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_864, X_879, Y_860, Z_866, X1_883, X2_877)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_876=X1_878 | Z_881=X1_878 | Z_881=X2_876 | Z_881=Y_887 | Y_887=X1_878 | Y_887=X2_876 | Y_887=X_873 | Z_881=X_873 | X_873=X1_878 | X_873=X2_876 | X_873=V_888 | Y_887=V_888 | Z_881=V_888 | X1_878=V_888 | X2_876=V_888 | ~member(U_193, X2_876, W_192) | ~member(U_193, X1_878, W_192) | ~member(U_193, Z_881, W_192) | ~member(U_193, Y_887, W_192) | ~member(U_193, X_873, W_192) | ~member(U_193, V_888, W_192) | X2_882=X1_862 | Z_863=X1_862 | Z_863=X2_882 | Z_863=Y_867 | Y_867=X1_862 | Y_867=X2_882 | Y_867=X_884 | Z_863=X_884 | X_884=X1_862 | X_884=X2_882 | X_884=V_872 | Y_867=V_872 | Z_863=V_872 | X1_862=V_872 | X2_882=V_872 | ~member(U_193, X2_882, W_192) | ~member(U_193, X1_862, W_192) | ~member(U_193, Z_863, W_192) | ~member(U_193, Y_867, W_192) | ~member(U_193, X_884, W_192) | ~member(U_193, V_872, W_192) | X2_880=X1_889 | Z_859=X1_889 | Z_859=X2_880 | Z_859=Y_858 | Y_858=X1_889 | Y_858=X2_880 | Y_858=X_865 | Z_859=X_865 | X_865=X1_889 | X_865=X2_880 | X_865=V_886 | Y_858=V_886 | Z_859=V_886 | X1_889=V_886 | X2_880=V_886 | ~member(U_193, X2_880, W_192) | ~member(U_193, X1_889, W_192) | ~member(U_193, Z_859, W_192) | ~member(U_193, Y_858, W_192) | ~member(U_193, X_865, W_192) | ~member(U_193, V_886, W_192) | X2_857=X1_861 | Z_868=X1_861 | Z_868=X2_857 | Z_868=Y_874 | Y_874=X1_861 | Y_874=X2_857 | Y_874=X_890 | Z_868=X_890 | X_890=X1_861 | X_890=X2_857 | X_890=V_871 | Y_874=V_871 | Z_868=V_871 | X1_861=V_871 | X2_857=V_871 | ~member(U_193, X2_857, W_192) | ~member(U_193, X1_861, W_192) | ~member(U_193, Z_868, W_192) | ~member(U_193, Y_874, W_192) | ~member(U_193, X_890, W_192) | ~member(U_193, V_871, 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)))). % 74.51/65.51 tff(c_1055, plain, (![X1_843, X1_830, X_836, Z_194, V_848, U_846, V_199, X1_847, Z_832, Z_851, X2_196, Z_852, X2_826, X2_855, X_856, X1_829, W_831, X1_834, Z_837, W_192, Y_844, V_824, X1_195, X2_827, X_828, X2_845, V_842, X_849, Y_825, V_841, X_197, Y_198, X_835, V_822, U_193, Z_850, X2_854, Y_833, Y_823, Y_853]: (skf21(V_824, X_835, Y_825, Z_852, X1_847, X2_854, W_192, U_193)=skf21(V_822, X_836, Y_823, Z_850, X1_843, X2_845, W_192, U_193) | skf21(V_848, X_849, Y_853, Z_832, X1_834, X2_855, W_192, U_193)=skf21(V_824, X_835, Y_825, Z_852, X1_847, X2_854, W_192, U_193) | skf21(V_848, X_849, Y_853, Z_832, X1_834, X2_855, W_192, U_193)=skf21(V_822, X_836, Y_823, Z_850, X1_843, X2_845, W_192, U_193) | skf21(V_848, X_849, Y_853, Z_832, X1_834, X2_855, W_192, U_193)=skf21(V_842, X_856, Y_844, Z_837, X1_830, X2_826, W_192, U_193) | skf21(V_842, X_856, Y_844, Z_837, X1_830, X2_826, W_192, U_193)=skf21(V_824, X_835, Y_825, Z_852, X1_847, X2_854, W_192, U_193) | skf21(V_842, X_856, Y_844, Z_837, X1_830, X2_826, W_192, U_193)=skf21(V_822, X_836, Y_823, Z_850, X1_843, X2_845, W_192, U_193) | skf21(V_842, X_856, Y_844, Z_837, X1_830, X2_826, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_848, X_849, Y_853, Z_832, X1_834, X2_855, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_824, X_835, Y_825, Z_852, X1_847, X2_854, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_822, X_836, Y_823, Z_850, X1_843, X2_845, 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_846 | skf21(V_842, X_856, Y_844, Z_837, X1_830, X2_826, W_192, U_193)=U_846 | skf21(V_848, X_849, Y_853, Z_832, X1_834, X2_855, W_192, U_193)=U_846 | skf21(V_824, X_835, Y_825, Z_852, X1_847, X2_854, W_192, U_193)=U_846 | skf21(V_822, X_836, Y_823, Z_850, X1_843, X2_845, W_192, U_193)=U_846 | ~member(U_193, U_846, W_192) | skf21(U_846, V_841, W_831, X_828, Y_833, Z_851, X1_829, X2_827)!=U_846 | X2_845=X1_843 | Z_850=X1_843 | Z_850=X2_845 | Z_850=Y_823 | Y_823=X1_843 | Y_823=X2_845 | Y_823=X_836 | Z_850=X_836 | X_836=X1_843 | X_836=X2_845 | X_836=V_822 | Y_823=V_822 | Z_850=V_822 | X1_843=V_822 | X2_845=V_822 | ~member(U_193, X2_845, W_192) | ~member(U_193, X1_843, W_192) | ~member(U_193, Z_850, W_192) | ~member(U_193, Y_823, W_192) | ~member(U_193, X_836, W_192) | ~member(U_193, V_822, W_192) | X2_854=X1_847 | Z_852=X1_847 | Z_852=X2_854 | Z_852=Y_825 | Y_825=X1_847 | Y_825=X2_854 | Y_825=X_835 | Z_852=X_835 | X_835=X1_847 | X_835=X2_854 | X_835=V_824 | Y_825=V_824 | Z_852=V_824 | X1_847=V_824 | X2_854=V_824 | ~member(U_193, X2_854, W_192) | ~member(U_193, X1_847, W_192) | ~member(U_193, Z_852, W_192) | ~member(U_193, Y_825, W_192) | ~member(U_193, X_835, W_192) | ~member(U_193, V_824, W_192) | X2_855=X1_834 | Z_832=X1_834 | Z_832=X2_855 | Z_832=Y_853 | Y_853=X1_834 | Y_853=X2_855 | Y_853=X_849 | Z_832=X_849 | X_849=X1_834 | X_849=X2_855 | X_849=V_848 | Y_853=V_848 | Z_832=V_848 | X1_834=V_848 | X2_855=V_848 | ~member(U_193, X2_855, W_192) | ~member(U_193, X1_834, W_192) | ~member(U_193, Z_832, W_192) | ~member(U_193, Y_853, W_192) | ~member(U_193, X_849, W_192) | ~member(U_193, V_848, W_192) | X2_826=X1_830 | Z_837=X1_830 | Z_837=X2_826 | Z_837=Y_844 | Y_844=X1_830 | Y_844=X2_826 | Y_844=X_856 | Z_837=X_856 | X_856=X1_830 | X_856=X2_826 | X_856=V_842 | Y_844=V_842 | Z_837=V_842 | X1_830=V_842 | X2_826=V_842 | ~member(U_193, X2_826, W_192) | ~member(U_193, X1_830, W_192) | ~member(U_193, Z_837, W_192) | ~member(U_193, Y_844, W_192) | ~member(U_193, X_856, W_192) | ~member(U_193, V_842, 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)))). % 74.66/65.52 tff(c_988, plain, (![X2_719, X2_708, X_735, Z_194, X1_730, V_199, X2_717, X2_196, V_718, Y_713, V_726, X2_710, Y_729, Z_734, V_715, U_720, Y_728, W_192, X_727, X1_195, Z_733, X_716, X1_721, Z_722, V_711, X_197, Y_198, X1_723, U_193, X_709, Z_732, Y_714, X1_712]: (skf21(V_718, X_727, Y_713, Z_733, X1_723, X2_719, W_192, U_193)=skf21(V_711, X_709, Y_714, Z_732, X1_730, X2_710, W_192, U_193) | skf21(V_726, X_735, Y_728, Z_722, X1_712, X2_708, W_192, U_193)=skf21(V_718, X_727, Y_713, Z_733, X1_723, X2_719, W_192, U_193) | skf21(V_726, X_735, Y_728, Z_722, X1_712, X2_708, W_192, U_193)=skf21(V_711, X_709, Y_714, Z_732, X1_730, X2_710, W_192, U_193) | skf21(V_726, X_735, Y_728, Z_722, X1_712, X2_708, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_718, X_727, Y_713, Z_733, X1_723, X2_719, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_711, X_709, Y_714, Z_732, X1_730, X2_710, 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_715 | skf21(V_726, X_735, Y_728, Z_722, X1_712, X2_708, W_192, U_193)=V_715 | skf21(V_718, X_727, Y_713, Z_733, X1_723, X2_719, W_192, U_193)=V_715 | skf21(V_711, X_709, Y_714, Z_732, X1_730, X2_710, W_192, U_193)=V_715 | V_715=U_720 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_720 | skf21(V_726, X_735, Y_728, Z_722, X1_712, X2_708, W_192, U_193)=U_720 | skf21(V_718, X_727, Y_713, Z_733, X1_723, X2_719, W_192, U_193)=U_720 | skf21(V_711, X_709, Y_714, Z_732, X1_730, X2_710, W_192, U_193)=U_720 | ~member(U_193, V_715, W_192) | ~member(U_193, U_720, W_192) | skf21(U_720, V_715, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_716, Y_729, Z_734, X1_721, X2_717)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_710=X1_730 | Z_732=X1_730 | Z_732=X2_710 | Z_732=Y_714 | Y_714=X1_730 | Y_714=X2_710 | Y_714=X_709 | Z_732=X_709 | X_709=X1_730 | X_709=X2_710 | X_709=V_711 | Y_714=V_711 | Z_732=V_711 | X1_730=V_711 | X2_710=V_711 | ~member(U_193, X2_710, W_192) | ~member(U_193, X1_730, W_192) | ~member(U_193, Z_732, W_192) | ~member(U_193, Y_714, W_192) | ~member(U_193, X_709, W_192) | ~member(U_193, V_711, W_192) | X2_719=X1_723 | Z_733=X1_723 | Z_733=X2_719 | Z_733=Y_713 | Y_713=X1_723 | Y_713=X2_719 | Y_713=X_727 | Z_733=X_727 | X_727=X1_723 | X_727=X2_719 | X_727=V_718 | Y_713=V_718 | Z_733=V_718 | X1_723=V_718 | X2_719=V_718 | ~member(U_193, X2_719, W_192) | ~member(U_193, X1_723, W_192) | ~member(U_193, Z_733, W_192) | ~member(U_193, Y_713, W_192) | ~member(U_193, X_727, W_192) | ~member(U_193, V_718, W_192) | X2_708=X1_712 | Z_722=X1_712 | Z_722=X2_708 | Z_722=Y_728 | Y_728=X1_712 | Y_728=X2_708 | Y_728=X_735 | Z_722=X_735 | X_735=X1_712 | X_735=X2_708 | X_735=V_726 | Y_728=V_726 | Z_722=V_726 | X1_712=V_726 | X2_708=V_726 | ~member(U_193, X2_708, W_192) | ~member(U_193, X1_712, W_192) | ~member(U_193, Z_722, W_192) | ~member(U_193, Y_728, W_192) | ~member(U_193, X_735, W_192) | ~member(U_193, V_726, 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)))). % 74.66/65.52 tff(c_1032, plain, (![V_779, X1_767, V_780, Z_772, X2_787, U_768, Z_194, V_199, X_775, X1_777, X2_196, Y_782, Z_773, Y_769, X_785, X2_792, X_794, W_192, Z_774, Y_791, X1_195, W_788, X_789, Z_784, X1_771, X2_793, X_197, Y_198, V_781, U_193, X1_783, Y_770, V_786, X2_766]: (skf21(V_786, X_775, Y_791, Z_773, X1_777, X2_793, W_192, U_193)=skf21(V_781, X_785, Y_770, Z_772, X1_783, X2_792, W_192, U_193) | skf21(V_786, X_775, Y_791, Z_773, X1_777, X2_793, W_192, U_193)=skf21(V_779, X_794, Y_782, Z_774, X1_767, X2_766, W_192, U_193) | skf21(V_781, X_785, Y_770, Z_772, X1_783, X2_792, W_192, U_193)=skf21(V_779, X_794, Y_782, Z_774, X1_767, X2_766, W_192, U_193) | skf21(V_779, X_794, Y_782, Z_774, X1_767, X2_766, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_786, X_775, Y_791, Z_773, X1_777, X2_793, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_781, X_785, Y_770, Z_772, X1_783, X2_792, 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_780 | skf21(V_779, X_794, Y_782, Z_774, X1_767, X2_766, W_192, U_193)=V_780 | skf21(V_786, X_775, Y_791, Z_773, X1_777, X2_793, W_192, U_193)=V_780 | skf21(V_781, X_785, Y_770, Z_772, X1_783, X2_792, W_192, U_193)=V_780 | V_780=U_768 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_768 | skf21(V_779, X_794, Y_782, Z_774, X1_767, X2_766, W_192, U_193)=U_768 | skf21(V_786, X_775, Y_791, Z_773, X1_777, X2_793, W_192, U_193)=U_768 | skf21(V_781, X_785, Y_770, Z_772, X1_783, X2_792, W_192, U_193)=U_768 | ~member(U_193, V_780, W_192) | ~member(U_193, U_768, W_192) | skf21(U_768, V_780, W_788, X_789, Y_769, Z_784, X1_771, X2_787)!=V_780 | X2_792=X1_783 | Z_772=X1_783 | Z_772=X2_792 | Z_772=Y_770 | Y_770=X1_783 | Y_770=X2_792 | Y_770=X_785 | Z_772=X_785 | X_785=X1_783 | X_785=X2_792 | X_785=V_781 | Y_770=V_781 | Z_772=V_781 | X1_783=V_781 | X2_792=V_781 | ~member(U_193, X2_792, W_192) | ~member(U_193, X1_783, W_192) | ~member(U_193, Z_772, W_192) | ~member(U_193, Y_770, W_192) | ~member(U_193, X_785, W_192) | ~member(U_193, V_781, W_192) | X2_793=X1_777 | Z_773=X1_777 | Z_773=X2_793 | Z_773=Y_791 | Y_791=X1_777 | Y_791=X2_793 | Y_791=X_775 | Z_773=X_775 | X_775=X1_777 | X_775=X2_793 | X_775=V_786 | Y_791=V_786 | Z_773=V_786 | X1_777=V_786 | X2_793=V_786 | ~member(U_193, X2_793, W_192) | ~member(U_193, X1_777, W_192) | ~member(U_193, Z_773, W_192) | ~member(U_193, Y_791, W_192) | ~member(U_193, X_775, W_192) | ~member(U_193, V_786, W_192) | X2_766=X1_767 | Z_774=X1_767 | Z_774=X2_766 | Z_774=Y_782 | Y_782=X1_767 | Y_782=X2_766 | Y_782=X_794 | Z_774=X_794 | X_794=X1_767 | X_794=X2_766 | X_794=V_779 | Y_782=V_779 | Z_774=V_779 | X1_767=V_779 | X2_766=V_779 | ~member(U_193, X2_766, W_192) | ~member(U_193, X1_767, W_192) | ~member(U_193, Z_774, W_192) | ~member(U_193, Y_782, W_192) | ~member(U_193, X_794, W_192) | ~member(U_193, V_779, 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)))). % 74.66/65.52 tff(c_1010, plain, (![Z_749, X1_756, X1_740, X1_742, Z_194, V_199, Y_759, Z_751, V_741, X2_196, X_760, Y_738, X5_746, X2_736, X_763, X2_747, W_192, Y_739, W_755, Y_757, Z_752, X1_195, V_744, U_758, X2_737, X2_745, V_754, X_197, Y_198, V_743, U_193, X_762, Z_764, X1_761, X_765]: (skf21(V_744, X_760, Y_759, Z_752, X1_756, X2_745, W_192, U_193)=skf21(V_741, X_763, Y_738, Z_751, X1_761, X2_747, W_192, U_193) | skf21(V_754, X_765, Y_757, Z_749, X1_742, X2_737, W_192, U_193)=skf21(V_741, X_763, Y_738, Z_751, X1_761, X2_747, W_192, U_193) | skf21(V_754, X_765, Y_757, Z_749, X1_742, X2_737, W_192, U_193)=skf21(V_744, X_760, Y_759, Z_752, X1_756, X2_745, W_192, U_193) | skf21(V_754, X_765, Y_757, Z_749, X1_742, X2_737, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_741, X_763, Y_738, Z_751, X1_761, X2_747, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_744, X_760, Y_759, Z_752, X1_756, X2_745, 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_746 | skf21(V_754, X_765, Y_757, Z_749, X1_742, X2_737, W_192, U_193)=X5_746 | skf21(V_741, X_763, Y_738, Z_751, X1_761, X2_747, W_192, U_193)=X5_746 | skf21(V_744, X_760, Y_759, Z_752, X1_756, X2_745, W_192, U_193)=X5_746 | X5_746=U_758 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_758 | skf21(V_754, X_765, Y_757, Z_749, X1_742, X2_737, W_192, U_193)=U_758 | skf21(V_741, X_763, Y_738, Z_751, X1_761, X2_747, W_192, U_193)=U_758 | skf21(V_744, X_760, Y_759, Z_752, X1_756, X2_745, W_192, U_193)=U_758 | ~member(U_193, X5_746, W_192) | ~member(U_193, U_758, W_192) | skf21(U_758, V_743, W_755, X_762, Y_739, Z_764, X1_740, X2_736)!=U_758 | X2_745=X1_756 | Z_752=X1_756 | Z_752=X2_745 | Z_752=Y_759 | Y_759=X1_756 | Y_759=X2_745 | Y_759=X_760 | Z_752=X_760 | X_760=X1_756 | X_760=X2_745 | X_760=V_744 | Y_759=V_744 | Z_752=V_744 | X1_756=V_744 | X2_745=V_744 | ~member(U_193, X2_745, W_192) | ~member(U_193, X1_756, W_192) | ~member(U_193, Z_752, W_192) | ~member(U_193, Y_759, W_192) | ~member(U_193, X_760, W_192) | ~member(U_193, V_744, W_192) | X2_747=X1_761 | Z_751=X1_761 | Z_751=X2_747 | Z_751=Y_738 | Y_738=X1_761 | Y_738=X2_747 | Y_738=X_763 | Z_751=X_763 | X_763=X1_761 | X_763=X2_747 | X_763=V_741 | Y_738=V_741 | Z_751=V_741 | X1_761=V_741 | X2_747=V_741 | ~member(U_193, X2_747, W_192) | ~member(U_193, X1_761, W_192) | ~member(U_193, Z_751, W_192) | ~member(U_193, Y_738, W_192) | ~member(U_193, X_763, W_192) | ~member(U_193, V_741, W_192) | X2_737=X1_742 | Z_749=X1_742 | Z_749=X2_737 | Z_749=Y_757 | Y_757=X1_742 | Y_757=X2_737 | Y_757=X_765 | Z_749=X_765 | X_765=X1_742 | X_765=X2_737 | X_765=V_754 | Y_757=V_754 | Z_749=V_754 | X1_742=V_754 | X2_737=V_754 | ~member(U_193, X2_737, W_192) | ~member(U_193, X1_742, W_192) | ~member(U_193, Z_749, W_192) | ~member(U_193, Y_757, W_192) | ~member(U_193, X_765, W_192) | ~member(U_193, V_754, 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)))). % 74.66/65.52 tff(c_899, plain, (![Y_598, X2_605, Z_194, V_199, X2_612, U_608, X2_196, Y_606, W_599, V_600, Y_611, X_614, X_593, W_192, X2_596, X1_594, X1_607, Z_609, X1_195, V_610, V_604, X_197, Y_198, Z_595, U_193, Z_601, X1_597]: (skf21(V_604, X_614, Y_606, Z_601, X1_597, X2_596, W_192, U_193)=skf21(V_600, X_593, Y_611, Z_609, X1_607, X2_612, W_192, U_193) | skf21(V_604, X_614, Y_606, Z_601, X1_597, X2_596, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_600, X_593, Y_611, Z_609, X1_607, X2_612, 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_599 | skf21(V_604, X_614, Y_606, Z_601, X1_597, X2_596, W_192, U_193)=W_599 | skf21(V_600, X_593, Y_611, Z_609, X1_607, X2_612, W_192, U_193)=W_599 | W_599=V_610 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_610 | skf21(V_604, X_614, Y_606, Z_601, X1_597, X2_596, W_192, U_193)=V_610 | skf21(V_600, X_593, Y_611, Z_609, X1_607, X2_612, W_192, U_193)=V_610 | V_610=U_608 | W_599=U_608 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_608 | skf21(V_604, X_614, Y_606, Z_601, X1_597, X2_596, W_192, U_193)=U_608 | skf21(V_600, X_593, Y_611, Z_609, X1_607, X2_612, W_192, U_193)=U_608 | ~member(U_193, W_599, W_192) | ~member(U_193, V_610, W_192) | ~member(U_193, U_608, W_192) | skf21(U_608, V_610, W_599, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_598, Z_595, X1_594, X2_605)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_612=X1_607 | Z_609=X1_607 | Z_609=X2_612 | Z_609=Y_611 | Y_611=X1_607 | Y_611=X2_612 | Y_611=X_593 | Z_609=X_593 | X_593=X1_607 | X_593=X2_612 | X_593=V_600 | Y_611=V_600 | Z_609=V_600 | X1_607=V_600 | X2_612=V_600 | ~member(U_193, X2_612, W_192) | ~member(U_193, X1_607, W_192) | ~member(U_193, Z_609, W_192) | ~member(U_193, Y_611, W_192) | ~member(U_193, X_593, W_192) | ~member(U_193, V_600, W_192) | X2_596=X1_597 | Z_601=X1_597 | Z_601=X2_596 | Z_601=Y_606 | Y_606=X1_597 | Y_606=X2_596 | Y_606=X_614 | Z_601=X_614 | X_614=X1_597 | X_614=X2_596 | X_614=V_604 | Y_606=V_604 | Z_601=V_604 | X1_597=V_604 | X2_596=V_604 | ~member(U_193, X2_596, W_192) | ~member(U_193, X1_597, W_192) | ~member(U_193, Z_601, W_192) | ~member(U_193, Y_606, W_192) | ~member(U_193, X_614, W_192) | ~member(U_193, V_604, 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)))). % 74.66/65.52 tff(c_943, plain, (![Z_194, V_199, X2_196, Y_657, U_659, X_640, V_655, V_644, X2_650, V_652, X2_656, Z_651, W_661, X_663, W_192, Z_646, X1_195, X_647, X2_641, X_197, Y_198, X1_645, Y_648, X5_658, U_193, Y_643, X1_662, Z_649, X1_660]: (skf21(V_655, X_663, Y_657, Z_651, X1_645, X2_641, W_192, U_193)=skf21(V_652, X_640, Y_643, Z_649, X1_662, X2_650, W_192, U_193) | skf21(V_655, X_663, Y_657, Z_651, X1_645, X2_641, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_652, X_640, Y_643, Z_649, X1_662, X2_650, 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_658 | skf21(V_655, X_663, Y_657, Z_651, X1_645, X2_641, W_192, U_193)=X5_658 | skf21(V_652, X_640, Y_643, Z_649, X1_662, X2_650, W_192, U_193)=X5_658 | X5_658=V_644 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_644 | skf21(V_655, X_663, Y_657, Z_651, X1_645, X2_641, W_192, U_193)=V_644 | skf21(V_652, X_640, Y_643, Z_649, X1_662, X2_650, W_192, U_193)=V_644 | V_644=U_659 | X5_658=U_659 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_659 | skf21(V_655, X_663, Y_657, Z_651, X1_645, X2_641, W_192, U_193)=U_659 | skf21(V_652, X_640, Y_643, Z_649, X1_662, X2_650, W_192, U_193)=U_659 | ~member(U_193, X5_658, W_192) | ~member(U_193, V_644, W_192) | ~member(U_193, U_659, W_192) | skf21(U_659, V_644, W_661, X_647, Y_648, Z_646, X1_660, X2_656)!=V_644 | X2_650=X1_662 | Z_649=X1_662 | Z_649=X2_650 | Z_649=Y_643 | Y_643=X1_662 | Y_643=X2_650 | Y_643=X_640 | Z_649=X_640 | X_640=X1_662 | X_640=X2_650 | X_640=V_652 | Y_643=V_652 | Z_649=V_652 | X1_662=V_652 | X2_650=V_652 | ~member(U_193, X2_650, W_192) | ~member(U_193, X1_662, W_192) | ~member(U_193, Z_649, W_192) | ~member(U_193, Y_643, W_192) | ~member(U_193, X_640, W_192) | ~member(U_193, V_652, W_192) | X2_641=X1_645 | Z_651=X1_645 | Z_651=X2_641 | Z_651=Y_657 | Y_657=X1_645 | Y_657=X2_641 | Y_657=X_663 | Z_651=X_663 | X_663=X1_645 | X_663=X2_641 | X_663=V_655 | Y_657=V_655 | Z_651=V_655 | X1_645=V_655 | X2_641=V_655 | ~member(U_193, X2_641, W_192) | ~member(U_193, X1_645, W_192) | ~member(U_193, Z_651, W_192) | ~member(U_193, Y_657, W_192) | ~member(U_193, X_663, W_192) | ~member(U_193, V_655, 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)))). % 74.66/65.52 tff(c_921, plain, (![V_623, Z_626, X6_633, X_639, X2_616, Z_194, V_199, U_634, X2_196, X2_635, Z_636, Z_617, X2_618, Y_615, Y_621, X1_624, W_192, X1_195, X_197, Y_198, X1_619, X5_622, U_193, X1_637, W_625, X_620, V_631, X_638, Y_632, V_627]: (skf21(V_631, X_639, Y_632, Z_626, X1_619, X2_616, W_192, U_193)=skf21(V_623, X_638, Y_621, Z_617, X1_637, X2_618, W_192, U_193) | skf21(V_631, X_639, Y_632, Z_626, X1_619, X2_616, 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_638, Y_621, Z_617, X1_637, X2_618, 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_633 | skf21(V_631, X_639, Y_632, Z_626, X1_619, X2_616, W_192, U_193)=X6_633 | skf21(V_623, X_638, Y_621, Z_617, X1_637, X2_618, W_192, U_193)=X6_633 | X6_633=X5_622 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_622 | skf21(V_631, X_639, Y_632, Z_626, X1_619, X2_616, W_192, U_193)=X5_622 | skf21(V_623, X_638, Y_621, Z_617, X1_637, X2_618, W_192, U_193)=X5_622 | X5_622=U_634 | X6_633=U_634 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_634 | skf21(V_631, X_639, Y_632, Z_626, X1_619, X2_616, W_192, U_193)=U_634 | skf21(V_623, X_638, Y_621, Z_617, X1_637, X2_618, W_192, U_193)=U_634 | ~member(U_193, X6_633, W_192) | ~member(U_193, X5_622, W_192) | ~member(U_193, U_634, W_192) | skf21(U_634, V_627, W_625, X_620, Y_615, Z_636, X1_624, X2_635)!=U_634 | X2_618=X1_637 | Z_617=X1_637 | Z_617=X2_618 | Z_617=Y_621 | Y_621=X1_637 | Y_621=X2_618 | Y_621=X_638 | Z_617=X_638 | X_638=X1_637 | X_638=X2_618 | X_638=V_623 | Y_621=V_623 | Z_617=V_623 | X1_637=V_623 | X2_618=V_623 | ~member(U_193, X2_618, W_192) | ~member(U_193, X1_637, W_192) | ~member(U_193, Z_617, W_192) | ~member(U_193, Y_621, W_192) | ~member(U_193, X_638, W_192) | ~member(U_193, V_623, W_192) | X2_616=X1_619 | Z_626=X1_619 | Z_626=X2_616 | Z_626=Y_632 | Y_632=X1_619 | Y_632=X2_616 | Y_632=X_639 | Z_626=X_639 | X_639=X1_619 | X_639=X2_616 | X_639=V_631 | Y_632=V_631 | Z_626=V_631 | X1_619=V_631 | X2_616=V_631 | ~member(U_193, X2_616, W_192) | ~member(U_193, X1_619, W_192) | ~member(U_193, Z_626, W_192) | ~member(U_193, Y_632, W_192) | ~member(U_193, X_639, W_192) | ~member(U_193, V_631, 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)))). % 74.66/65.52 tff(c_965, plain, (![X1_683, Z_194, V_199, X_670, X_668, V_664, Y_684, Z_678, X2_196, Y_674, V_676, X2_665, X2_673, W_671, W_192, X1_667, X1_195, V_681, Y_682, Z_685, U_672, X_197, Y_198, X1_677, U_193, X2_675, X_686, Z_666]: (skf21(V_681, X_686, Y_682, Z_678, X1_667, X2_665, W_192, U_193)=skf21(V_676, X_670, Y_674, Z_666, X1_683, X2_675, W_192, U_193) | skf21(V_681, X_686, Y_682, Z_678, X1_667, X2_665, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_676, X_670, Y_674, Z_666, X1_683, X2_675, 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_671 | skf21(V_681, X_686, Y_682, Z_678, X1_667, X2_665, W_192, U_193)=W_671 | skf21(V_676, X_670, Y_674, Z_666, X1_683, X2_675, W_192, U_193)=W_671 | W_671=V_664 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_664 | skf21(V_681, X_686, Y_682, Z_678, X1_667, X2_665, W_192, U_193)=V_664 | skf21(V_676, X_670, Y_674, Z_666, X1_683, X2_675, W_192, U_193)=V_664 | V_664=U_672 | W_671=U_672 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_672 | skf21(V_681, X_686, Y_682, Z_678, X1_667, X2_665, W_192, U_193)=U_672 | skf21(V_676, X_670, Y_674, Z_666, X1_683, X2_675, W_192, U_193)=U_672 | ~member(U_193, W_671, W_192) | ~member(U_193, V_664, W_192) | ~member(U_193, U_672, W_192) | skf21(U_672, V_664, W_671, X_668, Y_684, Z_685, X1_677, X2_673)!=W_671 | X2_675=X1_683 | Z_666=X1_683 | Z_666=X2_675 | Z_666=Y_674 | Y_674=X1_683 | Y_674=X2_675 | Y_674=X_670 | Z_666=X_670 | X_670=X1_683 | X_670=X2_675 | X_670=V_676 | Y_674=V_676 | Z_666=V_676 | X1_683=V_676 | X2_675=V_676 | ~member(U_193, X2_675, W_192) | ~member(U_193, X1_683, W_192) | ~member(U_193, Z_666, W_192) | ~member(U_193, Y_674, W_192) | ~member(U_193, X_670, W_192) | ~member(U_193, V_676, W_192) | X2_665=X1_667 | Z_678=X1_667 | Z_678=X2_665 | Z_678=Y_682 | Y_682=X1_667 | Y_682=X2_665 | Y_682=X_686 | Z_678=X_686 | X_686=X1_667 | X_686=X2_665 | X_686=V_681 | Y_682=V_681 | Z_678=V_681 | X1_667=V_681 | X2_665=V_681 | ~member(U_193, X2_665, W_192) | ~member(U_193, X1_667, W_192) | ~member(U_193, Z_678, W_192) | ~member(U_193, Y_682, W_192) | ~member(U_193, X_686, W_192) | ~member(U_193, V_681, 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)))). % 74.66/65.52 tff(c_788, plain, (![Z_488, X1_500, Z_194, V_199, W_494, X2_196, X_497, X2_489, V_503, Y_490, X_492, W_192, X1_195, Z_501, X2_495, V_502, X_197, Y_198, X1_499, U_193, U_493]: (skf21(V_502, X_497, Y_490, Z_488, X1_499, X2_495, 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_492 | skf21(V_502, X_497, Y_490, Z_488, X1_499, X2_495, W_192, U_193)=X_492 | X_492=W_494 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_494 | skf21(V_502, X_497, Y_490, Z_488, X1_499, X2_495, W_192, U_193)=W_494 | W_494=V_503 | X_492=V_503 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_503 | skf21(V_502, X_497, Y_490, Z_488, X1_499, X2_495, W_192, U_193)=V_503 | V_503=U_493 | W_494=U_493 | X_492=U_493 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_493 | skf21(V_502, X_497, Y_490, Z_488, X1_499, X2_495, W_192, U_193)=U_493 | ~member(U_193, X_492, W_192) | ~member(U_193, W_494, W_192) | ~member(U_193, V_503, W_192) | ~member(U_193, U_493, W_192) | skf21(U_493, V_503, W_494, X_492, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_501, X1_500, X2_489)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_495=X1_499 | Z_488=X1_499 | Z_488=X2_495 | Z_488=Y_490 | Y_490=X1_499 | Y_490=X2_495 | Y_490=X_497 | Z_488=X_497 | X_497=X1_499 | X_497=X2_495 | X_497=V_502 | Y_490=V_502 | Z_488=V_502 | X1_499=V_502 | X2_495=V_502 | ~member(U_193, X2_495, W_192) | ~member(U_193, X1_499, W_192) | ~member(U_193, Z_488, W_192) | ~member(U_193, Y_490, W_192) | ~member(U_193, X_497, 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)))). % 74.66/65.52 tff(c_810, plain, (![X5_520, Z_194, V_199, X_513, X2_196, Z_505, V_517, X2_509, X2_511, Y_506, W_510, W_192, X1_516, X1_195, U_512, X_197, Y_198, X1_504, U_193, V_518, Y_521, X_519, Z_507]: (skf21(V_518, X_513, Y_506, Z_505, X1_516, X2_509, 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_520 | skf21(V_518, X_513, Y_506, Z_505, X1_516, X2_509, W_192, U_193)=X5_520 | X5_520=W_510 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_510 | skf21(V_518, X_513, Y_506, Z_505, X1_516, X2_509, W_192, U_193)=W_510 | W_510=V_517 | X5_520=V_517 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_517 | skf21(V_518, X_513, Y_506, Z_505, X1_516, X2_509, W_192, U_193)=V_517 | V_517=U_512 | W_510=U_512 | X5_520=U_512 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_512 | skf21(V_518, X_513, Y_506, Z_505, X1_516, X2_509, W_192, U_193)=U_512 | ~member(U_193, X5_520, W_192) | ~member(U_193, W_510, W_192) | ~member(U_193, V_517, W_192) | ~member(U_193, U_512, W_192) | skf21(U_512, V_517, W_510, X_519, Y_521, Z_507, X1_504, X2_511)!=W_510 | X2_509=X1_516 | Z_505=X1_516 | Z_505=X2_509 | Z_505=Y_506 | Y_506=X1_516 | Y_506=X2_509 | Y_506=X_513 | Z_505=X_513 | X_513=X1_516 | X_513=X2_509 | X_513=V_518 | Y_506=V_518 | Z_505=V_518 | X1_516=V_518 | X2_509=V_518 | ~member(U_193, X2_509, W_192) | ~member(U_193, X1_516, W_192) | ~member(U_193, Z_505, W_192) | ~member(U_193, Y_506, W_192) | ~member(U_193, X_513, W_192) | ~member(U_193, V_518, 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)))). % 74.66/65.52 tff(c_854, plain, (![Z_543, Z_194, V_199, X1_560, X2_196, U_557, Y_545, V_556, X_550, X1_555, X5_548, X2_542, X2_547, W_192, X1_195, Y_559, X_552, X_197, V_549, Y_198, X6_544, U_193, Z_554, W_551]: (skf21(V_556, X_552, Y_545, Z_543, X1_555, X2_547, 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_544 | skf21(V_556, X_552, Y_545, Z_543, X1_555, X2_547, W_192, U_193)=X6_544 | X6_544=X5_548 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_548 | skf21(V_556, X_552, Y_545, Z_543, X1_555, X2_547, W_192, U_193)=X5_548 | X5_548=V_549 | X6_544=V_549 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_549 | skf21(V_556, X_552, Y_545, Z_543, X1_555, X2_547, W_192, U_193)=V_549 | V_549=U_557 | X5_548=U_557 | X6_544=U_557 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_557 | skf21(V_556, X_552, Y_545, Z_543, X1_555, X2_547, W_192, U_193)=U_557 | ~member(U_193, X6_544, W_192) | ~member(U_193, X5_548, W_192) | ~member(U_193, V_549, W_192) | ~member(U_193, U_557, W_192) | skf21(U_557, V_549, W_551, X_550, Y_559, Z_554, X1_560, X2_542)!=V_549 | X2_547=X1_555 | Z_543=X1_555 | Z_543=X2_547 | Z_543=Y_545 | Y_545=X1_555 | Y_545=X2_547 | Y_545=X_552 | Z_543=X_552 | X_552=X1_555 | X_552=X2_547 | X_552=V_556 | Y_545=V_556 | Z_543=V_556 | X1_555=V_556 | X2_547=V_556 | ~member(U_193, X2_547, W_192) | ~member(U_193, X1_555, W_192) | ~member(U_193, Z_543, W_192) | ~member(U_193, Y_545, W_192) | ~member(U_193, X_552, 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)))). % 74.66/65.52 tff(c_832, plain, (![Y_524, Y_535, X1_536, Z_194, V_199, Z_533, X2_196, X7_522, V_532, W_192, X5_540, X1_195, Z_523, X_530, W_526, X_529, V_538, X1_537, X_197, Y_198, X2_528, U_193, U_541, X6_539, X2_531]: (skf21(V_538, X_530, Y_524, Z_523, X1_536, X2_528, 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_522 | skf21(V_538, X_530, Y_524, Z_523, X1_536, X2_528, W_192, U_193)=X7_522 | X7_522=X6_539 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_539 | skf21(V_538, X_530, Y_524, Z_523, X1_536, X2_528, W_192, U_193)=X6_539 | X6_539=X5_540 | X7_522=X5_540 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_540 | skf21(V_538, X_530, Y_524, Z_523, X1_536, X2_528, W_192, U_193)=X5_540 | X5_540=U_541 | X6_539=U_541 | X7_522=U_541 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_541 | skf21(V_538, X_530, Y_524, Z_523, X1_536, X2_528, W_192, U_193)=U_541 | ~member(U_193, X7_522, W_192) | ~member(U_193, X6_539, W_192) | ~member(U_193, X5_540, W_192) | ~member(U_193, U_541, W_192) | skf21(U_541, V_532, W_526, X_529, Y_535, Z_533, X1_537, X2_531)!=U_541 | X2_528=X1_536 | Z_523=X1_536 | Z_523=X2_528 | Z_523=Y_524 | Y_524=X1_536 | Y_524=X2_528 | Y_524=X_530 | Z_523=X_530 | X_530=X1_536 | X_530=X2_528 | X_530=V_538 | Y_524=V_538 | Z_523=V_538 | X1_536=V_538 | X2_528=V_538 | ~member(U_193, X2_528, W_192) | ~member(U_193, X1_536, W_192) | ~member(U_193, Z_523, W_192) | ~member(U_193, Y_524, W_192) | ~member(U_193, X_530, W_192) | ~member(U_193, V_538, 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)))). % 74.66/65.53 tff(c_876, plain, (![X2_567, Y_562, V_577, Z_194, V_199, V_571, X1_576, X2_196, U_568, Z_563, X1_570, W_192, X2_569, X_573, X1_195, W_572, X_566, X_197, Y_198, Z_561, U_193, Y_565]: (skf21(V_577, X_573, Y_562, Z_561, X1_576, X2_569, 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_566 | skf21(V_577, X_573, Y_562, Z_561, X1_576, X2_569, W_192, U_193)=X_566 | X_566=W_572 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_572 | skf21(V_577, X_573, Y_562, Z_561, X1_576, X2_569, W_192, U_193)=W_572 | W_572=V_571 | X_566=V_571 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_571 | skf21(V_577, X_573, Y_562, Z_561, X1_576, X2_569, W_192, U_193)=V_571 | V_571=U_568 | W_572=U_568 | X_566=U_568 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_568 | skf21(V_577, X_573, Y_562, Z_561, X1_576, X2_569, W_192, U_193)=U_568 | ~member(U_193, X_566, W_192) | ~member(U_193, W_572, W_192) | ~member(U_193, V_571, W_192) | ~member(U_193, U_568, W_192) | skf21(U_568, V_571, W_572, X_566, Y_565, Z_563, X1_570, X2_567)!=X_566 | X2_569=X1_576 | Z_561=X1_576 | Z_561=X2_569 | Z_561=Y_562 | Y_562=X1_576 | Y_562=X2_569 | Y_562=X_573 | Z_561=X_573 | X_573=X1_576 | X_573=X2_569 | X_573=V_577 | Y_562=V_577 | Z_561=V_577 | X1_576=V_577 | X2_569=V_577 | ~member(U_193, X2_569, W_192) | ~member(U_193, X1_576, W_192) | ~member(U_193, Z_561, W_192) | ~member(U_193, Y_562, W_192) | ~member(U_193, X_573, W_192) | ~member(U_193, V_577, 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)))). % 74.66/65.53 tff(c_766, plain, (![X_206, X1_204, W_200, V_208, X1_481, W_484, X2_205, X_487, U_202, Y_207, U_483, Y_486, Z_482, X2_480, V_485]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=Y_207 | Y_207=X_206 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X_206 | X_206=W_200 | Y_207=W_200 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_202 | ~member(U_483, Y_207, W_484) | ~member(U_483, X_206, W_484) | ~member(U_483, W_200, W_484) | ~member(U_483, V_208, W_484) | ~member(U_483, U_202, W_484) | skf21(U_202, V_208, W_200, X_206, Y_207, skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483), X1_204, X2_205)!=skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483) | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 tff(c_769, plain, (![U_142, W_140, X1_481, X2_145, W_484, X5_138, Y_147, V_148, X_487, U_483, Z_143, Y_486, X1_144, X_146, Z_482, X2_480, V_485]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X5_138 | X_146=X5_138 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X_146 | X_146=W_140 | X5_138=W_140 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_142 | ~member(U_483, X5_138, W_484) | ~member(U_483, X_146, W_484) | ~member(U_483, W_140, W_484) | ~member(U_483, V_148, W_484) | ~member(U_483, U_142, W_484) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 tff(c_768, plain, (![X2_171, X6_164, X1_481, V_174, W_484, U_167, Z_168, W_165, X_487, X5_163, X1_170, X7_169, U_483, Y_486, X_172, Y_173, Z_482, X2_480, V_485]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X7_169 | X7_169=X6_164 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_167 | ~member(U_483, X7_169, W_484) | ~member(U_483, X6_164, W_484) | ~member(U_483, X5_163, W_484) | ~member(U_483, V_174, W_484) | ~member(U_483, U_167, W_484) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 tff(c_767, plain, (![Z_183, X8_190, X5_177, X1_481, W_484, X1_185, V_189, X_187, Y_188, U_181, X2_186, X7_184, X6_178, X_487, U_483, W_179, Y_486, Z_482, X2_480, V_485]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X8_190 | X8_190=X7_184 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_181 | ~member(U_483, X8_190, W_484) | ~member(U_483, X7_184, W_484) | ~member(U_483, X6_178, W_484) | ~member(U_483, X5_177, W_484) | ~member(U_483, U_181, W_484) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 tff(c_765, plain, (![X6_151, X2_158, X1_481, W_484, Y_160, X1_157, X_159, W_152, V_161, X_487, U_483, Y_486, X5_150, Z_482, X2_480, V_485, Z_155, U_154]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X6_151 | X6_151=X5_150 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_154 | ~member(U_483, X6_151, W_484) | ~member(U_483, X5_150, W_484) | ~member(U_483, W_152, W_484) | ~member(U_483, V_161, W_484) | ~member(U_483, U_154, W_484) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 tff(c_764, plain, (![U_130, X1_481, W_484, X1_132, V_136, Y_135, X_487, W_128, U_483, X2_133, Y_486, Z_131, Z_482, X2_480, X_134, V_485]: (skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=Y_135 | Y_135=X_134 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=X_134 | X_134=W_128 | Y_135=W_128 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf21(V_485, X_487, Y_486, Z_482, X1_481, X2_480, W_484, U_483)=U_130 | ~member(U_483, Y_135, W_484) | ~member(U_483, X_134, W_484) | ~member(U_483, W_128, W_484) | ~member(U_483, V_136, W_484) | ~member(U_483, U_130, W_484) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_480=X1_481 | Z_482=X1_481 | Z_482=X2_480 | Z_482=Y_486 | Y_486=X1_481 | Y_486=X2_480 | Y_486=X_487 | Z_482=X_487 | X_487=X1_481 | X_487=X2_480 | X_487=V_485 | Y_486=V_485 | Z_482=V_485 | X1_481=V_485 | X2_480=V_485 | six(U_483, W_484) | ~member(U_483, X2_480, W_484) | ~member(U_483, X1_481, W_484) | ~member(U_483, Z_482, W_484) | ~member(U_483, Y_486, W_484) | ~member(U_483, X_487, W_484) | ~member(U_483, V_485, W_484)))). % 74.66/65.53 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)))). % 74.66/65.53 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))). % 74.66/65.53 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))). % 74.66/65.53 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))). % 74.66/65.53 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))). % 74.66/65.53 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))). % 74.66/65.53 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))). % 74.66/65.53 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)))). % 74.66/65.53 tff(c_597, plain, (![U_215]: (~of(skc4, U_215, skc6) | ~cannon(skc4, U_215) | ~member(skc4, U_215, skc5)))). % 74.66/65.53 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)))). % 74.66/65.53 tff(c_595, plain, (skf20(skc5, skc4)!=skf18(skc5, skc4))). % 74.66/65.53 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf20(U_99, V_100)!=skf18(U_99, V_100)))). % 74.66/65.53 tff(c_590, plain, (skf18(skc5, skc4)!=skf10(skc5, skc4))). % 74.66/65.53 tff(c_585, plain, (skf16(skc5, skc4)!=skf12(skc5, skc4))). % 74.66/65.53 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf18(U_101, V_102)!=skf10(U_101, V_102)))). % 74.66/65.53 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf16(U_111, V_112)!=skf12(U_111, V_112)))). % 74.74/65.53 tff(c_580, plain, (skf16(skc5, skc4)!=skf10(skc5, skc4))). % 74.74/65.53 tff(c_575, plain, (skf18(skc5, skc4)!=skf14(skc5, skc4))). % 74.74/65.53 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf16(U_109, V_110)!=skf10(U_109, V_110)))). % 74.74/65.53 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf18(U_105, V_106)!=skf14(U_105, V_106)))). % 74.74/65.53 tff(c_569, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.53 tff(c_504, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 74.74/65.54 tff(c_560, plain, (skf14(skc5, skc4)!=skf12(skc5, skc4))). % 74.74/65.54 tff(c_555, plain, (act(skc4, skf10(skc5, skc4)))). % 74.74/65.54 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf14(U_117, V_118)!=skf12(U_117, V_118)))). % 74.74/65.54 tff(c_551, plain, (action(skc4, skf10(skc5, skc4)))). % 74.74/65.54 tff(c_547, plain, (shot(skc4, skf10(skc5, skc4)))). % 74.74/65.54 tff(c_539, plain, (~act(skc4, skc5))). % 74.74/65.54 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf10(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 74.74/65.54 tff(c_535, plain, (~event(skc4, skc5))). % 74.74/65.54 tff(c_531, plain, (~eventuality(skc4, skc5))). % 74.74/65.54 tff(c_408, plain, (![U_247, V_248]: (~eventuality(U_247, V_248) | ~group(U_247, V_248)))). % 74.74/65.54 tff(c_480, plain, (![U_362, V_363]: (artifact(U_362, V_363) | ~cannon(U_362, V_363)))). % 74.74/65.54 tff(c_525, plain, (skf14(skc5, skc4)!=skf10(skc5, skc4))). % 74.74/65.54 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf14(U_115, V_116)!=skf10(U_115, V_116)))). % 74.74/65.54 tff(c_520, plain, (act(skc4, skf16(skc5, skc4)))). % 74.74/65.54 tff(c_516, plain, (action(skc4, skf16(skc5, skc4)))). % 74.74/65.54 tff(c_512, plain, (shot(skc4, skf16(skc5, skc4)))). % 74.74/65.54 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf16(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 74.74/65.54 tff(c_432, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 74.74/65.54 tff(c_427, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 74.74/65.54 tff(c_490, plain, (skf20(skc5, skc4)!=skf12(skc5, skc4))). % 74.74/65.54 tff(c_494, plain, (~artifact(skc4, skc5))). % 74.74/65.54 tff(c_485, plain, (~entity(skc4, skc5))). % 74.74/65.54 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf20(U_93, V_94)!=skf12(U_93, V_94)))). % 74.74/65.54 tff(c_469, plain, (![U_247, V_248]: (~entity(U_247, V_248) | ~group(U_247, V_248)))). % 74.74/65.54 tff(c_334, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 74.74/65.54 tff(c_475, plain, (skf16(skc5, skc4)!=skf14(skc5, skc4))). % 74.74/65.54 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf16(U_113, V_114)!=skf14(U_113, V_114)))). % 74.74/65.54 tff(c_287, plain, (![U_304, V_305]: (~animate(U_304, V_305) | ~artifact(U_304, V_305)))). % 74.74/65.54 tff(c_366, plain, (![U_328, V_329]: (~multiple(U_328, V_329) | ~entity(U_328, V_329)))). % 74.74/65.54 tff(c_464, plain, (act(skc4, skf18(skc5, skc4)))). % 74.74/65.54 tff(c_460, plain, (action(skc4, skf18(skc5, skc4)))). % 74.74/65.54 tff(c_456, plain, (shot(skc4, skf18(skc5, skc4)))). % 74.74/65.54 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf18(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 74.74/65.54 tff(c_448, plain, (act(skc4, skf20(skc5, skc4)))). % 74.74/65.54 tff(c_444, plain, (action(skc4, skf20(skc5, skc4)))). % 74.74/65.54 tff(c_440, plain, (shot(skc4, skf20(skc5, skc4)))). % 74.74/65.54 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf20(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 74.74/65.54 tff(c_328, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 74.74/65.54 tff(c_286, plain, (![U_304, V_305]: (~living(U_304, V_305) | ~artifact(U_304, V_305)))). % 74.74/65.54 tff(c_422, plain, (skf20(skc5, skc4)!=skf16(skc5, skc4))). % 74.74/65.54 tff(c_417, plain, (~artifact(skc4, skc6))). % 74.74/65.54 tff(c_416, plain, (~artifact(skc4, skc7))). % 74.74/65.54 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf20(U_97, V_98)!=skf16(U_97, V_98)))). % 74.74/65.54 tff(c_398, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.54 tff(c_393, plain, (![U_336, V_337]: (~multiple(U_336, V_337) | ~eventuality(U_336, V_337)))). % 74.74/65.54 tff(c_403, plain, (skf20(skc5, skc4)!=skf14(skc5, skc4))). % 74.74/65.54 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf20(U_95, V_96)!=skf14(U_95, V_96)))). % 74.74/65.54 tff(c_387, plain, (skf18(skc5, skc4)!=skf16(skc5, skc4))). % 74.74/65.54 tff(c_269, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 74.74/65.54 tff(c_323, plain, (skf18(skc5, skc4)!=skf12(skc5, skc4))). % 74.74/65.54 tff(c_202, plain, (![U_255, V_256]: (singleton(U_255, V_256) | ~eventuality(U_255, V_256)))). % 74.74/65.55 tff(c_189, plain, (![U_247, V_248]: (multiple(U_247, V_248) | ~group(U_247, V_248)))). % 74.74/65.55 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf18(U_107, V_108)!=skf16(U_107, V_108)))). % 74.74/65.55 tff(c_382, plain, (act(skc4, skf14(skc5, skc4)))). % 74.74/65.55 tff(c_378, plain, (action(skc4, skf14(skc5, skc4)))). % 74.74/65.55 tff(c_374, plain, (shot(skc4, skf14(skc5, skc4)))). % 74.74/65.55 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf14(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 74.74/65.55 tff(c_207, plain, (![U_257, V_258]: (singleton(U_257, V_258) | ~entity(U_257, V_258)))). % 74.74/65.55 tff(c_223, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.55 tff(c_355, plain, (skf12(skc5, skc4)!=skf10(skc5, skc4))). % 74.74/65.55 tff(c_360, plain, (entity(skc4, skc7))). % 74.74/65.55 tff(c_240, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 74.74/65.55 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf12(U_119, V_120)!=skf10(U_119, V_120)))). % 74.74/65.55 tff(c_350, plain, (act(skc4, skf12(skc5, skc4)))). % 74.74/65.55 tff(c_346, plain, (action(skc4, skf12(skc5, skc4)))). % 74.74/65.55 tff(c_342, plain, (shot(skc4, skf12(skc5, skc4)))). % 74.74/65.55 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf12(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 74.74/65.55 tff(c_178, plain, (![U_241, V_242]: (instrumentality(U_241, V_242) | ~weapon(U_241, V_242)))). % 74.74/65.55 tff(c_184, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.55 tff(c_228, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 74.74/65.55 tff(c_310, plain, (skf20(skc5, skc4)!=skf10(skc5, skc4))). % 74.74/65.55 tff(c_318, plain, (~act(skc4, skc6))). % 74.74/65.55 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf18(U_103, V_104)!=skf12(U_103, V_104)))). % 74.74/65.55 tff(c_314, plain, (~act(skc4, skc7))). % 74.74/65.55 tff(c_305, plain, (~event(skc4, skc6))). % 74.74/65.55 tff(c_301, plain, (~event(skc4, skc7))). % 74.74/65.55 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf20(U_91, V_92)!=skf10(U_91, V_92)))). % 74.74/65.55 tff(c_297, plain, (~eventuality(skc4, skc6))). % 74.74/65.55 tff(c_296, plain, (~eventuality(skc4, skc7))). % 74.74/65.55 tff(c_270, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 74.74/65.55 tff(c_275, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 74.74/65.55 tff(c_213, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.55 tff(c_150, plain, (![U_210]: (shot(skc4, U_210) | ~member(skc4, U_210, skc5)))). % 74.74/65.55 tff(c_261, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 74.74/65.55 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 74.74/65.55 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 74.74/65.55 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 74.74/65.55 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 74.74/65.55 tff(c_256, plain, (human(skc4, skc7))). % 74.74/65.55 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 74.74/65.55 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 74.74/65.55 tff(c_250, plain, (animate(skc4, skc7))). % 74.74/65.55 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 74.74/65.55 tff(c_245, plain, (male(skc4, skc7))). % 74.74/65.55 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 74.74/65.55 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 74.74/65.55 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 74.74/65.55 tff(c_234, plain, (human_person(skc4, skc7))). % 74.74/65.55 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 74.74/65.55 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 74.74/65.55 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 74.74/65.55 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 74.74/65.55 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 74.74/65.55 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 74.74/65.55 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 74.74/65.55 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 74.74/65.56 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 74.74/65.56 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 74.74/65.56 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 74.74/65.56 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 74.74/65.56 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 74.74/65.56 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 74.74/65.56 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 74.74/65.56 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 74.74/65.56 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 74.74/65.56 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 74.74/65.56 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 74.74/65.56 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 74.74/65.56 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 74.74/65.56 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 74.74/65.56 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 74.74/65.56 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 74.74/65.56 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 74.74/65.56 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 74.74/65.56 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 74.74/65.56 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 74.74/65.56 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 74.74/65.56 tff(c_142, plain, (man(skc4, skc7))). % 74.74/65.56 tff(c_148, plain, (group(skc4, skc5))). % 74.74/65.56 tff(c_144, plain, (male(skc4, skc6))). % 74.74/65.56 tff(c_146, plain, (six(skc4, skc5))). % 74.74/65.56 tff(c_140, plain, (actual_world(skc4))). % 74.74/65.56 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 74.74/65.56 %------------------------------------------------------------------------------