%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP052-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n007.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 15.17s 8.16s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP052-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:17:08 EDT 2025 % 0.13/0.34 % CPUTime : % 15.17/8.15 % 15.17/8.16 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.17/8.16 % 15.17/8.16 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.17/8.16 %$ 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 > skc8 > skc7 > skc6 > skc11 > skc10 % 15.17/8.16 % 15.17/8.16 %Foreground sorts: % 15.17/8.16 % 15.17/8.16 % 15.17/8.16 %Background operators: % 15.17/8.16 % 15.17/8.16 % 15.17/8.16 %Foreground operators: % 15.17/8.16 tff(nonliving, type, nonliving: ($i * $i) > $o). % 15.17/8.16 tff(relation, type, relation: ($i * $i) > $o). % 15.17/8.16 tff(member, type, member: ($i * $i * $i) > $o). % 15.17/8.16 tff(forename, type, forename: ($i * $i) > $o). % 15.17/8.16 tff(skc7, type, skc7: $i). % 15.17/8.16 tff(female, type, female: ($i * $i) > $o). % 15.17/8.16 tff(living, type, living: ($i * $i) > $o). % 15.17/8.16 tff(cost, type, cost: ($i * $i) > $o). % 15.17/8.16 tff(human_person, type, human_person: ($i * $i) > $o). % 15.17/8.16 tff(present, type, present: ($i * $i) > $o). % 15.17/8.16 tff(skc11, type, skc11: $i). % 15.17/8.16 tff(skf18, type, skf18: ($i * $i * $i * $i * $i * $i * $i) > $i). % 15.17/8.16 tff(entity, type, entity: ($i * $i) > $o). % 15.17/8.16 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 15.17/8.16 tff(skc9, type, skc9: $i). % 15.17/8.16 tff(past, type, past: ($i * $i) > $o). % 15.17/8.16 tff(beverage, type, beverage: ($i * $i) > $o). % 15.17/8.16 tff(eventuality, type, eventuality: ($i * $i) > $o). % 15.17/8.16 tff(existent, type, existent: ($i * $i) > $o). % 15.17/8.16 tff(abstraction, type, abstraction: ($i * $i) > $o). % 15.17/8.16 tff(skc8, type, skc8: $i). % 15.17/8.16 tff(relname, type, relname: ($i * $i) > $o). % 15.17/8.16 tff(possession, type, possession: ($i * $i) > $o). % 15.17/8.16 tff(singleton, type, singleton: ($i * $i) > $o). % 15.17/8.16 tff(multiple, type, multiple: ($i * $i) > $o). % 15.17/8.16 tff(organism, type, organism: ($i * $i) > $o). % 15.17/8.16 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 15.17/8.16 tff(animate, type, animate: ($i * $i) > $o). % 15.17/8.16 tff(of, type, of: ($i * $i * $i) > $o). % 15.17/8.16 tff(actual_world, type, actual_world: $i > $o). % 15.17/8.16 tff(dollar, type, dollar: ($i * $i) > $o). % 15.17/8.16 tff(agent, type, agent: ($i * $i * $i) > $o). % 15.17/8.16 tff(skf9, type, skf9: ($i * $i) > $i). % 15.17/8.16 tff(skf17, type, skf17: ($i * $i) > $i). % 15.17/8.16 tff(group, type, group: ($i * $i) > $o). % 15.17/8.16 tff(five, type, five: ($i * $i) > $o). % 15.17/8.16 tff(general, type, general: ($i * $i) > $o). % 15.17/8.16 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 15.17/8.16 tff(food, type, food: ($i * $i) > $o). % 15.17/8.16 tff(event, type, event: ($i * $i) > $o). % 15.17/8.16 tff(woman, type, woman: ($i * $i) > $o). % 15.17/8.16 tff(currency, type, currency: ($i * $i) > $o). % 15.17/8.16 tff(skf7, type, skf7: $i > $i). % 15.17/8.16 tff(patient, type, patient: ($i * $i * $i) > $o). % 15.17/8.16 tff(skf15, type, skf15: ($i * $i) > $i). % 15.17/8.16 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 15.17/8.16 tff(cash, type, cash: ($i * $i) > $o). % 15.17/8.16 tff(skf11, type, skf11: ($i * $i) > $i). % 15.17/8.16 tff(thing, type, thing: ($i * $i) > $o). % 15.17/8.16 tff(human, type, human: ($i * $i) > $o). % 15.17/8.16 tff(skf13, type, skf13: ($i * $i) > $i). % 15.17/8.16 tff(unisex, type, unisex: ($i * $i) > $o). % 15.17/8.16 tff(set, type, set: ($i * $i) > $o). % 15.17/8.16 tff(skc6, type, skc6: $i). % 15.17/8.16 tff(impartial, type, impartial: ($i * $i) > $o). % 15.17/8.16 tff(object, type, object: ($i * $i) > $o). % 15.17/8.16 tff(order, type, order: ($i * $i) > $o). % 15.17/8.16 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 15.17/8.16 tff(specific, type, specific: ($i * $i) > $o). % 15.17/8.16 tff(skc10, type, skc10: $i). % 15.17/8.16 tff(act, type, act: ($i * $i) > $o). % 15.17/8.16 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 15.17/8.16 % 15.17/8.16 %Saturated clause set: % 15.17/8.17 tff(c_1639, plain, (![Z_924, V_935, X1_937, X1_915, Y_914, V_195, X_933, Z_917, Z_928, V_923, Y_926, Y_941, U_190, W_189, V_938, Z_927, X1_192, W_922, X_932, Y_916, V_931, X1_921, X1_918, X_940, X1_925, V_919, Z_920, Y_194, X_929, Z_191, X_939, Y_942, X_193]: (skf18(V_938, X_929, Y_942, Z_917, X1_921, W_189, U_190)=skf18(V_923, X_932, Y_914, Z_927, X1_918, W_189, U_190) | skf18(V_938, X_929, Y_942, Z_917, X1_921, W_189, U_190)=skf18(V_919, X_933, Y_941, Z_920, X1_937, W_189, U_190) | skf18(V_923, X_932, Y_914, Z_927, X1_918, W_189, U_190)=skf18(V_919, X_933, Y_941, Z_920, X1_937, W_189, U_190) | skf18(V_935, X_940, Y_926, Z_928, X1_915, W_189, U_190)=skf18(V_919, X_933, Y_941, Z_920, X1_937, W_189, U_190) | skf18(V_938, X_929, Y_942, Z_917, X1_921, W_189, U_190)=skf18(V_935, X_940, Y_926, Z_928, X1_915, W_189, U_190) | skf18(V_935, X_940, Y_926, Z_928, X1_915, W_189, U_190)=skf18(V_923, X_932, Y_914, Z_927, X1_918, W_189, U_190) | skf18(V_935, X_940, Y_926, Z_928, X1_915, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_919, X_933, Y_941, Z_920, X1_937, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_938, X_929, Y_942, Z_917, X1_921, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_923, X_932, Y_914, Z_927, X1_918, 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_931, W_922, X_939, Y_916, Z_924, X1_925)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_927=X1_918 | Z_927=Y_914 | Y_914=X1_918 | Y_914=X_932 | Z_927=X_932 | X_932=X1_918 | X_932=V_923 | Y_914=V_923 | Z_927=V_923 | X1_918=V_923 | ~member(U_190, X1_918, W_189) | ~member(U_190, Z_927, W_189) | ~member(U_190, Y_914, W_189) | ~member(U_190, X_932, W_189) | ~member(U_190, V_923, W_189) | Z_917=X1_921 | Z_917=Y_942 | Y_942=X1_921 | Y_942=X_929 | Z_917=X_929 | X_929=X1_921 | X_929=V_938 | Y_942=V_938 | Z_917=V_938 | X1_921=V_938 | ~member(U_190, X1_921, W_189) | ~member(U_190, Z_917, W_189) | ~member(U_190, Y_942, W_189) | ~member(U_190, X_929, W_189) | ~member(U_190, V_938, W_189) | Z_920=X1_937 | Z_920=Y_941 | Y_941=X1_937 | Y_941=X_933 | Z_920=X_933 | X_933=X1_937 | X_933=V_919 | Y_941=V_919 | Z_920=V_919 | X1_937=V_919 | ~member(U_190, X1_937, W_189) | ~member(U_190, Z_920, W_189) | ~member(U_190, Y_941, W_189) | ~member(U_190, X_933, W_189) | ~member(U_190, V_919, W_189) | Z_928=X1_915 | Z_928=Y_926 | Y_926=X1_915 | Y_926=X_940 | Z_928=X_940 | X_940=X1_915 | X_940=V_935 | Y_926=V_935 | Z_928=V_935 | X1_915=V_935 | ~member(U_190, X1_915, W_189) | ~member(U_190, Z_928, W_189) | ~member(U_190, Y_926, W_189) | ~member(U_190, X_940, 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)))). % 15.17/8.17 tff(c_1619, plain, (![X_890, V_195, X_880, V_887, X_873, Y_877, X1_867, U_883, Z_868, U_190, W_189, X_886, X1_192, V_889, Y_876, Z_878, X1_872, Z_870, Y_881, W_874, Z_871, Y_879, Y_194, V_884, X1_875, Z_191, X1_869, X_193]: (skf18(V_889, X_886, Y_879, Z_871, X1_872, W_189, U_190)=skf18(V_884, X_873, Y_876, Z_870, X1_867, W_189, U_190) | skf18(V_889, X_886, Y_879, Z_871, X1_872, W_189, U_190)=skf18(V_887, X_890, Y_877, Z_878, X1_869, W_189, U_190) | skf18(V_887, X_890, Y_877, Z_878, X1_869, W_189, U_190)=skf18(V_884, X_873, Y_876, Z_870, X1_867, W_189, U_190) | skf18(V_887, X_890, Y_877, Z_878, X1_869, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_889, X_886, Y_879, Z_871, X1_872, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_884, X_873, Y_876, Z_870, X1_867, 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_883 | skf18(V_887, X_890, Y_877, Z_878, X1_869, W_189, U_190)=U_883 | skf18(V_889, X_886, Y_879, Z_871, X1_872, W_189, U_190)=U_883 | skf18(V_884, X_873, Y_876, Z_870, X1_867, W_189, U_190)=U_883 | ~member(U_190, U_883, W_189) | skf18(U_883, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), W_874, X_880, Y_881, Z_868, X1_875)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_870=X1_867 | Z_870=Y_876 | Y_876=X1_867 | Y_876=X_873 | Z_870=X_873 | X_873=X1_867 | X_873=V_884 | Y_876=V_884 | Z_870=V_884 | X1_867=V_884 | ~member(U_190, X1_867, W_189) | ~member(U_190, Z_870, W_189) | ~member(U_190, Y_876, W_189) | ~member(U_190, X_873, W_189) | ~member(U_190, V_884, W_189) | Z_871=X1_872 | Z_871=Y_879 | Y_879=X1_872 | Y_879=X_886 | Z_871=X_886 | X_886=X1_872 | X_886=V_889 | Y_879=V_889 | Z_871=V_889 | X1_872=V_889 | ~member(U_190, X1_872, W_189) | ~member(U_190, Z_871, W_189) | ~member(U_190, Y_879, W_189) | ~member(U_190, X_886, W_189) | ~member(U_190, V_889, W_189) | Z_878=X1_869 | Z_878=Y_877 | Y_877=X1_869 | Y_877=X_890 | Z_878=X_890 | X_890=X1_869 | X_890=V_887 | Y_877=V_887 | Z_878=V_887 | X1_869=V_887 | ~member(U_190, X1_869, W_189) | ~member(U_190, Z_878, W_189) | ~member(U_190, Y_877, W_189) | ~member(U_190, X_890, W_189) | ~member(U_190, V_887, 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)))). % 15.17/8.17 tff(c_1600, plain, (![X1_843, V_195, Y_849, X_844, Y_852, X_865, V_859, Z_851, Z_853, Z_842, Y_854, U_190, W_189, X_864, X1_192, X_848, V_856, U_866, X1_845, Y_863, X1_850, W_858, V_847, Y_194, Z_191, X1_846, V_855, X_193, Z_860]: (skf18(V_856, X_844, Y_863, Z_851, X1_843, W_189, U_190)=skf18(V_855, X_848, Y_854, Z_860, X1_845, W_189, U_190) | skf18(V_859, X_865, Y_852, Z_853, X1_846, W_189, U_190)=skf18(V_855, X_848, Y_854, Z_860, X1_845, W_189, U_190) | skf18(V_859, X_865, Y_852, Z_853, X1_846, W_189, U_190)=skf18(V_856, X_844, Y_863, Z_851, X1_843, W_189, U_190) | skf18(V_859, X_865, Y_852, Z_853, X1_846, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_855, X_848, Y_854, Z_860, X1_845, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_856, X_844, Y_863, Z_851, X1_843, 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_866 | skf18(V_859, X_865, Y_852, Z_853, X1_846, W_189, U_190)=U_866 | skf18(V_855, X_848, Y_854, Z_860, X1_845, W_189, U_190)=U_866 | skf18(V_856, X_844, Y_863, Z_851, X1_843, W_189, U_190)=U_866 | ~member(U_190, U_866, W_189) | skf18(U_866, V_847, W_858, X_864, Y_849, Z_842, X1_850)!=U_866 | Z_851=X1_843 | Z_851=Y_863 | Y_863=X1_843 | Y_863=X_844 | Z_851=X_844 | X_844=X1_843 | X_844=V_856 | Y_863=V_856 | Z_851=V_856 | X1_843=V_856 | ~member(U_190, X1_843, W_189) | ~member(U_190, Z_851, W_189) | ~member(U_190, Y_863, W_189) | ~member(U_190, X_844, W_189) | ~member(U_190, V_856, W_189) | Z_860=X1_845 | Z_860=Y_854 | Y_854=X1_845 | Y_854=X_848 | Z_860=X_848 | X_848=X1_845 | X_848=V_855 | Y_854=V_855 | Z_860=V_855 | X1_845=V_855 | ~member(U_190, X1_845, W_189) | ~member(U_190, Z_860, W_189) | ~member(U_190, Y_854, W_189) | ~member(U_190, X_848, W_189) | ~member(U_190, V_855, W_189) | Z_853=X1_846 | Z_853=Y_852 | Y_852=X1_846 | Y_852=X_865 | Z_853=X_865 | X_865=X1_846 | X_865=V_859 | Y_852=V_859 | Z_853=V_859 | X1_846=V_859 | ~member(U_190, X1_846, W_189) | ~member(U_190, Z_853, W_189) | ~member(U_190, Y_852, W_189) | ~member(U_190, X_865, W_189) | ~member(U_190, V_859, 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)))). % 15.17/8.17 tff(c_1542, plain, (![X1_775, X_772, V_779, X1_764, V_768, V_195, U_782, V_767, Y_769, X1_765, U_190, W_189, X_771, X1_192, X_781, Z_766, Z_774, Z_777, Y_194, Z_191, Y_770, X_193, Y_773]: (skf18(V_779, X_781, Y_773, Z_774, X1_765, W_189, U_190)=skf18(V_768, X_772, Y_769, Z_766, X1_764, W_189, U_190) | skf18(V_779, X_781, Y_773, Z_774, X1_765, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_768, X_772, Y_769, Z_766, X1_764, 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_767 | skf18(V_779, X_781, Y_773, Z_774, X1_765, W_189, U_190)=V_767 | skf18(V_768, X_772, Y_769, Z_766, X1_764, W_189, U_190)=V_767 | V_767=U_782 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_782 | skf18(V_779, X_781, Y_773, Z_774, X1_765, W_189, U_190)=U_782 | skf18(V_768, X_772, Y_769, Z_766, X1_764, W_189, U_190)=U_782 | ~member(U_190, V_767, W_189) | ~member(U_190, U_782, W_189) | skf18(U_782, V_767, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), X_771, Y_770, Z_777, X1_775)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_766=X1_764 | Z_766=Y_769 | Y_769=X1_764 | Y_769=X_772 | Z_766=X_772 | X_772=X1_764 | X_772=V_768 | Y_769=V_768 | Z_766=V_768 | X1_764=V_768 | ~member(U_190, X1_764, W_189) | ~member(U_190, Z_766, W_189) | ~member(U_190, Y_769, W_189) | ~member(U_190, X_772, W_189) | ~member(U_190, V_768, W_189) | Z_774=X1_765 | Z_774=Y_773 | Y_773=X1_765 | Y_773=X_781 | Z_774=X_781 | X_781=X1_765 | X_781=V_779 | Y_773=V_779 | Z_774=V_779 | X1_765=V_779 | ~member(U_190, X1_765, W_189) | ~member(U_190, Z_774, W_189) | ~member(U_190, Y_773, W_189) | ~member(U_190, X_781, 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)))). % 15.17/8.17 tff(c_1561, plain, (![V_783, V_195, U_785, X1_784, Y_799, U_190, W_189, X1_192, X1_800, Y_793, X_802, X_794, Y_791, V_796, X_797, X1_790, Z_801, Y_194, W_787, Z_191, Z_792, V_786, X_193, Z_789]: (skf18(V_796, X_802, Y_791, Z_792, X1_784, W_189, U_190)=skf18(V_783, X_794, Y_793, Z_789, X1_790, W_189, U_190) | skf18(V_796, X_802, Y_791, Z_792, X1_784, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_783, X_794, Y_793, Z_789, X1_790, 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_786 | skf18(V_796, X_802, Y_791, Z_792, X1_784, W_189, U_190)=V_786 | skf18(V_783, X_794, Y_793, Z_789, X1_790, W_189, U_190)=V_786 | V_786=U_785 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_785 | skf18(V_796, X_802, Y_791, Z_792, X1_784, W_189, U_190)=U_785 | skf18(V_783, X_794, Y_793, Z_789, X1_790, W_189, U_190)=U_785 | ~member(U_190, V_786, W_189) | ~member(U_190, U_785, W_189) | skf18(U_785, V_786, W_787, X_797, Y_799, Z_801, X1_800)!=V_786 | Z_789=X1_790 | Z_789=Y_793 | Y_793=X1_790 | Y_793=X_794 | Z_789=X_794 | X_794=X1_790 | X_794=V_783 | Y_793=V_783 | Z_789=V_783 | X1_790=V_783 | ~member(U_190, X1_790, W_189) | ~member(U_190, Z_789, W_189) | ~member(U_190, Y_793, W_189) | ~member(U_190, X_794, W_189) | ~member(U_190, V_783, W_189) | Z_792=X1_784 | Z_792=Y_791 | Y_791=X1_784 | Y_791=X_802 | Z_792=X_802 | X_802=X1_784 | X_802=V_796 | Y_791=V_796 | Z_792=V_796 | X1_784=V_796 | ~member(U_190, X1_784, W_189) | ~member(U_190, Z_792, W_189) | ~member(U_190, Y_791, 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)))). % 15.17/8.17 tff(c_1580, plain, (![X_821, V_195, X4_819, Z_810, V_808, X1_804, U_190, W_189, X1_192, X_813, X1_823, W_820, V_803, U_818, X_806, V_815, Z_807, Y_811, X1_805, Y_809, Y_194, Z_817, Y_812, Z_191, X_193]: (skf18(V_815, X_821, Y_809, Z_810, X1_805, W_189, U_190)=skf18(V_803, X_806, Y_812, Z_817, X1_804, W_189, U_190) | skf18(V_815, X_821, Y_809, Z_810, X1_805, W_189, U_190)=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | skf18(V_803, X_806, Y_812, Z_817, X1_804, 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_819 | skf18(V_815, X_821, Y_809, Z_810, X1_805, W_189, U_190)=X4_819 | skf18(V_803, X_806, Y_812, Z_817, X1_804, W_189, U_190)=X4_819 | X4_819=U_818 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_818 | skf18(V_815, X_821, Y_809, Z_810, X1_805, W_189, U_190)=U_818 | skf18(V_803, X_806, Y_812, Z_817, X1_804, W_189, U_190)=U_818 | ~member(U_190, X4_819, W_189) | ~member(U_190, U_818, W_189) | skf18(U_818, V_808, W_820, X_813, Y_811, Z_807, X1_823)!=U_818 | Z_817=X1_804 | Z_817=Y_812 | Y_812=X1_804 | Y_812=X_806 | Z_817=X_806 | X_806=X1_804 | X_806=V_803 | Y_812=V_803 | Z_817=V_803 | X1_804=V_803 | ~member(U_190, X1_804, W_189) | ~member(U_190, Z_817, W_189) | ~member(U_190, Y_812, W_189) | ~member(U_190, X_806, W_189) | ~member(U_190, V_803, W_189) | Z_810=X1_805 | Z_810=Y_809 | Y_809=X1_805 | Y_809=X_821 | Z_810=X_821 | X_821=X1_805 | X_821=V_815 | Y_809=V_815 | Z_810=V_815 | X1_805=V_815 | ~member(U_190, X1_805, W_189) | ~member(U_190, Z_810, W_189) | ~member(U_190, Y_809, W_189) | ~member(U_190, X_821, W_189) | ~member(U_190, V_815, 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)))). % 15.17/8.18 tff(c_1484, plain, (![X1_706, V_195, Y_716, U_718, U_190, W_189, X_708, X1_192, W_707, V_719, Y_709, V_711, Y_194, Z_710, Z_191, Z_713, X_193, X1_712]: (skf18(V_719, X_708, Y_716, Z_713, 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_707 | skf18(V_719, X_708, Y_716, Z_713, X1_706, W_189, U_190)=W_707 | W_707=V_711 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_711 | skf18(V_719, X_708, Y_716, Z_713, X1_706, W_189, U_190)=V_711 | V_711=U_718 | W_707=U_718 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_718 | skf18(V_719, X_708, Y_716, Z_713, X1_706, W_189, U_190)=U_718 | ~member(U_190, W_707, W_189) | ~member(U_190, V_711, W_189) | ~member(U_190, U_718, W_189) | skf18(U_718, V_711, W_707, skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190), Y_709, Z_710, X1_712)!=skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190) | Z_713=X1_706 | Z_713=Y_716 | Y_716=X1_706 | Y_716=X_708 | Z_713=X_708 | X_708=X1_706 | X_708=V_719 | Y_716=V_719 | Z_713=V_719 | X1_706=V_719 | ~member(U_190, X1_706, W_189) | ~member(U_190, Z_713, W_189) | ~member(U_190, Y_716, W_189) | ~member(U_190, X_708, 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)))). % 15.17/8.18 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)))). % 15.17/8.18 tff(c_1503, plain, (![V_195, W_725, U_190, W_189, X1_192, Y_729, U_733, V_722, X_721, X_723, X1_734, Y_194, V_732, Y_730, Z_191, Z_735, X_193, X1_720, X4_726, Z_727]: (skf18(V_732, X_723, Y_729, Z_727, X1_720, 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_726 | skf18(V_732, X_723, Y_729, Z_727, X1_720, W_189, U_190)=X4_726 | X4_726=V_722 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_722 | skf18(V_732, X_723, Y_729, Z_727, X1_720, W_189, U_190)=V_722 | V_722=U_733 | X4_726=U_733 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_733 | skf18(V_732, X_723, Y_729, Z_727, X1_720, W_189, U_190)=U_733 | ~member(U_190, X4_726, W_189) | ~member(U_190, V_722, W_189) | ~member(U_190, U_733, W_189) | skf18(U_733, V_722, W_725, X_721, Y_730, Z_735, X1_734)!=V_722 | Z_727=X1_720 | Z_727=Y_729 | Y_729=X1_720 | Y_729=X_723 | Z_727=X_723 | X_723=X1_720 | X_723=V_732 | Y_729=V_732 | Z_727=V_732 | X1_720=V_732 | ~member(U_190, X1_720, W_189) | ~member(U_190, Z_727, W_189) | ~member(U_190, Y_729, W_189) | ~member(U_190, X_723, W_189) | ~member(U_190, V_732, 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)))). % 15.17/8.18 tff(c_1522, plain, (![Z_750, X1_739, V_195, U_190, W_189, X1_192, X_741, V_737, X1_736, V_749, U_748, Z_744, Y_743, W_738, Y_194, X_740, Z_191, X_193, Y_746]: (skf18(V_749, X_741, Y_746, Z_744, X1_736, 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_738 | skf18(V_749, X_741, Y_746, Z_744, X1_736, W_189, U_190)=W_738 | W_738=V_737 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=V_737 | skf18(V_749, X_741, Y_746, Z_744, X1_736, W_189, U_190)=V_737 | V_737=U_748 | W_738=U_748 | skf18(V_195, X_193, Y_194, Z_191, X1_192, W_189, U_190)=U_748 | skf18(V_749, X_741, Y_746, Z_744, X1_736, W_189, U_190)=U_748 | ~member(U_190, W_738, W_189) | ~member(U_190, V_737, W_189) | ~member(U_190, U_748, W_189) | skf18(U_748, V_737, W_738, X_740, Y_743, Z_750, X1_739)!=W_738 | Z_744=X1_736 | Z_744=Y_746 | Y_746=X1_736 | Y_746=X_741 | Z_744=X_741 | X_741=X1_736 | X_741=V_749 | Y_746=V_749 | Z_744=V_749 | X1_736=V_749 | ~member(U_190, X1_736, W_189) | ~member(U_190, Z_744, W_189) | ~member(U_190, Y_746, W_189) | ~member(U_190, X_741, W_189) | ~member(U_190, V_749, 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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)))). % 15.17/8.18 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))). % 15.17/8.18 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))). % 15.17/8.18 tff(c_1243, plain, (![W_598]: (skc10=W_598 | ~forename(skc6, W_598) | ~of(skc6, W_598, skc11)))). % 15.17/8.18 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))). % 15.17/8.18 tff(c_1369, plain, (~member(skc6, skc10, skc7))). % 15.17/8.18 tff(c_1219, plain, (![U_218]: (~agent(skc6, skf7(U_218), U_218) | ~member(skc6, U_218, skc7)))). % 15.17/8.18 tff(c_1363, plain, (~act(skc6, skc9))). % 15.17/8.18 tff(c_1301, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.18 tff(c_1256, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.18 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))). % 15.17/8.18 tff(c_1132, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 15.17/8.18 tff(c_1118, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 15.17/8.18 tff(c_1307, plain, (~food(skc6, skc11))). % 15.17/8.18 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))). % 15.17/8.18 tff(c_1047, plain, (![U_245, V_246]: (~food(U_245, V_246) | ~human_person(U_245, V_246)))). % 15.17/8.18 tff(c_1081, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 15.17/8.18 tff(c_1293, plain, (~abstraction(skc6, skc9))). % 15.17/8.18 tff(c_1056, plain, (![U_561, V_562]: (~abstraction(U_561, V_562) | ~beverage(U_561, V_562)))). % 15.17/8.18 tff(c_1262, plain, (~animate(skc6, skc9))). % 15.17/8.18 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)))). % 15.17/8.18 tff(c_1066, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.18 tff(c_1082, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 15.17/8.18 tff(c_1034, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 15.17/8.18 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)))). % 15.17/8.18 tff(c_1013, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 15.17/8.18 tff(c_1035, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 15.17/8.18 tff(c_1227, plain, (~beverage(skc6, skc11))). % 15.17/8.18 tff(c_933, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.18 tff(c_1222, plain, (~agent(skc6, skc8, skc9))). % 15.17/8.18 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)))). % 15.17/8.18 tff(c_1209, plain, (abstraction(skc6, skf13(skc7, skc6)))). % 15.17/8.18 tff(c_1205, plain, (cash(skc6, skf13(skc7, skc6)))). % 15.17/8.18 tff(c_1201, plain, (dollar(skc6, skf13(skc7, skc6)))). % 15.17/8.18 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf13(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 15.17/8.18 tff(c_1193, plain, (abstraction(skc6, skf9(skc7, skc6)))). % 15.17/8.18 tff(c_1173, plain, (abstraction(skc6, skf17(skc7, skc6)))). % 15.17/8.18 tff(c_1177, plain, (abstraction(skc6, skf11(skc7, skc6)))). % 15.17/8.18 tff(c_1189, plain, (cash(skc6, skf9(skc7, skc6)))). % 15.17/8.18 tff(c_1185, plain, (dollar(skc6, skf9(skc7, skc6)))). % 15.17/8.18 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf9(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 15.17/8.18 tff(c_1169, plain, (cash(skc6, skf11(skc7, skc6)))). % 15.17/8.18 tff(c_1157, plain, (cash(skc6, skf17(skc7, skc6)))). % 15.17/8.18 tff(c_1165, plain, (dollar(skc6, skf11(skc7, skc6)))). % 15.17/8.18 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf11(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 15.17/8.18 tff(c_1141, plain, (dollar(skc6, skf17(skc7, skc6)))). % 15.17/8.18 tff(c_1153, plain, (~cost(skc6, skc7))). % 15.17/8.18 tff(c_1152, plain, (~act(skc6, skc7))). % 15.17/8.18 tff(c_1145, plain, (~event(skc6, skc7))). % 15.17/8.18 tff(c_1133, plain, (~eventuality(skc6, skc7))). % 15.17/8.18 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf17(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 15.17/8.18 tff(c_989, plain, (![U_309, V_310]: (~eventuality(U_309, V_310) | ~group(U_309, V_310)))). % 15.17/8.18 tff(c_1124, plain, (skf9(skc7, skc6)!=skf11(skc7, skc6))). % 15.17/8.18 tff(c_1119, plain, (~abstraction(skc6, skc7))). % 15.17/8.18 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf9(U_135, V_136)!=skf11(U_135, V_136)))). % 15.17/8.18 tff(c_999, plain, (![U_309, V_310]: (~abstraction(U_309, V_310) | ~group(U_309, V_310)))). % 15.17/8.18 tff(c_1103, plain, (skf13(skc7, skc6)!=skf11(skc7, skc6))). % 15.17/8.18 tff(c_1098, plain, (![V_220]: (agent(skc6, skf7(V_220), skc10)))). % 15.17/8.18 tff(c_1108, plain, (![V_572]: (~beverage(skc6, skf7(V_572))))). % 15.17/8.18 tff(c_1080, plain, (![V_217]: (~entity(skc6, skf7(V_217))))). % 15.17/8.18 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf13(U_133, V_134)!=skf11(U_133, V_134)))). % 15.17/8.19 tff(c_1087, plain, (~beverage(skc6, skc8))). % 15.17/8.19 tff(c_1083, plain, (~entity(skc6, skc8))). % 15.17/8.19 tff(c_969, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 15.17/8.19 tff(c_954, plain, (![U_526, V_527]: (~animate(U_526, V_527) | ~food(U_526, V_527)))). % 15.17/8.19 tff(c_1061, plain, (skf17(skc7, skc6)!=skf11(skc7, skc6))). % 15.17/8.19 tff(c_1055, plain, (~beverage(skc6, skc7))). % 15.17/8.19 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf17(U_119, V_120)!=skf11(U_119, V_120)))). % 15.17/8.19 tff(c_994, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.19 tff(c_953, plain, (![U_526, V_527]: (~living(U_526, V_527) | ~food(U_526, V_527)))). % 15.17/8.19 tff(c_1042, plain, (skf15(skc7, skc6)!=skf13(skc7, skc6))). % 15.17/8.19 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf15(U_129, V_130)!=skf13(U_129, V_130)))). % 15.17/8.19 tff(c_1033, plain, (![V_217]: (~abstraction(skc6, skf7(V_217))))). % 15.17/8.19 tff(c_1036, plain, (~abstraction(skc6, skc8))). % 15.17/8.19 tff(c_974, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 15.17/8.19 tff(c_1019, plain, (skf9(skc7, skc6)!=skf13(skc7, skc6))). % 15.17/8.19 tff(c_1014, plain, (~entity(skc6, skc7))). % 15.17/8.19 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf9(U_131, V_132)!=skf13(U_131, V_132)))). % 15.17/8.19 tff(c_984, plain, (![U_309, V_310]: (~entity(U_309, V_310) | ~group(U_309, V_310)))). % 15.17/8.19 tff(c_601, plain, (![U_409, V_410]: (impartial(U_409, V_410) | ~food(U_409, V_410)))). % 15.17/8.19 tff(c_1004, plain, (skf17(skc7, skc6)!=skf13(skc7, skc6))). % 15.17/8.19 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf17(U_121, V_122)!=skf13(U_121, V_122)))). % 15.17/8.19 tff(c_369, plain, (![U_332, V_333]: (~multiple(U_332, V_333) | ~abstraction(U_332, V_333)))). % 15.17/8.19 tff(c_600, plain, (![U_409, V_410]: (entity(U_409, V_410) | ~food(U_409, V_410)))). % 15.17/8.19 tff(c_898, plain, (![U_508, V_509]: (~multiple(U_508, V_509) | ~eventuality(U_508, V_509)))). % 15.17/8.19 tff(c_489, plain, (![U_373, V_374]: (~multiple(U_373, V_374) | ~entity(U_373, V_374)))). % 15.17/8.19 tff(c_979, plain, (skf9(skc7, skc6)!=skf17(skc7, skc6))). % 15.17/8.19 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf9(U_117, V_118)!=skf17(U_117, V_118)))). % 15.17/8.19 tff(c_713, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 15.17/8.19 tff(c_703, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 15.17/8.19 tff(c_964, plain, (skf17(skc7, skc6)!=skf15(skc7, skc6))). % 15.17/8.19 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf17(U_123, V_124)!=skf15(U_123, V_124)))). % 15.17/8.19 tff(c_959, plain, (abstraction(skc6, skf15(skc7, skc6)))). % 15.17/8.19 tff(c_589, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 15.17/8.19 tff(c_602, plain, (![U_409, V_410]: (nonliving(U_409, V_410) | ~food(U_409, V_410)))). % 15.17/8.19 tff(c_945, plain, (cash(skc6, skf15(skc7, skc6)))). % 15.17/8.19 tff(c_941, plain, (dollar(skc6, skf15(skc7, skc6)))). % 15.17/8.19 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf15(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 15.17/8.19 tff(c_913, plain, (![U_49, V_50]: (~female(U_49, V_50) | ~food(U_49, V_50)))). % 15.17/8.19 tff(c_928, plain, (skf9(skc7, skc6)!=skf15(skc7, skc6))). % 15.17/8.19 tff(c_923, plain, (abstraction(skc6, skc10))). % 15.17/8.19 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf9(U_125, V_126)!=skf15(U_125, V_126)))). % 15.17/8.19 tff(c_363, plain, (![U_328, V_329]: (abstraction(U_328, V_329) | ~forename(U_328, V_329)))). % 15.17/8.19 tff(c_607, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 15.17/8.19 tff(c_260, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 15.17/8.19 tff(c_908, plain, (skf15(skc7, skc6)!=skf11(skc7, skc6))). % 15.17/8.19 tff(c_903, plain, (entity(skc6, skc11))). % 15.17/8.19 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf15(U_127, V_128)!=skf11(U_127, V_128)))). % 15.17/8.19 tff(c_291, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 15.17/8.19 tff(c_285, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 15.17/8.19 tff(c_892, plain, (~cost(skc6, skc11))). % 15.17/8.19 tff(c_196, plain, (![U_218]: (patient(skc6, skf7(U_218), U_218) | ~member(skc6, U_218, skc7)))). % 15.17/8.19 tff(c_891, plain, (~act(skc6, skc11))). % 15.17/8.19 tff(c_884, plain, (~event(skc6, skc11))). % 15.17/8.19 tff(c_880, plain, (~eventuality(skc6, skc11))). % 15.17/8.19 tff(c_261, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 15.17/8.19 tff(c_874, plain, (![V_217]: (event(skc6, skf7(V_217))))). % 15.17/8.19 tff(c_227, plain, (![U_245, V_246]: (impartial(U_245, V_246) | ~human_person(U_245, V_246)))). % 15.17/8.19 tff(c_296, plain, (![U_293, V_294]: (~general(U_293, V_294) | ~eventuality(U_293, V_294)))). % 15.17/8.19 tff(c_320, plain, (![U_307, V_308]: (~female(U_307, V_308) | ~abstraction(U_307, V_308)))). % 15.17/8.19 tff(c_314, plain, (![U_35, V_36]: (~existent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 15.17/8.19 tff(c_697, plain, (![V_213]: (nonreflexive(skc6, skf7(V_213))))). % 15.17/8.19 tff(c_228, plain, (![U_245, V_246]: (living(U_245, V_246) | ~human_person(U_245, V_246)))). % 15.17/8.19 tff(c_266, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 15.17/8.19 tff(c_249, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 15.17/8.19 tff(c_342, plain, (![U_319, V_320]: (abstraction(U_319, V_320) | ~currency(U_319, V_320)))). % 15.17/8.19 tff(c_583, plain, (![V_211]: (cost(skc6, skf7(V_211))))). % 15.17/8.19 tff(c_494, plain, (~abstraction(skc6, skc11))). % 15.17/8.19 tff(c_336, plain, (![U_15, V_16]: (~human(U_15, V_16) | ~abstraction(U_15, V_16)))). % 15.17/8.19 tff(c_284, plain, (![U_55, V_56]: (singleton(U_55, V_56) | ~entity(U_55, V_56)))). % 15.17/8.19 tff(c_483, plain, (![V_371]: (~past(skc6, skf7(V_371))))). % 15.17/8.19 tff(c_478, plain, (![V_215]: (present(skc6, skf7(V_215))))). % 15.17/8.19 tff(c_347, plain, (![U_321, V_322]: (singleton(U_321, V_322) | ~abstraction(U_321, V_322)))). % 15.17/8.19 tff(c_325, plain, (![U_309, V_310]: (multiple(U_309, V_310) | ~group(U_309, V_310)))). % 15.17/8.19 tff(c_357, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 15.17/8.19 tff(c_186, plain, (![U_209]: (dollar(skc6, U_209) | ~member(skc6, U_209, skc7)))). % 15.17/8.19 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 15.17/8.19 tff(c_352, plain, (act(skc6, skc8))). % 15.17/8.19 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 15.17/8.19 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 15.17/8.19 tff(c_337, plain, (~human(skc6, skc10))). % 15.17/8.19 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 15.17/8.19 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 15.17/8.19 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 15.17/8.19 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 15.17/8.19 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 15.17/8.19 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 15.17/8.19 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 15.17/8.19 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 15.17/8.19 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 15.17/8.19 tff(c_308, plain, (human(skc6, skc11))). % 15.17/8.19 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 15.17/8.19 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 15.17/8.19 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 15.17/8.19 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 15.17/8.19 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 15.17/8.19 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 15.17/8.19 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 15.17/8.19 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 15.17/8.19 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 15.17/8.19 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 15.17/8.19 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 15.17/8.19 tff(c_273, plain, (beverage(skc6, skc9))). % 15.17/8.20 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 15.17/8.20 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 15.17/8.20 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 15.17/8.20 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 15.17/8.20 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 15.17/8.20 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 15.17/8.20 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 15.17/8.20 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 15.17/8.20 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 15.17/8.20 tff(c_244, plain, (animate(skc6, skc11))). % 15.17/8.20 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 15.17/8.20 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 15.17/8.20 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 15.17/8.20 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 15.17/8.20 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 15.17/8.20 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 15.17/8.20 tff(c_234, plain, (female(skc6, skc11))). % 15.17/8.20 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 15.17/8.20 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 15.17/8.20 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 15.17/8.20 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 15.17/8.20 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 15.17/8.20 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 15.17/8.20 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 15.17/8.20 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 15.17/8.20 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 15.17/8.20 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 15.17/8.20 tff(c_211, plain, (human_person(skc6, skc11))). % 15.17/8.20 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 15.17/8.20 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 15.17/8.20 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 15.17/8.20 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 15.17/8.20 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 15.17/8.20 tff(c_180, plain, (of(skc6, skc10, skc11))). % 15.17/8.20 tff(c_182, plain, (agent(skc6, skc8, skc11))). % 15.17/8.20 tff(c_184, plain, (patient(skc6, skc8, skc9))). % 15.17/8.20 tff(c_160, plain, (shake_beverage(skc6, skc9))). % 15.17/8.20 tff(c_158, plain, (woman(skc6, skc11))). % 15.17/8.20 tff(c_176, plain, (five(skc6, skc7))). % 15.17/8.20 tff(c_174, plain, (nonhuman(skc6, skc10))). % 15.17/8.20 tff(c_172, plain, (mia_forename(skc6, skc10))). % 15.17/8.20 tff(c_170, plain, (forename(skc6, skc10))). % 15.17/8.20 tff(c_168, plain, (event(skc6, skc8))). % 15.17/8.20 tff(c_162, plain, (order(skc6, skc8))). % 15.17/8.20 tff(c_164, plain, (nonreflexive(skc6, skc8))). % 15.17/8.20 tff(c_166, plain, (past(skc6, skc8))). % 15.17/8.20 tff(c_178, plain, (group(skc6, skc7))). % 15.17/8.20 tff(c_156, plain, (actual_world(skc6))). % 15.17/8.20 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.17/8.20 %------------------------------------------------------------------------------