%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP053-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 : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:03 PM UTC 2025 % Result : Satisfiable 17.26s 9.23s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.10 % Problem : NLP053-1 : TPTP v9.0.0. Released v2.4.0. % 0.08/0.11 % 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.11/0.31 % Computer : n008.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.31 % DateTime : Tue Apr 8 08:17:47 EDT 2025 % 0.11/0.31 % CPUTime : % 17.26/9.23 % 17.26/9.23 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.26/9.23 % 17.26/9.23 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.26/9.24 %$ patient > of > member > agent > woman > unisex > thing > substance_matter > specific > singleton > shake_beverage > set > relname > relation > present > possession > past > organism > order > object > nonreflexive > nonliving > nonhuman > nonexistent > multiple > mia_forename > living > impartial > human_person > human > group > general > forename > food > five > female > existent > eventuality > event > entity > dollar > currency > cost > cash > beverage > animate > act > abstraction > actual_world > skf18 > skf9 > skf17 > skf15 > skf13 > skf11 > #nlpp > skf7 > skc9 > skc7 > skc6 > skc12 > skc11 > skc10 % 17.26/9.24 % 17.26/9.24 %Foreground sorts: % 17.26/9.24 % 17.26/9.24 % 17.26/9.24 %Background operators: % 17.26/9.24 % 17.26/9.24 % 17.26/9.24 %Foreground operators: % 17.26/9.24 tff(nonliving, type, nonliving: ($i * $i) > $o). % 17.26/9.24 tff(relation, type, relation: ($i * $i) > $o). % 17.26/9.24 tff(member, type, member: ($i * $i * $i) > $o). % 17.26/9.24 tff(forename, type, forename: ($i * $i) > $o). % 17.26/9.24 tff(skc7, type, skc7: $i). % 17.26/9.24 tff(female, type, female: ($i * $i) > $o). % 17.26/9.24 tff(living, type, living: ($i * $i) > $o). % 17.26/9.24 tff(cost, type, cost: ($i * $i) > $o). % 17.26/9.24 tff(human_person, type, human_person: ($i * $i) > $o). % 17.26/9.24 tff(present, type, present: ($i * $i) > $o). % 17.26/9.24 tff(skc11, type, skc11: $i). % 17.26/9.24 tff(skf18, type, skf18: ($i * $i * $i * $i * $i * $i * $i) > $i). % 17.26/9.24 tff(entity, type, entity: ($i * $i) > $o). % 17.26/9.24 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 17.26/9.24 tff(skc9, type, skc9: $i). % 17.26/9.24 tff(past, type, past: ($i * $i) > $o). % 17.26/9.24 tff(beverage, type, beverage: ($i * $i) > $o). % 17.26/9.24 tff(eventuality, type, eventuality: ($i * $i) > $o). % 17.26/9.24 tff(existent, type, existent: ($i * $i) > $o). % 17.26/9.24 tff(abstraction, type, abstraction: ($i * $i) > $o). % 17.26/9.24 tff(relname, type, relname: ($i * $i) > $o). % 17.26/9.24 tff(possession, type, possession: ($i * $i) > $o). % 17.26/9.24 tff(singleton, type, singleton: ($i * $i) > $o). % 17.26/9.24 tff(multiple, type, multiple: ($i * $i) > $o). % 17.26/9.24 tff(organism, type, organism: ($i * $i) > $o). % 17.26/9.24 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 17.26/9.24 tff(animate, type, animate: ($i * $i) > $o). % 17.26/9.24 tff(of, type, of: ($i * $i * $i) > $o). % 17.26/9.24 tff(actual_world, type, actual_world: $i > $o). % 17.26/9.24 tff(dollar, type, dollar: ($i * $i) > $o). % 17.26/9.24 tff(agent, type, agent: ($i * $i * $i) > $o). % 17.26/9.24 tff(skf9, type, skf9: ($i * $i) > $i). % 17.26/9.24 tff(skf17, type, skf17: ($i * $i) > $i). % 17.26/9.24 tff(group, type, group: ($i * $i) > $o). % 17.26/9.24 tff(five, type, five: ($i * $i) > $o). % 17.26/9.24 tff(general, type, general: ($i * $i) > $o). % 17.26/9.24 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 17.26/9.24 tff(food, type, food: ($i * $i) > $o). % 17.26/9.24 tff(event, type, event: ($i * $i) > $o). % 17.26/9.24 tff(woman, type, woman: ($i * $i) > $o). % 17.26/9.24 tff(currency, type, currency: ($i * $i) > $o). % 17.26/9.24 tff(skf7, type, skf7: $i > $i). % 17.26/9.24 tff(patient, type, patient: ($i * $i * $i) > $o). % 17.26/9.24 tff(skf15, type, skf15: ($i * $i) > $i). % 17.26/9.24 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 17.26/9.24 tff(cash, type, cash: ($i * $i) > $o). % 17.26/9.24 tff(skf11, type, skf11: ($i * $i) > $i). % 17.26/9.24 tff(thing, type, thing: ($i * $i) > $o). % 17.26/9.24 tff(human, type, human: ($i * $i) > $o). % 17.26/9.24 tff(skf13, type, skf13: ($i * $i) > $i). % 17.26/9.24 tff(unisex, type, unisex: ($i * $i) > $o). % 17.26/9.24 tff(set, type, set: ($i * $i) > $o). % 17.26/9.24 tff(skc6, type, skc6: $i). % 17.26/9.24 tff(impartial, type, impartial: ($i * $i) > $o). % 17.26/9.24 tff(object, type, object: ($i * $i) > $o). % 17.26/9.24 tff(skc12, type, skc12: $i). % 17.26/9.24 tff(order, type, order: ($i * $i) > $o). % 17.26/9.24 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 17.26/9.24 tff(specific, type, specific: ($i * $i) > $o). % 17.26/9.24 tff(skc10, type, skc10: $i). % 17.26/9.24 tff(act, type, act: ($i * $i) > $o). % 17.26/9.24 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 17.26/9.24 % 17.26/9.24 %Saturated clause set: % 17.36/9.24 tff(c_1639, plain, (![V_935, V_195, Z_917, V_941, X_931, X1_919, X1_916, X_925, Z_922, U_190, W_189, Z_927, X1_192, W_933, Y_930, V_915, Y_940, Y_928, X1_929, V_920, Y_924, Z_937, X_938, Y_194, V_921, Z_926, X1_914, Z_191, X1_932, X_939, Y_942, X_193, X_923]: (skf18(V_921, X_923, Y_928, Z_927, X1_929, W_189, U_190)=skf18(V_920, X_931, Y_930, Z_922, X1_932, W_189, U_190) | skf18(V_941, X_939, Y_940, Z_917, X1_919, W_189, U_190)=skf18(V_921, X_923, Y_928, Z_927, X1_929, W_189, U_190) | skf18(V_941, X_939, Y_940, Z_917, X1_919, W_189, U_190)=skf18(V_920, X_931, Y_930, Z_922, X1_932, W_189, U_190) | skf18(V_941, X_939, Y_940, Z_917, X1_919, W_189, U_190)=skf18(V_935, X_938, Y_924, Z_926, X1_916, W_189, U_190) | skf18(V_935, X_938, Y_924, Z_926, X1_916, W_189, U_190)=skf18(V_921, X_923, Y_928, Z_927, X1_929, W_189, U_190) | skf18(V_935, X_938, Y_924, Z_926, X1_916, W_189, U_190)=skf18(V_920, X_931, Y_930, Z_922, X1_932, W_189, U_190) | skf18(V_935, X_938, Y_924, Z_926, X1_916, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_941, X_939, Y_940, Z_917, X1_919, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_921, X_923, Y_928, Z_927, X1_929, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_920, X_931, Y_930, Z_922, X1_932, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), V_915, W_933, X_925, Y_942, Z_937, X1_914)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_922=X1_932 | Z_922=Y_930 | Y_930=X1_932 | Y_930=X_931 | Z_922=X_931 | X_931=X1_932 | X_931=V_920 | Y_930=V_920 | Z_922=V_920 | X1_932=V_920 | ~member(U_190, X1_932, W_189) | ~member(U_190, Z_922, W_189) | ~member(U_190, Y_930, W_189) | ~member(U_190, X_931, W_189) | ~member(U_190, V_920, W_189) | Z_927=X1_929 | Z_927=Y_928 | Y_928=X1_929 | Y_928=X_923 | Z_927=X_923 | X_923=X1_929 | X_923=V_921 | Y_928=V_921 | Z_927=V_921 | X1_929=V_921 | ~member(U_190, X1_929, W_189) | ~member(U_190, Z_927, W_189) | ~member(U_190, Y_928, W_189) | ~member(U_190, X_923, W_189) | ~member(U_190, V_921, W_189) | Z_917=X1_919 | Z_917=Y_940 | Y_940=X1_919 | Y_940=X_939 | Z_917=X_939 | X_939=X1_919 | X_939=V_941 | Y_940=V_941 | Z_917=V_941 | X1_919=V_941 | ~member(U_190, X1_919, W_189) | ~member(U_190, Z_917, W_189) | ~member(U_190, Y_940, W_189) | ~member(U_190, X_939, W_189) | ~member(U_190, V_941, W_189) | Z_926=X1_916 | Z_926=Y_924 | Y_924=X1_916 | Y_924=X_938 | Z_926=X_938 | X_938=X1_916 | X_938=V_935 | Y_924=V_935 | Z_926=V_935 | X1_916=V_935 | ~member(U_190, X1_916, W_189) | ~member(U_190, Z_926, W_189) | ~member(U_190, Y_924, W_189) | ~member(U_190, X_938, W_189) | ~member(U_190, V_935, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.24 tff(c_1619, plain, (![Y_878, X_890, Z_880, V_883, X_888, V_195, Y_872, X_873, Y_877, X1_867, V_882, U_190, W_189, Z_886, X1_192, Z_879, X1_871, U_868, W_875, V_889, Z_870, X_869, X1_887, Y_194, X1_876, Z_191, X_193, Y_874]: (skf18(V_889, X_873, Y_878, Z_886, X1_867, W_189, U_190)=skf18(V_882, X_869, Y_874, Z_880, X1_887, W_189, U_190) | skf18(V_889, X_873, Y_878, Z_886, X1_867, W_189, U_190)=skf18(V_883, X_890, Y_877, Z_879, X1_871, W_189, U_190) | skf18(V_883, X_890, Y_877, Z_879, X1_871, W_189, U_190)=skf18(V_882, X_869, Y_874, Z_880, X1_887, W_189, U_190) | skf18(V_883, X_890, Y_877, Z_879, X1_871, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_889, X_873, Y_878, Z_886, X1_867, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_882, X_869, Y_874, Z_880, X1_887, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_868 | skf18(V_883, X_890, Y_877, Z_879, X1_871, W_189, U_190)=U_868 | skf18(V_889, X_873, Y_878, Z_886, X1_867, W_189, U_190)=U_868 | skf18(V_882, X_869, Y_874, Z_880, X1_887, W_189, U_190)=U_868 | ~member(U_190, U_868, W_189) | skf18(U_868, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), W_875, X_888, Y_872, Z_870, X1_876)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_880=X1_887 | Z_880=Y_874 | Y_874=X1_887 | Y_874=X_869 | Z_880=X_869 | X_869=X1_887 | X_869=V_882 | Y_874=V_882 | Z_880=V_882 | X1_887=V_882 | ~member(U_190, X1_887, W_189) | ~member(U_190, Z_880, W_189) | ~member(U_190, Y_874, W_189) | ~member(U_190, X_869, W_189) | ~member(U_190, V_882, W_189) | Z_886=X1_867 | Z_886=Y_878 | Y_878=X1_867 | Y_878=X_873 | Z_886=X_873 | X_873=X1_867 | X_873=V_889 | Y_878=V_889 | Z_886=V_889 | X1_867=V_889 | ~member(U_190, X1_867, W_189) | ~member(U_190, Z_886, W_189) | ~member(U_190, Y_878, W_189) | ~member(U_190, X_873, W_189) | ~member(U_190, V_889, W_189) | Z_879=X1_871 | Z_879=Y_877 | Y_877=X1_871 | Y_877=X_890 | Z_879=X_890 | X_890=X1_871 | X_890=V_883 | Y_877=V_883 | Z_879=V_883 | X1_871=V_883 | ~member(U_190, X1_871, W_189) | ~member(U_190, Z_879, W_189) | ~member(U_190, Y_877, W_189) | ~member(U_190, X_890, W_189) | ~member(U_190, V_883, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1600, plain, (![V_861, X_866, V_195, Z_843, V_848, W_849, X1_847, V_865, Z_864, U_857, X1_844, Y_854, X1_855, U_190, W_189, X_850, X1_192, Y_851, X_860, Z_859, V_845, Z_856, X_846, Y_194, Y_842, Z_191, X_193, X1_852, Y_853]: (skf18(V_865, X_860, Y_842, Z_859, X1_855, W_189, U_190)=skf18(V_848, X_846, Y_853, Z_864, X1_852, W_189, U_190) | skf18(V_865, X_860, Y_842, Z_859, X1_855, W_189, U_190)=skf18(V_861, X_866, Y_854, Z_856, X1_847, W_189, U_190) | skf18(V_861, X_866, Y_854, Z_856, X1_847, W_189, U_190)=skf18(V_848, X_846, Y_853, Z_864, X1_852, W_189, U_190) | skf18(V_861, X_866, Y_854, Z_856, X1_847, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_865, X_860, Y_842, Z_859, X1_855, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_848, X_846, Y_853, Z_864, X1_852, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_857 | skf18(V_861, X_866, Y_854, Z_856, X1_847, W_189, U_190)=U_857 | skf18(V_865, X_860, Y_842, Z_859, X1_855, W_189, U_190)=U_857 | skf18(V_848, X_846, Y_853, Z_864, X1_852, W_189, U_190)=U_857 | ~member(U_190, U_857, W_189) | skf18(U_857, V_845, W_849, X_850, Y_851, Z_843, X1_844)!=U_857 | Z_864=X1_852 | Z_864=Y_853 | Y_853=X1_852 | Y_853=X_846 | Z_864=X_846 | X_846=X1_852 | X_846=V_848 | Y_853=V_848 | Z_864=V_848 | X1_852=V_848 | ~member(U_190, X1_852, W_189) | ~member(U_190, Z_864, W_189) | ~member(U_190, Y_853, W_189) | ~member(U_190, X_846, W_189) | ~member(U_190, V_848, W_189) | Z_859=X1_855 | Z_859=Y_842 | Y_842=X1_855 | Y_842=X_860 | Z_859=X_860 | X_860=X1_855 | X_860=V_865 | Y_842=V_865 | Z_859=V_865 | X1_855=V_865 | ~member(U_190, X1_855, W_189) | ~member(U_190, Z_859, W_189) | ~member(U_190, Y_842, W_189) | ~member(U_190, X_860, W_189) | ~member(U_190, V_865, W_189) | Z_856=X1_847 | Z_856=Y_854 | Y_854=X1_847 | Y_854=X_866 | Z_856=X_866 | X_866=X1_847 | X_866=V_861 | Y_854=V_861 | Z_856=V_861 | X1_847=V_861 | ~member(U_190, X1_847, W_189) | ~member(U_190, Z_856, W_189) | ~member(U_190, Y_854, W_189) | ~member(U_190, X_866, W_189) | ~member(U_190, V_861, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1580, plain, (![X_821, Y_806, V_195, Z_812, X1_820, X_822, X1_807, U_810, X_808, U_190, W_189, X1_192, V_816, Y_817, V_805, Z_819, V_814, Y_811, X1_809, Y_194, Z_823, Z_191, X_193]: (skf18(V_816, X_821, Y_811, Z_812, X1_807, W_189, U_190)=skf18(V_814, X_808, Y_806, Z_823, X1_809, W_189, U_190) | skf18(V_816, X_821, Y_811, Z_812, X1_807, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_814, X_808, Y_806, Z_823, X1_809, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_805 | skf18(V_816, X_821, Y_811, Z_812, X1_807, W_189, U_190)=V_805 | skf18(V_814, X_808, Y_806, Z_823, X1_809, W_189, U_190)=V_805 | V_805=U_810 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_810 | skf18(V_816, X_821, Y_811, Z_812, X1_807, W_189, U_190)=U_810 | skf18(V_814, X_808, Y_806, Z_823, X1_809, W_189, U_190)=U_810 | ~member(U_190, V_805, W_189) | ~member(U_190, U_810, W_189) | skf18(U_810, V_805, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), X_822, Y_817, Z_819, X1_820)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_823=X1_809 | Z_823=Y_806 | Y_806=X1_809 | Y_806=X_808 | Z_823=X_808 | X_808=X1_809 | X_808=V_814 | Y_806=V_814 | Z_823=V_814 | X1_809=V_814 | ~member(U_190, X1_809, W_189) | ~member(U_190, Z_823, W_189) | ~member(U_190, Y_806, W_189) | ~member(U_190, X_808, W_189) | ~member(U_190, V_814, W_189) | Z_812=X1_807 | Z_812=Y_811 | Y_811=X1_807 | Y_811=X_821 | Z_812=X_821 | X_821=X1_807 | X_821=V_816 | Y_811=V_816 | Z_812=V_816 | X1_807=V_816 | ~member(U_190, X1_807, W_189) | ~member(U_190, Z_812, W_189) | ~member(U_190, Y_811, W_189) | ~member(U_190, X_821, W_189) | ~member(U_190, V_816, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1542, plain, (![V_779, X1_764, X1_773, Z_772, V_195, Y_766, V_770, X_782, X_775, Y_771, X1_781, U_190, W_189, X1_192, U_783, Z_774, Z_777, W_769, V_765, Y_767, Y_194, Z_191, X_193, X_776]: (skf18(V_779, X_782, Y_771, Z_772, X1_764, W_189, U_190)=skf18(V_770, X_776, Y_767, Z_777, X1_781, W_189, U_190) | skf18(V_779, X_782, Y_771, Z_772, X1_764, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_770, X_776, Y_767, Z_777, X1_781, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_765 | skf18(V_779, X_782, Y_771, Z_772, X1_764, W_189, U_190)=V_765 | skf18(V_770, X_776, Y_767, Z_777, X1_781, W_189, U_190)=V_765 | V_765=U_783 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_783 | skf18(V_779, X_782, Y_771, Z_772, X1_764, W_189, U_190)=U_783 | skf18(V_770, X_776, Y_767, Z_777, X1_781, W_189, U_190)=U_783 | ~member(U_190, V_765, W_189) | ~member(U_190, U_783, W_189) | skf18(U_783, V_765, W_769, X_775, Y_766, Z_774, X1_773)!=V_765 | Z_777=X1_781 | Z_777=Y_767 | Y_767=X1_781 | Y_767=X_776 | Z_777=X_776 | X_776=X1_781 | X_776=V_770 | Y_767=V_770 | Z_777=V_770 | X1_781=V_770 | ~member(U_190, X1_781, W_189) | ~member(U_190, Z_777, W_189) | ~member(U_190, Y_767, W_189) | ~member(U_190, X_776, W_189) | ~member(U_190, V_770, W_189) | Z_772=X1_764 | Z_772=Y_771 | Y_771=X1_764 | Y_771=X_782 | Z_772=X_782 | X_782=X1_764 | X_782=V_779 | Y_771=V_779 | Z_772=V_779 | X1_764=V_779 | ~member(U_190, X1_764, W_189) | ~member(U_190, Z_772, W_189) | ~member(U_190, Y_771, W_189) | ~member(U_190, X_782, W_189) | ~member(U_190, V_779, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1561, plain, (![X1_786, V_195, Y_790, X4_800, Z_791, Z_788, X1_804, U_190, W_189, U_799, X1_192, Y_793, X_802, V_784, X_794, Z_798, V_796, V_789, X_787, Y_194, X1_785, Y_792, Z_191, W_801, X_193]: (skf18(V_796, X_802, Y_790, Z_791, X1_786, W_189, U_190)=skf18(V_784, X_787, Y_793, Z_798, X1_785, W_189, U_190) | skf18(V_796, X_802, Y_790, Z_791, X1_786, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_784, X_787, Y_793, Z_798, X1_785, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=X4_800 | skf18(V_796, X_802, Y_790, Z_791, X1_786, W_189, U_190)=X4_800 | skf18(V_784, X_787, Y_793, Z_798, X1_785, W_189, U_190)=X4_800 | X4_800=U_799 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_799 | skf18(V_796, X_802, Y_790, Z_791, X1_786, W_189, U_190)=U_799 | skf18(V_784, X_787, Y_793, Z_798, X1_785, W_189, U_190)=U_799 | ~member(U_190, X4_800, W_189) | ~member(U_190, U_799, W_189) | skf18(U_799, V_789, W_801, X_794, Y_792, Z_788, X1_804)!=U_799 | Z_798=X1_785 | Z_798=Y_793 | Y_793=X1_785 | Y_793=X_787 | Z_798=X_787 | X_787=X1_785 | X_787=V_784 | Y_793=V_784 | Z_798=V_784 | X1_785=V_784 | ~member(U_190, X1_785, W_189) | ~member(U_190, Z_798, W_189) | ~member(U_190, Y_793, W_189) | ~member(U_190, X_787, W_189) | ~member(U_190, V_784, W_189) | Z_791=X1_786 | Z_791=Y_790 | Y_790=X1_786 | Y_790=X_802 | Z_791=X_802 | X_802=X1_786 | X_802=V_796 | Y_790=V_796 | Z_791=V_796 | X1_786=V_796 | ~member(U_190, X1_786, W_189) | ~member(U_190, Z_791, W_189) | ~member(U_190, Y_790, W_189) | ~member(U_190, X_802, W_189) | ~member(U_190, V_796, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1503, plain, (![V_195, W_722, U_190, W_189, V_726, X1_192, V_734, U_733, Z_725, Z_728, Y_731, Y_724, X1_721, X1_727, X_723, Y_194, Z_191, X_193]: (skf18(V_734, X_723, Y_731, Z_728, X1_721, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=W_722 | skf18(V_734, X_723, Y_731, Z_728, X1_721, W_189, U_190)=W_722 | W_722=V_726 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_726 | skf18(V_734, X_723, Y_731, Z_728, X1_721, W_189, U_190)=V_726 | V_726=U_733 | W_722=U_733 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_733 | skf18(V_734, X_723, Y_731, Z_728, X1_721, W_189, U_190)=U_733 | ~member(U_190, W_722, W_189) | ~member(U_190, V_726, W_189) | ~member(U_190, U_733, W_189) | skf18(U_733, V_726, W_722, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), Y_724, Z_725, X1_727)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_728=X1_721 | Z_728=Y_731 | Y_731=X1_721 | Y_731=X_723 | Z_728=X_723 | X_723=X1_721 | X_723=V_734 | Y_731=V_734 | Z_728=V_734 | X1_721=V_734 | ~member(U_190, X1_721, W_189) | ~member(U_190, Z_728, W_189) | ~member(U_190, Y_731, W_189) | ~member(U_190, X_723, W_189) | ~member(U_190, V_734, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1484, plain, (![X1_706, V_195, W_708, V_707, Y_716, Y_713, U_718, U_190, W_189, X1_192, V_719, X_711, Z_714, X1_709, X_710, Z_720, Y_194, Z_191, X_193]: (skf18(V_719, X_711, Y_716, Z_714, X1_706, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=W_708 | skf18(V_719, X_711, Y_716, Z_714, X1_706, W_189, U_190)=W_708 | W_708=V_707 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_707 | skf18(V_719, X_711, Y_716, Z_714, X1_706, W_189, U_190)=V_707 | V_707=U_718 | W_708=U_718 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_718 | skf18(V_719, X_711, Y_716, Z_714, X1_706, W_189, U_190)=U_718 | ~member(U_190, W_708, W_189) | ~member(U_190, V_707, W_189) | ~member(U_190, U_718, W_189) | skf18(U_718, V_707, W_708, X_710, Y_713, Z_720, X1_709)!=W_708 | Z_714=X1_706 | Z_714=Y_716 | Y_716=X1_706 | Y_716=X_711 | Z_714=X_711 | X_711=X1_706 | X_711=V_719 | Y_716=V_719 | Z_714=V_719 | X1_706=V_719 | ~member(U_190, X1_706, W_189) | ~member(U_190, Z_714, W_189) | ~member(U_190, Y_716, W_189) | ~member(U_190, X_711, W_189) | ~member(U_190, V_719, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1465, plain, (![W_691, V_195, U_705, V_702, Y_704, X_692, X1_697, X_699, U_190, W_189, V_701, X1_192, X5_689, X4_693, Z_694, X1_690, Y_194, Y_698, Z_191, Z_703, X_193]: (skf18(V_702, X_692, Y_698, Z_694, X1_690, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=X5_689 | skf18(V_702, X_692, Y_698, Z_694, X1_690, W_189, U_190)=X5_689 | X5_689=X4_693 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=X4_693 | skf18(V_702, X_692, Y_698, Z_694, X1_690, W_189, U_190)=X4_693 | X4_693=U_705 | X5_689=U_705 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_705 | skf18(V_702, X_692, Y_698, Z_694, X1_690, W_189, U_190)=U_705 | ~member(U_190, X5_689, W_189) | ~member(U_190, X4_693, W_189) | ~member(U_190, U_705, W_189) | skf18(U_705, V_701, W_691, X_699, Y_704, Z_703, X1_697)!=U_705 | Z_694=X1_690 | Z_694=Y_698 | Y_698=X1_690 | Y_698=X_692 | Z_694=X_692 | X_692=X1_690 | X_692=V_702 | Y_698=V_702 | Z_694=V_702 | X1_690=V_702 | ~member(U_190, X1_690, W_189) | ~member(U_190, Z_694, W_189) | ~member(U_190, Y_698, W_189) | ~member(U_190, X_692, W_189) | ~member(U_190, V_702, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1522, plain, (![Z_750, V_747, X1_735, V_195, X_736, U_190, W_189, X1_192, V_737, Y_744, W_740, X_738, U_748, Y_745, X4_741, Y_194, X1_749, Z_191, X_193, Z_742]: (skf18(V_747, X_738, Y_744, Z_742, X1_735, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=X4_741 | skf18(V_747, X_738, Y_744, Z_742, X1_735, W_189, U_190)=X4_741 | X4_741=V_737 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_737 | skf18(V_747, X_738, Y_744, Z_742, X1_735, W_189, U_190)=V_737 | V_737=U_748 | X4_741=U_748 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_748 | skf18(V_747, X_738, Y_744, Z_742, X1_735, W_189, U_190)=U_748 | ~member(U_190, X4_741, W_189) | ~member(U_190, V_737, W_189) | ~member(U_190, U_748, W_189) | skf18(U_748, V_737, W_740, X_736, Y_745, Z_750, X1_749)!=V_737 | Z_742=X1_735 | Z_742=Y_744 | Y_744=X1_735 | Y_744=X_738 | Z_742=X_738 | X_738=X1_735 | X_738=V_747 | Y_744=V_747 | Z_742=V_747 | X1_735=V_747 | ~member(U_190, X1_735, W_189) | ~member(U_190, Z_742, W_189) | ~member(U_190, Y_744, W_189) | ~member(U_190, X_738, W_189) | ~member(U_190, V_747, W_189) | Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_1448, plain, (![Z_183, V_686, U_685, X_688, X1_184, W_687, W_180, X_186, V_188, U_182, Z_684, X1_682, Y_683]: (skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X_186 | X_186=W_180 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=W_180 | W_180=V_188 | X_186=V_188 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=V_188 | V_188=U_182 | W_180=U_182 | X_186=U_182 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=U_182 | ~member(U_685, X_186, W_687) | ~member(U_685, W_180, W_687) | ~member(U_685, V_188, W_687) | ~member(U_685, U_182, W_687) | skf18(U_182, V_188, W_180, X_186, skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685), Z_183, X1_184)!=skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685) | Z_684=X1_682 | Z_684=Y_683 | Y_683=X1_682 | Y_683=X_688 | Z_684=X_688 | X_688=X1_682 | X_688=V_686 | Y_683=V_686 | Z_684=V_686 | X1_682=V_686 | five(U_685, W_687) | ~member(U_685, X1_682, W_687) | ~member(U_685, Z_684, W_687) | ~member(U_685, Y_683, W_687) | ~member(U_685, X_688, W_687) | ~member(U_685, V_686, W_687)))). % 17.36/9.25 tff(c_1447, plain, (![Z_152, V_686, U_685, X4_158, X_155, X_688, X1_153, Y_156, X5_147, W_687, U_151, W_149, Z_684, X1_682, Y_683, V_157]: (skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X5_147 | X5_147=X4_158 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X4_158 | X4_158=V_157 | X5_147=V_157 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=V_157 | V_157=U_151 | X4_158=U_151 | X5_147=U_151 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=U_151 | ~member(U_685, X5_147, W_687) | ~member(U_685, X4_158, W_687) | ~member(U_685, V_157, W_687) | ~member(U_685, U_151, W_687) | skf18(U_151, V_157, W_149, X_155, Y_156, Z_152, X1_153)!=V_157 | Z_684=X1_682 | Z_684=Y_683 | Y_683=X1_682 | Y_683=X_688 | Z_684=X_688 | X_688=X1_682 | X_688=V_686 | Y_683=V_686 | Z_684=V_686 | X1_682=V_686 | five(U_685, W_687) | ~member(U_685, X1_682, W_687) | ~member(U_685, Z_684, W_687) | ~member(U_685, Y_683, W_687) | ~member(U_685, X_688, W_687) | ~member(U_685, V_686, W_687)))). % 17.36/9.25 tff(c_1445, plain, (![V_686, U_685, V_178, X_688, W_170, X_176, U_172, X1_174, Y_177, W_687, Z_173, Z_684, X1_682, Y_683]: (skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X_176 | X_176=W_170 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=W_170 | W_170=V_178 | X_176=V_178 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=V_178 | V_178=U_172 | W_170=U_172 | X_176=U_172 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=U_172 | ~member(U_685, X_176, W_687) | ~member(U_685, W_170, W_687) | ~member(U_685, V_178, W_687) | ~member(U_685, U_172, W_687) | skf18(U_172, V_178, W_170, X_176, Y_177, Z_173, X1_174)!=X_176 | Z_684=X1_682 | Z_684=Y_683 | Y_683=X1_682 | Y_683=X_688 | Z_684=X_688 | X_688=X1_682 | X_688=V_686 | Y_683=V_686 | Z_684=V_686 | X1_682=V_686 | five(U_685, W_687) | ~member(U_685, X1_682, W_687) | ~member(U_685, Z_684, W_687) | ~member(U_685, Y_683, W_687) | ~member(U_685, X_688, W_687) | ~member(U_685, V_686, W_687)))). % 17.36/9.25 tff(c_1446, plain, (![Z_163, V_686, U_685, X1_164, X_166, X_688, Y_167, W_160, W_687, U_162, X4_169, Z_684, X1_682, Y_683, V_168]: (skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X4_169 | X4_169=W_160 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=W_160 | W_160=V_168 | X4_169=V_168 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=V_168 | V_168=U_162 | W_160=U_162 | X4_169=U_162 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=U_162 | ~member(U_685, X4_169, W_687) | ~member(U_685, W_160, W_687) | ~member(U_685, V_168, W_687) | ~member(U_685, U_162, W_687) | skf18(U_162, V_168, W_160, X_166, Y_167, Z_163, X1_164)!=W_160 | Z_684=X1_682 | Z_684=Y_683 | Y_683=X1_682 | Y_683=X_688 | Z_684=X_688 | X_688=X1_682 | X_688=V_686 | Y_683=V_686 | Z_684=V_686 | X1_682=V_686 | five(U_685, W_687) | ~member(U_685, X1_682, W_687) | ~member(U_685, Z_684, W_687) | ~member(U_685, Y_683, W_687) | ~member(U_685, X_688, W_687) | ~member(U_685, V_686, W_687)))). % 17.36/9.25 tff(c_1444, plain, (![X4_208, V_686, U_685, X5_196, X_205, X_688, U_200, Z_201, X6_197, V_207, W_198, W_687, X1_203, Z_684, X1_682, Y_206, Y_683]: (skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X6_197 | X6_197=X5_196 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X5_196 | X5_196=X4_208 | X6_197=X4_208 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=X4_208 | X4_208=U_200 | X5_196=U_200 | X6_197=U_200 | skf18(V_686, X_688, Y_683, Z_684, X1_682, W_687, U_685)=U_200 | ~member(U_685, X6_197, W_687) | ~member(U_685, X5_196, W_687) | ~member(U_685, X4_208, W_687) | ~member(U_685, U_200, W_687) | skf18(U_200, V_207, W_198, X_205, Y_206, Z_201, X1_203)!=U_200 | Z_684=X1_682 | Z_684=Y_683 | Y_683=X1_682 | Y_683=X_688 | Z_684=X_688 | X_688=X1_682 | X_688=V_686 | Y_683=V_686 | Z_684=V_686 | X1_682=V_686 | five(U_685, W_687) | ~member(U_685, X1_682, W_687) | ~member(U_685, Z_684, W_687) | ~member(U_685, Y_683, W_687) | ~member(U_685, X_688, W_687) | ~member(U_685, V_686, W_687)))). % 17.36/9.25 tff(c_152, plain, (![V_195, U_190, W_189, X1_192, Y_194, Z_191, X_193]: (Z_191=X1_192 | Z_191=Y_194 | Y_194=X1_192 | Y_194=X_193 | Z_191=X_193 | X_193=X1_192 | X_193=V_195 | Y_194=V_195 | Z_191=V_195 | X1_192=V_195 | member(U_190, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), W_189) | five(U_190, W_189) | ~member(U_190, X1_192, W_189) | ~member(U_190, Z_191, W_189) | ~member(U_190, Y_194, W_189) | ~member(U_190, X_193, W_189) | ~member(U_190, V_195, W_189)))). % 17.36/9.25 tff(c_154, plain, (![X7_202, X4_208, X5_196, X_205, U_200, Z_201, X6_197, V_207, X3_199, W_198, X2_204, X1_203, Y_206]: (X7_202=X6_197 | X6_197=X5_196 | X7_202=X5_196 | X5_196=X4_208 | X6_197=X4_208 | X7_202=X4_208 | X4_208=U_200 | X5_196=U_200 | X6_197=U_200 | X7_202=U_200 | five(X2_204, X3_199) | ~member(X2_204, X7_202, X3_199) | ~member(X2_204, X6_197, X3_199) | ~member(X2_204, X5_196, X3_199) | ~member(X2_204, X4_208, X3_199) | ~member(X2_204, U_200, X3_199) | skf18(U_200, V_207, W_198, X_205, Y_206, Z_201, X1_203)!=U_200))). % 17.36/9.25 tff(c_148, plain, (![V_178, W_170, X_176, U_172, X1_174, Y_177, X2_175, X3_171, Z_173, X4_179]: (X_176=X4_179 | X_176=W_170 | X4_179=W_170 | W_170=V_178 | X_176=V_178 | X4_179=V_178 | V_178=U_172 | W_170=U_172 | X_176=U_172 | X4_179=U_172 | five(X2_175, X3_171) | ~member(X2_175, X4_179, X3_171) | ~member(X2_175, X_176, X3_171) | ~member(X2_175, W_170, X3_171) | ~member(X2_175, V_178, X3_171) | ~member(X2_175, U_172, X3_171) | skf18(U_172, V_178, W_170, X_176, Y_177, Z_173, X1_174)!=X_176))). % 17.36/9.25 tff(c_146, plain, (![Z_163, X1_164, X_166, Y_167, X5_159, W_160, U_162, X4_169, X3_161, V_168, X2_165]: (X5_159=X4_169 | X4_169=W_160 | X5_159=W_160 | W_160=V_168 | X4_169=V_168 | X5_159=V_168 | V_168=U_162 | W_160=U_162 | X4_169=U_162 | X5_159=U_162 | five(X2_165, X3_161) | ~member(X2_165, X5_159, X3_161) | ~member(X2_165, X4_169, X3_161) | ~member(X2_165, W_160, X3_161) | ~member(X2_165, V_168, X3_161) | ~member(X2_165, U_162, X3_161) | skf18(U_162, V_168, W_160, X_166, Y_167, Z_163, X1_164)!=W_160))). % 17.36/9.25 tff(c_1243, plain, (![W_598]: (skc11=W_598 | ~forename(skc6, W_598) | ~of(skc6, W_598, skc12)))). % 17.36/9.25 tff(c_1219, plain, (![U_218]: (~agent(skc6, skf7(U_218), U_218) | ~member(skc6, U_218, skc7)))). % 17.36/9.25 tff(c_1363, plain, (~act(skc6, skc10))). % 17.36/9.25 tff(c_1301, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.25 tff(c_1256, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.25 tff(c_144, plain, (![Z_152, X4_158, X_155, X1_153, Y_156, X5_147, X6_148, U_151, W_149, X2_154, X3_150, V_157]: (X6_148=X5_147 | X5_147=X4_158 | X6_148=X4_158 | X4_158=V_157 | X5_147=V_157 | X6_148=V_157 | V_157=U_151 | X4_158=U_151 | X5_147=U_151 | X6_148=U_151 | five(X2_154, X3_150) | ~member(X2_154, X6_148, X3_150) | ~member(X2_154, X5_147, X3_150) | ~member(X2_154, X4_158, X3_150) | ~member(X2_154, V_157, X3_150) | ~member(X2_154, U_151, X3_150) | skf18(U_151, V_157, W_149, X_155, Y_156, Z_152, X1_153)!=V_157))). % 17.36/9.25 tff(c_1132, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 17.36/9.25 tff(c_1118, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 17.36/9.25 tff(c_1307, plain, (~food(skc6, skc12))). % 17.36/9.25 tff(c_150, plain, (![Z_183, X2_185, X3_181, X1_184, Y_187, W_180, X_186, V_188, U_182]: (Y_187=X_186 | X_186=W_180 | Y_187=W_180 | W_180=V_188 | X_186=V_188 | Y_187=V_188 | V_188=U_182 | W_180=U_182 | X_186=U_182 | Y_187=U_182 | five(X2_185, X3_181) | ~member(X2_185, Y_187, X3_181) | ~member(X2_185, X_186, X3_181) | ~member(X2_185, W_180, X3_181) | ~member(X2_185, V_188, X3_181) | ~member(X2_185, U_182, X3_181) | skf18(U_182, V_188, W_180, X_186, Y_187, Z_183, X1_184)!=Y_187))). % 17.36/9.25 tff(c_1047, plain, (![U_245, V_246]: (~food(U_245, V_246) | ~human_person(U_245, V_246)))). % 17.36/9.25 tff(c_1081, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 17.36/9.25 tff(c_1293, plain, (~abstraction(skc6, skc10))). % 17.36/9.25 tff(c_1056, plain, (![U_561, V_562]: (~abstraction(U_561, V_562) | ~beverage(U_561, V_562)))). % 17.36/9.25 tff(c_1262, plain, (~animate(skc6, skc10))). % 17.36/9.25 tff(c_142, plain, (![W_146, U_144, V_145]: (skf17(W_146, U_144)=V_145 | skf15(W_146, U_144)=V_145 | skf13(W_146, U_144)=V_145 | skf11(W_146, U_144)=V_145 | skf9(W_146, U_144)=V_145 | ~five(U_144, W_146) | ~member(U_144, V_145, W_146)))). % 17.36/9.25 tff(c_1066, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.25 tff(c_1082, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 17.36/9.25 tff(c_1034, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 17.36/9.25 tff(c_140, plain, (![W_142, V_141, U_140, X_143]: (W_142=V_141 | ~entity(U_140, X_143) | ~of(U_140, V_141, X_143) | ~forename(U_140, W_142) | ~of(U_140, W_142, X_143) | ~forename(U_140, V_141)))). % 17.36/9.25 tff(c_1013, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 17.36/9.25 tff(c_1035, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 17.36/9.25 tff(c_1227, plain, (~beverage(skc6, skc12))). % 17.36/9.25 tff(c_933, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.26 tff(c_1222, plain, (~agent(skc6, skc9, skc10))). % 17.36/9.26 tff(c_138, plain, (![U_137, V_138, W_139]: (~agent(U_137, V_138, W_139) | ~patient(U_137, V_138, W_139) | ~nonreflexive(U_137, V_138)))). % 17.36/9.26 tff(c_1209, plain, (abstraction(skc6, skf13(skc7, skc6)))). % 17.36/9.26 tff(c_1205, plain, (cash(skc6, skf13(skc7, skc6)))). % 17.36/9.26 tff(c_1201, plain, (dollar(skc6, skf13(skc7, skc6)))). % 17.36/9.26 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf13(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 17.36/9.26 tff(c_1193, plain, (abstraction(skc6, skf9(skc7, skc6)))). % 17.36/9.26 tff(c_1173, plain, (abstraction(skc6, skf17(skc7, skc6)))). % 17.36/9.26 tff(c_1177, plain, (abstraction(skc6, skf11(skc7, skc6)))). % 17.36/9.26 tff(c_1189, plain, (cash(skc6, skf9(skc7, skc6)))). % 17.36/9.26 tff(c_1185, plain, (dollar(skc6, skf9(skc7, skc6)))). % 17.36/9.26 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf9(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 17.36/9.26 tff(c_1169, plain, (cash(skc6, skf11(skc7, skc6)))). % 17.36/9.26 tff(c_1157, plain, (cash(skc6, skf17(skc7, skc6)))). % 17.36/9.26 tff(c_1165, plain, (dollar(skc6, skf11(skc7, skc6)))). % 17.36/9.26 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf11(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 17.36/9.26 tff(c_1141, plain, (dollar(skc6, skf17(skc7, skc6)))). % 17.36/9.26 tff(c_1153, plain, (~cost(skc6, skc7))). % 17.36/9.26 tff(c_1152, plain, (~act(skc6, skc7))). % 17.36/9.26 tff(c_1145, plain, (~event(skc6, skc7))). % 17.36/9.26 tff(c_1133, plain, (~eventuality(skc6, skc7))). % 17.36/9.26 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf17(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 17.36/9.26 tff(c_989, plain, (![U_309, V_310]: (~eventuality(U_309, V_310) | ~group(U_309, V_310)))). % 17.36/9.26 tff(c_1124, plain, (skf9(skc7, skc6)!=skf11(skc7, skc6))). % 17.36/9.26 tff(c_1119, plain, (~abstraction(skc6, skc7))). % 17.36/9.26 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf9(U_135, V_136)!=skf11(U_135, V_136)))). % 17.36/9.26 tff(c_999, plain, (![U_309, V_310]: (~abstraction(U_309, V_310) | ~group(U_309, V_310)))). % 17.36/9.26 tff(c_1103, plain, (skf13(skc7, skc6)!=skf11(skc7, skc6))). % 17.36/9.26 tff(c_1098, plain, (![V_220]: (agent(skc6, skf7(V_220), skc7)))). % 17.36/9.26 tff(c_1108, plain, (![V_572]: (~beverage(skc6, skf7(V_572))))). % 17.36/9.26 tff(c_1080, plain, (![V_217]: (~entity(skc6, skf7(V_217))))). % 17.36/9.26 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf13(U_133, V_134)!=skf11(U_133, V_134)))). % 17.36/9.26 tff(c_1087, plain, (~beverage(skc6, skc9))). % 17.36/9.26 tff(c_1083, plain, (~entity(skc6, skc9))). % 17.36/9.26 tff(c_969, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 17.36/9.26 tff(c_954, plain, (![U_526, V_527]: (~animate(U_526, V_527) | ~food(U_526, V_527)))). % 17.36/9.26 tff(c_1061, plain, (skf17(skc7, skc6)!=skf11(skc7, skc6))). % 17.36/9.26 tff(c_1055, plain, (~beverage(skc6, skc7))). % 17.36/9.26 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf17(U_119, V_120)!=skf11(U_119, V_120)))). % 17.36/9.26 tff(c_994, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.26 tff(c_953, plain, (![U_526, V_527]: (~living(U_526, V_527) | ~food(U_526, V_527)))). % 17.36/9.26 tff(c_1042, plain, (skf15(skc7, skc6)!=skf13(skc7, skc6))). % 17.36/9.26 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf15(U_129, V_130)!=skf13(U_129, V_130)))). % 17.36/9.26 tff(c_1033, plain, (![V_217]: (~abstraction(skc6, skf7(V_217))))). % 17.36/9.26 tff(c_1036, plain, (~abstraction(skc6, skc9))). % 17.36/9.26 tff(c_974, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 17.36/9.26 tff(c_1019, plain, (skf9(skc7, skc6)!=skf13(skc7, skc6))). % 17.36/9.26 tff(c_1014, plain, (~entity(skc6, skc7))). % 17.36/9.26 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf9(U_131, V_132)!=skf13(U_131, V_132)))). % 17.36/9.26 tff(c_984, plain, (![U_309, V_310]: (~entity(U_309, V_310) | ~group(U_309, V_310)))). % 17.36/9.26 tff(c_601, plain, (![U_409, V_410]: (impartial(U_409, V_410) | ~food(U_409, V_410)))). % 17.36/9.26 tff(c_1004, plain, (skf17(skc7, skc6)!=skf13(skc7, skc6))). % 17.36/9.26 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf17(U_121, V_122)!=skf13(U_121, V_122)))). % 17.36/9.26 tff(c_369, plain, (![U_332, V_333]: (~multiple(U_332, V_333) | ~abstraction(U_332, V_333)))). % 17.36/9.26 tff(c_600, plain, (![U_409, V_410]: (entity(U_409, V_410) | ~food(U_409, V_410)))). % 17.36/9.26 tff(c_898, plain, (![U_508, V_509]: (~multiple(U_508, V_509) | ~eventuality(U_508, V_509)))). % 17.36/9.26 tff(c_489, plain, (![U_373, V_374]: (~multiple(U_373, V_374) | ~entity(U_373, V_374)))). % 17.36/9.26 tff(c_979, plain, (skf9(skc7, skc6)!=skf17(skc7, skc6))). % 17.36/9.26 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf9(U_117, V_118)!=skf17(U_117, V_118)))). % 17.36/9.26 tff(c_713, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 17.36/9.26 tff(c_703, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 17.36/9.26 tff(c_964, plain, (skf17(skc7, skc6)!=skf15(skc7, skc6))). % 17.36/9.26 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf17(U_123, V_124)!=skf15(U_123, V_124)))). % 17.36/9.26 tff(c_959, plain, (abstraction(skc6, skf15(skc7, skc6)))). % 17.36/9.26 tff(c_589, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 17.36/9.26 tff(c_602, plain, (![U_409, V_410]: (nonliving(U_409, V_410) | ~food(U_409, V_410)))). % 17.36/9.26 tff(c_945, plain, (cash(skc6, skf15(skc7, skc6)))). % 17.36/9.26 tff(c_941, plain, (dollar(skc6, skf15(skc7, skc6)))). % 17.36/9.26 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf15(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 17.36/9.26 tff(c_913, plain, (![U_49, V_50]: (~female(U_49, V_50) | ~food(U_49, V_50)))). % 17.36/9.26 tff(c_928, plain, (skf9(skc7, skc6)!=skf15(skc7, skc6))). % 17.36/9.26 tff(c_923, plain, (abstraction(skc6, skc11))). % 17.36/9.26 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf9(U_125, V_126)!=skf15(U_125, V_126)))). % 17.36/9.26 tff(c_363, plain, (![U_328, V_329]: (abstraction(U_328, V_329) | ~forename(U_328, V_329)))). % 17.36/9.26 tff(c_607, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 17.36/9.26 tff(c_260, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 17.36/9.26 tff(c_908, plain, (skf15(skc7, skc6)!=skf11(skc7, skc6))). % 17.36/9.26 tff(c_903, plain, (entity(skc6, skc12))). % 17.36/9.26 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf15(U_127, V_128)!=skf11(U_127, V_128)))). % 17.36/9.26 tff(c_291, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 17.36/9.26 tff(c_285, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 17.36/9.26 tff(c_892, plain, (~cost(skc6, skc12))). % 17.36/9.26 tff(c_196, plain, (![U_218]: (patient(skc6, skf7(U_218), U_218) | ~member(skc6, U_218, skc7)))). % 17.36/9.26 tff(c_891, plain, (~act(skc6, skc12))). % 17.36/9.26 tff(c_884, plain, (~event(skc6, skc12))). % 17.36/9.26 tff(c_880, plain, (~eventuality(skc6, skc12))). % 17.36/9.26 tff(c_261, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 17.36/9.26 tff(c_874, plain, (![V_217]: (event(skc6, skf7(V_217))))). % 17.36/9.26 tff(c_227, plain, (![U_245, V_246]: (impartial(U_245, V_246) | ~human_person(U_245, V_246)))). % 17.36/9.26 tff(c_296, plain, (![U_293, V_294]: (~general(U_293, V_294) | ~eventuality(U_293, V_294)))). % 17.36/9.26 tff(c_320, plain, (![U_307, V_308]: (~female(U_307, V_308) | ~abstraction(U_307, V_308)))). % 17.36/9.26 tff(c_314, plain, (![U_35, V_36]: (~existent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 17.36/9.26 tff(c_697, plain, (![V_213]: (nonreflexive(skc6, skf7(V_213))))). % 17.36/9.27 tff(c_228, plain, (![U_245, V_246]: (living(U_245, V_246) | ~human_person(U_245, V_246)))). % 17.36/9.27 tff(c_266, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 17.36/9.27 tff(c_249, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 17.36/9.27 tff(c_342, plain, (![U_319, V_320]: (abstraction(U_319, V_320) | ~currency(U_319, V_320)))). % 17.36/9.27 tff(c_583, plain, (![V_211]: (cost(skc6, skf7(V_211))))). % 17.36/9.27 tff(c_494, plain, (~abstraction(skc6, skc12))). % 17.36/9.27 tff(c_336, plain, (![U_15, V_16]: (~human(U_15, V_16) | ~abstraction(U_15, V_16)))). % 17.36/9.27 tff(c_284, plain, (![U_55, V_56]: (singleton(U_55, V_56) | ~entity(U_55, V_56)))). % 17.36/9.27 tff(c_483, plain, (![V_371]: (~past(skc6, skf7(V_371))))). % 17.36/9.27 tff(c_478, plain, (![V_215]: (present(skc6, skf7(V_215))))). % 17.36/9.27 tff(c_347, plain, (![U_321, V_322]: (singleton(U_321, V_322) | ~abstraction(U_321, V_322)))). % 17.36/9.27 tff(c_325, plain, (![U_309, V_310]: (multiple(U_309, V_310) | ~group(U_309, V_310)))). % 17.36/9.27 tff(c_357, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 17.36/9.27 tff(c_186, plain, (![U_209]: (dollar(skc6, U_209) | ~member(skc6, U_209, skc7)))). % 17.36/9.27 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 17.36/9.27 tff(c_352, plain, (act(skc6, skc9))). % 17.36/9.27 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 17.36/9.27 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 17.36/9.27 tff(c_337, plain, (~human(skc6, skc7))). % 17.36/9.27 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 17.36/9.27 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 17.36/9.27 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 17.36/9.27 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 17.36/9.27 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 17.36/9.27 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 17.36/9.27 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 17.36/9.27 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 17.36/9.27 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 17.36/9.27 tff(c_308, plain, (human(skc6, skc12))). % 17.36/9.27 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 17.36/9.27 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 17.36/9.27 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 17.36/9.27 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 17.36/9.27 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 17.36/9.27 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 17.36/9.27 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 17.36/9.27 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 17.36/9.27 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 17.36/9.27 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 17.36/9.27 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 17.36/9.27 tff(c_273, plain, (beverage(skc6, skc10))). % 17.36/9.27 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 17.36/9.27 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 17.36/9.27 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 17.36/9.27 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 17.36/9.27 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 17.36/9.27 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 17.36/9.27 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 17.36/9.27 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 17.36/9.27 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 17.36/9.27 tff(c_244, plain, (animate(skc6, skc12))). % 17.36/9.27 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 17.36/9.27 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 17.36/9.27 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 17.36/9.27 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 17.36/9.27 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 17.36/9.27 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 17.36/9.27 tff(c_234, plain, (female(skc6, skc12))). % 17.36/9.27 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 17.36/9.27 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 17.36/9.27 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 17.36/9.27 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 17.36/9.27 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 17.36/9.27 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 17.36/9.27 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 17.36/9.27 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 17.36/9.27 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 17.36/9.27 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 17.36/9.27 tff(c_211, plain, (human_person(skc6, skc12))). % 17.36/9.27 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 17.36/9.27 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 17.36/9.27 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 17.36/9.27 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 17.36/9.27 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 17.36/9.27 tff(c_180, plain, (of(skc6, skc11, skc12))). % 17.36/9.27 tff(c_182, plain, (agent(skc6, skc9, skc12))). % 17.36/9.27 tff(c_184, plain, (patient(skc6, skc9, skc10))). % 17.36/9.27 tff(c_160, plain, (shake_beverage(skc6, skc10))). % 17.36/9.27 tff(c_158, plain, (woman(skc6, skc12))). % 17.36/9.27 tff(c_176, plain, (forename(skc6, skc11))). % 17.36/9.27 tff(c_174, plain, (event(skc6, skc9))). % 17.36/9.27 tff(c_172, plain, (past(skc6, skc9))). % 17.36/9.27 tff(c_170, plain, (nonreflexive(skc6, skc9))). % 17.36/9.27 tff(c_168, plain, (order(skc6, skc9))). % 17.36/9.27 tff(c_162, plain, (nonhuman(skc6, skc7))). % 17.36/9.27 tff(c_164, plain, (five(skc6, skc7))). % 17.36/9.27 tff(c_166, plain, (group(skc6, skc7))). % 17.36/9.27 tff(c_178, plain, (mia_forename(skc6, skc11))). % 17.36/9.27 tff(c_156, plain, (actual_world(skc6))). % 17.36/9.27 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.36/9.27 %------------------------------------------------------------------------------