%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP070-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n022.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 60.33s 51.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP070-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:22:20 EDT 2025 % 0.12/0.34 % CPUTime : % 60.33/51.54 % 60.33/51.54 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 60.33/51.54 % 60.33/51.54 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 60.33/51.55 %$ 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 > skf23 > skf22 > skf20 > skf18 > skf16 > skf14 > skf12 > #nlpp > skf9 > skf10 > skc5 > skc4 > skc3 % 60.33/51.55 % 60.33/51.55 %Foreground sorts: % 60.33/51.55 % 60.33/51.55 % 60.33/51.55 %Background operators: % 60.33/51.55 % 60.33/51.55 % 60.33/51.55 %Foreground operators: % 60.33/51.55 tff(nonliving, type, nonliving: ($i * $i) > $o). % 60.33/51.55 tff(member, type, member: ($i * $i * $i) > $o). % 60.33/51.55 tff(living, type, living: ($i * $i) > $o). % 60.33/51.55 tff(fire, type, fire: ($i * $i) > $o). % 60.33/51.55 tff(human_person, type, human_person: ($i * $i) > $o). % 60.33/51.55 tff(action, type, action: ($i * $i) > $o). % 60.33/51.55 tff(present, type, present: ($i * $i) > $o). % 60.33/51.55 tff(shot, type, shot: ($i * $i) > $o). % 60.33/51.55 tff(skf22, type, skf22: ($i * $i) > $i). % 60.33/51.55 tff(entity, type, entity: ($i * $i) > $o). % 60.33/51.55 tff(eventuality, type, eventuality: ($i * $i) > $o). % 60.33/51.55 tff(weapon, type, weapon: ($i * $i) > $o). % 60.33/51.55 tff(existent, type, existent: ($i * $i) > $o). % 60.33/51.55 tff(singleton, type, singleton: ($i * $i) > $o). % 60.33/51.55 tff(male, type, male: ($i * $i) > $o). % 60.33/51.55 tff(multiple, type, multiple: ($i * $i) > $o). % 60.33/51.55 tff(organism, type, organism: ($i * $i) > $o). % 60.33/51.55 tff(animate, type, animate: ($i * $i) > $o). % 60.33/51.55 tff(of, type, of: ($i * $i * $i) > $o). % 60.33/51.55 tff(skf14, type, skf14: ($i * $i) > $i). % 60.33/51.55 tff(actual_world, type, actual_world: $i > $o). % 60.33/51.55 tff(agent, type, agent: ($i * $i * $i) > $o). % 60.33/51.55 tff(skf10, type, skf10: $i > $i). % 60.33/51.55 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 60.33/51.55 tff(group, type, group: ($i * $i) > $o). % 60.33/51.55 tff(artifact, type, artifact: ($i * $i) > $o). % 60.33/51.55 tff(cannon, type, cannon: ($i * $i) > $o). % 60.33/51.55 tff(event, type, event: ($i * $i) > $o). % 60.33/51.55 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 60.33/51.55 tff(patient, type, patient: ($i * $i * $i) > $o). % 60.33/51.55 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 60.33/51.55 tff(skc4, type, skc4: $i). % 60.33/51.55 tff(skc3, type, skc3: $i). % 60.33/51.55 tff(thing, type, thing: ($i * $i) > $o). % 60.33/51.55 tff(skf9, type, skf9: $i > $i). % 60.33/51.55 tff(human, type, human: ($i * $i) > $o). % 60.33/51.55 tff(six, type, six: ($i * $i) > $o). % 60.33/51.55 tff(skf18, type, skf18: ($i * $i) > $i). % 60.33/51.55 tff(man, type, man: ($i * $i) > $o). % 60.33/51.55 tff(skc5, type, skc5: $i). % 60.33/51.55 tff(weaponry, type, weaponry: ($i * $i) > $o). % 60.33/51.55 tff(unisex, type, unisex: ($i * $i) > $o). % 60.33/51.55 tff(skf16, type, skf16: ($i * $i) > $i). % 60.33/51.55 tff(set, type, set: ($i * $i) > $o). % 60.33/51.55 tff(skf12, type, skf12: ($i * $i) > $i). % 60.33/51.55 tff(impartial, type, impartial: ($i * $i) > $o). % 60.33/51.55 tff(skf23, type, skf23: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 60.33/51.55 tff(object, type, object: ($i * $i) > $o). % 60.33/51.55 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 60.33/51.55 tff(specific, type, specific: ($i * $i) > $o). % 60.33/51.55 tff(skf20, type, skf20: ($i * $i) > $i). % 60.33/51.55 tff(act, type, act: ($i * $i) > $o). % 60.33/51.55 % 60.33/51.55 %Saturated clause set: % 60.33/51.55 tff(c_1056, plain, (![Z_183, Z_943, X2_933, V_941, X1_959, X1_948, V_952, X2_185, X1_927, X_936, W_932, Y_926, X2_956, V_944, V_961, Y_947, Y_963, X2_934, Z_949, W_181, X_957, X_950, Y_938, Z_964, V_965, X1_184, X_954, X1_946, Z_945, Y_187, Z_960, Y_931, X1_939, Y_935, X2_930, X_186, V_188, Z_951, U_182, X_958, X2_940, X1_953, V_942, X2_962, X_955]: (skf23(V_961, X_957, Y_935, Z_960, X1_948, X2_956, W_181, U_182)=skf23(V_942, X_950, Y_947, Z_951, X1_927, X2_940, W_181, U_182) | skf23(V_942, X_950, Y_947, Z_951, X1_927, X2_940, W_181, U_182)=skf23(V_941, X_958, Y_931, Z_945, X1_946, X2_934, W_181, U_182) | skf23(V_961, X_957, Y_935, Z_960, X1_948, X2_956, W_181, U_182)=skf23(V_941, X_958, Y_931, Z_945, X1_946, X2_934, W_181, U_182) | skf23(V_952, X_936, Y_926, Z_949, X1_959, X2_962, W_181, U_182)=skf23(V_941, X_958, Y_931, Z_945, X1_946, X2_934, W_181, U_182) | skf23(V_952, X_936, Y_926, Z_949, X1_959, X2_962, W_181, U_182)=skf23(V_942, X_950, Y_947, Z_951, X1_927, X2_940, W_181, U_182) | skf23(V_961, X_957, Y_935, Z_960, X1_948, X2_956, W_181, U_182)=skf23(V_952, X_936, Y_926, Z_949, X1_959, X2_962, W_181, U_182) | skf23(V_965, X_954, Y_938, Z_943, X1_953, X2_930, W_181, U_182)=skf23(V_952, X_936, Y_926, Z_949, X1_959, X2_962, W_181, U_182) | skf23(V_965, X_954, Y_938, Z_943, X1_953, X2_930, W_181, U_182)=skf23(V_941, X_958, Y_931, Z_945, X1_946, X2_934, W_181, U_182) | skf23(V_965, X_954, Y_938, Z_943, X1_953, X2_930, W_181, U_182)=skf23(V_942, X_950, Y_947, Z_951, X1_927, X2_940, W_181, U_182) | skf23(V_965, X_954, Y_938, Z_943, X1_953, X2_930, W_181, U_182)=skf23(V_961, X_957, Y_935, Z_960, X1_948, X2_956, W_181, U_182) | skf23(V_965, X_954, Y_938, Z_943, X1_953, X2_930, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_952, X_936, Y_926, Z_949, X1_959, X2_962, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_941, X_958, Y_931, Z_945, X1_946, X2_934, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_942, X_950, Y_947, Z_951, X1_927, X2_940, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_961, X_957, Y_935, Z_960, X1_948, X2_956, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), V_944, W_932, X_955, Y_963, Z_964, X1_939, X2_933)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_956=X1_948 | Z_960=X1_948 | Z_960=X2_956 | Z_960=Y_935 | Y_935=X1_948 | Y_935=X2_956 | Y_935=X_957 | Z_960=X_957 | X_957=X1_948 | X_957=X2_956 | X_957=V_961 | Y_935=V_961 | Z_960=V_961 | X1_948=V_961 | X2_956=V_961 | ~member(U_182, X2_956, W_181) | ~member(U_182, X1_948, W_181) | ~member(U_182, Z_960, W_181) | ~member(U_182, Y_935, W_181) | ~member(U_182, X_957, W_181) | ~member(U_182, V_961, W_181) | X2_940=X1_927 | Z_951=X1_927 | Z_951=X2_940 | Z_951=Y_947 | Y_947=X1_927 | Y_947=X2_940 | Y_947=X_950 | Z_951=X_950 | X_950=X1_927 | X_950=X2_940 | X_950=V_942 | Y_947=V_942 | Z_951=V_942 | X1_927=V_942 | X2_940=V_942 | ~member(U_182, X2_940, W_181) | ~member(U_182, X1_927, W_181) | ~member(U_182, Z_951, W_181) | ~member(U_182, Y_947, W_181) | ~member(U_182, X_950, W_181) | ~member(U_182, V_942, W_181) | X2_934=X1_946 | Z_945=X1_946 | Z_945=X2_934 | Z_945=Y_931 | Y_931=X1_946 | Y_931=X2_934 | Y_931=X_958 | Z_945=X_958 | X_958=X1_946 | X_958=X2_934 | X_958=V_941 | Y_931=V_941 | Z_945=V_941 | X1_946=V_941 | X2_934=V_941 | ~member(U_182, X2_934, W_181) | ~member(U_182, X1_946, W_181) | ~member(U_182, Z_945, W_181) | ~member(U_182, Y_931, W_181) | ~member(U_182, X_958, W_181) | ~member(U_182, V_941, W_181) | X2_962=X1_959 | Z_949=X1_959 | Z_949=X2_962 | Z_949=Y_926 | Y_926=X1_959 | Y_926=X2_962 | Y_926=X_936 | Z_949=X_936 | X_936=X1_959 | X_936=X2_962 | X_936=V_952 | Y_926=V_952 | Z_949=V_952 | X1_959=V_952 | X2_962=V_952 | ~member(U_182, X2_962, W_181) | ~member(U_182, X1_959, W_181) | ~member(U_182, Z_949, W_181) | ~member(U_182, Y_926, W_181) | ~member(U_182, X_936, W_181) | ~member(U_182, V_952, W_181) | X2_930=X1_953 | Z_943=X1_953 | Z_943=X2_930 | Z_943=Y_938 | Y_938=X1_953 | Y_938=X2_930 | Y_938=X_954 | Z_943=X_954 | X_954=X1_953 | X_954=X2_930 | X_954=V_965 | Y_938=V_965 | Z_943=V_965 | X1_953=V_965 | X2_930=V_965 | ~member(U_182, X2_930, W_181) | ~member(U_182, X1_953, W_181) | ~member(U_182, Z_943, W_181) | ~member(U_182, Y_938, W_181) | ~member(U_182, X_954, W_181) | ~member(U_182, V_965, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_1033, plain, (![Z_183, Z_865, X_884, W_890, X_862, X_891, Z_887, X2_185, X2_874, X2_885, X2_863, X2_870, Y_873, Y_867, X_886, X1_860, U_868, Z_875, V_864, X1_883, W_181, Y_876, X1_888, Z_878, X1_866, X1_861, X2_889, X1_184, Y_187, X_186, V_188, U_182, V_881, Z_877, Y_871, V_892, Y_882, X_879, V_869]: (skf23(V_881, X_862, Y_876, Z_878, X1_888, X2_870, W_181, U_182)=skf23(V_864, X_886, Y_871, Z_865, X1_860, X2_889, W_181, U_182) | skf23(V_869, X_879, Y_882, Z_875, X1_861, X2_874, W_181, U_182)=skf23(V_864, X_886, Y_871, Z_865, X1_860, X2_889, W_181, U_182) | skf23(V_881, X_862, Y_876, Z_878, X1_888, X2_870, W_181, U_182)=skf23(V_869, X_879, Y_882, Z_875, X1_861, X2_874, W_181, U_182) | skf23(V_892, X_884, Y_873, Z_877, X1_883, X2_863, W_181, U_182)=skf23(V_869, X_879, Y_882, Z_875, X1_861, X2_874, W_181, U_182) | skf23(V_892, X_884, Y_873, Z_877, X1_883, X2_863, W_181, U_182)=skf23(V_864, X_886, Y_871, Z_865, X1_860, X2_889, W_181, U_182) | skf23(V_892, X_884, Y_873, Z_877, X1_883, X2_863, W_181, U_182)=skf23(V_881, X_862, Y_876, Z_878, X1_888, X2_870, W_181, U_182) | skf23(V_892, X_884, Y_873, Z_877, X1_883, X2_863, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_869, X_879, Y_882, Z_875, X1_861, X2_874, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_864, X_886, Y_871, Z_865, X1_860, X2_889, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_881, X_862, Y_876, Z_878, X1_888, X2_870, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_868 | skf23(V_892, X_884, Y_873, Z_877, X1_883, X2_863, W_181, U_182)=U_868 | skf23(V_869, X_879, Y_882, Z_875, X1_861, X2_874, W_181, U_182)=U_868 | skf23(V_864, X_886, Y_871, Z_865, X1_860, X2_889, W_181, U_182)=U_868 | skf23(V_881, X_862, Y_876, Z_878, X1_888, X2_870, W_181, U_182)=U_868 | ~member(U_182, U_868, W_181) | skf23(U_868, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), W_890, X_891, Y_867, Z_887, X1_866, X2_885)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_870=X1_888 | Z_878=X1_888 | Z_878=X2_870 | Z_878=Y_876 | Y_876=X1_888 | Y_876=X2_870 | Y_876=X_862 | Z_878=X_862 | X_862=X1_888 | X_862=X2_870 | X_862=V_881 | Y_876=V_881 | Z_878=V_881 | X1_888=V_881 | X2_870=V_881 | ~member(U_182, X2_870, W_181) | ~member(U_182, X1_888, W_181) | ~member(U_182, Z_878, W_181) | ~member(U_182, Y_876, W_181) | ~member(U_182, X_862, W_181) | ~member(U_182, V_881, W_181) | X2_889=X1_860 | Z_865=X1_860 | Z_865=X2_889 | Z_865=Y_871 | Y_871=X1_860 | Y_871=X2_889 | Y_871=X_886 | Z_865=X_886 | X_886=X1_860 | X_886=X2_889 | X_886=V_864 | Y_871=V_864 | Z_865=V_864 | X1_860=V_864 | X2_889=V_864 | ~member(U_182, X2_889, W_181) | ~member(U_182, X1_860, W_181) | ~member(U_182, Z_865, W_181) | ~member(U_182, Y_871, W_181) | ~member(U_182, X_886, W_181) | ~member(U_182, V_864, W_181) | X2_874=X1_861 | Z_875=X1_861 | Z_875=X2_874 | Z_875=Y_882 | Y_882=X1_861 | Y_882=X2_874 | Y_882=X_879 | Z_875=X_879 | X_879=X1_861 | X_879=X2_874 | X_879=V_869 | Y_882=V_869 | Z_875=V_869 | X1_861=V_869 | X2_874=V_869 | ~member(U_182, X2_874, W_181) | ~member(U_182, X1_861, W_181) | ~member(U_182, Z_875, W_181) | ~member(U_182, Y_882, W_181) | ~member(U_182, X_879, W_181) | ~member(U_182, V_869, W_181) | X2_863=X1_883 | Z_877=X1_883 | Z_877=X2_863 | Z_877=Y_873 | Y_873=X1_883 | Y_873=X2_863 | Y_873=X_884 | Z_877=X_884 | X_884=X1_883 | X_884=X2_863 | X_884=V_892 | Y_873=V_892 | Z_877=V_892 | X1_883=V_892 | X2_863=V_892 | ~member(U_182, X2_863, W_181) | ~member(U_182, X1_883, W_181) | ~member(U_182, Z_877, W_181) | ~member(U_182, Y_873, W_181) | ~member(U_182, X_884, W_181) | ~member(U_182, V_892, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_1011, plain, (![Z_183, X_840, Y_849, X_836, X1_851, V_826, X2_185, Y_843, Z_827, Z_846, X_853, Y_832, X1_844, X2_829, X2_830, X2_848, V_856, W_181, X1_845, V_824, V_831, X2_828, X1_184, X2_842, Y_187, X_838, U_833, X1_857, X_841, Y_834, V_858, Z_847, X_186, Y_837, V_188, U_182, Z_855, Z_850, W_839, X1_852]: (skf23(V_826, X_836, Y_834, Z_827, X1_844, X2_830, W_181, U_182)=skf23(V_824, X_838, Y_849, Z_850, X1_857, X2_828, W_181, U_182) | skf23(V_856, X_841, Y_843, Z_855, X1_852, X2_842, W_181, U_182)=skf23(V_826, X_836, Y_834, Z_827, X1_844, X2_830, W_181, U_182) | skf23(V_856, X_841, Y_843, Z_855, X1_852, X2_842, W_181, U_182)=skf23(V_824, X_838, Y_849, Z_850, X1_857, X2_828, W_181, U_182) | skf23(V_858, X_853, Y_837, Z_847, X1_851, X2_829, W_181, U_182)=skf23(V_856, X_841, Y_843, Z_855, X1_852, X2_842, W_181, U_182) | skf23(V_858, X_853, Y_837, Z_847, X1_851, X2_829, W_181, U_182)=skf23(V_826, X_836, Y_834, Z_827, X1_844, X2_830, W_181, U_182) | skf23(V_858, X_853, Y_837, Z_847, X1_851, X2_829, W_181, U_182)=skf23(V_824, X_838, Y_849, Z_850, X1_857, X2_828, W_181, U_182) | skf23(V_858, X_853, Y_837, Z_847, X1_851, X2_829, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_856, X_841, Y_843, Z_855, X1_852, X2_842, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_826, X_836, Y_834, Z_827, X1_844, X2_830, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_824, X_838, Y_849, Z_850, X1_857, X2_828, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_833 | skf23(V_858, X_853, Y_837, Z_847, X1_851, X2_829, W_181, U_182)=U_833 | skf23(V_856, X_841, Y_843, Z_855, X1_852, X2_842, W_181, U_182)=U_833 | skf23(V_826, X_836, Y_834, Z_827, X1_844, X2_830, W_181, U_182)=U_833 | skf23(V_824, X_838, Y_849, Z_850, X1_857, X2_828, W_181, U_182)=U_833 | ~member(U_182, U_833, W_181) | skf23(U_833, V_831, W_839, X_840, Y_832, Z_846, X1_845, X2_848)!=U_833 | X2_828=X1_857 | Z_850=X1_857 | Z_850=X2_828 | Z_850=Y_849 | Y_849=X1_857 | Y_849=X2_828 | Y_849=X_838 | Z_850=X_838 | X_838=X1_857 | X_838=X2_828 | X_838=V_824 | Y_849=V_824 | Z_850=V_824 | X1_857=V_824 | X2_828=V_824 | ~member(U_182, X2_828, W_181) | ~member(U_182, X1_857, W_181) | ~member(U_182, Z_850, W_181) | ~member(U_182, Y_849, W_181) | ~member(U_182, X_838, W_181) | ~member(U_182, V_824, W_181) | X2_830=X1_844 | Z_827=X1_844 | Z_827=X2_830 | Z_827=Y_834 | Y_834=X1_844 | Y_834=X2_830 | Y_834=X_836 | Z_827=X_836 | X_836=X1_844 | X_836=X2_830 | X_836=V_826 | Y_834=V_826 | Z_827=V_826 | X1_844=V_826 | X2_830=V_826 | ~member(U_182, X2_830, W_181) | ~member(U_182, X1_844, W_181) | ~member(U_182, Z_827, W_181) | ~member(U_182, Y_834, W_181) | ~member(U_182, X_836, W_181) | ~member(U_182, V_826, W_181) | X2_842=X1_852 | Z_855=X1_852 | Z_855=X2_842 | Z_855=Y_843 | Y_843=X1_852 | Y_843=X2_842 | Y_843=X_841 | Z_855=X_841 | X_841=X1_852 | X_841=X2_842 | X_841=V_856 | Y_843=V_856 | Z_855=V_856 | X1_852=V_856 | X2_842=V_856 | ~member(U_182, X2_842, W_181) | ~member(U_182, X1_852, W_181) | ~member(U_182, Z_855, W_181) | ~member(U_182, Y_843, W_181) | ~member(U_182, X_841, W_181) | ~member(U_182, V_856, W_181) | X2_829=X1_851 | Z_847=X1_851 | Z_847=X2_829 | Z_847=Y_837 | Y_837=X1_851 | Y_837=X2_829 | Y_837=X_853 | Z_847=X_853 | X_853=X1_851 | X_853=X2_829 | X_853=V_858 | Y_837=V_858 | Z_847=V_858 | X1_851=V_858 | X2_829=V_858 | ~member(U_182, X2_829, W_181) | ~member(U_182, X1_851, W_181) | ~member(U_182, Z_847, W_181) | ~member(U_182, Y_837, W_181) | ~member(U_182, X_853, W_181) | ~member(U_182, V_858, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_966, plain, (![X1_751, Z_183, V_742, V_746, X_761, X2_752, X_764, Y_759, X2_740, X2_185, V_763, X1_754, X2_743, Z_756, Y_744, Y_750, V_766, W_181, X1_758, X2_755, Z_747, X_745, X1_184, Y_741, U_748, Y_187, X1_760, X_186, Z_757, X_762, V_188, U_182, Z_765]: (skf23(V_763, X_761, Y_741, Z_747, X1_754, X2_752, W_181, U_182)=skf23(V_746, X_745, Y_744, Z_765, X1_758, X2_740, W_181, U_182) | skf23(V_766, X_764, Y_750, Z_756, X1_760, X2_743, W_181, U_182)=skf23(V_763, X_761, Y_741, Z_747, X1_754, X2_752, W_181, U_182) | skf23(V_766, X_764, Y_750, Z_756, X1_760, X2_743, W_181, U_182)=skf23(V_746, X_745, Y_744, Z_765, X1_758, X2_740, W_181, U_182) | skf23(V_766, X_764, Y_750, Z_756, X1_760, X2_743, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_763, X_761, Y_741, Z_747, X1_754, X2_752, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_746, X_745, Y_744, Z_765, X1_758, X2_740, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_742 | skf23(V_766, X_764, Y_750, Z_756, X1_760, X2_743, W_181, U_182)=V_742 | skf23(V_763, X_761, Y_741, Z_747, X1_754, X2_752, W_181, U_182)=V_742 | skf23(V_746, X_745, Y_744, Z_765, X1_758, X2_740, W_181, U_182)=V_742 | V_742=U_748 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_748 | skf23(V_766, X_764, Y_750, Z_756, X1_760, X2_743, W_181, U_182)=U_748 | skf23(V_763, X_761, Y_741, Z_747, X1_754, X2_752, W_181, U_182)=U_748 | skf23(V_746, X_745, Y_744, Z_765, X1_758, X2_740, W_181, U_182)=U_748 | ~member(U_182, V_742, W_181) | ~member(U_182, U_748, W_181) | skf23(U_748, V_742, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), X_762, Y_759, Z_757, X1_751, X2_755)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_740=X1_758 | Z_765=X1_758 | Z_765=X2_740 | Z_765=Y_744 | Y_744=X1_758 | Y_744=X2_740 | Y_744=X_745 | Z_765=X_745 | X_745=X1_758 | X_745=X2_740 | X_745=V_746 | Y_744=V_746 | Z_765=V_746 | X1_758=V_746 | X2_740=V_746 | ~member(U_182, X2_740, W_181) | ~member(U_182, X1_758, W_181) | ~member(U_182, Z_765, W_181) | ~member(U_182, Y_744, W_181) | ~member(U_182, X_745, W_181) | ~member(U_182, V_746, W_181) | X2_752=X1_754 | Z_747=X1_754 | Z_747=X2_752 | Z_747=Y_741 | Y_741=X1_754 | Y_741=X2_752 | Y_741=X_761 | Z_747=X_761 | X_761=X1_754 | X_761=X2_752 | X_761=V_763 | Y_741=V_763 | Z_747=V_763 | X1_754=V_763 | X2_752=V_763 | ~member(U_182, X2_752, W_181) | ~member(U_182, X1_754, W_181) | ~member(U_182, Z_747, W_181) | ~member(U_182, Y_741, W_181) | ~member(U_182, X_761, W_181) | ~member(U_182, V_763, W_181) | X2_743=X1_760 | Z_756=X1_760 | Z_756=X2_743 | Z_756=Y_750 | Y_750=X1_760 | Y_750=X2_743 | Y_750=X_764 | Z_756=X_764 | X_764=X1_760 | X_764=X2_743 | X_764=V_766 | Y_750=V_766 | Z_756=V_766 | X1_760=V_766 | X2_743=V_766 | ~member(U_182, X2_743, W_181) | ~member(U_182, X1_760, W_181) | ~member(U_182, Z_756, W_181) | ~member(U_182, Y_750, W_181) | ~member(U_182, X_764, W_181) | ~member(U_182, V_766, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_944, plain, (![Z_718, Z_183, V_714, X_730, X2_185, X1_729, X2_721, V_715, W_181, X1_733, W_723, X_726, V_738, Y_720, X1_184, X2_737, X1_732, Y_187, Y_724, X_710, Z_717, Y_722, U_736, X_186, Y_711, X_734, V_188, X2_716, U_182, X2_712, Z_735, X1_731, Z_727, V_728]: (skf23(V_728, X_726, Y_722, Z_717, X1_731, X2_721, W_181, U_182)=skf23(V_715, X_730, Y_711, Z_718, X1_732, X2_737, W_181, U_182) | skf23(V_738, X_734, Y_720, Z_727, X1_733, X2_716, W_181, U_182)=skf23(V_715, X_730, Y_711, Z_718, X1_732, X2_737, W_181, U_182) | skf23(V_738, X_734, Y_720, Z_727, X1_733, X2_716, W_181, U_182)=skf23(V_728, X_726, Y_722, Z_717, X1_731, X2_721, W_181, U_182) | skf23(V_738, X_734, Y_720, Z_727, X1_733, X2_716, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_715, X_730, Y_711, Z_718, X1_732, X2_737, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_728, X_726, Y_722, Z_717, X1_731, X2_721, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_714 | skf23(V_738, X_734, Y_720, Z_727, X1_733, X2_716, W_181, U_182)=V_714 | skf23(V_715, X_730, Y_711, Z_718, X1_732, X2_737, W_181, U_182)=V_714 | skf23(V_728, X_726, Y_722, Z_717, X1_731, X2_721, W_181, U_182)=V_714 | V_714=U_736 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_736 | skf23(V_738, X_734, Y_720, Z_727, X1_733, X2_716, W_181, U_182)=U_736 | skf23(V_715, X_730, Y_711, Z_718, X1_732, X2_737, W_181, U_182)=U_736 | skf23(V_728, X_726, Y_722, Z_717, X1_731, X2_721, W_181, U_182)=U_736 | ~member(U_182, V_714, W_181) | ~member(U_182, U_736, W_181) | skf23(U_736, V_714, W_723, X_710, Y_724, Z_735, X1_729, X2_712)!=V_714 | X2_721=X1_731 | Z_717=X1_731 | Z_717=X2_721 | Z_717=Y_722 | Y_722=X1_731 | Y_722=X2_721 | Y_722=X_726 | Z_717=X_726 | X_726=X1_731 | X_726=X2_721 | X_726=V_728 | Y_722=V_728 | Z_717=V_728 | X1_731=V_728 | X2_721=V_728 | ~member(U_182, X2_721, W_181) | ~member(U_182, X1_731, W_181) | ~member(U_182, Z_717, W_181) | ~member(U_182, Y_722, W_181) | ~member(U_182, X_726, W_181) | ~member(U_182, V_728, W_181) | X2_737=X1_732 | Z_718=X1_732 | Z_718=X2_737 | Z_718=Y_711 | Y_711=X1_732 | Y_711=X2_737 | Y_711=X_730 | Z_718=X_730 | X_730=X1_732 | X_730=X2_737 | X_730=V_715 | Y_711=V_715 | Z_718=V_715 | X1_732=V_715 | X2_737=V_715 | ~member(U_182, X2_737, W_181) | ~member(U_182, X1_732, W_181) | ~member(U_182, Z_718, W_181) | ~member(U_182, Y_711, W_181) | ~member(U_182, X_730, W_181) | ~member(U_182, V_715, W_181) | X2_716=X1_733 | Z_727=X1_733 | Z_727=X2_716 | Z_727=Y_720 | Y_720=X1_733 | Y_720=X2_716 | Y_720=X_734 | Z_727=X_734 | X_734=X1_733 | X_734=X2_716 | X_734=V_738 | Y_720=V_738 | Z_727=V_738 | X1_733=V_738 | X2_716=V_738 | ~member(U_182, X2_716, W_181) | ~member(U_182, X1_733, W_181) | ~member(U_182, Z_727, W_181) | ~member(U_182, Y_720, W_181) | ~member(U_182, X_734, W_181) | ~member(U_182, V_738, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_988, plain, (![Z_183, X5_778, X1_767, X_792, X1_795, Y_777, W_770, X2_185, X2_789, V_774, Z_782, V_788, Z_787, Y_786, V_784, X_794, W_181, X1_793, Y_780, X1_184, V_796, Y_187, X2_772, U_773, Z_779, X_768, X2_771, X_186, X2_783, X1_785, V_188, U_182, Y_781, Z_776, X_790]: (skf23(V_788, X_790, Y_786, Z_776, X1_767, X2_789, W_181, U_182)=skf23(V_774, X_792, Y_781, Z_782, X1_795, X2_783, W_181, U_182) | skf23(V_796, X_794, Y_777, Z_787, X1_793, X2_772, W_181, U_182)=skf23(V_774, X_792, Y_781, Z_782, X1_795, X2_783, W_181, U_182) | skf23(V_796, X_794, Y_777, Z_787, X1_793, X2_772, W_181, U_182)=skf23(V_788, X_790, Y_786, Z_776, X1_767, X2_789, W_181, U_182) | skf23(V_796, X_794, Y_777, Z_787, X1_793, X2_772, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_774, X_792, Y_781, Z_782, X1_795, X2_783, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_788, X_790, Y_786, Z_776, X1_767, X2_789, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_778 | skf23(V_796, X_794, Y_777, Z_787, X1_793, X2_772, W_181, U_182)=X5_778 | skf23(V_774, X_792, Y_781, Z_782, X1_795, X2_783, W_181, U_182)=X5_778 | skf23(V_788, X_790, Y_786, Z_776, X1_767, X2_789, W_181, U_182)=X5_778 | X5_778=U_773 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_773 | skf23(V_796, X_794, Y_777, Z_787, X1_793, X2_772, W_181, U_182)=U_773 | skf23(V_774, X_792, Y_781, Z_782, X1_795, X2_783, W_181, U_182)=U_773 | skf23(V_788, X_790, Y_786, Z_776, X1_767, X2_789, W_181, U_182)=U_773 | ~member(U_182, X5_778, W_181) | ~member(U_182, U_773, W_181) | skf23(U_773, V_784, W_770, X_768, Y_780, Z_779, X1_785, X2_771)!=U_773 | X2_789=X1_767 | Z_776=X1_767 | Z_776=X2_789 | Z_776=Y_786 | Y_786=X1_767 | Y_786=X2_789 | Y_786=X_790 | Z_776=X_790 | X_790=X1_767 | X_790=X2_789 | X_790=V_788 | Y_786=V_788 | Z_776=V_788 | X1_767=V_788 | X2_789=V_788 | ~member(U_182, X2_789, W_181) | ~member(U_182, X1_767, W_181) | ~member(U_182, Z_776, W_181) | ~member(U_182, Y_786, W_181) | ~member(U_182, X_790, W_181) | ~member(U_182, V_788, W_181) | X2_783=X1_795 | Z_782=X1_795 | Z_782=X2_783 | Z_782=Y_781 | Y_781=X1_795 | Y_781=X2_783 | Y_781=X_792 | Z_782=X_792 | X_792=X1_795 | X_792=X2_783 | X_792=V_774 | Y_781=V_774 | Z_782=V_774 | X1_795=V_774 | X2_783=V_774 | ~member(U_182, X2_783, W_181) | ~member(U_182, X1_795, W_181) | ~member(U_182, Z_782, W_181) | ~member(U_182, Y_781, W_181) | ~member(U_182, X_792, W_181) | ~member(U_182, V_774, W_181) | X2_772=X1_793 | Z_787=X1_793 | Z_787=X2_772 | Z_787=Y_777 | Y_777=X1_793 | Y_777=X2_772 | Y_777=X_794 | Z_787=X_794 | X_794=X1_793 | X_794=X2_772 | X_794=V_796 | Y_777=V_796 | Z_787=V_796 | X1_793=V_796 | X2_772=V_796 | ~member(U_182, X2_772, W_181) | ~member(U_182, X1_793, W_181) | ~member(U_182, Z_787, W_181) | ~member(U_182, Y_777, W_181) | ~member(U_182, X_794, W_181) | ~member(U_182, V_796, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_921, plain, (![Z_183, X1_683, W_680, U_673, Z_677, V_678, V_667, X2_185, Y_674, X_684, W_181, X1_676, Y_686, X2_685, X_682, X1_681, X1_184, X2_670, Y_187, V_688, Z_679, X_186, V_188, U_182, X2_671, Z_669, Y_687]: (skf23(V_688, X_684, Y_674, Z_677, X1_683, X2_670, W_181, U_182)=skf23(V_667, X_682, Y_686, Z_669, X1_681, X2_671, W_181, U_182) | skf23(V_688, X_684, Y_674, Z_677, X1_683, X2_670, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_667, X_682, Y_686, Z_669, X1_681, X2_671, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_680 | skf23(V_688, X_684, Y_674, Z_677, X1_683, X2_670, W_181, U_182)=W_680 | skf23(V_667, X_682, Y_686, Z_669, X1_681, X2_671, W_181, U_182)=W_680 | W_680=V_678 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_678 | skf23(V_688, X_684, Y_674, Z_677, X1_683, X2_670, W_181, U_182)=V_678 | skf23(V_667, X_682, Y_686, Z_669, X1_681, X2_671, W_181, U_182)=V_678 | V_678=U_673 | W_680=U_673 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_673 | skf23(V_688, X_684, Y_674, Z_677, X1_683, X2_670, W_181, U_182)=U_673 | skf23(V_667, X_682, Y_686, Z_669, X1_681, X2_671, W_181, U_182)=U_673 | ~member(U_182, W_680, W_181) | ~member(U_182, V_678, W_181) | ~member(U_182, U_673, W_181) | skf23(U_673, V_678, W_680, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), Y_687, Z_679, X1_676, X2_685)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_671=X1_681 | Z_669=X1_681 | Z_669=X2_671 | Z_669=Y_686 | Y_686=X1_681 | Y_686=X2_671 | Y_686=X_682 | Z_669=X_682 | X_682=X1_681 | X_682=X2_671 | X_682=V_667 | Y_686=V_667 | Z_669=V_667 | X1_681=V_667 | X2_671=V_667 | ~member(U_182, X2_671, W_181) | ~member(U_182, X1_681, W_181) | ~member(U_182, Z_669, W_181) | ~member(U_182, Y_686, W_181) | ~member(U_182, X_682, W_181) | ~member(U_182, V_667, W_181) | X2_670=X1_683 | Z_677=X1_683 | Z_677=X2_670 | Z_677=Y_674 | Y_674=X1_683 | Y_674=X2_670 | Y_674=X_684 | Z_677=X_684 | X_684=X1_683 | X_684=X2_670 | X_684=V_688 | Y_674=V_688 | Z_677=V_688 | X1_683=V_688 | X2_670=V_688 | ~member(U_182, X2_670, W_181) | ~member(U_182, X1_683, W_181) | ~member(U_182, Z_677, W_181) | ~member(U_182, Y_674, W_181) | ~member(U_182, X_684, W_181) | ~member(U_182, V_688, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_877, plain, (![V_641, Z_183, Z_631, W_618, X_623, Y_624, X2_185, Y_639, V_628, X1_625, X1_636, X2_632, X2_621, U_626, W_181, Y_629, X5_630, X6_642, X2_620, Z_640, X1_184, X_637, Y_187, V_635, Z_627, X_186, X1_634, V_188, U_182, X_638]: (skf23(V_641, X_638, Y_624, Z_631, X1_636, X2_620, W_181, U_182)=skf23(V_628, X_637, Y_639, Z_640, X1_625, X2_621, W_181, U_182) | skf23(V_641, X_638, Y_624, Z_631, X1_636, X2_620, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_628, X_637, Y_639, Z_640, X1_625, X2_621, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_642 | skf23(V_641, X_638, Y_624, Z_631, X1_636, X2_620, W_181, U_182)=X6_642 | skf23(V_628, X_637, Y_639, Z_640, X1_625, X2_621, W_181, U_182)=X6_642 | X6_642=X5_630 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_630 | skf23(V_641, X_638, Y_624, Z_631, X1_636, X2_620, W_181, U_182)=X5_630 | skf23(V_628, X_637, Y_639, Z_640, X1_625, X2_621, W_181, U_182)=X5_630 | X5_630=U_626 | X6_642=U_626 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_626 | skf23(V_641, X_638, Y_624, Z_631, X1_636, X2_620, W_181, U_182)=U_626 | skf23(V_628, X_637, Y_639, Z_640, X1_625, X2_621, W_181, U_182)=U_626 | ~member(U_182, X6_642, W_181) | ~member(U_182, X5_630, W_181) | ~member(U_182, U_626, W_181) | skf23(U_626, V_635, W_618, X_623, Y_629, Z_627, X1_634, X2_632)!=U_626 | X2_621=X1_625 | Z_640=X1_625 | Z_640=X2_621 | Z_640=Y_639 | Y_639=X1_625 | Y_639=X2_621 | Y_639=X_637 | Z_640=X_637 | X_637=X1_625 | X_637=X2_621 | X_637=V_628 | Y_639=V_628 | Z_640=V_628 | X1_625=V_628 | X2_621=V_628 | ~member(U_182, X2_621, W_181) | ~member(U_182, X1_625, W_181) | ~member(U_182, Z_640, W_181) | ~member(U_182, Y_639, W_181) | ~member(U_182, X_637, W_181) | ~member(U_182, V_628, W_181) | X2_620=X1_636 | Z_631=X1_636 | Z_631=X2_620 | Z_631=Y_624 | Y_624=X1_636 | Y_624=X2_620 | Y_624=X_638 | Z_631=X_638 | X_638=X1_636 | X_638=X2_620 | X_638=V_641 | Y_624=V_641 | Z_631=V_641 | X1_636=V_641 | X2_620=V_641 | ~member(U_182, X2_620, W_181) | ~member(U_182, X1_636, W_181) | ~member(U_182, Z_631, W_181) | ~member(U_182, Y_624, W_181) | ~member(U_182, X_638, W_181) | ~member(U_182, V_641, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_855, plain, (![Z_183, X1_605, X_597, X1_612, X1_601, V_596, Y_603, X_611, V_617, X2_185, X2_598, X_613, V_607, Y_609, Z_610, W_599, Z_606, Y_615, U_616, W_181, X1_184, Y_187, X2_608, X_186, V_188, U_182, X2_600, Z_604]: (skf23(V_617, X_613, Y_603, Z_606, X1_612, X2_600, W_181, U_182)=skf23(V_596, X_597, Y_615, Z_610, X1_605, X2_598, W_181, U_182) | skf23(V_617, X_613, Y_603, Z_606, X1_612, X2_600, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_596, X_597, Y_615, Z_610, X1_605, X2_598, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_599 | skf23(V_617, X_613, Y_603, Z_606, X1_612, X2_600, W_181, U_182)=W_599 | skf23(V_596, X_597, Y_615, Z_610, X1_605, X2_598, W_181, U_182)=W_599 | W_599=V_607 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_607 | skf23(V_617, X_613, Y_603, Z_606, X1_612, X2_600, W_181, U_182)=V_607 | skf23(V_596, X_597, Y_615, Z_610, X1_605, X2_598, W_181, U_182)=V_607 | V_607=U_616 | W_599=U_616 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_616 | skf23(V_617, X_613, Y_603, Z_606, X1_612, X2_600, W_181, U_182)=U_616 | skf23(V_596, X_597, Y_615, Z_610, X1_605, X2_598, W_181, U_182)=U_616 | ~member(U_182, W_599, W_181) | ~member(U_182, V_607, W_181) | ~member(U_182, U_616, W_181) | skf23(U_616, V_607, W_599, X_611, Y_609, Z_604, X1_601, X2_608)!=W_599 | X2_598=X1_605 | Z_610=X1_605 | Z_610=X2_598 | Z_610=Y_615 | Y_615=X1_605 | Y_615=X2_598 | Y_615=X_597 | Z_610=X_597 | X_597=X1_605 | X_597=X2_598 | X_597=V_596 | Y_615=V_596 | Z_610=V_596 | X1_605=V_596 | X2_598=V_596 | ~member(U_182, X2_598, W_181) | ~member(U_182, X1_605, W_181) | ~member(U_182, Z_610, W_181) | ~member(U_182, Y_615, W_181) | ~member(U_182, X_597, W_181) | ~member(U_182, V_596, W_181) | X2_600=X1_612 | Z_606=X1_612 | Z_606=X2_600 | Z_606=Y_603 | Y_603=X1_612 | Y_603=X2_600 | Y_603=X_613 | Z_606=X_613 | X_613=X1_612 | X_613=X2_600 | X_613=V_617 | Y_603=V_617 | Z_606=V_617 | X1_612=V_617 | X2_600=V_617 | ~member(U_182, X2_600, W_181) | ~member(U_182, X1_612, W_181) | ~member(U_182, Z_606, W_181) | ~member(U_182, Y_603, W_181) | ~member(U_182, X_613, W_181) | ~member(U_182, V_617, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_899, plain, (![Z_183, X_655, X2_661, Z_659, X5_649, Z_648, Y_644, X2_185, Z_658, U_660, Y_652, W_181, W_650, X2_647, X_663, V_666, V_665, X1_184, X2_657, Y_187, V_654, X1_656, X_664, X1_645, X_186, V_188, U_182, Y_643, X1_662]: (skf23(V_666, X_664, Y_652, Z_658, X1_662, X2_647, W_181, U_182)=skf23(V_665, X_663, Y_643, Z_648, X1_656, X2_657, W_181, U_182) | skf23(V_666, X_664, Y_652, Z_658, X1_662, X2_647, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_665, X_663, Y_643, Z_648, X1_656, X2_657, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_649 | skf23(V_666, X_664, Y_652, Z_658, X1_662, X2_647, W_181, U_182)=X5_649 | skf23(V_665, X_663, Y_643, Z_648, X1_656, X2_657, W_181, U_182)=X5_649 | X5_649=V_654 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_654 | skf23(V_666, X_664, Y_652, Z_658, X1_662, X2_647, W_181, U_182)=V_654 | skf23(V_665, X_663, Y_643, Z_648, X1_656, X2_657, W_181, U_182)=V_654 | V_654=U_660 | X5_649=U_660 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_660 | skf23(V_666, X_664, Y_652, Z_658, X1_662, X2_647, W_181, U_182)=U_660 | skf23(V_665, X_663, Y_643, Z_648, X1_656, X2_657, W_181, U_182)=U_660 | ~member(U_182, X5_649, W_181) | ~member(U_182, V_654, W_181) | ~member(U_182, U_660, W_181) | skf23(U_660, V_654, W_650, X_655, Y_644, Z_659, X1_645, X2_661)!=V_654 | X2_657=X1_656 | Z_648=X1_656 | Z_648=X2_657 | Z_648=Y_643 | Y_643=X1_656 | Y_643=X2_657 | Y_643=X_663 | Z_648=X_663 | X_663=X1_656 | X_663=X2_657 | X_663=V_665 | Y_643=V_665 | Z_648=V_665 | X1_656=V_665 | X2_657=V_665 | ~member(U_182, X2_657, W_181) | ~member(U_182, X1_656, W_181) | ~member(U_182, Z_648, W_181) | ~member(U_182, Y_643, W_181) | ~member(U_182, X_663, W_181) | ~member(U_182, V_665, W_181) | X2_647=X1_662 | Z_658=X1_662 | Z_658=X2_647 | Z_658=Y_652 | Y_652=X1_662 | Y_652=X2_647 | Y_652=X_664 | Z_658=X_664 | X_664=X1_662 | X_664=X2_647 | X_664=V_666 | Y_652=V_666 | Z_658=V_666 | X1_662=V_666 | X2_647=V_666 | ~member(U_182, X2_647, W_181) | ~member(U_182, X1_662, W_181) | ~member(U_182, Z_658, W_181) | ~member(U_182, Y_652, W_181) | ~member(U_182, X_664, W_181) | ~member(U_182, V_666, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_744, plain, (![Z_183, Y_500, X1_503, X2_498, Z_496, V_504, X1_492, X2_185, X2_505, W_181, X1_184, Y_187, W_497, X_491, X_186, X_494, V_188, U_182, U_490, V_501, Z_493]: (skf23(V_501, X_491, Y_500, Z_493, X1_492, X2_498, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X_494 | skf23(V_501, X_491, Y_500, Z_493, X1_492, X2_498, W_181, U_182)=X_494 | X_494=W_497 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_497 | skf23(V_501, X_491, Y_500, Z_493, X1_492, X2_498, W_181, U_182)=W_497 | W_497=V_504 | X_494=V_504 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_504 | skf23(V_501, X_491, Y_500, Z_493, X1_492, X2_498, W_181, U_182)=V_504 | V_504=U_490 | W_497=U_490 | X_494=U_490 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_490 | skf23(V_501, X_491, Y_500, Z_493, X1_492, X2_498, W_181, U_182)=U_490 | ~member(U_182, X_494, W_181) | ~member(U_182, W_497, W_181) | ~member(U_182, V_504, W_181) | ~member(U_182, U_490, W_181) | skf23(U_490, V_504, W_497, X_494, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), Z_496, X1_503, X2_505)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_498=X1_492 | Z_493=X1_492 | Z_493=X2_498 | Z_493=Y_500 | Y_500=X1_492 | Y_500=X2_498 | Y_500=X_491 | Z_493=X_491 | X_491=X1_492 | X_491=X2_498 | X_491=V_501 | Y_500=V_501 | Z_493=V_501 | X1_492=V_501 | X2_498=V_501 | ~member(U_182, X2_498, W_181) | ~member(U_182, X1_492, W_181) | ~member(U_182, Z_493, W_181) | ~member(U_182, Y_500, W_181) | ~member(U_182, X_491, W_181) | ~member(U_182, V_501, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_766, plain, (![Z_183, X1_514, X1_507, Z_513, V_511, U_510, X2_185, W_520, X2_516, X_506, X2_522, Y_518, W_181, X1_184, Y_187, Z_508, X_186, Y_509, V_188, U_182, V_519, X_515]: (skf23(V_519, X_506, Y_518, Z_508, X1_507, X2_516, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X_515 | skf23(V_519, X_506, Y_518, Z_508, X1_507, X2_516, W_181, U_182)=X_515 | X_515=W_520 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_520 | skf23(V_519, X_506, Y_518, Z_508, X1_507, X2_516, W_181, U_182)=W_520 | W_520=V_511 | X_515=V_511 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_511 | skf23(V_519, X_506, Y_518, Z_508, X1_507, X2_516, W_181, U_182)=V_511 | V_511=U_510 | W_520=U_510 | X_515=U_510 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_510 | skf23(V_519, X_506, Y_518, Z_508, X1_507, X2_516, W_181, U_182)=U_510 | ~member(U_182, X_515, W_181) | ~member(U_182, W_520, W_181) | ~member(U_182, V_511, W_181) | ~member(U_182, U_510, W_181) | skf23(U_510, V_511, W_520, X_515, Y_509, Z_513, X1_514, X2_522)!=X_515 | X2_516=X1_507 | Z_508=X1_507 | Z_508=X2_516 | Z_508=Y_518 | Y_518=X1_507 | Y_518=X2_516 | Y_518=X_506 | Z_508=X_506 | X_506=X1_507 | X_506=X2_516 | X_506=V_519 | Y_518=V_519 | Z_508=V_519 | X1_507=V_519 | X2_516=V_519 | ~member(U_182, X2_516, W_181) | ~member(U_182, X1_507, W_181) | ~member(U_182, Z_508, W_181) | ~member(U_182, Y_518, W_181) | ~member(U_182, X_506, W_181) | ~member(U_182, V_519, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_810, plain, (![Z_183, V_559, X1_546, Y_558, X2_555, X6_548, X1_554, X2_185, U_557, X5_551, Y_552, X_549, X2_553, W_181, W_561, X1_184, Z_547, Y_187, X_186, Z_550, X_545, V_188, U_182, V_543]: (skf23(V_559, X_545, Y_558, Z_547, X1_546, X2_555, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_548 | skf23(V_559, X_545, Y_558, Z_547, X1_546, X2_555, W_181, U_182)=X6_548 | X6_548=X5_551 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_551 | skf23(V_559, X_545, Y_558, Z_547, X1_546, X2_555, W_181, U_182)=X5_551 | X5_551=V_543 | X6_548=V_543 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_543 | skf23(V_559, X_545, Y_558, Z_547, X1_546, X2_555, W_181, U_182)=V_543 | V_543=U_557 | X5_551=U_557 | X6_548=U_557 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_557 | skf23(V_559, X_545, Y_558, Z_547, X1_546, X2_555, W_181, U_182)=U_557 | ~member(U_182, X6_548, W_181) | ~member(U_182, X5_551, W_181) | ~member(U_182, V_543, W_181) | ~member(U_182, U_557, W_181) | skf23(U_557, V_543, W_561, X_549, Y_552, Z_550, X1_554, X2_553)!=V_543 | X2_555=X1_546 | Z_547=X1_546 | Z_547=X2_555 | Z_547=Y_558 | Y_558=X1_546 | Y_558=X2_555 | Y_558=X_545 | Z_547=X_545 | X_545=X1_546 | X_545=X2_555 | X_545=V_559 | Y_558=V_559 | Z_547=V_559 | X1_546=V_559 | X2_555=V_559 | ~member(U_182, X2_555, W_181) | ~member(U_182, X1_546, W_181) | ~member(U_182, Z_547, W_181) | ~member(U_182, Y_558, W_181) | ~member(U_182, X_545, W_181) | ~member(U_182, V_559, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_788, plain, (![Z_183, X1_533, X6_529, W_539, X2_185, Y_538, Z_527, X_535, Y_530, X2_542, W_181, V_540, U_523, X_525, X1_184, Z_532, V_531, Y_187, X5_534, X_186, X1_526, V_188, U_182, X7_524, X2_536]: (skf23(V_540, X_525, Y_538, Z_527, X1_526, X2_536, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X7_524 | skf23(V_540, X_525, Y_538, Z_527, X1_526, X2_536, W_181, U_182)=X7_524 | X7_524=X6_529 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_529 | skf23(V_540, X_525, Y_538, Z_527, X1_526, X2_536, W_181, U_182)=X6_529 | X6_529=X5_534 | X7_524=X5_534 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_534 | skf23(V_540, X_525, Y_538, Z_527, X1_526, X2_536, W_181, U_182)=X5_534 | X5_534=U_523 | X6_529=U_523 | X7_524=U_523 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_523 | skf23(V_540, X_525, Y_538, Z_527, X1_526, X2_536, W_181, U_182)=U_523 | ~member(U_182, X7_524, W_181) | ~member(U_182, X6_529, W_181) | ~member(U_182, X5_534, W_181) | ~member(U_182, U_523, W_181) | skf23(U_523, V_531, W_539, X_535, Y_530, Z_532, X1_533, X2_542)!=U_523 | X2_536=X1_526 | Z_527=X1_526 | Z_527=X2_536 | Z_527=Y_538 | Y_538=X1_526 | Y_538=X2_536 | Y_538=X_525 | Z_527=X_525 | X_525=X1_526 | X_525=X2_536 | X_525=V_540 | Y_538=V_540 | Z_527=V_540 | X1_526=V_540 | X2_536=V_540 | ~member(U_182, X2_536, W_181) | ~member(U_182, X1_526, W_181) | ~member(U_182, Z_527, W_181) | ~member(U_182, Y_538, W_181) | ~member(U_182, X_525, W_181) | ~member(U_182, V_540, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_832, plain, (![Z_183, Y_570, X5_569, X2_566, X2_185, V_568, W_181, U_572, X1_578, X1_184, Y_575, Y_187, Z_577, X_567, X_186, X_563, V_188, U_182, Z_565, X2_573, X1_564, W_562, V_576]: (skf23(V_576, X_563, Y_575, Z_565, X1_564, X2_573, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_569 | skf23(V_576, X_563, Y_575, Z_565, X1_564, X2_573, W_181, U_182)=X5_569 | X5_569=W_562 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_562 | skf23(V_576, X_563, Y_575, Z_565, X1_564, X2_573, W_181, U_182)=W_562 | W_562=V_568 | X5_569=V_568 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_568 | skf23(V_576, X_563, Y_575, Z_565, X1_564, X2_573, W_181, U_182)=V_568 | V_568=U_572 | W_562=U_572 | X5_569=U_572 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_572 | skf23(V_576, X_563, Y_575, Z_565, X1_564, X2_573, W_181, U_182)=U_572 | ~member(U_182, X5_569, W_181) | ~member(U_182, W_562, W_181) | ~member(U_182, V_568, W_181) | ~member(U_182, U_572, W_181) | skf23(U_572, V_568, W_562, X_567, Y_570, Z_577, X1_578, X2_566)!=W_562 | X2_573=X1_564 | Z_565=X1_564 | Z_565=X2_573 | Z_565=Y_575 | Y_575=X1_564 | Y_575=X2_573 | Y_575=X_563 | Z_565=X_563 | X_563=X1_564 | X_563=X2_573 | X_563=V_576 | Y_575=V_576 | Z_565=V_576 | X1_564=V_576 | X2_573=V_576 | ~member(U_182, X2_573, W_181) | ~member(U_182, X1_564, W_181) | ~member(U_182, Z_565, W_181) | ~member(U_182, Y_575, W_181) | ~member(U_182, X_563, W_181) | ~member(U_182, V_576, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.56 tff(c_725, plain, (![U_484, Y_485, X1_193, Y_196, V_197, X_195, W_189, V_489, X1_487, U_191, X2_194, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=Y_196 | Y_196=X_195 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_195 | X_195=W_189 | Y_196=W_189 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_189 | W_189=V_197 | X_195=V_197 | Y_196=V_197 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_197 | V_197=U_191 | W_189=U_191 | X_195=U_191 | Y_196=U_191 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_191 | ~member(U_484, Y_196, W_482) | ~member(U_484, X_195, W_482) | ~member(U_484, W_189, W_482) | ~member(U_484, V_197, W_482) | ~member(U_484, U_191, W_482) | skf23(U_191, V_197, W_189, X_195, Y_196, skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484), X1_193, X2_194)!=skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484) | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_722, plain, (![U_484, Y_485, X6_140, X2_147, X5_139, V_489, X1_487, X1_146, X_148, W_141, Z_144, V_150, Z_486, X_488, X2_483, W_482, U_143, Y_149]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_140 | X6_140=X5_139 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_139 | X5_139=W_141 | X6_140=W_141 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_141 | W_141=V_150 | X5_139=V_150 | X6_140=V_150 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_150 | V_150=U_143 | W_141=U_143 | X5_139=U_143 | X6_140=U_143 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_143 | ~member(U_484, X6_140, W_482) | ~member(U_484, X5_139, W_482) | ~member(U_484, W_141, W_482) | ~member(U_484, V_150, W_482) | ~member(U_484, U_143, W_482) | skf23(U_143, V_150, W_141, X_148, Y_149, Z_144, X1_146, X2_147)!=W_141 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_724, plain, (![U_484, Y_485, X6_153, X2_160, V_163, U_156, Z_157, V_489, W_154, X1_487, X7_158, X5_152, X_161, Y_162, Z_486, X_488, X2_483, W_482, X1_159]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X7_158 | X7_158=X6_153 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_153 | X6_153=X5_152 | X7_158=X5_152 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_152 | X5_152=V_163 | X6_153=V_163 | X7_158=V_163 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_163 | V_163=U_156 | X5_152=U_156 | X6_153=U_156 | X7_158=U_156 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_156 | ~member(U_484, X7_158, W_482) | ~member(U_484, X6_153, W_482) | ~member(U_484, X5_152, W_482) | ~member(U_484, V_163, W_482) | ~member(U_484, U_156, W_482) | skf23(U_156, V_163, W_154, X_161, Y_162, Z_157, X1_159, X2_160)!=V_163 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_723, plain, (![U_484, Y_485, Z_172, X5_166, V_178, X_176, V_489, X1_487, U_170, X6_167, X1_174, Y_177, X7_173, X2_175, X8_179, W_168, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X8_179 | X8_179=X7_173 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X7_173 | X7_173=X6_167 | X8_179=X6_167 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_167 | X6_167=X5_166 | X7_173=X5_166 | X8_179=X5_166 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_166 | X5_166=U_170 | X6_167=U_170 | X7_173=U_170 | X8_179=U_170 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_170 | ~member(U_484, X8_179, W_482) | ~member(U_484, X7_173, W_482) | ~member(U_484, X6_167, W_482) | ~member(U_484, X5_166, W_482) | ~member(U_484, U_170, W_482) | skf23(U_170, V_178, W_168, X_176, Y_177, Z_172, X1_174, X2_175)!=U_170 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_721, plain, (![U_484, Y_485, Y_136, V_137, X5_127, X1_133, V_489, W_129, X1_487, Z_132, X_135, X2_134, Z_486, X_488, X2_483, W_482, U_131]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_127 | X_135=X5_127 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_135 | X_135=W_129 | X5_127=W_129 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_129 | W_129=V_137 | X_135=V_137 | X5_127=V_137 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_137 | V_137=U_131 | W_129=U_131 | X_135=U_131 | X5_127=U_131 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_131 | ~member(U_484, X5_127, W_482) | ~member(U_484, X_135, W_482) | ~member(U_484, W_129, W_482) | ~member(U_484, V_137, W_482) | ~member(U_484, U_131, W_482) | skf23(U_131, V_137, W_129, X_135, Y_136, Z_132, X1_133, X2_134)!=X_135 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_720, plain, (![U_484, Y_485, X_206, X1_204, W_200, V_208, V_489, X2_205, X1_487, U_202, Y_207, Z_203, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=Y_207 | Y_207=X_206 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_206 | X_206=W_200 | Y_207=W_200 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_202 | ~member(U_484, Y_207, W_482) | ~member(U_484, X_206, W_482) | ~member(U_484, W_200, W_482) | ~member(U_484, V_208, W_482) | ~member(U_484, U_202, W_482) | skf23(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Y_207 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 60.33/51.57 tff(c_134, plain, (![Z_183, X2_185, W_181, X1_184, Y_187, X_186, V_188, U_182]: (X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | member(U_182, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), W_181) | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 60.33/51.57 tff(c_138, plain, (![X3_201, X_206, X1_204, W_200, V_208, X2_205, X4_209, U_202, Y_207, X5_199, Z_203]: (Y_207=X5_199 | Y_207=X_206 | X_206=X5_199 | X_206=W_200 | Y_207=W_200 | X5_199=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | X5_199=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | X5_199=U_202 | six(X3_201, X4_209) | ~member(X3_201, X5_199, 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) | skf23(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Y_207))). % 60.33/51.57 tff(c_126, plain, (![X4_138, Y_136, V_137, X5_127, X1_133, W_129, X3_130, Z_132, X_135, X2_134, X6_128, U_131]: (X6_128=X5_127 | X_135=X5_127 | X_135=X6_128 | X_135=W_129 | X5_127=W_129 | X6_128=W_129 | W_129=V_137 | X_135=V_137 | X5_127=V_137 | X6_128=V_137 | V_137=U_131 | W_129=U_131 | X_135=U_131 | X5_127=U_131 | X6_128=U_131 | six(X3_130, X4_138) | ~member(X3_130, X6_128, X4_138) | ~member(X3_130, X5_127, X4_138) | ~member(X3_130, X_135, X4_138) | ~member(X3_130, W_129, X4_138) | ~member(X3_130, V_137, X4_138) | ~member(X3_130, U_131, X4_138) | skf23(U_131, V_137, W_129, X_135, Y_136, Z_132, X1_133, X2_134)!=X_135))). % 60.33/51.57 tff(c_128, plain, (![X4_151, X6_140, X2_147, X5_139, X3_142, X1_146, X_148, W_141, Z_144, V_150, U_143, X7_145, Y_149]: (X7_145=X6_140 | X6_140=X5_139 | X7_145=X5_139 | X5_139=W_141 | X6_140=W_141 | X7_145=W_141 | W_141=V_150 | X5_139=V_150 | X6_140=V_150 | X7_145=V_150 | V_150=U_143 | W_141=U_143 | X5_139=U_143 | X6_140=U_143 | X7_145=U_143 | six(X3_142, X4_151) | ~member(X3_142, X7_145, X4_151) | ~member(X3_142, X6_140, X4_151) | ~member(X3_142, X5_139, X4_151) | ~member(X3_142, W_141, X4_151) | ~member(X3_142, V_150, X4_151) | ~member(X3_142, U_143, X4_151) | skf23(U_143, V_150, W_141, X_148, Y_149, Z_144, X1_146, X2_147)!=W_141))). % 60.33/51.57 tff(c_132, plain, (![Z_172, X3_169, X5_166, X4_180, V_178, X_176, X9_171, U_170, X6_167, X1_174, Y_177, X7_173, X2_175, X8_179, W_168]: (X9_171=X8_179 | X8_179=X7_173 | X9_171=X7_173 | X7_173=X6_167 | X8_179=X6_167 | X9_171=X6_167 | X6_167=X5_166 | X7_173=X5_166 | X8_179=X5_166 | X9_171=X5_166 | X5_166=U_170 | X6_167=U_170 | X7_173=U_170 | X8_179=U_170 | X9_171=U_170 | six(X3_169, X4_180) | ~member(X3_169, X9_171, X4_180) | ~member(X3_169, X8_179, X4_180) | ~member(X3_169, X7_173, X4_180) | ~member(X3_169, X6_167, X4_180) | ~member(X3_169, X5_166, X4_180) | ~member(X3_169, U_170, X4_180) | skf23(U_170, V_178, W_168, X_176, Y_177, Z_172, X1_174, X2_175)!=U_170))). % 60.33/51.57 tff(c_130, plain, (![X6_153, X2_160, V_163, U_156, Z_157, W_154, X7_158, X8_164, X5_152, X_161, Y_162, X3_155, X1_159, X4_165]: (X8_164=X7_158 | X7_158=X6_153 | X8_164=X6_153 | X6_153=X5_152 | X7_158=X5_152 | X8_164=X5_152 | X5_152=V_163 | X6_153=V_163 | X7_158=V_163 | X8_164=V_163 | V_163=U_156 | X5_152=U_156 | X6_153=U_156 | X7_158=U_156 | X8_164=U_156 | six(X3_155, X4_165) | ~member(X3_155, X8_164, X4_165) | ~member(X3_155, X7_158, X4_165) | ~member(X3_155, X6_153, X4_165) | ~member(X3_155, X5_152, X4_165) | ~member(X3_155, V_163, X4_165) | ~member(X3_155, U_156, X4_165) | skf23(U_156, V_163, W_154, X_161, Y_162, Z_157, X1_159, X2_160)!=V_163))). % 60.33/51.57 tff(c_136, plain, (![X1_193, Y_196, V_197, X_195, X3_190, W_189, Z_192, U_191, X2_194, X4_198]: (Z_192=Y_196 | Y_196=X_195 | Z_192=X_195 | X_195=W_189 | Y_196=W_189 | Z_192=W_189 | W_189=V_197 | X_195=V_197 | Y_196=V_197 | Z_192=V_197 | V_197=U_191 | W_189=U_191 | X_195=U_191 | Y_196=U_191 | Z_192=U_191 | six(X3_190, X4_198) | ~member(X3_190, Z_192, X4_198) | ~member(X3_190, Y_196, X4_198) | ~member(X3_190, X_195, X4_198) | ~member(X3_190, W_189, X4_198) | ~member(X3_190, V_197, X4_198) | ~member(X3_190, U_191, X4_198) | skf23(U_191, V_197, W_189, X_195, Y_196, Z_192, X1_193, X2_194)!=Z_192))). % 60.33/51.57 tff(c_124, plain, (![W_126, U_124, V_125]: (skf22(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 | ~six(U_124, W_126) | ~member(U_124, V_125, W_126)))). % 60.33/51.57 tff(c_553, plain, (![U_213]: (~of(skc3, U_213, skc5) | ~cannon(skc3, U_213) | ~member(skc3, U_213, skc4)))). % 60.33/51.57 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)))). % 60.33/51.57 tff(c_551, plain, (skf22(skc4, skc3)!=skf16(skc4, skc3))). % 60.33/51.57 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf22(U_95, V_96)!=skf16(U_95, V_96)))). % 60.33/51.57 tff(c_546, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 60.33/51.57 tff(c_541, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 60.33/51.57 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf16(U_117, V_118)!=skf14(U_117, V_118)))). % 60.33/51.57 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf16(U_113, V_114)))). % 60.33/51.57 tff(c_536, plain, (skf22(skc4, skc3)!=skf12(skc4, skc3))). % 60.33/51.57 tff(c_531, plain, (skf22(skc4, skc3)!=skf18(skc4, skc3))). % 60.33/51.57 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf22(U_91, V_92)!=skf12(U_91, V_92)))). % 60.33/51.57 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf22(U_97, V_98)!=skf18(U_97, V_98)))). % 60.33/51.57 tff(c_510, plain, (skf20(skc4, skc3)!=skf12(skc4, skc3))). % 60.33/51.57 tff(c_526, plain, (act(skc3, skf12(skc4, skc3)))). % 60.33/51.57 tff(c_522, plain, (action(skc3, skf12(skc4, skc3)))). % 60.33/51.57 tff(c_518, plain, (shot(skc3, skf12(skc4, skc3)))). % 60.33/51.57 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf12(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 60.33/51.57 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf12(U_101, V_102)))). % 60.33/51.57 tff(c_499, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.33/51.57 tff(c_504, plain, (skf22(skc4, skc3)!=skf14(skc4, skc3))). % 60.33/51.57 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf22(U_93, V_94)!=skf14(U_93, V_94)))). % 60.33/51.57 tff(c_494, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 60.33/51.57 tff(c_402, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 60.33/51.57 tff(c_485, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 60.33/51.57 tff(c_489, plain, (~act(skc3, skc4))). % 60.33/51.57 tff(c_480, plain, (~event(skc3, skc4))). % 60.33/51.57 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf14(U_103, V_104)))). % 60.33/51.57 tff(c_476, plain, (~eventuality(skc3, skc4))). % 60.33/51.57 tff(c_412, plain, (![U_251, V_252]: (~eventuality(U_251, V_252) | ~group(U_251, V_252)))). % 60.33/51.57 tff(c_471, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 60.33/51.57 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf18(U_107, V_108)))). % 60.33/51.57 tff(c_397, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 60.33/51.57 tff(c_417, plain, (![U_356, V_357]: (artifact(U_356, V_357) | ~cannon(U_356, V_357)))). % 60.33/51.57 tff(c_464, plain, (act(skc3, skf16(skc4, skc3)))). % 60.33/51.57 tff(c_460, plain, (action(skc3, skf16(skc4, skc3)))). % 60.33/51.57 tff(c_456, plain, (shot(skc3, skf16(skc4, skc3)))). % 60.33/51.57 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf16(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 60.33/51.57 tff(c_444, plain, (skf16(skc4, skc3)!=skf12(skc4, skc3))). % 60.33/51.57 tff(c_448, plain, (~artifact(skc3, skc4))). % 60.33/51.57 tff(c_439, plain, (~entity(skc3, skc4))). % 60.33/51.57 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf16(U_115, V_116)!=skf12(U_115, V_116)))). % 60.33/51.57 tff(c_366, plain, (![U_251, V_252]: (~entity(U_251, V_252) | ~group(U_251, V_252)))). % 60.33/51.57 tff(c_355, plain, (![U_334, V_335]: (~animate(U_334, V_335) | ~artifact(U_334, V_335)))). % 60.33/51.57 tff(c_433, plain, (act(skc3, skf18(skc4, skc3)))). % 60.33/51.57 tff(c_429, plain, (action(skc3, skf18(skc4, skc3)))). % 60.33/51.57 tff(c_425, plain, (shot(skc3, skf18(skc4, skc3)))). % 60.33/51.57 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf18(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 60.33/51.57 tff(c_360, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 60.33/51.57 tff(c_268, plain, (![U_308, V_309]: (~multiple(U_308, V_309) | ~eventuality(U_308, V_309)))). % 60.33/51.57 tff(c_407, plain, (skf14(skc4, skc3)!=skf12(skc4, skc3))). % 60.33/51.57 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf14(U_119, V_120)!=skf12(U_119, V_120)))). % 60.33/51.57 tff(c_330, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 60.33/51.57 tff(c_354, plain, (![U_334, V_335]: (~living(U_334, V_335) | ~artifact(U_334, V_335)))). % 60.33/51.57 tff(c_392, plain, (act(skc3, skf22(skc4, skc3)))). % 60.33/51.57 tff(c_388, plain, (action(skc3, skf22(skc4, skc3)))). % 60.33/51.57 tff(c_384, plain, (shot(skc3, skf22(skc4, skc3)))). % 60.33/51.57 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf22(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 60.33/51.57 tff(c_376, plain, (~artifact(skc3, skc5))). % 60.33/51.57 tff(c_274, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.57/51.57 tff(c_371, plain, (skf22(skc4, skc3)!=skf20(skc4, skc3))). % 60.57/51.58 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf22(U_99, V_100)!=skf20(U_99, V_100)))). % 60.57/51.58 tff(c_341, plain, (![U_330, V_331]: (~multiple(U_330, V_331) | ~entity(U_330, V_331)))). % 60.57/51.58 tff(c_346, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 60.57/51.58 tff(c_185, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.57/51.58 tff(c_179, plain, (![U_245, V_246]: (instrumentality(U_245, V_246) | ~weapon(U_245, V_246)))). % 60.57/51.58 tff(c_214, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.57/51.58 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf16(U_105, V_106)))). % 60.57/51.58 tff(c_279, plain, (skf18(skc4, skc3)!=skf12(skc4, skc3))). % 60.57/51.58 tff(c_336, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 60.57/51.58 tff(c_208, plain, (![U_261, V_262]: (singleton(U_261, V_262) | ~entity(U_261, V_262)))). % 60.57/51.58 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf14(U_111, V_112)))). % 60.57/51.58 tff(c_224, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.57/51.58 tff(c_229, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 60.57/51.58 tff(c_325, plain, (act(skc3, skf14(skc4, skc3)))). % 60.57/51.58 tff(c_321, plain, (action(skc3, skf14(skc4, skc3)))). % 60.57/51.58 tff(c_317, plain, (shot(skc3, skf14(skc4, skc3)))). % 60.57/51.58 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf14(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 60.57/51.58 tff(c_309, plain, (act(skc3, skf20(skc4, skc3)))). % 60.57/51.58 tff(c_305, plain, (action(skc3, skf20(skc4, skc3)))). % 60.57/51.58 tff(c_301, plain, (shot(skc3, skf20(skc4, skc3)))). % 60.57/51.58 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf20(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 60.57/51.58 tff(c_190, plain, (![U_251, V_252]: (multiple(U_251, V_252) | ~group(U_251, V_252)))). % 60.57/51.58 tff(c_292, plain, (~act(skc3, skc5))). % 60.57/51.58 tff(c_288, plain, (~event(skc3, skc5))). % 60.57/51.58 tff(c_284, plain, (~eventuality(skc3, skc5))). % 60.57/51.58 tff(c_240, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 60.57/51.58 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf18(U_109, V_110)!=skf12(U_109, V_110)))). % 60.57/51.58 tff(c_239, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 60.57/51.58 tff(c_257, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 60.57/51.58 tff(c_203, plain, (![U_259, V_260]: (singleton(U_259, V_260) | ~eventuality(U_259, V_260)))). % 60.57/51.58 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 60.57/51.58 tff(c_252, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 60.57/51.58 tff(c_246, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 60.57/51.58 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 60.57/51.58 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 60.57/51.58 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 60.57/51.58 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 60.57/51.58 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 60.57/51.58 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 60.57/51.58 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 60.57/51.58 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 60.57/51.58 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 60.57/51.58 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 60.57/51.58 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 60.57/51.58 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 60.57/51.58 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 60.57/51.58 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 60.57/51.58 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 60.57/51.58 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 60.57/51.58 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 60.57/51.58 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 60.57/51.58 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 60.57/51.58 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 60.57/51.58 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 60.57/51.58 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 60.57/51.58 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 60.57/51.58 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 60.57/51.58 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 60.57/51.58 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 60.57/51.58 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 60.57/51.58 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 60.57/51.58 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 60.57/51.58 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 60.57/51.58 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 60.57/51.58 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 60.57/51.58 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 60.57/51.58 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 60.57/51.58 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 60.57/51.58 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 60.57/51.58 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 60.57/51.58 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 60.57/51.58 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 60.57/51.58 tff(c_142, plain, (male(skc3, skc5))). % 60.57/51.58 tff(c_146, plain, (six(skc3, skc4))). % 60.57/51.58 tff(c_144, plain, (group(skc3, skc4))). % 60.57/51.58 tff(c_140, plain, (actual_world(skc3))). % 60.57/51.58 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 60.57/51.58 %------------------------------------------------------------------------------