%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP077-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:08 PM UTC 2025 % Result : Satisfiable 67.95s 58.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : NLP077-1 : TPTP v9.0.0. Released v2.4.0. % 0.04/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.35 % Computer : n008.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:24:47 EDT 2025 % 0.13/0.35 % CPUTime : % 67.95/58.19 % 67.95/58.19 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 67.95/58.20 % 67.95/58.20 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 67.95/58.21 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf21 > skf8 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc3 > skc2 % 67.95/58.21 % 67.95/58.21 %Foreground sorts: % 67.95/58.21 % 67.95/58.21 % 67.95/58.21 %Background operators: % 67.95/58.21 % 67.95/58.21 % 67.95/58.21 %Foreground operators: % 67.95/58.21 tff(nonliving, type, nonliving: ($i * $i) > $o). % 67.95/58.21 tff(skf10, type, skf10: ($i * $i) > $i). % 67.95/58.21 tff(member, type, member: ($i * $i * $i) > $o). % 67.95/58.21 tff(living, type, living: ($i * $i) > $o). % 67.95/58.21 tff(fire, type, fire: ($i * $i) > $o). % 67.95/58.21 tff(human_person, type, human_person: ($i * $i) > $o). % 67.95/58.21 tff(action, type, action: ($i * $i) > $o). % 67.95/58.21 tff(present, type, present: ($i * $i) > $o). % 67.95/58.21 tff(shot, type, shot: ($i * $i) > $o). % 67.95/58.21 tff(entity, type, entity: ($i * $i) > $o). % 67.95/58.21 tff(eventuality, type, eventuality: ($i * $i) > $o). % 67.95/58.21 tff(weapon, type, weapon: ($i * $i) > $o). % 67.95/58.21 tff(existent, type, existent: ($i * $i) > $o). % 67.95/58.21 tff(singleton, type, singleton: ($i * $i) > $o). % 67.95/58.21 tff(male, type, male: ($i * $i) > $o). % 67.95/58.21 tff(multiple, type, multiple: ($i * $i) > $o). % 67.95/58.21 tff(organism, type, organism: ($i * $i) > $o). % 67.95/58.21 tff(animate, type, animate: ($i * $i) > $o). % 67.95/58.21 tff(of, type, of: ($i * $i * $i) > $o). % 67.95/58.21 tff(skf14, type, skf14: ($i * $i) > $i). % 67.95/58.21 tff(actual_world, type, actual_world: $i > $o). % 67.95/58.21 tff(agent, type, agent: ($i * $i * $i) > $o). % 67.95/58.21 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 67.95/58.21 tff(group, type, group: ($i * $i) > $o). % 67.95/58.21 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 67.95/58.21 tff(artifact, type, artifact: ($i * $i) > $o). % 67.95/58.21 tff(cannon, type, cannon: ($i * $i) > $o). % 67.95/58.21 tff(event, type, event: ($i * $i) > $o). % 67.95/58.21 tff(skc2, type, skc2: $i). % 67.95/58.21 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 67.95/58.21 tff(patient, type, patient: ($i * $i * $i) > $o). % 67.95/58.21 tff(skf8, type, skf8: ($i * $i) > $i). % 67.95/58.21 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 67.95/58.21 tff(skc3, type, skc3: $i). % 67.95/58.21 tff(thing, type, thing: ($i * $i) > $o). % 67.95/58.21 tff(human, type, human: ($i * $i) > $o). % 67.95/58.21 tff(six, type, six: ($i * $i) > $o). % 67.95/58.21 tff(skf18, type, skf18: ($i * $i) > $i). % 67.95/58.21 tff(man, type, man: ($i * $i) > $o). % 67.95/58.21 tff(weaponry, type, weaponry: ($i * $i) > $o). % 67.95/58.21 tff(unisex, type, unisex: ($i * $i) > $o). % 67.95/58.21 tff(skf16, type, skf16: ($i * $i) > $i). % 67.95/58.21 tff(set, type, set: ($i * $i) > $o). % 67.95/58.21 tff(skf12, type, skf12: ($i * $i) > $i). % 67.95/58.21 tff(impartial, type, impartial: ($i * $i) > $o). % 67.95/58.21 tff(object, type, object: ($i * $i) > $o). % 67.95/58.21 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 67.95/58.21 tff(specific, type, specific: ($i * $i) > $o). % 67.95/58.21 tff(skf20, type, skf20: ($i * $i) > $i). % 67.95/58.21 tff(act, type, act: ($i * $i) > $o). % 67.95/58.21 % 67.95/58.21 %Saturated clause set: % 67.95/58.21 tff(c_1036, plain, (![X2_948, X2_944, X1_966, Z_194, V_199, X1_952, V_945, X2_974, X2_196, X_967, X_951, Y_955, Z_969, X1_941, X1_970, V_946, X_949, Y_947, Y_963, V_972, W_192, X_957, X1_195, Y_939, Z_953, V_971, W_973, X1_968, X2_965, X_943, X_975, X_197, Y_198, V_936, Z_937, Z_956, X1_954, V_960, U_193, Z_942, Y_961, Y_950, X2_940, Z_962, X2_938]: (skf21(V_971, X_943, Y_950, Z_942, X1_954, X2_940, W_192, U_193)=skf21(V_936, X_967, Y_961, Z_953, X1_970, X2_974, W_192, U_193) | skf21(V_972, X_951, Y_939, Z_969, X1_968, X2_965, W_192, U_193)=skf21(V_971, X_943, Y_950, Z_942, X1_954, X2_940, W_192, U_193) | skf21(V_972, X_951, Y_939, Z_969, X1_968, X2_965, W_192, U_193)=skf21(V_936, X_967, Y_961, Z_953, X1_970, X2_974, W_192, U_193) | skf21(V_972, X_951, Y_939, Z_969, X1_968, X2_965, W_192, U_193)=skf21(V_946, X_949, Y_955, Z_962, X1_966, X2_948, W_192, U_193) | skf21(V_971, X_943, Y_950, Z_942, X1_954, X2_940, W_192, U_193)=skf21(V_946, X_949, Y_955, Z_962, X1_966, X2_948, W_192, U_193) | skf21(V_946, X_949, Y_955, Z_962, X1_966, X2_948, W_192, U_193)=skf21(V_936, X_967, Y_961, Z_953, X1_970, X2_974, W_192, U_193) | skf21(V_960, X_975, Y_963, Z_956, X1_941, X2_938, W_192, U_193)=skf21(V_946, X_949, Y_955, Z_962, X1_966, X2_948, W_192, U_193) | skf21(V_972, X_951, Y_939, Z_969, X1_968, X2_965, W_192, U_193)=skf21(V_960, X_975, Y_963, Z_956, X1_941, X2_938, W_192, U_193) | skf21(V_971, X_943, Y_950, Z_942, X1_954, X2_940, W_192, U_193)=skf21(V_960, X_975, Y_963, Z_956, X1_941, X2_938, W_192, U_193) | skf21(V_960, X_975, Y_963, Z_956, X1_941, X2_938, W_192, U_193)=skf21(V_936, X_967, Y_961, Z_953, X1_970, X2_974, W_192, U_193) | skf21(V_960, X_975, Y_963, Z_956, X1_941, 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_946, X_949, Y_955, Z_962, X1_966, X2_948, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_972, X_951, Y_939, Z_969, X1_968, 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_971, X_943, Y_950, Z_942, X1_954, X2_940, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_936, X_967, Y_961, Z_953, X1_970, X2_974, 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_945, W_973, X_957, Y_947, Z_937, X1_952, X2_944)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_974=X1_970 | Z_953=X1_970 | Z_953=X2_974 | Z_953=Y_961 | Y_961=X1_970 | Y_961=X2_974 | Y_961=X_967 | Z_953=X_967 | X_967=X1_970 | X_967=X2_974 | X_967=V_936 | Y_961=V_936 | Z_953=V_936 | X1_970=V_936 | X2_974=V_936 | ~member(U_193, X2_974, W_192) | ~member(U_193, X1_970, W_192) | ~member(U_193, Z_953, W_192) | ~member(U_193, Y_961, W_192) | ~member(U_193, X_967, W_192) | ~member(U_193, V_936, W_192) | X2_940=X1_954 | Z_942=X1_954 | Z_942=X2_940 | Z_942=Y_950 | Y_950=X1_954 | Y_950=X2_940 | Y_950=X_943 | Z_942=X_943 | X_943=X1_954 | X_943=X2_940 | X_943=V_971 | Y_950=V_971 | Z_942=V_971 | X1_954=V_971 | X2_940=V_971 | ~member(U_193, X2_940, W_192) | ~member(U_193, X1_954, W_192) | ~member(U_193, Z_942, W_192) | ~member(U_193, Y_950, W_192) | ~member(U_193, X_943, W_192) | ~member(U_193, V_971, W_192) | X2_965=X1_968 | Z_969=X1_968 | Z_969=X2_965 | Z_969=Y_939 | Y_939=X1_968 | Y_939=X2_965 | Y_939=X_951 | Z_969=X_951 | X_951=X1_968 | X_951=X2_965 | X_951=V_972 | Y_939=V_972 | Z_969=V_972 | X1_968=V_972 | X2_965=V_972 | ~member(U_193, X2_965, W_192) | ~member(U_193, X1_968, W_192) | ~member(U_193, Z_969, W_192) | ~member(U_193, Y_939, W_192) | ~member(U_193, X_951, W_192) | ~member(U_193, V_972, W_192) | X2_948=X1_966 | Z_962=X1_966 | Z_962=X2_948 | Z_962=Y_955 | Y_955=X1_966 | Y_955=X2_948 | Y_955=X_949 | Z_962=X_949 | X_949=X1_966 | X_949=X2_948 | X_949=V_946 | Y_955=V_946 | Z_962=V_946 | X1_966=V_946 | X2_948=V_946 | ~member(U_193, X2_948, W_192) | ~member(U_193, X1_966, W_192) | ~member(U_193, Z_962, W_192) | ~member(U_193, Y_955, W_192) | ~member(U_193, X_949, W_192) | ~member(U_193, V_946, W_192) | X2_938=X1_941 | Z_956=X1_941 | Z_956=X2_938 | Z_956=Y_963 | Y_963=X1_941 | Y_963=X2_938 | Y_963=X_975 | Z_956=X_975 | X_975=X1_941 | X_975=X2_938 | X_975=V_960 | Y_963=V_960 | Z_956=V_960 | X1_941=V_960 | X2_938=V_960 | ~member(U_193, X2_938, W_192) | ~member(U_193, X1_941, W_192) | ~member(U_193, Z_956, W_192) | ~member(U_193, Y_963, W_192) | ~member(U_193, X_975, 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)))). % 67.95/58.22 tff(c_991, plain, (![X1_843, V_851, X_840, X2_836, Z_194, X1_842, V_848, V_199, Y_841, X2_196, Z_852, Z_864, Z_835, X_861, X_867, X2_837, Y_858, W_859, U_866, W_192, X_860, Y_844, X1_195, V_839, X2_856, X1_838, X_857, X1_862, X_197, Y_198, Y_845, Z_847, U_193, X2_846, Z_855, X1_865, X2_854, Y_853, V_863]: (skf21(V_863, X_857, Y_845, Z_864, X1_843, X2_846, W_192, U_193)=skf21(V_848, X_861, Y_844, Z_852, X1_862, X2_837, W_192, U_193) | skf21(V_848, X_861, Y_844, Z_852, X1_862, X2_837, W_192, U_193)=skf21(V_839, X_840, Y_841, Z_855, X1_865, X2_856, W_192, U_193) | skf21(V_863, X_857, Y_845, Z_864, X1_843, X2_846, W_192, U_193)=skf21(V_839, X_840, Y_841, Z_855, X1_865, X2_856, W_192, U_193) | skf21(V_851, X_867, Y_853, Z_847, X1_838, X2_836, W_192, U_193)=skf21(V_839, X_840, Y_841, Z_855, X1_865, X2_856, W_192, U_193) | skf21(V_851, X_867, Y_853, Z_847, X1_838, X2_836, W_192, U_193)=skf21(V_848, X_861, Y_844, Z_852, X1_862, X2_837, W_192, U_193) | skf21(V_863, X_857, Y_845, Z_864, X1_843, X2_846, W_192, U_193)=skf21(V_851, X_867, Y_853, Z_847, X1_838, X2_836, W_192, U_193) | skf21(V_851, X_867, Y_853, Z_847, X1_838, 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_839, X_840, Y_841, Z_855, X1_865, 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_848, X_861, Y_844, Z_852, X1_862, X2_837, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_863, X_857, Y_845, Z_864, X1_843, X2_846, 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_866 | skf21(V_851, X_867, Y_853, Z_847, X1_838, X2_836, W_192, U_193)=U_866 | skf21(V_839, X_840, Y_841, Z_855, X1_865, X2_856, W_192, U_193)=U_866 | skf21(V_848, X_861, Y_844, Z_852, X1_862, X2_837, W_192, U_193)=U_866 | skf21(V_863, X_857, Y_845, Z_864, X1_843, X2_846, W_192, U_193)=U_866 | ~member(U_193, U_866, W_192) | skf21(U_866, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_859, X_860, Y_858, Z_835, X1_842, X2_854)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_846=X1_843 | Z_864=X1_843 | Z_864=X2_846 | Z_864=Y_845 | Y_845=X1_843 | Y_845=X2_846 | Y_845=X_857 | Z_864=X_857 | X_857=X1_843 | X_857=X2_846 | X_857=V_863 | Y_845=V_863 | Z_864=V_863 | X1_843=V_863 | X2_846=V_863 | ~member(U_193, X2_846, W_192) | ~member(U_193, X1_843, W_192) | ~member(U_193, Z_864, W_192) | ~member(U_193, Y_845, W_192) | ~member(U_193, X_857, W_192) | ~member(U_193, V_863, W_192) | X2_837=X1_862 | Z_852=X1_862 | Z_852=X2_837 | Z_852=Y_844 | Y_844=X1_862 | Y_844=X2_837 | Y_844=X_861 | Z_852=X_861 | X_861=X1_862 | X_861=X2_837 | X_861=V_848 | Y_844=V_848 | Z_852=V_848 | X1_862=V_848 | X2_837=V_848 | ~member(U_193, X2_837, W_192) | ~member(U_193, X1_862, W_192) | ~member(U_193, Z_852, W_192) | ~member(U_193, Y_844, W_192) | ~member(U_193, X_861, W_192) | ~member(U_193, V_848, W_192) | X2_856=X1_865 | Z_855=X1_865 | Z_855=X2_856 | Z_855=Y_841 | Y_841=X1_865 | Y_841=X2_856 | Y_841=X_840 | Z_855=X_840 | X_840=X1_865 | X_840=X2_856 | X_840=V_839 | Y_841=V_839 | Z_855=V_839 | X1_865=V_839 | X2_856=V_839 | ~member(U_193, X2_856, W_192) | ~member(U_193, X1_865, W_192) | ~member(U_193, Z_855, W_192) | ~member(U_193, Y_841, W_192) | ~member(U_193, X_840, W_192) | ~member(U_193, V_839, W_192) | X2_836=X1_838 | Z_847=X1_838 | Z_847=X2_836 | Z_847=Y_853 | Y_853=X1_838 | Y_853=X2_836 | Y_853=X_867 | Z_847=X_867 | X_867=X1_838 | X_867=X2_836 | X_867=V_851 | Y_853=V_851 | Z_847=V_851 | X1_838=V_851 | X2_836=V_851 | ~member(U_193, X2_836, W_192) | ~member(U_193, X1_838, W_192) | ~member(U_193, Z_847, W_192) | ~member(U_193, Y_853, W_192) | ~member(U_193, X_867, 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)))). % 67.95/58.22 tff(c_1013, plain, (![Z_895, Y_878, X_884, X1_901, Z_194, V_887, V_199, V_898, X_873, V_900, X1_881, X2_196, Z_874, X2_869, X2_896, X_889, Z_885, V_897, U_880, X1_883, W_192, X1_877, X_902, X1_195, V_891, W_868, Y_892, Z_882, X_197, Y_198, Y_879, U_193, X1_875, Y_893, X2_872, Y_871, X_870, Z_899, X2_886, X2_894]: (skf21(V_897, X_873, Y_879, Z_882, X1_883, X2_886, W_192, U_193)=skf21(V_887, X_889, Y_892, Z_895, X1_881, X2_872, W_192, U_193) | skf21(V_900, X_870, Y_871, Z_874, X1_877, X2_894, W_192, U_193)=skf21(V_897, X_873, Y_879, Z_882, X1_883, X2_886, W_192, U_193) | skf21(V_900, X_870, Y_871, Z_874, X1_877, X2_894, W_192, U_193)=skf21(V_887, X_889, Y_892, Z_895, X1_881, X2_872, W_192, U_193) | skf21(V_900, X_870, Y_871, Z_874, X1_877, X2_894, W_192, U_193)=skf21(V_891, X_902, Y_893, Z_885, X1_875, X2_869, W_192, U_193) | skf21(V_897, X_873, Y_879, Z_882, X1_883, X2_886, W_192, U_193)=skf21(V_891, X_902, Y_893, Z_885, X1_875, X2_869, W_192, U_193) | skf21(V_891, X_902, Y_893, Z_885, X1_875, X2_869, W_192, U_193)=skf21(V_887, X_889, Y_892, Z_895, X1_881, X2_872, W_192, U_193) | skf21(V_891, X_902, Y_893, Z_885, X1_875, X2_869, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_900, X_870, Y_871, Z_874, X1_877, X2_894, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_897, X_873, Y_879, Z_882, X1_883, X2_886, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_887, X_889, Y_892, Z_895, X1_881, X2_872, 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_880 | skf21(V_891, X_902, Y_893, Z_885, X1_875, X2_869, W_192, U_193)=U_880 | skf21(V_900, X_870, Y_871, Z_874, X1_877, X2_894, W_192, U_193)=U_880 | skf21(V_897, X_873, Y_879, Z_882, X1_883, X2_886, W_192, U_193)=U_880 | skf21(V_887, X_889, Y_892, Z_895, X1_881, X2_872, W_192, U_193)=U_880 | ~member(U_193, U_880, W_192) | skf21(U_880, V_898, W_868, X_884, Y_878, Z_899, X1_901, X2_896)!=U_880 | X2_872=X1_881 | Z_895=X1_881 | Z_895=X2_872 | Z_895=Y_892 | Y_892=X1_881 | Y_892=X2_872 | Y_892=X_889 | Z_895=X_889 | X_889=X1_881 | X_889=X2_872 | X_889=V_887 | Y_892=V_887 | Z_895=V_887 | X1_881=V_887 | X2_872=V_887 | ~member(U_193, X2_872, W_192) | ~member(U_193, X1_881, W_192) | ~member(U_193, Z_895, W_192) | ~member(U_193, Y_892, W_192) | ~member(U_193, X_889, W_192) | ~member(U_193, V_887, W_192) | X2_886=X1_883 | Z_882=X1_883 | Z_882=X2_886 | Z_882=Y_879 | Y_879=X1_883 | Y_879=X2_886 | Y_879=X_873 | Z_882=X_873 | X_873=X1_883 | X_873=X2_886 | X_873=V_897 | Y_879=V_897 | Z_882=V_897 | X1_883=V_897 | X2_886=V_897 | ~member(U_193, X2_886, W_192) | ~member(U_193, X1_883, W_192) | ~member(U_193, Z_882, W_192) | ~member(U_193, Y_879, W_192) | ~member(U_193, X_873, W_192) | ~member(U_193, V_897, W_192) | X2_894=X1_877 | Z_874=X1_877 | Z_874=X2_894 | Z_874=Y_871 | Y_871=X1_877 | Y_871=X2_894 | Y_871=X_870 | Z_874=X_870 | X_870=X1_877 | X_870=X2_894 | X_870=V_900 | Y_871=V_900 | Z_874=V_900 | X1_877=V_900 | X2_894=V_900 | ~member(U_193, X2_894, W_192) | ~member(U_193, X1_877, W_192) | ~member(U_193, Z_874, W_192) | ~member(U_193, Y_871, W_192) | ~member(U_193, X_870, W_192) | ~member(U_193, V_900, W_192) | X2_869=X1_875 | Z_885=X1_875 | Z_885=X2_869 | Z_885=Y_893 | Y_893=X1_875 | Y_893=X2_869 | Y_893=X_902 | Z_885=X_902 | X_902=X1_875 | X_902=X2_869 | X_902=V_891 | Y_893=V_891 | Z_885=V_891 | X1_875=V_891 | X2_869=V_891 | ~member(U_193, X2_869, W_192) | ~member(U_193, X1_875, W_192) | ~member(U_193, Z_885, W_192) | ~member(U_193, Y_893, W_192) | ~member(U_193, X_902, W_192) | ~member(U_193, V_891, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 68.07/58.22 tff(c_968, plain, (![X_788, Z_194, X2_780, V_199, X2_784, Z_802, X2_196, Y_797, U_804, Y_794, X1_787, Z_782, Z_805, X2_779, X_796, W_192, X1_195, V_799, V_793, X_806, V_800, X1_801, X2_790, X_197, Y_198, Y_795, X1_785, U_193, X_798, X1_783, Y_781, V_786, Z_789]: (skf21(V_799, X_788, Y_781, Z_805, X1_801, X2_780, W_192, U_193)=skf21(V_786, X_796, Y_795, Z_782, X1_785, X2_784, W_192, U_193) | skf21(V_793, X_806, Y_794, Z_789, X1_783, X2_779, W_192, U_193)=skf21(V_786, X_796, Y_795, Z_782, X1_785, X2_784, W_192, U_193) | skf21(V_799, X_788, Y_781, Z_805, X1_801, X2_780, W_192, U_193)=skf21(V_793, X_806, Y_794, Z_789, X1_783, X2_779, W_192, U_193) | skf21(V_793, X_806, Y_794, Z_789, X1_783, X2_779, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_786, X_796, Y_795, Z_782, X1_785, X2_784, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_799, X_788, Y_781, Z_805, X1_801, X2_780, 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_800 | skf21(V_793, X_806, Y_794, Z_789, X1_783, X2_779, W_192, U_193)=V_800 | skf21(V_786, X_796, Y_795, Z_782, X1_785, X2_784, W_192, U_193)=V_800 | skf21(V_799, X_788, Y_781, Z_805, X1_801, X2_780, W_192, U_193)=V_800 | V_800=U_804 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_804 | skf21(V_793, X_806, Y_794, Z_789, X1_783, X2_779, W_192, U_193)=U_804 | skf21(V_786, X_796, Y_795, Z_782, X1_785, X2_784, W_192, U_193)=U_804 | skf21(V_799, X_788, Y_781, Z_805, X1_801, X2_780, W_192, U_193)=U_804 | ~member(U_193, V_800, W_192) | ~member(U_193, U_804, W_192) | skf21(U_804, V_800, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_798, Y_797, Z_802, X1_787, X2_790)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_780=X1_801 | Z_805=X1_801 | Z_805=X2_780 | Z_805=Y_781 | Y_781=X1_801 | Y_781=X2_780 | Y_781=X_788 | Z_805=X_788 | X_788=X1_801 | X_788=X2_780 | X_788=V_799 | Y_781=V_799 | Z_805=V_799 | X1_801=V_799 | X2_780=V_799 | ~member(U_193, X2_780, W_192) | ~member(U_193, X1_801, W_192) | ~member(U_193, Z_805, W_192) | ~member(U_193, Y_781, W_192) | ~member(U_193, X_788, W_192) | ~member(U_193, V_799, W_192) | X2_784=X1_785 | Z_782=X1_785 | Z_782=X2_784 | Z_782=Y_795 | Y_795=X1_785 | Y_795=X2_784 | Y_795=X_796 | Z_782=X_796 | X_796=X1_785 | X_796=X2_784 | X_796=V_786 | Y_795=V_786 | Z_782=V_786 | X1_785=V_786 | X2_784=V_786 | ~member(U_193, X2_784, W_192) | ~member(U_193, X1_785, W_192) | ~member(U_193, Z_782, W_192) | ~member(U_193, Y_795, W_192) | ~member(U_193, X_796, W_192) | ~member(U_193, V_786, W_192) | X2_779=X1_783 | Z_789=X1_783 | Z_789=X2_779 | Z_789=Y_794 | Y_794=X1_783 | Y_794=X2_779 | Y_794=X_806 | Z_789=X_806 | X_806=X1_783 | X_806=X2_779 | X_806=V_793 | Y_794=V_793 | Z_789=V_793 | X1_783=V_793 | X2_779=V_793 | ~member(U_193, X2_779, W_192) | ~member(U_193, X1_783, W_192) | ~member(U_193, Z_789, W_192) | ~member(U_193, Y_794, W_192) | ~member(U_193, X_806, W_192) | ~member(U_193, V_793, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 68.07/58.22 tff(c_946, plain, (![X1_775, X1_773, Y_766, Z_194, V_199, X2_196, X_760, V_767, X_759, W_763, X2_765, V_771, X5_756, Y_761, X2_758, V_777, X_778, V_755, W_192, X2_750, X1_195, Y_751, U_754, Y_774, Z_768, X_197, Y_198, Z_753, Z_757, U_193, X_762, X1_772, Z_764, X2_749, X1_752]: (skf21(V_767, X_762, Y_751, Z_753, X1_773, X2_765, W_192, U_193)=skf21(V_755, X_759, Y_761, Z_764, X1_775, X2_758, W_192, U_193) | skf21(V_771, X_778, Y_774, Z_768, X1_752, X2_750, W_192, U_193)=skf21(V_767, X_762, Y_751, Z_753, X1_773, X2_765, W_192, U_193) | skf21(V_771, X_778, Y_774, Z_768, X1_752, X2_750, W_192, U_193)=skf21(V_755, X_759, Y_761, Z_764, X1_775, X2_758, W_192, U_193) | skf21(V_771, X_778, Y_774, Z_768, 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_767, X_762, Y_751, Z_753, X1_773, X2_765, 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_759, Y_761, Z_764, X1_775, X2_758, 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_756 | skf21(V_771, X_778, Y_774, Z_768, X1_752, X2_750, W_192, U_193)=X5_756 | skf21(V_767, X_762, Y_751, Z_753, X1_773, X2_765, W_192, U_193)=X5_756 | skf21(V_755, X_759, Y_761, Z_764, X1_775, X2_758, W_192, U_193)=X5_756 | X5_756=U_754 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_754 | skf21(V_771, X_778, Y_774, Z_768, X1_752, X2_750, W_192, U_193)=U_754 | skf21(V_767, X_762, Y_751, Z_753, X1_773, X2_765, W_192, U_193)=U_754 | skf21(V_755, X_759, Y_761, Z_764, X1_775, X2_758, W_192, U_193)=U_754 | ~member(U_193, X5_756, W_192) | ~member(U_193, U_754, W_192) | skf21(U_754, V_777, W_763, X_760, Y_766, Z_757, X1_772, X2_749)!=U_754 | X2_758=X1_775 | Z_764=X1_775 | Z_764=X2_758 | Z_764=Y_761 | Y_761=X1_775 | Y_761=X2_758 | Y_761=X_759 | Z_764=X_759 | X_759=X1_775 | X_759=X2_758 | X_759=V_755 | Y_761=V_755 | Z_764=V_755 | X1_775=V_755 | X2_758=V_755 | ~member(U_193, X2_758, W_192) | ~member(U_193, X1_775, W_192) | ~member(U_193, Z_764, W_192) | ~member(U_193, Y_761, W_192) | ~member(U_193, X_759, W_192) | ~member(U_193, V_755, W_192) | X2_765=X1_773 | Z_753=X1_773 | Z_753=X2_765 | Z_753=Y_751 | Y_751=X1_773 | Y_751=X2_765 | Y_751=X_762 | Z_753=X_762 | X_762=X1_773 | X_762=X2_765 | X_762=V_767 | Y_751=V_767 | Z_753=V_767 | X1_773=V_767 | X2_765=V_767 | ~member(U_193, X2_765, W_192) | ~member(U_193, X1_773, W_192) | ~member(U_193, Z_753, W_192) | ~member(U_193, Y_751, W_192) | ~member(U_193, X_762, W_192) | ~member(U_193, V_767, W_192) | X2_750=X1_752 | Z_768=X1_752 | Z_768=X2_750 | Z_768=Y_774 | Y_774=X1_752 | Y_774=X2_750 | Y_774=X_778 | Z_768=X_778 | X_778=X1_752 | X_778=X2_750 | X_778=V_771 | Y_774=V_771 | Z_768=V_771 | X1_752=V_771 | X2_750=V_771 | ~member(U_193, X2_750, W_192) | ~member(U_193, X1_752, W_192) | ~member(U_193, Z_768, W_192) | ~member(U_193, Y_774, W_192) | ~member(U_193, X_778, W_192) | ~member(U_193, V_771, 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)))). % 68.07/58.23 tff(c_924, plain, (![V_742, Z_194, V_199, X2_196, V_748, X_725, X2_732, V_737, Z_734, X_747, Z_730, W_192, Y_739, Z_724, X2_726, X1_195, V_744, X_745, W_728, U_729, X_738, X2_722, Y_741, Z_733, X1_721, X1_727, Y_743, X_197, Y_198, U_193, Y_740, X1_720, X1_731, X2_723]: (skf21(V_748, X_738, Y_743, Z_730, X1_720, X2_722, W_192, U_193)=skf21(V_742, X_745, Y_741, Z_724, X1_731, X2_726, W_192, U_193) | skf21(V_742, X_745, Y_741, Z_724, X1_731, X2_726, W_192, U_193)=skf21(V_737, X_747, Y_739, Z_733, X1_727, X2_723, W_192, U_193) | skf21(V_748, X_738, Y_743, Z_730, X1_720, X2_722, W_192, U_193)=skf21(V_737, X_747, Y_739, Z_733, X1_727, X2_723, W_192, U_193) | skf21(V_737, X_747, Y_739, Z_733, X1_727, X2_723, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_742, X_745, Y_741, Z_724, X1_731, X2_726, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_748, X_738, Y_743, Z_730, X1_720, X2_722, 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_744 | skf21(V_737, X_747, Y_739, Z_733, X1_727, X2_723, W_192, U_193)=V_744 | skf21(V_742, X_745, Y_741, Z_724, X1_731, X2_726, W_192, U_193)=V_744 | skf21(V_748, X_738, Y_743, Z_730, X1_720, X2_722, W_192, U_193)=V_744 | V_744=U_729 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_729 | skf21(V_737, X_747, Y_739, Z_733, X1_727, X2_723, W_192, U_193)=U_729 | skf21(V_742, X_745, Y_741, Z_724, X1_731, X2_726, W_192, U_193)=U_729 | skf21(V_748, X_738, Y_743, Z_730, X1_720, X2_722, W_192, U_193)=U_729 | ~member(U_193, V_744, W_192) | ~member(U_193, U_729, W_192) | skf21(U_729, V_744, W_728, X_725, Y_740, Z_734, X1_721, X2_732)!=V_744 | X2_722=X1_720 | Z_730=X1_720 | Z_730=X2_722 | Z_730=Y_743 | Y_743=X1_720 | Y_743=X2_722 | Y_743=X_738 | Z_730=X_738 | X_738=X1_720 | X_738=X2_722 | X_738=V_748 | Y_743=V_748 | Z_730=V_748 | X1_720=V_748 | X2_722=V_748 | ~member(U_193, X2_722, W_192) | ~member(U_193, X1_720, W_192) | ~member(U_193, Z_730, W_192) | ~member(U_193, Y_743, W_192) | ~member(U_193, X_738, W_192) | ~member(U_193, V_748, W_192) | X2_726=X1_731 | Z_724=X1_731 | Z_724=X2_726 | Z_724=Y_741 | Y_741=X1_731 | Y_741=X2_726 | Y_741=X_745 | Z_724=X_745 | X_745=X1_731 | X_745=X2_726 | X_745=V_742 | Y_741=V_742 | Z_724=V_742 | X1_731=V_742 | X2_726=V_742 | ~member(U_193, X2_726, W_192) | ~member(U_193, X1_731, W_192) | ~member(U_193, Z_724, W_192) | ~member(U_193, Y_741, W_192) | ~member(U_193, X_745, W_192) | ~member(U_193, V_742, W_192) | X2_723=X1_727 | Z_733=X1_727 | Z_733=X2_723 | Z_733=Y_739 | Y_739=X1_727 | Y_739=X2_723 | Y_739=X_747 | Z_733=X_747 | X_747=X1_727 | X_747=X2_723 | X_747=V_737 | Y_739=V_737 | Z_733=V_737 | X1_727=V_737 | X2_723=V_737 | ~member(U_193, X2_723, W_192) | ~member(U_193, X1_727, W_192) | ~member(U_193, Z_733, W_192) | ~member(U_193, Y_739, W_192) | ~member(U_193, X_747, W_192) | ~member(U_193, V_737, 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)))). % 68.07/58.23 tff(c_857, plain, (![Y_628, X_630, Z_194, V_199, X2_196, Z_647, W_646, Z_636, X2_629, V_640, U_637, X2_645, X1_631, W_192, X1_195, X1_632, V_635, X_197, Y_198, Y_648, U_193, Z_641, X1_634, X2_633, X_649, Y_643, V_642]: (skf21(V_640, X_649, Y_643, Z_636, X1_631, X2_629, W_192, U_193)=skf21(V_635, X_630, Y_628, Z_647, X1_632, X2_633, W_192, U_193) | skf21(V_640, X_649, Y_643, Z_636, X1_631, X2_629, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_635, X_630, Y_628, Z_647, X1_632, X2_633, 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_646 | skf21(V_640, X_649, Y_643, Z_636, X1_631, X2_629, W_192, U_193)=W_646 | skf21(V_635, X_630, Y_628, Z_647, X1_632, X2_633, W_192, U_193)=W_646 | W_646=V_642 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_642 | skf21(V_640, X_649, Y_643, Z_636, X1_631, X2_629, W_192, U_193)=V_642 | skf21(V_635, X_630, Y_628, Z_647, X1_632, X2_633, W_192, U_193)=V_642 | V_642=U_637 | W_646=U_637 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_637 | skf21(V_640, X_649, Y_643, Z_636, X1_631, X2_629, W_192, U_193)=U_637 | skf21(V_635, X_630, Y_628, Z_647, X1_632, X2_633, W_192, U_193)=U_637 | ~member(U_193, W_646, W_192) | ~member(U_193, V_642, W_192) | ~member(U_193, U_637, W_192) | skf21(U_637, V_642, W_646, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_648, Z_641, X1_634, X2_645)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_633=X1_632 | Z_647=X1_632 | Z_647=X2_633 | Z_647=Y_628 | Y_628=X1_632 | Y_628=X2_633 | Y_628=X_630 | Z_647=X_630 | X_630=X1_632 | X_630=X2_633 | X_630=V_635 | Y_628=V_635 | Z_647=V_635 | X1_632=V_635 | X2_633=V_635 | ~member(U_193, X2_633, W_192) | ~member(U_193, X1_632, W_192) | ~member(U_193, Z_647, W_192) | ~member(U_193, Y_628, W_192) | ~member(U_193, X_630, W_192) | ~member(U_193, V_635, W_192) | X2_629=X1_631 | Z_636=X1_631 | Z_636=X2_629 | Z_636=Y_643 | Y_643=X1_631 | Y_643=X2_629 | Y_643=X_649 | Z_636=X_649 | X_649=X1_631 | X_649=X2_629 | X_649=V_640 | Y_643=V_640 | Z_636=V_640 | X1_631=V_640 | X2_629=V_640 | ~member(U_193, X2_629, W_192) | ~member(U_193, X1_631, W_192) | ~member(U_193, Z_636, W_192) | ~member(U_193, Y_643, W_192) | ~member(U_193, X_649, W_192) | ~member(U_193, V_640, 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)))). % 68.07/58.23 tff(c_835, plain, (![X1_612, Z_194, V_199, X2_606, X_611, V_617, Z_620, X2_196, Y_622, W_610, V_618, Y_621, W_192, U_624, X1_607, V_614, X2_625, X1_195, Z_605, X_626, Z_613, Y_627, X_609, X_197, Y_198, X1_619, X2_608, U_193]: (skf21(V_618, X_626, Y_621, Z_613, X1_607, X2_606, W_192, U_193)=skf21(V_617, X_609, Y_627, Z_620, X1_619, X2_625, W_192, U_193) | skf21(V_618, X_626, Y_621, Z_613, 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_617, X_609, Y_627, Z_620, X1_619, X2_625, 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_610 | skf21(V_618, X_626, Y_621, Z_613, X1_607, X2_606, W_192, U_193)=W_610 | skf21(V_617, X_609, Y_627, Z_620, X1_619, X2_625, W_192, U_193)=W_610 | W_610=V_614 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_614 | skf21(V_618, X_626, Y_621, Z_613, X1_607, X2_606, W_192, U_193)=V_614 | skf21(V_617, X_609, Y_627, Z_620, X1_619, X2_625, W_192, U_193)=V_614 | V_614=U_624 | W_610=U_624 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_624 | skf21(V_618, X_626, Y_621, Z_613, X1_607, X2_606, W_192, U_193)=U_624 | skf21(V_617, X_609, Y_627, Z_620, X1_619, X2_625, W_192, U_193)=U_624 | ~member(U_193, W_610, W_192) | ~member(U_193, V_614, W_192) | ~member(U_193, U_624, W_192) | skf21(U_624, V_614, W_610, X_611, Y_622, Z_605, X1_612, X2_608)!=W_610 | X2_625=X1_619 | Z_620=X1_619 | Z_620=X2_625 | Z_620=Y_627 | Y_627=X1_619 | Y_627=X2_625 | Y_627=X_609 | Z_620=X_609 | X_609=X1_619 | X_609=X2_625 | X_609=V_617 | Y_627=V_617 | Z_620=V_617 | X1_619=V_617 | X2_625=V_617 | ~member(U_193, X2_625, W_192) | ~member(U_193, X1_619, W_192) | ~member(U_193, Z_620, W_192) | ~member(U_193, Y_627, W_192) | ~member(U_193, X_609, W_192) | ~member(U_193, V_617, W_192) | X2_606=X1_607 | Z_613=X1_607 | Z_613=X2_606 | Z_613=Y_621 | Y_621=X1_607 | Y_621=X2_606 | Y_621=X_626 | Z_613=X_626 | X_626=X1_607 | X_626=X2_606 | X_626=V_618 | Y_621=V_618 | Z_613=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_613, W_192) | ~member(U_193, Y_621, 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)))). % 68.07/58.23 tff(c_879, plain, (![X1_659, Z_194, Y_669, V_199, Z_668, X2_196, X6_672, X_673, X5_670, W_651, X1_653, Z_658, V_655, X_666, V_671, Y_663, Z_650, X2_674, W_192, X1_195, X_654, V_662, U_657, X1_656, X_197, Y_198, X2_652, U_193, X2_664, Y_665]: (skf21(V_671, X_666, Y_665, Z_650, X1_659, X2_674, W_192, U_193)=skf21(V_662, X_673, Y_663, Z_658, X1_653, X2_652, W_192, U_193) | skf21(V_662, X_673, Y_663, Z_658, X1_653, X2_652, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_671, X_666, Y_665, Z_650, X1_659, X2_674, 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_672 | skf21(V_662, X_673, Y_663, Z_658, X1_653, X2_652, W_192, U_193)=X6_672 | skf21(V_671, X_666, Y_665, Z_650, X1_659, X2_674, W_192, U_193)=X6_672 | X6_672=X5_670 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_670 | skf21(V_662, X_673, Y_663, Z_658, X1_653, X2_652, W_192, U_193)=X5_670 | skf21(V_671, X_666, Y_665, Z_650, X1_659, X2_674, W_192, U_193)=X5_670 | X5_670=U_657 | X6_672=U_657 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_657 | skf21(V_662, X_673, Y_663, Z_658, X1_653, X2_652, W_192, U_193)=U_657 | skf21(V_671, X_666, Y_665, Z_650, X1_659, X2_674, W_192, U_193)=U_657 | ~member(U_193, X6_672, W_192) | ~member(U_193, X5_670, W_192) | ~member(U_193, U_657, W_192) | skf21(U_657, V_655, W_651, X_654, Y_669, Z_668, X1_656, X2_664)!=U_657 | X2_674=X1_659 | Z_650=X1_659 | Z_650=X2_674 | Z_650=Y_665 | Y_665=X1_659 | Y_665=X2_674 | Y_665=X_666 | Z_650=X_666 | X_666=X1_659 | X_666=X2_674 | X_666=V_671 | Y_665=V_671 | Z_650=V_671 | X1_659=V_671 | X2_674=V_671 | ~member(U_193, X2_674, W_192) | ~member(U_193, X1_659, W_192) | ~member(U_193, Z_650, W_192) | ~member(U_193, Y_665, W_192) | ~member(U_193, X_666, W_192) | ~member(U_193, V_671, W_192) | X2_652=X1_653 | Z_658=X1_653 | Z_658=X2_652 | Z_658=Y_663 | Y_663=X1_653 | Y_663=X2_652 | Y_663=X_673 | Z_658=X_673 | X_673=X1_653 | X_673=X2_652 | X_673=V_662 | Y_663=V_662 | Z_658=V_662 | X1_653=V_662 | X2_652=V_662 | ~member(U_193, X2_652, W_192) | ~member(U_193, X1_653, W_192) | ~member(U_193, Z_658, W_192) | ~member(U_193, Y_663, W_192) | ~member(U_193, X_673, W_192) | ~member(U_193, V_662, 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)))). % 68.07/58.23 tff(c_901, plain, (![Z_688, V_683, X_698, Z_194, V_199, Y_695, Y_684, X2_196, V_693, Y_685, U_676, X5_689, X2_687, X1_690, W_192, W_694, X_678, X1_195, X_696, Z_681, X2_697, X_197, Y_198, Z_679, X1_677, U_193, X2_675, V_680, X1_682]: (skf21(V_693, X_698, Y_695, Z_688, X1_677, X2_675, W_192, U_193)=skf21(V_683, X_678, Y_685, Z_679, X1_682, X2_697, W_192, U_193) | skf21(V_693, X_698, Y_695, Z_688, 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_683, X_678, Y_685, Z_679, X1_682, X2_697, 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_689 | skf21(V_693, X_698, Y_695, Z_688, X1_677, X2_675, W_192, U_193)=X5_689 | skf21(V_683, X_678, Y_685, Z_679, X1_682, X2_697, W_192, U_193)=X5_689 | X5_689=V_680 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_680 | skf21(V_693, X_698, Y_695, Z_688, X1_677, X2_675, W_192, U_193)=V_680 | skf21(V_683, X_678, Y_685, Z_679, X1_682, X2_697, W_192, U_193)=V_680 | V_680=U_676 | X5_689=U_676 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_676 | skf21(V_693, X_698, Y_695, Z_688, X1_677, X2_675, W_192, U_193)=U_676 | skf21(V_683, X_678, Y_685, Z_679, X1_682, X2_697, W_192, U_193)=U_676 | ~member(U_193, X5_689, W_192) | ~member(U_193, V_680, W_192) | ~member(U_193, U_676, W_192) | skf21(U_676, V_680, W_694, X_696, Y_684, Z_681, X1_690, X2_687)!=V_680 | X2_697=X1_682 | Z_679=X1_682 | Z_679=X2_697 | Z_679=Y_685 | Y_685=X1_682 | Y_685=X2_697 | Y_685=X_678 | Z_679=X_678 | X_678=X1_682 | X_678=X2_697 | X_678=V_683 | Y_685=V_683 | Z_679=V_683 | X1_682=V_683 | X2_697=V_683 | ~member(U_193, X2_697, W_192) | ~member(U_193, X1_682, W_192) | ~member(U_193, Z_679, W_192) | ~member(U_193, Y_685, W_192) | ~member(U_193, X_678, W_192) | ~member(U_193, V_683, W_192) | X2_675=X1_677 | Z_688=X1_677 | Z_688=X2_675 | Z_688=Y_695 | Y_695=X1_677 | Y_695=X2_675 | Y_695=X_698 | Z_688=X_698 | X_698=X1_677 | X_698=X2_675 | X_698=V_693 | Y_695=V_693 | Z_688=V_693 | X1_677=V_693 | X2_675=V_693 | ~member(U_193, X2_675, W_192) | ~member(U_193, X1_677, W_192) | ~member(U_193, Z_688, W_192) | ~member(U_193, Y_695, W_192) | ~member(U_193, X_698, W_192) | ~member(U_193, V_693, 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)))). % 68.07/58.23 tff(c_768, plain, (![X1_546, Y_551, Z_536, Z_194, W_541, V_199, X_538, X2_196, X_549, Z_548, U_540, W_192, X1_195, X1_545, X2_537, V_547, X_197, Y_198, V_550, U_193, X2_539]: (skf21(V_547, X_549, Y_551, Z_536, X1_545, 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_538 | skf21(V_547, X_549, Y_551, Z_536, X1_545, X2_539, W_192, U_193)=X_538 | X_538=W_541 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_541 | skf21(V_547, X_549, Y_551, Z_536, X1_545, X2_539, W_192, U_193)=W_541 | W_541=V_550 | X_538=V_550 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_550 | skf21(V_547, X_549, Y_551, Z_536, X1_545, X2_539, W_192, U_193)=V_550 | V_550=U_540 | W_541=U_540 | X_538=U_540 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_540 | skf21(V_547, X_549, Y_551, Z_536, X1_545, X2_539, W_192, U_193)=U_540 | ~member(U_193, X_538, W_192) | ~member(U_193, W_541, W_192) | ~member(U_193, V_550, W_192) | ~member(U_193, U_540, W_192) | skf21(U_540, V_550, W_541, X_538, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_548, X1_546, X2_537)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_539=X1_545 | Z_536=X1_545 | Z_536=X2_539 | Z_536=Y_551 | Y_551=X1_545 | Y_551=X2_539 | Y_551=X_549 | Z_536=X_549 | X_549=X1_545 | X_549=X2_539 | X_549=V_547 | Y_551=V_547 | Z_536=V_547 | X1_545=V_547 | X2_539=V_547 | ~member(U_193, X2_539, W_192) | ~member(U_193, X1_545, W_192) | ~member(U_193, Z_536, W_192) | ~member(U_193, Y_551, W_192) | ~member(U_193, X_549, W_192) | ~member(U_193, V_547, 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)))). % 68.07/58.23 tff(c_724, plain, (![X1_511, Z_194, V_505, X1_518, V_199, X_513, X5_504, X2_196, Y_516, X_506, X2_500, U_514, W_192, X1_195, Z_501, X6_502, Y_517, Z_509, X_197, Y_198, X2_503, U_193, W_508, V_512]: (skf21(V_512, X_513, Y_517, Z_501, X1_511, X2_503, 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_502 | skf21(V_512, X_513, Y_517, Z_501, X1_511, X2_503, W_192, U_193)=X6_502 | X6_502=X5_504 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_504 | skf21(V_512, X_513, Y_517, Z_501, X1_511, X2_503, W_192, U_193)=X5_504 | X5_504=V_505 | X6_502=V_505 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_505 | skf21(V_512, X_513, Y_517, Z_501, X1_511, X2_503, W_192, U_193)=V_505 | V_505=U_514 | X5_504=U_514 | X6_502=U_514 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_514 | skf21(V_512, X_513, Y_517, Z_501, X1_511, X2_503, W_192, U_193)=U_514 | ~member(U_193, X6_502, 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_506, Y_516, Z_509, X1_518, X2_500)!=V_505 | X2_503=X1_511 | Z_501=X1_511 | Z_501=X2_503 | Z_501=Y_517 | Y_517=X1_511 | Y_517=X2_503 | Y_517=X_513 | Z_501=X_513 | X_513=X1_511 | X_513=X2_503 | X_513=V_512 | Y_517=V_512 | Z_501=V_512 | X1_511=V_512 | X2_503=V_512 | ~member(U_193, X2_503, W_192) | ~member(U_193, X1_511, W_192) | ~member(U_193, Z_501, W_192) | ~member(U_193, Y_517, W_192) | ~member(U_193, X_513, W_192) | ~member(U_193, V_512, 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)))). % 68.07/58.23 tff(c_790, plain, (![Y_570, X2_556, X5_569, V_560, X7_553, Y_562, V_566, Z_194, V_199, X1_565, X2_196, Z_552, W_192, X1_195, W_554, X_197, Y_198, X_567, Z_561, X6_568, U_193, X2_559, X_558, X1_564, U_571]: (skf21(V_566, X_567, Y_570, Z_552, X1_564, X2_556, 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_553 | skf21(V_566, X_567, Y_570, Z_552, X1_564, X2_556, W_192, U_193)=X7_553 | X7_553=X6_568 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_568 | skf21(V_566, X_567, Y_570, Z_552, X1_564, X2_556, W_192, U_193)=X6_568 | X6_568=X5_569 | X7_553=X5_569 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_569 | skf21(V_566, X_567, Y_570, Z_552, X1_564, X2_556, W_192, U_193)=X5_569 | X5_569=U_571 | X6_568=U_571 | X7_553=U_571 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_571 | skf21(V_566, X_567, Y_570, Z_552, X1_564, X2_556, W_192, U_193)=U_571 | ~member(U_193, X7_553, W_192) | ~member(U_193, X6_568, W_192) | ~member(U_193, X5_569, W_192) | ~member(U_193, U_571, W_192) | skf21(U_571, V_560, W_554, X_558, Y_562, Z_561, X1_565, X2_559)!=U_571 | X2_556=X1_564 | Z_552=X1_564 | Z_552=X2_556 | Z_552=Y_570 | Y_570=X1_564 | Y_570=X2_556 | Y_570=X_567 | Z_552=X_567 | X_567=X1_564 | X_567=X2_556 | X_567=V_566 | Y_570=V_566 | Z_552=V_566 | X1_564=V_566 | X2_556=V_566 | ~member(U_193, X2_556, W_192) | ~member(U_193, X1_564, W_192) | ~member(U_193, Z_552, W_192) | ~member(U_193, Y_570, W_192) | ~member(U_193, X_567, W_192) | ~member(U_193, V_566, 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)))). % 68.07/58.23 tff(c_746, plain, (![U_525, Y_535, X2_524, Z_194, V_199, V_533, V_527, X2_196, X2_523, Z_520, W_192, X_534, X1_195, Z_519, X_197, Y_198, X_522, X1_526, U_193, Y_521, W_529, X1_532]: (skf21(V_533, X_534, Y_535, Z_519, X1_532, X2_523, 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_522 | skf21(V_533, X_534, Y_535, Z_519, X1_532, X2_523, W_192, U_193)=X_522 | X_522=W_529 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_529 | skf21(V_533, X_534, Y_535, Z_519, X1_532, X2_523, W_192, U_193)=W_529 | W_529=V_527 | X_522=V_527 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_527 | skf21(V_533, X_534, Y_535, Z_519, X1_532, X2_523, W_192, U_193)=V_527 | V_527=U_525 | W_529=U_525 | X_522=U_525 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_525 | skf21(V_533, X_534, Y_535, Z_519, X1_532, X2_523, W_192, U_193)=U_525 | ~member(U_193, X_522, W_192) | ~member(U_193, W_529, W_192) | ~member(U_193, V_527, W_192) | ~member(U_193, U_525, W_192) | skf21(U_525, V_527, W_529, X_522, Y_521, Z_520, X1_526, X2_524)!=X_522 | X2_523=X1_532 | Z_519=X1_532 | Z_519=X2_523 | Z_519=Y_535 | Y_535=X1_532 | Y_535=X2_523 | Y_535=X_534 | Z_519=X_534 | X_534=X1_532 | X_534=X2_523 | X_534=V_533 | Y_535=V_533 | Z_519=V_533 | X1_532=V_533 | X2_523=V_533 | ~member(U_193, X2_523, W_192) | ~member(U_193, X1_532, W_192) | ~member(U_193, Z_519, W_192) | ~member(U_193, Y_535, W_192) | ~member(U_193, X_534, W_192) | ~member(U_193, V_533, 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)))). % 68.07/58.23 tff(c_812, plain, (![X_586, Z_194, X5_587, V_199, X2_577, X2_196, U_578, X1_573, X1_582, Z_574, Y_588, W_192, X1_195, Y_589, V_584, X2_575, X_197, Y_198, Z_572, W_576, X_585, U_193, V_583]: (skf21(V_584, X_585, Y_589, Z_572, X1_582, X2_575, 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_584, X_585, Y_589, Z_572, X1_582, X2_575, W_192, U_193)=X5_587 | X5_587=W_576 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_576 | skf21(V_584, X_585, Y_589, Z_572, X1_582, X2_575, W_192, U_193)=W_576 | W_576=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_584, X_585, Y_589, Z_572, X1_582, X2_575, W_192, U_193)=V_583 | V_583=U_578 | W_576=U_578 | X5_587=U_578 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_578 | skf21(V_584, X_585, Y_589, Z_572, X1_582, X2_575, W_192, U_193)=U_578 | ~member(U_193, X5_587, W_192) | ~member(U_193, W_576, W_192) | ~member(U_193, V_583, W_192) | ~member(U_193, U_578, W_192) | skf21(U_578, V_583, W_576, X_586, Y_588, Z_574, X1_573, X2_577)!=W_576 | X2_575=X1_582 | Z_572=X1_582 | Z_572=X2_575 | Z_572=Y_589 | Y_589=X1_582 | Y_589=X2_575 | Y_589=X_585 | Z_572=X_585 | X_585=X1_582 | X_585=X2_575 | X_585=V_584 | Y_589=V_584 | Z_572=V_584 | X1_582=V_584 | X2_575=V_584 | ~member(U_193, X2_575, W_192) | ~member(U_193, X1_582, W_192) | ~member(U_193, Z_572, W_192) | ~member(U_193, Y_589, W_192) | ~member(U_193, X_585, W_192) | ~member(U_193, V_584, 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)))). % 68.07/58.23 tff(c_704, plain, (![X_206, X1_204, X2_492, W_200, U_495, V_208, X2_205, Y_498, U_202, Y_207, V_497, Z_494, X_499, W_496, X1_493]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=Y_207 | Y_207=X_206 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X_206 | X_206=W_200 | Y_207=W_200 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_202 | ~member(U_495, Y_207, W_496) | ~member(U_495, X_206, W_496) | ~member(U_495, W_200, W_496) | ~member(U_495, V_208, W_496) | ~member(U_495, U_202, W_496) | skf21(U_202, V_208, W_200, X_206, Y_207, skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495), X1_204, X2_205)!=skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495) | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 tff(c_702, plain, (![X6_151, X2_158, X2_492, U_495, Y_160, X1_157, X_159, W_152, V_161, Y_498, V_497, Z_494, X5_150, X_499, W_496, X1_493, Z_155, U_154]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X6_151 | X6_151=X5_150 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_154 | ~member(U_495, X6_151, W_496) | ~member(U_495, X5_150, W_496) | ~member(U_495, W_152, W_496) | ~member(U_495, V_161, W_496) | ~member(U_495, U_154, W_496) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 tff(c_703, plain, (![Z_183, X8_190, X2_492, X5_177, U_495, X1_185, V_189, X_187, Y_188, U_181, X2_186, X7_184, X6_178, Y_498, V_497, W_179, Z_494, X_499, W_496, X1_493]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X8_190 | X8_190=X7_184 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_181 | ~member(U_495, X8_190, W_496) | ~member(U_495, X7_184, W_496) | ~member(U_495, X6_178, W_496) | ~member(U_495, X5_177, W_496) | ~member(U_495, U_181, W_496) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 tff(c_701, plain, (![U_130, X2_492, U_495, X1_132, V_136, Y_135, Y_498, W_128, V_497, X2_133, Z_494, Z_131, X_499, W_496, X_134, X1_493]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=Y_135 | Y_135=X_134 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X_134 | X_134=W_128 | Y_135=W_128 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_130 | ~member(U_495, Y_135, W_496) | ~member(U_495, X_134, W_496) | ~member(U_495, W_128, W_496) | ~member(U_495, V_136, W_496) | ~member(U_495, U_130, W_496) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 tff(c_705, plain, (![U_142, X2_492, W_140, U_495, X2_145, X5_138, Y_147, V_148, Y_498, V_497, Z_494, Z_143, X1_144, X_146, X_499, W_496, X1_493]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X5_138 | X_146=X5_138 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X_146 | X_146=W_140 | X5_138=W_140 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_142 | ~member(U_495, X5_138, W_496) | ~member(U_495, X_146, W_496) | ~member(U_495, W_140, W_496) | ~member(U_495, V_148, W_496) | ~member(U_495, U_142, W_496) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 tff(c_700, plain, (![X2_492, X2_171, U_495, X6_164, V_174, U_167, Z_168, W_165, Y_498, X5_163, X1_170, X7_169, V_497, Z_494, X_172, Y_173, X_499, W_496, X1_493]: (skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X7_169 | X7_169=X6_164 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf21(V_497, X_499, Y_498, Z_494, X1_493, X2_492, W_496, U_495)=U_167 | ~member(U_495, X7_169, W_496) | ~member(U_495, X6_164, W_496) | ~member(U_495, X5_163, W_496) | ~member(U_495, V_174, W_496) | ~member(U_495, U_167, W_496) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_492=X1_493 | Z_494=X1_493 | Z_494=X2_492 | Z_494=Y_498 | Y_498=X1_493 | Y_498=X2_492 | Y_498=X_499 | Z_494=X_499 | X_499=X1_493 | X_499=X2_492 | X_499=V_497 | Y_498=V_497 | Z_494=V_497 | X1_493=V_497 | X2_492=V_497 | six(U_495, W_496) | ~member(U_495, X2_492, W_496) | ~member(U_495, X1_493, W_496) | ~member(U_495, Z_494, W_496) | ~member(U_495, Y_498, W_496) | ~member(U_495, X_499, W_496) | ~member(U_495, V_497, W_496)))). % 68.07/58.24 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)))). % 68.07/58.24 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))). % 68.07/58.24 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))). % 68.07/58.24 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))). % 68.07/58.24 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))). % 68.07/58.24 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))). % 68.07/58.24 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))). % 68.07/58.24 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)))). % 68.07/58.24 tff(c_533, plain, (![V_212, U_211]: (~male(skc2, V_212) | ~man(skc2, V_212) | ~of(skc2, U_211, V_212) | ~member(skc2, U_211, skc3) | ~cannon(skc2, U_211)))). % 68.07/58.24 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)))). % 68.07/58.24 tff(c_531, plain, (skf16(skc3, skc2)!=skf14(skc3, skc2))). % 68.07/58.24 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf16(U_113, V_114)!=skf14(U_113, V_114)))). % 68.07/58.24 tff(c_526, plain, (skf18(skc3, skc2)!=skf10(skc3, skc2))). % 68.07/58.24 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf18(U_101, V_102)!=skf10(U_101, V_102)))). % 68.07/58.24 tff(c_521, plain, (skf18(skc3, skc2)!=skf12(skc3, skc2))). % 68.07/58.24 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf18(U_103, V_104)!=skf12(U_103, V_104)))). % 68.07/58.24 tff(c_516, plain, (skf16(skc3, skc2)!=skf12(skc3, skc2))). % 68.07/58.24 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf16(U_111, V_112)!=skf12(U_111, V_112)))). % 68.07/58.24 tff(c_511, plain, (skf12(skc3, skc2)!=skf10(skc3, skc2))). % 68.07/58.24 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf12(U_119, V_120)!=skf10(U_119, V_120)))). % 68.07/58.24 tff(c_506, plain, (act(skc2, skf14(skc3, skc2)))). % 68.07/58.24 tff(c_502, plain, (action(skc2, skf14(skc3, skc2)))). % 68.07/58.24 tff(c_498, plain, (shot(skc2, skf14(skc3, skc2)))). % 68.07/58.24 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf14(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 68.07/58.24 tff(c_490, plain, (skf14(skc3, skc2)!=skf10(skc3, skc2))). % 68.07/58.25 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf14(U_115, V_116)!=skf10(U_115, V_116)))). % 68.07/58.25 tff(c_485, plain, (act(skc2, skf18(skc3, skc2)))). % 68.07/58.25 tff(c_481, plain, (action(skc2, skf18(skc3, skc2)))). % 68.07/58.25 tff(c_477, plain, (shot(skc2, skf18(skc3, skc2)))). % 68.07/58.25 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf18(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 68.07/58.25 tff(c_469, plain, (act(skc2, skf16(skc3, skc2)))). % 68.07/58.25 tff(c_465, plain, (action(skc2, skf16(skc3, skc2)))). % 68.07/58.25 tff(c_461, plain, (shot(skc2, skf16(skc3, skc2)))). % 68.07/58.25 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf16(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 68.07/58.25 tff(c_453, plain, (skf18(skc3, skc2)!=skf14(skc3, skc2))). % 68.07/58.25 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf18(U_105, V_106)!=skf14(U_105, V_106)))). % 68.07/58.25 tff(c_448, plain, (act(skc2, skf20(skc3, skc2)))). % 68.07/58.25 tff(c_444, plain, (action(skc2, skf20(skc3, skc2)))). % 68.07/58.25 tff(c_440, plain, (shot(skc2, skf20(skc3, skc2)))). % 68.07/58.25 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf20(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 68.07/58.25 tff(c_431, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.07/58.25 tff(c_371, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 68.20/58.25 tff(c_426, plain, (skf20(skc3, skc2)!=skf12(skc3, skc2))). % 68.20/58.25 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf20(U_93, V_94)!=skf12(U_93, V_94)))). % 68.20/58.25 tff(c_324, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 68.20/58.25 tff(c_420, plain, (act(skc2, skf10(skc3, skc2)))). % 68.20/58.25 tff(c_416, plain, (action(skc2, skf10(skc3, skc2)))). % 68.20/58.25 tff(c_412, plain, (shot(skc2, skf10(skc3, skc2)))). % 68.20/58.25 tff(c_404, plain, (~artifact(skc2, skc3))). % 68.20/58.25 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf10(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 68.20/58.25 tff(c_400, plain, (~entity(skc2, skc3))). % 68.20/58.25 tff(c_356, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 68.20/58.25 tff(c_395, plain, (skf20(skc3, skc2)!=skf18(skc3, skc2))). % 68.20/58.25 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf20(U_99, V_100)!=skf18(U_99, V_100)))). % 68.20/58.25 tff(c_318, plain, (![U_345, V_346]: (artifact(U_345, V_346) | ~cannon(U_345, V_346)))). % 68.20/58.25 tff(c_381, plain, (skf18(skc3, skc2)!=skf16(skc3, skc2))). % 68.20/58.26 tff(c_389, plain, (~act(skc2, skc3))). % 68.20/58.26 tff(c_385, plain, (~event(skc2, skc3))). % 68.20/58.26 tff(c_376, plain, (~eventuality(skc2, skc3))). % 68.20/58.26 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf18(U_107, V_108)!=skf16(U_107, V_108)))). % 68.20/58.26 tff(c_361, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 68.20/58.26 tff(c_335, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 68.20/58.26 tff(c_366, plain, (skf20(skc3, skc2)!=skf16(skc3, skc2))). % 68.20/58.26 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf20(U_97, V_98)!=skf16(U_97, V_98)))). % 68.20/58.26 tff(c_290, plain, (![U_329, V_330]: (~multiple(U_329, V_330) | ~eventuality(U_329, V_330)))). % 68.20/58.26 tff(c_307, plain, (![U_339, V_340]: (~multiple(U_339, V_340) | ~entity(U_339, V_340)))). % 68.20/58.26 tff(c_351, plain, (act(skc2, skf12(skc3, skc2)))). % 68.20/58.26 tff(c_347, plain, (action(skc2, skf12(skc3, skc2)))). % 68.20/58.26 tff(c_343, plain, (shot(skc2, skf12(skc3, skc2)))). % 68.20/58.26 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf12(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 68.20/58.26 tff(c_261, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 68.20/58.26 tff(c_272, plain, (![U_319, V_320]: (~animate(U_319, V_320) | ~artifact(U_319, V_320)))). % 68.20/58.26 tff(c_329, plain, (skf20(skc3, skc2)!=skf14(skc3, skc2))). % 68.20/58.26 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf20(U_95, V_96)!=skf14(U_95, V_96)))). % 68.20/58.26 tff(c_273, plain, (![U_319, V_320]: (~living(U_319, V_320) | ~artifact(U_319, V_320)))). % 68.20/58.26 tff(c_279, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.20/58.26 tff(c_297, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 68.20/58.26 tff(c_313, plain, (skf20(skc3, skc2)!=skf10(skc3, skc2))). % 68.20/58.26 tff(c_302, plain, (skf14(skc3, skc2)!=skf12(skc3, skc2))). % 68.20/58.26 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf20(U_91, V_92)!=skf10(U_91, V_92)))). % 68.20/58.26 tff(c_199, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.20/58.26 tff(c_284, plain, (skf16(skc3, skc2)!=skf10(skc3, skc2))). % 68.20/58.26 tff(c_204, plain, (![U_270, V_271]: (singleton(U_270, V_271) | ~entity(U_270, V_271)))). % 68.20/58.26 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf14(U_117, V_118)!=skf12(U_117, V_118)))). % 68.20/58.26 tff(c_167, plain, (![U_238, V_239]: (instrumentality(U_238, V_239) | ~weapon(U_238, V_239)))). % 68.20/58.26 tff(c_193, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 68.20/58.26 tff(c_242, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 68.20/58.26 tff(c_178, plain, (![U_252, V_253]: (singleton(U_252, V_253) | ~eventuality(U_252, V_253)))). % 68.20/58.26 tff(c_247, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 68.20/58.26 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf16(U_109, V_110)!=skf10(U_109, V_110)))). % 68.20/58.26 tff(c_255, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 68.20/58.27 tff(c_256, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 68.20/58.27 tff(c_211, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.20/58.27 tff(c_146, plain, (![U_210]: (shot(skc2, U_210) | ~member(skc2, U_210, skc3)))). % 68.20/58.27 tff(c_222, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.20/58.27 tff(c_230, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 68.20/58.27 tff(c_235, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 68.20/58.27 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 68.20/58.27 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 68.20/58.27 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 68.20/58.27 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 68.20/58.27 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 68.20/58.27 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 68.20/58.27 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 68.20/58.27 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 68.20/58.27 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 68.20/58.27 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 68.20/58.27 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 68.20/58.27 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 68.20/58.27 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 68.20/58.27 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 68.20/58.27 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 68.20/58.27 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 68.20/58.27 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 68.20/58.27 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 68.20/58.27 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 68.20/58.27 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 68.20/58.27 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 68.20/58.27 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 68.20/58.27 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 68.20/58.27 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 68.20/58.27 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 68.20/58.27 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 68.20/58.27 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 68.20/58.27 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 68.20/58.27 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 68.20/58.27 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 68.20/58.27 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 68.20/58.27 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 68.20/58.27 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 68.20/58.27 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 68.20/58.27 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 68.20/58.27 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 68.20/58.27 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 68.20/58.27 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 68.20/58.27 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 68.20/58.27 tff(c_142, plain, (six(skc2, skc3))). % 68.20/58.27 tff(c_144, plain, (group(skc2, skc3))). % 68.20/58.27 tff(c_140, plain, (actual_world(skc2))). % 68.20/58.27 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 68.20/58.27 %------------------------------------------------------------------------------