%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP072-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 : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:07 PM UTC 2025 % Result : Satisfiable 69.09s 59.36s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP072-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:22:34 EDT 2025 % 0.13/0.34 % CPUTime : % 69.09/59.36 % 69.09/59.36 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 69.09/59.36 % 69.09/59.36 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 69.09/59.37 %$ 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 % 69.09/59.37 % 69.09/59.37 %Foreground sorts: % 69.09/59.37 % 69.09/59.37 % 69.09/59.37 %Background operators: % 69.09/59.37 % 69.09/59.37 % 69.09/59.37 %Foreground operators: % 69.09/59.37 tff(nonliving, type, nonliving: ($i * $i) > $o). % 69.09/59.37 tff(skf10, type, skf10: ($i * $i) > $i). % 69.09/59.37 tff(member, type, member: ($i * $i * $i) > $o). % 69.09/59.37 tff(skf8, type, skf8: ($i * $i * $i) > $i). % 69.09/59.37 tff(living, type, living: ($i * $i) > $o). % 69.09/59.37 tff(fire, type, fire: ($i * $i) > $o). % 69.09/59.37 tff(human_person, type, human_person: ($i * $i) > $o). % 69.09/59.37 tff(action, type, action: ($i * $i) > $o). % 69.09/59.37 tff(present, type, present: ($i * $i) > $o). % 69.09/59.37 tff(shot, type, shot: ($i * $i) > $o). % 69.09/59.37 tff(entity, type, entity: ($i * $i) > $o). % 69.09/59.37 tff(eventuality, type, eventuality: ($i * $i) > $o). % 69.09/59.37 tff(weapon, type, weapon: ($i * $i) > $o). % 69.09/59.37 tff(existent, type, existent: ($i * $i) > $o). % 69.09/59.37 tff(singleton, type, singleton: ($i * $i) > $o). % 69.09/59.37 tff(male, type, male: ($i * $i) > $o). % 69.09/59.37 tff(multiple, type, multiple: ($i * $i) > $o). % 69.09/59.37 tff(organism, type, organism: ($i * $i) > $o). % 69.09/59.37 tff(animate, type, animate: ($i * $i) > $o). % 69.09/59.37 tff(of, type, of: ($i * $i * $i) > $o). % 69.09/59.37 tff(skf14, type, skf14: ($i * $i) > $i). % 69.09/59.37 tff(actual_world, type, actual_world: $i > $o). % 69.09/59.37 tff(agent, type, agent: ($i * $i * $i) > $o). % 69.09/59.37 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 69.09/59.37 tff(group, type, group: ($i * $i) > $o). % 69.09/59.37 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 69.09/59.37 tff(artifact, type, artifact: ($i * $i) > $o). % 69.09/59.37 tff(cannon, type, cannon: ($i * $i) > $o). % 69.09/59.37 tff(event, type, event: ($i * $i) > $o). % 69.09/59.37 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 69.09/59.37 tff(patient, type, patient: ($i * $i * $i) > $o). % 69.09/59.37 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 69.09/59.37 tff(skc4, type, skc4: $i). % 69.09/59.37 tff(skc3, type, skc3: $i). % 69.09/59.37 tff(thing, type, thing: ($i * $i) > $o). % 69.09/59.37 tff(human, type, human: ($i * $i) > $o). % 69.09/59.37 tff(six, type, six: ($i * $i) > $o). % 69.09/59.37 tff(skf18, type, skf18: ($i * $i) > $i). % 69.09/59.37 tff(man, type, man: ($i * $i) > $o). % 69.09/59.37 tff(skc5, type, skc5: $i). % 69.09/59.37 tff(weaponry, type, weaponry: ($i * $i) > $o). % 69.09/59.37 tff(unisex, type, unisex: ($i * $i) > $o). % 69.09/59.37 tff(skf16, type, skf16: ($i * $i) > $i). % 69.09/59.37 tff(set, type, set: ($i * $i) > $o). % 69.09/59.37 tff(skf12, type, skf12: ($i * $i) > $i). % 69.09/59.37 tff(impartial, type, impartial: ($i * $i) > $o). % 69.09/59.37 tff(object, type, object: ($i * $i) > $o). % 69.09/59.37 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 69.09/59.37 tff(specific, type, specific: ($i * $i) > $o). % 69.09/59.37 tff(skf20, type, skf20: ($i * $i) > $i). % 69.09/59.37 tff(act, type, act: ($i * $i) > $o). % 69.09/59.37 % 69.09/59.37 %Saturated clause set: % 69.09/59.38 tff(c_1085, plain, (![X1_955, X_963, X_952, X1_977, Z_194, V_199, V_973, X2_196, X1_978, Z_965, X_980, Y_987, X1_956, Y_974, X1_949, X2_953, V_972, X2_957, W_192, Z_979, W_954, X1_195, Y_983, Z_971, V_976, X2_981, X_988, X2_958, X_975, X_197, Y_198, X_986, Z_967, Z_985, V_960, U_193, X2_951, Y_961, Y_950, V_964, Y_982, V_959, Z_984, X1_969, X2_962]: (skf21(V_976, X_986, Y_987, Z_984, X1_978, X2_962, W_192, U_193)=skf21(V_973, X_975, Y_950, Z_985, X1_955, X2_981, W_192, U_193) | skf21(V_976, X_986, Y_987, Z_984, X1_978, X2_962, W_192, U_193)=skf21(V_960, X_980, Y_961, Z_979, X1_977, X2_958, W_192, U_193) | skf21(V_973, X_975, Y_950, Z_985, X1_955, X2_981, W_192, U_193)=skf21(V_960, X_980, Y_961, Z_979, X1_977, X2_958, W_192, U_193) | skf21(V_964, X_952, Y_983, Z_971, X1_949, X2_957, W_192, U_193)=skf21(V_960, X_980, Y_961, Z_979, X1_977, X2_958, W_192, U_193) | skf21(V_976, X_986, Y_987, Z_984, X1_978, X2_962, W_192, U_193)=skf21(V_964, X_952, Y_983, Z_971, X1_949, X2_957, W_192, U_193) | skf21(V_973, X_975, Y_950, Z_985, X1_955, X2_981, W_192, U_193)=skf21(V_964, X_952, Y_983, Z_971, X1_949, X2_957, W_192, U_193) | skf21(V_972, X_988, Y_974, Z_965, X1_956, X2_951, W_192, U_193)=skf21(V_964, X_952, Y_983, Z_971, X1_949, X2_957, W_192, U_193) | skf21(V_972, X_988, Y_974, Z_965, X1_956, X2_951, W_192, U_193)=skf21(V_960, X_980, Y_961, Z_979, X1_977, X2_958, W_192, U_193) | skf21(V_976, X_986, Y_987, Z_984, X1_978, X2_962, W_192, U_193)=skf21(V_972, X_988, Y_974, Z_965, X1_956, X2_951, W_192, U_193) | skf21(V_973, X_975, Y_950, Z_985, X1_955, X2_981, W_192, U_193)=skf21(V_972, X_988, Y_974, Z_965, X1_956, X2_951, W_192, U_193) | skf21(V_972, X_988, Y_974, Z_965, X1_956, X2_951, 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_952, Y_983, Z_971, X1_949, X2_957, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_960, X_980, Y_961, Z_979, X1_977, X2_958, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_976, X_986, Y_987, Z_984, X1_978, X2_962, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_973, X_975, Y_950, Z_985, X1_955, X2_981, 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_959, W_954, X_963, Y_982, Z_967, X1_969, X2_953)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_981=X1_955 | Z_985=X1_955 | Z_985=X2_981 | Z_985=Y_950 | Y_950=X1_955 | Y_950=X2_981 | Y_950=X_975 | Z_985=X_975 | X_975=X1_955 | X_975=X2_981 | X_975=V_973 | Y_950=V_973 | Z_985=V_973 | X1_955=V_973 | X2_981=V_973 | ~member(U_193, X2_981, W_192) | ~member(U_193, X1_955, W_192) | ~member(U_193, Z_985, W_192) | ~member(U_193, Y_950, W_192) | ~member(U_193, X_975, W_192) | ~member(U_193, V_973, W_192) | X2_962=X1_978 | Z_984=X1_978 | Z_984=X2_962 | Z_984=Y_987 | Y_987=X1_978 | Y_987=X2_962 | Y_987=X_986 | Z_984=X_986 | X_986=X1_978 | X_986=X2_962 | X_986=V_976 | Y_987=V_976 | Z_984=V_976 | X1_978=V_976 | X2_962=V_976 | ~member(U_193, X2_962, W_192) | ~member(U_193, X1_978, W_192) | ~member(U_193, Z_984, W_192) | ~member(U_193, Y_987, W_192) | ~member(U_193, X_986, W_192) | ~member(U_193, V_976, W_192) | X2_958=X1_977 | Z_979=X1_977 | Z_979=X2_958 | Z_979=Y_961 | Y_961=X1_977 | Y_961=X2_958 | Y_961=X_980 | Z_979=X_980 | X_980=X1_977 | X_980=X2_958 | X_980=V_960 | Y_961=V_960 | Z_979=V_960 | X1_977=V_960 | X2_958=V_960 | ~member(U_193, X2_958, W_192) | ~member(U_193, X1_977, W_192) | ~member(U_193, Z_979, W_192) | ~member(U_193, Y_961, W_192) | ~member(U_193, X_980, W_192) | ~member(U_193, V_960, W_192) | X2_957=X1_949 | Z_971=X1_949 | Z_971=X2_957 | Z_971=Y_983 | Y_983=X1_949 | Y_983=X2_957 | Y_983=X_952 | Z_971=X_952 | X_952=X1_949 | X_952=X2_957 | X_952=V_964 | Y_983=V_964 | Z_971=V_964 | X1_949=V_964 | X2_957=V_964 | ~member(U_193, X2_957, W_192) | ~member(U_193, X1_949, W_192) | ~member(U_193, Z_971, W_192) | ~member(U_193, Y_983, W_192) | ~member(U_193, X_952, W_192) | ~member(U_193, V_964, W_192) | X2_951=X1_956 | Z_965=X1_956 | Z_965=X2_951 | Z_965=Y_974 | Y_974=X1_956 | Y_974=X2_951 | Y_974=X_988 | Z_965=X_988 | X_988=X1_956 | X_988=X2_951 | X_988=V_972 | Y_974=V_972 | Z_965=V_972 | X1_956=V_972 | X2_951=V_972 | ~member(U_193, X2_951, W_192) | ~member(U_193, X1_956, W_192) | ~member(U_193, Z_965, W_192) | ~member(U_193, Y_974, W_192) | ~member(U_193, X_988, W_192) | ~member(U_193, V_972, 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)))). % 69.09/59.38 tff(c_1062, plain, (![X2_911, X_890, W_909, X_888, Z_194, V_199, X_915, X_887, X2_196, X2_910, X2_885, Y_884, Z_914, X1_889, Z_896, V_901, V_886, V_897, X1_883, W_192, X1_913, X1_195, X1_902, Z_908, U_912, V_891, Y_892, Z_882, Y_904, X_197, Y_198, X_907, U_193, X1_895, Y_893, Y_903, Z_899, X2_894, X2_905]: (skf21(V_897, X_907, Y_904, Z_908, X1_902, X2_894, W_192, U_193)=skf21(V_886, X_890, Y_892, Z_882, X1_883, X2_910, W_192, U_193) | skf21(V_897, X_907, Y_904, Z_908, X1_902, X2_894, W_192, U_193)=skf21(V_891, X_887, Y_893, Z_914, X1_895, X2_911, W_192, U_193) | skf21(V_891, X_887, Y_893, Z_914, X1_895, X2_911, W_192, U_193)=skf21(V_886, X_890, Y_892, Z_882, X1_883, X2_910, W_192, U_193) | skf21(V_901, X_915, Y_903, Z_896, X1_889, X2_885, W_192, U_193)=skf21(V_891, X_887, Y_893, Z_914, X1_895, X2_911, W_192, U_193) | skf21(V_901, X_915, Y_903, Z_896, X1_889, X2_885, W_192, U_193)=skf21(V_897, X_907, Y_904, Z_908, X1_902, X2_894, W_192, U_193) | skf21(V_901, X_915, Y_903, Z_896, X1_889, X2_885, W_192, U_193)=skf21(V_886, X_890, Y_892, Z_882, X1_883, X2_910, W_192, U_193) | skf21(V_901, X_915, Y_903, Z_896, X1_889, X2_885, 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_887, Y_893, Z_914, X1_895, X2_911, 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_907, Y_904, Z_908, X1_902, 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_886, X_890, Y_892, Z_882, X1_883, X2_910, 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_912 | skf21(V_901, X_915, Y_903, Z_896, X1_889, X2_885, W_192, U_193)=U_912 | skf21(V_891, X_887, Y_893, Z_914, X1_895, X2_911, W_192, U_193)=U_912 | skf21(V_897, X_907, Y_904, Z_908, X1_902, X2_894, W_192, U_193)=U_912 | skf21(V_886, X_890, Y_892, Z_882, X1_883, X2_910, W_192, U_193)=U_912 | ~member(U_193, U_912, W_192) | skf21(U_912, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_909, X_888, Y_884, Z_899, X1_913, X2_905)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_910=X1_883 | Z_882=X1_883 | Z_882=X2_910 | Z_882=Y_892 | Y_892=X1_883 | Y_892=X2_910 | Y_892=X_890 | Z_882=X_890 | X_890=X1_883 | X_890=X2_910 | X_890=V_886 | Y_892=V_886 | Z_882=V_886 | X1_883=V_886 | X2_910=V_886 | ~member(U_193, X2_910, W_192) | ~member(U_193, X1_883, W_192) | ~member(U_193, Z_882, W_192) | ~member(U_193, Y_892, W_192) | ~member(U_193, X_890, W_192) | ~member(U_193, V_886, W_192) | X2_894=X1_902 | Z_908=X1_902 | Z_908=X2_894 | Z_908=Y_904 | Y_904=X1_902 | Y_904=X2_894 | Y_904=X_907 | Z_908=X_907 | X_907=X1_902 | X_907=X2_894 | X_907=V_897 | Y_904=V_897 | Z_908=V_897 | X1_902=V_897 | X2_894=V_897 | ~member(U_193, X2_894, W_192) | ~member(U_193, X1_902, W_192) | ~member(U_193, Z_908, W_192) | ~member(U_193, Y_904, W_192) | ~member(U_193, X_907, W_192) | ~member(U_193, V_897, W_192) | X2_911=X1_895 | Z_914=X1_895 | Z_914=X2_911 | Z_914=Y_893 | Y_893=X1_895 | Y_893=X2_911 | Y_893=X_887 | Z_914=X_887 | X_887=X1_895 | X_887=X2_911 | X_887=V_891 | Y_893=V_891 | Z_914=V_891 | X1_895=V_891 | X2_911=V_891 | ~member(U_193, X2_911, W_192) | ~member(U_193, X1_895, W_192) | ~member(U_193, Z_914, W_192) | ~member(U_193, Y_893, W_192) | ~member(U_193, X_887, W_192) | ~member(U_193, V_891, W_192) | X2_885=X1_889 | Z_896=X1_889 | Z_896=X2_885 | Z_896=Y_903 | Y_903=X1_889 | Y_903=X2_885 | Y_903=X_915 | Z_896=X_915 | X_915=X1_889 | X_915=X2_885 | X_915=V_901 | Y_903=V_901 | Z_896=V_901 | X1_889=V_901 | X2_885=V_901 | ~member(U_193, X2_885, W_192) | ~member(U_193, X1_889, W_192) | ~member(U_193, Z_896, W_192) | ~member(U_193, Y_903, W_192) | ~member(U_193, X_915, W_192) | ~member(U_193, V_901, 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)))). % 69.09/59.38 tff(c_1040, plain, (![X2_858, Z_865, Y_862, X_876, Z_194, V_199, Y_852, X1_853, Y_875, V_873, X2_196, X1_855, Y_880, X_864, Z_879, X2_859, X2_848, V_857, X2_867, X1_856, V_878, Y_863, W_192, X1_872, X_860, X1_861, X1_195, X_849, V_847, Z_871, X_197, Y_198, Z_866, W_851, U_193, Z_850, X2_854, X_881, V_870, U_874]: (skf21(V_873, X_864, Y_852, Z_871, X1_861, X2_854, W_192, U_193)=skf21(V_847, X_849, Y_863, Z_850, X1_872, X2_867, W_192, U_193) | skf21(V_873, X_864, Y_852, Z_871, X1_861, X2_854, W_192, U_193)=skf21(V_857, X_876, Y_880, Z_866, X1_856, X2_859, W_192, U_193) | skf21(V_857, X_876, Y_880, Z_866, X1_856, X2_859, W_192, U_193)=skf21(V_847, X_849, Y_863, Z_850, X1_872, X2_867, W_192, U_193) | skf21(V_870, X_881, Y_875, Z_865, X1_853, X2_848, W_192, U_193)=skf21(V_857, X_876, Y_880, Z_866, X1_856, X2_859, W_192, U_193) | skf21(V_873, X_864, Y_852, Z_871, X1_861, X2_854, W_192, U_193)=skf21(V_870, X_881, Y_875, Z_865, X1_853, X2_848, W_192, U_193) | skf21(V_870, X_881, Y_875, Z_865, X1_853, X2_848, W_192, U_193)=skf21(V_847, X_849, Y_863, Z_850, X1_872, X2_867, W_192, U_193) | skf21(V_870, X_881, Y_875, Z_865, X1_853, X2_848, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_857, X_876, Y_880, Z_866, X1_856, X2_859, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_873, X_864, Y_852, Z_871, X1_861, X2_854, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_847, X_849, Y_863, Z_850, X1_872, X2_867, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_874 | skf21(V_870, X_881, Y_875, Z_865, X1_853, X2_848, W_192, U_193)=U_874 | skf21(V_857, X_876, Y_880, Z_866, X1_856, X2_859, W_192, U_193)=U_874 | skf21(V_873, X_864, Y_852, Z_871, X1_861, X2_854, W_192, U_193)=U_874 | skf21(V_847, X_849, Y_863, Z_850, X1_872, X2_867, W_192, U_193)=U_874 | ~member(U_193, U_874, W_192) | skf21(U_874, V_878, W_851, X_860, Y_862, Z_879, X1_855, X2_858)!=U_874 | X2_867=X1_872 | Z_850=X1_872 | Z_850=X2_867 | Z_850=Y_863 | Y_863=X1_872 | Y_863=X2_867 | Y_863=X_849 | Z_850=X_849 | X_849=X1_872 | X_849=X2_867 | X_849=V_847 | Y_863=V_847 | Z_850=V_847 | X1_872=V_847 | X2_867=V_847 | ~member(U_193, X2_867, W_192) | ~member(U_193, X1_872, W_192) | ~member(U_193, Z_850, W_192) | ~member(U_193, Y_863, W_192) | ~member(U_193, X_849, W_192) | ~member(U_193, V_847, W_192) | X2_854=X1_861 | Z_871=X1_861 | Z_871=X2_854 | Z_871=Y_852 | Y_852=X1_861 | Y_852=X2_854 | Y_852=X_864 | Z_871=X_864 | X_864=X1_861 | X_864=X2_854 | X_864=V_873 | Y_852=V_873 | Z_871=V_873 | X1_861=V_873 | X2_854=V_873 | ~member(U_193, X2_854, W_192) | ~member(U_193, X1_861, W_192) | ~member(U_193, Z_871, W_192) | ~member(U_193, Y_852, W_192) | ~member(U_193, X_864, W_192) | ~member(U_193, V_873, W_192) | X2_859=X1_856 | Z_866=X1_856 | Z_866=X2_859 | Z_866=Y_880 | Y_880=X1_856 | Y_880=X2_859 | Y_880=X_876 | Z_866=X_876 | X_876=X1_856 | X_876=X2_859 | X_876=V_857 | Y_880=V_857 | Z_866=V_857 | X1_856=V_857 | X2_859=V_857 | ~member(U_193, X2_859, W_192) | ~member(U_193, X1_856, W_192) | ~member(U_193, Z_866, W_192) | ~member(U_193, Y_880, W_192) | ~member(U_193, X_876, W_192) | ~member(U_193, V_857, W_192) | X2_848=X1_853 | Z_865=X1_853 | Z_865=X2_848 | Z_865=Y_875 | Y_875=X1_853 | Y_875=X2_848 | Y_875=X_881 | Z_865=X_881 | X_881=X1_853 | X_881=X2_848 | X_881=V_870 | Y_875=V_870 | Z_865=V_870 | X1_853=V_870 | X2_848=V_870 | ~member(U_193, X2_848, W_192) | ~member(U_193, X1_853, W_192) | ~member(U_193, Z_865, W_192) | ~member(U_193, Y_875, W_192) | ~member(U_193, X_881, W_192) | ~member(U_193, V_870, 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)))). % 69.09/59.38 tff(c_1017, plain, (![X_792, U_809, X1_814, Z_804, Z_194, V_199, X1_810, Y_799, Y_813, X2_196, V_808, X_819, Z_805, Z_816, X1_800, X2_812, W_192, X2_797, X1_195, X_817, V_815, V_818, Y_811, X2_793, Z_803, X2_794, X_197, Y_198, Y_795, X1_796, V_802, U_193, X_798]: (skf21(V_815, X_817, Y_795, Z_816, X1_800, X2_812, W_192, U_193)=skf21(V_802, X_792, Y_799, Z_805, X1_810, X2_793, W_192, U_193) | skf21(V_808, X_819, Y_811, Z_804, X1_796, X2_794, W_192, U_193)=skf21(V_802, X_792, Y_799, Z_805, X1_810, X2_793, W_192, U_193) | skf21(V_815, X_817, Y_795, Z_816, X1_800, X2_812, W_192, U_193)=skf21(V_808, X_819, Y_811, Z_804, X1_796, X2_794, W_192, U_193) | skf21(V_808, X_819, Y_811, Z_804, X1_796, X2_794, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_802, X_792, Y_799, Z_805, X1_810, X2_793, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_815, X_817, Y_795, Z_816, X1_800, X2_812, 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_818 | skf21(V_808, X_819, Y_811, Z_804, X1_796, X2_794, W_192, U_193)=V_818 | skf21(V_802, X_792, Y_799, Z_805, X1_810, X2_793, W_192, U_193)=V_818 | skf21(V_815, X_817, Y_795, Z_816, X1_800, X2_812, W_192, U_193)=V_818 | V_818=U_809 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_809 | skf21(V_808, X_819, Y_811, Z_804, X1_796, X2_794, W_192, U_193)=U_809 | skf21(V_802, X_792, Y_799, Z_805, X1_810, X2_793, W_192, U_193)=U_809 | skf21(V_815, X_817, Y_795, Z_816, X1_800, X2_812, W_192, U_193)=U_809 | ~member(U_193, V_818, W_192) | ~member(U_193, U_809, W_192) | skf21(U_809, V_818, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_798, Y_813, Z_803, X1_814, X2_797)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_812=X1_800 | Z_816=X1_800 | Z_816=X2_812 | Z_816=Y_795 | Y_795=X1_800 | Y_795=X2_812 | Y_795=X_817 | Z_816=X_817 | X_817=X1_800 | X_817=X2_812 | X_817=V_815 | Y_795=V_815 | Z_816=V_815 | X1_800=V_815 | X2_812=V_815 | ~member(U_193, X2_812, W_192) | ~member(U_193, X1_800, W_192) | ~member(U_193, Z_816, W_192) | ~member(U_193, Y_795, W_192) | ~member(U_193, X_817, W_192) | ~member(U_193, V_815, W_192) | X2_793=X1_810 | Z_805=X1_810 | Z_805=X2_793 | Z_805=Y_799 | Y_799=X1_810 | Y_799=X2_793 | Y_799=X_792 | Z_805=X_792 | X_792=X1_810 | X_792=X2_793 | X_792=V_802 | Y_799=V_802 | Z_805=V_802 | X1_810=V_802 | X2_793=V_802 | ~member(U_193, X2_793, W_192) | ~member(U_193, X1_810, W_192) | ~member(U_193, Z_805, W_192) | ~member(U_193, Y_799, W_192) | ~member(U_193, X_792, W_192) | ~member(U_193, V_802, W_192) | X2_794=X1_796 | Z_804=X1_796 | Z_804=X2_794 | Z_804=Y_811 | Y_811=X1_796 | Y_811=X2_794 | Y_811=X_819 | Z_804=X_819 | X_819=X1_796 | X_819=X2_794 | X_819=V_808 | Y_811=V_808 | Z_804=V_808 | X1_796=V_808 | X2_794=V_808 | ~member(U_193, X2_794, W_192) | ~member(U_193, X1_796, W_192) | ~member(U_193, Z_804, W_192) | ~member(U_193, Y_811, W_192) | ~member(U_193, X_819, W_192) | ~member(U_193, V_808, 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)))). % 69.09/59.38 tff(c_973, plain, (![X1_756, X_761, Z_194, V_199, U_741, V_758, X2_735, Y_759, X2_196, Z_745, W_752, X1_743, X1_754, Y_753, Y_750, Z_736, V_755, W_192, V_733, Y_739, X2_744, X1_195, X_738, V_749, X1_737, X_197, Y_198, X2_742, X_757, U_193, X_751, Z_760, Z_746, X2_734]: (skf21(V_755, X_738, Y_753, Z_745, X1_756, X2_735, W_192, U_193)=skf21(V_733, X_757, Y_739, Z_760, X1_754, X2_744, W_192, U_193) | skf21(V_755, X_738, Y_753, Z_745, X1_756, X2_735, W_192, U_193)=skf21(V_749, X_761, Y_750, Z_746, X1_737, X2_734, W_192, U_193) | skf21(V_749, X_761, Y_750, Z_746, X1_737, X2_734, W_192, U_193)=skf21(V_733, X_757, Y_739, Z_760, X1_754, X2_744, W_192, U_193) | skf21(V_749, X_761, Y_750, Z_746, X1_737, X2_734, 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_738, Y_753, Z_745, X1_756, X2_735, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_733, X_757, Y_739, Z_760, X1_754, X2_744, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_758 | skf21(V_749, X_761, Y_750, Z_746, X1_737, X2_734, W_192, U_193)=V_758 | skf21(V_755, X_738, Y_753, Z_745, X1_756, X2_735, W_192, U_193)=V_758 | skf21(V_733, X_757, Y_739, Z_760, X1_754, X2_744, W_192, U_193)=V_758 | V_758=U_741 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_741 | skf21(V_749, X_761, Y_750, Z_746, X1_737, X2_734, W_192, U_193)=U_741 | skf21(V_755, X_738, Y_753, Z_745, X1_756, X2_735, W_192, U_193)=U_741 | skf21(V_733, X_757, Y_739, Z_760, X1_754, X2_744, W_192, U_193)=U_741 | ~member(U_193, V_758, W_192) | ~member(U_193, U_741, W_192) | skf21(U_741, V_758, W_752, X_751, Y_759, Z_736, X1_743, X2_742)!=V_758 | X2_744=X1_754 | Z_760=X1_754 | Z_760=X2_744 | Z_760=Y_739 | Y_739=X1_754 | Y_739=X2_744 | Y_739=X_757 | Z_760=X_757 | X_757=X1_754 | X_757=X2_744 | X_757=V_733 | Y_739=V_733 | Z_760=V_733 | X1_754=V_733 | X2_744=V_733 | ~member(U_193, X2_744, W_192) | ~member(U_193, X1_754, W_192) | ~member(U_193, Z_760, W_192) | ~member(U_193, Y_739, W_192) | ~member(U_193, X_757, W_192) | ~member(U_193, V_733, W_192) | X2_735=X1_756 | Z_745=X1_756 | Z_745=X2_735 | Z_745=Y_753 | Y_753=X1_756 | Y_753=X2_735 | Y_753=X_738 | Z_745=X_738 | X_738=X1_756 | X_738=X2_735 | X_738=V_755 | Y_753=V_755 | Z_745=V_755 | X1_756=V_755 | X2_735=V_755 | ~member(U_193, X2_735, W_192) | ~member(U_193, X1_756, W_192) | ~member(U_193, Z_745, W_192) | ~member(U_193, Y_753, W_192) | ~member(U_193, X_738, W_192) | ~member(U_193, V_755, W_192) | X2_734=X1_737 | Z_746=X1_737 | Z_746=X2_734 | Z_746=Y_750 | Y_750=X1_737 | Y_750=X2_734 | Y_750=X_761 | Z_746=X_761 | X_761=X1_737 | X_761=X2_734 | X_761=V_749 | Y_750=V_749 | Z_746=V_749 | X1_737=V_749 | X2_734=V_749 | ~member(U_193, X2_734, W_192) | ~member(U_193, X1_737, W_192) | ~member(U_193, Z_746, W_192) | ~member(U_193, Y_750, W_192) | ~member(U_193, X_761, W_192) | ~member(U_193, V_749, 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)))). % 69.09/59.38 tff(c_995, plain, (![X1_775, X_772, U_785, X5_773, Y_777, Z_194, V_770, V_199, X2_196, Y_769, V_774, Z_787, X1_766, X_778, X2_788, W_192, X1_195, V_782, X_791, Z_779, X_197, Y_198, X2_764, X2_783, X1_789, X1_763, U_193, X2_767, Z_771, W_776, Y_762, Y_784, V_786, X_790, Z_765]: (skf21(V_786, X_772, Y_769, Z_765, X1_775, X2_783, W_192, U_193)=skf21(V_774, X_778, Y_762, Z_771, X1_789, X2_788, W_192, U_193) | skf21(V_786, X_772, Y_769, Z_765, X1_775, X2_783, W_192, U_193)=skf21(V_782, X_791, Y_784, Z_779, X1_766, X2_764, W_192, U_193) | skf21(V_782, X_791, Y_784, Z_779, X1_766, X2_764, W_192, U_193)=skf21(V_774, X_778, Y_762, Z_771, X1_789, X2_788, W_192, U_193) | skf21(V_782, X_791, Y_784, Z_779, X1_766, X2_764, 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_772, Y_769, Z_765, X1_775, X2_783, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_774, X_778, Y_762, Z_771, X1_789, X2_788, 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_773 | skf21(V_782, X_791, Y_784, Z_779, X1_766, X2_764, W_192, U_193)=X5_773 | skf21(V_786, X_772, Y_769, Z_765, X1_775, X2_783, W_192, U_193)=X5_773 | skf21(V_774, X_778, Y_762, Z_771, X1_789, X2_788, W_192, U_193)=X5_773 | X5_773=U_785 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_785 | skf21(V_782, X_791, Y_784, Z_779, X1_766, X2_764, W_192, U_193)=U_785 | skf21(V_786, X_772, Y_769, Z_765, X1_775, X2_783, W_192, U_193)=U_785 | skf21(V_774, X_778, Y_762, Z_771, X1_789, X2_788, W_192, U_193)=U_785 | ~member(U_193, X5_773, W_192) | ~member(U_193, U_785, W_192) | skf21(U_785, V_770, W_776, X_790, Y_777, Z_787, X1_763, X2_767)!=U_785 | X2_788=X1_789 | Z_771=X1_789 | Z_771=X2_788 | Z_771=Y_762 | Y_762=X1_789 | Y_762=X2_788 | Y_762=X_778 | Z_771=X_778 | X_778=X1_789 | X_778=X2_788 | X_778=V_774 | Y_762=V_774 | Z_771=V_774 | X1_789=V_774 | X2_788=V_774 | ~member(U_193, X2_788, W_192) | ~member(U_193, X1_789, W_192) | ~member(U_193, Z_771, W_192) | ~member(U_193, Y_762, W_192) | ~member(U_193, X_778, W_192) | ~member(U_193, V_774, W_192) | X2_783=X1_775 | Z_765=X1_775 | Z_765=X2_783 | Z_765=Y_769 | Y_769=X1_775 | Y_769=X2_783 | Y_769=X_772 | Z_765=X_772 | X_772=X1_775 | X_772=X2_783 | X_772=V_786 | Y_769=V_786 | Z_765=V_786 | X1_775=V_786 | X2_783=V_786 | ~member(U_193, X2_783, W_192) | ~member(U_193, X1_775, W_192) | ~member(U_193, Z_765, W_192) | ~member(U_193, Y_769, W_192) | ~member(U_193, X_772, W_192) | ~member(U_193, V_786, W_192) | X2_764=X1_766 | Z_779=X1_766 | Z_779=X2_764 | Z_779=Y_784 | Y_784=X1_766 | Y_784=X2_764 | Y_784=X_791 | Z_779=X_791 | X_791=X1_766 | X_791=X2_764 | X_791=V_782 | Y_784=V_782 | Z_779=V_782 | X1_766=V_782 | X2_764=V_782 | ~member(U_193, X2_764, W_192) | ~member(U_193, X1_766, W_192) | ~member(U_193, Z_779, W_192) | ~member(U_193, Y_784, W_192) | ~member(U_193, X_791, W_192) | ~member(U_193, V_782, 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)))). % 69.09/59.38 tff(c_950, plain, (![Z_699, Z_194, V_199, V_703, Y_695, V_697, X2_196, Z_704, U_693, X2_691, Z_707, X_711, W_192, X1_692, X1_195, X1_698, Y_706, X_696, W_690, X_197, Y_198, X2_709, X2_705, U_193, X1_708, Y_700, V_710]: (skf21(V_710, X_696, Y_700, Z_704, X1_708, X2_705, W_192, U_193)=skf21(V_703, X_711, Y_706, Z_699, X1_692, X2_691, W_192, U_193) | skf21(V_703, X_711, Y_706, Z_699, X1_692, X2_691, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_710, X_696, Y_700, Z_704, X1_708, X2_705, 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_690 | skf21(V_703, X_711, Y_706, Z_699, X1_692, X2_691, W_192, U_193)=W_690 | skf21(V_710, X_696, Y_700, Z_704, X1_708, X2_705, W_192, U_193)=W_690 | W_690=V_697 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_697 | skf21(V_703, X_711, Y_706, Z_699, X1_692, X2_691, W_192, U_193)=V_697 | skf21(V_710, X_696, Y_700, Z_704, X1_708, X2_705, W_192, U_193)=V_697 | V_697=U_693 | W_690=U_693 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_693 | skf21(V_703, X_711, Y_706, Z_699, X1_692, X2_691, W_192, U_193)=U_693 | skf21(V_710, X_696, Y_700, Z_704, X1_708, X2_705, W_192, U_193)=U_693 | ~member(U_193, W_690, W_192) | ~member(U_193, V_697, W_192) | ~member(U_193, U_693, W_192) | skf21(U_693, V_697, W_690, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_695, Z_707, X1_698, X2_709)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_705=X1_708 | Z_704=X1_708 | Z_704=X2_705 | Z_704=Y_700 | Y_700=X1_708 | Y_700=X2_705 | Y_700=X_696 | Z_704=X_696 | X_696=X1_708 | X_696=X2_705 | X_696=V_710 | Y_700=V_710 | Z_704=V_710 | X1_708=V_710 | X2_705=V_710 | ~member(U_193, X2_705, W_192) | ~member(U_193, X1_708, W_192) | ~member(U_193, Z_704, W_192) | ~member(U_193, Y_700, W_192) | ~member(U_193, X_696, W_192) | ~member(U_193, V_710, W_192) | X2_691=X1_692 | Z_699=X1_692 | Z_699=X2_691 | Z_699=Y_706 | Y_706=X1_692 | Y_706=X2_691 | Y_706=X_711 | Z_699=X_711 | X_711=X1_692 | X_711=X2_691 | X_711=V_703 | Y_706=V_703 | Z_699=V_703 | X1_692=V_703 | X2_691=V_703 | ~member(U_193, X2_691, W_192) | ~member(U_193, X1_692, W_192) | ~member(U_193, Z_699, W_192) | ~member(U_193, Y_706, W_192) | ~member(U_193, X_711, W_192) | ~member(U_193, V_703, 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)))). % 69.09/59.38 tff(c_906, plain, (![V_656, W_659, Z_194, Y_658, V_199, X_645, X_665, X2_196, Z_647, V_660, Y_663, X2_662, X2_643, Z_651, X1_654, W_192, U_664, X1_646, X1_195, X_661, Y_650, X_197, Y_198, U_193, V_657, X1_649, X2_648, Z_652]: (skf21(V_660, X_661, Y_663, Z_647, X1_654, X2_648, W_192, U_193)=skf21(V_656, X_665, Y_658, Z_652, X1_646, X2_643, W_192, U_193) | skf21(V_656, X_665, Y_658, Z_652, X1_646, 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_660, X_661, Y_663, Z_647, X1_654, X2_648, 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_659 | skf21(V_656, X_665, Y_658, Z_652, X1_646, X2_643, W_192, U_193)=W_659 | skf21(V_660, X_661, Y_663, Z_647, X1_654, X2_648, W_192, U_193)=W_659 | W_659=V_657 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_657 | skf21(V_656, X_665, Y_658, Z_652, X1_646, X2_643, W_192, U_193)=V_657 | skf21(V_660, X_661, Y_663, Z_647, X1_654, X2_648, W_192, U_193)=V_657 | V_657=U_664 | W_659=U_664 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_664 | skf21(V_656, X_665, Y_658, Z_652, X1_646, X2_643, W_192, U_193)=U_664 | skf21(V_660, X_661, Y_663, Z_647, X1_654, X2_648, W_192, U_193)=U_664 | ~member(U_193, W_659, W_192) | ~member(U_193, V_657, W_192) | ~member(U_193, U_664, W_192) | skf21(U_664, V_657, W_659, X_645, Y_650, Z_651, X1_649, X2_662)!=W_659 | X2_648=X1_654 | Z_647=X1_654 | Z_647=X2_648 | Z_647=Y_663 | Y_663=X1_654 | Y_663=X2_648 | Y_663=X_661 | Z_647=X_661 | X_661=X1_654 | X_661=X2_648 | X_661=V_660 | Y_663=V_660 | Z_647=V_660 | X1_654=V_660 | X2_648=V_660 | ~member(U_193, X2_648, W_192) | ~member(U_193, X1_654, W_192) | ~member(U_193, Z_647, W_192) | ~member(U_193, Y_663, W_192) | ~member(U_193, X_661, W_192) | ~member(U_193, V_660, W_192) | X2_643=X1_646 | Z_652=X1_646 | Z_652=X2_643 | Z_652=Y_658 | Y_658=X1_646 | Y_658=X2_643 | Y_658=X_665 | Z_652=X_665 | X_665=X1_646 | X_665=X2_643 | X_665=V_656 | Y_658=V_656 | Z_652=V_656 | X1_646=V_656 | X2_643=V_656 | ~member(U_193, X2_643, W_192) | ~member(U_193, X1_646, W_192) | ~member(U_193, Z_652, W_192) | ~member(U_193, Y_658, W_192) | ~member(U_193, X_665, W_192) | ~member(U_193, V_656, 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)))). % 69.09/59.39 tff(c_884, plain, (![X_641, Y_636, X_639, X5_628, Z_194, X2_627, V_199, V_622, X2_196, V_633, X1_625, Z_629, X2_621, U_635, W_192, X1_195, X6_620, Y_626, X2_619, Z_634, X_197, Y_198, V_624, W_631, X1_623, Y_637, U_193, X1_640, X_642, Z_638]: (skf21(V_633, X_642, Y_637, Z_629, X1_623, X2_621, W_192, U_193)=skf21(V_624, X_641, Y_626, Z_634, X1_640, X2_619, W_192, U_193) | skf21(V_633, X_642, Y_637, Z_629, X1_623, X2_621, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_624, X_641, Y_626, Z_634, X1_640, X2_619, 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_620 | skf21(V_633, X_642, Y_637, Z_629, X1_623, X2_621, W_192, U_193)=X6_620 | skf21(V_624, X_641, Y_626, Z_634, X1_640, X2_619, W_192, U_193)=X6_620 | X6_620=X5_628 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_628 | skf21(V_633, X_642, Y_637, Z_629, X1_623, X2_621, W_192, U_193)=X5_628 | skf21(V_624, X_641, Y_626, Z_634, X1_640, X2_619, W_192, U_193)=X5_628 | X5_628=U_635 | X6_620=U_635 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_635 | skf21(V_633, X_642, Y_637, Z_629, X1_623, X2_621, W_192, U_193)=U_635 | skf21(V_624, X_641, Y_626, Z_634, X1_640, X2_619, W_192, U_193)=U_635 | ~member(U_193, X6_620, W_192) | ~member(U_193, X5_628, W_192) | ~member(U_193, U_635, W_192) | skf21(U_635, V_622, W_631, X_639, Y_636, Z_638, X1_625, X2_627)!=U_635 | X2_619=X1_640 | Z_634=X1_640 | Z_634=X2_619 | Z_634=Y_626 | Y_626=X1_640 | Y_626=X2_619 | Y_626=X_641 | Z_634=X_641 | X_641=X1_640 | X_641=X2_619 | X_641=V_624 | Y_626=V_624 | Z_634=V_624 | X1_640=V_624 | X2_619=V_624 | ~member(U_193, X2_619, W_192) | ~member(U_193, X1_640, W_192) | ~member(U_193, Z_634, W_192) | ~member(U_193, Y_626, W_192) | ~member(U_193, X_641, W_192) | ~member(U_193, V_624, W_192) | X2_621=X1_623 | Z_629=X1_623 | Z_629=X2_621 | Z_629=Y_637 | Y_637=X1_623 | Y_637=X2_621 | Y_637=X_642 | Z_629=X_642 | X_642=X1_623 | X_642=X2_621 | X_642=V_633 | Y_637=V_633 | Z_629=V_633 | X1_623=V_633 | X2_621=V_633 | ~member(U_193, X2_621, W_192) | ~member(U_193, X1_623, W_192) | ~member(U_193, Z_629, W_192) | ~member(U_193, Y_637, W_192) | ~member(U_193, X_642, W_192) | ~member(U_193, V_633, 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)))). % 69.09/59.39 tff(c_928, plain, (![X1_669, X2_667, X2_689, X1_672, Z_194, V_199, X_681, X2_196, X5_670, V_668, V_687, Y_674, X_688, U_676, W_666, X_684, Z_675, W_192, X1_195, Y_671, Z_685, X_197, Y_198, X1_677, U_193, V_680, Z_673, Y_683, X2_682]: (skf21(V_687, X_684, Y_674, Z_685, X1_672, X2_689, W_192, U_193)=skf21(V_680, X_688, Y_683, Z_675, X1_669, X2_667, W_192, U_193) | skf21(V_680, X_688, Y_683, Z_675, X1_669, X2_667, W_192, U_193)=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf21(V_687, X_684, Y_674, Z_685, X1_672, X2_689, 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_670 | skf21(V_680, X_688, Y_683, Z_675, X1_669, X2_667, W_192, U_193)=X5_670 | skf21(V_687, X_684, Y_674, Z_685, X1_672, X2_689, W_192, U_193)=X5_670 | X5_670=V_668 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_668 | skf21(V_680, X_688, Y_683, Z_675, X1_669, X2_667, W_192, U_193)=V_668 | skf21(V_687, X_684, Y_674, Z_685, X1_672, X2_689, W_192, U_193)=V_668 | V_668=U_676 | X5_670=U_676 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_676 | skf21(V_680, X_688, Y_683, Z_675, X1_669, X2_667, W_192, U_193)=U_676 | skf21(V_687, X_684, Y_674, Z_685, X1_672, X2_689, W_192, U_193)=U_676 | ~member(U_193, X5_670, W_192) | ~member(U_193, V_668, W_192) | ~member(U_193, U_676, W_192) | skf21(U_676, V_668, W_666, X_681, Y_671, Z_673, X1_677, X2_682)!=V_668 | X2_689=X1_672 | Z_685=X1_672 | Z_685=X2_689 | Z_685=Y_674 | Y_674=X1_672 | Y_674=X2_689 | Y_674=X_684 | Z_685=X_684 | X_684=X1_672 | X_684=X2_689 | X_684=V_687 | Y_674=V_687 | Z_685=V_687 | X1_672=V_687 | X2_689=V_687 | ~member(U_193, X2_689, W_192) | ~member(U_193, X1_672, W_192) | ~member(U_193, Z_685, W_192) | ~member(U_193, Y_674, W_192) | ~member(U_193, X_684, W_192) | ~member(U_193, V_687, W_192) | X2_667=X1_669 | Z_675=X1_669 | Z_675=X2_667 | Z_675=Y_683 | Y_683=X1_669 | Y_683=X2_667 | Y_683=X_688 | Z_675=X_688 | X_688=X1_669 | X_688=X2_667 | X_688=V_680 | Y_683=V_680 | Z_675=V_680 | X1_669=V_680 | X2_667=V_680 | ~member(U_193, X2_667, W_192) | ~member(U_193, X1_669, W_192) | ~member(U_193, Z_675, W_192) | ~member(U_193, Y_683, W_192) | ~member(U_193, X_688, W_192) | ~member(U_193, V_680, 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)))). % 69.09/59.39 tff(c_773, plain, (![X2_513, Z_528, X1_525, X_516, Z_194, V_199, V_527, X2_196, U_517, X2_522, W_192, X1_195, X_514, Z_526, X1_515, X_197, Y_198, U_193, V_518, Y_521, W_519]: (skf21(V_518, X_514, Y_521, Z_528, X1_515, X2_522, 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_516 | skf21(V_518, X_514, Y_521, Z_528, X1_515, X2_522, W_192, U_193)=X_516 | X_516=W_519 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_519 | skf21(V_518, X_514, Y_521, Z_528, X1_515, X2_522, W_192, U_193)=W_519 | W_519=V_527 | X_516=V_527 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_527 | skf21(V_518, X_514, Y_521, Z_528, X1_515, X2_522, W_192, U_193)=V_527 | V_527=U_517 | W_519=U_517 | X_516=U_517 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_517 | skf21(V_518, X_514, Y_521, Z_528, X1_515, X2_522, W_192, U_193)=U_517 | ~member(U_193, X_516, W_192) | ~member(U_193, W_519, W_192) | ~member(U_193, V_527, W_192) | ~member(U_193, U_517, W_192) | skf21(U_517, V_527, W_519, X_516, skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_526, X1_525, X2_513)!=skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_522=X1_515 | Z_528=X1_515 | Z_528=X2_522 | Z_528=Y_521 | Y_521=X1_515 | Y_521=X2_522 | Y_521=X_514 | Z_528=X_514 | X_514=X1_515 | X_514=X2_522 | X_514=V_518 | Y_521=V_518 | Z_528=V_518 | X1_515=V_518 | X2_522=V_518 | ~member(U_193, X2_522, W_192) | ~member(U_193, X1_515, W_192) | ~member(U_193, Z_528, W_192) | ~member(U_193, Y_521, W_192) | ~member(U_193, X_514, W_192) | ~member(U_193, V_518, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 69.09/59.39 tff(c_795, plain, (![X1_533, X_532, Y_540, Z_194, Z_545, V_199, W_539, X2_196, X2_534, U_535, Y_530, V_536, X2_542, W_192, X_531, X1_195, V_538, X1_537, X_197, Y_198, Z_529, U_193]: (skf21(V_536, X_531, Y_540, Z_545, X1_533, X2_542, 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_532 | skf21(V_536, X_531, Y_540, Z_545, X1_533, X2_542, W_192, U_193)=X_532 | X_532=W_539 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_539 | skf21(V_536, X_531, Y_540, Z_545, X1_533, X2_542, W_192, U_193)=W_539 | W_539=V_538 | X_532=V_538 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_538 | skf21(V_536, X_531, Y_540, Z_545, X1_533, X2_542, W_192, U_193)=V_538 | V_538=U_535 | W_539=U_535 | X_532=U_535 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_535 | skf21(V_536, X_531, Y_540, Z_545, X1_533, X2_542, W_192, U_193)=U_535 | ~member(U_193, X_532, W_192) | ~member(U_193, W_539, W_192) | ~member(U_193, V_538, W_192) | ~member(U_193, U_535, W_192) | skf21(U_535, V_538, W_539, X_532, Y_530, Z_529, X1_537, X2_534)!=X_532 | X2_542=X1_533 | Z_545=X1_533 | Z_545=X2_542 | Z_545=Y_540 | Y_540=X1_533 | Y_540=X2_542 | Y_540=X_531 | Z_545=X_531 | X_531=X1_533 | X_531=X2_542 | X_531=V_536 | Y_540=V_536 | Z_545=V_536 | X1_533=V_536 | X2_542=V_536 | ~member(U_193, X2_542, W_192) | ~member(U_193, X1_533, W_192) | ~member(U_193, Z_545, W_192) | ~member(U_193, Y_540, W_192) | ~member(U_193, X_531, W_192) | ~member(U_193, V_536, 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)))). % 69.09/59.39 tff(c_817, plain, (![X_553, X2_556, Z_557, Z_194, Y_555, V_199, V_552, X2_196, X5_551, X2_546, X6_547, X1_549, Y_563, W_192, X1_195, W_554, X_548, X_197, Y_198, Z_561, V_550, U_193, U_560, X1_564]: (skf21(V_550, X_548, Y_555, Z_561, X1_549, 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)=X6_547 | skf21(V_550, X_548, Y_555, Z_561, X1_549, X2_556, W_192, U_193)=X6_547 | X6_547=X5_551 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_551 | skf21(V_550, X_548, Y_555, Z_561, X1_549, X2_556, W_192, U_193)=X5_551 | X5_551=V_552 | X6_547=V_552 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_552 | skf21(V_550, X_548, Y_555, Z_561, X1_549, X2_556, W_192, U_193)=V_552 | V_552=U_560 | X5_551=U_560 | X6_547=U_560 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_560 | skf21(V_550, X_548, Y_555, Z_561, X1_549, X2_556, W_192, U_193)=U_560 | ~member(U_193, X6_547, W_192) | ~member(U_193, X5_551, W_192) | ~member(U_193, V_552, W_192) | ~member(U_193, U_560, W_192) | skf21(U_560, V_552, W_554, X_553, Y_563, Z_557, X1_564, X2_546)!=V_552 | X2_556=X1_549 | Z_561=X1_549 | Z_561=X2_556 | Z_561=Y_555 | Y_555=X1_549 | Y_555=X2_556 | Y_555=X_548 | Z_561=X_548 | X_548=X1_549 | X_548=X2_556 | X_548=V_550 | Y_555=V_550 | Z_561=V_550 | X1_549=V_550 | X2_556=V_550 | ~member(U_193, X2_556, W_192) | ~member(U_193, X1_549, W_192) | ~member(U_193, Z_561, W_192) | ~member(U_193, Y_555, W_192) | ~member(U_193, X_548, W_192) | ~member(U_193, V_550, 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)))). % 69.09/59.39 tff(c_839, plain, (![X1_568, Z_194, V_199, X1_565, Y_573, W_570, X_579, X2_196, V_578, X5_581, X2_571, W_192, X2_574, X1_195, Z_566, U_572, V_569, X_197, Y_198, X_567, U_193, Y_582, Z_580]: (skf21(V_569, X_567, Y_573, Z_580, X1_568, X2_574, 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_581 | skf21(V_569, X_567, Y_573, Z_580, X1_568, X2_574, W_192, U_193)=X5_581 | X5_581=W_570 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_570 | skf21(V_569, X_567, Y_573, Z_580, X1_568, X2_574, W_192, U_193)=W_570 | W_570=V_578 | X5_581=V_578 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_578 | skf21(V_569, X_567, Y_573, Z_580, X1_568, X2_574, W_192, U_193)=V_578 | V_578=U_572 | W_570=U_572 | X5_581=U_572 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_572 | skf21(V_569, X_567, Y_573, Z_580, X1_568, X2_574, W_192, U_193)=U_572 | ~member(U_193, X5_581, W_192) | ~member(U_193, W_570, W_192) | ~member(U_193, V_578, W_192) | ~member(U_193, U_572, W_192) | skf21(U_572, V_578, W_570, X_579, Y_582, Z_566, X1_565, X2_571)!=W_570 | X2_574=X1_568 | Z_580=X1_568 | Z_580=X2_574 | Z_580=Y_573 | Y_573=X1_568 | Y_573=X2_574 | Y_573=X_567 | Z_580=X_567 | X_567=X1_568 | X_567=X2_574 | X_567=V_569 | Y_573=V_569 | Z_580=V_569 | X1_568=V_569 | X2_574=V_569 | ~member(U_193, X2_574, W_192) | ~member(U_193, X1_568, W_192) | ~member(U_193, Z_580, W_192) | ~member(U_193, Y_573, W_192) | ~member(U_193, X_567, W_192) | ~member(U_193, V_569, 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)))). % 69.09/59.39 tff(c_861, plain, (![Y_594, Z_194, V_199, W_585, Z_593, X2_196, X6_599, X5_601, X2_590, Z_600, X7_583, X_584, W_192, X1_195, V_591, U_602, X_197, Y_198, U_193, X_589, X2_595, X1_586, Y_592, X1_597, V_588]: (skf21(V_588, X_584, Y_592, Z_600, X1_586, X2_595, 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_583 | skf21(V_588, X_584, Y_592, Z_600, X1_586, X2_595, W_192, U_193)=X7_583 | X7_583=X6_599 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_599 | skf21(V_588, X_584, Y_592, Z_600, X1_586, X2_595, W_192, U_193)=X6_599 | X6_599=X5_601 | X7_583=X5_601 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_601 | skf21(V_588, X_584, Y_592, Z_600, X1_586, X2_595, W_192, U_193)=X5_601 | X5_601=U_602 | X6_599=U_602 | X7_583=U_602 | skf21(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_602 | skf21(V_588, X_584, Y_592, Z_600, X1_586, X2_595, W_192, U_193)=U_602 | ~member(U_193, X7_583, W_192) | ~member(U_193, X6_599, W_192) | ~member(U_193, X5_601, W_192) | ~member(U_193, U_602, W_192) | skf21(U_602, V_591, W_585, X_589, Y_594, Z_593, X1_597, X2_590)!=U_602 | X2_595=X1_586 | Z_600=X1_586 | Z_600=X2_595 | Z_600=Y_592 | Y_592=X1_586 | Y_592=X2_595 | Y_592=X_584 | Z_600=X_584 | X_584=X1_586 | X_584=X2_595 | X_584=V_588 | Y_592=V_588 | Z_600=V_588 | X1_586=V_588 | X2_595=V_588 | ~member(U_193, X2_595, W_192) | ~member(U_193, X1_586, W_192) | ~member(U_193, Z_600, W_192) | ~member(U_193, Y_592, W_192) | ~member(U_193, X_584, W_192) | ~member(U_193, V_588, 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)))). % 69.09/59.39 tff(c_752, plain, (![X_206, X1_204, W_200, V_208, X2_505, V_510, X2_205, X1_506, Y_511, X_512, U_202, W_509, Y_207, U_508, Z_507]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=Y_207 | Y_207=X_206 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X_206 | X_206=W_200 | Y_207=W_200 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_202 | ~member(U_508, Y_207, W_509) | ~member(U_508, X_206, W_509) | ~member(U_508, W_200, W_509) | ~member(U_508, V_208, W_509) | ~member(U_508, U_202, W_509) | skf21(U_202, V_208, W_200, X_206, Y_207, skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508), X1_204, X2_205)!=skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508) | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 tff(c_753, plain, (![Z_183, X8_190, X5_177, X1_185, X2_505, V_510, V_189, X_187, Y_188, X1_506, Y_511, U_181, X_512, X2_186, X7_184, X6_178, W_509, W_179, U_508, Z_507]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X8_190 | X8_190=X7_184 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_181 | ~member(U_508, X8_190, W_509) | ~member(U_508, X7_184, W_509) | ~member(U_508, X6_178, W_509) | ~member(U_508, X5_177, W_509) | ~member(U_508, U_181, W_509) | skf21(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 tff(c_751, plain, (![X6_151, X2_158, Y_160, X2_505, V_510, X1_157, X1_506, Y_511, X_159, W_152, X_512, V_161, W_509, U_508, X5_150, Z_155, Z_507, U_154]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X6_151 | X6_151=X5_150 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_154 | ~member(U_508, X6_151, W_509) | ~member(U_508, X5_150, W_509) | ~member(U_508, W_152, W_509) | ~member(U_508, V_161, W_509) | ~member(U_508, U_154, W_509) | skf21(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 tff(c_750, plain, (![X2_171, X6_164, V_174, U_167, Z_168, X2_505, V_510, X1_506, W_165, Y_511, X_512, W_509, X5_163, X1_170, X7_169, U_508, X_172, Y_173, Z_507]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X7_169 | X7_169=X6_164 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_167 | ~member(U_508, X7_169, W_509) | ~member(U_508, X6_164, W_509) | ~member(U_508, X5_163, W_509) | ~member(U_508, V_174, W_509) | ~member(U_508, U_167, W_509) | skf21(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 tff(c_754, plain, (![U_142, W_140, X2_145, X5_138, X2_505, V_510, Y_147, V_148, X1_506, Y_511, X_512, W_509, U_508, Z_143, X1_144, X_146, Z_507]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X5_138 | X_146=X5_138 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X_146 | X_146=W_140 | X5_138=W_140 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_142 | ~member(U_508, X5_138, W_509) | ~member(U_508, X_146, W_509) | ~member(U_508, W_140, W_509) | ~member(U_508, V_148, W_509) | ~member(U_508, U_142, W_509) | skf21(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 tff(c_749, plain, (![U_130, X2_505, V_510, X1_132, X1_506, V_136, Y_511, Y_135, X_512, W_509, W_128, X2_133, U_508, Z_131, X_134, Z_507]: (skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=Y_135 | Y_135=X_134 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=X_134 | X_134=W_128 | Y_135=W_128 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf21(V_510, X_512, Y_511, Z_507, X1_506, X2_505, W_509, U_508)=U_130 | ~member(U_508, Y_135, W_509) | ~member(U_508, X_134, W_509) | ~member(U_508, W_128, W_509) | ~member(U_508, V_136, W_509) | ~member(U_508, U_130, W_509) | skf21(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_505=X1_506 | Z_507=X1_506 | Z_507=X2_505 | Z_507=Y_511 | Y_511=X1_506 | Y_511=X2_505 | Y_511=X_512 | Z_507=X_512 | X_512=X1_506 | X_512=X2_505 | X_512=V_510 | Y_511=V_510 | Z_507=V_510 | X1_506=V_510 | X2_505=V_510 | six(U_508, W_509) | ~member(U_508, X2_505, W_509) | ~member(U_508, X1_506, W_509) | ~member(U_508, Z_507, W_509) | ~member(U_508, Y_511, W_509) | ~member(U_508, X_512, W_509) | ~member(U_508, V_510, W_509)))). % 69.09/59.39 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)))). % 69.09/59.39 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))). % 69.09/59.39 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))). % 69.09/59.39 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))). % 69.09/59.39 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))). % 69.09/59.39 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))). % 69.09/59.39 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))). % 69.09/59.39 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)))). % 69.09/59.39 tff(c_582, plain, (![W_229]: (~man(skc3, W_229)))). % 69.09/59.39 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)))). % 69.09/59.39 tff(c_549, plain, (skf14(skc4, skc3)!=skf10(skc4, skc3))). % 69.09/59.39 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf14(U_115, V_116)!=skf10(U_115, V_116)))). % 69.09/59.39 tff(c_544, plain, (skf18(skc4, skc3)!=skf10(skc4, skc3))). % 69.09/59.39 tff(c_539, plain, (skf14(skc4, skc3)!=skf12(skc4, skc3))). % 69.09/59.39 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf18(U_101, V_102)!=skf10(U_101, V_102)))). % 69.09/59.39 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf14(U_117, V_118)!=skf12(U_117, V_118)))). % 69.09/59.39 tff(c_534, plain, (skf20(skc4, skc3)!=skf10(skc4, skc3))). % 69.09/59.39 tff(c_529, plain, (act(skc3, skf10(skc4, skc3)))). % 69.09/59.39 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf20(U_91, V_92)!=skf10(U_91, V_92)))). % 69.09/59.39 tff(c_525, plain, (act(skc3, skf16(skc4, skc3)))). % 69.09/59.39 tff(c_509, plain, (act(skc3, skf12(skc4, skc3)))). % 69.09/59.39 tff(c_521, plain, (action(skc3, skf10(skc4, skc3)))). % 69.09/59.39 tff(c_505, plain, (action(skc3, skf16(skc4, skc3)))). % 69.09/59.39 tff(c_517, plain, (shot(skc3, skf10(skc4, skc3)))). % 69.09/59.39 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf10(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 69.09/59.39 tff(c_501, plain, (action(skc3, skf12(skc4, skc3)))). % 69.09/59.39 tff(c_497, plain, (shot(skc3, skf16(skc4, skc3)))). % 69.09/59.39 tff(c_489, plain, (shot(skc3, skf12(skc4, skc3)))). % 69.09/59.39 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf16(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 69.09/59.39 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf12(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 69.09/59.39 tff(c_481, plain, (skf16(skc4, skc3)!=skf10(skc4, skc3))). % 69.09/59.39 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf16(U_109, V_110)!=skf10(U_109, V_110)))). % 69.09/59.40 tff(c_454, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.09/59.40 tff(c_475, plain, (skf16(skc4, skc3)!=skf12(skc4, skc3))). % 69.09/59.40 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf16(U_111, V_112)!=skf12(U_111, V_112)))). % 69.09/59.40 tff(c_470, plain, (act(skc3, skf20(skc4, skc3)))). % 69.09/59.40 tff(c_466, plain, (action(skc3, skf20(skc4, skc3)))). % 69.32/59.40 tff(c_462, plain, (shot(skc3, skf20(skc4, skc3)))). % 69.32/59.40 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf20(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 69.32/59.40 tff(c_394, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 69.32/59.40 tff(c_441, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 69.32/59.40 tff(c_449, plain, (~act(skc3, skc4))). % 69.32/59.40 tff(c_445, plain, (~event(skc3, skc4))). % 69.32/59.40 tff(c_436, plain, (~eventuality(skc3, skc4))). % 69.32/59.40 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf18(U_107, V_108)!=skf16(U_107, V_108)))). % 69.32/59.40 tff(c_359, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 69.32/59.40 tff(c_389, plain, (![U_378, V_379]: (artifact(U_378, V_379) | ~cannon(U_378, V_379)))). % 69.32/59.40 tff(c_430, plain, (skf18(skc4, skc3)!=skf12(skc4, skc3))). % 69.32/59.40 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf18(U_103, V_104)!=skf12(U_103, V_104)))). % 69.32/59.40 tff(c_425, plain, (~artifact(skc3, skc4))). % 69.32/59.40 tff(c_421, plain, (~entity(skc3, skc4))). % 69.32/59.40 tff(c_369, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 69.32/59.40 tff(c_354, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 69.32/59.40 tff(c_415, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 69.32/59.40 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf20(U_97, V_98)!=skf16(U_97, V_98)))). % 69.32/59.40 tff(c_410, plain, (act(skc3, skf14(skc4, skc3)))). % 69.32/59.40 tff(c_406, plain, (action(skc3, skf14(skc4, skc3)))). % 69.32/59.40 tff(c_402, plain, (shot(skc3, skf14(skc4, skc3)))). % 69.32/59.40 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf14(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 69.32/59.40 tff(c_374, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 69.32/59.40 tff(c_342, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 69.32/59.40 tff(c_384, plain, (~artifact(skc3, skc5))). % 69.32/59.40 tff(c_264, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.32/59.40 tff(c_379, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 69.32/59.40 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf20(U_95, V_96)!=skf14(U_95, V_96)))). % 69.32/59.40 tff(c_294, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 69.32/59.40 tff(c_270, plain, (![U_330, V_331]: (~multiple(U_330, V_331) | ~entity(U_330, V_331)))). % 69.32/59.40 tff(c_364, plain, (skf20(skc4, skc3)!=skf12(skc4, skc3))). % 69.32/59.40 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf20(U_93, V_94)!=skf12(U_93, V_94)))). % 69.32/59.40 tff(c_305, plain, (![U_346, V_347]: (~multiple(U_346, V_347) | ~eventuality(U_346, V_347)))). % 69.32/59.40 tff(c_336, plain, (![U_354, V_355]: (~living(U_354, V_355) | ~artifact(U_354, V_355)))). % 69.32/59.40 tff(c_337, plain, (![U_354, V_355]: (~animate(U_354, V_355) | ~artifact(U_354, V_355)))). % 69.32/59.40 tff(c_348, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 69.32/59.40 tff(c_328, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 69.32/59.40 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf16(U_113, V_114)!=skf14(U_113, V_114)))). % 69.32/59.40 tff(c_248, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 69.32/59.40 tff(c_179, plain, (![U_263, V_264]: (instrumentality(U_263, V_264) | ~weapon(U_263, V_264)))). % 69.32/59.40 tff(c_212, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.32/59.40 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf20(U_99, V_100)!=skf18(U_99, V_100)))). % 69.32/59.40 tff(c_299, plain, (skf12(skc4, skc3)!=skf10(skc4, skc3))). % 69.32/59.40 tff(c_315, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 69.32/59.40 tff(c_323, plain, (~act(skc3, skc5))). % 69.32/59.40 tff(c_319, plain, (~event(skc3, skc5))). % 69.32/59.40 tff(c_310, plain, (~eventuality(skc3, skc5))). % 69.32/59.40 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf18(U_105, V_106)!=skf14(U_105, V_106)))). % 69.32/59.40 tff(c_226, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 69.32/59.40 tff(c_173, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~eventuality(U_11, V_12)))). % 69.32/59.40 tff(c_200, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.32/59.40 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf12(U_119, V_120)!=skf10(U_119, V_120)))). % 69.32/59.40 tff(c_206, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 69.32/59.40 tff(c_195, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 69.32/59.40 tff(c_288, plain, (act(skc3, skf18(skc4, skc3)))). % 69.32/59.40 tff(c_284, plain, (action(skc3, skf18(skc4, skc3)))). % 69.32/59.40 tff(c_280, plain, (shot(skc3, skf18(skc4, skc3)))). % 69.32/59.40 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf18(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 69.32/59.40 tff(c_253, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 69.32/59.40 tff(c_258, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 69.32/59.40 tff(c_219, plain, (![U_293, V_294]: (singleton(U_293, V_294) | ~entity(U_293, V_294)))). % 69.32/59.40 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 69.32/59.40 tff(c_242, plain, (![U_315, V_316]: (~male(U_315, V_316) | ~object(U_315, V_316)))). % 69.32/59.40 tff(c_237, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.32/59.40 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 69.32/59.40 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 69.32/59.40 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 69.32/59.40 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 69.32/59.40 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 69.32/59.40 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 69.32/59.40 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 69.32/59.40 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 69.32/59.40 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 69.32/59.41 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 69.32/59.41 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 69.32/59.41 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 69.32/59.41 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 69.32/59.41 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 69.32/59.41 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 69.32/59.41 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 69.32/59.41 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 69.32/59.41 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 69.32/59.41 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 69.32/59.41 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 69.32/59.41 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 69.32/59.41 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 69.32/59.41 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 69.32/59.41 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 69.32/59.41 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 69.32/59.41 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 69.32/59.41 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 69.32/59.41 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 69.32/59.41 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 69.32/59.41 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 69.32/59.41 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 69.32/59.41 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 69.32/59.41 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 69.32/59.41 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 69.32/59.41 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 69.32/59.41 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 69.32/59.41 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 69.32/59.41 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 69.32/59.41 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 69.32/59.41 tff(c_146, plain, (six(skc3, skc4))). % 69.32/59.41 tff(c_142, plain, (male(skc3, skc5))). % 69.32/59.41 tff(c_144, plain, (group(skc3, skc4))). % 69.32/59.41 tff(c_140, plain, (actual_world(skc3))). % 69.32/59.41 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 69.32/59.41 %------------------------------------------------------------------------------