%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP241-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.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:44 PM UTC 2025 % Result : Satisfiable 13.60s 4.91s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NLP241-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.35 % Computer : n013.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Tue Apr 8 09:41:47 EDT 2025 % 0.14/0.35 % CPUTime : % 13.60/4.91 % 13.60/4.91 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.60/4.91 % 13.60/4.91 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.83/4.92 %$ be > theme > of > agent > vincent_forename > unisex > think_believe_consider > thing > state > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > jules_forename > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > actual_world > #nlpp > skf1 > skc29 > skc28 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 % 13.83/4.92 % 13.83/4.92 %Foreground sorts: % 13.83/4.92 % 13.83/4.92 % 13.83/4.92 %Background operators: % 13.83/4.92 % 13.83/4.92 % 13.83/4.92 %Foreground operators: % 13.83/4.92 tff(skc16, type, skc16: $i). % 13.83/4.92 tff(relation, type, relation: ($i * $i) > $o). % 13.83/4.92 tff(forename, type, forename: ($i * $i) > $o). % 13.83/4.92 tff(be, type, be: ($i * $i * $i * $i) > $o). % 13.83/4.92 tff(theme, type, theme: ($i * $i * $i) > $o). % 13.83/4.92 tff(living, type, living: ($i * $i) > $o). % 13.83/4.92 tff(human_person, type, human_person: ($i * $i) > $o). % 13.83/4.92 tff(present, type, present: ($i * $i) > $o). % 13.83/4.92 tff(entity, type, entity: ($i * $i) > $o). % 13.83/4.92 tff(skc18, type, skc18: $i). % 13.83/4.92 tff(skc29, type, skc29: $i). % 13.83/4.92 tff(eventuality, type, eventuality: ($i * $i) > $o). % 13.83/4.92 tff(existent, type, existent: ($i * $i) > $o). % 13.83/4.92 tff(abstraction, type, abstraction: ($i * $i) > $o). % 13.83/4.92 tff(skc25, type, skc25: $i). % 13.83/4.92 tff(skf1, type, skf1: $i > $i). % 13.83/4.92 tff(proposition, type, proposition: ($i * $i) > $o). % 13.83/4.92 tff(relname, type, relname: ($i * $i) > $o). % 13.83/4.92 tff(singleton, type, singleton: ($i * $i) > $o). % 13.83/4.92 tff(skc17, type, skc17: $i). % 13.83/4.92 tff(male, type, male: ($i * $i) > $o). % 13.83/4.92 tff(organism, type, organism: ($i * $i) > $o). % 13.83/4.92 tff(animate, type, animate: ($i * $i) > $o). % 13.83/4.92 tff(of, type, of: ($i * $i * $i) > $o). % 13.83/4.92 tff(actual_world, type, actual_world: $i > $o). % 13.83/4.92 tff(agent, type, agent: ($i * $i * $i) > $o). % 13.83/4.92 tff(skc26, type, skc26: $i). % 13.83/4.92 tff(skc24, type, skc24: $i). % 13.83/4.92 tff(skc20, type, skc20: $i). % 13.83/4.92 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 13.83/4.92 tff(general, type, general: ($i * $i) > $o). % 13.83/4.92 tff(smoke, type, smoke: ($i * $i) > $o). % 13.83/4.92 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 13.83/4.92 tff(skc23, type, skc23: $i). % 13.83/4.92 tff(event, type, event: ($i * $i) > $o). % 13.83/4.92 tff(skc21, type, skc21: $i). % 13.83/4.92 tff(skc22, type, skc22: $i). % 13.83/4.92 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 13.83/4.92 tff(skc27, type, skc27: $i). % 13.83/4.92 tff(state, type, state: ($i * $i) > $o). % 13.83/4.92 tff(thing, type, thing: ($i * $i) > $o). % 13.83/4.92 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 13.83/4.92 tff(skc15, type, skc15: $i). % 13.83/4.92 tff(human, type, human: ($i * $i) > $o). % 13.83/4.92 tff(man, type, man: ($i * $i) > $o). % 13.83/4.92 tff(unisex, type, unisex: ($i * $i) > $o). % 13.83/4.92 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 13.83/4.92 tff(impartial, type, impartial: ($i * $i) > $o). % 13.83/4.92 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 13.83/4.92 tff(specific, type, specific: ($i * $i) > $o). % 13.83/4.92 tff(skc19, type, skc19: $i). % 13.83/4.92 tff(skc28, type, skc28: $i). % 13.83/4.92 % 13.83/4.92 %Saturated clause set: % 13.83/4.92 tff(c_8573, plain, (![V_146, V_1517]: (animate(V_146, skc21) | ~accessible_world(V_1517, V_146) | ~accessible_world(skc26, V_1517)))). % 13.83/4.92 tff(c_8598, plain, (![V_143, V_1518]: (human(V_143, skc21) | ~accessible_world(V_1518, V_143) | ~accessible_world(skc26, V_1518)))). % 13.83/4.92 tff(c_8567, plain, (![V_125, V_1516]: (human_person(V_125, skc21) | ~accessible_world(V_1516, V_125) | ~accessible_world(skc26, V_1516)))). % 13.83/4.92 tff(c_8531, plain, (![V_149, V_1515]: (male(V_149, skc21) | ~accessible_world(V_1515, V_149) | ~accessible_world(skc26, V_1515)))). % 13.83/4.92 tff(c_8482, plain, (![V_122, V_1511]: (man(V_122, skc21) | ~accessible_world(V_1511, V_122) | ~accessible_world(skc26, V_1511)))). % 13.83/4.92 tff(c_8625, plain, (![U_3]: (~accessible_world(skc26, U_3) | ~event(U_3, skc21)))). % 13.83/4.92 tff(c_8359, plain, (![V_1509, V_742]: (skc16=V_1509 | ~think_believe_consider(V_742, skc17) | ~think_believe_consider(V_742, skf1(skc19)) | ~theme(V_742, skf1(skc19), V_1509) | ~proposition(V_742, skc16) | ~proposition(V_742, V_1509) | ~accessible_world(skc26, V_742) | ~accessible_world(skc15, V_742)))). % 13.83/4.92 tff(c_8533, plain, (![V_1515]: (~eventuality(V_1515, skc21) | ~accessible_world(skc26, V_1515)))). % 13.83/4.92 tff(c_8569, plain, (![V_1516]: (human(V_1516, skc21) | ~accessible_world(skc26, V_1516)))). % 13.83/4.93 tff(c_8568, plain, (![V_1516]: (animate(V_1516, skc21) | ~accessible_world(skc26, V_1516)))). % 13.83/4.93 tff(c_8432, plain, (![V_125]: (human_person(V_125, skc21) | ~accessible_world(skc26, V_125)))). % 13.83/4.93 tff(c_8416, plain, (![V_149]: (male(V_149, skc21) | ~accessible_world(skc26, V_149)))). % 13.83/4.93 tff(c_8371, plain, (![W_1496, V_1493, V_738]: (W_1496=V_1493 | ~theme(V_738, skc22, W_1496) | ~think_believe_consider(V_738, skc22) | ~think_believe_consider(V_738, skf1(skc21)) | ~theme(V_738, skf1(skc21), V_1493) | ~proposition(V_738, W_1496) | ~proposition(V_738, V_1493) | ~accessible_world(skc26, V_738) | ~accessible_world(skc16, V_738)))). % 13.83/4.93 tff(c_8381, plain, (![V_122]: (man(V_122, skc21) | ~accessible_world(skc26, V_122)))). % 13.83/4.93 tff(c_8450, plain, (~event(skc26, skc21))). % 13.83/4.93 tff(c_8433, plain, (animate(skc26, skc21))). % 13.83/4.93 tff(c_8434, plain, (human(skc26, skc21))). % 13.83/4.93 tff(c_8418, plain, (~eventuality(skc26, skc21))). % 13.83/4.93 tff(c_8383, plain, (human_person(skc26, skc21))). % 13.83/4.93 tff(c_8382, plain, (male(skc26, skc21))). % 13.83/4.93 tff(c_8372, plain, (man(skc26, skc21))). % 13.83/4.93 tff(c_8333, plain, (![W_1496, V_1493, V_738]: (W_1496=V_1493 | ~theme(V_738, skc17, W_1496) | ~think_believe_consider(V_738, skc17) | ~think_believe_consider(V_738, skf1(skc19)) | ~theme(V_738, skf1(skc19), V_1493) | ~proposition(V_738, W_1496) | ~proposition(V_738, V_1493) | ~accessible_world(skc26, V_738) | ~accessible_world(skc15, V_738)))). % 13.83/4.93 tff(c_8349, plain, (![V_1504, V_742]: (skc26=V_1504 | ~think_believe_consider(V_742, skc27) | ~think_believe_consider(V_742, skf1(skc29)) | ~theme(V_742, skf1(skc29), V_1504) | ~proposition(V_742, skc26) | ~proposition(V_742, V_1504) | ~accessible_world(skc26, V_742) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8330, plain, (![W_1496, V_1493, V_738]: (W_1496=V_1493 | ~theme(V_738, skc27, W_1496) | ~think_believe_consider(V_738, skc27) | ~think_believe_consider(V_738, skf1(skc29)) | ~theme(V_738, skf1(skc29), V_1493) | ~proposition(V_738, W_1496) | ~proposition(V_738, V_1493) | ~accessible_world(skc26, V_738) | ~accessible_world(skc15, V_738)))). % 13.83/4.93 tff(c_8326, plain, (![W_1496, V_1493, V_738, U_196]: (W_1496=V_1493 | ~theme(V_738, skf1(U_196), W_1496) | ~think_believe_consider(V_738, skf1(U_196)) | ~theme(V_738, skf1(U_196), V_1493) | ~proposition(V_738, W_1496) | ~proposition(V_738, V_1493) | ~accessible_world(skc26, V_738) | ~man(skc26, U_196)))). % 13.83/4.93 tff(c_8308, plain, (![V_742]: (~agent(V_742, skc17, skc29) | ~think_believe_consider(V_742, skc17) | ~think_believe_consider(V_742, skc27) | ~proposition(V_742, skc16) | ~proposition(V_742, skc26) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_4497, plain, (![V_189, Y_188, U_937, V_936, W_184]: (W_184=V_189 | ~agent(V_936, Y_188, U_937) | ~theme(V_936, Y_188, W_184) | ~think_believe_consider(V_936, Y_188) | ~think_believe_consider(V_936, skf1(U_937)) | ~theme(V_936, skf1(U_937), V_189) | ~proposition(V_936, W_184) | ~proposition(V_936, V_189) | ~accessible_world(skc26, V_936) | ~man(skc26, U_937)))). % 13.83/4.93 tff(c_8252, plain, (![V_1481, V_742]: (skc16=V_1481 | ~agent(V_742, skc17, skc29) | ~think_believe_consider(V_742, skc17) | ~think_believe_consider(V_742, skc27) | ~theme(V_742, skc27, V_1481) | ~proposition(V_742, skc16) | ~proposition(V_742, V_1481) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8296, plain, (~accessible_world(skc16, skc26))). % 13.83/4.93 tff(c_8294, plain, (![V_742]: (~agent(V_742, skc27, skc19) | ~think_believe_consider(V_742, skc27) | ~think_believe_consider(V_742, skc17) | ~proposition(V_742, skc26) | ~proposition(V_742, skc16) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8234, plain, (![V_1477, V_742]: (skc26=V_1477 | ~agent(V_742, skc27, skc19) | ~think_believe_consider(V_742, skc27) | ~think_believe_consider(V_742, skc17) | ~theme(V_742, skc17, V_1477) | ~proposition(V_742, skc26) | ~proposition(V_742, V_1477) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8251, plain, (![V_1481, V_742]: (skc26=V_1481 | ~agent(V_742, skc27, skc29) | ~think_believe_consider(V_742, skc27) | ~theme(V_742, skc27, V_1481) | ~proposition(V_742, skc26) | ~proposition(V_742, V_1481) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8235, plain, (![V_1477, V_742]: (skc16=V_1477 | ~agent(V_742, skc17, skc19) | ~think_believe_consider(V_742, skc17) | ~theme(V_742, skc17, V_1477) | ~proposition(V_742, skc16) | ~proposition(V_742, V_1477) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_2921, plain, (![W_184, V_189, V_800, Y_188]: (W_184=V_189 | ~agent(V_800, Y_188, skc29) | ~theme(V_800, Y_188, W_184) | ~think_believe_consider(V_800, Y_188) | ~think_believe_consider(V_800, skc27) | ~theme(V_800, skc27, V_189) | ~proposition(V_800, W_184) | ~proposition(V_800, V_189) | ~accessible_world(skc15, V_800)))). % 13.83/4.93 tff(c_2910, plain, (![W_184, V_189, V_797, Y_188]: (W_184=V_189 | ~agent(V_797, Y_188, skc19) | ~theme(V_797, Y_188, W_184) | ~think_believe_consider(V_797, Y_188) | ~think_believe_consider(V_797, skc17) | ~theme(V_797, skc17, V_189) | ~proposition(V_797, W_184) | ~proposition(V_797, V_189) | ~accessible_world(skc15, V_797)))). % 13.83/4.93 tff(c_8216, plain, (![V_1469, V_742]: (skc16=V_1469 | ~agent(V_742, skc17, skc21) | ~think_believe_consider(V_742, skc17) | ~think_believe_consider(V_742, skc22) | ~theme(V_742, skc22, V_1469) | ~proposition(V_742, skc16) | ~proposition(V_742, V_1469) | ~accessible_world(skc16, V_742) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_8215, plain, (![V_1469, V_742]: (skc26=V_1469 | ~agent(V_742, skc27, skc21) | ~think_believe_consider(V_742, skc27) | ~think_believe_consider(V_742, skc22) | ~theme(V_742, skc22, V_1469) | ~proposition(V_742, skc26) | ~proposition(V_742, V_1469) | ~accessible_world(skc16, V_742) | ~accessible_world(skc15, V_742)))). % 13.83/4.93 tff(c_2928, plain, (![W_184, V_189, V_801, Y_188]: (W_184=V_189 | ~agent(V_801, Y_188, skc21) | ~theme(V_801, Y_188, W_184) | ~think_believe_consider(V_801, Y_188) | ~think_believe_consider(V_801, skc22) | ~theme(V_801, skc22, V_189) | ~proposition(V_801, W_184) | ~proposition(V_801, V_189) | ~accessible_world(skc16, V_801)))). % 13.83/4.93 tff(c_8080, plain, (![V_146, V_1440]: (animate(V_146, skc29) | ~accessible_world(V_1440, V_146) | ~accessible_world(skc26, V_1440)))). % 13.83/4.93 tff(c_8075, plain, (![V_143, V_1439]: (human(V_143, skc29) | ~accessible_world(V_1439, V_143) | ~accessible_world(skc26, V_1439)))). % 13.83/4.93 tff(c_7775, plain, (![V_146, V_1432]: (animate(V_146, skc19) | ~accessible_world(V_1432, V_146) | ~accessible_world(skc26, V_1432)))). % 13.83/4.93 tff(c_7800, plain, (![V_143, V_1433]: (human(V_143, skc19) | ~accessible_world(V_1433, V_143) | ~accessible_world(skc26, V_1433)))). % 13.83/4.93 tff(c_7769, plain, (![V_125, V_1431]: (human_person(V_125, skc19) | ~accessible_world(V_1431, V_125) | ~accessible_world(skc26, V_1431)))). % 13.83/4.93 tff(c_7732, plain, (![V_149, V_1430]: (male(V_149, skc19) | ~accessible_world(V_1430, V_149) | ~accessible_world(skc26, V_1430)))). % 13.83/4.93 tff(c_8012, plain, (![V_149, V_1437]: (male(V_149, skc29) | ~accessible_world(V_1437, V_149) | ~accessible_world(skc26, V_1437)))). % 13.83/4.93 tff(c_8048, plain, (![V_125, V_1438]: (human_person(V_125, skc29) | ~accessible_world(V_1438, V_125) | ~accessible_world(skc26, V_1438)))). % 13.83/4.93 tff(c_7674, plain, (![V_101, V_1428]: (think_believe_consider(V_101, skc17) | ~accessible_world(V_1428, V_101) | ~accessible_world(skc26, V_1428)))). % 13.83/4.93 tff(c_7966, plain, (![V_101, V_1436]: (think_believe_consider(V_101, skc27) | ~accessible_world(V_1436, V_101) | ~accessible_world(skc26, V_1436)))). % 13.83/4.93 tff(c_7684, plain, (![V_122, V_1429]: (man(V_122, skc19) | ~accessible_world(V_1429, V_122) | ~accessible_world(skc26, V_1429)))). % 13.83/4.93 tff(c_7947, plain, (![V_122, V_1435]: (man(V_122, skc29) | ~accessible_world(V_1435, V_122) | ~accessible_world(skc26, V_1435)))). % 13.83/4.93 tff(c_7827, plain, (![U_3]: (~accessible_world(skc26, U_3) | ~event(U_3, skc19)))). % 13.83/4.93 tff(c_8107, plain, (![U_3]: (~accessible_world(skc26, U_3) | ~event(U_3, skc29)))). % 13.83/4.93 tff(c_8014, plain, (![V_1437]: (~eventuality(V_1437, skc29) | ~accessible_world(skc26, V_1437)))). % 13.83/4.94 tff(c_8081, plain, (~think_believe_consider(skc26, skf1(skc29)))). % 13.83/4.94 tff(c_7918, plain, (![V_146]: (animate(V_146, skc29) | ~accessible_world(skc26, V_146)))). % 13.83/4.94 tff(c_7936, plain, (![V_143]: (human(V_143, skc29) | ~accessible_world(skc26, V_143)))). % 13.83/4.94 tff(c_7897, plain, (![V_125]: (human_person(V_125, skc29) | ~accessible_world(skc26, V_125)))). % 13.83/4.94 tff(c_7881, plain, (![V_149]: (male(V_149, skc29) | ~accessible_world(skc26, V_149)))). % 13.83/4.94 tff(c_7962, plain, (![V_101]: (think_believe_consider(V_101, skc27) | ~accessible_world(skc26, V_101)))). % 13.83/4.94 tff(c_7959, plain, (think_believe_consider(skc26, skc27))). % 13.83/4.94 tff(c_7846, plain, (![V_122]: (man(V_122, skc29) | ~accessible_world(skc26, V_122)))). % 13.83/4.94 tff(c_7915, plain, (~event(skc26, skc29))). % 13.83/4.94 tff(c_7899, plain, (human(skc26, skc29))). % 13.83/4.94 tff(c_7898, plain, (animate(skc26, skc29))). % 13.83/4.94 tff(c_7883, plain, (~eventuality(skc26, skc29))). % 13.83/4.94 tff(c_7848, plain, (human_person(skc26, skc29))). % 13.83/4.94 tff(c_7847, plain, (male(skc26, skc29))). % 13.83/4.94 tff(c_7837, plain, (man(skc26, skc29))). % 13.83/4.94 tff(c_7734, plain, (![V_1430]: (~eventuality(V_1430, skc19) | ~accessible_world(skc26, V_1430)))). % 13.83/4.94 tff(c_7669, plain, (![V_143]: (human(V_143, skc19) | ~accessible_world(skc26, V_143)))). % 13.83/4.94 tff(c_7770, plain, (![V_1431]: (animate(V_1431, skc19) | ~accessible_world(skc26, V_1431)))). % 13.83/4.94 tff(c_7617, plain, (![V_125]: (human_person(V_125, skc19) | ~accessible_world(skc26, V_125)))). % 13.83/4.94 tff(c_7735, plain, (~think_believe_consider(skc26, skf1(skc19)))). % 13.83/4.94 tff(c_7601, plain, (![V_149]: (male(V_149, skc19) | ~accessible_world(skc26, V_149)))). % 13.83/4.94 tff(c_7566, plain, (![V_122]: (man(V_122, skc19) | ~accessible_world(skc26, V_122)))). % 13.83/4.94 tff(c_7632, plain, (![V_101]: (think_believe_consider(V_101, skc17) | ~accessible_world(skc26, V_101)))). % 13.83/4.94 tff(c_7648, plain, (~event(skc26, skc19))). % 13.83/4.94 tff(c_7619, plain, (human(skc26, skc19))). % 13.83/4.94 tff(c_7618, plain, (animate(skc26, skc19))). % 13.83/4.94 tff(c_7603, plain, (~eventuality(skc26, skc19))). % 13.83/4.94 tff(c_7629, plain, (think_believe_consider(skc26, skc17))). % 13.83/4.94 tff(c_7568, plain, (human_person(skc26, skc19))). % 13.83/4.94 tff(c_7567, plain, (male(skc26, skc19))). % 13.83/4.94 tff(c_7557, plain, (man(skc26, skc19))). % 13.83/4.94 tff(c_4859, plain, (![W_962, V_963, U_196]: (W_962=V_963 | ~theme(skc26, skf1(U_196), W_962) | ~think_believe_consider(skc26, skf1(U_196)) | ~theme(skc26, skf1(U_196), V_963) | ~proposition(skc26, W_962) | ~proposition(skc26, V_963) | ~man(skc26, U_196)))). % 13.83/4.94 tff(c_2863, plain, (![W_182, V_778]: (skc18=W_182 | ~entity(V_778, skc19) | ~forename(V_778, W_182) | ~of(V_778, W_182, skc19) | ~forename(V_778, skc18) | ~accessible_world(skc15, V_778)))). % 13.83/4.94 tff(c_2943, plain, (![W_182, V_804]: (skc20=W_182 | ~entity(V_804, skc21) | ~forename(V_804, W_182) | ~of(V_804, W_182, skc21) | ~forename(V_804, skc20) | ~accessible_world(skc15, V_804)))). % 13.83/4.94 tff(c_2873, plain, (![W_182, V_782]: (skc25=W_182 | ~entity(V_782, skc24) | ~forename(V_782, W_182) | ~of(V_782, W_182, skc24) | ~forename(V_782, skc25) | ~accessible_world(skc15, V_782)))). % 13.83/4.94 tff(c_2844, plain, (![W_182, V_773]: (skc28=W_182 | ~entity(V_773, skc29) | ~forename(V_773, W_182) | ~of(V_773, W_182, skc29) | ~forename(V_773, skc28) | ~accessible_world(skc15, V_773)))). % 13.83/4.94 tff(c_6473, plain, (![V_137, V_1183, V_1182]: (impartial(V_137, V_1183) | ~accessible_world(V_1182, V_137) | ~accessible_world(skc16, V_1182) | ~human_person(skc15, V_1183)))). % 13.83/4.94 tff(c_6411, plain, (![V_86, V_1170, V_1169]: (singleton(V_86, V_1170) | ~accessible_world(V_1169, V_86) | ~accessible_world(skc26, V_1169) | ~entity(skc15, V_1170)))). % 13.83/4.94 tff(c_6129, plain, (![V_140, V_1149, V_1148]: (living(V_140, V_1149) | ~accessible_world(V_1148, V_140) | ~accessible_world(skc16, V_1148) | ~human_person(skc15, V_1149)))). % 13.83/4.94 tff(c_6578, plain, (![V_86, V_1209, V_1208]: (singleton(V_86, V_1209) | ~accessible_world(V_1208, V_86) | ~accessible_world(skc16, V_1208) | ~eventuality(skc15, V_1209)))). % 13.83/4.94 tff(c_6060, plain, (![V_137, V_1143, V_1142]: (impartial(V_137, V_1143) | ~accessible_world(V_1142, V_137) | ~accessible_world(skc26, V_1142) | ~human_person(skc15, V_1143)))). % 13.83/4.94 tff(c_6461, plain, (![V_86, V_1179, V_1178]: (singleton(V_86, V_1179) | ~accessible_world(V_1178, V_86) | ~accessible_world(skc16, V_1178) | ~entity(skc15, V_1179)))). % 13.83/4.94 tff(c_6530, plain, (![V_86, V_1199, V_1198]: (singleton(V_86, V_1199) | ~accessible_world(V_1198, V_86) | ~accessible_world(skc26, V_1198) | ~abstraction(skc15, V_1199)))). % 13.83/4.94 tff(c_6509, plain, (![V_86, V_1191, V_1190]: (singleton(V_86, V_1191) | ~accessible_world(V_1190, V_86) | ~accessible_world(skc26, V_1190) | ~eventuality(skc15, V_1191)))). % 13.83/4.94 tff(c_6468, plain, (![V_107, V_1181, V_1180]: (relation(V_107, V_1181) | ~accessible_world(V_1180, V_107) | ~accessible_world(skc16, V_1180) | ~forename(skc15, V_1181)))). % 13.83/4.94 tff(c_6143, plain, (![V_140, V_1154, V_1153]: (living(V_140, V_1154) | ~accessible_world(V_1153, V_140) | ~accessible_world(skc26, V_1153) | ~human_person(skc15, V_1154)))). % 13.83/4.94 tff(c_6505, plain, (![V_86, V_1189, V_1188]: (singleton(V_86, V_1189) | ~accessible_world(V_1188, V_86) | ~accessible_world(skc16, V_1188) | ~abstraction(skc15, V_1189)))). % 13.83/4.94 tff(c_6646, plain, (![V_107, V_1217, V_1216]: (relation(V_107, V_1217) | ~accessible_world(V_1216, V_107) | ~accessible_world(skc26, V_1216) | ~forename(skc15, V_1217)))). % 13.83/4.94 tff(c_5741, plain, (![V_92, V_1125, V_1124]: (nonexistent(V_92, V_1125) | ~accessible_world(V_1124, V_92) | ~accessible_world(skc16, V_1124) | ~eventuality(skc15, V_1125)))). % 13.83/4.94 tff(c_5427, plain, (![V_134, V_1081, V_1080]: (existent(V_134, V_1081) | ~accessible_world(V_1080, V_134) | ~accessible_world(skc26, V_1080) | ~entity(skc15, V_1081)))). % 13.83/4.94 tff(c_5377, plain, (![V_89, V_1073, V_1072]: (specific(V_89, V_1073) | ~accessible_world(V_1072, V_89) | ~accessible_world(skc26, V_1072) | ~entity(skc15, V_1073)))). % 13.83/4.94 tff(c_5728, plain, (![V_80, V_1123, V_1122]: (eventuality(V_80, V_1123) | ~accessible_world(V_1122, V_80) | ~accessible_world(skc26, V_1122) | ~event(skc15, V_1123)))). % 13.83/4.94 tff(c_5325, plain, (![V_80, V_1060, V_1059]: (eventuality(V_80, V_1060) | ~accessible_world(V_1059, V_80) | ~accessible_world(skc16, V_1059) | ~event(skc15, V_1060)))). % 13.83/4.94 tff(c_5385, plain, (![V_155, V_1075, V_1074]: (relname(V_155, V_1075) | ~accessible_world(V_1074, V_155) | ~accessible_world(skc16, V_1074) | ~forename(skc15, V_1075)))). % 13.83/4.94 tff(c_5544, plain, (![V_116, V_1103, V_1102]: (general(V_116, V_1103) | ~accessible_world(V_1102, V_116) | ~accessible_world(skc16, V_1102) | ~abstraction(skc15, V_1103)))). % 13.83/4.94 tff(c_5226, plain, (![V_83, V_1054, V_1053]: (thing(V_83, V_1054) | ~accessible_world(V_1053, V_83) | ~accessible_world(skc26, V_1053) | ~abstraction(skc15, V_1054)))). % 13.83/4.94 tff(c_5399, plain, (![V_128, V_1077, V_1076]: (organism(V_128, V_1077) | ~accessible_world(V_1076, V_128) | ~accessible_world(skc16, V_1076) | ~human_person(skc15, V_1077)))). % 13.83/4.94 tff(c_5645, plain, (![V_89, V_1121, V_1120]: (specific(V_89, V_1121) | ~accessible_world(V_1120, V_89) | ~accessible_world(skc16, V_1120) | ~entity(skc15, V_1121)))). % 13.83/4.94 tff(c_5218, plain, (![V_89, V_1052, V_1051]: (specific(V_89, V_1052) | ~accessible_world(V_1051, V_89) | ~accessible_world(skc16, V_1051) | ~eventuality(skc15, V_1052)))). % 13.83/4.95 tff(c_5553, plain, (![V_89, V_1105, V_1104]: (specific(V_89, V_1105) | ~accessible_world(V_1104, V_89) | ~accessible_world(skc26, V_1104) | ~eventuality(skc15, V_1105)))). % 13.83/4.95 tff(c_5179, plain, (![V_107, V_1042, V_1041]: (relation(V_107, V_1042) | ~accessible_world(V_1041, V_107) | ~accessible_world(skc16, V_1041) | ~proposition(skc15, V_1042)))). % 13.83/4.95 tff(c_5409, plain, (![V_83, V_1079, V_1078]: (thing(V_83, V_1079) | ~accessible_world(V_1078, V_83) | ~accessible_world(skc16, V_1078) | ~entity(skc15, V_1079)))). % 13.83/4.95 tff(c_5491, plain, (![V_83, V_1095, V_1094]: (thing(V_83, V_1095) | ~accessible_world(V_1094, V_83) | ~accessible_world(skc26, V_1094) | ~entity(skc15, V_1095)))). % 13.83/4.95 tff(c_4498, plain, (![V_164, U_937, V_936]: (agent(V_164, skf1(U_937), U_937) | ~accessible_world(V_936, V_164) | ~accessible_world(skc26, V_936) | ~man(skc26, U_937)))). % 13.83/4.95 tff(c_5628, plain, (![V_116, V_1117, V_1116]: (general(V_116, V_1117) | ~accessible_world(V_1116, V_116) | ~accessible_world(skc26, V_1116) | ~abstraction(skc15, V_1117)))). % 13.83/4.95 tff(c_5361, plain, (![V_113, V_1068, V_1067]: (nonhuman(V_113, V_1068) | ~accessible_world(V_1067, V_113) | ~accessible_world(skc16, V_1067) | ~abstraction(skc15, V_1068)))). % 13.83/4.95 tff(c_5443, plain, (![V_107, V_1085, V_1084]: (relation(V_107, V_1085) | ~accessible_world(V_1084, V_107) | ~accessible_world(skc26, V_1084) | ~proposition(skc15, V_1085)))). % 13.83/4.95 tff(c_5346, plain, (![V_92, V_1064, V_1063]: (nonexistent(V_92, V_1064) | ~accessible_world(V_1063, V_92) | ~accessible_world(skc26, V_1063) | ~eventuality(skc15, V_1064)))). % 13.83/4.95 tff(c_5499, plain, (![V_155, V_1097, V_1096]: (relname(V_155, V_1097) | ~accessible_world(V_1096, V_155) | ~accessible_world(skc26, V_1096) | ~forename(skc15, V_1097)))). % 13.83/4.95 tff(c_5187, plain, (![V_95, V_1044, V_1043]: (unisex(V_95, V_1044) | ~accessible_world(V_1043, V_95) | ~accessible_world(skc16, V_1043) | ~eventuality(skc15, V_1044)))). % 13.83/4.95 tff(c_5435, plain, (![V_83, V_1083, V_1082]: (thing(V_83, V_1083) | ~accessible_world(V_1082, V_83) | ~accessible_world(skc26, V_1082) | ~eventuality(skc15, V_1083)))). % 13.83/4.95 tff(c_5637, plain, (![V_95, V_1119, V_1118]: (unisex(V_95, V_1119) | ~accessible_world(V_1118, V_95) | ~accessible_world(skc26, V_1118) | ~abstraction(skc15, V_1119)))). % 13.83/4.95 tff(c_7246, plain, (~agent(skc15, skc17, skc29))). % 13.83/4.95 tff(c_5451, plain, (![V_113, V_1087, V_1086]: (nonhuman(V_113, V_1087) | ~accessible_world(V_1086, V_113) | ~accessible_world(skc26, V_1086) | ~abstraction(skc15, V_1087)))). % 13.83/4.95 tff(c_5164, plain, (![V_83, V_1038, V_1037]: (thing(V_83, V_1038) | ~accessible_world(V_1037, V_83) | ~accessible_world(skc16, V_1037) | ~eventuality(skc15, V_1038)))). % 13.83/4.95 tff(c_5242, plain, (![V_95, V_1058, V_1057]: (unisex(V_95, V_1058) | ~accessible_world(V_1057, V_95) | ~accessible_world(skc16, V_1057) | ~abstraction(skc15, V_1058)))). % 13.83/4.95 tff(c_5469, plain, (![V_134, V_1089, V_1088]: (existent(V_134, V_1089) | ~accessible_world(V_1088, V_134) | ~accessible_world(skc16, V_1088) | ~entity(skc15, V_1089)))). % 13.83/4.95 tff(c_5338, plain, (![V_95, V_1062, V_1061]: (unisex(V_95, V_1062) | ~accessible_world(V_1061, V_95) | ~accessible_world(skc26, V_1061) | ~eventuality(skc15, V_1062)))). % 13.83/4.95 tff(c_5595, plain, (![V_128, V_1115, V_1114]: (organism(V_128, V_1115) | ~accessible_world(V_1114, V_128) | ~accessible_world(skc26, V_1114) | ~human_person(skc15, V_1115)))). % 13.83/4.95 tff(c_5202, plain, (![V_83, V_1048, V_1047]: (thing(V_83, V_1048) | ~accessible_world(V_1047, V_83) | ~accessible_world(skc16, V_1047) | ~abstraction(skc15, V_1048)))). % 13.83/4.95 tff(c_4601, plain, (![V_131, V_942]: (entity(V_131, skc19) | ~accessible_world(V_942, V_131) | ~accessible_world(skc16, V_942)))). % 13.83/4.95 tff(c_7187, plain, (~agent(skc15, skc27, skc19))). % 13.83/4.95 tff(c_4658, plain, (![V_131, V_944]: (entity(V_131, skc19) | ~accessible_world(V_944, V_131) | ~accessible_world(skc26, V_944)))). % 13.83/4.95 tff(c_4793, plain, (![V_131, V_951]: (entity(V_131, skc24) | ~accessible_world(V_951, V_131) | ~accessible_world(skc26, V_951)))). % 13.83/4.95 tff(c_4737, plain, (![V_131, V_949]: (entity(V_131, skc29) | ~accessible_world(V_949, V_131) | ~accessible_world(skc26, V_949)))). % 13.83/4.95 tff(c_4821, plain, (![V_131, V_952]: (entity(V_131, skc21) | ~accessible_world(V_952, V_131) | ~accessible_world(skc26, V_952)))). % 13.83/4.95 tff(c_4765, plain, (![V_131, V_950]: (entity(V_131, skc29) | ~accessible_world(V_950, V_131) | ~accessible_world(skc16, V_950)))). % 13.83/4.95 tff(c_4630, plain, (![V_131, V_943]: (entity(V_131, skc24) | ~accessible_world(V_943, V_131) | ~accessible_world(skc16, V_943)))). % 13.83/4.95 tff(c_4686, plain, (![V_131, V_945]: (entity(V_131, skc21) | ~accessible_world(V_945, V_131) | ~accessible_world(skc16, V_945)))). % 13.83/4.95 tff(c_6676, plain, (![U_3, V_4]: (~accessible_world(skc26, U_3) | ~entity(skc15, V_4) | ~event(U_3, V_4)))). % 13.83/4.95 tff(c_6770, plain, (![U_3, V_4]: (~accessible_world(skc16, U_3) | ~abstraction(skc15, V_4) | ~event(U_3, V_4)))). % 13.83/4.95 tff(c_5962, plain, (![U_3, V_4]: (~accessible_world(skc16, U_3) | ~entity(skc15, V_4) | ~event(U_3, V_4)))). % 13.83/4.95 tff(c_5900, plain, (![U_23, V_24]: (~accessible_world(skc16, U_23) | ~entity(skc15, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.95 tff(c_6997, plain, (![U_1261]: (~accessible_world(skc26, U_1261) | ~entity(U_1261, skc23)))). % 13.83/4.95 tff(c_6494, plain, (![U_41, V_42]: (~accessible_world(skc26, U_41) | ~eventuality(skc15, V_42) | ~entity(U_41, V_42)))). % 13.83/4.95 tff(c_6227, plain, (![U_23, V_24]: (~accessible_world(skc26, U_23) | ~entity(skc15, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.95 tff(c_5983, plain, (![U_23, V_24]: (~accessible_world(skc26, U_23) | ~eventuality(skc15, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.95 tff(c_6974, plain, (![U_1254]: (~accessible_world(skc16, U_1254) | ~entity(U_1254, skc23)))). % 13.83/4.95 tff(c_6345, plain, (![U_41, V_42]: (~accessible_world(skc16, U_41) | ~eventuality(skc15, V_42) | ~entity(U_41, V_42)))). % 13.83/4.95 tff(c_6469, plain, (![V_1180, V_1181]: (abstraction(V_1180, V_1181) | ~accessible_world(skc16, V_1180) | ~forename(skc15, V_1181)))). % 13.83/4.95 tff(c_6457, plain, (![U_3, V_4]: (~accessible_world(skc26, U_3) | ~abstraction(skc15, V_4) | ~event(U_3, V_4)))). % 13.83/4.95 tff(c_6639, plain, (![U_23, V_24]: (~accessible_world(skc16, U_23) | ~eventuality(skc15, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.95 tff(c_6647, plain, (![V_1216, V_1217]: (abstraction(V_1216, V_1217) | ~accessible_world(skc26, V_1216) | ~forename(skc15, V_1217)))). % 13.83/4.95 tff(c_2243, plain, (![V_146, V_656]: (animate(V_146, skc24) | ~accessible_world(V_656, V_146) | ~accessible_world(skc15, V_656)))). % 13.83/4.95 tff(c_2472, plain, (![V_143, V_693]: (human(V_143, skc29) | ~accessible_world(V_693, V_143) | ~accessible_world(skc15, V_693)))). % 13.83/4.95 tff(c_2209, plain, (![V_146, V_647]: (animate(V_146, skc19) | ~accessible_world(V_647, V_146) | ~accessible_world(skc15, V_647)))). % 13.83/4.95 tff(c_2953, plain, (![V_179, V_809]: (be(V_179, skc23, skc24, skc24) | ~accessible_world(V_809, V_179) | ~accessible_world(skc15, V_809)))). % 13.83/4.95 tff(c_5188, plain, (![V_1043, V_1044]: (~male(V_1043, V_1044) | ~accessible_world(skc16, V_1043) | ~eventuality(skc15, V_1044)))). % 13.83/4.95 tff(c_5326, plain, (![V_1059, V_1060]: (~entity(V_1059, V_1060) | ~accessible_world(skc16, V_1059) | ~event(skc15, V_1060)))). % 13.83/4.95 tff(c_2426, plain, (![V_682, V_633]: (human(V_682, skc19) | ~accessible_world(V_633, V_682) | ~accessible_world(skc15, V_633)))). % 13.83/4.95 tff(c_5545, plain, (![V_1102, V_1103]: (~eventuality(V_1102, V_1103) | ~accessible_world(skc16, V_1102) | ~abstraction(skc15, V_1103)))). % 13.83/4.95 tff(c_5339, plain, (![V_1061, V_1062]: (~male(V_1061, V_1062) | ~accessible_world(skc26, V_1061) | ~eventuality(skc15, V_1062)))). % 13.83/4.95 tff(c_2922, plain, (![V_164, V_800]: (agent(V_164, skc27, skc29) | ~accessible_world(V_800, V_164) | ~accessible_world(skc15, V_800)))). % 13.83/4.95 tff(c_2464, plain, (![V_143, V_692]: (human(V_143, skc24) | ~accessible_world(V_692, V_143) | ~accessible_world(skc15, V_692)))). % 13.83/4.95 tff(c_2229, plain, (![V_131, V_652]: (entity(V_131, skc21) | ~accessible_world(V_652, V_131) | ~accessible_world(skc15, V_652)))). % 13.83/4.95 tff(c_2494, plain, (![V_131, V_698]: (entity(V_131, skc29) | ~accessible_world(V_698, V_131) | ~accessible_world(skc15, V_698)))). % 13.83/4.95 tff(c_5428, plain, (![V_1080, V_1081]: (~eventuality(V_1080, V_1081) | ~accessible_world(skc26, V_1080) | ~entity(skc15, V_1081)))). % 13.83/4.95 tff(c_3657, plain, (![V_107, V_881]: (relation(V_107, V_881) | ~accessible_world(skc26, V_107) | ~forename(skc15, V_881)))). % 13.83/4.95 tff(c_5219, plain, (![V_1051, V_1052]: (~general(V_1051, V_1052) | ~accessible_world(skc16, V_1051) | ~eventuality(skc15, V_1052)))). % 13.83/4.95 tff(c_2864, plain, (![V_172, V_778]: (of(V_172, skc18, skc19) | ~accessible_world(V_778, V_172) | ~accessible_world(skc15, V_778)))). % 13.83/4.95 tff(c_5452, plain, (![V_1086, V_1087]: (~human(V_1086, V_1087) | ~accessible_world(skc26, V_1086) | ~abstraction(skc15, V_1087)))). % 13.83/4.95 tff(c_5165, plain, (![V_1037, V_1038]: (singleton(V_1037, V_1038) | ~accessible_world(skc16, V_1037) | ~eventuality(skc15, V_1038)))). % 13.83/4.95 tff(c_2572, plain, (![V_143, V_714]: (human(V_143, skc21) | ~accessible_world(V_714, V_143) | ~accessible_world(skc15, V_714)))). % 13.83/4.95 tff(c_2639, plain, (![V_146, V_725]: (animate(V_146, skc29) | ~accessible_world(V_725, V_146) | ~accessible_world(skc15, V_725)))). % 13.83/4.95 tff(c_5402, plain, (![V_1076, V_1077]: (entity(V_1076, V_1077) | ~accessible_world(skc16, V_1076) | ~human_person(skc15, V_1077)))). % 13.83/4.96 tff(c_5444, plain, (![V_1084, V_1085]: (abstraction(V_1084, V_1085) | ~accessible_world(skc26, V_1084) | ~proposition(skc15, V_1085)))). % 13.83/4.96 tff(c_5227, plain, (![V_1053, V_1054]: (singleton(V_1053, V_1054) | ~accessible_world(skc26, V_1053) | ~abstraction(skc15, V_1054)))). % 13.83/4.96 tff(c_2221, plain, (![V_131, V_651]: (entity(V_131, skc24) | ~accessible_world(V_651, V_131) | ~accessible_world(skc15, V_651)))). % 13.83/4.96 tff(c_2845, plain, (![V_172, V_773]: (of(V_172, skc28, skc29) | ~accessible_world(V_773, V_172) | ~accessible_world(skc15, V_773)))). % 13.83/4.96 tff(c_5180, plain, (![V_1041, V_1042]: (abstraction(V_1041, V_1042) | ~accessible_world(skc16, V_1041) | ~proposition(skc15, V_1042)))). % 13.83/4.96 tff(c_5436, plain, (![V_1082, V_1083]: (singleton(V_1082, V_1083) | ~accessible_world(skc26, V_1082) | ~eventuality(skc15, V_1083)))). % 13.83/4.96 tff(c_3092, plain, (![V_86, V_828]: (singleton(V_86, V_828) | ~accessible_world(skc16, V_86) | ~abstraction(skc15, V_828)))). % 13.83/4.96 tff(c_2517, plain, (![V_146, V_703]: (animate(V_146, skc21) | ~accessible_world(V_703, V_146) | ~accessible_world(skc15, V_703)))). % 13.83/4.96 tff(c_5347, plain, (![V_1063, V_1064]: (~existent(V_1063, V_1064) | ~accessible_world(skc26, V_1063) | ~eventuality(skc15, V_1064)))). % 13.83/4.96 tff(c_5401, plain, (![V_1076, V_1077]: (impartial(V_1076, V_1077) | ~accessible_world(skc16, V_1076) | ~human_person(skc15, V_1077)))). % 13.83/4.96 tff(c_5386, plain, (![V_1074, V_1075]: (relation(V_1074, V_1075) | ~accessible_world(skc16, V_1074) | ~forename(skc15, V_1075)))). % 13.83/4.96 tff(c_5410, plain, (![V_1078, V_1079]: (singleton(V_1078, V_1079) | ~accessible_world(skc16, V_1078) | ~entity(skc15, V_1079)))). % 13.83/4.96 tff(c_5629, plain, (![V_1116, V_1117]: (~eventuality(V_1116, V_1117) | ~accessible_world(skc26, V_1116) | ~abstraction(skc15, V_1117)))). % 13.83/4.96 tff(c_2936, plain, (![V_74, V_803, V_802]: (smoke(V_74, skf1(V_803)) | ~accessible_world(V_802, V_74) | ~accessible_world(skc26, V_802)))). % 13.83/4.96 tff(c_2635, plain, (![V_131, V_724]: (entity(V_131, skc19) | ~accessible_world(V_724, V_131) | ~accessible_world(skc15, V_724)))). % 13.83/4.96 tff(c_5492, plain, (![V_1094, V_1095]: (singleton(V_1094, V_1095) | ~accessible_world(skc26, V_1094) | ~entity(skc15, V_1095)))). % 13.83/4.96 tff(c_5362, plain, (![V_1067, V_1068]: (~human(V_1067, V_1068) | ~accessible_world(skc16, V_1067) | ~abstraction(skc15, V_1068)))). % 13.83/4.96 tff(c_5598, plain, (![V_1114, V_1115]: (entity(V_1114, V_1115) | ~accessible_world(skc26, V_1114) | ~human_person(skc15, V_1115)))). % 13.83/4.96 tff(c_5742, plain, (![V_1124, V_1125]: (~existent(V_1124, V_1125) | ~accessible_world(skc16, V_1124) | ~eventuality(skc15, V_1125)))). % 13.83/4.96 tff(c_5546, plain, (![V_1102, V_1103]: (~entity(V_1102, V_1103) | ~accessible_world(skc16, V_1102) | ~abstraction(skc15, V_1103)))). % 13.83/4.96 tff(c_5378, plain, (![V_1072, V_1073]: (~general(V_1072, V_1073) | ~accessible_world(skc26, V_1072) | ~entity(skc15, V_1073)))). % 13.83/4.96 tff(c_5327, plain, (![V_1059, V_1060]: (~abstraction(V_1059, V_1060) | ~accessible_world(skc16, V_1059) | ~event(skc15, V_1060)))). % 13.83/4.96 tff(c_2911, plain, (![V_164, V_797]: (agent(V_164, skc17, skc19) | ~accessible_world(V_797, V_164) | ~accessible_world(skc15, V_797)))). % 13.83/4.96 tff(c_6144, plain, (~event(skc15, skc18))). % 13.83/4.96 tff(c_5596, plain, (![V_1114, V_1115]: (living(V_1114, V_1115) | ~accessible_world(skc26, V_1114) | ~human_person(skc15, V_1115)))). % 13.83/4.96 tff(c_2903, plain, (![V_77, V_796, V_795]: (event(V_77, skf1(V_796)) | ~accessible_world(V_795, V_77) | ~accessible_world(skc26, V_795)))). % 13.83/4.96 tff(c_6131, plain, (~event(skc15, skc28))). % 13.83/4.96 tff(c_6130, plain, (~event(skc15, skc16))). % 13.83/4.96 tff(c_6125, plain, (~event(skc15, skc25))). % 13.83/4.96 tff(c_5400, plain, (![V_1076, V_1077]: (living(V_1076, V_1077) | ~accessible_world(skc16, V_1076) | ~human_person(skc15, V_1077)))). % 13.83/4.96 tff(c_6124, plain, (~event(skc15, skc26))). % 13.83/4.96 tff(c_2886, plain, (![V_168, V_791]: (theme(V_168, skc17, skc16) | ~accessible_world(V_791, V_168) | ~accessible_world(skc15, V_791)))). % 13.83/4.96 tff(c_6116, plain, (~event(skc15, skc20))). % 13.83/4.96 tff(c_5730, plain, (![V_1122, V_1123]: (~abstraction(V_1122, V_1123) | ~accessible_world(skc26, V_1122) | ~event(skc15, V_1123)))). % 13.83/4.96 tff(c_5597, plain, (![V_1114, V_1115]: (impartial(V_1114, V_1115) | ~accessible_world(skc26, V_1114) | ~human_person(skc15, V_1115)))). % 13.83/4.96 tff(c_5729, plain, (![V_1122, V_1123]: (~entity(V_1122, V_1123) | ~accessible_world(skc26, V_1122) | ~event(skc15, V_1123)))). % 13.83/4.96 tff(c_5554, plain, (![V_1104, V_1105]: (~general(V_1104, V_1105) | ~accessible_world(skc26, V_1104) | ~eventuality(skc15, V_1105)))). % 13.83/4.96 tff(c_5470, plain, (![V_1088, V_1089]: (~eventuality(V_1088, V_1089) | ~accessible_world(skc16, V_1088) | ~entity(skc15, V_1089)))). % 13.83/4.96 tff(c_5638, plain, (![V_1118, V_1119]: (~male(V_1118, V_1119) | ~accessible_world(skc26, V_1118) | ~abstraction(skc15, V_1119)))). % 13.83/4.96 tff(c_5646, plain, (![V_1120, V_1121]: (~general(V_1120, V_1121) | ~accessible_world(skc16, V_1120) | ~entity(skc15, V_1121)))). % 13.83/4.96 tff(c_2944, plain, (![V_172, V_804]: (of(V_172, skc20, skc21) | ~accessible_world(V_804, V_172) | ~accessible_world(skc15, V_804)))). % 13.83/4.96 tff(c_5243, plain, (![V_1057, V_1058]: (~male(V_1057, V_1058) | ~accessible_world(skc16, V_1057) | ~abstraction(skc15, V_1058)))). % 13.83/4.96 tff(c_5630, plain, (![V_1116, V_1117]: (~entity(V_1116, V_1117) | ~accessible_world(skc26, V_1116) | ~abstraction(skc15, V_1117)))). % 13.83/4.96 tff(c_3708, plain, (![V_92, V_892]: (nonexistent(V_92, V_892) | ~accessible_world(skc16, V_92) | ~eventuality(skc15, V_892)))). % 13.83/4.96 tff(c_4166, plain, (![V_80, V_921]: (eventuality(V_80, V_921) | ~accessible_world(skc26, V_80) | ~event(skc15, V_921)))). % 13.83/4.96 tff(c_3081, plain, (![V_89, V_826]: (specific(V_89, V_826) | ~accessible_world(skc16, V_89) | ~entity(skc15, V_826)))). % 13.83/4.96 tff(c_3153, plain, (![V_95, V_835]: (unisex(V_95, V_835) | ~accessible_world(skc26, V_95) | ~abstraction(skc15, V_835)))). % 13.83/4.96 tff(c_3809, plain, (![V_116, V_899]: (general(V_116, V_899) | ~accessible_world(skc26, V_116) | ~abstraction(skc15, V_899)))). % 13.83/4.96 tff(c_3543, plain, (![V_128, V_873]: (organism(V_128, V_873) | ~accessible_world(skc26, V_128) | ~human_person(skc15, V_873)))). % 13.83/4.96 tff(c_2010, plain, (![V_125, V_617]: (human_person(V_125, skc21) | ~accessible_world(V_617, V_125) | ~accessible_world(skc15, V_617)))). % 13.83/4.96 tff(c_2874, plain, (![V_172, V_782]: (of(V_172, skc25, skc24) | ~accessible_world(V_782, V_172) | ~accessible_world(skc15, V_782)))). % 13.83/4.96 tff(c_2365, plain, (![V_149, V_671]: (male(V_149, skc29) | ~accessible_world(V_671, V_149) | ~accessible_world(skc15, V_671)))). % 13.83/4.96 tff(c_2115, plain, (![V_125, V_633]: (human_person(V_125, skc19) | ~accessible_world(V_633, V_125) | ~accessible_world(skc15, V_633)))). % 13.83/4.96 tff(c_3271, plain, (![V_89, V_843]: (specific(V_89, V_843) | ~accessible_world(skc26, V_89) | ~eventuality(skc15, V_843)))). % 13.83/4.96 tff(c_3829, plain, (![V_116, V_900]: (general(V_116, V_900) | ~accessible_world(skc16, V_116) | ~abstraction(skc15, V_900)))). % 13.83/4.96 tff(c_2381, plain, (![V_149, V_675]: (male(V_149, skc24) | ~accessible_world(V_675, V_149) | ~accessible_world(skc15, V_675)))). % 13.83/4.96 tff(c_2393, plain, (![V_149, V_676]: (male(V_149, skc19) | ~accessible_world(V_676, V_149) | ~accessible_world(skc15, V_676)))). % 13.83/4.96 tff(c_3521, plain, (![V_155, V_871]: (relname(V_155, V_871) | ~accessible_world(skc26, V_155) | ~forename(skc15, V_871)))). % 13.83/4.96 tff(c_3300, plain, (![V_83, V_849]: (thing(V_83, V_849) | ~accessible_world(skc26, V_83) | ~entity(skc15, V_849)))). % 13.83/4.96 tff(c_2292, plain, (![V_149, V_663]: (male(V_149, skc21) | ~accessible_world(V_663, V_149) | ~accessible_world(skc15, V_663)))). % 13.83/4.96 tff(c_2892, plain, (![V_168, V_794]: (theme(V_168, skc27, skc26) | ~accessible_world(V_794, V_168) | ~accessible_world(skc15, V_794)))). % 13.83/4.96 tff(c_3998, plain, (![V_134, V_911]: (existent(V_134, V_911) | ~accessible_world(skc16, V_134) | ~entity(skc15, V_911)))). % 13.83/4.96 tff(c_2969, plain, (![V_113, V_813]: (nonhuman(V_113, V_813) | ~accessible_world(skc26, V_113) | ~abstraction(skc15, V_813)))). % 13.83/4.96 tff(c_3443, plain, (![V_107, V_861]: (relation(V_107, V_861) | ~accessible_world(skc26, V_107) | ~proposition(skc15, V_861)))). % 13.83/4.96 tff(c_3641, plain, (![V_83, V_879]: (thing(V_83, V_879) | ~accessible_world(skc26, V_83) | ~eventuality(skc15, V_879)))). % 13.83/4.96 tff(c_3986, plain, (![V_134, V_910]: (existent(V_134, V_910) | ~accessible_world(skc26, V_134) | ~entity(skc15, V_910)))). % 13.83/4.96 tff(c_3308, plain, (![V_83, V_850]: (thing(V_83, V_850) | ~accessible_world(skc16, V_83) | ~entity(skc15, V_850)))). % 13.83/4.96 tff(c_3559, plain, (![V_128, V_874]: (organism(V_128, V_874) | ~accessible_world(skc16, V_128) | ~human_person(skc15, V_874)))). % 13.83/4.96 tff(c_3529, plain, (![V_155, V_872]: (relname(V_155, V_872) | ~accessible_world(skc16, V_155) | ~forename(skc15, V_872)))). % 13.83/4.96 tff(c_3073, plain, (![V_89, V_825]: (specific(V_89, V_825) | ~accessible_world(skc26, V_89) | ~entity(skc15, V_825)))). % 13.83/4.96 tff(c_2915, plain, (![V_98, V_799, V_798]: (present(V_98, skf1(V_799)) | ~accessible_world(V_798, V_98) | ~accessible_world(skc26, V_798)))). % 13.83/4.96 tff(c_2977, plain, (![V_113, V_814]: (nonhuman(V_113, V_814) | ~accessible_world(skc16, V_113) | ~abstraction(skc15, V_814)))). % 13.83/4.96 tff(c_2606, plain, (![V_719, V_639]: (event(V_719, skc23) | ~accessible_world(V_639, V_719) | ~accessible_world(skc15, V_639)))). % 13.83/4.96 tff(c_3700, plain, (![V_92, V_891]: (nonexistent(V_92, V_891) | ~accessible_world(skc26, V_92) | ~eventuality(skc15, V_891)))). % 13.83/4.96 tff(c_4351, plain, (![V_95, V_929]: (unisex(V_95, V_929) | ~accessible_world(skc26, V_95) | ~eventuality(skc15, V_929)))). % 13.83/4.96 tff(c_4214, plain, (![V_80, V_922]: (eventuality(V_80, V_922) | ~accessible_world(skc16, V_80) | ~event(skc15, V_922)))). % 13.83/4.96 tff(c_3161, plain, (![V_95, V_836]: (unisex(V_95, V_836) | ~accessible_world(skc16, V_95) | ~abstraction(skc15, V_836)))). % 13.83/4.96 tff(c_2605, plain, (![V_719, V_708]: (event(V_719, skc22) | ~accessible_world(V_708, V_719) | ~accessible_world(skc16, V_708)))). % 13.83/4.96 tff(c_3057, plain, (![V_83, V_823]: (thing(V_83, V_823) | ~accessible_world(skc26, V_83) | ~abstraction(skc15, V_823)))). % 13.83/4.96 tff(c_3279, plain, (![V_89, V_844]: (specific(V_89, V_844) | ~accessible_world(skc16, V_89) | ~eventuality(skc15, V_844)))). % 13.83/4.96 tff(c_2929, plain, (![V_164, V_801]: (agent(V_164, skc22, skc21) | ~accessible_world(V_801, V_164) | ~accessible_world(skc16, V_801)))). % 13.83/4.96 tff(c_3065, plain, (![V_83, V_824]: (thing(V_83, V_824) | ~accessible_world(skc16, V_83) | ~abstraction(skc15, V_824)))). % 13.83/4.96 tff(c_2237, plain, (![V_653, V_639]: (eventuality(V_653, skc23) | ~accessible_world(V_639, V_653) | ~accessible_world(skc15, V_639)))). % 13.83/4.96 tff(c_4359, plain, (![V_95, V_930]: (unisex(V_95, V_930) | ~accessible_world(skc16, V_95) | ~eventuality(skc15, V_930)))). % 13.83/4.96 tff(c_3451, plain, (![V_107, V_862]: (relation(V_107, V_862) | ~accessible_world(skc16, V_107) | ~proposition(skc15, V_862)))). % 13.83/4.96 tff(c_1994, plain, (![V_125, V_616]: (human_person(V_125, skc24) | ~accessible_world(V_616, V_125) | ~accessible_world(skc15, V_616)))). % 13.83/4.96 tff(c_3649, plain, (![V_83, V_880]: (thing(V_83, V_880) | ~accessible_world(skc16, V_83) | ~eventuality(skc15, V_880)))). % 13.83/4.96 tff(c_2099, plain, (![V_125, V_632]: (human_person(V_125, skc29) | ~accessible_world(V_632, V_125) | ~accessible_world(skc15, V_632)))). % 13.83/4.96 tff(c_2453, plain, (![V_101, V_690]: (think_believe_consider(V_101, skc17) | ~accessible_world(V_690, V_101) | ~accessible_world(skc15, V_690)))). % 13.83/4.96 tff(c_2457, plain, (![V_101, V_691]: (think_believe_consider(V_101, skc27) | ~accessible_world(V_691, V_101) | ~accessible_world(skc15, V_691)))). % 13.83/4.96 tff(c_2085, plain, (![V_629, V_260, U_259]: (living(V_629, V_260) | ~accessible_world(U_259, V_629) | ~human_person(U_259, V_260)))). % 13.83/4.96 tff(c_2399, plain, (![V_677, V_260, U_259]: (impartial(V_677, V_260) | ~accessible_world(U_259, V_677) | ~human_person(U_259, V_260)))). % 13.83/4.97 tff(c_2653, plain, (![V_158, V_729]: (vincent_forename(V_158, skc18) | ~accessible_world(V_729, V_158) | ~accessible_world(skc15, V_729)))). % 13.83/4.97 tff(c_2708, plain, (![V_733, V_238, U_237]: (singleton(V_733, V_238) | ~accessible_world(U_237, V_733) | ~entity(U_237, V_238)))). % 13.83/4.97 tff(c_2558, plain, (![V_711, V_242, U_241]: (relation(V_711, V_242) | ~accessible_world(U_241, V_711) | ~forename(U_241, V_242)))). % 13.83/4.97 tff(c_2341, plain, (![V_122, V_669]: (man(V_122, skc21) | ~accessible_world(V_669, V_122) | ~accessible_world(skc15, V_669)))). % 13.83/4.97 tff(c_1961, plain, (![V_152, V_610]: (forename(V_152, skc25) | ~accessible_world(V_610, V_152) | ~accessible_world(skc15, V_610)))). % 13.83/4.97 tff(c_2809, plain, (![W_759]: (skc28=W_759 | ~forename(skc15, W_759) | ~of(skc15, W_759, skc29)))). % 13.83/4.97 tff(c_1885, plain, (![V_104, V_591]: (proposition(V_104, skc26) | ~accessible_world(V_591, V_104) | ~accessible_world(skc15, V_591)))). % 13.83/4.97 tff(c_2537, plain, (![V_74, V_708]: (smoke(V_74, skc22) | ~accessible_world(V_708, V_74) | ~accessible_world(skc16, V_708)))). % 13.83/4.97 tff(c_1949, plain, (![V_152, V_607]: (forename(V_152, skc18) | ~accessible_world(V_607, V_152) | ~accessible_world(skc15, V_607)))). % 13.83/4.97 tff(c_2063, plain, (![V_161, V_626]: (jules_forename(V_161, skc20) | ~accessible_world(V_626, V_161) | ~accessible_world(skc15, V_626)))). % 13.83/4.97 tff(c_2626, plain, (![V_77, V_723]: (event(V_77, skc27) | ~accessible_world(V_723, V_77) | ~accessible_world(skc15, V_723)))). % 13.83/4.97 tff(c_1932, plain, (![V_98, V_603]: (present(V_98, skc22) | ~accessible_world(V_603, V_98) | ~accessible_world(skc16, V_603)))). % 13.83/4.97 tff(c_2071, plain, (![V_161, V_627]: (jules_forename(V_161, skc25) | ~accessible_world(V_627, V_161) | ~accessible_world(skc15, V_627)))). % 13.83/4.97 tff(c_2661, plain, (![V_158, V_730]: (vincent_forename(V_158, skc28) | ~accessible_world(V_730, V_158) | ~accessible_world(skc15, V_730)))). % 13.83/4.97 tff(c_2709, plain, (![V_733, V_258, U_257]: (singleton(V_733, V_258) | ~accessible_world(U_257, V_733) | ~eventuality(U_257, V_258)))). % 13.83/4.97 tff(c_1924, plain, (![V_98, V_601]: (present(V_98, skc17) | ~accessible_world(V_601, V_98) | ~accessible_world(skc15, V_601)))). % 13.83/4.97 tff(c_2800, plain, (![W_759]: (skc25=W_759 | ~forename(skc15, W_759) | ~of(skc15, W_759, skc24)))). % 13.83/4.97 tff(c_2803, plain, (![W_759]: (skc20=W_759 | ~forename(skc15, W_759) | ~of(skc15, W_759, skc21)))). % 13.83/4.97 tff(c_4570, plain, (![V_940]: (skc16=V_940 | ~theme(skc15, skc17, V_940) | ~proposition(skc15, V_940)))). % 13.83/4.97 tff(c_1953, plain, (![V_152, V_608]: (forename(V_152, skc20) | ~accessible_world(V_608, V_152) | ~accessible_world(skc15, V_608)))). % 13.83/4.97 tff(c_2148, plain, (![V_119, V_639]: (state(V_119, skc23) | ~accessible_world(V_639, V_119) | ~accessible_world(skc15, V_639)))). % 13.83/4.97 tff(c_1877, plain, (![V_104, V_590]: (proposition(V_104, skc16) | ~accessible_world(V_590, V_104) | ~accessible_world(skc15, V_590)))). % 13.83/4.97 tff(c_1928, plain, (![V_98, V_602]: (present(V_98, skc27) | ~accessible_world(V_602, V_98) | ~accessible_world(skc15, V_602)))). % 13.83/4.97 tff(c_2329, plain, (![V_122, V_668]: (man(V_122, skc19) | ~accessible_world(V_668, V_122) | ~accessible_world(skc15, V_668)))). % 13.83/4.97 tff(c_1957, plain, (![V_152, V_609]: (forename(V_152, skc28) | ~accessible_world(V_609, V_152) | ~accessible_world(skc15, V_609)))). % 13.83/4.97 tff(c_2353, plain, (![V_122, V_670]: (man(V_122, skc24) | ~accessible_world(V_670, V_122) | ~accessible_world(skc15, V_670)))). % 13.83/4.97 tff(c_2618, plain, (![V_77, V_722]: (event(V_77, skc17) | ~accessible_world(V_722, V_77) | ~accessible_world(skc15, V_722)))). % 13.83/4.97 tff(c_2806, plain, (![W_759]: (skc18=W_759 | ~forename(skc15, W_759) | ~of(skc15, W_759, skc19)))). % 13.83/4.97 tff(c_4706, plain, (![V_947]: (skc26=V_947 | ~theme(skc15, skc27, V_947) | ~proposition(skc15, V_947)))). % 13.83/4.97 tff(c_4869, plain, (~accessible_world(skc15, skc15))). % 13.83/4.97 tff(c_2317, plain, (![V_122, V_667]: (man(V_122, skc29) | ~accessible_world(V_667, V_122) | ~accessible_world(skc15, V_667)))). % 13.83/4.97 tff(c_4657, plain, (![V_944]: (~abstraction(V_944, skc19) | ~accessible_world(skc26, V_944)))). % 13.83/4.97 tff(c_4600, plain, (![V_942]: (~abstraction(V_942, skc19) | ~accessible_world(skc16, V_942)))). % 13.83/4.97 tff(c_2828, plain, (![W_768, V_766, Y_767, U_196]: (W_768=V_766 | ~agent(skc26, Y_767, U_196) | ~theme(skc26, Y_767, W_768) | ~think_believe_consider(skc26, Y_767) | ~think_believe_consider(skc26, skf1(U_196)) | ~theme(skc26, skf1(U_196), V_766) | ~proposition(skc26, W_768) | ~proposition(skc26, V_766) | ~man(skc26, U_196)))). % 13.83/4.97 tff(c_4685, plain, (![V_945]: (~abstraction(V_945, skc21) | ~accessible_world(skc16, V_945)))). % 13.83/4.97 tff(c_4629, plain, (![V_943]: (~abstraction(V_943, skc24) | ~accessible_world(skc16, V_943)))). % 13.83/4.97 tff(c_4764, plain, (![V_950]: (~abstraction(V_950, skc29) | ~accessible_world(skc16, V_950)))). % 13.83/4.97 tff(c_4736, plain, (![V_949]: (~abstraction(V_949, skc29) | ~accessible_world(skc26, V_949)))). % 13.83/4.97 tff(c_4792, plain, (![V_951]: (~abstraction(V_951, skc24) | ~accessible_world(skc26, V_951)))). % 13.83/4.97 tff(c_2707, plain, (![V_733, V_212, U_211]: (singleton(V_733, V_212) | ~accessible_world(U_211, V_733) | ~abstraction(U_211, V_212)))). % 13.83/4.97 tff(c_4820, plain, (![V_952]: (~abstraction(V_952, skc21) | ~accessible_world(skc26, V_952)))). % 13.83/4.97 tff(c_4822, plain, (~think_believe_consider(skc16, skc22))). % 13.83/4.97 tff(c_3606, plain, (![V_131]: (entity(V_131, skc21) | ~accessible_world(skc26, V_131)))). % 13.83/4.97 tff(c_3613, plain, (![V_131]: (entity(V_131, skc24) | ~accessible_world(skc26, V_131)))). % 13.83/4.97 tff(c_3784, plain, (![V_131]: (entity(V_131, skc29) | ~accessible_world(skc16, V_131)))). % 13.83/4.97 tff(c_3627, plain, (![V_131]: (entity(V_131, skc29) | ~accessible_world(skc26, V_131)))). % 13.83/4.97 tff(c_2832, plain, (![W_768, V_766, Y_767]: (W_768=V_766 | ~agent(skc15, Y_767, skc29) | ~theme(skc15, Y_767, W_768) | ~think_believe_consider(skc15, Y_767) | ~theme(skc15, skc27, V_766) | ~proposition(skc15, W_768) | ~proposition(skc15, V_766)))). % 13.83/4.97 tff(c_3763, plain, (![V_131]: (entity(V_131, skc21) | ~accessible_world(skc16, V_131)))). % 13.83/4.97 tff(c_3620, plain, (![V_131]: (entity(V_131, skc19) | ~accessible_world(skc26, V_131)))). % 13.83/4.97 tff(c_3770, plain, (![V_131]: (entity(V_131, skc24) | ~accessible_world(skc16, V_131)))). % 13.83/4.97 tff(c_3777, plain, (![V_131]: (entity(V_131, skc19) | ~accessible_world(skc16, V_131)))). % 13.83/4.97 tff(c_2835, plain, (![W_768, V_766, Y_767]: (W_768=V_766 | ~agent(skc15, Y_767, skc19) | ~theme(skc15, Y_767, W_768) | ~think_believe_consider(skc15, Y_767) | ~theme(skc15, skc17, V_766) | ~proposition(skc15, W_768) | ~proposition(skc15, V_766)))). % 13.83/4.97 tff(c_3678, plain, (![V_885]: (abstraction(skc16, V_885) | ~forename(skc15, V_885)))). % 13.83/4.97 tff(c_2729, plain, (![V_738, U_196]: (agent(V_738, skf1(U_196), U_196) | ~accessible_world(skc26, V_738) | ~man(skc26, U_196)))). % 13.83/4.97 tff(c_4490, plain, (![V_195]: (~entity(skc15, skf1(V_195))))). % 13.83/4.97 tff(c_4012, plain, (![V_4]: (~entity(skc15, V_4) | ~event(skc26, V_4)))). % 13.83/4.97 tff(c_4454, plain, (~entity(skc15, skc22))). % 13.83/4.97 tff(c_4062, plain, (![V_4]: (~entity(skc15, V_4) | ~event(skc16, V_4)))). % 13.83/4.97 tff(c_4360, plain, (![V_930]: (~male(skc16, V_930) | ~eventuality(skc15, V_930)))). % 13.83/4.97 tff(c_4352, plain, (![V_929]: (~male(skc26, V_929) | ~eventuality(skc15, V_929)))). % 13.83/4.97 tff(c_4344, plain, (![V_927]: (unisex(skc16, V_927) | ~eventuality(skc15, V_927)))). % 13.83/4.97 tff(c_4343, plain, (![V_927]: (unisex(skc26, V_927) | ~eventuality(skc15, V_927)))). % 13.83/4.97 tff(c_4337, plain, (~entity(skc16, skc27))). % 13.83/4.97 tff(c_2579, plain, (![V_715, V_14, U_13]: (unisex(V_715, V_14) | ~accessible_world(U_13, V_715) | ~eventuality(U_13, V_14)))). % 13.83/4.97 tff(c_4336, plain, (~entity(skc16, skc17))). % 13.83/4.97 tff(c_4215, plain, (![V_922]: (~entity(skc16, V_922) | ~event(skc15, V_922)))). % 13.83/4.97 tff(c_4299, plain, (~entity(skc26, skc27))). % 13.83/4.97 tff(c_4298, plain, (~entity(skc26, skc17))). % 13.83/4.97 tff(c_4167, plain, (![V_921]: (~entity(skc26, V_921) | ~event(skc15, V_921)))). % 13.83/4.97 tff(c_3658, plain, (![V_881]: (abstraction(skc26, V_881) | ~forename(skc15, V_881)))). % 13.83/4.97 tff(c_4120, plain, (![V_919]: (eventuality(skc16, V_919) | ~event(skc15, V_919)))). % 13.83/4.97 tff(c_4119, plain, (![V_919]: (eventuality(skc26, V_919) | ~event(skc15, V_919)))). % 13.83/4.97 tff(c_4113, plain, (~abstraction(skc15, skc22))). % 13.83/4.97 tff(c_2239, plain, (![V_653, V_4, U_3]: (eventuality(V_653, V_4) | ~accessible_world(U_3, V_653) | ~event(U_3, V_4)))). % 13.83/4.97 tff(c_3968, plain, (![V_4]: (~abstraction(skc15, V_4) | ~event(skc16, V_4)))). % 13.83/4.97 tff(c_4076, plain, (~entity(skc16, skc23))). % 13.83/4.97 tff(c_3837, plain, (![V_42]: (~eventuality(skc15, V_42) | ~entity(skc16, V_42)))). % 13.83/4.97 tff(c_3999, plain, (![V_911]: (~eventuality(skc16, V_911) | ~entity(skc15, V_911)))). % 13.83/4.97 tff(c_4048, plain, (![V_195]: (~abstraction(skc15, skf1(V_195))))). % 13.83/4.97 tff(c_3865, plain, (![V_4]: (~abstraction(skc15, V_4) | ~event(skc26, V_4)))). % 13.83/4.97 tff(c_3987, plain, (![V_910]: (~eventuality(skc26, V_910) | ~entity(skc15, V_910)))). % 13.83/4.97 tff(c_3975, plain, (![V_908]: (existent(skc16, V_908) | ~entity(skc15, V_908)))). % 13.83/4.97 tff(c_3974, plain, (![V_908]: (existent(skc26, V_908) | ~entity(skc15, V_908)))). % 13.83/4.97 tff(c_2371, plain, (![V_672, V_42, U_41]: (existent(V_672, V_42) | ~accessible_world(U_41, V_672) | ~entity(U_41, V_42)))). % 13.83/4.97 tff(c_3830, plain, (![V_900]: (~eventuality(skc16, V_900) | ~abstraction(skc15, V_900)))). % 13.83/4.97 tff(c_3811, plain, (![V_899]: (~entity(skc26, V_899) | ~abstraction(skc15, V_899)))). % 13.83/4.97 tff(c_3831, plain, (![V_900]: (~entity(skc16, V_900) | ~abstraction(skc15, V_900)))). % 13.83/4.97 tff(c_3810, plain, (![V_899]: (~eventuality(skc26, V_899) | ~abstraction(skc15, V_899)))). % 13.83/4.97 tff(c_3851, plain, (~entity(skc26, skc23))). % 13.83/4.97 tff(c_3719, plain, (![V_42]: (~eventuality(skc15, V_42) | ~entity(skc26, V_42)))). % 13.83/4.97 tff(c_3709, plain, (![V_892]: (~existent(skc16, V_892) | ~eventuality(skc15, V_892)))). % 13.83/4.97 tff(c_3791, plain, (![V_897]: (general(skc16, V_897) | ~abstraction(skc15, V_897)))). % 13.83/4.97 tff(c_3790, plain, (![V_897]: (general(skc26, V_897) | ~abstraction(skc15, V_897)))). % 13.83/4.97 tff(c_2213, plain, (![V_648, V_24, U_23]: (general(V_648, V_24) | ~accessible_world(U_23, V_648) | ~abstraction(U_23, V_24)))). % 13.83/4.97 tff(c_3756, plain, (entity(skc16, skc29))). % 13.83/4.97 tff(c_3755, plain, (entity(skc16, skc19))). % 13.83/4.97 tff(c_3754, plain, (entity(skc16, skc24))). % 13.83/4.97 tff(c_3753, plain, (entity(skc16, skc21))). % 13.83/4.97 tff(c_3562, plain, (![V_874]: (entity(skc16, V_874) | ~human_person(skc15, V_874)))). % 13.83/4.97 tff(c_3701, plain, (![V_891]: (~existent(skc26, V_891) | ~eventuality(skc15, V_891)))). % 13.83/4.97 tff(c_3545, plain, (![V_873]: (impartial(skc26, V_873) | ~human_person(skc15, V_873)))). % 13.83/4.97 tff(c_3693, plain, (![V_889]: (nonexistent(skc16, V_889) | ~eventuality(skc15, V_889)))). % 13.83/4.97 tff(c_3692, plain, (![V_889]: (nonexistent(skc26, V_889) | ~eventuality(skc15, V_889)))). % 13.83/4.97 tff(c_2498, plain, (![V_699, V_12, U_11]: (nonexistent(V_699, V_12) | ~accessible_world(U_11, V_699) | ~eventuality(U_11, V_12)))). % 13.83/4.97 tff(c_3561, plain, (![V_874]: (impartial(skc16, V_874) | ~human_person(skc15, V_874)))). % 13.83/4.98 tff(c_3560, plain, (![V_874]: (living(skc16, V_874) | ~human_person(skc15, V_874)))). % 13.83/4.98 tff(c_3530, plain, (![V_872]: (relation(skc16, V_872) | ~forename(skc15, V_872)))). % 13.83/4.98 tff(c_3544, plain, (![V_873]: (living(skc26, V_873) | ~human_person(skc15, V_873)))). % 13.83/4.98 tff(c_3642, plain, (![V_879]: (singleton(skc26, V_879) | ~eventuality(skc15, V_879)))). % 13.83/4.98 tff(c_3650, plain, (![V_880]: (singleton(skc16, V_880) | ~eventuality(skc15, V_880)))). % 13.83/4.98 tff(c_3522, plain, (![V_871]: (relation(skc26, V_871) | ~forename(skc15, V_871)))). % 13.83/4.98 tff(c_3634, plain, (![V_877]: (thing(skc16, V_877) | ~eventuality(skc15, V_877)))). % 13.83/4.98 tff(c_3633, plain, (![V_877]: (thing(skc26, V_877) | ~eventuality(skc15, V_877)))). % 13.83/4.98 tff(c_1978, plain, (![V_613, V_6, U_5]: (thing(V_613, V_6) | ~accessible_world(U_5, V_613) | ~eventuality(U_5, V_6)))). % 13.83/4.98 tff(c_3599, plain, (entity(skc26, skc29))). % 13.83/4.98 tff(c_3598, plain, (entity(skc26, skc19))). % 13.83/4.98 tff(c_3597, plain, (entity(skc26, skc24))). % 13.83/4.98 tff(c_3596, plain, (entity(skc26, skc21))). % 13.83/4.98 tff(c_3546, plain, (![V_873]: (entity(skc26, V_873) | ~human_person(skc15, V_873)))). % 13.83/4.98 tff(c_3514, plain, (![V_869]: (organism(skc16, V_869) | ~human_person(skc15, V_869)))). % 13.83/4.98 tff(c_3513, plain, (![V_869]: (organism(skc26, V_869) | ~human_person(skc15, V_869)))). % 13.83/4.98 tff(c_3507, plain, (![V_866]: (relname(skc16, V_866) | ~forename(skc15, V_866)))). % 13.83/4.98 tff(c_3506, plain, (![V_866]: (relname(skc26, V_866) | ~forename(skc15, V_866)))). % 13.83/4.98 tff(c_1889, plain, (![V_592, V_34, U_33]: (organism(V_592, V_34) | ~accessible_world(U_33, V_592) | ~human_person(U_33, V_34)))). % 13.83/4.98 tff(c_2016, plain, (![V_618, V_54, U_53]: (relname(V_618, V_54) | ~accessible_world(U_53, V_618) | ~forename(U_53, V_54)))). % 13.83/4.98 tff(c_3500, plain, (~accessible_world(skc26, skc15))). % 13.83/4.98 tff(c_3499, plain, (~accessible_world(skc16, skc15))). % 13.83/4.98 tff(c_3452, plain, (![V_862]: (abstraction(skc16, V_862) | ~proposition(skc15, V_862)))). % 13.83/4.98 tff(c_3444, plain, (![V_861]: (abstraction(skc26, V_861) | ~proposition(skc15, V_861)))). % 13.83/4.98 tff(c_3436, plain, (![V_859]: (relation(skc16, V_859) | ~proposition(skc15, V_859)))). % 13.83/4.98 tff(c_3435, plain, (![V_859]: (relation(skc26, V_859) | ~proposition(skc15, V_859)))). % 13.83/4.98 tff(c_2559, plain, (![V_711, V_16, U_15]: (relation(V_711, V_16) | ~accessible_world(U_15, V_711) | ~proposition(U_15, V_16)))). % 13.83/4.98 tff(c_3353, plain, (![V_4]: (~abstraction(skc26, V_4) | ~event(skc15, V_4)))). % 13.83/4.98 tff(c_3338, plain, (![V_4]: (~abstraction(skc16, V_4) | ~event(skc15, V_4)))). % 13.83/4.98 tff(c_3286, plain, (![V_24]: (~eventuality(skc15, V_24) | ~abstraction(skc26, V_24)))). % 13.83/4.98 tff(c_3315, plain, (![V_24]: (~eventuality(skc15, V_24) | ~abstraction(skc16, V_24)))). % 13.83/4.98 tff(c_3309, plain, (![V_850]: (singleton(skc16, V_850) | ~entity(skc15, V_850)))). % 13.83/4.98 tff(c_3301, plain, (![V_849]: (singleton(skc26, V_849) | ~entity(skc15, V_849)))). % 13.83/4.98 tff(c_3280, plain, (![V_844]: (~general(skc16, V_844) | ~eventuality(skc15, V_844)))). % 13.83/4.98 tff(c_3293, plain, (![V_847]: (thing(skc16, V_847) | ~entity(skc15, V_847)))). % 13.83/4.98 tff(c_3292, plain, (![V_847]: (thing(skc26, V_847) | ~entity(skc15, V_847)))). % 13.83/4.98 tff(c_1979, plain, (![V_613, V_38, U_37]: (thing(V_613, V_38) | ~accessible_world(U_37, V_613) | ~entity(U_37, V_38)))). % 13.83/4.98 tff(c_3272, plain, (![V_843]: (~general(skc26, V_843) | ~eventuality(skc15, V_843)))). % 13.83/4.98 tff(c_3264, plain, (![V_841]: (specific(skc16, V_841) | ~eventuality(skc15, V_841)))). % 13.83/4.98 tff(c_3263, plain, (![V_841]: (specific(skc26, V_841) | ~eventuality(skc15, V_841)))). % 13.83/4.98 tff(c_1869, plain, (![V_587, V_10, U_9]: (specific(V_587, V_10) | ~accessible_world(U_9, V_587) | ~eventuality(U_9, V_10)))). % 13.83/4.98 tff(c_3102, plain, (![V_24]: (~entity(skc15, V_24) | ~abstraction(skc16, V_24)))). % 13.83/4.98 tff(c_3162, plain, (![V_836]: (~male(skc16, V_836) | ~abstraction(skc15, V_836)))). % 13.83/4.98 tff(c_3154, plain, (![V_835]: (~male(skc26, V_835) | ~abstraction(skc15, V_835)))). % 13.83/4.98 tff(c_3146, plain, (![V_833]: (unisex(skc16, V_833) | ~abstraction(skc15, V_833)))). % 13.83/4.98 tff(c_3145, plain, (![V_833]: (unisex(skc26, V_833) | ~abstraction(skc15, V_833)))). % 13.83/4.98 tff(c_2580, plain, (![V_715, V_26, U_25]: (unisex(V_715, V_26) | ~accessible_world(U_25, V_715) | ~abstraction(U_25, V_26)))). % 13.83/4.98 tff(c_3088, plain, (![V_24]: (~entity(skc15, V_24) | ~abstraction(skc26, V_24)))). % 13.83/4.98 tff(c_3082, plain, (![V_826]: (~general(skc16, V_826) | ~entity(skc15, V_826)))). % 13.83/4.98 tff(c_3058, plain, (![V_823]: (singleton(skc26, V_823) | ~abstraction(skc15, V_823)))). % 13.83/4.98 tff(c_3066, plain, (![V_824]: (singleton(skc16, V_824) | ~abstraction(skc15, V_824)))). % 13.83/4.98 tff(c_3074, plain, (![V_825]: (~general(skc26, V_825) | ~entity(skc15, V_825)))). % 13.83/4.98 tff(c_3050, plain, (![V_821]: (specific(skc16, V_821) | ~entity(skc15, V_821)))). % 13.83/4.98 tff(c_3049, plain, (![V_821]: (specific(skc26, V_821) | ~entity(skc15, V_821)))). % 13.83/4.98 tff(c_3043, plain, (![V_818]: (thing(skc16, V_818) | ~abstraction(skc15, V_818)))). % 13.83/4.98 tff(c_3042, plain, (![V_818]: (thing(skc26, V_818) | ~abstraction(skc15, V_818)))). % 13.83/4.98 tff(c_1868, plain, (![V_587, V_40, U_39]: (specific(V_587, V_40) | ~accessible_world(U_39, V_587) | ~entity(U_39, V_40)))). % 13.83/4.98 tff(c_1980, plain, (![V_613, V_20, U_19]: (thing(V_613, V_20) | ~accessible_world(U_19, V_613) | ~abstraction(U_19, V_20)))). % 13.83/4.98 tff(c_2978, plain, (![V_814]: (~human(skc16, V_814) | ~abstraction(skc15, V_814)))). % 13.83/4.98 tff(c_2970, plain, (![V_813]: (~human(skc26, V_813) | ~abstraction(skc15, V_813)))). % 13.83/4.98 tff(c_2962, plain, (![V_811]: (nonhuman(skc16, V_811) | ~abstraction(skc15, V_811)))). % 13.83/4.98 tff(c_2961, plain, (![V_811]: (nonhuman(skc26, V_811) | ~abstraction(skc15, V_811)))). % 13.83/4.98 tff(c_2486, plain, (![V_695, V_22, U_21]: (nonhuman(V_695, V_22) | ~accessible_world(U_21, V_695) | ~abstraction(U_21, V_22)))). % 13.83/4.98 tff(c_2787, plain, (![V_757]: (be(V_757, skc23, skc24, skc24) | ~accessible_world(skc15, V_757)))). % 13.83/4.98 tff(c_2902, plain, (![V_795, V_796]: (~entity(V_795, skf1(V_796)) | ~accessible_world(skc26, V_795)))). % 13.83/4.98 tff(c_2904, plain, (![V_795, V_796]: (~abstraction(V_795, skf1(V_796)) | ~accessible_world(skc26, V_795)))). % 13.83/4.98 tff(c_2766, plain, (![V_748]: (of(V_748, skc20, skc21) | ~accessible_world(skc15, V_748)))). % 13.83/4.98 tff(c_2529, plain, (![V_705, V_191]: (smoke(V_705, skf1(V_191)) | ~accessible_world(skc26, V_705)))). % 13.83/4.98 tff(c_2730, plain, (![V_738]: (agent(V_738, skc22, skc21) | ~accessible_world(skc16, V_738)))). % 13.83/4.98 tff(c_2731, plain, (![V_738]: (agent(V_738, skc27, skc29) | ~accessible_world(skc15, V_738)))). % 13.83/4.98 tff(c_1917, plain, (![V_598, V_193]: (present(V_598, skf1(V_193)) | ~accessible_world(skc26, V_598)))). % 13.83/4.98 tff(c_2732, plain, (![V_738]: (agent(V_738, skc17, skc19) | ~accessible_world(skc15, V_738)))). % 13.83/4.98 tff(c_2607, plain, (![V_719, V_195]: (event(V_719, skf1(V_195)) | ~accessible_world(skc26, V_719)))). % 13.83/4.98 tff(c_2744, plain, (![V_742]: (theme(V_742, skc27, skc26) | ~accessible_world(skc15, V_742)))). % 13.83/4.98 tff(c_2510, plain, (![V_110]: (abstraction(V_110, skc25) | ~accessible_world(skc26, V_110)))). % 13.83/4.98 tff(c_2513, plain, (![V_110]: (abstraction(V_110, skc25) | ~accessible_world(skc16, V_110)))). % 13.83/4.98 tff(c_2745, plain, (![V_742]: (theme(V_742, skc17, skc16) | ~accessible_world(skc15, V_742)))). % 13.83/4.98 tff(c_2735, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc26, V_110)))). % 13.83/4.98 tff(c_2738, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc16, V_110)))). % 13.83/4.98 tff(c_2774, plain, (![V_110]: (abstraction(V_110, skc20) | ~accessible_world(skc16, V_110)))). % 13.83/4.98 tff(c_2565, plain, (![V_110]: (abstraction(V_110, skc28) | ~accessible_world(skc26, V_110)))). % 13.83/4.98 tff(c_2771, plain, (![V_110]: (abstraction(V_110, skc20) | ~accessible_world(skc26, V_110)))). % 13.83/4.98 tff(c_2562, plain, (![V_110]: (abstraction(V_110, skc28) | ~accessible_world(skc16, V_110)))). % 13.83/4.98 tff(c_2442, plain, (![U_3]: (~accessible_world(skc15, U_3) | ~event(U_3, skc24)))). % 13.83/4.98 tff(c_2188, plain, (![V_642]: (abstraction(V_642, skc16) | ~accessible_world(skc16, V_642)))). % 13.83/4.98 tff(c_2765, plain, (![V_748]: (of(V_748, skc25, skc24) | ~accessible_world(skc15, V_748)))). % 13.83/4.98 tff(c_2189, plain, (![V_642]: (abstraction(V_642, skc16) | ~accessible_world(skc26, V_642)))). % 13.83/4.98 tff(c_2543, plain, (![V_709]: (~abstraction(V_709, skc22) | ~accessible_world(skc16, V_709)))). % 13.83/4.98 tff(c_2182, plain, (![V_642]: (abstraction(V_642, skc26) | ~accessible_world(skc26, V_642)))). % 13.83/4.98 tff(c_2767, plain, (![V_748]: (of(V_748, skc18, skc19) | ~accessible_world(skc15, V_748)))). % 13.83/4.98 tff(c_2691, plain, (![V_719]: (~entity(V_719, skc27) | ~accessible_world(skc15, V_719)))). % 13.83/4.98 tff(c_2523, plain, (![U_3]: (~accessible_world(skc15, U_3) | ~event(U_3, skc21)))). % 13.83/4.98 tff(c_2436, plain, (![U_3]: (~accessible_world(skc15, U_3) | ~event(U_3, skc29)))). % 13.83/4.98 tff(c_2854, plain, (~abstraction(skc16, skc27))). % 13.83/4.98 tff(c_2853, plain, (~abstraction(skc26, skc27))). % 13.83/4.98 tff(c_2627, plain, (![V_723]: (~abstraction(V_723, skc27) | ~accessible_world(skc15, V_723)))). % 13.83/4.98 tff(c_2768, plain, (![V_748]: (of(V_748, skc28, skc29) | ~accessible_world(skc15, V_748)))). % 13.83/4.98 tff(c_2693, plain, (![V_708]: (~entity(V_708, skc22) | ~accessible_world(skc16, V_708)))). % 13.83/4.98 tff(c_2183, plain, (![V_642]: (abstraction(V_642, skc26) | ~accessible_world(skc16, V_642)))). % 13.83/4.98 tff(c_2405, plain, (![U_3]: (~accessible_world(skc15, U_3) | ~event(U_3, skc19)))). % 13.83/4.98 tff(c_142, plain, (![Z_186, V_189, X_187, Y_188, U_185, W_184]: (W_184=V_189 | ~agent(U_185, X_187, Z_186) | ~agent(U_185, Y_188, Z_186) | ~theme(U_185, Y_188, W_184) | ~think_believe_consider(U_185, Y_188) | ~think_believe_consider(U_185, X_187) | ~theme(U_185, X_187, V_189) | ~proposition(U_185, W_184) | ~proposition(U_185, V_189)))). % 13.83/4.98 tff(c_2818, plain, (~abstraction(skc16, skc17))). % 13.83/4.98 tff(c_2817, plain, (~abstraction(skc26, skc17))). % 13.83/4.98 tff(c_2619, plain, (![V_722]: (~abstraction(V_722, skc17) | ~accessible_world(skc15, V_722)))). % 13.83/4.98 tff(c_140, plain, (![W_182, V_181, U_180, X_183]: (W_182=V_181 | ~entity(U_180, X_183) | ~of(U_180, V_181, X_183) | ~forename(U_180, W_182) | ~of(U_180, W_182, X_183) | ~forename(U_180, V_181)))). % 13.83/4.98 tff(c_2692, plain, (![V_719]: (~entity(V_719, skc17) | ~accessible_world(skc15, V_719)))). % 13.83/4.98 tff(c_2783, plain, (~abstraction(skc16, skc21))). % 13.83/4.98 tff(c_2782, plain, (~abstraction(skc26, skc21))). % 13.83/4.98 tff(c_138, plain, (![X_177, Y_178, U_176, W_175, V_179]: (be(V_179, W_175, X_177, Y_178) | ~be(U_176, W_175, X_177, Y_178) | ~accessible_world(U_176, V_179)))). % 13.83/4.98 tff(c_2293, plain, (![V_663]: (~abstraction(V_663, skc21) | ~accessible_world(skc15, V_663)))). % 13.83/4.98 tff(c_2755, plain, (abstraction(skc16, skc20))). % 13.83/4.98 tff(c_2754, plain, (abstraction(skc26, skc20))). % 13.83/4.98 tff(c_136, plain, (![V_172, W_173, X_174, U_171]: (of(V_172, W_173, X_174) | ~of(U_171, W_173, X_174) | ~accessible_world(U_171, V_172)))). % 13.83/4.98 tff(c_2044, plain, (![V_604]: (abstraction(V_604, skc20) | ~accessible_world(skc15, V_604)))). % 13.83/4.98 tff(c_2159, plain, (![V_641]: (~entity(V_641, skc23) | ~accessible_world(skc15, V_641)))). % 13.83/4.98 tff(c_134, plain, (![V_168, W_169, X_170, U_167]: (theme(V_168, W_169, X_170) | ~theme(U_167, W_169, X_170) | ~accessible_world(U_167, V_168)))). % 13.83/4.98 tff(c_2719, plain, (abstraction(skc16, skc18))). % 13.83/4.98 tff(c_2718, plain, (abstraction(skc26, skc18))). % 13.83/4.98 tff(c_132, plain, (![V_164, W_165, X_166, U_163]: (agent(V_164, W_165, X_166) | ~agent(U_163, W_165, X_166) | ~accessible_world(U_163, V_164)))). % 13.83/4.98 tff(c_2045, plain, (![V_604]: (abstraction(V_604, skc18) | ~accessible_world(skc15, V_604)))). % 13.83/4.98 tff(c_2695, plain, (![V_195]: (~entity(skc26, skf1(V_195))))). % 13.83/4.98 tff(c_2698, plain, (~entity(skc15, skc27))). % 13.83/4.98 tff(c_2699, plain, (~entity(skc16, skc22))). % 13.83/4.98 tff(c_2697, plain, (~entity(skc15, skc17))). % 13.83/4.98 tff(c_80, plain, (![V_86, W_87, U_85]: (singleton(V_86, W_87) | ~singleton(U_85, W_87) | ~accessible_world(U_85, V_86)))). % 13.83/4.98 tff(c_1970, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 13.83/4.98 tff(c_2646, plain, (![V_726]: (vincent_forename(V_726, skc28) | ~accessible_world(skc15, V_726)))). % 13.83/4.98 tff(c_2645, plain, (![V_726]: (vincent_forename(V_726, skc18) | ~accessible_world(skc15, V_726)))). % 13.83/4.98 tff(c_128, plain, (![V_158, W_159, U_157]: (vincent_forename(V_158, W_159) | ~vincent_forename(U_157, W_159) | ~accessible_world(U_157, V_158)))). % 13.83/4.98 tff(c_2100, plain, (![V_632]: (animate(V_632, skc29) | ~accessible_world(skc15, V_632)))). % 13.83/4.99 tff(c_1809, plain, (![V_131]: (entity(V_131, skc19) | ~accessible_world(skc15, V_131)))). % 13.83/4.99 tff(c_2610, plain, (![V_719]: (event(V_719, skc27) | ~accessible_world(skc15, V_719)))). % 13.83/4.99 tff(c_2609, plain, (![V_719]: (event(V_719, skc17) | ~accessible_world(skc15, V_719)))). % 13.83/4.99 tff(c_74, plain, (![V_77, W_78, U_76]: (event(V_77, W_78) | ~event(U_76, W_78) | ~accessible_world(U_76, V_77)))). % 13.83/4.99 tff(c_2589, plain, (~abstraction(skc16, skc29))). % 13.83/4.99 tff(c_2588, plain, (~abstraction(skc26, skc29))). % 13.83/4.99 tff(c_2366, plain, (![V_671]: (~abstraction(V_671, skc29) | ~accessible_world(skc15, V_671)))). % 13.83/4.99 tff(c_86, plain, (![V_95, W_96, U_94]: (unisex(V_95, W_96) | ~unisex(U_94, W_96) | ~accessible_world(U_94, V_95)))). % 13.83/4.99 tff(c_2012, plain, (![V_617]: (human(V_617, skc21) | ~accessible_world(skc15, V_617)))). % 13.83/4.99 tff(c_2551, plain, (abstraction(skc26, skc28))). % 13.83/4.99 tff(c_2552, plain, (abstraction(skc16, skc28))). % 13.83/4.99 tff(c_94, plain, (![V_107, W_108, U_106]: (relation(V_107, W_108) | ~relation(U_106, W_108) | ~accessible_world(U_106, V_107)))). % 13.83/4.99 tff(c_2043, plain, (![V_604]: (abstraction(V_604, skc28) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_2538, plain, (![V_708]: (event(V_708, skc22) | ~accessible_world(skc16, V_708)))). % 13.83/4.99 tff(c_2530, plain, (![V_705]: (smoke(V_705, skc22) | ~accessible_world(skc16, V_705)))). % 13.83/4.99 tff(c_72, plain, (![V_74, W_75, U_73]: (smoke(V_74, W_75) | ~smoke(U_73, W_75) | ~accessible_world(U_73, V_74)))). % 13.83/4.99 tff(c_2294, plain, (![V_663]: (~eventuality(V_663, skc21) | ~accessible_world(skc15, V_663)))). % 13.83/4.99 tff(c_1826, plain, (![V_576]: (animate(V_576, skc21) | ~accessible_world(skc15, V_576)))). % 13.83/4.99 tff(c_2507, plain, (abstraction(skc16, skc25))). % 13.83/4.99 tff(c_2506, plain, (abstraction(skc26, skc25))). % 13.83/4.99 tff(c_2042, plain, (![V_604]: (abstraction(V_604, skc25) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_84, plain, (![V_92, W_93, U_91]: (nonexistent(V_92, W_93) | ~nonexistent(U_91, W_93) | ~accessible_world(U_91, V_92)))). % 13.83/4.99 tff(c_1812, plain, (![V_131]: (entity(V_131, skc29) | ~accessible_world(skc15, V_131)))). % 13.83/4.99 tff(c_2482, plain, (~abstraction(skc16, skc24))). % 13.83/4.99 tff(c_2481, plain, (~abstraction(skc26, skc24))). % 13.83/4.99 tff(c_98, plain, (![V_113, W_114, U_112]: (nonhuman(V_113, W_114) | ~nonhuman(U_112, W_114) | ~accessible_world(U_112, V_113)))). % 13.83/4.99 tff(c_2382, plain, (![V_675]: (~abstraction(V_675, skc24) | ~accessible_world(skc15, V_675)))). % 13.83/4.99 tff(c_2427, plain, (![V_682]: (human(V_682, skc29) | ~accessible_world(skc15, V_682)))). % 13.83/4.99 tff(c_2429, plain, (![V_682]: (human(V_682, skc24) | ~accessible_world(skc15, V_682)))). % 13.83/4.99 tff(c_2449, plain, (![V_687]: (think_believe_consider(V_687, skc27) | ~accessible_world(skc15, V_687)))). % 13.83/4.99 tff(c_2448, plain, (![V_687]: (think_believe_consider(V_687, skc17) | ~accessible_world(skc15, V_687)))). % 13.83/4.99 tff(c_90, plain, (![V_101, W_102, U_100]: (think_believe_consider(V_101, W_102) | ~think_believe_consider(U_100, W_102) | ~accessible_world(U_100, V_101)))). % 13.83/4.99 tff(c_2383, plain, (![V_675]: (~eventuality(V_675, skc24) | ~accessible_world(skc15, V_675)))). % 13.83/4.99 tff(c_2367, plain, (![V_671]: (~eventuality(V_671, skc29) | ~accessible_world(skc15, V_671)))). % 13.83/4.99 tff(c_2414, plain, (~abstraction(skc16, skc19))). % 13.83/4.99 tff(c_118, plain, (![V_143, W_144, U_142]: (human(V_143, W_144) | ~human(U_142, W_144) | ~accessible_world(U_142, V_143)))). % 13.83/4.99 tff(c_2413, plain, (~abstraction(skc26, skc19))). % 13.83/4.99 tff(c_2394, plain, (![V_676]: (~abstraction(V_676, skc19) | ~accessible_world(skc15, V_676)))). % 13.83/4.99 tff(c_2395, plain, (![V_676]: (~eventuality(V_676, skc19) | ~accessible_world(skc15, V_676)))). % 13.83/4.99 tff(c_114, plain, (![V_137, W_138, U_136]: (impartial(V_137, W_138) | ~impartial(U_136, W_138) | ~accessible_world(U_136, V_137)))). % 13.83/4.99 tff(c_2330, plain, (![V_668]: (male(V_668, skc19) | ~accessible_world(skc15, V_668)))). % 13.83/4.99 tff(c_2279, plain, (![V_659]: (male(V_659, skc24) | ~accessible_world(skc15, V_659)))). % 13.83/4.99 tff(c_112, plain, (![V_134, W_135, U_133]: (existent(V_134, W_135) | ~existent(U_133, W_135) | ~accessible_world(U_133, V_134)))). % 13.83/4.99 tff(c_2281, plain, (![V_659]: (male(V_659, skc29) | ~accessible_world(skc15, V_659)))). % 13.83/4.99 tff(c_2307, plain, (![V_664]: (man(V_664, skc24) | ~accessible_world(skc15, V_664)))). % 13.83/4.99 tff(c_2306, plain, (![V_664]: (man(V_664, skc21) | ~accessible_world(skc15, V_664)))). % 13.83/4.99 tff(c_2305, plain, (![V_664]: (man(V_664, skc19) | ~accessible_world(skc15, V_664)))). % 13.83/4.99 tff(c_2304, plain, (![V_664]: (man(V_664, skc29) | ~accessible_world(skc15, V_664)))). % 13.83/4.99 tff(c_104, plain, (![V_122, W_123, U_121]: (man(V_122, W_123) | ~man(U_121, W_123) | ~accessible_world(U_121, V_122)))). % 13.83/4.99 tff(c_2278, plain, (![V_659]: (male(V_659, skc21) | ~accessible_world(skc15, V_659)))). % 13.83/4.99 tff(c_2264, plain, (![V_195]: (~abstraction(skc26, skf1(V_195))))). % 13.83/4.99 tff(c_2268, plain, (~abstraction(skc16, skc22))). % 13.83/4.99 tff(c_122, plain, (![V_149, W_150, U_148]: (male(V_149, W_150) | ~male(U_148, W_150) | ~accessible_world(U_148, V_149)))). % 13.83/4.99 tff(c_2267, plain, (~abstraction(skc15, skc27))). % 13.83/4.99 tff(c_2266, plain, (~abstraction(skc15, skc17))). % 13.83/4.99 tff(c_1898, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 13.83/4.99 tff(c_1823, plain, (![V_576]: (animate(V_576, skc24) | ~accessible_world(skc15, V_576)))). % 13.83/4.99 tff(c_76, plain, (![V_80, W_81, U_79]: (eventuality(V_80, W_81) | ~eventuality(U_79, W_81) | ~accessible_world(U_79, V_80)))). % 13.83/4.99 tff(c_1806, plain, (![V_571]: (entity(V_571, skc21) | ~accessible_world(skc15, V_571)))). % 13.83/4.99 tff(c_1805, plain, (![V_571]: (entity(V_571, skc24) | ~accessible_world(skc15, V_571)))). % 13.83/4.99 tff(c_100, plain, (![V_116, W_117, U_115]: (general(V_116, W_117) | ~general(U_115, W_117) | ~accessible_world(U_115, V_116)))). % 13.83/4.99 tff(c_2116, plain, (![V_633]: (animate(V_633, skc19) | ~accessible_world(skc15, V_633)))). % 13.83/4.99 tff(c_2205, plain, (~abstraction(skc16, skc23))). % 13.83/4.99 tff(c_2204, plain, (~abstraction(skc26, skc23))). % 13.83/4.99 tff(c_2160, plain, (![V_641]: (~abstraction(V_641, skc23) | ~accessible_world(skc15, V_641)))). % 13.83/4.99 tff(c_2117, plain, (![V_633]: (human(V_633, skc19) | ~accessible_world(skc15, V_633)))). % 13.83/4.99 tff(c_96, plain, (![V_110, W_111, U_109]: (abstraction(V_110, W_111) | ~abstraction(U_109, W_111) | ~accessible_world(U_109, V_110)))). % 13.83/4.99 tff(c_2150, plain, (![V_639]: (eventuality(V_639, skc23) | ~accessible_world(skc15, V_639)))). % 13.83/4.99 tff(c_2149, plain, (![V_639]: (event(V_639, skc23) | ~accessible_world(skc15, V_639)))). % 13.83/4.99 tff(c_2138, plain, (![V_636]: (state(V_636, skc23) | ~accessible_world(skc15, V_636)))). % 13.83/4.99 tff(c_102, plain, (![V_119, W_120, U_118]: (state(V_119, W_120) | ~state(U_118, W_120) | ~accessible_world(U_118, V_119)))). % 13.83/4.99 tff(c_1848, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.99 tff(c_1757, plain, (![V_561]: (human_person(V_561, skc19) | ~accessible_world(skc15, V_561)))). % 13.83/4.99 tff(c_1758, plain, (![V_561]: (human_person(V_561, skc29) | ~accessible_world(skc15, V_561)))). % 13.83/4.99 tff(c_2080, plain, (abstraction(skc26, skc26))). % 13.83/4.99 tff(c_2081, plain, (abstraction(skc16, skc26))). % 13.83/4.99 tff(c_116, plain, (![V_140, W_141, U_139]: (living(V_140, W_141) | ~living(U_139, W_141) | ~accessible_world(U_139, V_140)))). % 13.83/4.99 tff(c_1884, plain, (![V_591]: (abstraction(V_591, skc26) | ~accessible_world(skc15, V_591)))). % 13.83/4.99 tff(c_2056, plain, (![V_623]: (jules_forename(V_623, skc25) | ~accessible_world(skc15, V_623)))). % 13.83/4.99 tff(c_2055, plain, (![V_623]: (jules_forename(V_623, skc20) | ~accessible_world(skc15, V_623)))). % 13.83/4.99 tff(c_130, plain, (![V_161, W_162, U_160]: (jules_forename(V_161, W_162) | ~jules_forename(U_160, W_162) | ~accessible_world(U_160, V_161)))). % 13.83/4.99 tff(c_2049, plain, (abstraction(skc15, skc25))). % 13.83/4.99 tff(c_2048, plain, (abstraction(skc15, skc28))). % 13.83/4.99 tff(c_2047, plain, (abstraction(skc15, skc20))). % 13.83/4.99 tff(c_2046, plain, (abstraction(skc15, skc18))). % 13.83/4.99 tff(c_1744, plain, (![U_557, V_558]: (abstraction(U_557, V_558) | ~forename(U_557, V_558)))). % 13.83/4.99 tff(c_126, plain, (![V_155, W_156, U_154]: (relname(V_155, W_156) | ~relname(U_154, W_156) | ~accessible_world(U_154, V_155)))). % 13.83/4.99 tff(c_1755, plain, (![V_561]: (human_person(V_561, skc21) | ~accessible_world(skc15, V_561)))). % 13.83/4.99 tff(c_1756, plain, (![V_561]: (human_person(V_561, skc24) | ~accessible_world(skc15, V_561)))). % 13.83/4.99 tff(c_1969, plain, (~entity(skc15, skc23))). % 13.83/4.99 tff(c_78, plain, (![V_83, W_84, U_82]: (thing(V_83, W_84) | ~thing(U_82, W_84) | ~accessible_world(U_82, V_83)))). % 13.83/4.99 tff(c_1739, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 13.83/4.99 tff(c_1945, plain, (![V_604]: (forename(V_604, skc25) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_1944, plain, (![V_604]: (forename(V_604, skc28) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_1943, plain, (![V_604]: (forename(V_604, skc20) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_1942, plain, (![V_604]: (forename(V_604, skc18) | ~accessible_world(skc15, V_604)))). % 13.83/4.99 tff(c_124, plain, (![V_152, W_153, U_151]: (forename(V_152, W_153) | ~forename(U_151, W_153) | ~accessible_world(U_151, V_152)))). % 13.83/4.99 tff(c_1920, plain, (![V_598]: (present(V_598, skc22) | ~accessible_world(skc16, V_598)))). % 13.83/4.99 tff(c_1919, plain, (![V_598]: (present(V_598, skc27) | ~accessible_world(skc15, V_598)))). % 13.83/4.99 tff(c_1918, plain, (![V_598]: (present(V_598, skc17) | ~accessible_world(skc15, V_598)))). % 13.83/4.99 tff(c_88, plain, (![V_98, W_99, U_97]: (present(V_98, W_99) | ~present(U_97, W_99) | ~accessible_world(U_97, V_98)))). % 13.83/4.99 tff(c_1907, plain, (abstraction(skc16, skc16))). % 13.83/4.99 tff(c_1906, plain, (abstraction(skc26, skc16))). % 13.83/4.99 tff(c_1876, plain, (![V_590]: (abstraction(V_590, skc16) | ~accessible_world(skc15, V_590)))). % 13.83/4.99 tff(c_1897, plain, (~abstraction(skc15, skc23))). % 13.83/4.99 tff(c_1853, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.83/4.99 tff(c_108, plain, (![V_128, W_129, U_127]: (organism(V_128, W_129) | ~organism(U_127, W_129) | ~accessible_world(U_127, V_128)))). % 13.83/4.99 tff(c_1782, plain, (![V_566]: (proposition(V_566, skc26) | ~accessible_world(skc15, V_566)))). % 13.83/4.99 tff(c_1781, plain, (![V_566]: (proposition(V_566, skc16) | ~accessible_world(skc15, V_566)))). % 13.83/4.99 tff(c_1862, plain, (abstraction(skc15, skc26))). % 13.83/4.99 tff(c_82, plain, (![V_89, W_90, U_88]: (specific(V_89, W_90) | ~specific(U_88, W_90) | ~accessible_world(U_88, V_89)))). % 13.83/4.99 tff(c_1861, plain, (abstraction(skc15, skc16))). % 13.83/4.99 tff(c_343, plain, (![U_15, V_16]: (abstraction(U_15, V_16) | ~proposition(U_15, V_16)))). % 13.83/4.99 tff(c_305, plain, (![U_235, V_236]: (~general(U_235, V_236) | ~eventuality(U_235, V_236)))). % 13.83/4.99 tff(c_348, plain, (![U_249, V_250]: (~general(U_249, V_250) | ~entity(U_249, V_250)))). % 13.83/4.99 tff(c_370, plain, (![U_253, V_254]: (~human(U_253, V_254) | ~abstraction(U_253, V_254)))). % 13.83/4.99 tff(c_120, plain, (![V_146, W_147, U_145]: (animate(V_146, W_147) | ~animate(U_145, W_147) | ~accessible_world(U_145, V_146)))). % 13.83/4.99 tff(c_246, plain, (![U_211, V_212]: (singleton(U_211, V_212) | ~abstraction(U_211, V_212)))). % 13.83/4.99 tff(c_1799, plain, (entity(skc15, skc29))). % 13.83/4.99 tff(c_1798, plain, (entity(skc15, skc19))). % 13.83/4.99 tff(c_110, plain, (![V_131, W_132, U_130]: (entity(V_131, W_132) | ~entity(U_130, W_132) | ~accessible_world(U_130, V_131)))). % 13.83/4.99 tff(c_1797, plain, (entity(skc15, skc24))). % 13.83/4.99 tff(c_1796, plain, (entity(skc15, skc21))). % 13.83/4.99 tff(c_389, plain, (![U_259, V_260]: (entity(U_259, V_260) | ~human_person(U_259, V_260)))). % 13.83/4.99 tff(c_1775, plain, (~abstraction(skc15, skc29))). % 13.83/4.99 tff(c_1774, plain, (~abstraction(skc15, skc19))). % 13.83/4.99 tff(c_92, plain, (![V_104, W_105, U_103]: (proposition(V_104, W_105) | ~proposition(U_103, W_105) | ~accessible_world(U_103, V_104)))). % 13.83/4.99 tff(c_1773, plain, (~abstraction(skc15, skc24))). % 13.83/4.99 tff(c_1772, plain, (~abstraction(skc15, skc21))). % 13.83/4.99 tff(c_338, plain, (![U_245, V_246]: (~male(U_245, V_246) | ~abstraction(U_245, V_246)))). % 13.83/4.99 tff(c_106, plain, (![V_125, W_126, U_124]: (human_person(V_125, W_126) | ~human_person(U_124, W_126) | ~accessible_world(U_124, V_125)))). % 13.83/4.99 tff(c_310, plain, (![U_237, V_238]: (singleton(U_237, V_238) | ~entity(U_237, V_238)))). % 13.83/4.99 tff(c_316, plain, (![U_241, V_242]: (relation(U_241, V_242) | ~forename(U_241, V_242)))). % 13.83/4.99 tff(c_264, plain, (![U_11, V_12]: (~existent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 13.83/4.99 tff(c_1733, plain, (~event(skc15, skc24))). % 13.83/4.99 tff(c_1715, plain, (~event(skc15, skc21))). % 13.83/4.99 tff(c_224, plain, (![U_196]: (agent(skc26, skf1(U_196), U_196) | ~man(skc26, U_196)))). % 13.83/4.99 tff(c_1719, plain, (~event(skc15, skc29))). % 13.83/4.99 tff(c_1723, plain, (~event(skc15, skc19))). % 13.83/4.99 tff(c_1443, plain, (~eventuality(skc15, skc24))). % 13.83/4.99 tff(c_1711, plain, (![V_191]: (smoke(skc26, skf1(V_191))))). % 13.83/5.00 tff(c_1444, plain, (~eventuality(skc15, skc19))). % 13.83/5.00 tff(c_1445, plain, (~eventuality(skc15, skc29))). % 13.83/5.00 tff(c_1442, plain, (~eventuality(skc15, skc21))). % 13.83/5.00 tff(c_411, plain, (![U_263, V_264]: (~male(U_263, V_264) | ~eventuality(U_263, V_264)))). % 13.83/5.00 tff(c_388, plain, (![U_259, V_260]: (impartial(U_259, V_260) | ~human_person(U_259, V_260)))). % 13.83/5.00 tff(c_387, plain, (![U_259, V_260]: (living(U_259, V_260) | ~human_person(U_259, V_260)))). % 13.83/5.00 tff(c_70, plain, (![X_72, W_71, U_69, V_70]: (X_72=W_71 | ~be(U_69, V_70, W_71, X_72)))). % 13.83/5.00 tff(c_376, plain, (![U_257, V_258]: (singleton(U_257, V_258) | ~eventuality(U_257, V_258)))). % 13.83/5.00 tff(c_1417, plain, (![V_195]: (event(skc26, skf1(V_195))))). % 13.83/5.00 tff(c_1000, plain, (![V_193]: (present(skc26, skf1(V_193))))). % 13.83/5.00 tff(c_405, plain, (male(skc15, skc21))). % 13.83/5.00 tff(c_406, plain, (male(skc15, skc24))). % 13.83/5.00 tff(c_404, plain, (male(skc15, skc19))). % 13.83/5.00 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 13.83/5.00 tff(c_403, plain, (male(skc15, skc29))). % 13.83/5.00 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 13.83/5.00 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 13.83/5.00 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 13.83/5.00 tff(c_363, plain, (animate(skc15, skc24))). % 13.83/5.00 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 13.83/5.00 tff(c_364, plain, (animate(skc15, skc19))). % 13.83/5.00 tff(c_365, plain, (animate(skc15, skc29))). % 13.83/5.00 tff(c_362, plain, (animate(skc15, skc21))). % 13.83/5.00 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 13.83/5.00 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 13.83/5.00 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 14.24/5.00 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 14.24/5.00 tff(c_333, plain, (human(skc15, skc29))). % 14.24/5.00 tff(c_332, plain, (human(skc15, skc19))). % 14.24/5.00 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 14.24/5.00 tff(c_331, plain, (human(skc15, skc24))). % 14.24/5.00 tff(c_330, plain, (human(skc15, skc21))). % 14.24/5.00 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 14.24/5.00 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 14.24/5.00 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 14.24/5.00 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 14.24/5.00 tff(c_299, plain, (human_person(skc15, skc21))). % 14.24/5.00 tff(c_300, plain, (human_person(skc15, skc24))). % 14.24/5.00 tff(c_298, plain, (human_person(skc15, skc19))). % 14.24/5.00 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 14.24/5.00 tff(c_297, plain, (human_person(skc15, skc29))). % 14.24/5.00 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 14.24/5.00 tff(c_283, plain, (event(skc15, skc23))). % 14.24/5.00 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 14.24/5.00 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 14.24/5.00 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 14.24/5.00 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 14.24/5.00 tff(c_270, plain, (eventuality(skc15, skc23))). % 14.24/5.00 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 14.24/5.00 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 14.24/5.00 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 14.24/5.00 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 14.24/5.00 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 14.24/5.00 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 14.24/5.00 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 14.24/5.00 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 14.24/5.00 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 14.24/5.00 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 14.24/5.00 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 14.24/5.00 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 14.24/5.00 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 14.24/5.00 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 14.24/5.00 tff(c_216, plain, (be(skc15, skc23, skc24, skc24))). % 14.24/5.00 tff(c_202, plain, (theme(skc15, skc27, skc26))). % 14.24/5.00 tff(c_214, plain, (theme(skc15, skc17, skc16))). % 14.24/5.00 tff(c_204, plain, (of(skc15, skc25, skc24))). % 14.24/5.00 tff(c_206, plain, (of(skc15, skc20, skc21))). % 14.24/5.00 tff(c_208, plain, (agent(skc16, skc22, skc21))). % 14.24/5.00 tff(c_210, plain, (of(skc15, skc18, skc19))). % 14.24/5.00 tff(c_200, plain, (agent(skc15, skc27, skc29))). % 14.24/5.00 tff(c_212, plain, (agent(skc15, skc17, skc19))). % 14.24/5.00 tff(c_198, plain, (of(skc15, skc28, skc29))). % 14.24/5.00 tff(c_176, plain, (present(skc15, skc17))). % 14.24/5.00 tff(c_178, plain, (event(skc15, skc17))). % 14.24/5.00 tff(c_180, plain, (forename(skc15, skc18))). % 14.24/5.00 tff(c_182, plain, (vincent_forename(skc15, skc18))). % 14.24/5.00 tff(c_146, plain, (man(skc15, skc29))). % 14.24/5.00 tff(c_184, plain, (forename(skc15, skc20))). % 14.24/5.00 tff(c_194, plain, (accessible_world(skc15, skc26))). % 14.24/5.00 tff(c_174, plain, (think_believe_consider(skc15, skc17))). % 14.24/5.00 tff(c_186, plain, (jules_forename(skc15, skc20))). % 14.24/5.00 tff(c_172, plain, (man(skc15, skc19))). % 14.24/5.00 tff(c_152, plain, (event(skc15, skc27))). % 14.24/5.00 tff(c_148, plain, (forename(skc15, skc28))). % 14.24/5.00 tff(c_150, plain, (vincent_forename(skc15, skc28))). % 14.24/5.00 tff(c_188, plain, (proposition(skc15, skc16))). % 14.24/5.00 tff(c_154, plain, (present(skc15, skc27))). % 14.24/5.00 tff(c_190, plain, (accessible_world(skc15, skc16))). % 14.24/5.00 tff(c_156, plain, (think_believe_consider(skc15, skc27))). % 14.24/5.00 tff(c_170, plain, (smoke(skc16, skc22))). % 14.24/5.00 tff(c_168, plain, (present(skc16, skc22))). % 14.24/5.00 tff(c_166, plain, (man(skc15, skc21))). % 14.24/5.00 tff(c_164, plain, (event(skc16, skc22))). % 14.24/5.00 tff(c_158, plain, (jules_forename(skc15, skc25))). % 14.24/5.00 tff(c_160, plain, (forename(skc15, skc25))). % 14.24/5.00 tff(c_162, plain, (man(skc15, skc24))). % 14.24/5.00 tff(c_192, plain, (state(skc15, skc23))). % 14.24/5.00 tff(c_196, plain, (proposition(skc15, skc26))). % 14.24/5.00 tff(c_144, plain, (actual_world(skc15))). % 14.24/5.00 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.24/5.00 %------------------------------------------------------------------------------