%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP245-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n019.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:45 PM UTC 2025 % Result : Satisfiable 12.93s 4.45s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NLP245-1 : TPTP v9.0.0. Released v2.4.0. % 0.13/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.35 % Computer : n019.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:45:47 EDT 2025 % 0.14/0.35 % CPUTime : % 12.93/4.45 % 12.93/4.45 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.93/4.45 % 12.93/4.45 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.93/4.46 %$ 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 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 > skc14 > skc13 % 12.93/4.46 % 12.93/4.46 %Foreground sorts: % 12.93/4.46 % 12.93/4.46 % 12.93/4.46 %Background operators: % 12.93/4.46 % 12.93/4.46 % 12.93/4.46 %Foreground operators: % 12.93/4.46 tff(skc16, type, skc16: $i). % 12.93/4.46 tff(relation, type, relation: ($i * $i) > $o). % 12.93/4.46 tff(forename, type, forename: ($i * $i) > $o). % 12.93/4.46 tff(be, type, be: ($i * $i * $i * $i) > $o). % 12.93/4.46 tff(theme, type, theme: ($i * $i * $i) > $o). % 12.93/4.46 tff(living, type, living: ($i * $i) > $o). % 12.93/4.46 tff(human_person, type, human_person: ($i * $i) > $o). % 12.93/4.46 tff(present, type, present: ($i * $i) > $o). % 12.93/4.46 tff(entity, type, entity: ($i * $i) > $o). % 12.93/4.46 tff(skc18, type, skc18: $i). % 12.93/4.46 tff(eventuality, type, eventuality: ($i * $i) > $o). % 12.93/4.46 tff(existent, type, existent: ($i * $i) > $o). % 12.93/4.46 tff(abstraction, type, abstraction: ($i * $i) > $o). % 12.93/4.46 tff(skc25, type, skc25: $i). % 12.93/4.46 tff(skf1, type, skf1: $i > $i). % 12.93/4.46 tff(proposition, type, proposition: ($i * $i) > $o). % 12.93/4.46 tff(relname, type, relname: ($i * $i) > $o). % 12.93/4.46 tff(skc14, type, skc14: $i). % 12.93/4.46 tff(singleton, type, singleton: ($i * $i) > $o). % 12.93/4.46 tff(skc17, type, skc17: $i). % 12.93/4.46 tff(skc13, type, skc13: $i). % 12.93/4.46 tff(male, type, male: ($i * $i) > $o). % 12.93/4.46 tff(organism, type, organism: ($i * $i) > $o). % 12.93/4.46 tff(animate, type, animate: ($i * $i) > $o). % 12.93/4.46 tff(of, type, of: ($i * $i * $i) > $o). % 12.93/4.46 tff(actual_world, type, actual_world: $i > $o). % 12.93/4.46 tff(agent, type, agent: ($i * $i * $i) > $o). % 12.93/4.46 tff(skc24, type, skc24: $i). % 12.93/4.46 tff(skc20, type, skc20: $i). % 12.93/4.46 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 12.93/4.46 tff(general, type, general: ($i * $i) > $o). % 12.93/4.46 tff(smoke, type, smoke: ($i * $i) > $o). % 12.93/4.46 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 12.93/4.46 tff(skc23, type, skc23: $i). % 12.93/4.46 tff(event, type, event: ($i * $i) > $o). % 12.93/4.46 tff(skc21, type, skc21: $i). % 12.93/4.46 tff(skc22, type, skc22: $i). % 12.93/4.46 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 12.93/4.46 tff(state, type, state: ($i * $i) > $o). % 12.93/4.46 tff(thing, type, thing: ($i * $i) > $o). % 12.93/4.46 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 12.93/4.46 tff(skc15, type, skc15: $i). % 12.93/4.46 tff(human, type, human: ($i * $i) > $o). % 12.93/4.46 tff(man, type, man: ($i * $i) > $o). % 12.93/4.46 tff(unisex, type, unisex: ($i * $i) > $o). % 12.93/4.46 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 12.93/4.46 tff(impartial, type, impartial: ($i * $i) > $o). % 12.93/4.46 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 12.93/4.46 tff(specific, type, specific: ($i * $i) > $o). % 12.93/4.46 tff(skc19, type, skc19: $i). % 12.93/4.46 % 12.93/4.46 %Saturated clause set: % 12.93/4.46 tff(c_7836, plain, (![V_1573, V_886]: (skc22=V_1573 | ~think_believe_consider(V_886, skc23) | ~think_believe_consider(V_886, skf1(skc25)) | ~theme(V_886, skf1(skc25), V_1573) | ~proposition(V_886, skc22) | ~proposition(V_886, V_1573) | ~accessible_world(skc22, V_886) | ~accessible_world(skc13, V_886)))). % 12.93/4.46 tff(c_7805, plain, (![W_1559, V_1557, V_879]: (W_1559=V_1557 | ~theme(V_879, skc23, W_1559) | ~think_believe_consider(V_879, skc23) | ~think_believe_consider(V_879, skf1(skc25)) | ~theme(V_879, skf1(skc25), V_1557) | ~proposition(V_879, W_1559) | ~proposition(V_879, V_1557) | ~accessible_world(skc22, V_879) | ~accessible_world(skc13, V_879)))). % 12.93/4.46 tff(c_7826, plain, (![V_1568, V_886]: (skc14=V_1568 | ~think_believe_consider(V_886, skc15) | ~think_believe_consider(V_886, skf1(skc17)) | ~theme(V_886, skf1(skc17), V_1568) | ~proposition(V_886, skc14) | ~proposition(V_886, V_1568) | ~accessible_world(skc22, V_886) | ~accessible_world(skc13, V_886)))). % 12.93/4.46 tff(c_7808, plain, (![W_1559, V_1557, V_879]: (W_1559=V_1557 | ~theme(V_879, skc15, W_1559) | ~think_believe_consider(V_879, skc15) | ~think_believe_consider(V_879, skf1(skc17)) | ~theme(V_879, skf1(skc17), V_1557) | ~proposition(V_879, W_1559) | ~proposition(V_879, V_1557) | ~accessible_world(skc22, V_879) | ~accessible_world(skc13, V_879)))). % 12.93/4.46 tff(c_7802, plain, (![W_1559, V_1557, V_879]: (W_1559=V_1557 | ~theme(V_879, skc20, W_1559) | ~think_believe_consider(V_879, skc20) | ~think_believe_consider(V_879, skf1(skc17)) | ~theme(V_879, skf1(skc17), V_1557) | ~proposition(V_879, W_1559) | ~proposition(V_879, V_1557) | ~accessible_world(skc22, V_879) | ~accessible_world(skc14, V_879)))). % 12.93/4.46 tff(c_7799, plain, (![W_1559, V_1557, V_879, U_196]: (W_1559=V_1557 | ~theme(V_879, skf1(U_196), W_1559) | ~think_believe_consider(V_879, skf1(U_196)) | ~theme(V_879, skf1(U_196), V_1557) | ~proposition(V_879, W_1559) | ~proposition(V_879, V_1557) | ~accessible_world(skc22, V_879) | ~man(skc22, U_196)))). % 12.93/4.46 tff(c_4711, plain, (![V_1060, V_189, Y_188, U_1061, W_184]: (W_184=V_189 | ~agent(V_1060, Y_188, U_1061) | ~theme(V_1060, Y_188, W_184) | ~think_believe_consider(V_1060, Y_188) | ~think_believe_consider(V_1060, skf1(U_1061)) | ~theme(V_1060, skf1(U_1061), V_189) | ~proposition(V_1060, W_184) | ~proposition(V_1060, V_189) | ~accessible_world(skc22, V_1060) | ~man(skc22, U_1061)))). % 12.93/4.46 tff(c_7029, plain, (![V_1490, V_886]: (skc22=V_1490 | ~agent(V_886, skc23, skc17) | ~think_believe_consider(V_886, skc23) | ~think_believe_consider(V_886, skc20) | ~theme(V_886, skc20, V_1490) | ~proposition(V_886, skc22) | ~proposition(V_886, V_1490) | ~accessible_world(skc14, V_886) | ~accessible_world(skc13, V_886)))). % 12.93/4.46 tff(c_7028, plain, (![V_1490, V_886]: (skc14=V_1490 | ~agent(V_886, skc15, skc17) | ~think_believe_consider(V_886, skc15) | ~think_believe_consider(V_886, skc20) | ~theme(V_886, skc20, V_1490) | ~proposition(V_886, skc14) | ~proposition(V_886, V_1490) | ~accessible_world(skc14, V_886) | ~accessible_world(skc13, V_886)))). % 12.93/4.46 tff(c_7776, plain, (![V_886]: (~agent(V_886, skc15, skc25) | ~think_believe_consider(V_886, skc15) | ~think_believe_consider(V_886, skc23) | ~proposition(V_886, skc14) | ~proposition(V_886, skc22) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_7744, plain, (![V_1542, V_886]: (skc14=V_1542 | ~agent(V_886, skc15, skc25) | ~think_believe_consider(V_886, skc15) | ~think_believe_consider(V_886, skc23) | ~theme(V_886, skc23, V_1542) | ~proposition(V_886, skc14) | ~proposition(V_886, V_1542) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_7745, plain, (![V_1542, V_886]: (skc22=V_1542 | ~agent(V_886, skc23, skc25) | ~think_believe_consider(V_886, skc23) | ~theme(V_886, skc23, V_1542) | ~proposition(V_886, skc22) | ~proposition(V_886, V_1542) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_7734, plain, (![V_886]: (~agent(V_886, skc23, skc17) | ~think_believe_consider(V_886, skc23) | ~think_believe_consider(V_886, skc15) | ~proposition(V_886, skc22) | ~proposition(V_886, skc14) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_3241, plain, (![W_920, V_918, V_879, Y_919]: (W_920=V_918 | ~agent(V_879, Y_919, skc25) | ~theme(V_879, Y_919, W_920) | ~think_believe_consider(V_879, Y_919) | ~think_believe_consider(V_879, skc23) | ~theme(V_879, skc23, V_918) | ~proposition(V_879, W_920) | ~proposition(V_879, V_918) | ~accessible_world(skc13, V_879)))). % 12.93/4.47 tff(c_7704, plain, (![V_1534, V_886]: (skc22=V_1534 | ~agent(V_886, skc23, skc17) | ~think_believe_consider(V_886, skc23) | ~think_believe_consider(V_886, skc15) | ~theme(V_886, skc15, V_1534) | ~proposition(V_886, skc22) | ~proposition(V_886, V_1534) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_7703, plain, (![V_1534, V_886]: (skc14=V_1534 | ~agent(V_886, skc15, skc17) | ~think_believe_consider(V_886, skc15) | ~theme(V_886, skc15, V_1534) | ~proposition(V_886, skc14) | ~proposition(V_886, V_1534) | ~accessible_world(skc13, V_886)))). % 12.93/4.47 tff(c_3242, plain, (![W_920, V_918, V_879, Y_919]: (W_920=V_918 | ~agent(V_879, Y_919, skc17) | ~theme(V_879, Y_919, W_920) | ~think_believe_consider(V_879, Y_919) | ~think_believe_consider(V_879, skc15) | ~theme(V_879, skc15, V_918) | ~proposition(V_879, W_920) | ~proposition(V_879, V_918) | ~accessible_world(skc13, V_879)))). % 12.93/4.47 tff(c_7542, plain, (![V_146, V_1504]: (animate(V_146, skc25) | ~accessible_world(V_1504, V_146) | ~accessible_world(skc22, V_1504)))). % 12.93/4.47 tff(c_7314, plain, (![V_143, V_1499]: (human(V_143, skc17) | ~accessible_world(V_1499, V_143) | ~accessible_world(skc22, V_1499)))). % 12.93/4.47 tff(c_7567, plain, (![V_143, V_1505]: (human(V_143, skc25) | ~accessible_world(V_1505, V_143) | ~accessible_world(skc22, V_1505)))). % 12.93/4.47 tff(c_7289, plain, (![V_146, V_1498]: (animate(V_146, skc17) | ~accessible_world(V_1498, V_146) | ~accessible_world(skc22, V_1498)))). % 12.93/4.47 tff(c_7535, plain, (![V_125, V_1503]: (human_person(V_125, skc25) | ~accessible_world(V_1503, V_125) | ~accessible_world(skc22, V_1503)))). % 12.93/4.47 tff(c_7500, plain, (![V_149, V_1502]: (male(V_149, skc25) | ~accessible_world(V_1502, V_149) | ~accessible_world(skc22, V_1502)))). % 12.93/4.47 tff(c_7257, plain, (![V_149, V_1496]: (male(V_149, skc17) | ~accessible_world(V_1496, V_149) | ~accessible_world(skc22, V_1496)))). % 12.93/4.47 tff(c_7207, plain, (![V_125, V_1495]: (human_person(V_125, skc17) | ~accessible_world(V_1495, V_125) | ~accessible_world(skc22, V_1495)))). % 12.93/4.47 tff(c_7172, plain, (![V_122, V_1494]: (man(V_122, skc17) | ~accessible_world(V_1494, V_122) | ~accessible_world(skc22, V_1494)))). % 12.93/4.47 tff(c_7454, plain, (![V_101, V_1501]: (think_believe_consider(V_101, skc23) | ~accessible_world(V_1501, V_101) | ~accessible_world(skc22, V_1501)))). % 12.93/4.47 tff(c_7162, plain, (![V_101, V_1493]: (think_believe_consider(V_101, skc15) | ~accessible_world(V_1493, V_101) | ~accessible_world(skc22, V_1493)))). % 12.93/4.47 tff(c_7435, plain, (![V_122, V_1500]: (man(V_122, skc25) | ~accessible_world(V_1500, V_122) | ~accessible_world(skc22, V_1500)))). % 12.93/4.47 tff(c_7596, plain, (![U_3]: (~accessible_world(skc22, U_3) | ~event(U_3, skc25)))). % 12.93/4.47 tff(c_7501, plain, (![V_1502]: (~eventuality(V_1502, skc25) | ~accessible_world(skc22, V_1502)))). % 12.93/4.47 tff(c_7285, plain, (![U_3]: (~accessible_world(skc22, U_3) | ~event(U_3, skc17)))). % 12.93/4.47 tff(c_7569, plain, (~think_believe_consider(skc22, skf1(skc25)))). % 12.93/4.47 tff(c_7421, plain, (![V_143]: (human(V_143, skc25) | ~accessible_world(skc22, V_143)))). % 12.93/4.47 tff(c_7425, plain, (![V_146]: (animate(V_146, skc25) | ~accessible_world(skc22, V_146)))). % 12.93/4.47 tff(c_7383, plain, (![V_125]: (human_person(V_125, skc25) | ~accessible_world(skc22, V_125)))). % 12.93/4.47 tff(c_7436, plain, (![V_1500]: (male(V_1500, skc25) | ~accessible_world(skc22, V_1500)))). % 12.93/4.47 tff(c_7450, plain, (![V_101]: (think_believe_consider(V_101, skc23) | ~accessible_world(skc22, V_101)))). % 12.93/4.47 tff(c_7447, plain, (think_believe_consider(skc22, skc23))). % 12.93/4.47 tff(c_7334, plain, (![V_122]: (man(V_122, skc25) | ~accessible_world(skc22, V_122)))). % 12.93/4.47 tff(c_7403, plain, (~event(skc22, skc25))). % 12.93/4.47 tff(c_7387, plain, (animate(skc22, skc25))). % 12.93/4.47 tff(c_7386, plain, (human(skc22, skc25))). % 12.93/4.47 tff(c_7370, plain, (~eventuality(skc22, skc25))). % 12.93/4.47 tff(c_7336, plain, (human_person(skc22, skc25))). % 12.93/4.47 tff(c_7335, plain, (male(skc22, skc25))). % 12.93/4.47 tff(c_7325, plain, (man(skc22, skc25))). % 12.93/4.47 tff(c_7157, plain, (![V_143]: (human(V_143, skc17) | ~accessible_world(skc22, V_143)))). % 12.93/4.47 tff(c_7210, plain, (![V_1495]: (animate(V_1495, skc17) | ~accessible_world(skc22, V_1495)))). % 12.93/4.47 tff(c_7258, plain, (![V_1496]: (~eventuality(V_1496, skc17) | ~accessible_world(skc22, V_1496)))). % 12.93/4.47 tff(c_7089, plain, (![V_149]: (male(V_149, skc17) | ~accessible_world(skc22, V_149)))). % 12.93/4.47 tff(c_7211, plain, (~think_believe_consider(skc22, skf1(skc17)))). % 12.93/4.47 tff(c_7103, plain, (![V_125]: (human_person(V_125, skc17) | ~accessible_world(skc22, V_125)))). % 12.93/4.47 tff(c_7054, plain, (![V_122]: (man(V_122, skc17) | ~accessible_world(skc22, V_122)))). % 12.93/4.47 tff(c_7120, plain, (![V_101]: (think_believe_consider(V_101, skc15) | ~accessible_world(skc22, V_101)))). % 12.93/4.47 tff(c_7136, plain, (~event(skc22, skc17))). % 12.93/4.47 tff(c_7106, plain, (human(skc22, skc17))). % 12.93/4.47 tff(c_7107, plain, (animate(skc22, skc17))). % 12.93/4.47 tff(c_7090, plain, (~eventuality(skc22, skc17))). % 12.93/4.47 tff(c_7117, plain, (think_believe_consider(skc22, skc15))). % 12.93/4.47 tff(c_7056, plain, (human_person(skc22, skc17))). % 12.93/4.47 tff(c_7055, plain, (male(skc22, skc17))). % 12.93/4.47 tff(c_7045, plain, (man(skc22, skc17))). % 12.93/4.47 tff(c_3240, plain, (![W_920, V_918, V_879, Y_919]: (W_920=V_918 | ~agent(V_879, Y_919, skc17) | ~theme(V_879, Y_919, W_920) | ~think_believe_consider(V_879, Y_919) | ~think_believe_consider(V_879, skc20) | ~theme(V_879, skc20, V_918) | ~proposition(V_879, W_920) | ~proposition(V_879, V_918) | ~accessible_world(skc14, V_879)))). % 12.93/4.47 tff(c_5078, plain, (![W_1112, V_1113, U_196]: (W_1112=V_1113 | ~theme(skc22, skf1(U_196), W_1112) | ~think_believe_consider(skc22, skf1(U_196)) | ~theme(skc22, skf1(U_196), V_1113) | ~proposition(skc22, W_1112) | ~proposition(skc22, V_1113) | ~man(skc22, U_196)))). % 12.93/4.47 tff(c_3211, plain, (![W_182, V_911]: (skc24=W_182 | ~entity(V_911, skc25) | ~forename(V_911, W_182) | ~of(V_911, W_182, skc25) | ~forename(V_911, skc24) | ~accessible_world(skc13, V_911)))). % 12.93/4.48 tff(c_3204, plain, (![W_182, V_910]: (skc18=W_182 | ~entity(V_910, skc17) | ~forename(V_910, W_182) | ~of(V_910, W_182, skc17) | ~forename(V_910, skc18) | ~accessible_world(skc13, V_910)))). % 12.93/4.48 tff(c_5839, plain, (![V_86, V_1247, V_1246]: (singleton(V_86, V_1247) | ~accessible_world(V_1246, V_86) | ~accessible_world(skc22, V_1246) | ~eventuality(skc13, V_1247)))). % 12.93/4.48 tff(c_5950, plain, (![V_86, V_1257, V_1256]: (singleton(V_86, V_1257) | ~accessible_world(V_1256, V_86) | ~accessible_world(skc22, V_1256) | ~entity(skc13, V_1257)))). % 12.93/4.48 tff(c_5720, plain, (![V_137, V_1225, V_1224]: (impartial(V_137, V_1225) | ~accessible_world(V_1224, V_137) | ~accessible_world(skc22, V_1224) | ~human_person(skc13, V_1225)))). % 12.93/4.48 tff(c_5909, plain, (![V_86, V_1253, V_1252]: (singleton(V_86, V_1253) | ~accessible_world(V_1252, V_86) | ~accessible_world(skc22, V_1252) | ~abstraction(skc13, V_1253)))). % 12.93/4.48 tff(c_6115, plain, (![V_86, V_1280, V_1279]: (singleton(V_86, V_1280) | ~accessible_world(V_1279, V_86) | ~accessible_world(skc14, V_1279) | ~eventuality(skc13, V_1280)))). % 12.93/4.48 tff(c_6130, plain, (![V_107, V_1286, V_1285]: (relation(V_107, V_1286) | ~accessible_world(V_1285, V_107) | ~accessible_world(skc14, V_1285) | ~forename(skc13, V_1286)))). % 12.93/4.48 tff(c_6152, plain, (![V_137, V_1290, V_1289]: (impartial(V_137, V_1290) | ~accessible_world(V_1289, V_137) | ~accessible_world(skc14, V_1289) | ~human_person(skc13, V_1290)))). % 12.93/4.48 tff(c_5986, plain, (![V_107, V_1264, V_1263]: (relation(V_107, V_1264) | ~accessible_world(V_1263, V_107) | ~accessible_world(skc22, V_1263) | ~forename(skc13, V_1264)))). % 12.93/4.48 tff(c_5835, plain, (![V_86, V_1245, V_1244]: (singleton(V_86, V_1245) | ~accessible_world(V_1244, V_86) | ~accessible_world(skc14, V_1244) | ~abstraction(skc13, V_1245)))). % 12.93/4.48 tff(c_5663, plain, (![V_140, V_1217, V_1216]: (living(V_140, V_1217) | ~accessible_world(V_1216, V_140) | ~accessible_world(skc22, V_1216) | ~human_person(skc13, V_1217)))). % 12.93/4.48 tff(c_5732, plain, (![V_140, V_1230, V_1229]: (living(V_140, V_1230) | ~accessible_world(V_1229, V_140) | ~accessible_world(skc14, V_1229) | ~human_person(skc13, V_1230)))). % 12.93/4.48 tff(c_5998, plain, (![V_86, V_1268, V_1267]: (singleton(V_86, V_1268) | ~accessible_world(V_1267, V_86) | ~accessible_world(skc14, V_1267) | ~entity(skc13, V_1268)))). % 12.93/4.48 tff(c_5481, plain, (![V_83, V_1195, V_1194]: (thing(V_83, V_1195) | ~accessible_world(V_1194, V_83) | ~accessible_world(skc22, V_1194) | ~entity(skc13, V_1195)))). % 12.93/4.48 tff(c_5414, plain, (![V_92, V_1179, V_1178]: (nonexistent(V_92, V_1179) | ~accessible_world(V_1178, V_92) | ~accessible_world(skc22, V_1178) | ~eventuality(skc13, V_1179)))). % 12.93/4.48 tff(c_5231, plain, (![V_89, V_1157, V_1156]: (specific(V_89, V_1157) | ~accessible_world(V_1156, V_89) | ~accessible_world(skc14, V_1156) | ~entity(skc13, V_1157)))). % 12.93/4.48 tff(c_5177, plain, (![V_83, V_1143, V_1142]: (thing(V_83, V_1143) | ~accessible_world(V_1142, V_83) | ~accessible_world(skc22, V_1142) | ~eventuality(skc13, V_1143)))). % 12.93/4.48 tff(c_5223, plain, (![V_83, V_1155, V_1154]: (thing(V_83, V_1155) | ~accessible_world(V_1154, V_83) | ~accessible_world(skc22, V_1154) | ~abstraction(skc13, V_1155)))). % 12.93/4.48 tff(c_4712, plain, (![V_164, U_1061, V_1060]: (agent(V_164, skf1(U_1061), U_1061) | ~accessible_world(V_1060, V_164) | ~accessible_world(skc22, V_1060) | ~man(skc22, U_1061)))). % 12.93/4.48 tff(c_5398, plain, (![V_155, V_1175, V_1174]: (relname(V_155, V_1175) | ~accessible_world(V_1174, V_155) | ~accessible_world(skc22, V_1174) | ~forename(skc13, V_1175)))). % 12.93/4.48 tff(c_5327, plain, (![V_134, V_1163, V_1162]: (existent(V_134, V_1163) | ~accessible_world(V_1162, V_134) | ~accessible_world(skc22, V_1162) | ~entity(skc13, V_1163)))). % 12.93/4.48 tff(c_5358, plain, (![V_116, V_1165, V_1164]: (general(V_116, V_1165) | ~accessible_world(V_1164, V_116) | ~accessible_world(skc22, V_1164) | ~abstraction(skc13, V_1165)))). % 12.93/4.48 tff(c_5153, plain, (![V_83, V_1137, V_1136]: (thing(V_83, V_1137) | ~accessible_world(V_1136, V_83) | ~accessible_world(skc14, V_1136) | ~abstraction(skc13, V_1137)))). % 12.93/4.48 tff(c_5428, plain, (![V_128, V_1181, V_1180]: (organism(V_128, V_1181) | ~accessible_world(V_1180, V_128) | ~accessible_world(skc14, V_1180) | ~human_person(skc13, V_1181)))). % 12.93/4.48 tff(c_5208, plain, (![V_95, V_1151, V_1150]: (unisex(V_95, V_1151) | ~accessible_world(V_1150, V_95) | ~accessible_world(skc14, V_1150) | ~abstraction(skc13, V_1151)))). % 12.93/4.48 tff(c_5161, plain, (![V_83, V_1139, V_1138]: (thing(V_83, V_1139) | ~accessible_world(V_1138, V_83) | ~accessible_world(skc14, V_1138) | ~eventuality(skc13, V_1139)))). % 12.93/4.48 tff(c_5497, plain, (![V_107, V_1199, V_1198]: (relation(V_107, V_1199) | ~accessible_world(V_1198, V_107) | ~accessible_world(skc14, V_1198) | ~proposition(skc13, V_1199)))). % 12.93/4.48 tff(c_6809, plain, (~agent(skc13, skc15, skc25))). % 12.93/4.48 tff(c_5657, plain, (![V_134, V_1213, V_1212]: (existent(V_134, V_1213) | ~accessible_world(V_1212, V_134) | ~accessible_world(skc14, V_1212) | ~entity(skc13, V_1213)))). % 12.93/4.48 tff(c_5137, plain, (![V_113, V_1133, V_1132]: (nonhuman(V_113, V_1133) | ~accessible_world(V_1132, V_113) | ~accessible_world(skc14, V_1132) | ~abstraction(skc13, V_1133)))). % 12.93/4.48 tff(c_5367, plain, (![V_89, V_1167, V_1166]: (specific(V_89, V_1167) | ~accessible_world(V_1166, V_89) | ~accessible_world(skc22, V_1166) | ~entity(skc13, V_1167)))). % 12.93/4.48 tff(c_5489, plain, (![V_89, V_1197, V_1196]: (specific(V_89, V_1197) | ~accessible_world(V_1196, V_89) | ~accessible_world(skc14, V_1196) | ~eventuality(skc13, V_1197)))). % 13.21/4.48 tff(c_5614, plain, (![V_116, V_1205, V_1204]: (general(V_116, V_1205) | ~accessible_world(V_1204, V_116) | ~accessible_world(skc14, V_1204) | ~abstraction(skc13, V_1205)))). % 13.21/4.48 tff(c_5145, plain, (![V_92, V_1135, V_1134]: (nonexistent(V_92, V_1135) | ~accessible_world(V_1134, V_92) | ~accessible_world(skc14, V_1134) | ~eventuality(skc13, V_1135)))). % 13.21/4.48 tff(c_5390, plain, (![V_107, V_1173, V_1172]: (relation(V_107, V_1173) | ~accessible_world(V_1172, V_107) | ~accessible_world(skc22, V_1172) | ~proposition(skc13, V_1173)))). % 13.21/4.48 tff(c_5438, plain, (![V_83, V_1183, V_1182]: (thing(V_83, V_1183) | ~accessible_world(V_1182, V_83) | ~accessible_world(skc14, V_1182) | ~entity(skc13, V_1183)))). % 13.21/4.48 tff(c_6752, plain, (~agent(skc13, skc23, skc17))). % 13.21/4.48 tff(c_5406, plain, (![V_89, V_1177, V_1176]: (specific(V_89, V_1177) | ~accessible_world(V_1176, V_89) | ~accessible_world(skc22, V_1176) | ~eventuality(skc13, V_1177)))). % 13.21/4.48 tff(c_5169, plain, (![V_113, V_1141, V_1140]: (nonhuman(V_113, V_1141) | ~accessible_world(V_1140, V_113) | ~accessible_world(skc22, V_1140) | ~abstraction(skc13, V_1141)))). % 13.21/4.48 tff(c_5239, plain, (![V_95, V_1159, V_1158]: (unisex(V_95, V_1159) | ~accessible_world(V_1158, V_95) | ~accessible_world(skc14, V_1158) | ~eventuality(skc13, V_1159)))). % 13.21/4.48 tff(c_5639, plain, (![V_95, V_1211, V_1210]: (unisex(V_95, V_1211) | ~accessible_world(V_1210, V_95) | ~accessible_world(skc22, V_1210) | ~abstraction(skc13, V_1211)))). % 13.21/4.48 tff(c_5185, plain, (![V_155, V_1145, V_1144]: (relname(V_155, V_1145) | ~accessible_world(V_1144, V_155) | ~accessible_world(skc14, V_1144) | ~forename(skc13, V_1145)))). % 13.21/4.48 tff(c_5193, plain, (![V_95, V_1147, V_1146]: (unisex(V_95, V_1147) | ~accessible_world(V_1146, V_95) | ~accessible_world(skc22, V_1146) | ~eventuality(skc13, V_1147)))). % 13.21/4.48 tff(c_5564, plain, (![V_80, V_1201, V_1200]: (eventuality(V_80, V_1201) | ~accessible_world(V_1200, V_80) | ~accessible_world(skc14, V_1200) | ~event(skc13, V_1201)))). % 13.21/4.48 tff(c_5306, plain, (![V_80, V_1161, V_1160]: (eventuality(V_80, V_1161) | ~accessible_world(V_1160, V_80) | ~accessible_world(skc22, V_1160) | ~event(skc13, V_1161)))). % 13.21/4.48 tff(c_5581, plain, (![V_128, V_1203, V_1202]: (organism(V_128, V_1203) | ~accessible_world(V_1202, V_128) | ~accessible_world(skc22, V_1202) | ~human_person(skc13, V_1203)))). % 13.21/4.48 tff(c_4440, plain, (![V_131, V_1029]: (entity(V_131, skc17) | ~accessible_world(V_1029, V_131) | ~accessible_world(skc14, V_1029)))). % 13.21/4.48 tff(c_4458, plain, (![V_131, V_1030]: (entity(V_131, skc25) | ~accessible_world(V_1030, V_131) | ~accessible_world(skc14, V_1030)))). % 13.21/4.48 tff(c_4668, plain, (![V_131, V_1048]: (entity(V_131, skc25) | ~accessible_world(V_1048, V_131) | ~accessible_world(skc22, V_1048)))). % 13.21/4.48 tff(c_4587, plain, (![V_131, V_1040]: (entity(V_131, skc17) | ~accessible_world(V_1040, V_131) | ~accessible_world(skc22, V_1040)))). % 13.21/4.48 tff(c_6131, plain, (![V_1285, V_1286]: (abstraction(V_1285, V_1286) | ~accessible_world(skc14, V_1285) | ~forename(skc13, V_1286)))). % 13.21/4.48 tff(c_6074, plain, (![U_3, V_4]: (~accessible_world(skc22, U_3) | ~abstraction(skc13, V_4) | ~event(U_3, V_4)))). % 13.21/4.48 tff(c_6181, plain, (![U_3, V_4]: (~accessible_world(skc14, U_3) | ~abstraction(skc13, V_4) | ~event(U_3, V_4)))). % 13.21/4.48 tff(c_6567, plain, (![U_1336]: (~accessible_world(skc14, U_1336) | ~entity(U_1336, skc16)))). % 13.21/4.48 tff(c_5808, plain, (![U_41, V_42]: (~accessible_world(skc14, U_41) | ~eventuality(skc13, V_42) | ~entity(U_41, V_42)))). % 13.21/4.48 tff(c_3258, plain, (![V_179, V_924]: (be(V_179, skc16, skc17, skc17) | ~accessible_world(V_924, V_179) | ~accessible_world(skc13, V_924)))). % 13.21/4.48 tff(c_5971, plain, (![U_23, V_24]: (~accessible_world(skc22, U_23) | ~entity(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.49 tff(c_5905, plain, (![U_3, V_4]: (~accessible_world(skc22, U_3) | ~entity(skc13, V_4) | ~event(U_3, V_4)))). % 13.21/4.49 tff(c_6036, plain, (![U_23, V_24]: (~accessible_world(skc14, U_23) | ~eventuality(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.49 tff(c_5692, plain, (![U_3, V_4]: (~accessible_world(skc14, U_3) | ~entity(skc13, V_4) | ~event(U_3, V_4)))). % 13.21/4.49 tff(c_6362, plain, (![U_23, V_24]: (~accessible_world(skc14, U_23) | ~entity(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.49 tff(c_6235, plain, (![U_23, V_24]: (~accessible_world(skc22, U_23) | ~eventuality(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.49 tff(c_5987, plain, (![V_1263, V_1264]: (abstraction(V_1263, V_1264) | ~accessible_world(skc22, V_1263) | ~forename(skc13, V_1264)))). % 13.21/4.49 tff(c_6452, plain, (![U_1317]: (~accessible_world(skc22, U_1317) | ~entity(U_1317, skc16)))). % 13.21/4.49 tff(c_6400, plain, (![U_41, V_42]: (~accessible_world(skc22, U_41) | ~eventuality(skc13, V_42) | ~entity(U_41, V_42)))). % 13.21/4.49 tff(c_5429, plain, (![V_1180, V_1181]: (entity(V_1180, V_1181) | ~accessible_world(skc14, V_1180) | ~human_person(skc13, V_1181)))). % 13.21/4.49 tff(c_5170, plain, (![V_1140, V_1141]: (~human(V_1140, V_1141) | ~accessible_world(skc22, V_1140) | ~abstraction(skc13, V_1141)))). % 13.21/4.49 tff(c_5415, plain, (![V_1178, V_1179]: (~existent(V_1178, V_1179) | ~accessible_world(skc22, V_1178) | ~eventuality(skc13, V_1179)))). % 13.21/4.49 tff(c_5138, plain, (![V_1132, V_1133]: (~human(V_1132, V_1133) | ~accessible_world(skc14, V_1132) | ~abstraction(skc13, V_1133)))). % 13.21/4.49 tff(c_5232, plain, (![V_1156, V_1157]: (~general(V_1156, V_1157) | ~accessible_world(skc14, V_1156) | ~entity(skc13, V_1157)))). % 13.21/4.49 tff(c_5615, plain, (![V_1204, V_1205]: (~entity(V_1204, V_1205) | ~accessible_world(skc14, V_1204) | ~abstraction(skc13, V_1205)))). % 13.21/4.49 tff(c_3146, plain, (![V_164, V_895]: (agent(V_164, skc20, skc17) | ~accessible_world(V_895, V_164) | ~accessible_world(skc14, V_895)))). % 13.21/4.49 tff(c_5359, plain, (![V_1164, V_1165]: (~entity(V_1164, V_1165) | ~accessible_world(skc22, V_1164) | ~abstraction(skc13, V_1165)))). % 13.21/4.49 tff(c_5407, plain, (![V_1176, V_1177]: (~general(V_1176, V_1177) | ~accessible_world(skc22, V_1176) | ~eventuality(skc13, V_1177)))). % 13.21/4.49 tff(c_2951, plain, (![V_131, V_833]: (entity(V_131, skc25) | ~accessible_world(V_833, V_131) | ~accessible_world(skc13, V_833)))). % 13.21/4.49 tff(c_5194, plain, (![V_1146, V_1147]: (~male(V_1146, V_1147) | ~accessible_world(skc22, V_1146) | ~eventuality(skc13, V_1147)))). % 13.21/4.49 tff(c_3212, plain, (![V_172, V_911]: (of(V_172, skc24, skc25) | ~accessible_world(V_911, V_172) | ~accessible_world(skc13, V_911)))). % 13.21/4.49 tff(c_5616, plain, (![V_1204, V_1205]: (~eventuality(V_1204, V_1205) | ~accessible_world(skc14, V_1204) | ~abstraction(skc13, V_1205)))). % 13.21/4.49 tff(c_3572, plain, (![V_137, V_954]: (impartial(V_137, V_954) | ~accessible_world(skc14, V_137) | ~human_person(skc13, V_954)))). % 13.21/4.49 tff(c_5209, plain, (![V_1150, V_1151]: (~male(V_1150, V_1151) | ~accessible_world(skc14, V_1150) | ~abstraction(skc13, V_1151)))). % 13.21/4.49 tff(c_3647, plain, (![V_107, V_963]: (relation(V_107, V_963) | ~accessible_world(skc14, V_107) | ~forename(skc13, V_963)))). % 13.21/4.49 tff(c_5498, plain, (![V_1198, V_1199]: (abstraction(V_1198, V_1199) | ~accessible_world(skc14, V_1198) | ~proposition(skc13, V_1199)))). % 13.21/4.49 tff(c_2900, plain, (![V_146, V_823]: (animate(V_146, skc17) | ~accessible_world(V_823, V_146) | ~accessible_world(skc13, V_823)))). % 13.21/4.49 tff(c_3874, plain, (![V_86, V_987]: (singleton(V_86, V_987) | ~accessible_world(skc14, V_86) | ~eventuality(skc13, V_987)))). % 13.21/4.49 tff(c_5307, plain, (![V_1160, V_1161]: (~entity(V_1160, V_1161) | ~accessible_world(skc22, V_1160) | ~event(skc13, V_1161)))). % 13.21/4.49 tff(c_5360, plain, (![V_1164, V_1165]: (~eventuality(V_1164, V_1165) | ~accessible_world(skc22, V_1164) | ~abstraction(skc13, V_1165)))). % 13.21/4.49 tff(c_2943, plain, (![V_131, V_832]: (entity(V_131, skc17) | ~accessible_world(V_832, V_131) | ~accessible_world(skc13, V_832)))). % 13.21/4.49 tff(c_5490, plain, (![V_1196, V_1197]: (~general(V_1196, V_1197) | ~accessible_world(skc14, V_1196) | ~eventuality(skc13, V_1197)))). % 13.21/4.49 tff(c_5240, plain, (![V_1158, V_1159]: (~male(V_1158, V_1159) | ~accessible_world(skc14, V_1158) | ~eventuality(skc13, V_1159)))). % 13.21/4.49 tff(c_5439, plain, (![V_1182, V_1183]: (singleton(V_1182, V_1183) | ~accessible_world(skc14, V_1182) | ~entity(skc13, V_1183)))). % 13.21/4.49 tff(c_2680, plain, (![V_143, V_786]: (human(V_143, skc17) | ~accessible_world(V_786, V_143) | ~accessible_world(skc13, V_786)))). % 13.21/4.49 tff(c_3639, plain, (![V_107, V_962]: (relation(V_107, V_962) | ~accessible_world(skc22, V_107) | ~forename(skc13, V_962)))). % 13.21/4.49 tff(c_3160, plain, (![V_77, V_902, V_901]: (event(V_77, skf1(V_902)) | ~accessible_world(V_901, V_77) | ~accessible_world(skc22, V_901)))). % 13.21/4.49 tff(c_5368, plain, (![V_1166, V_1167]: (~general(V_1166, V_1167) | ~accessible_world(skc22, V_1166) | ~entity(skc13, V_1167)))). % 13.21/4.49 tff(c_3746, plain, (![V_86, V_971]: (singleton(V_86, V_971) | ~accessible_world(skc22, V_86) | ~entity(skc13, V_971)))). % 13.21/4.49 tff(c_5565, plain, (![V_1200, V_1201]: (~entity(V_1200, V_1201) | ~accessible_world(skc14, V_1200) | ~event(skc13, V_1201)))). % 13.21/4.49 tff(c_5224, plain, (![V_1154, V_1155]: (singleton(V_1154, V_1155) | ~accessible_world(skc22, V_1154) | ~abstraction(skc13, V_1155)))). % 13.21/4.49 tff(c_5328, plain, (![V_1162, V_1163]: (~eventuality(V_1162, V_1163) | ~accessible_world(skc22, V_1162) | ~entity(skc13, V_1163)))). % 13.21/4.49 tff(c_5566, plain, (![V_1200, V_1201]: (~abstraction(V_1200, V_1201) | ~accessible_world(skc14, V_1200) | ~event(skc13, V_1201)))). % 13.21/4.49 tff(c_3878, plain, (![V_86, V_988]: (singleton(V_86, V_988) | ~accessible_world(skc22, V_86) | ~eventuality(skc13, V_988)))). % 13.21/4.49 tff(c_4700, plain, (![V_86, V_1058]: (singleton(V_86, V_1058) | ~accessible_world(skc14, V_86) | ~abstraction(skc13, V_1058)))). % 13.21/4.49 tff(c_3169, plain, (![V_74, V_904, V_903]: (smoke(V_74, skf1(V_904)) | ~accessible_world(V_903, V_74) | ~accessible_world(skc22, V_903)))). % 13.21/4.49 tff(c_5582, plain, (![V_1202, V_1203]: (entity(V_1202, V_1203) | ~accessible_world(skc22, V_1202) | ~human_person(skc13, V_1203)))). % 13.21/4.49 tff(c_5146, plain, (![V_1134, V_1135]: (~existent(V_1134, V_1135) | ~accessible_world(skc14, V_1134) | ~eventuality(skc13, V_1135)))). % 13.21/4.49 tff(c_2904, plain, (![V_146, V_824]: (animate(V_146, skc25) | ~accessible_world(V_824, V_146) | ~accessible_world(skc13, V_824)))). % 13.21/4.49 tff(c_5780, plain, (~event(skc13, skc14))). % 13.21/4.49 tff(c_5772, plain, (~event(skc13, skc18))). % 13.21/4.49 tff(c_3223, plain, (![V_168, V_913]: (theme(V_168, skc15, skc14) | ~accessible_world(V_913, V_168) | ~accessible_world(skc13, V_913)))). % 13.21/4.49 tff(c_5771, plain, (~event(skc13, skc22))). % 13.21/4.49 tff(c_5770, plain, (~event(skc13, skc24))). % 13.21/4.49 tff(c_5308, plain, (![V_1160, V_1161]: (~abstraction(V_1160, V_1161) | ~accessible_world(skc22, V_1160) | ~event(skc13, V_1161)))). % 13.21/4.49 tff(c_5431, plain, (![V_1180, V_1181]: (living(V_1180, V_1181) | ~accessible_world(skc14, V_1180) | ~human_person(skc13, V_1181)))). % 13.21/4.49 tff(c_3130, plain, (![V_98, V_891, V_890]: (present(V_98, skf1(V_891)) | ~accessible_world(V_890, V_98) | ~accessible_world(skc22, V_890)))). % 13.21/4.49 tff(c_5583, plain, (![V_1202, V_1203]: (impartial(V_1202, V_1203) | ~accessible_world(skc22, V_1202) | ~human_person(skc13, V_1203)))). % 13.21/4.49 tff(c_2895, plain, (![V_143, V_822]: (human(V_143, skc25) | ~accessible_world(V_822, V_143) | ~accessible_world(skc13, V_822)))). % 13.21/4.49 tff(c_5640, plain, (![V_1210, V_1211]: (~male(V_1210, V_1211) | ~accessible_world(skc22, V_1210) | ~abstraction(skc13, V_1211)))). % 13.21/4.49 tff(c_5658, plain, (![V_1212, V_1213]: (~eventuality(V_1212, V_1213) | ~accessible_world(skc14, V_1212) | ~entity(skc13, V_1213)))). % 13.21/4.49 tff(c_3568, plain, (![V_140, V_953]: (living(V_140, V_953) | ~accessible_world(skc22, V_140) | ~human_person(skc13, V_953)))). % 13.21/4.49 tff(c_5391, plain, (![V_1172, V_1173]: (abstraction(V_1172, V_1173) | ~accessible_world(skc22, V_1172) | ~proposition(skc13, V_1173)))). % 13.21/4.49 tff(c_3973, plain, (![V_134, V_995]: (existent(V_134, V_995) | ~accessible_world(skc14, V_134) | ~entity(skc13, V_995)))). % 13.21/4.49 tff(c_4610, plain, (![V_95, V_1045]: (unisex(V_95, V_1045) | ~accessible_world(skc22, V_95) | ~abstraction(skc13, V_1045)))). % 13.21/4.49 tff(c_2836, plain, (![V_813, V_782]: (event(V_813, skc20) | ~accessible_world(V_782, V_813) | ~accessible_world(skc14, V_782)))). % 13.21/4.49 tff(c_5617, plain, (![V_172, V_905]: (of(V_172, skc18, skc17) | ~accessible_world(V_905, V_172) | ~accessible_world(skc13, V_905)))). % 13.21/4.49 tff(c_4115, plain, (![V_116, V_1005]: (general(V_116, V_1005) | ~accessible_world(skc14, V_116) | ~abstraction(skc13, V_1005)))). % 13.21/4.49 tff(c_3557, plain, (![V_128, V_951]: (organism(V_128, V_951) | ~accessible_world(skc22, V_128) | ~human_person(skc13, V_951)))). % 13.21/4.49 tff(c_3344, plain, (![V_80, V_935]: (eventuality(V_80, V_935) | ~accessible_world(skc14, V_80) | ~event(skc13, V_935)))). % 13.21/4.49 tff(c_4242, plain, (![V_107, V_1015]: (relation(V_107, V_1015) | ~accessible_world(skc14, V_107) | ~proposition(skc13, V_1015)))). % 13.21/4.49 tff(c_3386, plain, (![V_89, V_940]: (specific(V_89, V_940) | ~accessible_world(skc14, V_89) | ~eventuality(skc13, V_940)))). % 13.21/4.49 tff(c_3703, plain, (![V_83, V_969]: (thing(V_83, V_969) | ~accessible_world(skc22, V_83) | ~entity(skc13, V_969)))). % 13.21/4.49 tff(c_2519, plain, (![V_149, V_754]: (male(V_149, skc25) | ~accessible_world(V_754, V_149) | ~accessible_world(skc13, V_754)))). % 13.21/4.49 tff(c_2531, plain, (![V_149, V_755]: (male(V_149, skc17) | ~accessible_world(V_755, V_149) | ~accessible_world(skc13, V_755)))). % 13.21/4.49 tff(c_3047, plain, (![V_125, V_860]: (human_person(V_125, skc17) | ~accessible_world(V_860, V_125) | ~accessible_world(skc13, V_860)))). % 13.21/4.49 tff(c_3142, plain, (![V_164, V_894]: (agent(V_164, skc23, skc25) | ~accessible_world(V_894, V_164) | ~accessible_world(skc13, V_894)))). % 13.21/4.49 tff(c_2635, plain, (![V_775, V_766]: (eventuality(V_775, skc16) | ~accessible_world(V_766, V_775) | ~accessible_world(skc13, V_766)))). % 13.21/4.49 tff(c_3695, plain, (![V_83, V_968]: (thing(V_83, V_968) | ~accessible_world(skc14, V_83) | ~entity(skc13, V_968)))). % 13.21/4.49 tff(c_3541, plain, (![V_128, V_950]: (organism(V_128, V_950) | ~accessible_world(skc14, V_128) | ~human_person(skc13, V_950)))). % 13.21/4.49 tff(c_3773, plain, (![V_92, V_977]: (nonexistent(V_92, V_977) | ~accessible_world(skc22, V_92) | ~eventuality(skc13, V_977)))). % 13.21/4.49 tff(c_3394, plain, (![V_89, V_941]: (specific(V_89, V_941) | ~accessible_world(skc22, V_89) | ~eventuality(skc13, V_941)))). % 13.21/4.49 tff(c_3627, plain, (![V_155, V_960]: (relname(V_155, V_960) | ~accessible_world(skc22, V_155) | ~forename(skc13, V_960)))). % 13.21/4.49 tff(c_4250, plain, (![V_107, V_1016]: (relation(V_107, V_1016) | ~accessible_world(skc22, V_107) | ~proposition(skc13, V_1016)))). % 13.21/4.49 tff(c_2837, plain, (![V_813, V_766]: (event(V_813, skc16) | ~accessible_world(V_766, V_813) | ~accessible_world(skc13, V_766)))). % 13.21/4.49 tff(c_3138, plain, (![V_164, V_893]: (agent(V_164, skc15, skc17) | ~accessible_world(V_893, V_164) | ~accessible_world(skc13, V_893)))). % 13.21/4.49 tff(c_4481, plain, (![V_89, V_1035]: (specific(V_89, V_1035) | ~accessible_world(skc22, V_89) | ~entity(skc13, V_1035)))). % 13.21/4.50 tff(c_4131, plain, (![V_116, V_1006]: (general(V_116, V_1006) | ~accessible_world(skc22, V_116) | ~abstraction(skc13, V_1006)))). % 13.21/4.50 tff(c_3985, plain, (![V_134, V_996]: (existent(V_134, V_996) | ~accessible_world(skc22, V_134) | ~entity(skc13, V_996)))). % 13.21/4.50 tff(c_3377, plain, (![V_80, V_939]: (eventuality(V_80, V_939) | ~accessible_world(skc22, V_80) | ~event(skc13, V_939)))). % 13.21/4.50 tff(c_4384, plain, (![V_95, V_1025]: (unisex(V_95, V_1025) | ~accessible_world(skc14, V_95) | ~eventuality(skc13, V_1025)))). % 13.21/4.50 tff(c_4473, plain, (![V_89, V_1034]: (specific(V_89, V_1034) | ~accessible_world(skc14, V_89) | ~entity(skc13, V_1034)))). % 13.21/4.50 tff(c_4695, plain, (![V_83, V_1057]: (thing(V_83, V_1057) | ~accessible_world(skc22, V_83) | ~abstraction(skc13, V_1057)))). % 13.21/4.50 tff(c_3031, plain, (![V_125, V_859]: (human_person(V_125, skc25) | ~accessible_world(V_859, V_125) | ~accessible_world(skc13, V_859)))). % 13.21/4.50 tff(c_4602, plain, (![V_95, V_1044]: (unisex(V_95, V_1044) | ~accessible_world(skc14, V_95) | ~abstraction(skc13, V_1044)))). % 13.21/4.50 tff(c_3134, plain, (![V_168, V_892]: (theme(V_168, skc23, skc22) | ~accessible_world(V_892, V_168) | ~accessible_world(skc13, V_892)))). % 13.21/4.50 tff(c_4392, plain, (![V_95, V_1026]: (unisex(V_95, V_1026) | ~accessible_world(skc22, V_95) | ~eventuality(skc13, V_1026)))). % 13.21/4.50 tff(c_3619, plain, (![V_155, V_959]: (relname(V_155, V_959) | ~accessible_world(skc14, V_155) | ~forename(skc13, V_959)))). % 13.21/4.50 tff(c_3869, plain, (![V_83, V_986]: (thing(V_83, V_986) | ~accessible_world(skc22, V_83) | ~eventuality(skc13, V_986)))). % 13.21/4.50 tff(c_3282, plain, (![V_113, V_929]: (nonhuman(V_113, V_929) | ~accessible_world(skc22, V_113) | ~abstraction(skc13, V_929)))). % 13.21/4.50 tff(c_3861, plain, (![V_83, V_985]: (thing(V_83, V_985) | ~accessible_world(skc14, V_83) | ~eventuality(skc13, V_985)))). % 13.21/4.50 tff(c_4687, plain, (![V_83, V_1056]: (thing(V_83, V_1056) | ~accessible_world(skc14, V_83) | ~abstraction(skc13, V_1056)))). % 13.21/4.50 tff(c_3765, plain, (![V_92, V_976]: (nonexistent(V_92, V_976) | ~accessible_world(skc14, V_92) | ~eventuality(skc13, V_976)))). % 13.21/4.50 tff(c_3274, plain, (![V_113, V_928]: (nonhuman(V_113, V_928) | ~accessible_world(skc14, V_113) | ~abstraction(skc13, V_928)))). % 13.21/4.50 tff(c_2371, plain, (![V_152, V_726]: (forename(V_152, skc24) | ~accessible_world(V_726, V_152) | ~accessible_world(skc13, V_726)))). % 13.21/4.50 tff(c_2864, plain, (![V_77, V_817]: (event(V_77, skc23) | ~accessible_world(V_817, V_77) | ~accessible_world(skc13, V_817)))). % 13.21/4.50 tff(c_2914, plain, (![V_825, V_210, U_209]: (singleton(V_825, V_210) | ~accessible_world(U_209, V_825) | ~abstraction(U_209, V_210)))). % 13.21/4.50 tff(c_2587, plain, (![V_119, V_766]: (state(V_119, skc16) | ~accessible_world(V_766, V_119) | ~accessible_world(skc13, V_766)))). % 13.21/4.50 tff(c_5093, plain, (![V_158, V_800]: (vincent_forename(V_158, skc18) | ~accessible_world(V_800, V_158) | ~accessible_world(skc13, V_800)))). % 13.21/4.50 tff(c_3008, plain, (![V_850, V_246, U_245]: (living(V_850, V_246) | ~accessible_world(U_245, V_850) | ~human_person(U_245, V_246)))). % 13.21/4.50 tff(c_3001, plain, (![V_104, V_847]: (proposition(V_104, skc22) | ~accessible_world(V_847, V_104) | ~accessible_world(skc13, V_847)))). % 13.21/4.50 tff(c_3243, plain, (![W_920, V_918, Y_919, U_196]: (W_920=V_918 | ~agent(skc22, Y_919, U_196) | ~theme(skc22, Y_919, W_920) | ~think_believe_consider(skc22, Y_919) | ~think_believe_consider(skc22, skf1(U_196)) | ~theme(skc22, skf1(U_196), V_918) | ~proposition(skc22, W_920) | ~proposition(skc22, V_918) | ~man(skc22, U_196)))). % 13.21/4.50 tff(c_3082, plain, (![V_122, V_868]: (man(V_122, skc25) | ~accessible_world(V_868, V_122) | ~accessible_world(skc13, V_868)))). % 13.21/4.50 tff(c_2573, plain, (![V_98, V_762]: (present(V_98, skc23) | ~accessible_world(V_762, V_98) | ~accessible_world(skc13, V_762)))). % 13.21/4.50 tff(c_2852, plain, (![V_77, V_816]: (event(V_77, skc15) | ~accessible_world(V_816, V_77) | ~accessible_world(skc13, V_816)))). % 13.21/4.50 tff(c_2618, plain, (![V_101, V_773]: (think_believe_consider(V_101, skc23) | ~accessible_world(V_773, V_101) | ~accessible_world(skc13, V_773)))). % 13.21/4.50 tff(c_3198, plain, (![W_906]: (skc24=W_906 | ~forename(skc13, W_906) | ~of(skc13, W_906, skc25)))). % 13.21/4.50 tff(c_2989, plain, (![V_104, V_843]: (proposition(V_104, skc14) | ~accessible_world(V_843, V_104) | ~accessible_world(skc13, V_843)))). % 13.21/4.50 tff(c_2718, plain, (![V_792, V_246, U_245]: (impartial(V_792, V_246) | ~accessible_world(U_245, V_792) | ~human_person(U_245, V_246)))). % 13.21/4.50 tff(c_2660, plain, (![V_74, V_782]: (smoke(V_74, skc20) | ~accessible_world(V_782, V_74) | ~accessible_world(skc14, V_782)))). % 13.21/4.50 tff(c_4989, plain, (~think_believe_consider(skc14, skc20))). % 13.21/4.50 tff(c_2565, plain, (![V_98, V_760]: (present(V_98, skc15) | ~accessible_world(V_760, V_98) | ~accessible_world(skc13, V_760)))). % 13.21/4.50 tff(c_2367, plain, (![V_152, V_725]: (forename(V_152, skc18) | ~accessible_world(V_725, V_152) | ~accessible_world(skc13, V_725)))). % 13.21/4.50 tff(c_2756, plain, (![V_158, V_801]: (vincent_forename(V_158, skc24) | ~accessible_world(V_801, V_158) | ~accessible_world(skc13, V_801)))). % 13.21/4.50 tff(c_2614, plain, (![V_101, V_772]: (think_believe_consider(V_101, skc15) | ~accessible_world(V_772, V_101) | ~accessible_world(skc13, V_772)))). % 13.21/4.50 tff(c_4909, plain, (![V_1076]: (skc22=V_1076 | ~theme(skc13, skc23, V_1076) | ~proposition(skc13, V_1076)))). % 13.21/4.50 tff(c_2913, plain, (![V_825, V_262, U_261]: (singleton(V_825, V_262) | ~accessible_world(U_261, V_825) | ~eventuality(U_261, V_262)))). % 13.21/4.50 tff(c_3070, plain, (![V_122, V_867]: (man(V_122, skc17) | ~accessible_world(V_867, V_122) | ~accessible_world(skc13, V_867)))). % 13.21/4.50 tff(c_4840, plain, (![V_1067]: (skc14=V_1067 | ~theme(skc13, skc15, V_1067) | ~proposition(skc13, V_1067)))). % 13.21/4.50 tff(c_2312, plain, (![V_702, V_230, U_229]: (relation(V_702, V_230) | ~accessible_world(U_229, V_702) | ~forename(U_229, V_230)))). % 13.21/4.50 tff(c_3247, plain, (![W_920, V_918, Y_919]: (W_920=V_918 | ~agent(skc13, Y_919, skc25) | ~theme(skc13, Y_919, W_920) | ~think_believe_consider(skc13, Y_919) | ~theme(skc13, skc23, V_918) | ~proposition(skc13, W_920) | ~proposition(skc13, V_918)))). % 13.21/4.50 tff(c_2569, plain, (![V_98, V_761]: (present(V_98, skc20) | ~accessible_world(V_761, V_98) | ~accessible_world(skc14, V_761)))). % 13.21/4.50 tff(c_4863, plain, (![W_906]: (skc18=W_906 | ~forename(skc13, W_906) | ~of(skc13, W_906, skc17)))). % 13.21/4.50 tff(c_4862, plain, (~accessible_world(skc13, skc13))). % 13.21/4.50 tff(c_4854, plain, (![V_161, V_811]: (jules_forename(V_161, skc18) | ~accessible_world(V_811, V_161) | ~accessible_world(skc13, V_811)))). % 13.21/4.50 tff(c_4845, plain, (![V_797]: (vincent_forename(V_797, skc18) | ~accessible_world(skc13, V_797)))). % 13.21/4.50 tff(c_3250, plain, (![W_920, V_918, Y_919]: (W_920=V_918 | ~agent(skc13, Y_919, skc17) | ~theme(skc13, Y_919, W_920) | ~think_believe_consider(skc13, Y_919) | ~theme(skc13, skc15, V_918) | ~proposition(skc13, W_920) | ~proposition(skc13, V_918)))). % 13.21/4.50 tff(c_4811, plain, (vincent_forename(skc13, skc18))). % 13.21/4.50 tff(c_4784, plain, (skc19=skc18)). % 13.21/4.50 tff(c_4750, plain, (skc21=skc18)). % 13.21/4.50 tff(c_2912, plain, (![V_825, V_264, U_263]: (singleton(V_825, V_264) | ~accessible_world(U_263, V_825) | ~entity(U_263, V_264)))). % 13.21/4.50 tff(c_3113, plain, (![V_879, U_196]: (agent(V_879, skf1(U_196), U_196) | ~accessible_world(skc22, V_879) | ~man(skc22, U_196)))). % 13.21/4.50 tff(c_4705, plain, (~accessible_world(skc22, skc13))). % 13.21/4.50 tff(c_4696, plain, (![V_1057]: (singleton(skc22, V_1057) | ~abstraction(skc13, V_1057)))). % 13.21/4.50 tff(c_4688, plain, (![V_1056]: (singleton(skc14, V_1056) | ~abstraction(skc13, V_1056)))). % 13.21/4.50 tff(c_4680, plain, (![V_1054]: (thing(skc22, V_1054) | ~abstraction(skc13, V_1054)))). % 13.21/4.50 tff(c_4679, plain, (![V_1054]: (thing(skc14, V_1054) | ~abstraction(skc13, V_1054)))). % 13.21/4.50 tff(c_2776, plain, (![V_803, V_20, U_19]: (thing(V_803, V_20) | ~accessible_world(U_19, V_803) | ~abstraction(U_19, V_20)))). % 13.21/4.50 tff(c_4669, plain, (![V_1048]: (~abstraction(V_1048, skc25) | ~accessible_world(skc22, V_1048)))). % 13.21/4.50 tff(c_4441, plain, (![V_1029]: (~abstraction(V_1029, skc17) | ~accessible_world(skc14, V_1029)))). % 13.21/4.50 tff(c_4588, plain, (![V_1040]: (~abstraction(V_1040, skc17) | ~accessible_world(skc22, V_1040)))). % 13.21/4.50 tff(c_4459, plain, (![V_1030]: (~abstraction(V_1030, skc25) | ~accessible_world(skc14, V_1030)))). % 13.21/4.50 tff(c_3673, plain, (![V_131]: (entity(V_131, skc25) | ~accessible_world(skc22, V_131)))). % 13.21/4.50 tff(c_4611, plain, (![V_1045]: (~male(skc22, V_1045) | ~abstraction(skc13, V_1045)))). % 13.21/4.50 tff(c_4603, plain, (![V_1044]: (~male(skc14, V_1044) | ~abstraction(skc13, V_1044)))). % 13.21/4.50 tff(c_4595, plain, (![V_1042]: (unisex(skc22, V_1042) | ~abstraction(skc13, V_1042)))). % 13.21/4.50 tff(c_4594, plain, (![V_1042]: (unisex(skc14, V_1042) | ~abstraction(skc13, V_1042)))). % 13.21/4.50 tff(c_2275, plain, (![V_690, V_26, U_25]: (unisex(V_690, V_26) | ~accessible_world(U_25, V_690) | ~abstraction(U_25, V_26)))). % 13.21/4.50 tff(c_3680, plain, (![V_131]: (entity(V_131, skc17) | ~accessible_world(skc22, V_131)))). % 13.21/4.50 tff(c_4502, plain, (![V_24]: (~entity(skc13, V_24) | ~abstraction(skc22, V_24)))). % 13.21/4.50 tff(c_4492, plain, (![V_24]: (~entity(skc13, V_24) | ~abstraction(skc14, V_24)))). % 13.21/4.50 tff(c_4482, plain, (![V_1035]: (~general(skc22, V_1035) | ~entity(skc13, V_1035)))). % 13.21/4.50 tff(c_4474, plain, (![V_1034]: (~general(skc14, V_1034) | ~entity(skc13, V_1034)))). % 13.21/4.50 tff(c_4466, plain, (![V_1032]: (specific(skc22, V_1032) | ~entity(skc13, V_1032)))). % 13.21/4.50 tff(c_4465, plain, (![V_1032]: (specific(skc14, V_1032) | ~entity(skc13, V_1032)))). % 13.21/4.50 tff(c_2480, plain, (![V_745, V_40, U_39]: (specific(V_745, V_40) | ~accessible_world(U_39, V_745) | ~entity(U_39, V_40)))). % 13.21/4.50 tff(c_3597, plain, (![V_131]: (entity(V_131, skc25) | ~accessible_world(skc14, V_131)))). % 13.21/4.50 tff(c_3611, plain, (![V_131]: (entity(V_131, skc17) | ~accessible_world(skc14, V_131)))). % 13.21/4.50 tff(c_4393, plain, (![V_1026]: (~male(skc22, V_1026) | ~eventuality(skc13, V_1026)))). % 13.21/4.50 tff(c_4385, plain, (![V_1025]: (~male(skc14, V_1025) | ~eventuality(skc13, V_1025)))). % 13.21/4.50 tff(c_4377, plain, (![V_1023]: (unisex(skc22, V_1023) | ~eventuality(skc13, V_1023)))). % 13.21/4.50 tff(c_4376, plain, (![V_1023]: (unisex(skc14, V_1023) | ~eventuality(skc13, V_1023)))). % 13.21/4.50 tff(c_2274, plain, (![V_690, V_14, U_13]: (unisex(V_690, V_14) | ~accessible_world(U_13, V_690) | ~eventuality(U_13, V_14)))). % 13.21/4.50 tff(c_4369, plain, (![V_195]: (~abstraction(skc13, skf1(V_195))))). % 13.21/4.50 tff(c_4188, plain, (![V_4]: (~abstraction(skc13, V_4) | ~event(skc22, V_4)))). % 13.21/4.50 tff(c_4333, plain, (~abstraction(skc13, skc20))). % 13.21/4.50 tff(c_4228, plain, (![V_4]: (~abstraction(skc13, V_4) | ~event(skc14, V_4)))). % 13.21/4.50 tff(c_4251, plain, (![V_1016]: (abstraction(skc22, V_1016) | ~proposition(skc13, V_1016)))). % 13.21/4.50 tff(c_4243, plain, (![V_1015]: (abstraction(skc14, V_1015) | ~proposition(skc13, V_1015)))). % 13.21/4.50 tff(c_4235, plain, (![V_1013]: (relation(skc22, V_1013) | ~proposition(skc13, V_1013)))). % 13.21/4.50 tff(c_4234, plain, (![V_1013]: (relation(skc14, V_1013) | ~proposition(skc13, V_1013)))). % 13.21/4.50 tff(c_2313, plain, (![V_702, V_16, U_15]: (relation(V_702, V_16) | ~accessible_world(U_15, V_702) | ~proposition(U_15, V_16)))). % 13.21/4.51 tff(c_4117, plain, (![V_1005]: (~eventuality(skc14, V_1005) | ~abstraction(skc13, V_1005)))). % 13.21/4.51 tff(c_4132, plain, (![V_1006]: (~entity(skc22, V_1006) | ~abstraction(skc13, V_1006)))). % 13.21/4.51 tff(c_4133, plain, (![V_1006]: (~eventuality(skc22, V_1006) | ~abstraction(skc13, V_1006)))). % 13.21/4.51 tff(c_4116, plain, (![V_1005]: (~entity(skc14, V_1005) | ~abstraction(skc13, V_1005)))). % 13.21/4.51 tff(c_3401, plain, (![V_24]: (~eventuality(skc13, V_24) | ~abstraction(skc14, V_24)))). % 13.21/4.51 tff(c_4100, plain, (![V_1002]: (general(skc22, V_1002) | ~abstraction(skc13, V_1002)))). % 13.21/4.51 tff(c_4099, plain, (![V_1002]: (general(skc14, V_1002) | ~abstraction(skc13, V_1002)))). % 13.21/4.51 tff(c_4093, plain, (![V_195]: (~entity(skc13, skf1(V_195))))). % 13.21/4.51 tff(c_2393, plain, (![V_731, V_24, U_23]: (general(V_731, V_24) | ~accessible_world(U_23, V_731) | ~abstraction(U_23, V_24)))). % 13.21/4.51 tff(c_4056, plain, (![V_4]: (~entity(skc13, V_4) | ~event(skc22, V_4)))). % 13.21/4.51 tff(c_4057, plain, (~accessible_world(skc14, skc13))). % 13.21/4.51 tff(c_3986, plain, (![V_996]: (~eventuality(skc22, V_996) | ~entity(skc13, V_996)))). % 13.21/4.51 tff(c_4039, plain, (~entity(skc13, skc20))). % 13.21/4.51 tff(c_4003, plain, (![V_4]: (~entity(skc13, V_4) | ~event(skc14, V_4)))). % 13.21/4.51 tff(c_3974, plain, (![V_995]: (~eventuality(skc14, V_995) | ~entity(skc13, V_995)))). % 13.21/4.51 tff(c_3962, plain, (![V_993]: (existent(skc22, V_993) | ~entity(skc13, V_993)))). % 13.21/4.51 tff(c_3961, plain, (![V_993]: (existent(skc14, V_993) | ~entity(skc13, V_993)))). % 13.21/4.51 tff(c_2685, plain, (![V_787, V_42, U_41]: (existent(V_787, V_42) | ~accessible_world(U_41, V_787) | ~entity(U_41, V_42)))). % 13.21/4.51 tff(c_3786, plain, (![V_42]: (~eventuality(skc13, V_42) | ~entity(skc22, V_42)))). % 13.21/4.51 tff(c_3640, plain, (![V_962]: (abstraction(skc22, V_962) | ~forename(skc13, V_962)))). % 13.21/4.51 tff(c_3780, plain, (![V_42]: (~eventuality(skc13, V_42) | ~entity(skc14, V_42)))). % 13.21/4.51 tff(c_3870, plain, (![V_986]: (singleton(skc22, V_986) | ~eventuality(skc13, V_986)))). % 13.21/4.51 tff(c_3862, plain, (![V_985]: (singleton(skc14, V_985) | ~eventuality(skc13, V_985)))). % 13.21/4.51 tff(c_3854, plain, (![V_983]: (thing(skc22, V_983) | ~eventuality(skc13, V_983)))). % 13.21/4.51 tff(c_3853, plain, (![V_983]: (thing(skc14, V_983) | ~eventuality(skc13, V_983)))). % 13.21/4.51 tff(c_2775, plain, (![V_803, V_6, U_5]: (thing(V_803, V_6) | ~accessible_world(U_5, V_803) | ~eventuality(U_5, V_6)))). % 13.21/4.51 tff(c_3648, plain, (![V_963]: (abstraction(skc14, V_963) | ~forename(skc13, V_963)))). % 13.21/4.51 tff(c_3407, plain, (![V_24]: (~eventuality(skc13, V_24) | ~abstraction(skc22, V_24)))). % 13.21/4.51 tff(c_3774, plain, (![V_977]: (~existent(skc22, V_977) | ~eventuality(skc13, V_977)))). % 13.21/4.51 tff(c_3766, plain, (![V_976]: (~existent(skc14, V_976) | ~eventuality(skc13, V_976)))). % 13.21/4.51 tff(c_3758, plain, (![V_974]: (nonexistent(skc22, V_974) | ~eventuality(skc13, V_974)))). % 13.21/4.51 tff(c_3757, plain, (![V_974]: (nonexistent(skc14, V_974) | ~eventuality(skc13, V_974)))). % 13.21/4.51 tff(c_2298, plain, (![V_699, V_12, U_11]: (nonexistent(V_699, V_12) | ~accessible_world(U_11, V_699) | ~eventuality(U_11, V_12)))). % 13.21/4.51 tff(c_3696, plain, (![V_968]: (singleton(skc14, V_968) | ~entity(skc13, V_968)))). % 13.21/4.51 tff(c_3704, plain, (![V_969]: (singleton(skc22, V_969) | ~entity(skc13, V_969)))). % 13.21/4.51 tff(c_3740, plain, (~entity(skc14, skc16))). % 13.21/4.51 tff(c_3742, plain, (~entity(skc14, skc23))). % 13.21/4.51 tff(c_3741, plain, (~entity(skc14, skc15))). % 13.21/4.51 tff(c_3345, plain, (![V_935]: (~entity(skc14, V_935) | ~event(skc13, V_935)))). % 13.21/4.51 tff(c_3688, plain, (![V_966]: (thing(skc22, V_966) | ~entity(skc13, V_966)))). % 13.21/4.51 tff(c_3687, plain, (![V_966]: (thing(skc14, V_966) | ~entity(skc13, V_966)))). % 13.21/4.51 tff(c_2774, plain, (![V_803, V_38, U_37]: (thing(V_803, V_38) | ~accessible_world(U_37, V_803) | ~entity(U_37, V_38)))). % 13.21/4.51 tff(c_3667, plain, (entity(skc22, skc17))). % 13.21/4.51 tff(c_3666, plain, (entity(skc22, skc25))). % 13.21/4.51 tff(c_3558, plain, (![V_951]: (entity(skc22, V_951) | ~human_person(skc13, V_951)))). % 13.21/4.51 tff(c_3620, plain, (![V_959]: (relation(skc14, V_959) | ~forename(skc13, V_959)))). % 13.21/4.51 tff(c_3628, plain, (![V_960]: (relation(skc22, V_960) | ~forename(skc13, V_960)))). % 13.21/4.51 tff(c_3559, plain, (![V_951]: (impartial(skc22, V_951) | ~human_person(skc13, V_951)))). % 13.21/4.51 tff(c_3605, plain, (![V_957]: (relname(skc22, V_957) | ~forename(skc13, V_957)))). % 13.21/4.51 tff(c_3604, plain, (![V_957]: (relname(skc14, V_957) | ~forename(skc13, V_957)))). % 13.21/4.51 tff(c_3591, plain, (entity(skc14, skc17))). % 13.21/4.51 tff(c_2430, plain, (![V_736, V_54, U_53]: (relname(V_736, V_54) | ~accessible_world(U_53, V_736) | ~forename(U_53, V_54)))). % 13.21/4.51 tff(c_3590, plain, (entity(skc14, skc25))). % 13.21/4.51 tff(c_3542, plain, (![V_950]: (entity(skc14, V_950) | ~human_person(skc13, V_950)))). % 13.21/4.51 tff(c_3543, plain, (![V_950]: (impartial(skc14, V_950) | ~human_person(skc13, V_950)))). % 13.21/4.51 tff(c_3560, plain, (![V_951]: (living(skc22, V_951) | ~human_person(skc13, V_951)))). % 13.21/4.51 tff(c_3544, plain, (![V_950]: (living(skc14, V_950) | ~human_person(skc13, V_950)))). % 13.21/4.51 tff(c_3528, plain, (![V_948]: (organism(skc22, V_948) | ~human_person(skc13, V_948)))). % 13.21/4.51 tff(c_3527, plain, (![V_948]: (organism(skc14, V_948) | ~human_person(skc13, V_948)))). % 13.21/4.51 tff(c_3521, plain, (~entity(skc22, skc23))). % 13.21/4.51 tff(c_3520, plain, (~entity(skc22, skc15))). % 13.21/4.51 tff(c_2957, plain, (![V_835, V_34, U_33]: (organism(V_835, V_34) | ~accessible_world(U_33, V_835) | ~human_person(U_33, V_34)))). % 13.21/4.51 tff(c_3519, plain, (~entity(skc22, skc16))). % 13.21/4.51 tff(c_3378, plain, (![V_939]: (~entity(skc22, V_939) | ~event(skc13, V_939)))). % 13.21/4.51 tff(c_3379, plain, (![V_939]: (~abstraction(skc22, V_939) | ~event(skc13, V_939)))). % 13.21/4.51 tff(c_3346, plain, (![V_935]: (~abstraction(skc14, V_935) | ~event(skc13, V_935)))). % 13.21/4.51 tff(c_3395, plain, (![V_941]: (~general(skc22, V_941) | ~eventuality(skc13, V_941)))). % 13.21/4.51 tff(c_3387, plain, (![V_940]: (~general(skc14, V_940) | ~eventuality(skc13, V_940)))). % 13.21/4.51 tff(c_3353, plain, (![V_937]: (specific(skc22, V_937) | ~eventuality(skc13, V_937)))). % 13.21/4.51 tff(c_3352, plain, (![V_937]: (specific(skc14, V_937) | ~eventuality(skc13, V_937)))). % 13.21/4.51 tff(c_3320, plain, (![V_933]: (eventuality(skc22, V_933) | ~event(skc13, V_933)))). % 13.21/4.51 tff(c_2479, plain, (![V_745, V_10, U_9]: (specific(V_745, V_10) | ~accessible_world(U_9, V_745) | ~eventuality(U_9, V_10)))). % 13.21/4.51 tff(c_3319, plain, (![V_933]: (eventuality(skc14, V_933) | ~event(skc13, V_933)))). % 13.21/4.51 tff(c_2637, plain, (![V_775, V_4, U_3]: (eventuality(V_775, V_4) | ~accessible_world(U_3, V_775) | ~event(U_3, V_4)))). % 13.21/4.51 tff(c_3283, plain, (![V_929]: (~human(skc22, V_929) | ~abstraction(skc13, V_929)))). % 13.21/4.51 tff(c_3275, plain, (![V_928]: (~human(skc14, V_928) | ~abstraction(skc13, V_928)))). % 13.21/4.51 tff(c_3267, plain, (![V_926]: (nonhuman(skc22, V_926) | ~abstraction(skc13, V_926)))). % 13.21/4.51 tff(c_3266, plain, (![V_926]: (nonhuman(skc14, V_926) | ~abstraction(skc13, V_926)))). % 13.21/4.51 tff(c_2994, plain, (![V_844, V_22, U_21]: (nonhuman(V_844, V_22) | ~accessible_world(U_21, V_844) | ~abstraction(U_21, V_22)))). % 13.21/4.51 tff(c_3150, plain, (![V_900]: (be(V_900, skc16, skc17, skc17) | ~accessible_world(skc13, V_900)))). % 13.21/4.51 tff(c_3161, plain, (![V_901, V_902]: (~entity(V_901, skf1(V_902)) | ~accessible_world(skc22, V_901)))). % 13.21/4.51 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.21/4.51 tff(c_3162, plain, (![V_901, V_902]: (~abstraction(V_901, skf1(V_902)) | ~accessible_world(skc22, V_901)))). % 13.21/4.51 tff(c_3125, plain, (![V_886]: (theme(V_886, skc15, skc14) | ~accessible_world(skc13, V_886)))). % 13.21/4.51 tff(c_3098, plain, (![V_870]: (of(V_870, skc24, skc25) | ~accessible_world(skc13, V_870)))). % 13.21/4.51 tff(c_3096, plain, (![V_870]: (of(V_870, skc18, skc17) | ~accessible_world(skc13, V_870)))). % 13.21/4.51 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.21/4.51 tff(c_2652, plain, (![V_779, V_191]: (smoke(V_779, skf1(V_191)) | ~accessible_world(skc22, V_779)))). % 13.21/4.51 tff(c_2838, plain, (![V_813, V_195]: (event(V_813, skf1(V_195)) | ~accessible_world(skc22, V_813)))). % 13.21/4.51 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.21/4.51 tff(c_3114, plain, (![V_879]: (agent(V_879, skc20, skc17) | ~accessible_world(skc14, V_879)))). % 13.21/4.51 tff(c_3115, plain, (![V_879]: (agent(V_879, skc23, skc25) | ~accessible_world(skc13, V_879)))). % 13.21/4.51 tff(c_3116, plain, (![V_879]: (agent(V_879, skc15, skc17) | ~accessible_world(skc13, V_879)))). % 13.21/4.51 tff(c_3126, plain, (![V_886]: (theme(V_886, skc23, skc22) | ~accessible_world(skc13, V_886)))). % 13.21/4.51 tff(c_2552, plain, (![V_757, V_193]: (present(V_757, skf1(V_193)) | ~accessible_world(skc22, V_757)))). % 13.21/4.51 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.21/4.51 tff(c_2561, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc22, V_110)))). % 13.21/4.51 tff(c_2558, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc14, V_110)))). % 13.21/4.51 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.21/4.51 tff(c_2779, plain, (![V_110]: (abstraction(V_110, skc24) | ~accessible_world(skc22, V_110)))). % 13.21/4.51 tff(c_2470, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc14, V_110)))). % 13.21/4.51 tff(c_2731, plain, (![V_110]: (abstraction(V_110, skc22) | ~accessible_world(skc14, V_110)))). % 13.21/4.51 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.21/4.51 tff(c_2473, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc22, V_110)))). % 13.21/4.51 tff(c_3060, plain, (![V_864]: (man(V_864, skc25) | ~accessible_world(skc13, V_864)))). % 13.21/4.51 tff(c_3059, plain, (![V_864]: (man(V_864, skc17) | ~accessible_world(skc13, V_864)))). % 13.21/4.51 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.21/4.51 tff(c_2782, plain, (![V_110]: (abstraction(V_110, skc24) | ~accessible_world(skc14, V_110)))). % 13.21/4.51 tff(c_2734, plain, (![V_110]: (abstraction(V_110, skc22) | ~accessible_world(skc22, V_110)))). % 13.21/4.51 tff(c_3018, plain, (![V_856]: (human_person(V_856, skc17) | ~accessible_world(skc13, V_856)))). % 13.21/4.51 tff(c_3017, plain, (![V_856]: (human_person(V_856, skc25) | ~accessible_world(skc13, V_856)))). % 13.21/4.51 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.21/4.51 tff(c_2788, plain, (![U_3]: (~accessible_world(skc13, U_3) | ~event(U_3, skc25)))). % 13.21/4.51 tff(c_2853, plain, (![V_816]: (~entity(V_816, skc15) | ~accessible_world(skc13, V_816)))). % 13.21/4.51 tff(c_2672, plain, (![U_3]: (~accessible_world(skc13, U_3) | ~event(U_3, skc17)))). % 13.21/4.51 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.21/4.51 tff(c_2708, plain, (![V_782]: (~entity(V_782, skc20) | ~accessible_world(skc14, V_782)))). % 13.21/4.51 tff(c_2666, plain, (![V_783]: (~abstraction(V_783, skc20) | ~accessible_world(skc14, V_783)))). % 13.21/4.51 tff(c_2982, plain, (![V_840]: (proposition(V_840, skc22) | ~accessible_world(skc13, V_840)))). % 13.21/4.52 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.21/4.52 tff(c_2981, plain, (![V_840]: (proposition(V_840, skc14) | ~accessible_world(skc13, V_840)))). % 13.21/4.52 tff(c_2975, plain, (~abstraction(skc22, skc23))). % 13.21/4.52 tff(c_2974, plain, (~abstraction(skc14, skc23))). % 13.21/4.52 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.21/4.52 tff(c_2866, plain, (![V_817]: (~abstraction(V_817, skc23) | ~accessible_world(skc13, V_817)))). % 13.21/4.52 tff(c_2966, plain, (~abstraction(skc22, skc15))). % 13.21/4.52 tff(c_2965, plain, (~abstraction(skc14, skc15))). % 13.21/4.52 tff(c_2854, plain, (![V_816]: (~abstraction(V_816, skc15) | ~accessible_world(skc13, V_816)))). % 13.21/4.52 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.21/4.52 tff(c_2865, plain, (![V_817]: (~entity(V_817, skc23) | ~accessible_world(skc13, V_817)))). % 13.21/4.52 tff(c_2936, plain, (![V_829]: (entity(V_829, skc25) | ~accessible_world(skc13, V_829)))). % 13.21/4.52 tff(c_2935, plain, (![V_829]: (entity(V_829, skc17) | ~accessible_world(skc13, V_829)))). % 13.21/4.52 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.21/4.52 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.21/4.52 tff(c_2888, plain, (![V_819]: (animate(V_819, skc25) | ~accessible_world(skc13, V_819)))). % 13.21/4.52 tff(c_2887, plain, (![V_819]: (animate(V_819, skc17) | ~accessible_world(skc13, V_819)))). % 13.21/4.52 tff(c_2359, plain, (![V_721]: (human(V_721, skc25) | ~accessible_world(skc13, V_721)))). % 13.21/4.52 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.21/4.52 tff(c_2841, plain, (![V_813]: (event(V_813, skc23) | ~accessible_world(skc13, V_813)))). % 13.21/4.52 tff(c_2840, plain, (![V_813]: (event(V_813, skc15) | ~accessible_world(skc13, V_813)))). % 13.21/4.52 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.21/4.52 tff(c_2804, plain, (![V_808]: (jules_forename(V_808, skc18) | ~accessible_world(skc13, V_808)))). % 13.21/4.52 tff(c_2797, plain, (~abstraction(skc22, skc25))). % 13.21/4.52 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.21/4.52 tff(c_2796, plain, (~abstraction(skc14, skc25))). % 13.21/4.52 tff(c_2521, plain, (![V_754]: (~abstraction(V_754, skc25) | ~accessible_world(skc13, V_754)))). % 13.21/4.52 tff(c_2520, plain, (![V_754]: (~eventuality(V_754, skc25) | ~accessible_world(skc13, V_754)))). % 13.21/4.52 tff(c_2765, plain, (abstraction(skc14, skc24))). % 13.21/4.52 tff(c_2766, plain, (abstraction(skc22, skc24))). % 13.21/4.52 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.21/4.52 tff(c_2419, plain, (![V_713]: (abstraction(V_713, skc24) | ~accessible_world(skc13, V_713)))). % 13.21/4.52 tff(c_2741, plain, (![V_797]: (vincent_forename(V_797, skc24) | ~accessible_world(skc13, V_797)))). % 13.21/4.52 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.21/4.52 tff(c_2728, plain, (abstraction(skc22, skc22))). % 13.21/4.52 tff(c_2727, plain, (abstraction(skc14, skc22))). % 13.21/4.52 tff(c_2457, plain, (![V_741]: (abstraction(V_741, skc22) | ~accessible_world(skc13, V_741)))). % 13.21/4.52 tff(c_2710, plain, (![V_195]: (~entity(skc22, skf1(V_195))))). % 13.21/4.52 tff(c_2714, plain, (~entity(skc14, skc20))). % 13.21/4.52 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.21/4.52 tff(c_2713, plain, (~entity(skc13, skc23))). % 13.21/4.52 tff(c_2712, plain, (~entity(skc13, skc15))). % 13.21/4.52 tff(c_2439, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 13.21/4.52 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.21/4.52 tff(c_2358, plain, (![V_721]: (human(V_721, skc17) | ~accessible_world(skc13, V_721)))). % 13.21/4.52 tff(c_2597, plain, (![V_767]: (~entity(V_767, skc16) | ~accessible_world(skc13, V_767)))). % 13.21/4.52 tff(c_2532, plain, (![V_755]: (~eventuality(V_755, skc17) | ~accessible_world(skc13, V_755)))). % 13.21/4.52 tff(c_2661, plain, (![V_782]: (event(V_782, skc20) | ~accessible_world(skc14, V_782)))). % 13.21/4.52 tff(c_2653, plain, (![V_779]: (smoke(V_779, skc20) | ~accessible_world(skc14, V_779)))). % 13.21/4.52 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.21/4.52 tff(c_2646, plain, (~abstraction(skc22, skc17))). % 13.21/4.52 tff(c_2645, plain, (~abstraction(skc14, skc17))). % 13.21/4.52 tff(c_2533, plain, (![V_755]: (~abstraction(V_755, skc17) | ~accessible_world(skc13, V_755)))). % 13.21/4.52 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.21/4.52 tff(c_2627, plain, (~abstraction(skc22, skc16))). % 13.21/4.52 tff(c_2626, plain, (~abstraction(skc14, skc16))). % 13.21/4.52 tff(c_2598, plain, (![V_767]: (~abstraction(V_767, skc16) | ~accessible_world(skc13, V_767)))). % 13.21/4.52 tff(c_2610, plain, (![V_769]: (think_believe_consider(V_769, skc23) | ~accessible_world(skc13, V_769)))). % 13.21/4.52 tff(c_2609, plain, (![V_769]: (think_believe_consider(V_769, skc15) | ~accessible_world(skc13, V_769)))). % 13.21/4.52 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.21/4.52 tff(c_2589, plain, (![V_766]: (event(V_766, skc16) | ~accessible_world(skc13, V_766)))). % 13.21/4.52 tff(c_2588, plain, (![V_766]: (eventuality(V_766, skc16) | ~accessible_world(skc13, V_766)))). % 13.21/4.52 tff(c_2577, plain, (![V_763]: (state(V_763, skc16) | ~accessible_world(skc13, V_763)))). % 13.21/4.52 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.21/4.52 tff(c_2555, plain, (![V_757]: (present(V_757, skc23) | ~accessible_world(skc13, V_757)))). % 13.21/4.52 tff(c_2554, plain, (![V_757]: (present(V_757, skc20) | ~accessible_world(skc14, V_757)))). % 13.21/4.52 tff(c_2553, plain, (![V_757]: (present(V_757, skc15) | ~accessible_world(skc13, V_757)))). % 13.21/4.52 tff(c_2542, plain, (abstraction(skc22, skc14))). % 13.21/4.52 tff(c_2541, plain, (abstraction(skc14, skc14))). % 13.21/4.52 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.21/4.52 tff(c_2458, plain, (![V_741]: (abstraction(V_741, skc14) | ~accessible_world(skc13, V_741)))). % 13.21/4.52 tff(c_2509, plain, (![V_751]: (male(V_751, skc17) | ~accessible_world(skc13, V_751)))). % 13.21/4.52 tff(c_2508, plain, (![V_751]: (male(V_751, skc25) | ~accessible_world(skc13, V_751)))). % 13.21/4.52 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.21/4.52 tff(c_2497, plain, (![V_195]: (~abstraction(skc22, skf1(V_195))))). % 13.21/4.52 tff(c_2501, plain, (~abstraction(skc14, skc20))). % 13.21/4.52 tff(c_2500, plain, (~abstraction(skc13, skc23))). % 13.21/4.52 tff(c_2499, plain, (~abstraction(skc13, skc15))). % 13.21/4.52 tff(c_2389, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 13.21/4.52 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.21/4.52 tff(c_2467, plain, (abstraction(skc22, skc18))). % 13.21/4.52 tff(c_2466, plain, (abstraction(skc14, skc18))). % 13.21/4.52 tff(c_2420, plain, (![V_713]: (abstraction(V_713, skc18) | ~accessible_world(skc13, V_713)))). % 13.21/4.52 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.21/4.52 tff(c_2438, plain, (~entity(skc13, skc16))). % 13.21/4.52 tff(c_2324, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 13.21/4.52 tff(c_2425, plain, (abstraction(skc13, skc18))). % 13.21/4.52 tff(c_2424, plain, (abstraction(skc13, skc24))). % 13.21/4.52 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.21/4.52 tff(c_1720, plain, (![U_555, V_556]: (abstraction(U_555, V_556) | ~forename(U_555, V_556)))). % 13.21/4.52 tff(c_2388, plain, (~abstraction(skc13, skc16))). % 13.21/4.52 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.21/4.52 tff(c_973, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.52 tff(c_2319, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.52 tff(c_2336, plain, (![V_713]: (forename(V_713, skc24) | ~accessible_world(skc13, V_713)))). % 13.21/4.52 tff(c_2337, plain, (![V_713]: (forename(V_713, skc18) | ~accessible_world(skc13, V_713)))). % 13.21/4.52 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.21/4.52 tff(c_375, plain, (![U_263, V_264]: (singleton(U_263, V_264) | ~entity(U_263, V_264)))). % 13.21/4.52 tff(c_346, plain, (![U_253, V_254]: (~human(U_253, V_254) | ~abstraction(U_253, V_254)))). % 13.21/4.52 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.21/4.52 tff(c_329, plain, (![U_245, V_246]: (impartial(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.21/4.52 tff(c_276, plain, (![U_11, V_12]: (~existent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 13.21/4.52 tff(c_335, plain, (![U_247, V_248]: (~general(U_247, V_248) | ~entity(U_247, V_248)))). % 13.21/4.52 tff(c_370, plain, (![U_261, V_262]: (singleton(U_261, V_262) | ~eventuality(U_261, V_262)))). % 13.21/4.52 tff(c_2306, plain, (~event(skc13, skc17))). % 13.21/4.52 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.21/4.52 tff(c_2302, plain, (~event(skc13, skc25))). % 13.21/4.52 tff(c_2294, plain, (~eventuality(skc13, skc17))). % 13.21/4.52 tff(c_2293, plain, (~eventuality(skc13, skc25))). % 13.21/4.52 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.21/4.52 tff(c_356, plain, (![U_257, V_258]: (~male(U_257, V_258) | ~eventuality(U_257, V_258)))). % 13.21/4.52 tff(c_330, plain, (![U_245, V_246]: (living(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.21/4.52 tff(c_2284, plain, (entity(skc13, skc17))). % 13.21/4.52 tff(c_2283, plain, (entity(skc13, skc25))). % 13.21/4.52 tff(c_328, plain, (![U_245, V_246]: (entity(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.21/4.52 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.21/4.52 tff(c_2268, plain, (abstraction(skc13, skc22))). % 13.21/4.52 tff(c_2267, plain, (abstraction(skc13, skc14))). % 13.21/4.52 tff(c_351, plain, (![U_15, V_16]: (abstraction(U_15, V_16) | ~proposition(U_15, V_16)))). % 13.21/4.52 tff(c_220, plain, (![U_196]: (agent(skc22, skf1(U_196), U_196) | ~man(skc22, U_196)))). % 13.21/4.52 tff(c_249, plain, (![U_209, V_210]: (singleton(U_209, V_210) | ~abstraction(U_209, V_210)))). % 13.21/4.52 tff(c_2257, plain, (~abstraction(skc13, skc17))). % 13.21/4.52 tff(c_2256, plain, (~abstraction(skc13, skc25))). % 13.21/4.52 tff(c_282, plain, (![U_223, V_224]: (~male(U_223, V_224) | ~abstraction(U_223, V_224)))). % 13.21/4.52 tff(c_2236, plain, (![V_191]: (smoke(skc22, skf1(V_191))))). % 13.21/4.52 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.21/4.52 tff(c_289, plain, (![U_229, V_230]: (relation(U_229, V_230) | ~forename(U_229, V_230)))). % 13.21/4.52 tff(c_1714, plain, (![V_195]: (event(skc22, skf1(V_195))))). % 13.21/4.52 tff(c_341, plain, (![U_251, V_252]: (~general(U_251, V_252) | ~eventuality(U_251, V_252)))). % 13.21/4.52 tff(c_967, plain, (![V_193]: (present(skc22, skf1(V_193))))). % 13.21/4.53 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 13.21/4.53 tff(c_365, plain, (human(skc13, skc17))). % 13.21/4.53 tff(c_364, plain, (human(skc13, skc25))). % 13.21/4.53 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 13.21/4.53 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 13.21/4.53 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 13.21/4.53 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 13.21/4.53 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 13.21/4.53 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 13.21/4.53 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 13.21/4.53 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 13.21/4.53 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 13.21/4.53 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 13.21/4.53 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 13.21/4.53 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 13.21/4.53 tff(c_309, plain, (eventuality(skc13, skc16))). % 13.21/4.53 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 13.21/4.53 tff(c_304, plain, (event(skc13, skc16))). % 13.21/4.53 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 13.21/4.53 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 13.21/4.53 tff(c_298, plain, (male(skc13, skc25))). % 13.21/4.53 tff(c_297, plain, (male(skc13, skc17))). % 13.21/4.53 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 13.21/4.53 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 13.21/4.53 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 13.21/4.53 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 13.21/4.53 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 13.21/4.53 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 13.21/4.53 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 13.21/4.53 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 13.21/4.53 tff(c_260, plain, (animate(skc13, skc17))). % 13.21/4.53 tff(c_259, plain, (animate(skc13, skc25))). % 13.21/4.53 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 13.21/4.53 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 13.21/4.53 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 13.21/4.53 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 13.21/4.53 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 13.21/4.53 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 13.21/4.53 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 13.21/4.53 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.21/4.53 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 13.21/4.53 tff(c_229, plain, (human_person(skc13, skc25))). % 13.21/4.53 tff(c_228, plain, (human_person(skc13, skc17))). % 13.21/4.53 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 13.21/4.53 tff(c_212, plain, (be(skc13, skc16, skc17, skc17))). % 13.21/4.53 tff(c_210, plain, (theme(skc13, skc15, skc14))). % 13.21/4.53 tff(c_202, plain, (of(skc13, skc18, skc17))). % 13.21/4.53 tff(c_204, plain, (agent(skc14, skc20, skc17))). % 13.21/4.53 tff(c_198, plain, (theme(skc13, skc23, skc22))). % 13.21/4.53 tff(c_196, plain, (agent(skc13, skc23, skc25))). % 13.21/4.53 tff(c_194, plain, (of(skc13, skc24, skc25))). % 13.21/4.53 tff(c_206, plain, (agent(skc13, skc15, skc17))). % 13.21/4.53 tff(c_174, plain, (man(skc13, skc17))). % 13.21/4.53 tff(c_178, plain, (state(skc13, skc16))). % 13.21/4.53 tff(c_180, plain, (think_believe_consider(skc13, skc15))). % 13.21/4.53 tff(c_182, plain, (present(skc13, skc15))). % 13.21/4.53 tff(c_172, plain, (smoke(skc14, skc20))). % 13.21/4.53 tff(c_170, plain, (present(skc14, skc20))). % 13.21/4.53 tff(c_184, plain, (event(skc13, skc15))). % 13.21/4.53 tff(c_146, plain, (man(skc13, skc25))). % 13.21/4.53 tff(c_186, plain, (proposition(skc13, skc14))). % 13.21/4.53 tff(c_148, plain, (forename(skc13, skc24))). % 13.21/4.53 tff(c_150, plain, (vincent_forename(skc13, skc24))). % 13.21/4.53 tff(c_152, plain, (event(skc13, skc23))). % 13.21/4.53 tff(c_164, plain, (forename(skc13, skc18))). % 13.21/4.53 tff(c_188, plain, (accessible_world(skc13, skc14))). % 13.21/4.53 tff(c_162, plain, (jules_forename(skc13, skc18))). % 13.21/4.53 tff(c_160, plain, (event(skc14, skc20))). % 13.21/4.53 tff(c_154, plain, (present(skc13, skc23))). % 13.21/4.53 tff(c_156, plain, (think_believe_consider(skc13, skc23))). % 13.21/4.53 tff(c_190, plain, (accessible_world(skc13, skc22))). % 13.21/4.53 tff(c_192, plain, (proposition(skc13, skc22))). % 13.21/4.53 tff(c_144, plain, (actual_world(skc13))). % 13.21/4.53 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.21/4.53 %------------------------------------------------------------------------------