%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP220-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 : n031.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:39 PM UTC 2025 % Result : Satisfiable 11.14s 4.01s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.10 % Problem : NLP220-1 : TPTP v9.0.0. Released v2.4.0. % 0.06/0.11 % 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.11/0.31 % Computer : n031.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 09:26:22 EDT 2025 % 0.11/0.32 % CPUTime : % 11.14/4.01 % 11.14/4.01 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.14/4.01 % 11.14/4.01 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.14/4.02 %$ theme > of > agent > vincent_forename > unisex > think_believe_consider > thing > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > actual_world > #nlpp > skf1 > skc9 > skc8 > skc7 > skc6 > skc5 % 11.14/4.02 % 11.14/4.02 %Foreground sorts: % 11.14/4.02 % 11.14/4.02 % 11.14/4.02 %Background operators: % 11.14/4.02 % 11.14/4.02 % 11.14/4.02 %Foreground operators: % 11.14/4.02 tff(relation, type, relation: ($i * $i) > $o). % 11.14/4.02 tff(forename, type, forename: ($i * $i) > $o). % 11.14/4.02 tff(skc7, type, skc7: $i). % 11.14/4.02 tff(theme, type, theme: ($i * $i * $i) > $o). % 11.14/4.02 tff(living, type, living: ($i * $i) > $o). % 11.14/4.02 tff(human_person, type, human_person: ($i * $i) > $o). % 11.14/4.02 tff(present, type, present: ($i * $i) > $o). % 11.14/4.02 tff(entity, type, entity: ($i * $i) > $o). % 11.14/4.02 tff(skc9, type, skc9: $i). % 11.14/4.02 tff(eventuality, type, eventuality: ($i * $i) > $o). % 11.14/4.02 tff(existent, type, existent: ($i * $i) > $o). % 11.14/4.02 tff(abstraction, type, abstraction: ($i * $i) > $o). % 11.14/4.02 tff(skf1, type, skf1: $i > $i). % 11.14/4.02 tff(skc8, type, skc8: $i). % 11.14/4.02 tff(proposition, type, proposition: ($i * $i) > $o). % 11.14/4.02 tff(relname, type, relname: ($i * $i) > $o). % 11.14/4.02 tff(singleton, type, singleton: ($i * $i) > $o). % 11.14/4.02 tff(male, type, male: ($i * $i) > $o). % 11.14/4.02 tff(organism, type, organism: ($i * $i) > $o). % 11.14/4.02 tff(animate, type, animate: ($i * $i) > $o). % 11.14/4.02 tff(of, type, of: ($i * $i * $i) > $o). % 11.14/4.02 tff(actual_world, type, actual_world: $i > $o). % 11.14/4.02 tff(agent, type, agent: ($i * $i * $i) > $o). % 11.14/4.02 tff(general, type, general: ($i * $i) > $o). % 11.14/4.02 tff(smoke, type, smoke: ($i * $i) > $o). % 11.14/4.02 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 11.14/4.02 tff(event, type, event: ($i * $i) > $o). % 11.14/4.02 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 11.14/4.02 tff(thing, type, thing: ($i * $i) > $o). % 11.14/4.02 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 11.14/4.02 tff(human, type, human: ($i * $i) > $o). % 11.14/4.02 tff(man, type, man: ($i * $i) > $o). % 11.14/4.02 tff(skc5, type, skc5: $i). % 11.14/4.02 tff(unisex, type, unisex: ($i * $i) > $o). % 11.14/4.02 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 11.14/4.02 tff(skc6, type, skc6: $i). % 11.14/4.02 tff(impartial, type, impartial: ($i * $i) > $o). % 11.14/4.02 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 11.14/4.02 tff(specific, type, specific: ($i * $i) > $o). % 11.14/4.02 % 11.14/4.02 %Saturated clause set: % 11.14/4.03 tff(c_3028, plain, (![V_1123, V_766]: (skc6=V_1123 | ~think_believe_consider(V_766, skc7) | ~think_believe_consider(V_766, skf1(skc9)) | ~theme(V_766, skf1(skc9), V_1123) | ~proposition(V_766, skc6) | ~proposition(V_766, V_1123) | ~accessible_world(skc6, V_766) | ~accessible_world(skc5, V_766)))). % 11.14/4.03 tff(c_3016, plain, (![W_1115, V_1113, V_774]: (W_1115=V_1113 | ~theme(V_774, skc7, W_1115) | ~think_believe_consider(V_774, skc7) | ~think_believe_consider(V_774, skf1(skc9)) | ~theme(V_774, skf1(skc9), V_1113) | ~proposition(V_774, W_1115) | ~proposition(V_774, V_1113) | ~accessible_world(skc6, V_774) | ~accessible_world(skc5, V_774)))). % 11.14/4.03 tff(c_3021, plain, (~accessible_world(skc6, skc5))). % 11.14/4.03 tff(c_3013, plain, (![W_1115, V_1113, V_774, U_175]: (W_1115=V_1113 | ~theme(V_774, skf1(U_175), W_1115) | ~think_believe_consider(V_774, skf1(U_175)) | ~theme(V_774, skf1(U_175), V_1113) | ~proposition(V_774, W_1115) | ~proposition(V_774, V_1113) | ~accessible_world(skc6, V_774) | ~man(skc6, U_175)))). % 11.14/4.03 tff(c_2074, plain, (![Y_167, W_163, V_868, U_869, V_168]: (W_163=V_168 | ~agent(V_868, Y_167, U_869) | ~theme(V_868, Y_167, W_163) | ~think_believe_consider(V_868, Y_167) | ~think_believe_consider(V_868, skf1(U_869)) | ~theme(V_868, skf1(U_869), V_168) | ~proposition(V_868, W_163) | ~proposition(V_868, V_168) | ~accessible_world(skc6, V_868) | ~man(skc6, U_869)))). % 11.14/4.03 tff(c_2988, plain, (![V_1108, V_766]: (skc6=V_1108 | ~agent(V_766, skc7, skc9) | ~think_believe_consider(V_766, skc7) | ~theme(V_766, skc7, V_1108) | ~proposition(V_766, skc6) | ~proposition(V_766, V_1108) | ~accessible_world(skc5, V_766)))). % 11.14/4.03 tff(c_1710, plain, (![W_796, V_794, V_774, Y_798]: (W_796=V_794 | ~agent(V_774, Y_798, skc9) | ~theme(V_774, Y_798, W_796) | ~think_believe_consider(V_774, Y_798) | ~think_believe_consider(V_774, skc7) | ~theme(V_774, skc7, V_794) | ~proposition(V_774, W_796) | ~proposition(V_774, V_794) | ~accessible_world(skc5, V_774)))). % 11.14/4.03 tff(c_2918, plain, (![V_115, V_1091]: (animate(V_115, skc9) | ~accessible_world(V_1091, V_115) | ~accessible_world(skc6, V_1091)))). % 11.14/4.03 tff(c_2950, plain, (![V_112, V_1093]: (human(V_112, skc9) | ~accessible_world(V_1093, V_112) | ~accessible_world(skc6, V_1093)))). % 11.14/4.03 tff(c_2886, plain, (![V_118, V_1089]: (male(V_118, skc9) | ~accessible_world(V_1089, V_118) | ~accessible_world(skc6, V_1089)))). % 11.14/4.03 tff(c_2911, plain, (![V_94, V_1090]: (human_person(V_94, skc9) | ~accessible_world(V_1090, V_94) | ~accessible_world(skc6, V_1090)))). % 11.14/4.03 tff(c_2858, plain, (![V_121, V_1088]: (think_believe_consider(V_121, skc7) | ~accessible_world(V_1088, V_121) | ~accessible_world(skc6, V_1088)))). % 11.14/4.03 tff(c_2851, plain, (![V_91, V_1087]: (man(V_91, skc9) | ~accessible_world(V_1087, V_91) | ~accessible_world(skc6, V_1087)))). % 11.14/4.03 tff(c_2934, plain, (![U_3]: (~accessible_world(skc6, U_3) | ~event(U_3, skc9)))). % 11.14/4.03 tff(c_2828, plain, (![V_112]: (human(V_112, skc9) | ~accessible_world(skc6, V_112)))). % 11.14/4.03 tff(c_2888, plain, (![V_1089]: (~eventuality(V_1089, skc9) | ~accessible_world(skc6, V_1089)))). % 11.14/4.03 tff(c_2914, plain, (![V_1090]: (animate(V_1090, skc9) | ~accessible_world(skc6, V_1090)))). % 11.14/4.03 tff(c_2780, plain, (![V_94]: (human_person(V_94, skc9) | ~accessible_world(skc6, V_94)))). % 11.14/4.03 tff(c_2809, plain, (![V_118]: (male(V_118, skc9) | ~accessible_world(skc6, V_118)))). % 11.14/4.03 tff(c_2768, plain, (![V_121]: (think_believe_consider(V_121, skc7) | ~accessible_world(skc6, V_121)))). % 11.14/4.03 tff(c_2854, plain, (~think_believe_consider(skc6, skf1(skc9)))). % 11.14/4.03 tff(c_2753, plain, (![V_91]: (man(V_91, skc9) | ~accessible_world(skc6, V_91)))). % 11.14/4.03 tff(c_2841, plain, (~event(skc6, skc9))). % 11.14/4.03 tff(c_2811, plain, (~eventuality(skc6, skc9))). % 11.14/4.03 tff(c_2783, plain, (human(skc6, skc9))). % 11.14/4.03 tff(c_2784, plain, (animate(skc6, skc9))). % 11.14/4.03 tff(c_2755, plain, (male(skc6, skc9))). % 11.14/4.04 tff(c_2754, plain, (human_person(skc6, skc9))). % 11.14/4.04 tff(c_2765, plain, (think_believe_consider(skc6, skc7))). % 11.14/4.04 tff(c_2744, plain, (man(skc6, skc9))). % 11.14/4.04 tff(c_2196, plain, (![W_909, V_910, U_175]: (W_909=V_910 | ~theme(skc6, skf1(U_175), W_909) | ~think_believe_consider(skc6, skf1(U_175)) | ~theme(skc6, skf1(U_175), V_910) | ~proposition(skc6, W_909) | ~proposition(skc6, V_910) | ~man(skc6, U_175)))). % 11.14/4.04 tff(c_2485, plain, (![V_109, V_976, V_975]: (living(V_109, V_976) | ~accessible_world(V_975, V_109) | ~accessible_world(skc6, V_975) | ~human_person(skc5, V_976)))). % 11.14/4.04 tff(c_2376, plain, (![V_76, V_946, V_945]: (singleton(V_76, V_946) | ~accessible_world(V_945, V_76) | ~accessible_world(skc6, V_945) | ~abstraction(skc5, V_946)))). % 11.14/4.04 tff(c_2480, plain, (![V_127, V_974, V_973]: (relation(V_127, V_974) | ~accessible_world(V_973, V_127) | ~accessible_world(skc6, V_973) | ~forename(skc5, V_974)))). % 11.14/4.04 tff(c_2528, plain, (![V_76, V_986, V_985]: (singleton(V_76, V_986) | ~accessible_world(V_985, V_76) | ~accessible_world(skc6, V_985) | ~entity(skc5, V_986)))). % 11.14/4.04 tff(c_2424, plain, (![V_76, V_957, V_956]: (singleton(V_76, V_957) | ~accessible_world(V_956, V_76) | ~accessible_world(skc6, V_956) | ~eventuality(skc5, V_957)))). % 11.14/4.04 tff(c_1662, plain, (![W_781, V_760]: (skc8=W_781 | ~entity(V_760, skc9) | ~forename(V_760, W_781) | ~of(V_760, W_781, skc9) | ~forename(V_760, skc8) | ~accessible_world(skc5, V_760)))). % 11.14/4.04 tff(c_2489, plain, (![V_106, V_978, V_977]: (impartial(V_106, V_978) | ~accessible_world(V_977, V_106) | ~accessible_world(skc6, V_977) | ~human_person(skc5, V_978)))). % 11.14/4.04 tff(c_2371, plain, (![V_85, V_944, V_943]: (unisex(V_85, V_944) | ~accessible_world(V_943, V_85) | ~accessible_world(skc6, V_943) | ~eventuality(skc5, V_944)))). % 11.14/4.04 tff(c_2355, plain, (![V_127, V_938, V_937]: (relation(V_127, V_938) | ~accessible_world(V_937, V_127) | ~accessible_world(skc6, V_937) | ~proposition(skc5, V_938)))). % 11.40/4.04 tff(c_2255, plain, (![V_97, V_922, V_921]: (organism(V_97, V_922) | ~accessible_world(V_921, V_97) | ~accessible_world(skc6, V_921) | ~human_person(skc5, V_922)))). % 11.40/4.04 tff(c_2224, plain, (![V_136, V_916, V_915]: (general(V_136, V_916) | ~accessible_world(V_915, V_136) | ~accessible_world(skc6, V_915) | ~abstraction(skc5, V_916)))). % 11.40/4.04 tff(c_2278, plain, (![V_133, V_926, V_925]: (nonhuman(V_133, V_926) | ~accessible_world(V_925, V_133) | ~accessible_world(skc6, V_925) | ~abstraction(skc5, V_926)))). % 11.40/4.04 tff(c_2339, plain, (![V_82, V_934, V_933]: (nonexistent(V_82, V_934) | ~accessible_world(V_933, V_82) | ~accessible_world(skc6, V_933) | ~eventuality(skc5, V_934)))). % 11.40/4.04 tff(c_2270, plain, (![V_103, V_924, V_923]: (existent(V_103, V_924) | ~accessible_world(V_923, V_103) | ~accessible_world(skc6, V_923) | ~entity(skc5, V_924)))). % 11.40/4.04 tff(c_2241, plain, (![V_79, V_920, V_919]: (specific(V_79, V_920) | ~accessible_world(V_919, V_79) | ~accessible_world(skc6, V_919) | ~eventuality(skc5, V_920)))). % 11.40/4.04 tff(c_2075, plain, (![V_148, U_869, V_868]: (agent(V_148, skf1(U_869), U_869) | ~accessible_world(V_868, V_148) | ~accessible_world(skc6, V_868) | ~man(skc6, U_869)))). % 11.40/4.04 tff(c_2173, plain, (![V_142, V_906, V_905]: (relname(V_142, V_906) | ~accessible_world(V_905, V_142) | ~accessible_world(skc6, V_905) | ~forename(skc5, V_906)))). % 11.40/4.04 tff(c_2316, plain, (![V_70, V_928, V_927]: (eventuality(V_70, V_928) | ~accessible_world(V_927, V_70) | ~accessible_world(skc6, V_927) | ~event(skc5, V_928)))). % 11.40/4.04 tff(c_2233, plain, (![V_73, V_918, V_917]: (thing(V_73, V_918) | ~accessible_world(V_917, V_73) | ~accessible_world(skc6, V_917) | ~eventuality(skc5, V_918)))). % 11.40/4.04 tff(c_2181, plain, (![V_73, V_908, V_907]: (thing(V_73, V_908) | ~accessible_world(V_907, V_73) | ~accessible_world(skc6, V_907) | ~entity(skc5, V_908)))). % 11.40/4.04 tff(c_2347, plain, (![V_73, V_936, V_935]: (thing(V_73, V_936) | ~accessible_world(V_935, V_73) | ~accessible_world(skc6, V_935) | ~abstraction(skc5, V_936)))). % 11.40/4.04 tff(c_2327, plain, (![V_85, V_930, V_929]: (unisex(V_85, V_930) | ~accessible_world(V_929, V_85) | ~accessible_world(skc6, V_929) | ~abstraction(skc5, V_930)))). % 11.40/4.05 tff(c_2203, plain, (![V_79, V_914, V_913]: (specific(V_79, V_914) | ~accessible_world(V_913, V_79) | ~accessible_world(skc6, V_913) | ~entity(skc5, V_914)))). % 11.40/4.05 tff(c_1636, plain, (![V_100, V_772]: (entity(V_100, skc9) | ~accessible_world(V_772, V_100) | ~accessible_world(skc6, V_772)))). % 11.40/4.05 tff(c_2515, plain, (![U_3, V_4]: (~accessible_world(skc6, U_3) | ~abstraction(skc5, V_4) | ~event(U_3, V_4)))). % 11.40/4.05 tff(c_1652, plain, (![V_148, V_779]: (agent(V_148, skc7, skc9) | ~accessible_world(V_779, V_148) | ~accessible_world(skc5, V_779)))). % 11.40/4.05 tff(c_2502, plain, (![U_45, V_46]: (~accessible_world(skc6, U_45) | ~eventuality(skc5, V_46) | ~abstraction(U_45, V_46)))). % 11.40/4.05 tff(c_2473, plain, (![U_45, V_46]: (~accessible_world(skc6, U_45) | ~entity(skc5, V_46) | ~abstraction(U_45, V_46)))). % 11.40/4.05 tff(c_2481, plain, (![V_973, V_974]: (abstraction(V_973, V_974) | ~accessible_world(skc6, V_973) | ~forename(skc5, V_974)))). % 11.40/4.05 tff(c_2389, plain, (![U_25, V_26]: (~accessible_world(skc6, U_25) | ~eventuality(skc5, V_26) | ~entity(U_25, V_26)))). % 11.40/4.05 tff(c_2318, plain, (![V_927, V_928]: (~entity(V_927, V_928) | ~accessible_world(skc6, V_927) | ~event(skc5, V_928)))). % 11.40/4.05 tff(c_2450, plain, (![U_3, V_4]: (~accessible_world(skc6, U_3) | ~entity(skc5, V_4) | ~event(U_3, V_4)))). % 11.40/4.05 tff(c_1284, plain, (![V_100, V_658]: (entity(V_100, skc9) | ~accessible_world(V_658, V_100) | ~accessible_world(skc5, V_658)))). % 11.40/4.05 tff(c_1407, plain, (![V_67, V_689, V_688]: (event(V_67, skf1(V_689)) | ~accessible_world(V_688, V_67) | ~accessible_world(skc6, V_688)))). % 11.40/4.05 tff(c_2555, plain, (~event(skc5, skc8))). % 11.40/4.05 tff(c_2554, plain, (~event(skc5, skc6))). % 11.40/4.05 tff(c_2319, plain, (![V_927, V_928]: (~abstraction(V_927, V_928) | ~accessible_world(skc6, V_927) | ~event(skc5, V_928)))). % 11.40/4.05 tff(c_2256, plain, (![V_921, V_922]: (entity(V_921, V_922) | ~accessible_world(skc6, V_921) | ~human_person(skc5, V_922)))). % 11.40/4.05 tff(c_1648, plain, (![V_152, V_778]: (theme(V_152, skc7, skc6) | ~accessible_world(V_778, V_152) | ~accessible_world(skc5, V_778)))). % 11.40/4.05 tff(c_2182, plain, (![V_907, V_908]: (singleton(V_907, V_908) | ~accessible_world(skc6, V_907) | ~entity(skc5, V_908)))). % 11.40/4.05 tff(c_2328, plain, (![V_929, V_930]: (~male(V_929, V_930) | ~accessible_world(skc6, V_929) | ~abstraction(skc5, V_930)))). % 11.40/4.05 tff(c_2225, plain, (![V_915, V_916]: (~eventuality(V_915, V_916) | ~accessible_world(skc6, V_915) | ~abstraction(skc5, V_916)))). % 11.40/4.05 tff(c_2242, plain, (![V_919, V_920]: (~general(V_919, V_920) | ~accessible_world(skc6, V_919) | ~eventuality(skc5, V_920)))). % 11.40/4.05 tff(c_2257, plain, (![V_921, V_922]: (impartial(V_921, V_922) | ~accessible_world(skc6, V_921) | ~human_person(skc5, V_922)))). % 11.40/4.05 tff(c_2258, plain, (![V_921, V_922]: (living(V_921, V_922) | ~accessible_world(skc6, V_921) | ~human_person(skc5, V_922)))). % 11.40/4.05 tff(c_2174, plain, (![V_905, V_906]: (relation(V_905, V_906) | ~accessible_world(skc6, V_905) | ~forename(skc5, V_906)))). % 11.40/4.05 tff(c_2204, plain, (![V_913, V_914]: (~general(V_913, V_914) | ~accessible_world(skc6, V_913) | ~entity(skc5, V_914)))). % 11.40/4.05 tff(c_1416, plain, (![V_64, V_691, V_690]: (smoke(V_64, skf1(V_691)) | ~accessible_world(V_690, V_64) | ~accessible_world(skc6, V_690)))). % 11.40/4.05 tff(c_1288, plain, (![V_115, V_659]: (animate(V_115, skc9) | ~accessible_world(V_659, V_115) | ~accessible_world(skc5, V_659)))). % 11.40/4.05 tff(c_2356, plain, (![V_937, V_938]: (abstraction(V_937, V_938) | ~accessible_world(skc6, V_937) | ~proposition(skc5, V_938)))). % 11.40/4.05 tff(c_2271, plain, (![V_923, V_924]: (~eventuality(V_923, V_924) | ~accessible_world(skc6, V_923) | ~entity(skc5, V_924)))). % 11.40/4.05 tff(c_1488, plain, (![V_717, V_669]: (human(V_717, skc9) | ~accessible_world(V_669, V_717) | ~accessible_world(skc5, V_669)))). % 11.40/4.05 tff(c_2279, plain, (![V_925, V_926]: (~human(V_925, V_926) | ~accessible_world(skc6, V_925) | ~abstraction(skc5, V_926)))). % 11.40/4.05 tff(c_2234, plain, (![V_917, V_918]: (singleton(V_917, V_918) | ~accessible_world(skc6, V_917) | ~eventuality(skc5, V_918)))). % 11.40/4.05 tff(c_2372, plain, (![V_943, V_944]: (~male(V_943, V_944) | ~accessible_world(skc6, V_943) | ~eventuality(skc5, V_944)))). % 11.40/4.05 tff(c_1397, plain, (![V_88, V_687, V_686]: (present(V_88, skf1(V_687)) | ~accessible_world(V_686, V_88) | ~accessible_world(skc6, V_686)))). % 11.40/4.05 tff(c_2226, plain, (![V_915, V_916]: (~entity(V_915, V_916) | ~accessible_world(skc6, V_915) | ~abstraction(skc5, V_916)))). % 11.40/4.06 tff(c_2340, plain, (![V_933, V_934]: (~existent(V_933, V_934) | ~accessible_world(skc6, V_933) | ~eventuality(skc5, V_934)))). % 11.40/4.06 tff(c_1726, plain, (![V_76, V_801]: (singleton(V_76, V_801) | ~accessible_world(skc6, V_76) | ~abstraction(skc5, V_801)))). % 11.40/4.06 tff(c_1785, plain, (![V_85, V_819]: (unisex(V_85, V_819) | ~accessible_world(skc6, V_85) | ~eventuality(skc5, V_819)))). % 11.40/4.06 tff(c_1425, plain, (![V_696, V_667]: (male(V_696, skc9) | ~accessible_world(V_667, V_696) | ~accessible_world(skc5, V_667)))). % 11.40/4.06 tff(c_1466, plain, (![V_709, V_667]: (human_person(V_709, skc9) | ~accessible_world(V_667, V_709) | ~accessible_world(skc5, V_667)))). % 11.40/4.06 tff(c_1561, plain, (![V_127, V_755]: (relation(V_127, V_755) | ~accessible_world(skc6, V_127) | ~proposition(skc5, V_755)))). % 11.40/4.06 tff(c_1721, plain, (![V_73, V_800]: (thing(V_73, V_800) | ~accessible_world(skc6, V_73) | ~abstraction(skc5, V_800)))). % 11.40/4.06 tff(c_1777, plain, (![V_82, V_818]: (nonexistent(V_82, V_818) | ~accessible_world(skc6, V_82) | ~eventuality(skc5, V_818)))). % 11.40/4.06 tff(c_1656, plain, (![V_156, V_780]: (of(V_156, skc8, skc9) | ~accessible_world(V_780, V_156) | ~accessible_world(skc5, V_780)))). % 11.40/4.06 tff(c_1753, plain, (![V_85, V_810]: (unisex(V_85, V_810) | ~accessible_world(skc6, V_85) | ~abstraction(skc5, V_810)))). % 11.40/4.06 tff(c_1843, plain, (![V_70, V_830]: (eventuality(V_70, V_830) | ~accessible_world(skc6, V_70) | ~event(skc5, V_830)))). % 11.40/4.06 tff(c_2019, plain, (![V_133, V_857]: (nonhuman(V_133, V_857) | ~accessible_world(skc6, V_133) | ~abstraction(skc5, V_857)))). % 11.40/4.06 tff(c_1894, plain, (![V_103, V_836]: (existent(V_103, V_836) | ~accessible_world(skc6, V_103) | ~entity(skc5, V_836)))). % 11.40/4.06 tff(c_1595, plain, (![V_97, V_764]: (organism(V_97, V_764) | ~accessible_world(skc6, V_97) | ~human_person(skc5, V_764)))). % 11.40/4.06 tff(c_1961, plain, (![V_79, V_845]: (specific(V_79, V_845) | ~accessible_world(skc6, V_79) | ~eventuality(skc5, V_845)))). % 11.40/4.06 tff(c_2059, plain, (![V_73, V_864]: (thing(V_73, V_864) | ~accessible_world(skc6, V_73) | ~eventuality(skc5, V_864)))). % 11.40/4.06 tff(c_1862, plain, (![V_136, V_831]: (general(V_136, V_831) | ~accessible_world(skc6, V_136) | ~abstraction(skc5, V_831)))). % 11.40/4.06 tff(c_1676, plain, (![V_79, V_788]: (specific(V_79, V_788) | ~accessible_world(skc6, V_79) | ~entity(skc5, V_788)))). % 11.40/4.06 tff(c_1711, plain, (![W_796, V_794, Y_798, U_175]: (W_796=V_794 | ~agent(skc6, Y_798, U_175) | ~theme(skc6, Y_798, W_796) | ~think_believe_consider(skc6, Y_798) | ~think_believe_consider(skc6, skf1(U_175)) | ~theme(skc6, skf1(U_175), V_794) | ~proposition(skc6, W_796) | ~proposition(skc6, V_794) | ~man(skc6, U_175)))). % 11.49/4.06 tff(c_1737, plain, (![V_73, V_805]: (thing(V_73, V_805) | ~accessible_world(skc6, V_73) | ~entity(skc5, V_805)))). % 11.49/4.06 tff(c_2011, plain, (![V_142, V_856]: (relname(V_142, V_856) | ~accessible_world(skc6, V_142) | ~forename(skc5, V_856)))). % 11.49/4.06 tff(c_1508, plain, (![V_145, V_729]: (vincent_forename(V_145, skc8) | ~accessible_world(V_729, V_145) | ~accessible_world(skc5, V_729)))). % 11.49/4.06 tff(c_1385, plain, (![V_678, V_6, U_5]: (singleton(V_678, V_6) | ~accessible_world(U_5, V_678) | ~eventuality(U_5, V_6)))). % 11.49/4.06 tff(c_2127, plain, (![V_887]: (skc6=V_887 | ~theme(skc5, skc7, V_887) | ~proposition(skc5, V_887)))). % 11.49/4.06 tff(c_1314, plain, (![V_91, V_667]: (man(V_91, skc9) | ~accessible_world(V_667, V_91) | ~accessible_world(skc5, V_667)))). % 11.49/4.06 tff(c_1497, plain, (![V_723, V_199, U_198]: (impartial(V_723, V_199) | ~accessible_world(U_198, V_723) | ~human_person(U_198, V_199)))). % 11.49/4.06 tff(c_1550, plain, (![V_749, V_199, U_198]: (living(V_749, V_199) | ~accessible_world(U_198, V_749) | ~human_person(U_198, V_199)))). % 11.49/4.06 tff(c_1320, plain, (![V_88, V_668]: (present(V_88, skc7) | ~accessible_world(V_668, V_88) | ~accessible_world(skc5, V_668)))). % 11.49/4.06 tff(c_1714, plain, (![W_796, V_794, Y_798]: (W_796=V_794 | ~agent(skc5, Y_798, skc9) | ~theme(skc5, Y_798, W_796) | ~think_believe_consider(skc5, Y_798) | ~theme(skc5, skc7, V_794) | ~proposition(skc5, W_796) | ~proposition(skc5, V_794)))). % 11.49/4.06 tff(c_1350, plain, (![V_67, V_673]: (event(V_67, skc7) | ~accessible_world(V_673, V_67) | ~accessible_world(skc5, V_673)))). % 11.49/4.06 tff(c_1665, plain, (![W_781]: (skc8=W_781 | ~forename(skc5, W_781) | ~of(skc5, W_781, skc9)))). % 11.49/4.06 tff(c_1387, plain, (![V_678, V_42, U_41]: (singleton(V_678, V_42) | ~accessible_world(U_41, V_678) | ~abstraction(U_41, V_42)))). % 11.49/4.06 tff(c_1195, plain, (![V_127, V_618, U_617]: (relation(V_127, V_618) | ~accessible_world(U_617, V_127) | ~forename(U_617, V_618)))). % 11.49/4.06 tff(c_1386, plain, (![V_678, V_22, U_21]: (singleton(V_678, V_22) | ~accessible_world(U_21, V_678) | ~entity(U_21, V_22)))). % 11.49/4.06 tff(c_1454, plain, (![V_124, V_707]: (proposition(V_124, skc6) | ~accessible_world(V_707, V_124) | ~accessible_world(skc5, V_707)))). % 11.49/4.06 tff(c_1536, plain, (![V_121, V_745]: (think_believe_consider(V_121, skc7) | ~accessible_world(V_745, V_121) | ~accessible_world(skc5, V_745)))). % 11.49/4.06 tff(c_2076, plain, (~accessible_world(skc5, skc5))). % 11.49/4.06 tff(c_1643, plain, (![V_774, U_175]: (agent(V_774, skf1(U_175), U_175) | ~accessible_world(skc6, V_774) | ~man(skc6, U_175)))). % 11.49/4.06 tff(c_1437, plain, (![V_139, V_702]: (forename(V_139, skc8) | ~accessible_world(V_702, V_139) | ~accessible_world(skc5, V_702)))). % 11.49/4.06 tff(c_2060, plain, (![V_864]: (singleton(skc6, V_864) | ~eventuality(skc5, V_864)))). % 11.49/4.06 tff(c_2052, plain, (![V_862]: (thing(skc6, V_862) | ~eventuality(skc5, V_862)))). % 11.49/4.06 tff(c_1545, plain, (![V_746, V_6, U_5]: (thing(V_746, V_6) | ~accessible_world(U_5, V_746) | ~eventuality(U_5, V_6)))). % 11.49/4.06 tff(c_2028, plain, (![V_858]: (abstraction(skc6, V_858) | ~forename(skc5, V_858)))). % 11.49/4.06 tff(c_2020, plain, (![V_857]: (~human(skc6, V_857) | ~abstraction(skc5, V_857)))). % 11.49/4.07 tff(c_2012, plain, (![V_856]: (relation(skc6, V_856) | ~forename(skc5, V_856)))). % 11.49/4.07 tff(c_2004, plain, (![V_854]: (nonhuman(skc6, V_854) | ~abstraction(skc5, V_854)))). % 11.49/4.07 tff(c_2000, plain, (![V_851]: (relname(skc6, V_851) | ~forename(skc5, V_851)))). % 11.49/4.07 tff(c_1187, plain, (![V_612, V_44, U_43]: (nonhuman(V_612, V_44) | ~accessible_world(U_43, V_612) | ~abstraction(U_43, V_44)))). % 11.49/4.07 tff(c_1262, plain, (![V_649, V_50, U_49]: (relname(V_649, V_50) | ~accessible_world(U_49, V_649) | ~forename(U_49, V_50)))). % 11.49/4.07 tff(c_1972, plain, (![V_46]: (~eventuality(skc5, V_46) | ~abstraction(skc6, V_46)))). % 11.49/4.07 tff(c_1989, plain, (![V_174]: (~entity(skc5, skf1(V_174))))). % 11.49/4.07 tff(c_1932, plain, (![V_4]: (~entity(skc5, V_4) | ~event(skc6, V_4)))). % 11.49/4.07 tff(c_1962, plain, (![V_845]: (~general(skc6, V_845) | ~eventuality(skc5, V_845)))). % 11.49/4.07 tff(c_1953, plain, (![V_842]: (specific(skc6, V_842) | ~eventuality(skc5, V_842)))). % 11.49/4.07 tff(c_1949, plain, (![V_174]: (~abstraction(skc5, skf1(V_174))))). % 11.49/4.07 tff(c_1207, plain, (![V_621, V_10, U_9]: (specific(V_621, V_10) | ~accessible_world(U_9, V_621) | ~eventuality(U_9, V_10)))). % 11.49/4.07 tff(c_1905, plain, (![V_4]: (~abstraction(skc5, V_4) | ~event(skc6, V_4)))). % 11.49/4.07 tff(c_1895, plain, (![V_836]: (~eventuality(skc6, V_836) | ~entity(skc5, V_836)))). % 11.49/4.07 tff(c_1864, plain, (![V_831]: (~entity(skc6, V_831) | ~abstraction(skc5, V_831)))). % 11.49/4.07 tff(c_1863, plain, (![V_831]: (~eventuality(skc6, V_831) | ~abstraction(skc5, V_831)))). % 11.49/4.07 tff(c_1883, plain, (![V_834]: (existent(skc6, V_834) | ~entity(skc5, V_834)))). % 11.49/4.07 tff(c_1493, plain, (![V_720, V_26, U_25]: (existent(V_720, V_26) | ~accessible_world(U_25, V_720) | ~entity(U_25, V_26)))). % 11.49/4.07 tff(c_1848, plain, (![V_830]: (~abstraction(skc6, V_830) | ~event(skc5, V_830)))). % 11.49/4.07 tff(c_1829, plain, (![V_828]: (general(skc6, V_828) | ~abstraction(skc5, V_828)))). % 11.49/4.07 tff(c_1825, plain, (![V_825]: (eventuality(skc6, V_825) | ~event(skc5, V_825)))). % 11.49/4.07 tff(c_1276, plain, (![V_655, V_46, U_45]: (general(V_655, V_46) | ~accessible_world(U_45, V_655) | ~abstraction(U_45, V_46)))). % 11.49/4.07 tff(c_1528, plain, (![V_739, V_4, U_3]: (eventuality(V_739, V_4) | ~accessible_world(U_3, V_739) | ~event(U_3, V_4)))). % 11.49/4.07 tff(c_1821, plain, (~entity(skc6, skc7))). % 11.49/4.07 tff(c_1806, plain, (![V_4]: (~entity(skc6, V_4) | ~event(skc5, V_4)))). % 11.49/4.07 tff(c_1792, plain, (![V_26]: (~eventuality(skc5, V_26) | ~entity(skc6, V_26)))). % 11.49/4.07 tff(c_1786, plain, (![V_819]: (~male(skc6, V_819) | ~eventuality(skc5, V_819)))). % 11.49/4.07 tff(c_1778, plain, (![V_818]: (~existent(skc6, V_818) | ~eventuality(skc5, V_818)))). % 11.49/4.07 tff(c_1770, plain, (![V_816]: (unisex(skc6, V_816) | ~eventuality(skc5, V_816)))). % 11.49/4.07 tff(c_1766, plain, (![V_813]: (nonexistent(skc6, V_813) | ~eventuality(skc5, V_813)))). % 11.49/4.07 tff(c_1520, plain, (![V_733, V_14, U_13]: (unisex(V_733, V_14) | ~accessible_world(U_13, V_733) | ~eventuality(U_13, V_14)))). % 11.49/4.07 tff(c_1513, plain, (![V_730, V_12, U_11]: (nonexistent(V_730, V_12) | ~accessible_world(U_11, V_730) | ~eventuality(U_11, V_12)))). % 11.49/4.07 tff(c_1754, plain, (![V_810]: (~male(skc6, V_810) | ~abstraction(skc5, V_810)))). % 11.49/4.07 tff(c_1746, plain, (![V_808]: (unisex(skc6, V_808) | ~abstraction(skc5, V_808)))). % 11.49/4.07 tff(c_1519, plain, (![V_733, V_48, U_47]: (unisex(V_733, V_48) | ~accessible_world(U_47, V_733) | ~abstraction(U_47, V_48)))). % 11.49/4.07 tff(c_1738, plain, (![V_805]: (singleton(skc6, V_805) | ~entity(skc5, V_805)))). % 11.49/4.07 tff(c_1730, plain, (![V_803]: (thing(skc6, V_803) | ~entity(skc5, V_803)))). % 11.49/4.07 tff(c_1546, plain, (![V_746, V_22, U_21]: (thing(V_746, V_22) | ~accessible_world(U_21, V_746) | ~entity(U_21, V_22)))). % 11.49/4.07 tff(c_1722, plain, (![V_800]: (singleton(skc6, V_800) | ~abstraction(skc5, V_800)))). % 11.49/4.07 tff(c_1702, plain, (![V_792]: (thing(skc6, V_792) | ~abstraction(skc5, V_792)))). % 11.49/4.07 tff(c_128, plain, (![U_164, X_166, Y_167, W_163, Z_165, V_168]: (W_163=V_168 | ~agent(U_164, X_166, Z_165) | ~agent(U_164, Y_167, Z_165) | ~theme(U_164, Y_167, W_163) | ~think_believe_consider(U_164, Y_167) | ~think_believe_consider(U_164, X_166) | ~theme(U_164, X_166, V_168) | ~proposition(U_164, W_163) | ~proposition(U_164, V_168)))). % 11.49/4.07 tff(c_1544, plain, (![V_746, V_42, U_41]: (thing(V_746, V_42) | ~accessible_world(U_41, V_746) | ~abstraction(U_41, V_42)))). % 11.49/4.07 tff(c_1683, plain, (![V_46]: (~entity(skc5, V_46) | ~abstraction(skc6, V_46)))). % 11.49/4.07 tff(c_1677, plain, (![V_788]: (~general(skc6, V_788) | ~entity(skc5, V_788)))). % 11.49/4.07 tff(c_1669, plain, (![V_786]: (specific(skc6, V_786) | ~entity(skc5, V_786)))). % 11.49/4.07 tff(c_1208, plain, (![V_621, V_24, U_23]: (specific(V_621, V_24) | ~accessible_world(U_23, V_621) | ~entity(U_23, V_24)))). % 11.49/4.07 tff(c_126, plain, (![W_161, V_160, U_159, X_162]: (W_161=V_160 | ~entity(U_159, X_162) | ~of(U_159, V_160, X_162) | ~forename(U_159, W_161) | ~of(U_159, W_161, X_162) | ~forename(U_159, V_160)))). % 11.49/4.07 tff(c_1582, plain, (![V_760]: (of(V_760, skc8, skc9) | ~accessible_world(skc5, V_760)))). % 11.49/4.07 tff(c_1644, plain, (![V_774]: (agent(V_774, skc7, skc9) | ~accessible_world(skc5, V_774)))). % 11.49/4.08 tff(c_1619, plain, (![V_766]: (theme(V_766, skc7, skc6) | ~accessible_world(skc5, V_766)))). % 11.49/4.08 tff(c_120, plain, (![V_148, W_149, X_150, U_147]: (agent(V_148, W_149, X_150) | ~agent(U_147, W_149, X_150) | ~accessible_world(U_147, V_148)))). % 11.49/4.08 tff(c_1635, plain, (![V_772]: (~abstraction(V_772, skc9) | ~accessible_world(skc6, V_772)))). % 11.49/4.08 tff(c_1615, plain, (![V_100]: (entity(V_100, skc9) | ~accessible_world(skc6, V_100)))). % 11.49/4.08 tff(c_1598, plain, (![V_764]: (living(skc6, V_764) | ~human_person(skc5, V_764)))). % 11.49/4.08 tff(c_1597, plain, (![V_764]: (impartial(skc6, V_764) | ~human_person(skc5, V_764)))). % 11.49/4.08 tff(c_122, plain, (![V_152, W_153, X_154, U_151]: (theme(V_152, W_153, X_154) | ~theme(U_151, W_153, X_154) | ~accessible_world(U_151, V_152)))). % 11.49/4.08 tff(c_1608, plain, (entity(skc6, skc9))). % 11.49/4.08 tff(c_1596, plain, (![V_764]: (entity(skc6, V_764) | ~human_person(skc5, V_764)))). % 11.49/4.08 tff(c_1578, plain, (![V_758]: (organism(skc6, V_758) | ~human_person(skc5, V_758)))). % 11.49/4.08 tff(c_124, plain, (![V_156, W_157, X_158, U_155]: (of(V_156, W_157, X_158) | ~of(U_155, W_157, X_158) | ~accessible_world(U_155, V_156)))). % 11.49/4.08 tff(c_1524, plain, (![V_736, V_18, U_17]: (organism(V_736, V_18) | ~accessible_world(U_17, V_736) | ~human_person(U_17, V_18)))). % 11.49/4.08 tff(c_1562, plain, (![V_755]: (abstraction(skc6, V_755) | ~proposition(skc5, V_755)))). % 11.49/4.08 tff(c_1554, plain, (![V_753]: (relation(skc6, V_753) | ~proposition(skc5, V_753)))). % 11.49/4.08 tff(c_1168, plain, (![V_603, V_38, U_37]: (relation(V_603, V_38) | ~accessible_world(U_37, V_603) | ~proposition(U_37, V_38)))). % 11.49/4.08 tff(c_94, plain, (![V_109, W_110, U_108]: (living(V_109, W_110) | ~living(U_108, W_110) | ~accessible_world(U_108, V_109)))). % 11.49/4.08 tff(c_70, plain, (![V_73, W_74, U_72]: (thing(V_73, W_74) | ~thing(U_72, W_74) | ~accessible_world(U_72, V_73)))). % 11.49/4.08 tff(c_1532, plain, (![V_742]: (think_believe_consider(V_742, skc7) | ~accessible_world(skc5, V_742)))). % 11.49/4.08 tff(c_102, plain, (![V_121, W_122, U_120]: (think_believe_consider(V_121, W_122) | ~think_believe_consider(U_120, W_122) | ~accessible_world(U_120, V_121)))). % 11.49/4.08 tff(c_68, plain, (![V_70, W_71, U_69]: (eventuality(V_70, W_71) | ~eventuality(U_69, W_71) | ~accessible_world(U_69, V_70)))). % 11.49/4.08 tff(c_86, plain, (![V_97, W_98, U_96]: (organism(V_97, W_98) | ~organism(U_96, W_98) | ~accessible_world(U_96, V_97)))). % 11.49/4.08 tff(c_78, plain, (![V_85, W_86, U_84]: (unisex(V_85, W_86) | ~unisex(U_84, W_86) | ~accessible_world(U_84, V_85)))). % 11.49/4.08 tff(c_76, plain, (![V_82, W_83, U_81]: (nonexistent(V_82, W_83) | ~nonexistent(U_81, W_83) | ~accessible_world(U_81, V_82)))). % 11.49/4.08 tff(c_1501, plain, (![V_726]: (vincent_forename(V_726, skc8) | ~accessible_world(skc5, V_726)))). % 11.49/4.08 tff(c_118, plain, (![V_145, W_146, U_144]: (vincent_forename(V_145, W_146) | ~vincent_forename(U_144, W_146) | ~accessible_world(U_144, V_145)))). % 11.49/4.08 tff(c_92, plain, (![V_106, W_107, U_105]: (impartial(V_106, W_107) | ~impartial(U_105, W_107) | ~accessible_world(U_105, V_106)))). % 11.49/4.08 tff(c_90, plain, (![V_103, W_104, U_102]: (existent(V_103, W_104) | ~existent(U_102, W_104) | ~accessible_world(U_102, V_103)))). % 11.49/4.08 tff(c_96, plain, (![V_112, W_113, U_111]: (human(V_112, W_113) | ~human(U_111, W_113) | ~accessible_world(U_111, V_112)))). % 11.49/4.08 tff(c_1478, plain, (![V_712]: (abstraction(V_712, skc8) | ~accessible_world(skc6, V_712)))). % 11.49/4.08 tff(c_1477, plain, (![V_712]: (abstraction(V_712, skc6) | ~accessible_world(skc6, V_712)))). % 11.49/4.08 tff(c_108, plain, (![V_130, W_131, U_129]: (abstraction(V_130, W_131) | ~abstraction(U_129, W_131) | ~accessible_world(U_129, V_130)))). % 11.49/4.08 tff(c_84, plain, (![V_94, W_95, U_93]: (human_person(V_94, W_95) | ~human_person(U_93, W_95) | ~accessible_world(U_93, V_94)))). % 11.49/4.08 tff(c_1460, plain, (abstraction(skc6, skc6))). % 11.49/4.08 tff(c_1455, plain, (![V_707]: (abstraction(V_707, skc6) | ~accessible_world(skc5, V_707)))). % 11.49/4.08 tff(c_1447, plain, (![V_704]: (proposition(V_704, skc6) | ~accessible_world(skc5, V_704)))). % 11.49/4.08 tff(c_1443, plain, (abstraction(skc6, skc8))). % 11.49/4.08 tff(c_104, plain, (![V_124, W_125, U_123]: (proposition(V_124, W_125) | ~proposition(U_123, W_125) | ~accessible_world(U_123, V_124)))). % 11.49/4.08 tff(c_1438, plain, (![V_702]: (abstraction(V_702, skc8) | ~accessible_world(skc5, V_702)))). % 11.49/4.08 tff(c_1430, plain, (![V_699]: (forename(V_699, skc8) | ~accessible_world(skc5, V_699)))). % 11.49/4.08 tff(c_114, plain, (![V_139, W_140, U_138]: (forename(V_139, W_140) | ~forename(U_138, W_140) | ~accessible_world(U_138, V_139)))). % 11.49/4.08 tff(c_100, plain, (![V_118, W_119, U_117]: (male(V_118, W_119) | ~male(U_117, W_119) | ~accessible_world(U_117, V_118)))). % 11.49/4.08 tff(c_1409, plain, (![V_688, V_689]: (~entity(V_688, skf1(V_689)) | ~accessible_world(skc6, V_688)))). % 11.49/4.08 tff(c_1408, plain, (![V_688, V_689]: (~abstraction(V_688, skf1(V_689)) | ~accessible_world(skc6, V_688)))). % 11.49/4.08 tff(c_1393, plain, (![V_683, V_170]: (smoke(V_683, skf1(V_170)) | ~accessible_world(skc6, V_683)))). % 11.49/4.08 tff(c_1339, plain, (![V_670, V_174]: (event(V_670, skf1(V_174)) | ~accessible_world(skc6, V_670)))). % 11.49/4.08 tff(c_1303, plain, (![V_664, V_172]: (present(V_664, skf1(V_172)) | ~accessible_world(skc6, V_664)))). % 11.49/4.08 tff(c_64, plain, (![V_64, W_65, U_63]: (smoke(V_64, W_65) | ~smoke(U_63, W_65) | ~accessible_world(U_63, V_64)))). % 11.49/4.08 tff(c_1372, plain, (![U_3]: (~accessible_world(skc5, U_3) | ~event(U_3, skc9)))). % 11.49/4.08 tff(c_1352, plain, (![V_673]: (~entity(V_673, skc7) | ~accessible_world(skc5, V_673)))). % 11.49/4.08 tff(c_1377, plain, (~abstraction(skc6, skc7))). % 11.49/4.08 tff(c_72, plain, (![V_76, W_77, U_75]: (singleton(V_76, W_77) | ~singleton(U_75, W_77) | ~accessible_world(U_75, V_76)))). % 11.49/4.08 tff(c_1351, plain, (![V_673]: (~abstraction(V_673, skc7) | ~accessible_world(skc5, V_673)))). % 11.49/4.09 tff(c_1361, plain, (![V_674]: (~eventuality(V_674, skc9) | ~accessible_world(skc5, V_674)))). % 11.49/4.09 tff(c_1332, plain, (![V_669]: (human(V_669, skc9) | ~accessible_world(skc5, V_669)))). % 11.49/4.09 tff(c_1316, plain, (![V_667]: (male(V_667, skc9) | ~accessible_world(skc5, V_667)))). % 11.49/4.09 tff(c_1340, plain, (![V_670]: (event(V_670, skc7) | ~accessible_world(skc5, V_670)))). % 11.49/4.09 tff(c_66, plain, (![V_67, W_68, U_66]: (event(V_67, W_68) | ~event(U_66, W_68) | ~accessible_world(U_66, V_67)))). % 11.49/4.09 tff(c_1315, plain, (![V_667]: (human_person(V_667, skc9) | ~accessible_world(skc5, V_667)))). % 11.49/4.09 tff(c_1304, plain, (![V_664]: (present(V_664, skc7) | ~accessible_world(skc5, V_664)))). % 11.49/4.09 tff(c_1297, plain, (![V_661]: (man(V_661, skc9) | ~accessible_world(skc5, V_661)))). % 11.49/4.09 tff(c_80, plain, (![V_88, W_89, U_87]: (present(V_88, W_89) | ~present(U_87, W_89) | ~accessible_world(U_87, V_88)))). % 11.49/4.09 tff(c_82, plain, (![V_91, W_92, U_90]: (man(V_91, W_92) | ~man(U_90, W_92) | ~accessible_world(U_90, V_91)))). % 11.49/4.09 tff(c_1293, plain, (~abstraction(skc6, skc9))). % 11.49/4.09 tff(c_1283, plain, (![V_658]: (~abstraction(V_658, skc9) | ~accessible_world(skc5, V_658)))). % 11.49/4.09 tff(c_1224, plain, (![V_632]: (animate(V_632, skc9) | ~accessible_world(skc5, V_632)))). % 11.49/4.09 tff(c_1243, plain, (![V_641]: (entity(V_641, skc9) | ~accessible_world(skc5, V_641)))). % 11.49/4.09 tff(c_112, plain, (![V_136, W_137, U_135]: (general(V_136, W_137) | ~general(U_135, W_137) | ~accessible_world(U_135, V_136)))). % 11.49/4.09 tff(c_1270, plain, (![V_174]: (~abstraction(skc6, skf1(V_174))))). % 11.49/4.09 tff(c_1271, plain, (~abstraction(skc5, skc7))). % 11.49/4.09 tff(c_1229, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 11.49/4.09 tff(c_116, plain, (![V_142, W_143, U_141]: (relname(V_142, W_143) | ~relname(U_141, W_143) | ~accessible_world(U_141, V_142)))). % 11.49/4.09 tff(c_1256, plain, (![V_174]: (~entity(skc6, skf1(V_174))))). % 11.49/4.09 tff(c_1257, plain, (~entity(skc5, skc7))). % 11.49/4.09 tff(c_1234, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 11.49/4.09 tff(c_1164, plain, (![U_45, V_46]: (~entity(U_45, V_46) | ~abstraction(U_45, V_46)))). % 11.49/4.09 tff(c_1239, plain, (abstraction(skc5, skc8))). % 11.49/4.09 tff(c_88, plain, (![V_100, W_101, U_99]: (entity(V_100, W_101) | ~entity(U_99, W_101) | ~accessible_world(U_99, V_100)))). % 11.49/4.09 tff(c_1196, plain, (![U_617, V_618]: (abstraction(U_617, V_618) | ~forename(U_617, V_618)))). % 11.49/4.09 tff(c_1214, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~entity(U_25, V_26)))). % 11.49/4.09 tff(c_1183, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~abstraction(U_45, V_46)))). % 11.49/4.09 tff(c_98, plain, (![V_115, W_116, U_114]: (animate(V_115, W_116) | ~animate(U_114, W_116) | ~accessible_world(U_114, V_115)))). % 11.49/4.09 tff(c_187, plain, (![U_198, V_199]: (impartial(U_198, V_199) | ~human_person(U_198, V_199)))). % 11.49/4.09 tff(c_1219, plain, (entity(skc5, skc9))). % 11.49/4.09 tff(c_217, plain, (![U_17, V_18]: (entity(U_17, V_18) | ~human_person(U_17, V_18)))). % 11.49/4.09 tff(c_222, plain, (![U_11, V_12]: (~existent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 11.49/4.09 tff(c_258, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 11.49/4.09 tff(c_74, plain, (![V_79, W_80, U_78]: (specific(V_79, W_80) | ~specific(U_78, W_80) | ~accessible_world(U_78, V_79)))). % 11.49/4.09 tff(c_232, plain, (![U_43, V_44]: (~human(U_43, V_44) | ~abstraction(U_43, V_44)))). % 11.49/4.09 tff(c_227, plain, (![U_49, V_50]: (relation(U_49, V_50) | ~forename(U_49, V_50)))). % 11.49/4.09 tff(c_188, plain, (![U_198, V_199]: (living(U_198, V_199) | ~human_person(U_198, V_199)))). % 11.49/4.09 tff(c_110, plain, (![V_133, W_134, U_132]: (nonhuman(V_133, W_134) | ~nonhuman(U_132, W_134) | ~accessible_world(U_132, V_133)))). % 11.49/4.09 tff(c_267, plain, (![U_9, V_10]: (~general(U_9, V_10) | ~eventuality(U_9, V_10)))). % 11.49/4.09 tff(c_1178, plain, (~abstraction(skc5, skc9))). % 11.49/4.09 tff(c_240, plain, (![U_47, V_48]: (~male(U_47, V_48) | ~abstraction(U_47, V_48)))). % 11.49/4.09 tff(c_1173, plain, (abstraction(skc5, skc6))). % 11.49/4.09 tff(c_177, plain, (![U_37, V_38]: (abstraction(U_37, V_38) | ~proposition(U_37, V_38)))). % 11.49/4.09 tff(c_106, plain, (![V_127, W_128, U_126]: (relation(V_127, W_128) | ~relation(U_126, W_128) | ~accessible_world(U_126, V_127)))). % 11.49/4.09 tff(c_268, plain, (![U_23, V_24]: (~general(U_23, V_24) | ~entity(U_23, V_24)))). % 11.49/4.09 tff(c_259, plain, (![U_21, V_22]: (singleton(U_21, V_22) | ~entity(U_21, V_22)))). % 11.49/4.09 tff(c_257, plain, (![U_41, V_42]: (singleton(U_41, V_42) | ~abstraction(U_41, V_42)))). % 11.49/4.09 tff(c_160, plain, (![U_175]: (agent(skc6, skf1(U_175), U_175) | ~man(skc6, U_175)))). % 11.49/4.09 tff(c_1150, plain, (![V_170]: (smoke(skc6, skf1(V_170))))). % 11.49/4.09 tff(c_850, plain, (![V_174]: (event(skc6, skf1(V_174))))). % 11.49/4.09 tff(c_575, plain, (![V_172]: (present(skc6, skf1(V_172))))). % 11.49/4.09 tff(c_277, plain, (~event(skc5, skc9))). % 11.49/4.09 tff(c_273, plain, (~eventuality(skc5, skc9))). % 11.49/4.09 tff(c_241, plain, (![U_13, V_14]: (~male(U_13, V_14) | ~eventuality(U_13, V_14)))). % 11.49/4.10 tff(c_58, plain, (![U_57, V_58]: (~specific(U_57, V_58) | ~general(U_57, V_58)))). % 11.49/4.10 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 11.49/4.10 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~abstraction(U_41, V_42)))). % 11.49/4.10 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 11.49/4.10 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 11.49/4.10 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 11.49/4.10 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 11.49/4.10 tff(c_56, plain, (![U_55, V_56]: (~unisex(U_55, V_56) | ~male(U_55, V_56)))). % 11.49/4.10 tff(c_60, plain, (![U_59, V_60]: (~nonhuman(U_59, V_60) | ~human(U_59, V_60)))). % 11.49/4.10 tff(c_52, plain, (![U_51, V_52]: (relation(U_51, V_52) | ~relname(U_51, V_52)))). % 11.49/4.10 tff(c_62, plain, (![U_61, V_62]: (~existent(U_61, V_62) | ~nonexistent(U_61, V_62)))). % 11.49/4.10 tff(c_20, plain, (![U_19, V_20]: (entity(U_19, V_20) | ~organism(U_19, V_20)))). % 11.49/4.10 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~vincent_forename(U_53, V_54)))). % 11.49/4.10 tff(c_206, plain, (animate(skc5, skc9))). % 11.49/4.10 tff(c_205, plain, (human(skc5, skc9))). % 11.49/4.10 tff(c_198, plain, (human_person(skc5, skc9))). % 11.49/4.10 tff(c_16, plain, (![U_15, V_16]: (human_person(U_15, V_16) | ~man(U_15, V_16)))). % 11.49/4.10 tff(c_50, plain, (![U_49, V_50]: (relname(U_49, V_50) | ~forename(U_49, V_50)))). % 11.49/4.10 tff(c_48, plain, (![U_47, V_48]: (unisex(U_47, V_48) | ~abstraction(U_47, V_48)))). % 11.49/4.10 tff(c_44, plain, (![U_43, V_44]: (nonhuman(U_43, V_44) | ~abstraction(U_43, V_44)))). % 11.49/4.10 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 11.49/4.10 tff(c_46, plain, (![U_45, V_46]: (general(U_45, V_46) | ~abstraction(U_45, V_46)))). % 11.49/4.10 tff(c_18, plain, (![U_17, V_18]: (organism(U_17, V_18) | ~human_person(U_17, V_18)))). % 11.49/4.10 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 11.49/4.10 tff(c_22, plain, (![U_21, V_22]: (thing(U_21, V_22) | ~entity(U_21, V_22)))). % 11.49/4.10 tff(c_40, plain, (![U_39, V_40]: (abstraction(U_39, V_40) | ~relation(U_39, V_40)))). % 11.49/4.10 tff(c_171, plain, (male(skc5, skc9))). % 11.49/4.10 tff(c_38, plain, (![U_37, V_38]: (relation(U_37, V_38) | ~proposition(U_37, V_38)))). % 11.49/4.10 tff(c_36, plain, (![U_35, V_36]: (male(U_35, V_36) | ~man(U_35, V_36)))). % 11.49/4.10 tff(c_24, plain, (![U_23, V_24]: (specific(U_23, V_24) | ~entity(U_23, V_24)))). % 11.49/4.10 tff(c_26, plain, (![U_25, V_26]: (existent(U_25, V_26) | ~entity(U_25, V_26)))). % 11.49/4.10 tff(c_28, plain, (![U_27, V_28]: (impartial(U_27, V_28) | ~organism(U_27, V_28)))). % 11.49/4.10 tff(c_30, plain, (![U_29, V_30]: (living(U_29, V_30) | ~organism(U_29, V_30)))). % 11.49/4.10 tff(c_32, plain, (![U_31, V_32]: (human(U_31, V_32) | ~human_person(U_31, V_32)))). % 11.49/4.10 tff(c_34, plain, (![U_33, V_34]: (animate(U_33, V_34) | ~human_person(U_33, V_34)))). % 11.49/4.10 tff(c_150, plain, (agent(skc5, skc7, skc9))). % 11.49/4.10 tff(c_152, plain, (theme(skc5, skc7, skc6))). % 11.49/4.10 tff(c_148, plain, (of(skc5, skc8, skc9))). % 11.49/4.10 tff(c_136, plain, (vincent_forename(skc5, skc8))). % 11.49/4.10 tff(c_134, plain, (forename(skc5, skc8))). % 11.49/4.10 tff(c_132, plain, (man(skc5, skc9))). % 11.49/4.10 tff(c_138, plain, (event(skc5, skc7))). % 11.49/4.10 tff(c_140, plain, (present(skc5, skc7))). % 11.49/4.10 tff(c_142, plain, (think_believe_consider(skc5, skc7))). % 11.49/4.10 tff(c_144, plain, (accessible_world(skc5, skc6))). % 11.49/4.10 tff(c_146, plain, (proposition(skc5, skc6))). % 11.49/4.10 tff(c_130, plain, (actual_world(skc5))). % 11.49/4.10 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.49/4.10 %------------------------------------------------------------------------------