%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP069-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 : n025.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 61.98s 52.94s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP069-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/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.13/0.35 % Computer : n025.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Apr 8 08:21:50 EDT 2025 % 0.13/0.35 % CPUTime : % 61.98/52.94 % 61.98/52.94 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.98/52.94 % 61.98/52.94 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.01/52.95 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf21 > skf8 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc5 > skc4 > skc3 % 62.01/52.95 % 62.01/52.95 %Foreground sorts: % 62.01/52.95 % 62.01/52.95 % 62.01/52.95 %Background operators: % 62.01/52.95 % 62.01/52.95 % 62.01/52.95 %Foreground operators: % 62.01/52.95 tff(nonliving, type, nonliving: ($i * $i) > $o). % 62.01/52.95 tff(skf10, type, skf10: ($i * $i) > $i). % 62.01/52.95 tff(member, type, member: ($i * $i * $i) > $o). % 62.01/52.95 tff(living, type, living: ($i * $i) > $o). % 62.01/52.95 tff(fire, type, fire: ($i * $i) > $o). % 62.01/52.95 tff(human_person, type, human_person: ($i * $i) > $o). % 62.01/52.95 tff(action, type, action: ($i * $i) > $o). % 62.01/52.95 tff(present, type, present: ($i * $i) > $o). % 62.01/52.95 tff(shot, type, shot: ($i * $i) > $o). % 62.01/52.95 tff(entity, type, entity: ($i * $i) > $o). % 62.01/52.95 tff(eventuality, type, eventuality: ($i * $i) > $o). % 62.01/52.95 tff(weapon, type, weapon: ($i * $i) > $o). % 62.01/52.95 tff(existent, type, existent: ($i * $i) > $o). % 62.01/52.95 tff(singleton, type, singleton: ($i * $i) > $o). % 62.01/52.95 tff(male, type, male: ($i * $i) > $o). % 62.01/52.95 tff(multiple, type, multiple: ($i * $i) > $o). % 62.01/52.95 tff(organism, type, organism: ($i * $i) > $o). % 62.01/52.95 tff(animate, type, animate: ($i * $i) > $o). % 62.01/52.95 tff(of, type, of: ($i * $i * $i) > $o). % 62.01/52.95 tff(skf14, type, skf14: ($i * $i) > $i). % 62.01/52.95 tff(actual_world, type, actual_world: $i > $o). % 62.01/52.95 tff(agent, type, agent: ($i * $i * $i) > $o). % 62.01/52.95 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 62.01/52.95 tff(group, type, group: ($i * $i) > $o). % 62.01/52.95 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 62.01/52.95 tff(artifact, type, artifact: ($i * $i) > $o). % 62.01/52.95 tff(cannon, type, cannon: ($i * $i) > $o). % 62.01/52.95 tff(event, type, event: ($i * $i) > $o). % 62.01/52.95 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 62.01/52.95 tff(patient, type, patient: ($i * $i * $i) > $o). % 62.01/52.95 tff(skf8, type, skf8: ($i * $i) > $i). % 62.01/52.95 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 62.01/52.95 tff(skc4, type, skc4: $i). % 62.01/52.95 tff(skc3, type, skc3: $i). % 62.01/52.95 tff(thing, type, thing: ($i * $i) > $o). % 62.01/52.95 tff(human, type, human: ($i * $i) > $o). % 62.01/52.95 tff(six, type, six: ($i * $i) > $o). % 62.01/52.95 tff(skf18, type, skf18: ($i * $i) > $i). % 62.01/52.95 tff(man, type, man: ($i * $i) > $o). % 62.01/52.95 tff(skc5, type, skc5: $i). % 62.01/52.95 tff(weaponry, type, weaponry: ($i * $i) > $o). % 62.01/52.95 tff(unisex, type, unisex: ($i * $i) > $o). % 62.01/52.95 tff(skf16, type, skf16: ($i * $i) > $i). % 62.01/52.95 tff(set, type, set: ($i * $i) > $o). % 62.01/52.95 tff(skf12, type, skf12: ($i * $i) > $i). % 62.01/52.95 tff(impartial, type, impartial: ($i * $i) > $o). % 62.01/52.95 tff(object, type, object: ($i * $i) > $o). % 62.01/52.95 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 62.01/52.95 tff(specific, type, specific: ($i * $i) > $o). % 62.01/52.95 tff(skf20, type, skf20: ($i * $i) > $i). % 62.01/52.95 tff(act, type, act: ($i * $i) > $o). % 62.01/52.95 % 62.01/52.95 %Saturated clause set: % 62.01/52.95 tff(c_1054, plain, (![X1_944, X_974, X_948, Z_194, X2_950, V_199, V_951, Z_936, X2_941, X2_196, X_973, X1_970, V_966, Y_952, Y_963, V_972, Y_956, Y_967, W_192, V_969, X1_940, Z_957, X1_195, X1_961, Z_953, W_968, Z_945, X2_965, Y_946, X_943, X_197, Y_198, X2_947, X1_954, V_960, U_193, X2_937, X1_942, Z_935, V_964, X_939, Z_962, X2_938, Y_949, X_955]: (skf21(V_964, X_955, Y_949, Z_935, X1_954, X2_947, W_192, U_193)=skf21(V_951, X_943, Y_952, Z_936, X1_940, X2_937, W_192, U_193) | skf21(V_972, X_973, Y_967, Z_953, X1_961, X2_965, W_192, U_193)=skf21(V_964, X_955, Y_949, Z_935, X1_954, X2_947, W_192, U_193) | skf21(V_972, X_973, Y_967, Z_953, X1_961, X2_965, W_192, U_193)=skf21(V_951, X_943, Y_952, Z_936, X1_940, X2_937, W_192, U_193) | skf21(V_972, X_973, Y_967, Z_953, X1_961, X2_965, W_192, U_193)=skf21(V_969, X_948, Y_956, Z_945, X1_944, X2_941, W_192, U_193) | skf21(V_969, X_948, Y_956, Z_945, X1_944, X2_941, W_192, U_193)=skf21(V_964, X_955, Y_949, Z_935, X1_954, X2_947, W_192, U_193) | skf21(V_969, X_948, Y_956, Z_945, X1_944, X2_941, W_192, U_193)=skf21(V_951, X_943, Y_952, Z_936, X1_940, X2_937, W_192, U_193) | skf21(V_969, X_948, Y_956, Z_945, X1_944, X2_941, W_192, U_193)=skf21(V_960, X_974, Y_963, Z_957, X1_942, X2_938, W_192, U_193) | skf21(V_972, X_973, Y_967, Z_953, X1_961, X2_965, W_192, U_193)=skf21(V_960, X_974, Y_963, Z_957, X1_942, X2_938, W_192, U_193) | skf21(V_964, X_955, Y_949, Z_935, X1_954, X2_947, W_192, U_193)=skf21(V_960, X_974, Y_963, Z_957, X1_942, X2_938, W_192, U_193) | skf21(V_960, X_974, Y_963, Z_957, X1_942, X2_938, W_192, U_193)=skf21(V_951, X_943, Y_952, Z_936, X1_940, X2_937, W_192, U_193) | skf21(V_960, X_974, Y_963, Z_957, X1_942, X2_938, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_969, X_948, Y_956, Z_945, X1_944, X2_941, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_972, X_973, Y_967, Z_953, X1_961, X2_965, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_964, X_955, Y_949, Z_935, X1_954, X2_947, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_951, X_943, Y_952, Z_936, X1_940, X2_937, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), V_966, W_968, X_939, Y_946, Z_962, X1_970, X2_950)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_937=X1_940 | Z_936=X1_940 | Z_936=X2_937 | Z_936=Y_952 | Y_952=X1_940 | Y_952=X2_937 | Y_952=X_943 | Z_936=X_943 | X_943=X1_940 | X_943=X2_937 | X_943=V_951 | Y_952=V_951 | Z_936=V_951 | X1_940=V_951 | X2_937=V_951 | ~member(U_193, X2_937, W_192) | ~member(U_193, X1_940, W_192) | ~member(U_193, Z_936, W_192) | ~member(U_193, Y_952, W_192) | ~member(U_193, X_943, W_192) | ~member(U_193, V_951, W_192) | X2_947=X1_954 | Z_935=X1_954 | Z_935=X2_947 | Z_935=Y_949 | Y_949=X1_954 | Y_949=X2_947 | Y_949=X_955 | Z_935=X_955 | X_955=X1_954 | X_955=X2_947 | X_955=V_964 | Y_949=V_964 | Z_935=V_964 | X1_954=V_964 | X2_947=V_964 | ~member(U_193, X2_947, W_192) | ~member(U_193, X1_954, W_192) | ~member(U_193, Z_935, W_192) | ~member(U_193, Y_949, W_192) | ~member(U_193, X_955, W_192) | ~member(U_193, V_964, W_192) | X2_965=X1_961 | Z_953=X1_961 | Z_953=X2_965 | Z_953=Y_967 | Y_967=X1_961 | Y_967=X2_965 | Y_967=X_973 | Z_953=X_973 | X_973=X1_961 | X_973=X2_965 | X_973=V_972 | Y_967=V_972 | Z_953=V_972 | X1_961=V_972 | X2_965=V_972 | ~member(U_193, X2_965, W_192) | ~member(U_193, X1_961, W_192) | ~member(U_193, Z_953, W_192) | ~member(U_193, Y_967, W_192) | ~member(U_193, X_973, W_192) | ~member(U_193, V_972, W_192) | X2_941=X1_944 | Z_945=X1_944 | Z_945=X2_941 | Z_945=Y_956 | Y_956=X1_944 | Y_956=X2_941 | Y_956=X_948 | Z_945=X_948 | X_948=X1_944 | X_948=X2_941 | X_948=V_969 | Y_956=V_969 | Z_945=V_969 | X1_944=V_969 | X2_941=V_969 | ~member(U_193, X2_941, W_192) | ~member(U_193, X1_944, W_192) | ~member(U_193, Z_945, W_192) | ~member(U_193, Y_956, W_192) | ~member(U_193, X_948, W_192) | ~member(U_193, V_969, W_192) | X2_938=X1_942 | Z_957=X1_942 | Z_957=X2_938 | Z_957=Y_963 | Y_963=X1_942 | Y_963=X2_938 | Y_963=X_974 | Z_957=X_974 | X_974=X1_942 | X_974=X2_938 | X_974=V_960 | Y_963=V_960 | Z_957=V_960 | X1_942=V_960 | X2_938=V_960 | ~member(U_193, X2_938, W_192) | ~member(U_193, X1_942, W_192) | ~member(U_193, Z_957, W_192) | ~member(U_193, Y_963, W_192) | ~member(U_193, X_974, W_192) | ~member(U_193, V_960, 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)))). % 62.01/52.96 tff(c_1009, plain, (![V_861, V_851, W_844, Z_865, X_866, X2_836, X_854, Z_194, U_846, V_199, X1_840, X1_853, Z_838, X2_196, V_860, X1_837, Z_863, Y_855, X1_845, W_192, X_839, X1_195, X2_841, X2_856, X2_834, V_835, Z_858, X_857, X1_862, Y_848, X_197, Y_198, X_852, Z_847, Y_859, U_193, Y_842, Y_833, X2_864]: (skf21(V_861, X_857, Y_842, Z_863, X1_853, X2_841, W_192, U_193)=skf21(V_860, X_854, Y_833, Z_838, X1_845, X2_856, W_192, U_193) | skf21(V_861, X_857, Y_842, Z_863, X1_853, X2_841, W_192, U_193)=skf21(V_835, X_839, Y_848, Z_858, X1_840, X2_836, W_192, U_193) | skf21(V_860, X_854, Y_833, Z_838, X1_845, X2_856, W_192, U_193)=skf21(V_835, X_839, Y_848, Z_858, X1_840, X2_836, W_192, U_193) | skf21(V_851, X_866, Y_855, Z_847, X1_837, X2_834, W_192, U_193)=skf21(V_835, X_839, Y_848, Z_858, X1_840, X2_836, W_192, U_193) | skf21(V_861, X_857, Y_842, Z_863, X1_853, X2_841, W_192, U_193)=skf21(V_851, X_866, Y_855, Z_847, X1_837, X2_834, W_192, U_193) | skf21(V_860, X_854, Y_833, Z_838, X1_845, X2_856, W_192, U_193)=skf21(V_851, X_866, Y_855, Z_847, X1_837, X2_834, W_192, U_193) | skf21(V_851, X_866, Y_855, Z_847, X1_837, X2_834, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_835, X_839, Y_848, Z_858, X1_840, X2_836, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_861, X_857, Y_842, Z_863, X1_853, X2_841, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_860, X_854, Y_833, Z_838, X1_845, X2_856, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_846 | skf21(V_851, X_866, Y_855, Z_847, X1_837, X2_834, W_192, U_193)=U_846 | skf21(V_835, X_839, Y_848, Z_858, X1_840, X2_836, W_192, U_193)=U_846 | skf21(V_861, X_857, Y_842, Z_863, X1_853, X2_841, W_192, U_193)=U_846 | skf21(V_860, X_854, Y_833, Z_838, X1_845, X2_856, W_192, U_193)=U_846 | ~member(U_193, U_846, W_192) | skf21(U_846, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_844, X_852, Y_859, Z_865, X1_862, X2_864)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_856=X1_845 | Z_838=X1_845 | Z_838=X2_856 | Z_838=Y_833 | Y_833=X1_845 | Y_833=X2_856 | Y_833=X_854 | Z_838=X_854 | X_854=X1_845 | X_854=X2_856 | X_854=V_860 | Y_833=V_860 | Z_838=V_860 | X1_845=V_860 | X2_856=V_860 | ~member(U_193, X2_856, W_192) | ~member(U_193, X1_845, W_192) | ~member(U_193, Z_838, W_192) | ~member(U_193, Y_833, W_192) | ~member(U_193, X_854, W_192) | ~member(U_193, V_860, W_192) | X2_841=X1_853 | Z_863=X1_853 | Z_863=X2_841 | Z_863=Y_842 | Y_842=X1_853 | Y_842=X2_841 | Y_842=X_857 | Z_863=X_857 | X_857=X1_853 | X_857=X2_841 | X_857=V_861 | Y_842=V_861 | Z_863=V_861 | X1_853=V_861 | X2_841=V_861 | ~member(U_193, X2_841, W_192) | ~member(U_193, X1_853, W_192) | ~member(U_193, Z_863, W_192) | ~member(U_193, Y_842, W_192) | ~member(U_193, X_857, W_192) | ~member(U_193, V_861, W_192) | X2_836=X1_840 | Z_858=X1_840 | Z_858=X2_836 | Z_858=Y_848 | Y_848=X1_840 | Y_848=X2_836 | Y_848=X_839 | Z_858=X_839 | X_839=X1_840 | X_839=X2_836 | X_839=V_835 | Y_848=V_835 | Z_858=V_835 | X1_840=V_835 | X2_836=V_835 | ~member(U_193, X2_836, W_192) | ~member(U_193, X1_840, W_192) | ~member(U_193, Z_858, W_192) | ~member(U_193, Y_848, W_192) | ~member(U_193, X_839, W_192) | ~member(U_193, V_835, W_192) | X2_834=X1_837 | Z_847=X1_837 | Z_847=X2_834 | Z_847=Y_855 | Y_855=X1_837 | Y_855=X2_834 | Y_855=X_866 | Z_847=X_866 | X_866=X1_837 | X_866=X2_834 | X_866=V_851 | Y_855=V_851 | Z_847=V_851 | X1_837=V_851 | X2_834=V_851 | ~member(U_193, X2_834, W_192) | ~member(U_193, X1_837, W_192) | ~member(U_193, Z_847, W_192) | ~member(U_193, Y_855, W_192) | ~member(U_193, X_866, W_192) | ~member(U_193, V_851, 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)))). % 62.01/52.96 tff(c_1031, plain, (![W_894, Y_878, X1_885, X_880, Z_194, V_199, V_900, X1_881, U_875, X2_196, X_883, Z_886, X1_871, X2_892, V_890, Y_876, W_192, X2_895, X2_884, X1_195, Z_867, V_891, X1_897, X_869, X_197, Y_198, Z_872, U_193, Y_893, V_896, Z_877, X_901, X_870, Z_899, Y_887, Y_882, X2_879, X2_868, X1_898, V_874]: (skf21(V_891, X_883, Y_878, Z_867, X1_898, X2_879, W_192, U_193)=skf21(V_874, X_870, Y_887, Z_899, X1_885, X2_884, W_192, U_193) | skf21(V_900, X_880, Y_876, Z_872, X1_897, X2_895, W_192, U_193)=skf21(V_874, X_870, Y_887, Z_899, X1_885, X2_884, W_192, U_193) | skf21(V_900, X_880, Y_876, Z_872, X1_897, X2_895, W_192, U_193)=skf21(V_891, X_883, Y_878, Z_867, X1_898, X2_879, W_192, U_193) | skf21(V_900, X_880, Y_876, Z_872, X1_897, X2_895, W_192, U_193)=skf21(V_890, X_901, Y_893, Z_886, X1_871, X2_868, W_192, U_193) | skf21(V_890, X_901, Y_893, Z_886, X1_871, X2_868, W_192, U_193)=skf21(V_874, X_870, Y_887, Z_899, X1_885, X2_884, W_192, U_193) | skf21(V_891, X_883, Y_878, Z_867, X1_898, X2_879, W_192, U_193)=skf21(V_890, X_901, Y_893, Z_886, X1_871, X2_868, W_192, U_193) | skf21(V_890, X_901, Y_893, Z_886, X1_871, X2_868, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_900, X_880, Y_876, Z_872, X1_897, X2_895, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_874, X_870, Y_887, Z_899, X1_885, X2_884, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_891, X_883, Y_878, Z_867, X1_898, X2_879, 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_875 | skf21(V_890, X_901, Y_893, Z_886, X1_871, X2_868, W_192, U_193)=U_875 | skf21(V_900, X_880, Y_876, Z_872, X1_897, X2_895, W_192, U_193)=U_875 | skf21(V_874, X_870, Y_887, Z_899, X1_885, X2_884, W_192, U_193)=U_875 | skf21(V_891, X_883, Y_878, Z_867, X1_898, X2_879, W_192, U_193)=U_875 | ~member(U_193, U_875, W_192) | skf21(U_875, V_896, W_894, X_869, Y_882, Z_877, X1_881, X2_892)!=U_875 | X2_879=X1_898 | Z_867=X1_898 | Z_867=X2_879 | Z_867=Y_878 | Y_878=X1_898 | Y_878=X2_879 | Y_878=X_883 | Z_867=X_883 | X_883=X1_898 | X_883=X2_879 | X_883=V_891 | Y_878=V_891 | Z_867=V_891 | X1_898=V_891 | X2_879=V_891 | ~member(U_193, X2_879, W_192) | ~member(U_193, X1_898, W_192) | ~member(U_193, Z_867, W_192) | ~member(U_193, Y_878, W_192) | ~member(U_193, X_883, W_192) | ~member(U_193, V_891, W_192) | X2_884=X1_885 | Z_899=X1_885 | Z_899=X2_884 | Z_899=Y_887 | Y_887=X1_885 | Y_887=X2_884 | Y_887=X_870 | Z_899=X_870 | X_870=X1_885 | X_870=X2_884 | X_870=V_874 | Y_887=V_874 | Z_899=V_874 | X1_885=V_874 | X2_884=V_874 | ~member(U_193, X2_884, W_192) | ~member(U_193, X1_885, W_192) | ~member(U_193, Z_899, W_192) | ~member(U_193, Y_887, W_192) | ~member(U_193, X_870, W_192) | ~member(U_193, V_874, W_192) | X2_895=X1_897 | Z_872=X1_897 | Z_872=X2_895 | Z_872=Y_876 | Y_876=X1_897 | Y_876=X2_895 | Y_876=X_880 | Z_872=X_880 | X_880=X1_897 | X_880=X2_895 | X_880=V_900 | Y_876=V_900 | Z_872=V_900 | X1_897=V_900 | X2_895=V_900 | ~member(U_193, X2_895, W_192) | ~member(U_193, X1_897, W_192) | ~member(U_193, Z_872, W_192) | ~member(U_193, Y_876, W_192) | ~member(U_193, X_880, W_192) | ~member(U_193, V_900, W_192) | X2_868=X1_871 | Z_886=X1_871 | Z_886=X2_868 | Z_886=Y_893 | Y_893=X1_871 | Y_893=X2_868 | Y_893=X_901 | Z_886=X_901 | X_901=X1_871 | X_901=X2_868 | X_901=V_890 | Y_893=V_890 | Z_886=V_890 | X1_871=V_890 | X2_868=V_890 | ~member(U_193, X2_868, W_192) | ~member(U_193, X1_871, W_192) | ~member(U_193, Z_886, W_192) | ~member(U_193, Y_893, W_192) | ~member(U_193, X_901, W_192) | ~member(U_193, V_890, 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)))). % 62.01/52.96 tff(c_964, plain, (![Z_772, Y_766, U_774, Z_194, V_199, V_761, X_775, X2_196, Y_769, X1_765, X_771, V_764, Z_756, V_759, Y_768, V_755, W_192, X_770, X2_750, X1_195, Y_751, X2_748, X_197, Y_198, X_773, X1_757, X1_749, U_193, X2_753, X2_767, Z_760, Z_754, X1_752]: (skf21(V_759, X_773, Y_768, Z_754, X1_765, X2_753, W_192, U_193)=skf21(V_755, X_770, Y_751, Z_772, X1_752, X2_750, W_192, U_193) | skf21(V_764, X_775, Y_766, Z_760, X1_749, X2_748, W_192, U_193)=skf21(V_755, X_770, Y_751, Z_772, X1_752, X2_750, W_192, U_193) | skf21(V_764, X_775, Y_766, Z_760, X1_749, X2_748, W_192, U_193)=skf21(V_759, X_773, Y_768, Z_754, X1_765, X2_753, W_192, U_193) | skf21(V_764, X_775, Y_766, Z_760, X1_749, X2_748, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_755, X_770, Y_751, Z_772, X1_752, X2_750, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_759, X_773, Y_768, Z_754, X1_765, X2_753, 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_761 | skf21(V_764, X_775, Y_766, Z_760, X1_749, X2_748, W_192, U_193)=V_761 | skf21(V_755, X_770, Y_751, Z_772, X1_752, X2_750, W_192, U_193)=V_761 | skf21(V_759, X_773, Y_768, Z_754, X1_765, X2_753, W_192, U_193)=V_761 | V_761=U_774 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_774 | skf21(V_764, X_775, Y_766, Z_760, X1_749, X2_748, W_192, U_193)=U_774 | skf21(V_755, X_770, Y_751, Z_772, X1_752, X2_750, W_192, U_193)=U_774 | skf21(V_759, X_773, Y_768, Z_754, X1_765, X2_753, W_192, U_193)=U_774 | ~member(U_193, V_761, W_192) | ~member(U_193, U_774, W_192) | skf21(U_774, V_761, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_771, Y_769, Z_756, X1_757, X2_767)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_753=X1_765 | Z_754=X1_765 | Z_754=X2_753 | Z_754=Y_768 | Y_768=X1_765 | Y_768=X2_753 | Y_768=X_773 | Z_754=X_773 | X_773=X1_765 | X_773=X2_753 | X_773=V_759 | Y_768=V_759 | Z_754=V_759 | X1_765=V_759 | X2_753=V_759 | ~member(U_193, X2_753, W_192) | ~member(U_193, X1_765, W_192) | ~member(U_193, Z_754, W_192) | ~member(U_193, Y_768, W_192) | ~member(U_193, X_773, W_192) | ~member(U_193, V_759, W_192) | X2_750=X1_752 | Z_772=X1_752 | Z_772=X2_750 | Z_772=Y_751 | Y_751=X1_752 | Y_751=X2_750 | Y_751=X_770 | Z_772=X_770 | X_770=X1_752 | X_770=X2_750 | X_770=V_755 | Y_751=V_755 | Z_772=V_755 | X1_752=V_755 | X2_750=V_755 | ~member(U_193, X2_750, W_192) | ~member(U_193, X1_752, W_192) | ~member(U_193, Z_772, W_192) | ~member(U_193, Y_751, W_192) | ~member(U_193, X_770, W_192) | ~member(U_193, V_755, W_192) | X2_748=X1_749 | Z_760=X1_749 | Z_760=X2_748 | Z_760=Y_766 | Y_766=X1_749 | Y_766=X2_748 | Y_766=X_775 | Z_760=X_775 | X_775=X1_749 | X_775=X2_748 | X_775=V_764 | Y_766=V_764 | Z_760=V_764 | X1_749=V_764 | X2_748=V_764 | ~member(U_193, X2_748, W_192) | ~member(U_193, X1_749, W_192) | ~member(U_193, Z_760, W_192) | ~member(U_193, Y_766, W_192) | ~member(U_193, X_775, W_192) | ~member(U_193, V_764, 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)))). % 62.01/52.96 tff(c_986, plain, (![X1_786, V_780, X1_795, Z_194, V_199, X5_802, Z_788, X2_196, Y_794, Z_783, X2_776, X2_781, W_779, X_796, V_784, X_778, W_192, X2_777, X1_782, Y_798, X1_793, X1_195, U_800, X2_803, X_197, Y_198, X_804, Y_805, X_787, U_193, Z_799, V_792, V_797, Z_789, Y_801]: (skf21(V_797, X_796, Y_805, Z_788, X1_793, X2_776, W_192, U_193)=skf21(V_784, X_787, Y_801, Z_799, X1_786, X2_803, W_192, U_193) | skf21(V_792, X_804, Y_794, Z_789, X1_782, X2_777, W_192, U_193)=skf21(V_784, X_787, Y_801, Z_799, X1_786, X2_803, W_192, U_193) | skf21(V_797, X_796, Y_805, Z_788, X1_793, X2_776, W_192, U_193)=skf21(V_792, X_804, Y_794, Z_789, X1_782, X2_777, W_192, U_193) | skf21(V_792, X_804, Y_794, Z_789, X1_782, X2_777, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_784, X_787, Y_801, Z_799, X1_786, X2_803, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_797, X_796, Y_805, Z_788, X1_793, X2_776, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_802 | skf21(V_792, X_804, Y_794, Z_789, X1_782, X2_777, W_192, U_193)=X5_802 | skf21(V_784, X_787, Y_801, Z_799, X1_786, X2_803, W_192, U_193)=X5_802 | skf21(V_797, X_796, Y_805, Z_788, X1_793, X2_776, W_192, U_193)=X5_802 | X5_802=U_800 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_800 | skf21(V_792, X_804, Y_794, Z_789, X1_782, X2_777, W_192, U_193)=U_800 | skf21(V_784, X_787, Y_801, Z_799, X1_786, X2_803, W_192, U_193)=U_800 | skf21(V_797, X_796, Y_805, Z_788, X1_793, X2_776, W_192, U_193)=U_800 | ~member(U_193, X5_802, W_192) | ~member(U_193, U_800, W_192) | skf21(U_800, V_780, W_779, X_778, Y_798, Z_783, X1_795, X2_781)!=U_800 | X2_776=X1_793 | Z_788=X1_793 | Z_788=X2_776 | Z_788=Y_805 | Y_805=X1_793 | Y_805=X2_776 | Y_805=X_796 | Z_788=X_796 | X_796=X1_793 | X_796=X2_776 | X_796=V_797 | Y_805=V_797 | Z_788=V_797 | X1_793=V_797 | X2_776=V_797 | ~member(U_193, X2_776, W_192) | ~member(U_193, X1_793, W_192) | ~member(U_193, Z_788, W_192) | ~member(U_193, Y_805, W_192) | ~member(U_193, X_796, W_192) | ~member(U_193, V_797, W_192) | X2_803=X1_786 | Z_799=X1_786 | Z_799=X2_803 | Z_799=Y_801 | Y_801=X1_786 | Y_801=X2_803 | Y_801=X_787 | Z_799=X_787 | X_787=X1_786 | X_787=X2_803 | X_787=V_784 | Y_801=V_784 | Z_799=V_784 | X1_786=V_784 | X2_803=V_784 | ~member(U_193, X2_803, W_192) | ~member(U_193, X1_786, W_192) | ~member(U_193, Z_799, W_192) | ~member(U_193, Y_801, W_192) | ~member(U_193, X_787, W_192) | ~member(U_193, V_784, W_192) | X2_777=X1_782 | Z_789=X1_782 | Z_789=X2_777 | Z_789=Y_794 | Y_794=X1_782 | Y_794=X2_777 | Y_794=X_804 | Z_789=X_804 | X_804=X1_782 | X_804=X2_777 | X_804=V_792 | Y_794=V_792 | Z_789=V_792 | X1_782=V_792 | X2_777=V_792 | ~member(U_193, X2_777, W_192) | ~member(U_193, X1_782, W_192) | ~member(U_193, Z_789, W_192) | ~member(U_193, Y_794, W_192) | ~member(U_193, X_804, W_192) | ~member(U_193, V_792, 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)))). % 62.01/52.96 tff(c_942, plain, (![X2_719, Z_729, Y_742, Y_737, X1_728, Z_194, V_199, V_735, X2_196, Y_738, X2_725, X_736, X1_743, X2_721, V_726, Z_740, U_724, X_747, X1_722, Z_730, W_192, V_733, Y_739, W_734, X1_195, V_727, Z_744, X2_745, X_723, X1_746, X_197, Y_198, U_193, X_720]: (skf21(V_735, X_720, Y_739, Z_730, X1_728, X2_721, W_192, U_193)=skf21(V_727, X_723, Y_738, Z_744, X1_746, X2_745, W_192, U_193) | skf21(V_735, X_720, Y_739, Z_730, X1_728, X2_721, W_192, U_193)=skf21(V_733, X_747, Y_737, Z_729, X1_722, X2_719, W_192, U_193) | skf21(V_733, X_747, Y_737, Z_729, X1_722, X2_719, W_192, U_193)=skf21(V_727, X_723, Y_738, Z_744, X1_746, X2_745, W_192, U_193) | skf21(V_733, X_747, Y_737, Z_729, X1_722, 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_735, X_720, Y_739, Z_730, X1_728, X2_721, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_727, X_723, Y_738, Z_744, X1_746, 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)=V_726 | skf21(V_733, X_747, Y_737, Z_729, X1_722, X2_719, W_192, U_193)=V_726 | skf21(V_735, X_720, Y_739, Z_730, X1_728, X2_721, W_192, U_193)=V_726 | skf21(V_727, X_723, Y_738, Z_744, X1_746, X2_745, W_192, U_193)=V_726 | V_726=U_724 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_724 | skf21(V_733, X_747, Y_737, Z_729, X1_722, X2_719, W_192, U_193)=U_724 | skf21(V_735, X_720, Y_739, Z_730, X1_728, X2_721, W_192, U_193)=U_724 | skf21(V_727, X_723, Y_738, Z_744, X1_746, X2_745, W_192, U_193)=U_724 | ~member(U_193, V_726, W_192) | ~member(U_193, U_724, W_192) | skf21(U_724, V_726, W_734, X_736, Y_742, Z_740, X1_743, X2_725)!=V_726 | X2_745=X1_746 | Z_744=X1_746 | Z_744=X2_745 | Z_744=Y_738 | Y_738=X1_746 | Y_738=X2_745 | Y_738=X_723 | Z_744=X_723 | X_723=X1_746 | X_723=X2_745 | X_723=V_727 | Y_738=V_727 | Z_744=V_727 | X1_746=V_727 | X2_745=V_727 | ~member(U_193, X2_745, W_192) | ~member(U_193, X1_746, W_192) | ~member(U_193, Z_744, W_192) | ~member(U_193, Y_738, W_192) | ~member(U_193, X_723, W_192) | ~member(U_193, V_727, W_192) | X2_721=X1_728 | Z_730=X1_728 | Z_730=X2_721 | Z_730=Y_739 | Y_739=X1_728 | Y_739=X2_721 | Y_739=X_720 | Z_730=X_720 | X_720=X1_728 | X_720=X2_721 | X_720=V_735 | Y_739=V_735 | Z_730=V_735 | X1_728=V_735 | X2_721=V_735 | ~member(U_193, X2_721, W_192) | ~member(U_193, X1_728, W_192) | ~member(U_193, Z_730, W_192) | ~member(U_193, Y_739, W_192) | ~member(U_193, X_720, W_192) | ~member(U_193, V_735, W_192) | X2_719=X1_722 | Z_729=X1_722 | Z_729=X2_719 | Z_729=Y_737 | Y_737=X1_722 | Y_737=X2_719 | Y_737=X_747 | Z_729=X_747 | X_747=X1_722 | X_747=X2_719 | X_747=V_733 | Y_737=V_733 | Z_729=V_733 | X1_722=V_733 | X2_719=V_733 | ~member(U_193, X2_719, W_192) | ~member(U_193, X1_722, W_192) | ~member(U_193, Z_729, W_192) | ~member(U_193, Y_737, W_192) | ~member(U_193, X_747, W_192) | ~member(U_193, V_733, 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)))). % 62.01/52.97 tff(c_875, plain, (![X1_630, Z_194, V_199, X2_196, X_629, Z_647, V_640, Y_646, V_639, Y_641, X2_643, X2_628, Z_633, W_632, U_635, W_192, X2_642, X1_195, Y_645, X_648, X_197, Y_198, U_193, X1_634, Z_638, V_627, X1_644]: (skf21(V_639, X_648, Y_641, Z_633, X1_630, X2_628, W_192, U_193)=skf21(V_627, X_629, Y_646, Z_638, X1_634, X2_643, W_192, U_193) | skf21(V_639, X_648, Y_641, Z_633, X1_630, X2_628, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_627, X_629, Y_646, Z_638, X1_634, X2_643, 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_632 | skf21(V_639, X_648, Y_641, Z_633, X1_630, X2_628, W_192, U_193)=W_632 | skf21(V_627, X_629, Y_646, Z_638, X1_634, X2_643, W_192, U_193)=W_632 | W_632=V_640 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_640 | skf21(V_639, X_648, Y_641, Z_633, X1_630, X2_628, W_192, U_193)=V_640 | skf21(V_627, X_629, Y_646, Z_638, X1_634, X2_643, W_192, U_193)=V_640 | V_640=U_635 | W_632=U_635 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_635 | skf21(V_639, X_648, Y_641, Z_633, X1_630, X2_628, W_192, U_193)=U_635 | skf21(V_627, X_629, Y_646, Z_638, X1_634, X2_643, W_192, U_193)=U_635 | ~member(U_193, W_632, W_192) | ~member(U_193, V_640, W_192) | ~member(U_193, U_635, W_192) | skf21(U_635, V_640, W_632, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_645, Z_647, X1_644, X2_642)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_643=X1_634 | Z_638=X1_634 | Z_638=X2_643 | Z_638=Y_646 | Y_646=X1_634 | Y_646=X2_643 | Y_646=X_629 | Z_638=X_629 | X_629=X1_634 | X_629=X2_643 | X_629=V_627 | Y_646=V_627 | Z_638=V_627 | X1_634=V_627 | X2_643=V_627 | ~member(U_193, X2_643, W_192) | ~member(U_193, X1_634, W_192) | ~member(U_193, Z_638, W_192) | ~member(U_193, Y_646, W_192) | ~member(U_193, X_629, W_192) | ~member(U_193, V_627, W_192) | X2_628=X1_630 | Z_633=X1_630 | Z_633=X2_628 | Z_633=Y_641 | Y_641=X1_630 | Y_641=X2_628 | Y_641=X_648 | Z_633=X_648 | X_648=X1_630 | X_648=X2_628 | X_648=V_639 | Y_641=V_639 | Z_633=V_639 | X1_630=V_639 | X2_628=V_639 | ~member(U_193, X2_628, W_192) | ~member(U_193, X1_630, W_192) | ~member(U_193, Z_633, W_192) | ~member(U_193, Y_641, W_192) | ~member(U_193, X_648, W_192) | ~member(U_193, V_639, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 62.01/52.97 tff(c_897, plain, (![X2_654, Y_662, X1_672, Z_659, Z_194, V_199, X2_649, X_670, V_664, X2_196, Y_657, X_673, X1_653, Z_658, V_655, W_668, Z_650, W_192, X1_195, V_666, Y_667, X_197, Y_198, U_652, U_193, X5_665, X_669, X1_651, X2_671, X6_656]: (skf21(V_664, X_673, Y_667, Z_659, X1_651, X2_649, W_192, U_193)=skf21(V_655, X_669, Y_662, Z_650, X1_653, X2_671, W_192, U_193) | skf21(V_664, X_673, Y_667, Z_659, X1_651, X2_649, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_655, X_669, Y_662, Z_650, X1_653, X2_671, 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_656 | skf21(V_664, X_673, Y_667, Z_659, X1_651, X2_649, W_192, U_193)=X6_656 | skf21(V_655, X_669, Y_662, Z_650, X1_653, X2_671, W_192, U_193)=X6_656 | X6_656=X5_665 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_665 | skf21(V_664, X_673, Y_667, Z_659, X1_651, X2_649, W_192, U_193)=X5_665 | skf21(V_655, X_669, Y_662, Z_650, X1_653, X2_671, W_192, U_193)=X5_665 | X5_665=U_652 | X6_656=U_652 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_652 | skf21(V_664, X_673, Y_667, Z_659, X1_651, X2_649, W_192, U_193)=U_652 | skf21(V_655, X_669, Y_662, Z_650, X1_653, X2_671, W_192, U_193)=U_652 | ~member(U_193, X6_656, W_192) | ~member(U_193, X5_665, W_192) | ~member(U_193, U_652, W_192) | skf21(U_652, V_666, W_668, X_670, Y_657, Z_658, X1_672, X2_654)!=U_652 | X2_671=X1_653 | Z_650=X1_653 | Z_650=X2_671 | Z_650=Y_662 | Y_662=X1_653 | Y_662=X2_671 | Y_662=X_669 | Z_650=X_669 | X_669=X1_653 | X_669=X2_671 | X_669=V_655 | Y_662=V_655 | Z_650=V_655 | X1_653=V_655 | X2_671=V_655 | ~member(U_193, X2_671, W_192) | ~member(U_193, X1_653, W_192) | ~member(U_193, Z_650, W_192) | ~member(U_193, Y_662, W_192) | ~member(U_193, X_669, W_192) | ~member(U_193, V_655, W_192) | X2_649=X1_651 | Z_659=X1_651 | Z_659=X2_649 | Z_659=Y_667 | Y_667=X1_651 | Y_667=X2_649 | Y_667=X_673 | Z_659=X_673 | X_673=X1_651 | X_673=X2_649 | X_673=V_664 | Y_667=V_664 | Z_659=V_664 | X1_651=V_664 | X2_649=V_664 | ~member(U_193, X2_649, W_192) | ~member(U_193, X1_651, W_192) | ~member(U_193, Z_659, W_192) | ~member(U_193, Y_667, W_192) | ~member(U_193, X_673, W_192) | ~member(U_193, V_664, 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)))). % 62.01/52.97 tff(c_853, plain, (![Z_614, X1_605, V_612, Z_194, V_199, X2_606, X_611, X2_196, X2_624, Z_625, V_618, Y_621, X_608, W_192, X1_607, Z_609, X1_195, X2_620, U_610, V_615, X_626, X_197, Y_198, X1_623, U_193, W_604, Y_619, Y_613]: (skf21(V_618, X_626, Y_619, Z_614, X1_607, X2_606, W_192, U_193)=skf21(V_612, X_608, Y_613, Z_609, X1_605, X2_620, W_192, U_193) | skf21(V_618, X_626, Y_619, Z_614, X1_607, X2_606, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_612, X_608, Y_613, Z_609, X1_605, X2_620, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_604 | skf21(V_618, X_626, Y_619, Z_614, X1_607, X2_606, W_192, U_193)=W_604 | skf21(V_612, X_608, Y_613, Z_609, X1_605, X2_620, W_192, U_193)=W_604 | W_604=V_615 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_615 | skf21(V_618, X_626, Y_619, Z_614, X1_607, X2_606, W_192, U_193)=V_615 | skf21(V_612, X_608, Y_613, Z_609, X1_605, X2_620, W_192, U_193)=V_615 | V_615=U_610 | W_604=U_610 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_610 | skf21(V_618, X_626, Y_619, Z_614, X1_607, X2_606, W_192, U_193)=U_610 | skf21(V_612, X_608, Y_613, Z_609, X1_605, X2_620, W_192, U_193)=U_610 | ~member(U_193, W_604, W_192) | ~member(U_193, V_615, W_192) | ~member(U_193, U_610, W_192) | skf21(U_610, V_615, W_604, X_611, Y_621, Z_625, X1_623, X2_624)!=W_604 | X2_620=X1_605 | Z_609=X1_605 | Z_609=X2_620 | Z_609=Y_613 | Y_613=X1_605 | Y_613=X2_620 | Y_613=X_608 | Z_609=X_608 | X_608=X1_605 | X_608=X2_620 | X_608=V_612 | Y_613=V_612 | Z_609=V_612 | X1_605=V_612 | X2_620=V_612 | ~member(U_193, X2_620, W_192) | ~member(U_193, X1_605, W_192) | ~member(U_193, Z_609, W_192) | ~member(U_193, Y_613, W_192) | ~member(U_193, X_608, W_192) | ~member(U_193, V_612, W_192) | X2_606=X1_607 | Z_614=X1_607 | Z_614=X2_606 | Z_614=Y_619 | Y_619=X1_607 | Y_619=X2_606 | Y_619=X_626 | Z_614=X_626 | X_626=X1_607 | X_626=X2_606 | X_626=V_618 | Y_619=V_618 | Z_614=V_618 | X1_607=V_618 | X2_606=V_618 | ~member(U_193, X2_606, W_192) | ~member(U_193, X1_607, W_192) | ~member(U_193, Z_614, W_192) | ~member(U_193, Y_619, W_192) | ~member(U_193, X_626, W_192) | ~member(U_193, V_618, 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)))). % 62.01/52.97 tff(c_919, plain, (![V_689, X2_683, X_687, Z_194, V_199, V_679, Z_678, X2_196, X1_697, Y_691, Y_685, Z_682, U_676, Z_694, X2_674, X_693, W_192, X1_692, X1_195, V_695, X_696, Y_680, W_690, X_197, Y_198, X1_677, U_193, X2_675, X5_684]: (skf21(V_695, X_693, Y_685, Z_678, X1_697, X2_683, W_192, U_193)=skf21(V_689, X_696, Y_691, Z_682, X1_677, X2_675, W_192, U_193) | skf21(V_689, X_696, Y_691, Z_682, X1_677, 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_695, X_693, Y_685, Z_678, X1_697, X2_683, 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_684 | skf21(V_689, X_696, Y_691, Z_682, X1_677, X2_675, W_192, U_193)=X5_684 | skf21(V_695, X_693, Y_685, Z_678, X1_697, X2_683, W_192, U_193)=X5_684 | X5_684=V_679 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_679 | skf21(V_689, X_696, Y_691, Z_682, X1_677, X2_675, W_192, U_193)=V_679 | skf21(V_695, X_693, Y_685, Z_678, X1_697, X2_683, W_192, U_193)=V_679 | V_679=U_676 | X5_684=U_676 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_676 | skf21(V_689, X_696, Y_691, Z_682, X1_677, X2_675, W_192, U_193)=U_676 | skf21(V_695, X_693, Y_685, Z_678, X1_697, X2_683, W_192, U_193)=U_676 | ~member(U_193, X5_684, W_192) | ~member(U_193, V_679, W_192) | ~member(U_193, U_676, W_192) | skf21(U_676, V_679, W_690, X_687, Y_680, Z_694, X1_692, X2_674)!=V_679 | X2_683=X1_697 | Z_678=X1_697 | Z_678=X2_683 | Z_678=Y_685 | Y_685=X1_697 | Y_685=X2_683 | Y_685=X_693 | Z_678=X_693 | X_693=X1_697 | X_693=X2_683 | X_693=V_695 | Y_685=V_695 | Z_678=V_695 | X1_697=V_695 | X2_683=V_695 | ~member(U_193, X2_683, W_192) | ~member(U_193, X1_697, W_192) | ~member(U_193, Z_678, W_192) | ~member(U_193, Y_685, W_192) | ~member(U_193, X_693, W_192) | ~member(U_193, V_695, W_192) | X2_675=X1_677 | Z_682=X1_677 | Z_682=X2_675 | Z_682=Y_691 | Y_691=X1_677 | Y_691=X2_675 | Y_691=X_696 | Z_682=X_696 | X_696=X1_677 | X_696=X2_675 | X_696=V_689 | Y_691=V_689 | Z_682=V_689 | X1_677=V_689 | X2_675=V_689 | ~member(U_193, X2_675, W_192) | ~member(U_193, X1_677, W_192) | ~member(U_193, Z_682, W_192) | ~member(U_193, Y_691, W_192) | ~member(U_193, X_696, W_192) | ~member(U_193, V_689, 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)))). % 62.01/52.97 tff(c_786, plain, (![X_546, Z_194, Z_545, V_199, X2_196, X2_538, X1_549, Z_552, U_542, Y_548, W_192, X1_195, V_540, V_553, W_543, X_197, Y_198, X_541, X1_547, U_193, X2_539]: (skf21(V_540, X_546, Y_548, Z_545, X1_547, X2_539, 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_541 | skf21(V_540, X_546, Y_548, Z_545, X1_547, X2_539, W_192, U_193)=X_541 | X_541=W_543 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_543 | skf21(V_540, X_546, Y_548, Z_545, X1_547, X2_539, W_192, U_193)=W_543 | W_543=V_553 | X_541=V_553 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_553 | skf21(V_540, X_546, Y_548, Z_545, X1_547, X2_539, W_192, U_193)=V_553 | V_553=U_542 | W_543=U_542 | X_541=U_542 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_542 | skf21(V_540, X_546, Y_548, Z_545, X1_547, X2_539, W_192, U_193)=U_542 | ~member(U_193, X_541, W_192) | ~member(U_193, W_543, W_192) | ~member(U_193, V_553, W_192) | ~member(U_193, U_542, W_192) | skf21(U_542, V_553, W_543, X_541, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_552, X1_549, X2_538)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_539=X1_547 | Z_545=X1_547 | Z_545=X2_539 | Z_545=Y_548 | Y_548=X1_547 | Y_548=X2_539 | Y_548=X_546 | Z_545=X_546 | X_546=X1_547 | X_546=X2_539 | X_546=V_540 | Y_548=V_540 | Z_545=V_540 | X1_547=V_540 | X2_539=V_540 | ~member(U_193, X2_539, W_192) | ~member(U_193, X1_547, W_192) | ~member(U_193, Z_545, W_192) | ~member(U_193, Y_548, W_192) | ~member(U_193, X_546, W_192) | ~member(U_193, V_540, 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)))). % 62.01/52.97 tff(c_742, plain, (![Z_194, V_505, V_199, X5_504, X2_196, Y_516, X2_501, X_506, X1_517, Y_511, U_514, W_192, X1_195, Z_510, X_507, V_502, X1_509, X2_499, X_197, Y_198, Z_503, U_193, X6_500, W_508]: (skf21(V_502, X_506, Y_511, Z_503, X1_509, X2_501, 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_500 | skf21(V_502, X_506, Y_511, Z_503, X1_509, X2_501, W_192, U_193)=X6_500 | X6_500=X5_504 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_504 | skf21(V_502, X_506, Y_511, Z_503, X1_509, X2_501, W_192, U_193)=X5_504 | X5_504=V_505 | X6_500=V_505 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_505 | skf21(V_502, X_506, Y_511, Z_503, X1_509, X2_501, W_192, U_193)=V_505 | V_505=U_514 | X5_504=U_514 | X6_500=U_514 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_514 | skf21(V_502, X_506, Y_511, Z_503, X1_509, X2_501, W_192, U_193)=U_514 | ~member(U_193, X6_500, W_192) | ~member(U_193, X5_504, W_192) | ~member(U_193, V_505, W_192) | ~member(U_193, U_514, W_192) | skf21(U_514, V_505, W_508, X_507, Y_516, Z_510, X1_517, X2_499)!=V_505 | X2_501=X1_509 | Z_503=X1_509 | Z_503=X2_501 | Z_503=Y_511 | Y_511=X1_509 | Y_511=X2_501 | Y_511=X_506 | Z_503=X_506 | X_506=X1_509 | X_506=X2_501 | X_506=V_502 | Y_511=V_502 | Z_503=V_502 | X1_509=V_502 | X2_501=V_502 | ~member(U_193, X2_501, W_192) | ~member(U_193, X1_509, W_192) | ~member(U_193, Z_503, W_192) | ~member(U_193, Y_511, W_192) | ~member(U_193, X_506, 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)))). % 62.01/52.97 tff(c_764, plain, (![X5_536, Z_528, Z_194, V_199, V_527, X2_196, W_520, X7_518, X_524, X2_519, X1_530, Y_529, V_521, W_192, X1_531, X1_195, Z_523, X_525, X2_526, X6_535, X_197, Y_198, Y_532, U_193, U_537]: (skf21(V_521, X_524, Y_532, Z_523, X1_530, X2_519, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X7_518 | skf21(V_521, X_524, Y_532, Z_523, X1_530, X2_519, W_192, U_193)=X7_518 | X7_518=X6_535 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_535 | skf21(V_521, X_524, Y_532, Z_523, X1_530, X2_519, W_192, U_193)=X6_535 | X6_535=X5_536 | X7_518=X5_536 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_536 | skf21(V_521, X_524, Y_532, Z_523, X1_530, X2_519, W_192, U_193)=X5_536 | X5_536=U_537 | X6_535=U_537 | X7_518=U_537 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_537 | skf21(V_521, X_524, Y_532, Z_523, X1_530, X2_519, W_192, U_193)=U_537 | ~member(U_193, X7_518, W_192) | ~member(U_193, X6_535, W_192) | ~member(U_193, X5_536, W_192) | ~member(U_193, U_537, W_192) | skf21(U_537, V_527, W_520, X_525, Y_529, Z_528, X1_531, X2_526)!=U_537 | X2_519=X1_530 | Z_523=X1_530 | Z_523=X2_519 | Z_523=Y_532 | Y_532=X1_530 | Y_532=X2_519 | Y_532=X_524 | Z_523=X_524 | X_524=X1_530 | X_524=X2_519 | X_524=V_521 | Y_532=V_521 | Z_523=V_521 | X1_530=V_521 | X2_519=V_521 | ~member(U_193, X2_519, W_192) | ~member(U_193, X1_530, W_192) | ~member(U_193, Z_523, W_192) | ~member(U_193, Y_532, W_192) | ~member(U_193, X_524, W_192) | ~member(U_193, V_521, 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)))). % 62.01/52.97 tff(c_808, plain, (![Z_194, V_199, X2_196, Y_568, X2_554, V_557, Y_556, W_192, Z_562, X1_195, Z_555, V_564, X1_567, X_197, Y_198, W_565, X_563, U_193, X2_559, X_558, U_560, X1_561]: (skf21(V_557, X_563, Y_568, Z_562, X1_567, X2_554, 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_558 | skf21(V_557, X_563, Y_568, Z_562, X1_567, X2_554, W_192, U_193)=X_558 | X_558=W_565 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_565 | skf21(V_557, X_563, Y_568, Z_562, X1_567, X2_554, W_192, U_193)=W_565 | W_565=V_564 | X_558=V_564 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_564 | skf21(V_557, X_563, Y_568, Z_562, X1_567, X2_554, W_192, U_193)=V_564 | V_564=U_560 | W_565=U_560 | X_558=U_560 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_560 | skf21(V_557, X_563, Y_568, Z_562, X1_567, X2_554, W_192, U_193)=U_560 | ~member(U_193, X_558, W_192) | ~member(U_193, W_565, W_192) | ~member(U_193, V_564, W_192) | ~member(U_193, U_560, W_192) | skf21(U_560, V_564, W_565, X_558, Y_556, Z_555, X1_561, X2_559)!=X_558 | X2_554=X1_567 | Z_562=X1_567 | Z_562=X2_554 | Z_562=Y_568 | Y_568=X1_567 | Y_568=X2_554 | Y_568=X_563 | Z_562=X_563 | X_563=X1_567 | X_563=X2_554 | X_563=V_557 | Y_568=V_557 | Z_562=V_557 | X1_567=V_557 | X2_554=V_557 | ~member(U_193, X2_554, W_192) | ~member(U_193, X1_567, W_192) | ~member(U_193, Z_562, W_192) | ~member(U_193, Y_568, W_192) | ~member(U_193, X_563, W_192) | ~member(U_193, V_557, 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)))). % 62.01/52.97 tff(c_830, plain, (![V_574, X_586, Z_194, X5_587, V_199, X1_571, X2_572, X2_196, X2_576, Y_588, Z_573, W_192, X1_195, W_575, U_579, Z_577, X_197, Y_198, X_578, U_193, X1_581, V_583, Y_582]: (skf21(V_574, X_578, Y_582, Z_577, X1_581, X2_572, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_587 | skf21(V_574, X_578, Y_582, Z_577, X1_581, X2_572, W_192, U_193)=X5_587 | X5_587=W_575 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_575 | skf21(V_574, X_578, Y_582, Z_577, X1_581, X2_572, W_192, U_193)=W_575 | W_575=V_583 | X5_587=V_583 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_583 | skf21(V_574, X_578, Y_582, Z_577, X1_581, X2_572, W_192, U_193)=V_583 | V_583=U_579 | W_575=U_579 | X5_587=U_579 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_579 | skf21(V_574, X_578, Y_582, Z_577, X1_581, X2_572, W_192, U_193)=U_579 | ~member(U_193, X5_587, W_192) | ~member(U_193, W_575, W_192) | ~member(U_193, V_583, W_192) | ~member(U_193, U_579, W_192) | skf21(U_579, V_583, W_575, X_586, Y_588, Z_573, X1_571, X2_576)!=W_575 | X2_572=X1_581 | Z_577=X1_581 | Z_577=X2_572 | Z_577=Y_582 | Y_582=X1_581 | Y_582=X2_572 | Y_582=X_578 | Z_577=X_578 | X_578=X1_581 | X_578=X2_572 | X_578=V_574 | Y_582=V_574 | Z_577=V_574 | X1_581=V_574 | X2_572=V_574 | ~member(U_193, X2_572, W_192) | ~member(U_193, X1_581, W_192) | ~member(U_193, Z_577, W_192) | ~member(U_193, Y_582, W_192) | ~member(U_193, X_578, W_192) | ~member(U_193, V_574, 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)))). % 62.01/52.97 tff(c_722, plain, (![V_496, X_206, X1_204, W_200, X1_492, V_208, W_495, X2_205, U_494, X_498, U_202, Y_207, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=Y_207 | Y_207=X_206 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_206 | X_206=W_200 | Y_207=W_200 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_202 | ~member(U_494, Y_207, W_495) | ~member(U_494, X_206, W_495) | ~member(U_494, W_200, W_495) | ~member(U_494, V_208, W_495) | ~member(U_494, U_202, W_495) | skf21(U_202, V_208, W_200, X_206, Y_207, skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494), X1_204, X2_205)!=skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494) | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 tff(c_720, plain, (![V_496, X6_151, X2_158, X1_492, Y_160, W_495, X1_157, X_159, W_152, U_494, V_161, X_498, X5_150, Y_497, X2_491, Z_493, Z_155, U_154]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_151 | X6_151=X5_150 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_154 | ~member(U_494, X6_151, W_495) | ~member(U_494, X5_150, W_495) | ~member(U_494, W_152, W_495) | ~member(U_494, V_161, W_495) | ~member(U_494, U_154, W_495) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 tff(c_721, plain, (![V_496, U_142, W_140, X1_492, X2_145, X5_138, W_495, Y_147, V_148, U_494, X_498, Z_143, X1_144, X_146, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_138 | X_146=X5_138 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_146 | X_146=W_140 | X5_138=W_140 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_142 | ~member(U_494, X5_138, W_495) | ~member(U_494, X_146, W_495) | ~member(U_494, W_140, W_495) | ~member(U_494, V_148, W_495) | ~member(U_494, U_142, W_495) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 tff(c_719, plain, (![V_496, U_130, X1_492, W_495, X1_132, V_136, Y_135, U_494, X_498, W_128, X2_133, Y_497, Z_131, X2_491, X_134, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=Y_135 | Y_135=X_134 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X_134 | X_134=W_128 | Y_135=W_128 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_130 | ~member(U_494, Y_135, W_495) | ~member(U_494, X_134, W_495) | ~member(U_494, W_128, W_495) | ~member(U_494, V_136, W_495) | ~member(U_494, U_130, W_495) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 tff(c_723, plain, (![Z_183, V_496, X8_190, X5_177, X1_492, W_495, X1_185, V_189, X_187, Y_188, U_494, U_181, X2_186, X7_184, X6_178, X_498, W_179, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X8_190 | X8_190=X7_184 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_181 | ~member(U_494, X8_190, W_495) | ~member(U_494, X7_184, W_495) | ~member(U_494, X6_178, W_495) | ~member(U_494, X5_177, W_495) | ~member(U_494, U_181, W_495) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 tff(c_718, plain, (![V_496, X2_171, X1_492, X6_164, V_174, W_495, U_167, Z_168, W_165, U_494, X_498, X5_163, X1_170, X7_169, X_172, Y_173, Y_497, X2_491, Z_493]: (skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X7_169 | X7_169=X6_164 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf21(V_496, X_498, Y_497, Z_493, X1_492, X2_491, W_495, U_494)=U_167 | ~member(U_494, X7_169, W_495) | ~member(U_494, X6_164, W_495) | ~member(U_494, X5_163, W_495) | ~member(U_494, V_174, W_495) | ~member(U_494, U_167, W_495) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_491=X1_492 | Z_493=X1_492 | Z_493=X2_491 | Z_493=Y_497 | Y_497=X1_492 | Y_497=X2_491 | Y_497=X_498 | Z_493=X_498 | X_498=X1_492 | X_498=X2_491 | X_498=V_496 | Y_497=V_496 | Z_493=V_496 | X1_492=V_496 | X2_491=V_496 | six(U_494, W_495) | ~member(U_494, X2_491, W_495) | ~member(U_494, X1_492, W_495) | ~member(U_494, Z_493, W_495) | ~member(U_494, Y_497, W_495) | ~member(U_494, X_498, W_495) | ~member(U_494, V_496, W_495)))). % 62.01/52.97 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)))). % 62.01/52.97 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))). % 62.01/52.97 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))). % 62.01/52.97 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))). % 62.01/52.97 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))). % 62.01/52.97 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))). % 62.01/52.97 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))). % 62.01/52.97 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)))). % 62.01/52.97 tff(c_551, plain, (![U_223]: (~member(skc3, U_223, skc4) | ~cannon(skc3, U_223) | ~of(skc3, U_223, skc5)))). % 62.01/52.97 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)))). % 62.01/52.97 tff(c_549, plain, (skf14(skc4, skc3)!=skf10(skc4, skc3))). % 62.01/52.97 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf14(U_115, V_116)!=skf10(U_115, V_116)))). % 62.01/52.97 tff(c_544, plain, (skf18(skc4, skc3)!=skf10(skc4, skc3))). % 62.01/52.97 tff(c_539, plain, (skf14(skc4, skc3)!=skf12(skc4, skc3))). % 62.01/52.97 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf18(U_101, V_102)!=skf10(U_101, V_102)))). % 62.01/52.97 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf14(U_117, V_118)!=skf12(U_117, V_118)))). % 62.01/52.97 tff(c_534, plain, (skf20(skc4, skc3)!=skf10(skc4, skc3))). % 62.01/52.97 tff(c_529, plain, (act(skc3, skf10(skc4, skc3)))). % 62.01/52.97 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf20(U_91, V_92)!=skf10(U_91, V_92)))). % 62.01/52.97 tff(c_525, plain, (act(skc3, skf16(skc4, skc3)))). % 62.01/52.98 tff(c_509, plain, (act(skc3, skf12(skc4, skc3)))). % 62.01/52.98 tff(c_521, plain, (action(skc3, skf10(skc4, skc3)))). % 62.01/52.98 tff(c_505, plain, (action(skc3, skf16(skc4, skc3)))). % 62.01/52.98 tff(c_517, plain, (shot(skc3, skf10(skc4, skc3)))). % 62.01/52.98 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf10(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 62.01/52.98 tff(c_501, plain, (action(skc3, skf12(skc4, skc3)))). % 62.01/52.98 tff(c_497, plain, (shot(skc3, skf16(skc4, skc3)))). % 62.01/52.98 tff(c_489, plain, (shot(skc3, skf12(skc4, skc3)))). % 62.01/52.98 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf16(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 62.01/52.98 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf12(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 62.01/52.98 tff(c_481, plain, (skf16(skc4, skc3)!=skf10(skc4, skc3))). % 62.01/52.98 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf16(U_109, V_110)!=skf10(U_109, V_110)))). % 62.01/52.98 tff(c_454, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.98 tff(c_475, plain, (skf16(skc4, skc3)!=skf12(skc4, skc3))). % 62.01/52.98 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf16(U_111, V_112)!=skf12(U_111, V_112)))). % 62.01/52.98 tff(c_470, plain, (act(skc3, skf20(skc4, skc3)))). % 62.01/52.98 tff(c_466, plain, (action(skc3, skf20(skc4, skc3)))). % 62.01/52.98 tff(c_462, plain, (shot(skc3, skf20(skc4, skc3)))). % 62.01/52.98 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf20(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 62.01/52.98 tff(c_394, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 62.01/52.98 tff(c_441, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 62.01/52.98 tff(c_449, plain, (~act(skc3, skc4))). % 62.01/52.98 tff(c_445, plain, (~event(skc3, skc4))). % 62.01/52.98 tff(c_436, plain, (~eventuality(skc3, skc4))). % 62.01/52.98 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf18(U_107, V_108)!=skf16(U_107, V_108)))). % 62.01/52.98 tff(c_359, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 62.01/52.98 tff(c_389, plain, (![U_365, V_366]: (artifact(U_365, V_366) | ~cannon(U_365, V_366)))). % 62.01/52.98 tff(c_430, plain, (skf18(skc4, skc3)!=skf12(skc4, skc3))). % 62.01/52.98 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf18(U_103, V_104)!=skf12(U_103, V_104)))). % 62.01/52.98 tff(c_425, plain, (~artifact(skc3, skc4))). % 62.01/52.98 tff(c_421, plain, (~entity(skc3, skc4))). % 62.01/52.98 tff(c_369, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 62.01/52.98 tff(c_354, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.01/52.98 tff(c_415, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 62.01/52.98 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf20(U_97, V_98)!=skf16(U_97, V_98)))). % 62.01/52.98 tff(c_410, plain, (act(skc3, skf14(skc4, skc3)))). % 62.01/52.98 tff(c_406, plain, (action(skc3, skf14(skc4, skc3)))). % 62.01/52.98 tff(c_402, plain, (shot(skc3, skf14(skc4, skc3)))). % 62.01/52.98 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf14(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 62.01/52.98 tff(c_374, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 62.01/52.98 tff(c_342, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 62.01/52.98 tff(c_384, plain, (~artifact(skc3, skc5))). % 62.01/52.98 tff(c_264, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.98 tff(c_379, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 62.01/52.98 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf20(U_95, V_96)!=skf14(U_95, V_96)))). % 62.01/52.98 tff(c_294, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 62.01/52.98 tff(c_270, plain, (![U_317, V_318]: (~multiple(U_317, V_318) | ~entity(U_317, V_318)))). % 62.01/52.98 tff(c_364, plain, (skf20(skc4, skc3)!=skf12(skc4, skc3))). % 62.01/52.98 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf20(U_93, V_94)!=skf12(U_93, V_94)))). % 62.01/52.98 tff(c_305, plain, (![U_333, V_334]: (~multiple(U_333, V_334) | ~eventuality(U_333, V_334)))). % 62.01/52.98 tff(c_336, plain, (![U_341, V_342]: (~living(U_341, V_342) | ~artifact(U_341, V_342)))). % 62.01/52.98 tff(c_337, plain, (![U_341, V_342]: (~animate(U_341, V_342) | ~artifact(U_341, V_342)))). % 62.01/52.98 tff(c_348, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 62.01/52.98 tff(c_328, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 62.01/52.98 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf16(U_113, V_114)!=skf14(U_113, V_114)))). % 62.01/52.98 tff(c_248, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.01/52.98 tff(c_179, plain, (![U_250, V_251]: (instrumentality(U_250, V_251) | ~weapon(U_250, V_251)))). % 62.01/52.98 tff(c_212, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.98 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf20(U_99, V_100)!=skf18(U_99, V_100)))). % 62.01/52.98 tff(c_299, plain, (skf12(skc4, skc3)!=skf10(skc4, skc3))). % 62.01/52.98 tff(c_315, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 62.01/52.98 tff(c_323, plain, (~act(skc3, skc5))). % 62.01/52.98 tff(c_319, plain, (~event(skc3, skc5))). % 62.01/52.98 tff(c_310, plain, (~eventuality(skc3, skc5))). % 62.01/52.98 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf18(U_105, V_106)!=skf14(U_105, V_106)))). % 62.01/52.98 tff(c_226, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 62.01/52.98 tff(c_173, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~eventuality(U_11, V_12)))). % 62.01/52.98 tff(c_200, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.98 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf12(U_119, V_120)!=skf10(U_119, V_120)))). % 62.01/52.98 tff(c_206, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 62.01/52.98 tff(c_195, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 62.01/52.98 tff(c_288, plain, (act(skc3, skf18(skc4, skc3)))). % 62.01/52.98 tff(c_284, plain, (action(skc3, skf18(skc4, skc3)))). % 62.01/52.98 tff(c_280, plain, (shot(skc3, skf18(skc4, skc3)))). % 62.01/52.98 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf18(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 62.01/52.98 tff(c_253, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.01/52.98 tff(c_258, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.01/52.98 tff(c_219, plain, (![U_280, V_281]: (singleton(U_280, V_281) | ~entity(U_280, V_281)))). % 62.01/52.98 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 62.01/52.98 tff(c_242, plain, (![U_302, V_303]: (~male(U_302, V_303) | ~object(U_302, V_303)))). % 62.01/52.98 tff(c_237, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.98 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 62.01/52.98 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 62.01/52.99 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 62.01/52.99 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 62.01/52.99 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 62.01/52.99 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 62.01/52.99 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 62.01/52.99 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 62.01/52.99 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 62.01/52.99 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 62.01/52.99 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 62.01/52.99 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 62.01/52.99 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 62.01/52.99 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 62.01/52.99 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 62.01/52.99 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 62.01/52.99 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 62.01/52.99 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 62.01/52.99 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 62.01/52.99 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 62.01/52.99 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 62.01/52.99 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 62.01/52.99 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 62.01/52.99 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 62.01/52.99 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 62.01/52.99 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 62.01/52.99 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 62.01/52.99 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 62.01/52.99 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 62.01/52.99 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 62.01/52.99 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 62.01/52.99 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 62.01/52.99 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 62.01/52.99 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 62.01/52.99 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 62.01/52.99 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 62.01/52.99 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 62.01/52.99 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 62.01/52.99 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 62.01/52.99 tff(c_146, plain, (six(skc3, skc4))). % 62.01/52.99 tff(c_142, plain, (male(skc3, skc5))). % 62.01/52.99 tff(c_144, plain, (group(skc3, skc4))). % 62.01/52.99 tff(c_140, plain, (actual_world(skc3))). % 62.01/52.99 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.01/52.99 %------------------------------------------------------------------------------