%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP073-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n003.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 63.29s 54.07s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP073-1 : TPTP v9.0.0. Released v2.4.0. % 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n003.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:22:48 EDT 2025 % 0.12/0.34 % CPUTime : % 63.29/54.06 % 63.29/54.07 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.29/54.07 % 63.29/54.07 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.29/54.07 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf23 > skf9 > skf22 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc5 > skc4 > skc3 % 63.29/54.07 % 63.29/54.07 %Foreground sorts: % 63.29/54.07 % 63.29/54.07 % 63.29/54.07 %Background operators: % 63.29/54.07 % 63.29/54.07 % 63.29/54.07 %Foreground operators: % 63.29/54.07 tff(nonliving, type, nonliving: ($i * $i) > $o). % 63.29/54.07 tff(skf10, type, skf10: ($i * $i) > $i). % 63.29/54.07 tff(member, type, member: ($i * $i * $i) > $o). % 63.29/54.07 tff(living, type, living: ($i * $i) > $o). % 63.29/54.07 tff(fire, type, fire: ($i * $i) > $o). % 63.29/54.07 tff(human_person, type, human_person: ($i * $i) > $o). % 63.29/54.07 tff(action, type, action: ($i * $i) > $o). % 63.29/54.07 tff(present, type, present: ($i * $i) > $o). % 63.29/54.07 tff(shot, type, shot: ($i * $i) > $o). % 63.29/54.07 tff(skf22, type, skf22: ($i * $i) > $i). % 63.29/54.07 tff(entity, type, entity: ($i * $i) > $o). % 63.29/54.07 tff(eventuality, type, eventuality: ($i * $i) > $o). % 63.29/54.07 tff(weapon, type, weapon: ($i * $i) > $o). % 63.29/54.07 tff(existent, type, existent: ($i * $i) > $o). % 63.29/54.07 tff(singleton, type, singleton: ($i * $i) > $o). % 63.29/54.07 tff(male, type, male: ($i * $i) > $o). % 63.29/54.07 tff(multiple, type, multiple: ($i * $i) > $o). % 63.29/54.07 tff(organism, type, organism: ($i * $i) > $o). % 63.29/54.07 tff(animate, type, animate: ($i * $i) > $o). % 63.29/54.07 tff(of, type, of: ($i * $i * $i) > $o). % 63.29/54.07 tff(skf14, type, skf14: ($i * $i) > $i). % 63.29/54.07 tff(actual_world, type, actual_world: $i > $o). % 63.29/54.07 tff(agent, type, agent: ($i * $i * $i) > $o). % 63.29/54.07 tff(skf9, type, skf9: ($i * $i) > $i). % 63.29/54.07 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 63.29/54.07 tff(group, type, group: ($i * $i) > $o). % 63.29/54.07 tff(artifact, type, artifact: ($i * $i) > $o). % 63.29/54.07 tff(cannon, type, cannon: ($i * $i) > $o). % 63.29/54.07 tff(event, type, event: ($i * $i) > $o). % 63.29/54.07 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 63.29/54.07 tff(patient, type, patient: ($i * $i * $i) > $o). % 63.29/54.07 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 63.29/54.07 tff(skc4, type, skc4: $i). % 63.29/54.07 tff(skc3, type, skc3: $i). % 63.29/54.07 tff(thing, type, thing: ($i * $i) > $o). % 63.29/54.07 tff(human, type, human: ($i * $i) > $o). % 63.29/54.07 tff(six, type, six: ($i * $i) > $o). % 63.29/54.07 tff(skf18, type, skf18: ($i * $i) > $i). % 63.29/54.07 tff(man, type, man: ($i * $i) > $o). % 63.29/54.07 tff(skc5, type, skc5: $i). % 63.29/54.07 tff(weaponry, type, weaponry: ($i * $i) > $o). % 63.29/54.07 tff(unisex, type, unisex: ($i * $i) > $o). % 63.29/54.07 tff(skf16, type, skf16: ($i * $i) > $i). % 63.29/54.07 tff(set, type, set: ($i * $i) > $o). % 63.29/54.07 tff(skf12, type, skf12: ($i * $i) > $i). % 63.29/54.07 tff(impartial, type, impartial: ($i * $i) > $o). % 63.29/54.07 tff(skf23, type, skf23: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 63.29/54.07 tff(object, type, object: ($i * $i) > $o). % 63.29/54.07 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 63.29/54.07 tff(specific, type, specific: ($i * $i) > $o). % 63.29/54.07 tff(skf20, type, skf20: ($i * $i) > $i). % 63.29/54.07 tff(act, type, act: ($i * $i) > $o). % 63.29/54.07 % 63.29/54.07 %Saturated clause set: % 63.29/54.08 tff(c_1089, plain, (![Z_981, X2_948, W_980, X2_955, Z_194, V_199, X1_952, V_956, X_978, Y_985, Z_966, Z_947, X1_963, X2_196, Z_965, X_984, V_950, V_946, X2_975, X2_960, X1_949, X_961, X1_962, Y_967, W_192, Z_979, X_983, X1_195, Z_971, Y_951, V_954, X_197, Y_198, Y_964, X_953, U_193, X1_976, X1_982, X_958, V_970, X2_973, V_959, Y_972, X2_977, Y_957]: (skf23(V_954, X_961, Y_951, Z_981, X1_962, X2_955, W_192, U_193)=skf23(V_950, X_983, Y_985, Z_971, X1_949, X2_973, W_192, U_193) | skf23(V_959, X_953, Y_957, Z_966, X1_982, X2_975, W_192, U_193)=skf23(V_950, X_983, Y_985, Z_971, X1_949, X2_973, W_192, U_193) | skf23(V_959, X_953, Y_957, Z_966, X1_982, X2_975, W_192, U_193)=skf23(V_954, X_961, Y_951, Z_981, X1_962, X2_955, W_192, U_193) | skf23(V_959, X_953, Y_957, Z_966, X1_982, X2_975, W_192, U_193)=skf23(V_956, X_958, Y_967, Z_979, X1_976, X2_960, W_192, U_193) | skf23(V_956, X_958, Y_967, Z_979, X1_976, X2_960, W_192, U_193)=skf23(V_950, X_983, Y_985, Z_971, X1_949, X2_973, W_192, U_193) | skf23(V_956, X_958, Y_967, Z_979, X1_976, X2_960, W_192, U_193)=skf23(V_954, X_961, Y_951, Z_981, X1_962, X2_955, W_192, U_193) | skf23(V_970, X_984, Y_972, Z_965, X1_952, X2_948, W_192, U_193)=skf23(V_956, X_958, Y_967, Z_979, X1_976, X2_960, W_192, U_193) | skf23(V_970, X_984, Y_972, Z_965, X1_952, X2_948, W_192, U_193)=skf23(V_959, X_953, Y_957, Z_966, X1_982, X2_975, W_192, U_193) | skf23(V_970, X_984, Y_972, Z_965, X1_952, X2_948, W_192, U_193)=skf23(V_950, X_983, Y_985, Z_971, X1_949, X2_973, W_192, U_193) | skf23(V_970, X_984, Y_972, Z_965, X1_952, X2_948, W_192, U_193)=skf23(V_954, X_961, Y_951, Z_981, X1_962, X2_955, W_192, U_193) | skf23(V_970, X_984, Y_972, Z_965, X1_952, X2_948, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_956, X_958, Y_967, Z_979, X1_976, X2_960, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_959, X_953, Y_957, Z_966, X1_982, X2_975, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_950, X_983, Y_985, Z_971, X1_949, X2_973, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_954, X_961, Y_951, Z_981, X1_962, X2_955, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), V_946, W_980, X_978, Y_964, Z_947, X1_963, X2_977)!=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_955=X1_962 | Z_981=X1_962 | Z_981=X2_955 | Z_981=Y_951 | Y_951=X1_962 | Y_951=X2_955 | Y_951=X_961 | Z_981=X_961 | X_961=X1_962 | X_961=X2_955 | X_961=V_954 | Y_951=V_954 | Z_981=V_954 | X1_962=V_954 | X2_955=V_954 | ~member(U_193, X2_955, W_192) | ~member(U_193, X1_962, W_192) | ~member(U_193, Z_981, W_192) | ~member(U_193, Y_951, W_192) | ~member(U_193, X_961, W_192) | ~member(U_193, V_954, W_192) | X2_973=X1_949 | Z_971=X1_949 | Z_971=X2_973 | Z_971=Y_985 | Y_985=X1_949 | Y_985=X2_973 | Y_985=X_983 | Z_971=X_983 | X_983=X1_949 | X_983=X2_973 | X_983=V_950 | Y_985=V_950 | Z_971=V_950 | X1_949=V_950 | X2_973=V_950 | ~member(U_193, X2_973, W_192) | ~member(U_193, X1_949, W_192) | ~member(U_193, Z_971, W_192) | ~member(U_193, Y_985, W_192) | ~member(U_193, X_983, W_192) | ~member(U_193, V_950, W_192) | X2_975=X1_982 | Z_966=X1_982 | Z_966=X2_975 | Z_966=Y_957 | Y_957=X1_982 | Y_957=X2_975 | Y_957=X_953 | Z_966=X_953 | X_953=X1_982 | X_953=X2_975 | X_953=V_959 | Y_957=V_959 | Z_966=V_959 | X1_982=V_959 | X2_975=V_959 | ~member(U_193, X2_975, W_192) | ~member(U_193, X1_982, W_192) | ~member(U_193, Z_966, W_192) | ~member(U_193, Y_957, W_192) | ~member(U_193, X_953, W_192) | ~member(U_193, V_959, W_192) | X2_960=X1_976 | Z_979=X1_976 | Z_979=X2_960 | Z_979=Y_967 | Y_967=X1_976 | Y_967=X2_960 | Y_967=X_958 | Z_979=X_958 | X_958=X1_976 | X_958=X2_960 | X_958=V_956 | Y_967=V_956 | Z_979=V_956 | X1_976=V_956 | X2_960=V_956 | ~member(U_193, X2_960, W_192) | ~member(U_193, X1_976, W_192) | ~member(U_193, Z_979, W_192) | ~member(U_193, Y_967, W_192) | ~member(U_193, X_958, W_192) | ~member(U_193, V_956, W_192) | X2_948=X1_952 | Z_965=X1_952 | Z_965=X2_948 | Z_965=Y_972 | Y_972=X1_952 | Y_972=X2_948 | Y_972=X_984 | Z_965=X_984 | X_984=X1_952 | X_984=X2_948 | X_984=V_970 | Y_972=V_970 | Z_965=V_970 | X1_952=V_970 | X2_948=V_970 | ~member(U_193, X2_948, W_192) | ~member(U_193, X1_952, W_192) | ~member(U_193, Z_965, W_192) | ~member(U_193, Y_972, W_192) | ~member(U_193, X_984, W_192) | ~member(U_193, V_970, 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)))). % 63.29/54.08 tff(c_1044, plain, (![X_858, Z_876, Z_865, X2_847, X_877, Y_872, Y_862, Z_194, V_199, Z_854, V_873, U_851, X2_196, X2_874, X1_848, Z_852, X2_870, X1_844, X_850, X2_866, X_859, W_192, X1_861, X1_849, X1_195, W_856, V_868, X_857, X_197, Y_198, Y_845, U_193, X2_875, Y_871, X1_846, V_855, Y_853, V_869, Z_860]: (skf23(V_873, X_850, Y_845, Z_854, X1_848, X2_866, W_192, U_193)=skf23(V_868, X_858, Y_853, Z_865, X1_861, X2_874, W_192, U_193) | skf23(V_868, X_858, Y_853, Z_865, X1_861, X2_874, W_192, U_193)=skf23(V_855, X_857, Y_872, Z_876, X1_846, X2_870, W_192, U_193) | skf23(V_873, X_850, Y_845, Z_854, X1_848, X2_866, W_192, U_193)=skf23(V_855, X_857, Y_872, Z_876, X1_846, X2_870, W_192, U_193) | skf23(V_869, X_877, Y_871, Z_860, X1_849, X2_847, W_192, U_193)=skf23(V_855, X_857, Y_872, Z_876, X1_846, X2_870, W_192, U_193) | skf23(V_869, X_877, Y_871, Z_860, X1_849, X2_847, W_192, U_193)=skf23(V_868, X_858, Y_853, Z_865, X1_861, X2_874, W_192, U_193) | skf23(V_873, X_850, Y_845, Z_854, X1_848, X2_866, W_192, U_193)=skf23(V_869, X_877, Y_871, Z_860, X1_849, X2_847, W_192, U_193) | skf23(V_869, X_877, Y_871, Z_860, X1_849, X2_847, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_855, X_857, Y_872, Z_876, X1_846, X2_870, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_868, X_858, Y_853, Z_865, X1_861, X2_874, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_873, X_850, Y_845, Z_854, X1_848, X2_866, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_851 | skf23(V_869, X_877, Y_871, Z_860, X1_849, X2_847, W_192, U_193)=U_851 | skf23(V_855, X_857, Y_872, Z_876, X1_846, X2_870, W_192, U_193)=U_851 | skf23(V_868, X_858, Y_853, Z_865, X1_861, X2_874, W_192, U_193)=U_851 | skf23(V_873, X_850, Y_845, Z_854, X1_848, X2_866, W_192, U_193)=U_851 | ~member(U_193, U_851, W_192) | skf23(U_851, skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), W_856, X_859, Y_862, Z_852, X1_844, X2_875)!=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_866=X1_848 | Z_854=X1_848 | Z_854=X2_866 | Z_854=Y_845 | Y_845=X1_848 | Y_845=X2_866 | Y_845=X_850 | Z_854=X_850 | X_850=X1_848 | X_850=X2_866 | X_850=V_873 | Y_845=V_873 | Z_854=V_873 | X1_848=V_873 | X2_866=V_873 | ~member(U_193, X2_866, W_192) | ~member(U_193, X1_848, W_192) | ~member(U_193, Z_854, W_192) | ~member(U_193, Y_845, W_192) | ~member(U_193, X_850, W_192) | ~member(U_193, V_873, W_192) | X2_874=X1_861 | Z_865=X1_861 | Z_865=X2_874 | Z_865=Y_853 | Y_853=X1_861 | Y_853=X2_874 | Y_853=X_858 | Z_865=X_858 | X_858=X1_861 | X_858=X2_874 | X_858=V_868 | Y_853=V_868 | Z_865=V_868 | X1_861=V_868 | X2_874=V_868 | ~member(U_193, X2_874, W_192) | ~member(U_193, X1_861, W_192) | ~member(U_193, Z_865, W_192) | ~member(U_193, Y_853, W_192) | ~member(U_193, X_858, W_192) | ~member(U_193, V_868, W_192) | X2_870=X1_846 | Z_876=X1_846 | Z_876=X2_870 | Z_876=Y_872 | Y_872=X1_846 | Y_872=X2_870 | Y_872=X_857 | Z_876=X_857 | X_857=X1_846 | X_857=X2_870 | X_857=V_855 | Y_872=V_855 | Z_876=V_855 | X1_846=V_855 | X2_870=V_855 | ~member(U_193, X2_870, W_192) | ~member(U_193, X1_846, W_192) | ~member(U_193, Z_876, W_192) | ~member(U_193, Y_872, W_192) | ~member(U_193, X_857, W_192) | ~member(U_193, V_855, W_192) | X2_847=X1_849 | Z_860=X1_849 | Z_860=X2_847 | Z_860=Y_871 | Y_871=X1_849 | Y_871=X2_847 | Y_871=X_877 | Z_860=X_877 | X_877=X1_849 | X_877=X2_847 | X_877=V_869 | Y_871=V_869 | Z_860=V_869 | X1_849=V_869 | X2_847=V_869 | ~member(U_193, X2_847, W_192) | ~member(U_193, X1_849, W_192) | ~member(U_193, Z_860, W_192) | ~member(U_193, Y_871, W_192) | ~member(U_193, X_877, W_192) | ~member(U_193, V_869, 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)))). % 63.29/54.09 tff(c_1066, plain, (![X2_882, X1_879, W_909, X_908, Y_883, Z_194, V_199, V_898, X_887, X_900, Y_890, Z_902, X1_881, Z_911, X2_196, V_906, Y_901, Z_885, X1_893, U_904, W_192, X1_195, X2_889, X1_907, Y_888, V_903, V_910, X_197, Y_198, Y_886, Z_894, X2_880, U_193, V_884, X1_891, X_912, X_892, Z_899, X2_878, X2_905]: (skf23(V_906, X_900, Y_888, Z_885, X1_891, X2_880, W_192, U_193)=skf23(V_884, X_892, Y_886, Z_911, X1_893, X2_905, W_192, U_193) | skf23(V_910, X_908, Y_883, Z_902, X1_881, X2_889, W_192, U_193)=skf23(V_906, X_900, Y_888, Z_885, X1_891, X2_880, W_192, U_193) | skf23(V_910, X_908, Y_883, Z_902, X1_881, X2_889, W_192, U_193)=skf23(V_884, X_892, Y_886, Z_911, X1_893, X2_905, W_192, U_193) | skf23(V_910, X_908, Y_883, Z_902, X1_881, X2_889, W_192, U_193)=skf23(V_898, X_912, Y_901, Z_894, X1_879, X2_878, W_192, U_193) | skf23(V_906, X_900, Y_888, Z_885, X1_891, X2_880, W_192, U_193)=skf23(V_898, X_912, Y_901, Z_894, X1_879, X2_878, W_192, U_193) | skf23(V_898, X_912, Y_901, Z_894, X1_879, X2_878, W_192, U_193)=skf23(V_884, X_892, Y_886, Z_911, X1_893, X2_905, W_192, U_193) | skf23(V_898, X_912, Y_901, Z_894, X1_879, X2_878, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_910, X_908, Y_883, Z_902, X1_881, X2_889, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_906, X_900, Y_888, Z_885, X1_891, X2_880, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_884, X_892, Y_886, Z_911, X1_893, X2_905, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_904 | skf23(V_898, X_912, Y_901, Z_894, X1_879, X2_878, W_192, U_193)=U_904 | skf23(V_910, X_908, Y_883, Z_902, X1_881, X2_889, W_192, U_193)=U_904 | skf23(V_906, X_900, Y_888, Z_885, X1_891, X2_880, W_192, U_193)=U_904 | skf23(V_884, X_892, Y_886, Z_911, X1_893, X2_905, W_192, U_193)=U_904 | ~member(U_193, U_904, W_192) | skf23(U_904, V_903, W_909, X_887, Y_890, Z_899, X1_907, X2_882)!=U_904 | X2_905=X1_893 | Z_911=X1_893 | Z_911=X2_905 | Z_911=Y_886 | Y_886=X1_893 | Y_886=X2_905 | Y_886=X_892 | Z_911=X_892 | X_892=X1_893 | X_892=X2_905 | X_892=V_884 | Y_886=V_884 | Z_911=V_884 | X1_893=V_884 | X2_905=V_884 | ~member(U_193, X2_905, W_192) | ~member(U_193, X1_893, W_192) | ~member(U_193, Z_911, W_192) | ~member(U_193, Y_886, W_192) | ~member(U_193, X_892, W_192) | ~member(U_193, V_884, W_192) | X2_880=X1_891 | Z_885=X1_891 | Z_885=X2_880 | Z_885=Y_888 | Y_888=X1_891 | Y_888=X2_880 | Y_888=X_900 | Z_885=X_900 | X_900=X1_891 | X_900=X2_880 | X_900=V_906 | Y_888=V_906 | Z_885=V_906 | X1_891=V_906 | X2_880=V_906 | ~member(U_193, X2_880, W_192) | ~member(U_193, X1_891, W_192) | ~member(U_193, Z_885, W_192) | ~member(U_193, Y_888, W_192) | ~member(U_193, X_900, W_192) | ~member(U_193, V_906, W_192) | X2_889=X1_881 | Z_902=X1_881 | Z_902=X2_889 | Z_902=Y_883 | Y_883=X1_881 | Y_883=X2_889 | Y_883=X_908 | Z_902=X_908 | X_908=X1_881 | X_908=X2_889 | X_908=V_910 | Y_883=V_910 | Z_902=V_910 | X1_881=V_910 | X2_889=V_910 | ~member(U_193, X2_889, W_192) | ~member(U_193, X1_881, W_192) | ~member(U_193, Z_902, W_192) | ~member(U_193, Y_883, W_192) | ~member(U_193, X_908, W_192) | ~member(U_193, V_910, W_192) | X2_878=X1_879 | Z_894=X1_879 | Z_894=X2_878 | Z_894=Y_901 | Y_901=X1_879 | Y_901=X2_878 | Y_901=X_912 | Z_894=X_912 | X_912=X1_879 | X_912=X2_878 | X_912=V_898 | Y_901=V_898 | Z_894=V_898 | X1_879=V_898 | X2_878=V_898 | ~member(U_193, X2_878, W_192) | ~member(U_193, X1_879, W_192) | ~member(U_193, Z_894, W_192) | ~member(U_193, Y_901, W_192) | ~member(U_193, X_912, W_192) | ~member(U_193, V_898, 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)))). % 63.29/54.09 tff(c_1021, plain, (![V_798, U_809, Y_808, X2_791, Z_194, Z_813, X_799, V_199, X2_196, Y_797, Y_810, X2_789, Y_814, X1_815, Z_794, V_795, V_805, X_807, W_192, X1_793, X1_195, X1_812, X2_800, X2_790, Z_803, X_197, Y_198, Z_801, X1_796, U_193, V_806, X_811, X_816]: (skf23(V_805, X_811, Y_814, Z_803, X1_815, X2_789, W_192, U_193)=skf23(V_795, X_799, Y_797, Z_813, X1_812, X2_800, W_192, U_193) | skf23(V_806, X_816, Y_808, Z_801, X1_793, X2_790, W_192, U_193)=skf23(V_805, X_811, Y_814, Z_803, X1_815, X2_789, W_192, U_193) | skf23(V_806, X_816, Y_808, Z_801, X1_793, X2_790, W_192, U_193)=skf23(V_795, X_799, Y_797, Z_813, X1_812, X2_800, W_192, U_193) | skf23(V_806, X_816, Y_808, Z_801, X1_793, X2_790, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_805, X_811, Y_814, Z_803, X1_815, X2_789, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_795, X_799, Y_797, Z_813, X1_812, X2_800, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_798 | skf23(V_806, X_816, Y_808, Z_801, X1_793, X2_790, W_192, U_193)=V_798 | skf23(V_805, X_811, Y_814, Z_803, X1_815, X2_789, W_192, U_193)=V_798 | skf23(V_795, X_799, Y_797, Z_813, X1_812, X2_800, W_192, U_193)=V_798 | V_798=U_809 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_809 | skf23(V_806, X_816, Y_808, Z_801, X1_793, X2_790, W_192, U_193)=U_809 | skf23(V_805, X_811, Y_814, Z_803, X1_815, X2_789, W_192, U_193)=U_809 | skf23(V_795, X_799, Y_797, Z_813, X1_812, X2_800, W_192, U_193)=U_809 | ~member(U_193, V_798, W_192) | ~member(U_193, U_809, W_192) | skf23(U_809, V_798, skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), X_807, Y_810, Z_794, X1_796, X2_791)!=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_800=X1_812 | Z_813=X1_812 | Z_813=X2_800 | Z_813=Y_797 | Y_797=X1_812 | Y_797=X2_800 | Y_797=X_799 | Z_813=X_799 | X_799=X1_812 | X_799=X2_800 | X_799=V_795 | Y_797=V_795 | Z_813=V_795 | X1_812=V_795 | X2_800=V_795 | ~member(U_193, X2_800, W_192) | ~member(U_193, X1_812, W_192) | ~member(U_193, Z_813, W_192) | ~member(U_193, Y_797, W_192) | ~member(U_193, X_799, W_192) | ~member(U_193, V_795, W_192) | X2_789=X1_815 | Z_803=X1_815 | Z_803=X2_789 | Z_803=Y_814 | Y_814=X1_815 | Y_814=X2_789 | Y_814=X_811 | Z_803=X_811 | X_811=X1_815 | X_811=X2_789 | X_811=V_805 | Y_814=V_805 | Z_803=V_805 | X1_815=V_805 | X2_789=V_805 | ~member(U_193, X2_789, W_192) | ~member(U_193, X1_815, W_192) | ~member(U_193, Z_803, W_192) | ~member(U_193, Y_814, W_192) | ~member(U_193, X_811, W_192) | ~member(U_193, V_805, W_192) | X2_790=X1_793 | Z_801=X1_793 | Z_801=X2_790 | Z_801=Y_808 | Y_808=X1_793 | Y_808=X2_790 | Y_808=X_816 | Z_801=X_816 | X_816=X1_793 | X_816=X2_790 | X_816=V_806 | Y_808=V_806 | Z_801=V_806 | X1_793=V_806 | X2_790=V_806 | ~member(U_193, X2_790, W_192) | ~member(U_193, X1_793, W_192) | ~member(U_193, Z_801, W_192) | ~member(U_193, Y_808, W_192) | ~member(U_193, X_816, W_192) | ~member(U_193, V_806, 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)))). % 63.29/54.09 tff(c_999, plain, (![U_760, X_772, V_779, V_780, X1_773, X2_763, X2_787, X_788, Y_777, Z_194, V_199, V_761, X2_196, X5_771, W_785, Z_762, X1_770, X_774, X1_766, V_759, Y_768, X1_769, W_192, X1_195, Z_784, X2_782, X_786, X_197, Y_198, Y_767, X2_764, Z_775, U_193, Y_781, Z_765]: (skf23(V_761, X_772, Y_777, Z_762, X1_769, X2_787, W_192, U_193)=skf23(V_759, X_774, Y_767, Z_784, X1_773, X2_782, W_192, U_193) | skf23(V_779, X_788, Y_781, Z_775, X1_766, X2_763, W_192, U_193)=skf23(V_759, X_774, Y_767, Z_784, X1_773, X2_782, W_192, U_193) | skf23(V_779, X_788, Y_781, Z_775, X1_766, X2_763, W_192, U_193)=skf23(V_761, X_772, Y_777, Z_762, X1_769, X2_787, W_192, U_193) | skf23(V_779, X_788, Y_781, Z_775, X1_766, X2_763, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_759, X_774, Y_767, Z_784, X1_773, X2_782, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_761, X_772, Y_777, Z_762, X1_769, X2_787, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_771 | skf23(V_779, X_788, Y_781, Z_775, X1_766, X2_763, W_192, U_193)=X5_771 | skf23(V_759, X_774, Y_767, Z_784, X1_773, X2_782, W_192, U_193)=X5_771 | skf23(V_761, X_772, Y_777, Z_762, X1_769, X2_787, W_192, U_193)=X5_771 | X5_771=U_760 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_760 | skf23(V_779, X_788, Y_781, Z_775, X1_766, X2_763, W_192, U_193)=U_760 | skf23(V_759, X_774, Y_767, Z_784, X1_773, X2_782, W_192, U_193)=U_760 | skf23(V_761, X_772, Y_777, Z_762, X1_769, X2_787, W_192, U_193)=U_760 | ~member(U_193, X5_771, W_192) | ~member(U_193, U_760, W_192) | skf23(U_760, V_780, W_785, X_786, Y_768, Z_765, X1_770, X2_764)!=U_760 | X2_787=X1_769 | Z_762=X1_769 | Z_762=X2_787 | Z_762=Y_777 | Y_777=X1_769 | Y_777=X2_787 | Y_777=X_772 | Z_762=X_772 | X_772=X1_769 | X_772=X2_787 | X_772=V_761 | Y_777=V_761 | Z_762=V_761 | X1_769=V_761 | X2_787=V_761 | ~member(U_193, X2_787, W_192) | ~member(U_193, X1_769, W_192) | ~member(U_193, Z_762, W_192) | ~member(U_193, Y_777, W_192) | ~member(U_193, X_772, W_192) | ~member(U_193, V_761, W_192) | X2_782=X1_773 | Z_784=X1_773 | Z_784=X2_782 | Z_784=Y_767 | Y_767=X1_773 | Y_767=X2_782 | Y_767=X_774 | Z_784=X_774 | X_774=X1_773 | X_774=X2_782 | X_774=V_759 | Y_767=V_759 | Z_784=V_759 | X1_773=V_759 | X2_782=V_759 | ~member(U_193, X2_782, W_192) | ~member(U_193, X1_773, W_192) | ~member(U_193, Z_784, W_192) | ~member(U_193, Y_767, W_192) | ~member(U_193, X_774, W_192) | ~member(U_193, V_759, W_192) | X2_763=X1_766 | Z_775=X1_766 | Z_775=X2_763 | Z_775=Y_781 | Y_781=X1_766 | Y_781=X2_763 | Y_781=X_788 | Z_775=X_788 | X_788=X1_766 | X_788=X2_763 | X_788=V_779 | Y_781=V_779 | Z_775=V_779 | X1_766=V_779 | X2_763=V_779 | ~member(U_193, X2_763, W_192) | ~member(U_193, X1_766, W_192) | ~member(U_193, Z_775, W_192) | ~member(U_193, Y_781, W_192) | ~member(U_193, X_788, W_192) | ~member(U_193, V_779, W_192) | X2_196=X1_195 | Z_194=X1_195 | Z_194=X2_196 | Z_194=Y_198 | Y_198=X1_195 | Y_198=X2_196 | Y_198=X_197 | Z_194=X_197 | X_197=X1_195 | X_197=X2_196 | X_197=V_199 | Y_198=V_199 | Z_194=V_199 | X1_195=V_199 | X2_196=V_199 | six(U_193, W_192) | ~member(U_193, X2_196, W_192) | ~member(U_193, X1_195, W_192) | ~member(U_193, Z_194, W_192) | ~member(U_193, Y_198, W_192) | ~member(U_193, X_197, W_192) | ~member(U_193, V_199, W_192)))). % 63.29/54.09 tff(c_977, plain, (![X_758, Z_749, V_742, X1_739, X2_730, Z_194, V_199, Y_754, X2_196, U_744, V_745, X1_755, X_741, Y_753, Y_734, Z_736, W_192, X1_733, Z_747, W_735, X1_195, V_751, X2_737, X1_732, X2_738, X_197, Y_198, V_743, Y_756, X_757, X_740, U_193, X2_731, Z_746]: (skf23(V_745, X_757, Y_756, Z_747, X1_733, X2_738, W_192, U_193)=skf23(V_743, X_740, Y_754, Z_736, X1_739, X2_730, W_192, U_193) | skf23(V_751, X_758, Y_753, Z_746, X1_732, X2_731, W_192, U_193)=skf23(V_743, X_740, Y_754, Z_736, X1_739, X2_730, W_192, U_193) | skf23(V_751, X_758, Y_753, Z_746, X1_732, X2_731, W_192, U_193)=skf23(V_745, X_757, Y_756, Z_747, X1_733, X2_738, W_192, U_193) | skf23(V_751, X_758, Y_753, Z_746, X1_732, X2_731, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_743, X_740, Y_754, Z_736, X1_739, X2_730, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_745, X_757, Y_756, Z_747, X1_733, X2_738, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_742 | skf23(V_751, X_758, Y_753, Z_746, X1_732, X2_731, W_192, U_193)=V_742 | skf23(V_743, X_740, Y_754, Z_736, X1_739, X2_730, W_192, U_193)=V_742 | skf23(V_745, X_757, Y_756, Z_747, X1_733, X2_738, W_192, U_193)=V_742 | V_742=U_744 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_744 | skf23(V_751, X_758, Y_753, Z_746, X1_732, X2_731, W_192, U_193)=U_744 | skf23(V_743, X_740, Y_754, Z_736, X1_739, X2_730, W_192, U_193)=U_744 | skf23(V_745, X_757, Y_756, Z_747, X1_733, X2_738, W_192, U_193)=U_744 | ~member(U_193, V_742, W_192) | ~member(U_193, U_744, W_192) | skf23(U_744, V_742, W_735, X_741, Y_734, Z_749, X1_755, X2_737)!=V_742 | X2_738=X1_733 | Z_747=X1_733 | Z_747=X2_738 | Z_747=Y_756 | Y_756=X1_733 | Y_756=X2_738 | Y_756=X_757 | Z_747=X_757 | X_757=X1_733 | X_757=X2_738 | X_757=V_745 | Y_756=V_745 | Z_747=V_745 | X1_733=V_745 | X2_738=V_745 | ~member(U_193, X2_738, W_192) | ~member(U_193, X1_733, W_192) | ~member(U_193, Z_747, W_192) | ~member(U_193, Y_756, W_192) | ~member(U_193, X_757, W_192) | ~member(U_193, V_745, W_192) | X2_730=X1_739 | Z_736=X1_739 | Z_736=X2_730 | Z_736=Y_754 | Y_754=X1_739 | Y_754=X2_730 | Y_754=X_740 | Z_736=X_740 | X_740=X1_739 | X_740=X2_730 | X_740=V_743 | Y_754=V_743 | Z_736=V_743 | X1_739=V_743 | X2_730=V_743 | ~member(U_193, X2_730, W_192) | ~member(U_193, X1_739, W_192) | ~member(U_193, Z_736, W_192) | ~member(U_193, Y_754, W_192) | ~member(U_193, X_740, W_192) | ~member(U_193, V_743, W_192) | X2_731=X1_732 | Z_746=X1_732 | Z_746=X2_731 | Z_746=Y_753 | Y_753=X1_732 | Y_753=X2_731 | Y_753=X_758 | Z_746=X_758 | X_758=X1_732 | X_758=X2_731 | X_758=V_751 | Y_753=V_751 | Z_746=V_751 | X1_732=V_751 | X2_731=V_751 | ~member(U_193, X2_731, W_192) | ~member(U_193, X1_732, W_192) | ~member(U_193, Z_746, W_192) | ~member(U_193, Y_753, W_192) | ~member(U_193, X_758, W_192) | ~member(U_193, V_751, 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)))). % 63.29/54.09 tff(c_910, plain, (![X1_648, X1_641, X2_640, Z_194, V_199, X2_649, X_645, X2_196, Z_647, Z_644, V_652, U_655, Y_638, X1_643, Y_656, W_192, X1_195, X2_646, Z_639, V_658, X_659, X_197, Y_198, W_642, U_193, V_657, Y_654]: (skf23(V_657, X_645, Y_656, Z_639, X1_648, X2_649, W_192, U_193)=skf23(V_652, X_659, Y_654, Z_647, X1_641, X2_640, W_192, U_193) | skf23(V_652, X_659, Y_654, Z_647, X1_641, X2_640, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_657, X_645, Y_656, Z_639, X1_648, X2_649, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_642 | skf23(V_652, X_659, Y_654, Z_647, X1_641, X2_640, W_192, U_193)=W_642 | skf23(V_657, X_645, Y_656, Z_639, X1_648, X2_649, W_192, U_193)=W_642 | W_642=V_658 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_658 | skf23(V_652, X_659, Y_654, Z_647, X1_641, X2_640, W_192, U_193)=V_658 | skf23(V_657, X_645, Y_656, Z_639, X1_648, X2_649, W_192, U_193)=V_658 | V_658=U_655 | W_642=U_655 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_655 | skf23(V_652, X_659, Y_654, Z_647, X1_641, X2_640, W_192, U_193)=U_655 | skf23(V_657, X_645, Y_656, Z_639, X1_648, X2_649, W_192, U_193)=U_655 | ~member(U_193, W_642, W_192) | ~member(U_193, V_658, W_192) | ~member(U_193, U_655, W_192) | skf23(U_655, V_658, W_642, skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Y_638, Z_644, X1_643, X2_646)!=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_649=X1_648 | Z_639=X1_648 | Z_639=X2_649 | Z_639=Y_656 | Y_656=X1_648 | Y_656=X2_649 | Y_656=X_645 | Z_639=X_645 | X_645=X1_648 | X_645=X2_649 | X_645=V_657 | Y_656=V_657 | Z_639=V_657 | X1_648=V_657 | X2_649=V_657 | ~member(U_193, X2_649, W_192) | ~member(U_193, X1_648, W_192) | ~member(U_193, Z_639, W_192) | ~member(U_193, Y_656, W_192) | ~member(U_193, X_645, W_192) | ~member(U_193, V_657, W_192) | X2_640=X1_641 | Z_647=X1_641 | Z_647=X2_640 | Z_647=Y_654 | Y_654=X1_641 | Y_654=X2_640 | Y_654=X_659 | Z_647=X_659 | X_659=X1_641 | X_659=X2_640 | X_659=V_652 | Y_654=V_652 | Z_647=V_652 | X1_641=V_652 | X2_640=V_652 | ~member(U_193, X2_640, W_192) | ~member(U_193, X1_641, W_192) | ~member(U_193, Z_647, W_192) | ~member(U_193, Y_654, W_192) | ~member(U_193, X_659, W_192) | ~member(U_193, V_652, 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)))). % 63.29/54.09 tff(c_888, plain, (![X1_630, V_623, Z_626, X2_616, Z_194, V_199, U_634, X2_617, Y_624, X2_196, Y_635, X_625, X_636, V_618, Z_632, X1_620, V_629, W_621, W_192, X1_195, Y_631, X_637, X_197, Y_198, X1_619, X2_622, U_193, Z_615]: (skf23(V_629, X_637, Y_631, Z_626, X1_620, X2_617, W_192, U_193)=skf23(V_623, X_625, Y_624, Z_632, X1_619, X2_616, W_192, U_193) | skf23(V_629, X_637, Y_631, Z_626, X1_620, X2_617, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_623, X_625, Y_624, Z_632, X1_619, X2_616, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_621 | skf23(V_629, X_637, Y_631, Z_626, X1_620, X2_617, W_192, U_193)=W_621 | skf23(V_623, X_625, Y_624, Z_632, X1_619, X2_616, W_192, U_193)=W_621 | W_621=V_618 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_618 | skf23(V_629, X_637, Y_631, Z_626, X1_620, X2_617, W_192, U_193)=V_618 | skf23(V_623, X_625, Y_624, Z_632, X1_619, X2_616, W_192, U_193)=V_618 | V_618=U_634 | W_621=U_634 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_634 | skf23(V_629, X_637, Y_631, Z_626, X1_620, X2_617, W_192, U_193)=U_634 | skf23(V_623, X_625, Y_624, Z_632, X1_619, X2_616, W_192, U_193)=U_634 | ~member(U_193, W_621, W_192) | ~member(U_193, V_618, W_192) | ~member(U_193, U_634, W_192) | skf23(U_634, V_618, W_621, X_636, Y_635, Z_615, X1_630, X2_622)!=W_621 | X2_616=X1_619 | Z_632=X1_619 | Z_632=X2_616 | Z_632=Y_624 | Y_624=X1_619 | Y_624=X2_616 | Y_624=X_625 | Z_632=X_625 | X_625=X1_619 | X_625=X2_616 | X_625=V_623 | Y_624=V_623 | Z_632=V_623 | X1_619=V_623 | X2_616=V_623 | ~member(U_193, X2_616, W_192) | ~member(U_193, X1_619, W_192) | ~member(U_193, Z_632, W_192) | ~member(U_193, Y_624, W_192) | ~member(U_193, X_625, W_192) | ~member(U_193, V_623, W_192) | X2_617=X1_620 | Z_626=X1_620 | Z_626=X2_617 | Z_626=Y_631 | Y_631=X1_620 | Y_631=X2_617 | Y_631=X_637 | Z_626=X_637 | X_637=X1_620 | X_637=X2_617 | X_637=V_629 | Y_631=V_629 | Z_626=V_629 | X1_620=V_629 | X2_617=V_629 | ~member(U_193, X2_617, W_192) | ~member(U_193, X1_620, W_192) | ~member(U_193, Z_626, W_192) | ~member(U_193, Y_631, W_192) | ~member(U_193, X_637, W_192) | ~member(U_193, V_629, 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)))). % 63.29/54.09 tff(c_954, plain, (![V_689, Z_688, Z_194, V_702, Y_699, V_199, V_697, X2_196, Z_690, X1_686, X6_685, X1_707, X_708, X2_684, X_691, X2_698, W_192, X1_704, X1_195, X2_700, W_706, U_687, Z_692, Y_693, X5_701, X_705, X_197, Y_198, Y_703, U_193]: (skf23(V_702, X_705, Y_703, Z_690, X1_707, X2_698, W_192, U_193)=skf23(V_697, X_708, Y_699, Z_692, X1_686, X2_684, W_192, U_193) | skf23(V_697, X_708, Y_699, Z_692, X1_686, X2_684, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_702, X_705, Y_703, Z_690, X1_707, X2_698, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_685 | skf23(V_697, X_708, Y_699, Z_692, X1_686, X2_684, W_192, U_193)=X6_685 | skf23(V_702, X_705, Y_703, Z_690, X1_707, X2_698, W_192, U_193)=X6_685 | X6_685=X5_701 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_701 | skf23(V_697, X_708, Y_699, Z_692, X1_686, X2_684, W_192, U_193)=X5_701 | skf23(V_702, X_705, Y_703, Z_690, X1_707, X2_698, W_192, U_193)=X5_701 | X5_701=U_687 | X6_685=U_687 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_687 | skf23(V_697, X_708, Y_699, Z_692, X1_686, X2_684, W_192, U_193)=U_687 | skf23(V_702, X_705, Y_703, Z_690, X1_707, X2_698, W_192, U_193)=U_687 | ~member(U_193, X6_685, W_192) | ~member(U_193, X5_701, W_192) | ~member(U_193, U_687, W_192) | skf23(U_687, V_689, W_706, X_691, Y_693, Z_688, X1_704, X2_700)!=U_687 | X2_698=X1_707 | Z_690=X1_707 | Z_690=X2_698 | Z_690=Y_703 | Y_703=X1_707 | Y_703=X2_698 | Y_703=X_705 | Z_690=X_705 | X_705=X1_707 | X_705=X2_698 | X_705=V_702 | Y_703=V_702 | Z_690=V_702 | X1_707=V_702 | X2_698=V_702 | ~member(U_193, X2_698, W_192) | ~member(U_193, X1_707, W_192) | ~member(U_193, Z_690, W_192) | ~member(U_193, Y_703, W_192) | ~member(U_193, X_705, W_192) | ~member(U_193, V_702, W_192) | X2_684=X1_686 | Z_692=X1_686 | Z_692=X2_684 | Z_692=Y_699 | Y_699=X1_686 | Y_699=X2_684 | Y_699=X_708 | Z_692=X_708 | X_708=X1_686 | X_708=X2_684 | X_708=V_697 | Y_699=V_697 | Z_692=V_697 | X1_686=V_697 | X2_684=V_697 | ~member(U_193, X2_684, W_192) | ~member(U_193, X1_686, W_192) | ~member(U_193, Z_692, W_192) | ~member(U_193, Y_699, W_192) | ~member(U_193, X_708, W_192) | ~member(U_193, V_697, 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)))). % 63.29/54.09 tff(c_932, plain, (![Y_677, X2_661, Z_194, V_199, V_675, Z_676, V_679, X2_196, X1_664, X_666, Y_660, X1_670, W_192, X5_663, X1_195, X_667, X1_665, W_678, Z_671, Y_680, V_662, U_672, Z_681, X_197, Y_198, X_683, U_193, X2_668, X2_669]: (skf23(V_675, X_683, Y_677, Z_671, X1_665, X2_661, W_192, U_193)=skf23(V_662, X_667, Y_680, Z_681, X1_664, X2_668, W_192, U_193) | skf23(V_675, X_683, Y_677, Z_671, X1_665, X2_661, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_662, X_667, Y_680, Z_681, X1_664, X2_668, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_663 | skf23(V_675, X_683, Y_677, Z_671, X1_665, X2_661, W_192, U_193)=X5_663 | skf23(V_662, X_667, Y_680, Z_681, X1_664, X2_668, W_192, U_193)=X5_663 | X5_663=V_679 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_679 | skf23(V_675, X_683, Y_677, Z_671, X1_665, X2_661, W_192, U_193)=V_679 | skf23(V_662, X_667, Y_680, Z_681, X1_664, X2_668, W_192, U_193)=V_679 | V_679=U_672 | X5_663=U_672 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_672 | skf23(V_675, X_683, Y_677, Z_671, X1_665, X2_661, W_192, U_193)=U_672 | skf23(V_662, X_667, Y_680, Z_681, X1_664, X2_668, W_192, U_193)=U_672 | ~member(U_193, X5_663, W_192) | ~member(U_193, V_679, W_192) | ~member(U_193, U_672, W_192) | skf23(U_672, V_679, W_678, X_666, Y_660, Z_676, X1_670, X2_669)!=V_679 | X2_668=X1_664 | Z_681=X1_664 | Z_681=X2_668 | Z_681=Y_680 | Y_680=X1_664 | Y_680=X2_668 | Y_680=X_667 | Z_681=X_667 | X_667=X1_664 | X_667=X2_668 | X_667=V_662 | Y_680=V_662 | Z_681=V_662 | X1_664=V_662 | X2_668=V_662 | ~member(U_193, X2_668, W_192) | ~member(U_193, X1_664, W_192) | ~member(U_193, Z_681, W_192) | ~member(U_193, Y_680, W_192) | ~member(U_193, X_667, W_192) | ~member(U_193, V_662, W_192) | X2_661=X1_665 | Z_671=X1_665 | Z_671=X2_661 | Z_671=Y_677 | Y_677=X1_665 | Y_677=X2_661 | Y_677=X_683 | Z_671=X_683 | X_683=X1_665 | X_683=X2_661 | X_683=V_675 | Y_677=V_675 | Z_671=V_675 | X1_665=V_675 | X2_661=V_675 | ~member(U_193, X2_661, W_192) | ~member(U_193, X1_665, W_192) | ~member(U_193, Z_671, W_192) | ~member(U_193, Y_677, W_192) | ~member(U_193, X_683, W_192) | ~member(U_193, V_675, 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)))). % 63.29/54.09 tff(c_843, plain, (![X1_579, Z_194, V_199, X2_566, X2_196, X1_577, V_568, W_192, X2_581, V_580, X1_195, W_572, Y_575, X_197, Y_198, X_567, U_193, X_570, U_571, Z_578, Z_576]: (skf23(V_568, X_567, Y_575, Z_576, X1_579, X2_581, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_570 | skf23(V_568, X_567, Y_575, Z_576, X1_579, X2_581, W_192, U_193)=X_570 | X_570=W_572 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_572 | skf23(V_568, X_567, Y_575, Z_576, X1_579, X2_581, W_192, U_193)=W_572 | W_572=V_580 | X_570=V_580 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_580 | skf23(V_568, X_567, Y_575, Z_576, X1_579, X2_581, W_192, U_193)=V_580 | V_580=U_571 | W_572=U_571 | X_570=U_571 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_571 | skf23(V_568, X_567, Y_575, Z_576, X1_579, X2_581, W_192, U_193)=U_571 | ~member(U_193, X_570, W_192) | ~member(U_193, W_572, W_192) | ~member(U_193, V_580, W_192) | ~member(U_193, U_571, W_192) | skf23(U_571, V_580, W_572, X_570, skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193), Z_578, X1_577, X2_566)!=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | X2_581=X1_579 | Z_576=X1_579 | Z_576=X2_581 | Z_576=Y_575 | Y_575=X1_579 | Y_575=X2_581 | Y_575=X_567 | Z_576=X_567 | X_567=X1_579 | X_567=X2_581 | X_567=V_568 | Y_575=V_568 | Z_576=V_568 | X1_579=V_568 | X2_581=V_568 | ~member(U_193, X2_581, W_192) | ~member(U_193, X1_579, W_192) | ~member(U_193, Z_576, W_192) | ~member(U_193, Y_575, W_192) | ~member(U_193, X_567, W_192) | ~member(U_193, V_568, 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)))). % 63.29/54.09 tff(c_799, plain, (![Z_543, Z_539, X5_547, Y_540, Z_194, V_199, X7_529, X2_196, X2_546, X1_544, X1_541, Y_542, W_532, W_192, X1_195, X_530, V_531, X_536, X2_537, V_538, X_197, Y_198, U_193, U_548, X6_545]: (skf23(V_531, X_530, Y_542, Z_543, X1_544, X2_546, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X7_529 | skf23(V_531, X_530, Y_542, Z_543, X1_544, X2_546, W_192, U_193)=X7_529 | X7_529=X6_545 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_545 | skf23(V_531, X_530, Y_542, Z_543, X1_544, X2_546, W_192, U_193)=X6_545 | X6_545=X5_547 | X7_529=X5_547 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_547 | skf23(V_531, X_530, Y_542, Z_543, X1_544, X2_546, W_192, U_193)=X5_547 | X5_547=U_548 | X6_545=U_548 | X7_529=U_548 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_548 | skf23(V_531, X_530, Y_542, Z_543, X1_544, X2_546, W_192, U_193)=U_548 | ~member(U_193, X7_529, W_192) | ~member(U_193, X6_545, W_192) | ~member(U_193, X5_547, W_192) | ~member(U_193, U_548, W_192) | skf23(U_548, V_538, W_532, X_536, Y_540, Z_539, X1_541, X2_537)!=U_548 | X2_546=X1_544 | Z_543=X1_544 | Z_543=X2_546 | Z_543=Y_542 | Y_542=X1_544 | Y_542=X2_546 | Y_542=X_530 | Z_543=X_530 | X_530=X1_544 | X_530=X2_546 | X_530=V_531 | Y_542=V_531 | Z_543=V_531 | X1_544=V_531 | X2_546=V_531 | ~member(U_193, X2_546, W_192) | ~member(U_193, X1_544, W_192) | ~member(U_193, Z_543, W_192) | ~member(U_193, Y_542, W_192) | ~member(U_193, X_530, W_192) | ~member(U_193, V_531, 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)))). % 63.29/54.09 tff(c_777, plain, (![Z_194, X2_510, Z_522, V_199, V_516, X2_196, X5_515, U_524, X_517, Y_527, Z_520, X1_523, X1_528, X_512, W_192, X1_195, V_513, X2_525, X_197, Y_198, U_193, Y_521, W_519, X6_511]: (skf23(V_513, X_512, Y_521, Z_522, X1_523, X2_525, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X6_511 | skf23(V_513, X_512, Y_521, Z_522, X1_523, X2_525, W_192, U_193)=X6_511 | X6_511=X5_515 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_515 | skf23(V_513, X_512, Y_521, Z_522, X1_523, X2_525, W_192, U_193)=X5_515 | X5_515=V_516 | X6_511=V_516 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_516 | skf23(V_513, X_512, Y_521, Z_522, X1_523, X2_525, W_192, U_193)=V_516 | V_516=U_524 | X5_515=U_524 | X6_511=U_524 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_524 | skf23(V_513, X_512, Y_521, Z_522, X1_523, X2_525, W_192, U_193)=U_524 | ~member(U_193, X6_511, W_192) | ~member(U_193, X5_515, W_192) | ~member(U_193, V_516, W_192) | ~member(U_193, U_524, W_192) | skf23(U_524, V_516, W_519, X_517, Y_527, Z_520, X1_528, X2_510)!=V_516 | X2_525=X1_523 | Z_522=X1_523 | Z_522=X2_525 | Z_522=Y_521 | Y_521=X1_523 | Y_521=X2_525 | Y_521=X_512 | Z_522=X_512 | X_512=X1_523 | X_512=X2_525 | X_512=V_513 | Y_521=V_513 | Z_522=V_513 | X1_523=V_513 | X2_525=V_513 | ~member(U_193, X2_525, W_192) | ~member(U_193, X1_523, W_192) | ~member(U_193, Z_522, W_192) | ~member(U_193, Y_521, W_192) | ~member(U_193, X_512, W_192) | ~member(U_193, V_513, 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)))). % 63.29/54.09 tff(c_821, plain, (![X_553, X1_557, V_559, Y_562, Z_194, X2_555, V_199, X2_196, X2_565, Y_552, X_549, Z_563, W_192, Z_551, X1_195, U_556, X_197, Y_198, V_550, U_193, W_560, X1_564]: (skf23(V_550, X_549, Y_562, Z_563, X1_564, X2_565, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X_553 | skf23(V_550, X_549, Y_562, Z_563, X1_564, X2_565, W_192, U_193)=X_553 | X_553=W_560 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_560 | skf23(V_550, X_549, Y_562, Z_563, X1_564, X2_565, W_192, U_193)=W_560 | W_560=V_559 | X_553=V_559 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_559 | skf23(V_550, X_549, Y_562, Z_563, X1_564, X2_565, W_192, U_193)=V_559 | V_559=U_556 | W_560=U_556 | X_553=U_556 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_556 | skf23(V_550, X_549, Y_562, Z_563, X1_564, X2_565, W_192, U_193)=U_556 | ~member(U_193, X_553, W_192) | ~member(U_193, W_560, W_192) | ~member(U_193, V_559, W_192) | ~member(U_193, U_556, W_192) | skf23(U_556, V_559, W_560, X_553, Y_552, Z_551, X1_557, X2_555)!=X_553 | X2_565=X1_564 | Z_563=X1_564 | Z_563=X2_565 | Z_563=Y_562 | Y_562=X1_564 | Y_562=X2_565 | Y_562=X_549 | Z_563=X_549 | X_549=X1_564 | X_549=X2_565 | X_549=V_550 | Y_562=V_550 | Z_563=V_550 | X1_564=V_550 | X2_565=V_550 | ~member(U_193, X2_565, W_192) | ~member(U_193, X1_564, W_192) | ~member(U_193, Z_563, W_192) | ~member(U_193, Y_562, W_192) | ~member(U_193, X_549, 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)))). % 63.29/54.09 tff(c_865, plain, (![X2_588, V_585, Z_194, V_199, U_590, X_583, Z_593, X2_196, X1_595, X2_598, X1_582, W_192, X5_597, X1_195, W_587, Y_599, X_197, Y_198, X_596, U_193, V_594, Z_584, Y_592]: (skf23(V_585, X_583, Y_592, Z_593, X1_595, X2_598, W_192, U_193)=skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193) | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=X5_597 | skf23(V_585, X_583, Y_592, Z_593, X1_595, X2_598, W_192, U_193)=X5_597 | X5_597=W_587 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=W_587 | skf23(V_585, X_583, Y_592, Z_593, X1_595, X2_598, W_192, U_193)=W_587 | W_587=V_594 | X5_597=V_594 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=V_594 | skf23(V_585, X_583, Y_592, Z_593, X1_595, X2_598, W_192, U_193)=V_594 | V_594=U_590 | W_587=U_590 | X5_597=U_590 | skf23(V_199, X_197, Y_198, Z_194, X1_195, X2_196, W_192, U_193)=U_590 | skf23(V_585, X_583, Y_592, Z_593, X1_595, X2_598, W_192, U_193)=U_590 | ~member(U_193, X5_597, W_192) | ~member(U_193, W_587, W_192) | ~member(U_193, V_594, W_192) | ~member(U_193, U_590, W_192) | skf23(U_590, V_594, W_587, X_596, Y_599, Z_584, X1_582, X2_588)!=W_587 | X2_598=X1_595 | Z_593=X1_595 | Z_593=X2_598 | Z_593=Y_592 | Y_592=X1_595 | Y_592=X2_598 | Y_592=X_583 | Z_593=X_583 | X_583=X1_595 | X_583=X2_598 | X_583=V_585 | Y_592=V_585 | Z_593=V_585 | X1_595=V_585 | X2_598=V_585 | ~member(U_193, X2_598, W_192) | ~member(U_193, X1_595, W_192) | ~member(U_193, Z_593, W_192) | ~member(U_193, Y_592, W_192) | ~member(U_193, X_583, W_192) | ~member(U_193, V_585, 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)))). % 63.29/54.09 tff(c_755, plain, (![X2_502, X1_503, X_206, Y_508, X1_204, W_200, X_509, V_208, W_506, X2_205, U_505, Z_504, U_202, V_507, Y_207]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=Y_207 | Y_207=X_206 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X_206 | X_206=W_200 | Y_207=W_200 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_202 | ~member(U_505, Y_207, W_506) | ~member(U_505, X_206, W_506) | ~member(U_505, W_200, W_506) | ~member(U_505, V_208, W_506) | ~member(U_505, U_202, W_506) | skf23(U_202, V_208, W_200, X_206, Y_207, skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505), X1_204, X2_205)!=skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505) | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 tff(c_756, plain, (![X2_502, X6_151, X1_503, Y_508, X2_158, X_509, W_506, Y_160, X1_157, X_159, W_152, V_161, U_505, Z_504, V_507, X5_150, Z_155, U_154]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X6_151 | X6_151=X5_150 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X5_150 | X5_150=W_152 | X6_151=W_152 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=W_152 | W_152=V_161 | X5_150=V_161 | X6_151=V_161 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=V_161 | V_161=U_154 | W_152=U_154 | X5_150=U_154 | X6_151=U_154 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_154 | ~member(U_505, X6_151, W_506) | ~member(U_505, X5_150, W_506) | ~member(U_505, W_152, W_506) | ~member(U_505, V_161, W_506) | ~member(U_505, U_154, W_506) | skf23(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152 | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 tff(c_754, plain, (![X2_502, U_130, X1_503, Y_508, X_509, W_506, X1_132, V_136, Y_135, U_505, Z_504, W_128, V_507, X2_133, Z_131, X_134]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=Y_135 | Y_135=X_134 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X_134 | X_134=W_128 | Y_135=W_128 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=W_128 | W_128=V_136 | X_134=V_136 | Y_135=V_136 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=V_136 | V_136=U_130 | W_128=U_130 | X_134=U_130 | Y_135=U_130 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_130 | ~member(U_505, Y_135, W_506) | ~member(U_505, X_134, W_506) | ~member(U_505, W_128, W_506) | ~member(U_505, V_136, W_506) | ~member(U_505, U_130, W_506) | skf23(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135 | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 tff(c_757, plain, (![X2_502, X1_503, U_142, Y_508, X_509, W_140, W_506, X2_145, X5_138, Y_147, V_148, U_505, Z_504, V_507, Z_143, X1_144, X_146]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X5_138 | X_146=X5_138 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X_146 | X_146=W_140 | X5_138=W_140 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=W_140 | W_140=V_148 | X_146=V_148 | X5_138=V_148 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=V_148 | V_148=U_142 | W_140=U_142 | X_146=U_142 | X5_138=U_142 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_142 | ~member(U_505, X5_138, W_506) | ~member(U_505, X_146, W_506) | ~member(U_505, W_140, W_506) | ~member(U_505, V_148, W_506) | ~member(U_505, U_142, W_506) | skf23(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146 | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 tff(c_758, plain, (![Z_183, X2_502, X1_503, Y_508, X8_190, X5_177, X_509, W_506, X1_185, V_189, X_187, Y_188, U_181, X2_186, X7_184, X6_178, U_505, Z_504, V_507, W_179]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X8_190 | X8_190=X7_184 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X7_184 | X7_184=X6_178 | X8_190=X6_178 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X6_178 | X6_178=X5_177 | X7_184=X5_177 | X8_190=X5_177 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X5_177 | X5_177=U_181 | X6_178=U_181 | X7_184=U_181 | X8_190=U_181 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_181 | ~member(U_505, X8_190, W_506) | ~member(U_505, X7_184, W_506) | ~member(U_505, X6_178, W_506) | ~member(U_505, X5_177, W_506) | ~member(U_505, U_181, W_506) | skf23(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181 | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 tff(c_753, plain, (![X2_502, X1_503, Y_508, X_509, X2_171, X6_164, W_506, V_174, U_167, Z_168, W_165, U_505, Z_504, X5_163, X1_170, X7_169, V_507, X_172, Y_173]: (skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X7_169 | X7_169=X6_164 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X6_164 | X6_164=X5_163 | X7_169=X5_163 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=X5_163 | X5_163=V_174 | X6_164=V_174 | X7_169=V_174 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=V_174 | V_174=U_167 | X5_163=U_167 | X6_164=U_167 | X7_169=U_167 | skf23(V_507, X_509, Y_508, Z_504, X1_503, X2_502, W_506, U_505)=U_167 | ~member(U_505, X7_169, W_506) | ~member(U_505, X6_164, W_506) | ~member(U_505, X5_163, W_506) | ~member(U_505, V_174, W_506) | ~member(U_505, U_167, W_506) | skf23(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174 | X2_502=X1_503 | Z_504=X1_503 | Z_504=X2_502 | Z_504=Y_508 | Y_508=X1_503 | Y_508=X2_502 | Y_508=X_509 | Z_504=X_509 | X_509=X1_503 | X_509=X2_502 | X_509=V_507 | Y_508=V_507 | Z_504=V_507 | X1_503=V_507 | X2_502=V_507 | six(U_505, W_506) | ~member(U_505, X2_502, W_506) | ~member(U_505, X1_503, W_506) | ~member(U_505, Z_504, W_506) | ~member(U_505, Y_508, W_506) | ~member(U_505, X_509, W_506) | ~member(U_505, V_507, W_506)))). % 63.29/54.09 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, skf23(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)))). % 63.29/54.09 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) | skf23(U_167, V_174, W_165, X_172, Y_173, Z_168, X1_170, X2_171)!=V_174))). % 63.29/54.09 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) | skf23(U_130, V_136, W_128, X_134, Y_135, Z_131, X1_132, X2_133)!=Y_135))). % 63.29/54.09 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) | skf23(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Z_203))). % 63.29/54.09 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) | skf23(U_154, V_161, W_152, X_159, Y_160, Z_155, X1_157, X2_158)!=W_152))). % 63.29/54.10 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) | skf23(U_142, V_148, W_140, X_146, Y_147, Z_143, X1_144, X2_145)!=X_146))). % 63.29/54.10 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) | skf23(U_181, V_189, W_179, X_187, Y_188, Z_183, X1_185, X2_186)!=U_181))). % 63.29/54.10 tff(c_124, plain, (![W_126, U_124, V_125]: (skf22(W_126, U_124)=V_125 | skf20(W_126, U_124)=V_125 | skf18(W_126, U_124)=V_125 | skf16(W_126, U_124)=V_125 | skf14(W_126, U_124)=V_125 | skf12(W_126, U_124)=V_125 | ~six(U_124, W_126) | ~member(U_124, V_125, W_126)))). % 63.29/54.10 tff(c_586, plain, (![V_224]: (~man(skc3, V_224)))). % 63.29/54.10 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)))). % 63.29/54.10 tff(c_521, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 63.29/54.10 tff(c_553, plain, (act(skc3, skf20(skc4, skc3)))). % 63.29/54.10 tff(c_549, plain, (action(skc3, skf20(skc4, skc3)))). % 63.29/54.10 tff(c_545, plain, (shot(skc3, skf20(skc4, skc3)))). % 63.29/54.10 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf20(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 63.29/54.10 tff(c_537, plain, (act(skc3, skf18(skc4, skc3)))). % 63.29/54.10 tff(c_533, plain, (action(skc3, skf18(skc4, skc3)))). % 63.29/54.10 tff(c_529, plain, (shot(skc3, skf18(skc4, skc3)))). % 63.29/54.10 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf18(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 63.29/54.10 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf14(U_111, V_112)))). % 63.29/54.10 tff(c_516, plain, (skf22(skc4, skc3)!=skf16(skc4, skc3))). % 63.29/54.10 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf22(U_95, V_96)!=skf16(U_95, V_96)))). % 63.29/54.10 tff(c_511, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 63.29/54.10 tff(c_498, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 63.29/54.10 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf16(U_117, V_118)!=skf14(U_117, V_118)))). % 63.29/54.10 tff(c_506, plain, (act(skc3, skf14(skc4, skc3)))). % 63.29/54.10 tff(c_502, plain, (action(skc3, skf14(skc4, skc3)))). % 63.29/54.10 tff(c_493, plain, (shot(skc3, skf14(skc4, skc3)))). % 63.29/54.10 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf18(U_107, V_108)))). % 63.29/54.10 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf14(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 63.29/54.10 tff(c_485, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 63.29/54.10 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf16(U_105, V_106)))). % 63.29/54.10 tff(c_458, plain, (![U_258, V_259]: (~act(U_258, V_259) | ~artifact(U_258, V_259)))). % 63.29/54.10 tff(c_479, plain, (skf18(skc4, skc3)!=skf12(skc4, skc3))). % 63.29/54.10 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf18(U_109, V_110)!=skf12(U_109, V_110)))). % 63.29/54.10 tff(c_474, plain, (act(skc3, skf12(skc4, skc3)))). % 63.29/54.10 tff(c_470, plain, (action(skc3, skf12(skc4, skc3)))). % 63.29/54.10 tff(c_466, plain, (shot(skc3, skf12(skc4, skc3)))). % 63.29/54.10 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf12(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 63.29/54.10 tff(c_420, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 63.29/54.10 tff(c_453, plain, (~artifact(skc3, skc4))). % 63.29/54.10 tff(c_449, plain, (~entity(skc3, skc4))). % 63.29/54.10 tff(c_368, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 63.29/54.10 tff(c_444, plain, (skf22(skc4, skc3)!=skf14(skc4, skc3))). % 63.29/54.10 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf22(U_93, V_94)!=skf14(U_93, V_94)))). % 63.29/54.10 tff(c_394, plain, (![U_371, V_372]: (artifact(U_371, V_372) | ~cannon(U_371, V_372)))). % 63.29/54.10 tff(c_438, plain, (skf14(skc4, skc3)!=skf12(skc4, skc3))). % 63.29/54.10 tff(c_433, plain, (~act(skc3, skc4))). % 63.29/54.10 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf14(U_119, V_120)!=skf12(U_119, V_120)))). % 63.29/54.10 tff(c_429, plain, (~event(skc3, skc4))). % 63.29/54.10 tff(c_425, plain, (~eventuality(skc3, skc4))). % 63.29/54.10 tff(c_379, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 63.29/54.10 tff(c_409, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 63.29/54.10 tff(c_415, plain, (skf22(skc4, skc3)!=skf18(skc4, skc3))). % 63.29/54.10 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf22(U_97, V_98)!=skf18(U_97, V_98)))). % 63.29/54.10 tff(c_389, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.29/54.10 tff(c_296, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 63.29/54.10 tff(c_404, plain, (skf16(skc4, skc3)!=skf12(skc4, skc3))). % 63.29/54.10 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf16(U_115, V_116)!=skf12(U_115, V_116)))). % 63.29/54.10 tff(c_399, plain, (~artifact(skc3, skc5))). % 63.29/54.10 tff(c_363, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.29/54.10 tff(c_291, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 63.29/54.10 tff(c_305, plain, (![U_335, V_336]: (~living(U_335, V_336) | ~artifact(U_335, V_336)))). % 63.29/54.10 tff(c_384, plain, (skf22(skc4, skc3)!=skf12(skc4, skc3))). % 63.29/54.10 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf22(U_91, V_92)!=skf12(U_91, V_92)))). % 63.29/54.10 tff(c_334, plain, (![U_345, V_346]: (~multiple(U_345, V_346) | ~eventuality(U_345, V_346)))). % 63.29/54.10 tff(c_306, plain, (![U_335, V_336]: (~animate(U_335, V_336) | ~artifact(U_335, V_336)))). % 63.29/54.10 tff(c_373, plain, (skf20(skc4, skc3)!=skf12(skc4, skc3))). % 63.29/54.10 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf12(U_101, V_102)))). % 63.29/54.10 tff(c_281, plain, (![U_325, V_326]: (~multiple(U_325, V_326) | ~entity(U_325, V_326)))). % 63.29/54.10 tff(c_357, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 63.29/54.10 tff(c_328, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 63.29/54.10 tff(c_256, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 63.29/54.10 tff(c_216, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.29/54.10 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf14(U_103, V_104)))). % 63.29/54.10 tff(c_352, plain, (act(skc3, skf16(skc4, skc3)))). % 63.29/54.10 tff(c_348, plain, (action(skc3, skf16(skc4, skc3)))). % 63.29/54.10 tff(c_344, plain, (shot(skc3, skf16(skc4, skc3)))). % 63.29/54.10 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf16(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 63.29/54.10 tff(c_262, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.29/54.10 tff(c_286, plain, (skf22(skc4, skc3)!=skf20(skc4, skc3))). % 63.29/54.10 tff(c_247, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.29/54.10 tff(c_203, plain, (![U_276, V_277]: (singleton(U_276, V_277) | ~eventuality(U_276, V_277)))). % 63.29/54.10 tff(c_198, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 63.29/54.10 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf16(U_113, V_114)))). % 63.29/54.10 tff(c_323, plain, (act(skc3, skf22(skc4, skc3)))). % 63.29/54.10 tff(c_319, plain, (action(skc3, skf22(skc4, skc3)))). % 63.29/54.10 tff(c_315, plain, (shot(skc3, skf22(skc4, skc3)))). % 63.29/54.10 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf22(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 63.29/54.10 tff(c_178, plain, (![U_258, V_259]: (entity(U_258, V_259) | ~artifact(U_258, V_259)))). % 63.29/54.10 tff(c_228, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.29/54.10 tff(c_242, plain, (![U_312, V_313]: (entity(U_312, V_313) | ~human_person(U_312, V_313)))). % 63.29/54.10 tff(c_222, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 63.29/54.10 tff(c_185, plain, (![U_264, V_265]: (instrumentality(U_264, V_265) | ~weapon(U_264, V_265)))). % 63.29/54.10 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf22(U_99, V_100)!=skf20(U_99, V_100)))). % 63.29/54.10 tff(c_192, plain, (![U_270, V_271]: (singleton(U_270, V_271) | ~entity(U_270, V_271)))). % 63.29/54.10 tff(c_276, plain, (~act(skc3, skc5))). % 63.29/54.10 tff(c_271, plain, (~event(skc3, skc5))). % 63.29/54.10 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 63.29/54.10 tff(c_267, plain, (~eventuality(skc3, skc5))). % 63.29/54.10 tff(c_257, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 63.29/54.10 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 63.29/54.11 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 63.29/54.11 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 63.29/54.11 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 63.29/54.11 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.29/54.11 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 63.29/54.11 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 63.29/54.11 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 63.29/54.11 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 63.29/54.11 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 63.29/54.11 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 63.29/54.11 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 63.29/54.11 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 63.29/54.11 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 63.29/54.11 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 63.29/54.11 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 63.29/54.11 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 63.29/54.11 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 63.29/54.11 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 63.29/54.11 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 63.29/54.11 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 63.29/54.11 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 63.29/54.11 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 63.29/54.11 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 63.29/54.11 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 63.29/54.11 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 63.29/54.11 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 63.29/54.11 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 63.29/54.11 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 63.29/54.11 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 63.29/54.11 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 63.29/54.11 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.29/54.11 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 63.29/54.11 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 63.29/54.11 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 63.29/54.11 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 63.29/54.11 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 63.29/54.11 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 63.29/54.11 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 63.29/54.11 tff(c_144, plain, (group(skc3, skc4))). % 63.29/54.11 tff(c_142, plain, (male(skc3, skc5))). % 63.29/54.11 tff(c_146, plain, (six(skc3, skc4))). % 63.29/54.11 tff(c_140, plain, (actual_world(skc3))). % 63.29/54.11 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.29/54.11 %------------------------------------------------------------------------------