%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP246-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 : n009.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:46 PM UTC 2025 % Result : Satisfiable 13.11s 4.38s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP246-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 09:46:41 EDT 2025 % 0.13/0.34 % CPUTime : % 13.11/4.38 % 13.11/4.38 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.11/4.38 % 13.11/4.38 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.11/4.39 %$ 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 % 13.11/4.39 % 13.11/4.39 %Foreground sorts: % 13.11/4.39 % 13.11/4.39 % 13.11/4.39 %Background operators: % 13.11/4.39 % 13.11/4.39 % 13.11/4.39 %Foreground operators: % 13.11/4.39 tff(skc16, type, skc16: $i). % 13.11/4.39 tff(relation, type, relation: ($i * $i) > $o). % 13.11/4.39 tff(forename, type, forename: ($i * $i) > $o). % 13.11/4.39 tff(be, type, be: ($i * $i * $i * $i) > $o). % 13.11/4.39 tff(theme, type, theme: ($i * $i * $i) > $o). % 13.11/4.39 tff(living, type, living: ($i * $i) > $o). % 13.11/4.39 tff(human_person, type, human_person: ($i * $i) > $o). % 13.11/4.39 tff(present, type, present: ($i * $i) > $o). % 13.11/4.39 tff(entity, type, entity: ($i * $i) > $o). % 13.11/4.39 tff(skc18, type, skc18: $i). % 13.11/4.39 tff(eventuality, type, eventuality: ($i * $i) > $o). % 13.11/4.39 tff(existent, type, existent: ($i * $i) > $o). % 13.11/4.39 tff(abstraction, type, abstraction: ($i * $i) > $o). % 13.11/4.39 tff(skc25, type, skc25: $i). % 13.11/4.39 tff(skf1, type, skf1: $i > $i). % 13.11/4.39 tff(proposition, type, proposition: ($i * $i) > $o). % 13.11/4.39 tff(relname, type, relname: ($i * $i) > $o). % 13.11/4.39 tff(skc14, type, skc14: $i). % 13.11/4.39 tff(singleton, type, singleton: ($i * $i) > $o). % 13.11/4.39 tff(skc17, type, skc17: $i). % 13.11/4.39 tff(skc13, type, skc13: $i). % 13.11/4.39 tff(male, type, male: ($i * $i) > $o). % 13.11/4.39 tff(organism, type, organism: ($i * $i) > $o). % 13.11/4.39 tff(animate, type, animate: ($i * $i) > $o). % 13.11/4.39 tff(of, type, of: ($i * $i * $i) > $o). % 13.11/4.39 tff(actual_world, type, actual_world: $i > $o). % 13.11/4.39 tff(agent, type, agent: ($i * $i * $i) > $o). % 13.11/4.39 tff(skc24, type, skc24: $i). % 13.11/4.39 tff(skc20, type, skc20: $i). % 13.11/4.39 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 13.11/4.39 tff(general, type, general: ($i * $i) > $o). % 13.11/4.39 tff(smoke, type, smoke: ($i * $i) > $o). % 13.11/4.39 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 13.11/4.39 tff(skc23, type, skc23: $i). % 13.11/4.39 tff(event, type, event: ($i * $i) > $o). % 13.11/4.39 tff(skc21, type, skc21: $i). % 13.11/4.39 tff(skc22, type, skc22: $i). % 13.11/4.39 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 13.11/4.39 tff(state, type, state: ($i * $i) > $o). % 13.11/4.39 tff(thing, type, thing: ($i * $i) > $o). % 13.11/4.39 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 13.11/4.39 tff(skc15, type, skc15: $i). % 13.11/4.39 tff(human, type, human: ($i * $i) > $o). % 13.11/4.39 tff(man, type, man: ($i * $i) > $o). % 13.11/4.39 tff(unisex, type, unisex: ($i * $i) > $o). % 13.11/4.39 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 13.11/4.39 tff(impartial, type, impartial: ($i * $i) > $o). % 13.11/4.39 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 13.11/4.39 tff(specific, type, specific: ($i * $i) > $o). % 13.11/4.39 tff(skc19, type, skc19: $i). % 13.11/4.39 % 13.11/4.39 %Saturated clause set: % 13.11/4.40 tff(c_7869, plain, (![V_1586, V_883]: (skc14=V_1586 | ~think_believe_consider(V_883, skc15) | ~think_believe_consider(V_883, skf1(skc17)) | ~theme(V_883, skf1(skc17), V_1586) | ~proposition(V_883, skc14) | ~proposition(V_883, V_1586) | ~accessible_world(skc20, V_883) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7835, plain, (![W_1572, V_1570, V_888]: (W_1572=V_1570 | ~theme(V_888, skc15, W_1572) | ~think_believe_consider(V_888, skc15) | ~think_believe_consider(V_888, skf1(skc17)) | ~theme(V_888, skf1(skc17), V_1570) | ~proposition(V_888, W_1572) | ~proposition(V_888, V_1570) | ~accessible_world(skc20, V_888) | ~accessible_world(skc13, V_888)))). % 13.11/4.40 tff(c_7859, plain, (![V_1581, V_883]: (skc20=V_1581 | ~think_believe_consider(V_883, skc21) | ~think_believe_consider(V_883, skf1(skc23)) | ~theme(V_883, skf1(skc23), V_1581) | ~proposition(V_883, skc20) | ~proposition(V_883, V_1581) | ~accessible_world(skc20, V_883) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7838, plain, (![W_1572, V_1570, V_888]: (W_1572=V_1570 | ~theme(V_888, skc21, W_1572) | ~think_believe_consider(V_888, skc21) | ~think_believe_consider(V_888, skf1(skc23)) | ~theme(V_888, skf1(skc23), V_1570) | ~proposition(V_888, W_1572) | ~proposition(V_888, V_1570) | ~accessible_world(skc20, V_888) | ~accessible_world(skc13, V_888)))). % 13.11/4.40 tff(c_7841, plain, (![W_1572, V_1570, V_888]: (W_1572=V_1570 | ~theme(V_888, skc24, W_1572) | ~think_believe_consider(V_888, skc24) | ~think_believe_consider(V_888, skf1(skc23)) | ~theme(V_888, skf1(skc23), V_1570) | ~proposition(V_888, W_1572) | ~proposition(V_888, V_1570) | ~accessible_world(skc20, V_888) | ~accessible_world(skc14, V_888)))). % 13.11/4.40 tff(c_7832, plain, (![W_1572, V_1570, V_888, U_196]: (W_1572=V_1570 | ~theme(V_888, skf1(U_196), W_1572) | ~think_believe_consider(V_888, skf1(U_196)) | ~theme(V_888, skf1(U_196), V_1570) | ~proposition(V_888, W_1572) | ~proposition(V_888, V_1570) | ~accessible_world(skc20, V_888) | ~man(skc20, U_196)))). % 13.11/4.40 tff(c_4763, plain, (![U_1076, V_1075, V_189, Y_188, W_184]: (W_184=V_189 | ~agent(V_1075, Y_188, U_1076) | ~theme(V_1075, Y_188, W_184) | ~think_believe_consider(V_1075, Y_188) | ~think_believe_consider(V_1075, skf1(U_1076)) | ~theme(V_1075, skf1(U_1076), V_189) | ~proposition(V_1075, W_184) | ~proposition(V_1075, V_189) | ~accessible_world(skc20, V_1075) | ~man(skc20, U_1076)))). % 13.11/4.40 tff(c_7804, plain, (![V_1561, V_883]: (skc20=V_1561 | ~agent(V_883, skc21, skc23) | ~think_believe_consider(V_883, skc21) | ~think_believe_consider(V_883, skc24) | ~theme(V_883, skc24, V_1561) | ~proposition(V_883, skc20) | ~proposition(V_883, V_1561) | ~accessible_world(skc14, V_883) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7803, plain, (![V_1561, V_883]: (skc14=V_1561 | ~agent(V_883, skc15, skc23) | ~think_believe_consider(V_883, skc15) | ~think_believe_consider(V_883, skc24) | ~theme(V_883, skc24, V_1561) | ~proposition(V_883, skc14) | ~proposition(V_883, V_1561) | ~accessible_world(skc14, V_883) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_3264, plain, (![W_184, V_189, V_927, Y_188]: (W_184=V_189 | ~agent(V_927, Y_188, skc23) | ~theme(V_927, Y_188, W_184) | ~think_believe_consider(V_927, Y_188) | ~think_believe_consider(V_927, skc24) | ~theme(V_927, skc24, V_189) | ~proposition(V_927, W_184) | ~proposition(V_927, V_189) | ~accessible_world(skc14, V_927)))). % 13.11/4.40 tff(c_7792, plain, (![V_883]: (~agent(V_883, skc21, skc17) | ~think_believe_consider(V_883, skc21) | ~think_believe_consider(V_883, skc15) | ~proposition(V_883, skc20) | ~proposition(V_883, skc14) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7761, plain, (![V_1551, V_883]: (skc20=V_1551 | ~agent(V_883, skc21, skc17) | ~think_believe_consider(V_883, skc21) | ~think_believe_consider(V_883, skc15) | ~theme(V_883, skc15, V_1551) | ~proposition(V_883, skc20) | ~proposition(V_883, V_1551) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7760, plain, (![V_1551, V_883]: (skc14=V_1551 | ~agent(V_883, skc15, skc17) | ~think_believe_consider(V_883, skc15) | ~theme(V_883, skc15, V_1551) | ~proposition(V_883, skc14) | ~proposition(V_883, V_1551) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7750, plain, (![V_883]: (~agent(V_883, skc15, skc23) | ~think_believe_consider(V_883, skc15) | ~think_believe_consider(V_883, skc21) | ~proposition(V_883, skc14) | ~proposition(V_883, skc20) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_3278, plain, (![W_184, V_189, V_929, Y_188]: (W_184=V_189 | ~agent(V_929, Y_188, skc17) | ~theme(V_929, Y_188, W_184) | ~think_believe_consider(V_929, Y_188) | ~think_believe_consider(V_929, skc15) | ~theme(V_929, skc15, V_189) | ~proposition(V_929, W_184) | ~proposition(V_929, V_189) | ~accessible_world(skc13, V_929)))). % 13.11/4.40 tff(c_7719, plain, (![V_1543, V_883]: (skc14=V_1543 | ~agent(V_883, skc15, skc23) | ~think_believe_consider(V_883, skc15) | ~think_believe_consider(V_883, skc21) | ~theme(V_883, skc21, V_1543) | ~proposition(V_883, skc14) | ~proposition(V_883, V_1543) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_7720, plain, (![V_1543, V_883]: (skc20=V_1543 | ~agent(V_883, skc21, skc23) | ~think_believe_consider(V_883, skc21) | ~theme(V_883, skc21, V_1543) | ~proposition(V_883, skc20) | ~proposition(V_883, V_1543) | ~accessible_world(skc13, V_883)))). % 13.11/4.40 tff(c_3271, plain, (![W_184, V_189, V_928, Y_188]: (W_184=V_189 | ~agent(V_928, Y_188, skc23) | ~theme(V_928, Y_188, W_184) | ~think_believe_consider(V_928, Y_188) | ~think_believe_consider(V_928, skc21) | ~theme(V_928, skc21, V_189) | ~proposition(V_928, W_184) | ~proposition(V_928, V_189) | ~accessible_world(skc13, V_928)))). % 13.11/4.40 tff(c_7583, plain, (![V_143, V_1514]: (human(V_143, skc23) | ~accessible_world(V_1514, V_143) | ~accessible_world(skc20, V_1514)))). % 13.11/4.40 tff(c_7558, plain, (![V_146, V_1513]: (animate(V_146, skc23) | ~accessible_world(V_1513, V_146) | ~accessible_world(skc20, V_1513)))). % 13.11/4.40 tff(c_7300, plain, (![V_143, V_1506]: (human(V_143, skc17) | ~accessible_world(V_1506, V_143) | ~accessible_world(skc20, V_1506)))). % 13.11/4.40 tff(c_7305, plain, (![V_146, V_1507]: (animate(V_146, skc17) | ~accessible_world(V_1507, V_146) | ~accessible_world(skc20, V_1507)))). % 13.11/4.40 tff(c_7272, plain, (![V_125, V_1505]: (human_person(V_125, skc17) | ~accessible_world(V_1505, V_125) | ~accessible_world(skc20, V_1505)))). % 13.11/4.40 tff(c_7236, plain, (![V_149, V_1504]: (male(V_149, skc17) | ~accessible_world(V_1504, V_149) | ~accessible_world(skc20, V_1504)))). % 13.11/4.40 tff(c_7516, plain, (![V_149, V_1511]: (male(V_149, skc23) | ~accessible_world(V_1511, V_149) | ~accessible_world(skc20, V_1511)))). % 13.11/4.40 tff(c_7551, plain, (![V_125, V_1512]: (human_person(V_125, skc23) | ~accessible_world(V_1512, V_125) | ~accessible_world(skc20, V_1512)))). % 13.11/4.40 tff(c_7178, plain, (![V_101, V_1502]: (think_believe_consider(V_101, skc15) | ~accessible_world(V_1502, V_101) | ~accessible_world(skc20, V_1502)))). % 13.11/4.40 tff(c_7470, plain, (![V_101, V_1510]: (think_believe_consider(V_101, skc21) | ~accessible_world(V_1510, V_101) | ~accessible_world(skc20, V_1510)))). % 13.11/4.40 tff(c_7188, plain, (![V_122, V_1503]: (man(V_122, skc17) | ~accessible_world(V_1503, V_122) | ~accessible_world(skc20, V_1503)))). % 13.11/4.40 tff(c_7451, plain, (![V_122, V_1509]: (man(V_122, skc23) | ~accessible_world(V_1509, V_122) | ~accessible_world(skc20, V_1509)))). % 13.11/4.40 tff(c_7331, plain, (![U_3]: (~accessible_world(skc20, U_3) | ~event(U_3, skc17)))). % 13.11/4.40 tff(c_7611, plain, (![U_3]: (~accessible_world(skc20, U_3) | ~event(U_3, skc23)))). % 13.11/4.40 tff(c_7517, plain, (![V_1511]: (~eventuality(V_1511, skc23) | ~accessible_world(skc20, V_1511)))). % 13.11/4.40 tff(c_7585, plain, (~think_believe_consider(skc20, skf1(skc23)))). % 13.11/4.41 tff(c_7437, plain, (![V_143]: (human(V_143, skc23) | ~accessible_world(skc20, V_143)))). % 13.11/4.41 tff(c_7441, plain, (![V_146]: (animate(V_146, skc23) | ~accessible_world(skc20, V_146)))). % 13.11/4.41 tff(c_7399, plain, (![V_125]: (human_person(V_125, skc23) | ~accessible_world(skc20, V_125)))). % 13.11/4.41 tff(c_7385, plain, (![V_149]: (male(V_149, skc23) | ~accessible_world(skc20, V_149)))). % 13.11/4.41 tff(c_7466, plain, (![V_101]: (think_believe_consider(V_101, skc21) | ~accessible_world(skc20, V_101)))). % 13.11/4.41 tff(c_7463, plain, (think_believe_consider(skc20, skc21))). % 13.11/4.41 tff(c_7350, plain, (![V_122]: (man(V_122, skc23) | ~accessible_world(skc20, V_122)))). % 13.11/4.41 tff(c_7419, plain, (~event(skc20, skc23))). % 13.11/4.41 tff(c_7403, plain, (animate(skc20, skc23))). % 13.11/4.41 tff(c_7402, plain, (human(skc20, skc23))). % 13.11/4.41 tff(c_7386, plain, (~eventuality(skc20, skc23))). % 13.11/4.41 tff(c_7352, plain, (human_person(skc20, skc23))). % 13.11/4.41 tff(c_7351, plain, (male(skc20, skc23))). % 13.11/4.41 tff(c_7341, plain, (man(skc20, skc23))). % 13.11/4.41 tff(c_7237, plain, (![V_1504]: (~eventuality(V_1504, skc17) | ~accessible_world(skc20, V_1504)))). % 13.11/4.41 tff(c_7174, plain, (![V_146]: (animate(V_146, skc17) | ~accessible_world(skc20, V_146)))). % 13.11/4.41 tff(c_7274, plain, (![V_1505]: (human(V_1505, skc17) | ~accessible_world(skc20, V_1505)))). % 13.11/4.41 tff(c_7119, plain, (![V_125]: (human_person(V_125, skc17) | ~accessible_world(skc20, V_125)))). % 13.11/4.41 tff(c_7239, plain, (~think_believe_consider(skc20, skf1(skc17)))). % 13.11/4.41 tff(c_7105, plain, (![V_149]: (male(V_149, skc17) | ~accessible_world(skc20, V_149)))). % 13.11/4.41 tff(c_7070, plain, (![V_122]: (man(V_122, skc17) | ~accessible_world(skc20, V_122)))). % 13.11/4.41 tff(c_7136, plain, (![V_101]: (think_believe_consider(V_101, skc15) | ~accessible_world(skc20, V_101)))). % 13.11/4.41 tff(c_7152, plain, (~event(skc20, skc17))). % 13.11/4.41 tff(c_7123, plain, (animate(skc20, skc17))). % 13.11/4.41 tff(c_7122, plain, (human(skc20, skc17))). % 13.11/4.41 tff(c_7106, plain, (~eventuality(skc20, skc17))). % 13.11/4.41 tff(c_7133, plain, (think_believe_consider(skc20, skc15))). % 13.11/4.41 tff(c_7072, plain, (human_person(skc20, skc17))). % 13.11/4.41 tff(c_7071, plain, (male(skc20, skc17))). % 13.11/4.41 tff(c_7061, plain, (man(skc20, skc17))). % 13.11/4.41 tff(c_5148, plain, (![W_1137, V_1138, U_196]: (W_1137=V_1138 | ~theme(skc20, skf1(U_196), W_1137) | ~think_believe_consider(skc20, skf1(U_196)) | ~theme(skc20, skf1(U_196), V_1138) | ~proposition(skc20, W_1137) | ~proposition(skc20, V_1138) | ~man(skc20, U_196)))). % 13.11/4.41 tff(c_6151, plain, (![V_86, V_1290, V_1289]: (singleton(V_86, V_1290) | ~accessible_world(V_1289, V_86) | ~accessible_world(skc14, V_1289) | ~abstraction(skc13, V_1290)))). % 13.11/4.41 tff(c_6139, plain, (![V_140, V_1284, V_1283]: (living(V_140, V_1284) | ~accessible_world(V_1283, V_140) | ~accessible_world(skc20, V_1283) | ~human_person(skc13, V_1284)))). % 13.11/4.41 tff(c_6143, plain, (![V_140, V_1286, V_1285]: (living(V_140, V_1286) | ~accessible_world(V_1285, V_140) | ~accessible_world(skc14, V_1285) | ~human_person(skc13, V_1286)))). % 13.11/4.41 tff(c_5969, plain, (![V_137, V_1262, V_1261]: (impartial(V_137, V_1262) | ~accessible_world(V_1261, V_137) | ~accessible_world(skc20, V_1261) | ~human_person(skc13, V_1262)))). % 13.11/4.41 tff(c_5734, plain, (![V_86, V_1235, V_1234]: (singleton(V_86, V_1235) | ~accessible_world(V_1234, V_86) | ~accessible_world(skc20, V_1234) | ~abstraction(skc13, V_1235)))). % 13.11/4.41 tff(c_5729, plain, (![V_107, V_1233, V_1232]: (relation(V_107, V_1233) | ~accessible_world(V_1232, V_107) | ~accessible_world(skc20, V_1232) | ~forename(skc13, V_1233)))). % 13.11/4.41 tff(c_6350, plain, (![V_86, V_1316, V_1315]: (singleton(V_86, V_1316) | ~accessible_world(V_1315, V_86) | ~accessible_world(skc14, V_1315) | ~entity(skc13, V_1316)))). % 13.11/4.41 tff(c_6221, plain, (![V_86, V_1302, V_1301]: (singleton(V_86, V_1302) | ~accessible_world(V_1301, V_86) | ~accessible_world(skc20, V_1301) | ~eventuality(skc13, V_1302)))). % 13.11/4.41 tff(c_6217, plain, (![V_137, V_1300, V_1299]: (impartial(V_137, V_1300) | ~accessible_world(V_1299, V_137) | ~accessible_world(skc14, V_1299) | ~human_person(skc13, V_1300)))). % 13.11/4.41 tff(c_6147, plain, (![V_86, V_1288, V_1287]: (singleton(V_86, V_1288) | ~accessible_world(V_1287, V_86) | ~accessible_world(skc14, V_1287) | ~eventuality(skc13, V_1288)))). % 13.11/4.41 tff(c_6048, plain, (![V_107, V_1272, V_1271]: (relation(V_107, V_1272) | ~accessible_world(V_1271, V_107) | ~accessible_world(skc14, V_1271) | ~forename(skc13, V_1272)))). % 13.11/4.41 tff(c_6960, plain, (![W_182, V_930]: (skc22=W_182 | ~entity(V_930, skc23) | ~forename(V_930, W_182) | ~of(V_930, W_182, skc23) | ~forename(V_930, skc22) | ~accessible_world(skc13, V_930)))). % 13.11/4.41 tff(c_6354, plain, (![V_86, V_1318, V_1317]: (singleton(V_86, V_1318) | ~accessible_world(V_1317, V_86) | ~accessible_world(skc20, V_1317) | ~entity(skc13, V_1318)))). % 13.11/4.41 tff(c_5377, plain, (![V_80, V_1162, V_1161]: (eventuality(V_80, V_1162) | ~accessible_world(V_1161, V_80) | ~accessible_world(skc14, V_1161) | ~event(skc13, V_1162)))). % 13.11/4.41 tff(c_5420, plain, (![V_113, V_1172, V_1171]: (nonhuman(V_113, V_1172) | ~accessible_world(V_1171, V_113) | ~accessible_world(skc20, V_1171) | ~abstraction(skc13, V_1172)))). % 13.11/4.41 tff(c_5478, plain, (![V_155, V_1184, V_1183]: (relname(V_155, V_1184) | ~accessible_world(V_1183, V_155) | ~accessible_world(skc14, V_1183) | ~forename(skc13, V_1184)))). % 13.11/4.41 tff(c_5684, plain, (![V_134, V_1225, V_1224]: (existent(V_134, V_1225) | ~accessible_world(V_1224, V_134) | ~accessible_world(skc14, V_1224) | ~entity(skc13, V_1225)))). % 13.11/4.41 tff(c_5602, plain, (![V_128, V_1206, V_1205]: (organism(V_128, V_1206) | ~accessible_world(V_1205, V_128) | ~accessible_world(skc20, V_1205) | ~human_person(skc13, V_1206)))). % 13.11/4.41 tff(c_5155, plain, (![V_92, V_1142, V_1141]: (nonexistent(V_92, V_1142) | ~accessible_world(V_1141, V_92) | ~accessible_world(skc20, V_1141) | ~eventuality(skc13, V_1142)))). % 13.11/4.41 tff(c_5634, plain, (![V_95, V_1214, V_1213]: (unisex(V_95, V_1214) | ~accessible_world(V_1213, V_95) | ~accessible_world(skc14, V_1213) | ~eventuality(skc13, V_1214)))). % 13.11/4.41 tff(c_5454, plain, (![V_89, V_1178, V_1177]: (specific(V_89, V_1178) | ~accessible_world(V_1177, V_89) | ~accessible_world(skc20, V_1177) | ~entity(skc13, V_1178)))). % 13.11/4.41 tff(c_3243, plain, (![W_182, V_924]: (skc18=W_182 | ~entity(V_924, skc17) | ~forename(V_924, W_182) | ~of(V_924, W_182, skc17) | ~forename(V_924, skc18) | ~accessible_world(skc13, V_924)))). % 13.11/4.41 tff(c_5531, plain, (![V_128, V_1196, V_1195]: (organism(V_128, V_1196) | ~accessible_world(V_1195, V_128) | ~accessible_world(skc14, V_1195) | ~human_person(skc13, V_1196)))). % 13.11/4.42 tff(c_5666, plain, (![V_83, V_1223, V_1222]: (thing(V_83, V_1223) | ~accessible_world(V_1222, V_83) | ~accessible_world(skc14, V_1222) | ~eventuality(skc13, V_1223)))). % 13.11/4.42 tff(c_5396, plain, (![V_83, V_1166, V_1165]: (thing(V_83, V_1166) | ~accessible_world(V_1165, V_83) | ~accessible_world(skc20, V_1165) | ~entity(skc13, V_1166)))). % 13.11/4.42 tff(c_5229, plain, (![V_80, V_1146, V_1145]: (eventuality(V_80, V_1146) | ~accessible_world(V_1145, V_80) | ~accessible_world(skc20, V_1145) | ~event(skc13, V_1146)))). % 13.11/4.42 tff(c_5612, plain, (![V_107, V_1208, V_1207]: (relation(V_107, V_1208) | ~accessible_world(V_1207, V_107) | ~accessible_world(skc20, V_1207) | ~proposition(skc13, V_1208)))). % 13.11/4.42 tff(c_5388, plain, (![V_107, V_1164, V_1163]: (relation(V_107, V_1164) | ~accessible_world(V_1163, V_107) | ~accessible_world(skc14, V_1163) | ~proposition(skc13, V_1164)))). % 13.11/4.42 tff(c_5494, plain, (![V_83, V_1188, V_1187]: (thing(V_83, V_1188) | ~accessible_world(V_1187, V_83) | ~accessible_world(skc20, V_1187) | ~abstraction(skc13, V_1188)))). % 13.11/4.42 tff(c_5303, plain, (![V_83, V_1158, V_1157]: (thing(V_83, V_1158) | ~accessible_world(V_1157, V_83) | ~accessible_world(skc14, V_1157) | ~entity(skc13, V_1158)))). % 13.11/4.42 tff(c_5658, plain, (![V_89, V_1221, V_1220]: (specific(V_89, V_1221) | ~accessible_world(V_1220, V_89) | ~accessible_world(skc14, V_1220) | ~entity(skc13, V_1221)))). % 13.11/4.42 tff(c_4764, plain, (![V_164, U_1076, V_1075]: (agent(V_164, skf1(U_1076), U_1076) | ~accessible_world(V_1075, V_164) | ~accessible_world(skc20, V_1075) | ~man(skc20, U_1076)))). % 13.11/4.42 tff(c_5263, plain, (![V_95, V_1154, V_1153]: (unisex(V_95, V_1154) | ~accessible_world(V_1153, V_95) | ~accessible_world(skc14, V_1153) | ~abstraction(skc13, V_1154)))). % 13.11/4.42 tff(c_5486, plain, (![V_83, V_1186, V_1185]: (thing(V_83, V_1186) | ~accessible_world(V_1185, V_83) | ~accessible_world(skc20, V_1185) | ~eventuality(skc13, V_1186)))). % 13.11/4.42 tff(c_5412, plain, (![V_95, V_1170, V_1169]: (unisex(V_95, V_1170) | ~accessible_world(V_1169, V_95) | ~accessible_world(skc20, V_1169) | ~eventuality(skc13, V_1170)))). % 13.11/4.42 tff(c_5248, plain, (![V_95, V_1150, V_1149]: (unisex(V_95, V_1150) | ~accessible_world(V_1149, V_95) | ~accessible_world(skc20, V_1149) | ~abstraction(skc13, V_1150)))). % 13.11/4.42 tff(c_5404, plain, (![V_113, V_1168, V_1167]: (nonhuman(V_113, V_1168) | ~accessible_world(V_1167, V_113) | ~accessible_world(skc14, V_1167) | ~abstraction(skc13, V_1168)))). % 13.11/4.42 tff(c_5588, plain, (![V_89, V_1204, V_1203]: (specific(V_89, V_1204) | ~accessible_world(V_1203, V_89) | ~accessible_world(skc14, V_1203) | ~eventuality(skc13, V_1204)))). % 13.11/4.42 tff(c_5572, plain, (![V_116, V_1200, V_1199]: (general(V_116, V_1200) | ~accessible_world(V_1199, V_116) | ~accessible_world(skc14, V_1199) | ~abstraction(skc13, V_1200)))). % 13.11/4.42 tff(c_5517, plain, (![V_89, V_1194, V_1193]: (specific(V_89, V_1194) | ~accessible_world(V_1193, V_89) | ~accessible_world(skc20, V_1193) | ~eventuality(skc13, V_1194)))). % 13.11/4.42 tff(c_6758, plain, (~agent(skc13, skc15, skc23))). % 13.11/4.42 tff(c_5240, plain, (![V_83, V_1148, V_1147]: (thing(V_83, V_1148) | ~accessible_world(V_1147, V_83) | ~accessible_world(skc14, V_1147) | ~abstraction(skc13, V_1148)))). % 13.11/4.42 tff(c_5502, plain, (![V_92, V_1190, V_1189]: (nonexistent(V_92, V_1190) | ~accessible_world(V_1189, V_92) | ~accessible_world(skc14, V_1189) | ~eventuality(skc13, V_1190)))). % 13.11/4.42 tff(c_5294, plain, (![V_116, V_1156, V_1155]: (general(V_116, V_1156) | ~accessible_world(V_1155, V_116) | ~accessible_world(skc20, V_1155) | ~abstraction(skc13, V_1156)))). % 13.11/4.42 tff(c_5650, plain, (![V_155, V_1219, V_1218]: (relname(V_155, V_1219) | ~accessible_world(V_1218, V_155) | ~accessible_world(skc20, V_1218) | ~forename(skc13, V_1219)))). % 13.11/4.42 tff(c_5438, plain, (![V_134, V_1174, V_1173]: (existent(V_134, V_1174) | ~accessible_world(V_1173, V_134) | ~accessible_world(skc20, V_1173) | ~entity(skc13, V_1174)))). % 13.11/4.42 tff(c_4288, plain, (![V_131, V_1026]: (entity(V_131, skc17) | ~accessible_world(V_1026, V_131) | ~accessible_world(skc14, V_1026)))). % 13.11/4.42 tff(c_4179, plain, (![V_131, V_1017]: (entity(V_131, skc23) | ~accessible_world(V_1017, V_131) | ~accessible_world(skc20, V_1017)))). % 13.11/4.42 tff(c_4306, plain, (![V_131, V_1027]: (entity(V_131, skc17) | ~accessible_world(V_1027, V_131) | ~accessible_world(skc20, V_1027)))). % 13.11/4.42 tff(c_6695, plain, (~agent(skc13, skc21, skc17))). % 13.11/4.42 tff(c_3723, plain, (![V_131, V_979]: (entity(V_131, skc23) | ~accessible_world(V_979, V_131) | ~accessible_world(skc14, V_979)))). % 13.11/4.42 tff(c_6683, plain, (![U_1355]: (~accessible_world(skc20, U_1355) | ~entity(U_1355, skc16)))). % 13.11/4.42 tff(c_5762, plain, (![U_41, V_42]: (~accessible_world(skc20, U_41) | ~eventuality(skc13, V_42) | ~entity(U_41, V_42)))). % 13.11/4.42 tff(c_6049, plain, (![V_1271, V_1272]: (abstraction(V_1271, V_1272) | ~accessible_world(skc14, V_1271) | ~forename(skc13, V_1272)))). % 13.11/4.42 tff(c_5919, plain, (![U_3, V_4]: (~accessible_world(skc20, U_3) | ~abstraction(skc13, V_4) | ~event(U_3, V_4)))). % 13.11/4.42 tff(c_5948, plain, (![U_3, V_4]: (~accessible_world(skc14, U_3) | ~entity(skc13, V_4) | ~event(U_3, V_4)))). % 13.11/4.42 tff(c_5713, plain, (![U_23, V_24]: (~accessible_world(skc14, U_23) | ~entity(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.11/4.42 tff(c_6213, plain, (![U_23, V_24]: (~accessible_world(skc20, U_23) | ~entity(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.11/4.42 tff(c_6291, plain, (![U_23, V_24]: (~accessible_world(skc20, U_23) | ~eventuality(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.11/4.42 tff(c_3294, plain, (![V_179, V_933]: (be(V_179, skc16, skc17, skc17) | ~accessible_world(V_933, V_179) | ~accessible_world(skc13, V_933)))). % 13.11/4.42 tff(c_5730, plain, (![V_1232, V_1233]: (abstraction(V_1232, V_1233) | ~accessible_world(skc20, V_1232) | ~forename(skc13, V_1233)))). % 13.11/4.42 tff(c_6034, plain, (![U_23, V_24]: (~accessible_world(skc14, U_23) | ~eventuality(skc13, V_24) | ~abstraction(U_23, V_24)))). % 13.11/4.42 tff(c_5882, plain, (![U_3, V_4]: (~accessible_world(skc14, U_3) | ~abstraction(skc13, V_4) | ~event(U_3, V_4)))). % 13.11/4.42 tff(c_6526, plain, (![U_1332]: (~accessible_world(skc14, U_1332) | ~entity(U_1332, skc16)))). % 13.11/4.42 tff(c_6466, plain, (![U_41, V_42]: (~accessible_world(skc14, U_41) | ~eventuality(skc13, V_42) | ~entity(U_41, V_42)))). % 13.11/4.42 tff(c_6383, plain, (![U_3, V_4]: (~accessible_world(skc20, U_3) | ~entity(skc13, V_4) | ~event(U_3, V_4)))). % 13.11/4.42 tff(c_5503, plain, (![V_1189, V_1190]: (~existent(V_1189, V_1190) | ~accessible_world(skc14, V_1189) | ~eventuality(skc13, V_1190)))). % 13.11/4.42 tff(c_5231, plain, (![V_1145, V_1146]: (~abstraction(V_1145, V_1146) | ~accessible_world(skc20, V_1145) | ~event(skc13, V_1146)))). % 13.11/4.42 tff(c_3216, plain, (![V_74, V_918, V_917]: (smoke(V_74, skf1(V_918)) | ~accessible_world(V_917, V_74) | ~accessible_world(skc20, V_917)))). % 13.11/4.42 tff(c_5413, plain, (![V_1169, V_1170]: (~male(V_1169, V_1170) | ~accessible_world(skc20, V_1169) | ~eventuality(skc13, V_1170)))). % 13.11/4.42 tff(c_5439, plain, (![V_1173, V_1174]: (~eventuality(V_1173, V_1174) | ~accessible_world(skc20, V_1173) | ~entity(skc13, V_1174)))). % 13.11/4.42 tff(c_4606, plain, (![V_86, V_1054]: (singleton(V_86, V_1054) | ~accessible_world(skc20, V_86) | ~entity(skc13, V_1054)))). % 13.11/4.42 tff(c_4610, plain, (![V_86, V_1055]: (singleton(V_86, V_1055) | ~accessible_world(skc14, V_86) | ~entity(skc13, V_1055)))). % 13.11/4.42 tff(c_5249, plain, (![V_1149, V_1150]: (~male(V_1149, V_1150) | ~accessible_world(skc20, V_1149) | ~abstraction(skc13, V_1150)))). % 13.11/4.42 tff(c_5230, plain, (![V_1145, V_1146]: (~entity(V_1145, V_1146) | ~accessible_world(skc20, V_1145) | ~event(skc13, V_1146)))). % 13.11/4.42 tff(c_5518, plain, (![V_1193, V_1194]: (~general(V_1193, V_1194) | ~accessible_world(skc20, V_1193) | ~eventuality(skc13, V_1194)))). % 13.11/4.42 tff(c_6263, plain, (~event(skc13, skc14))). % 13.11/4.42 tff(c_3279, plain, (![V_164, V_929]: (agent(V_164, skc15, skc17) | ~accessible_world(V_929, V_164) | ~accessible_world(skc13, V_929)))). % 13.11/4.42 tff(c_6262, plain, (~event(skc13, skc20))). % 13.11/4.42 tff(c_6261, plain, (~event(skc13, skc22))). % 13.11/4.42 tff(c_5389, plain, (![V_1163, V_1164]: (abstraction(V_1163, V_1164) | ~accessible_world(skc14, V_1163) | ~proposition(skc13, V_1164)))). % 13.11/4.42 tff(c_6259, plain, (~event(skc13, skc18))). % 13.11/4.42 tff(c_5379, plain, (![V_1161, V_1162]: (~abstraction(V_1161, V_1162) | ~accessible_world(skc14, V_1161) | ~event(skc13, V_1162)))). % 13.11/4.42 tff(c_4158, plain, (![V_86, V_1015]: (singleton(V_86, V_1015) | ~accessible_world(skc20, V_86) | ~eventuality(skc13, V_1015)))). % 13.11/4.42 tff(c_5533, plain, (![V_1195, V_1196]: (impartial(V_1195, V_1196) | ~accessible_world(skc14, V_1195) | ~human_person(skc13, V_1196)))). % 13.11/4.42 tff(c_5455, plain, (![V_1177, V_1178]: (~general(V_1177, V_1178) | ~accessible_world(skc20, V_1177) | ~entity(skc13, V_1178)))). % 13.11/4.42 tff(c_5635, plain, (![V_1213, V_1214]: (~male(V_1213, V_1214) | ~accessible_world(skc14, V_1213) | ~eventuality(skc13, V_1214)))). % 13.11/4.43 tff(c_5421, plain, (![V_1171, V_1172]: (~human(V_1171, V_1172) | ~accessible_world(skc20, V_1171) | ~abstraction(skc13, V_1172)))). % 13.11/4.43 tff(c_3221, plain, (![V_168, V_919]: (theme(V_168, skc15, skc14) | ~accessible_world(V_919, V_168) | ~accessible_world(skc13, V_919)))). % 13.11/4.43 tff(c_5241, plain, (![V_1147, V_1148]: (singleton(V_1147, V_1148) | ~accessible_world(skc14, V_1147) | ~abstraction(skc13, V_1148)))). % 13.11/4.43 tff(c_5667, plain, (![V_1222, V_1223]: (singleton(V_1222, V_1223) | ~accessible_world(skc14, V_1222) | ~eventuality(skc13, V_1223)))). % 13.11/4.43 tff(c_5534, plain, (![V_1195, V_1196]: (living(V_1195, V_1196) | ~accessible_world(skc14, V_1195) | ~human_person(skc13, V_1196)))). % 13.11/4.43 tff(c_3427, plain, (![V_140, V_950]: (living(V_140, V_950) | ~accessible_world(skc20, V_140) | ~human_person(skc13, V_950)))). % 13.11/4.43 tff(c_2929, plain, (![V_146, V_833]: (animate(V_146, skc17) | ~accessible_world(V_833, V_146) | ~accessible_world(skc13, V_833)))). % 13.11/4.43 tff(c_2952, plain, (![V_836, V_791]: (human(V_836, skc23) | ~accessible_world(V_791, V_836) | ~accessible_world(skc13, V_791)))). % 13.11/4.43 tff(c_5603, plain, (![V_1205, V_1206]: (entity(V_1205, V_1206) | ~accessible_world(skc20, V_1205) | ~human_person(skc13, V_1206)))). % 13.11/4.43 tff(c_5295, plain, (![V_1155, V_1156]: (~entity(V_1155, V_1156) | ~accessible_world(skc20, V_1155) | ~abstraction(skc13, V_1156)))). % 13.11/4.43 tff(c_6050, plain, (![V_172, V_926]: (of(V_172, skc18, skc17) | ~accessible_world(V_926, V_172) | ~accessible_world(skc13, V_926)))). % 13.11/4.43 tff(c_5479, plain, (![V_1183, V_1184]: (relation(V_1183, V_1184) | ~accessible_world(skc14, V_1183) | ~forename(skc13, V_1184)))). % 13.11/4.43 tff(c_2976, plain, (![V_143, V_843]: (human(V_143, skc17) | ~accessible_world(V_843, V_143) | ~accessible_world(skc13, V_843)))). % 13.11/4.43 tff(c_5589, plain, (![V_1203, V_1204]: (~general(V_1203, V_1204) | ~accessible_world(skc14, V_1203) | ~eventuality(skc13, V_1204)))). % 13.11/4.43 tff(c_2762, plain, (![V_146, V_802]: (animate(V_146, skc23) | ~accessible_world(V_802, V_146) | ~accessible_world(skc13, V_802)))). % 13.11/4.43 tff(c_5378, plain, (![V_1161, V_1162]: (~entity(V_1161, V_1162) | ~accessible_world(skc14, V_1161) | ~event(skc13, V_1162)))). % 13.11/4.43 tff(c_5604, plain, (![V_1205, V_1206]: (impartial(V_1205, V_1206) | ~accessible_world(skc20, V_1205) | ~human_person(skc13, V_1206)))). % 13.11/4.43 tff(c_5264, plain, (![V_1153, V_1154]: (~male(V_1153, V_1154) | ~accessible_world(skc14, V_1153) | ~abstraction(skc13, V_1154)))). % 13.11/4.43 tff(c_5685, plain, (![V_1224, V_1225]: (~eventuality(V_1224, V_1225) | ~accessible_world(skc14, V_1224) | ~entity(skc13, V_1225)))). % 13.11/4.43 tff(c_5296, plain, (![V_1155, V_1156]: (~eventuality(V_1155, V_1156) | ~accessible_world(skc20, V_1155) | ~abstraction(skc13, V_1156)))). % 13.11/4.43 tff(c_3237, plain, (![V_98, V_923, V_922]: (present(V_98, skf1(V_923)) | ~accessible_world(V_922, V_98) | ~accessible_world(skc20, V_922)))). % 13.11/4.43 tff(c_5574, plain, (![V_1199, V_1200]: (~eventuality(V_1199, V_1200) | ~accessible_world(skc14, V_1199) | ~abstraction(skc13, V_1200)))). % 13.11/4.43 tff(c_5573, plain, (![V_1199, V_1200]: (~entity(V_1199, V_1200) | ~accessible_world(skc14, V_1199) | ~abstraction(skc13, V_1200)))). % 13.11/4.43 tff(c_5532, plain, (![V_1195, V_1196]: (entity(V_1195, V_1196) | ~accessible_world(skc14, V_1195) | ~human_person(skc13, V_1196)))). % 13.11/4.43 tff(c_2961, plain, (![V_131, V_839]: (entity(V_131, skc23) | ~accessible_world(V_839, V_131) | ~accessible_world(skc13, V_839)))). % 13.11/4.43 tff(c_5613, plain, (![V_1207, V_1208]: (abstraction(V_1207, V_1208) | ~accessible_world(skc20, V_1207) | ~proposition(skc13, V_1208)))). % 13.11/4.43 tff(c_5405, plain, (![V_1167, V_1168]: (~human(V_1167, V_1168) | ~accessible_world(skc14, V_1167) | ~abstraction(skc13, V_1168)))). % 13.11/4.43 tff(c_5156, plain, (![V_1141, V_1142]: (~existent(V_1141, V_1142) | ~accessible_world(skc20, V_1141) | ~eventuality(skc13, V_1142)))). % 13.11/4.43 tff(c_3272, plain, (![V_164, V_928]: (agent(V_164, skc21, skc23) | ~accessible_world(V_928, V_164) | ~accessible_world(skc13, V_928)))). % 13.11/4.43 tff(c_5495, plain, (![V_1187, V_1188]: (singleton(V_1187, V_1188) | ~accessible_world(skc20, V_1187) | ~abstraction(skc13, V_1188)))). % 13.11/4.43 tff(c_5651, plain, (![V_1218, V_1219]: (relation(V_1218, V_1219) | ~accessible_world(skc20, V_1218) | ~forename(skc13, V_1219)))). % 13.11/4.43 tff(c_2861, plain, (![V_131, V_820]: (entity(V_131, skc17) | ~accessible_world(V_820, V_131) | ~accessible_world(skc13, V_820)))). % 13.11/4.43 tff(c_5659, plain, (![V_1220, V_1221]: (~general(V_1220, V_1221) | ~accessible_world(skc14, V_1220) | ~entity(skc13, V_1221)))). % 13.11/4.43 tff(c_3046, plain, (![V_857, V_811]: (event(V_857, skc16) | ~accessible_world(V_811, V_857) | ~accessible_world(skc13, V_811)))). % 13.11/4.43 tff(c_3754, plain, (![V_134, V_984]: (existent(V_134, V_984) | ~accessible_world(skc14, V_134) | ~entity(skc13, V_984)))). % 13.11/4.43 tff(c_4153, plain, (![V_83, V_1014]: (thing(V_83, V_1014) | ~accessible_world(skc14, V_83) | ~eventuality(skc13, V_1014)))). % 13.11/4.43 tff(c_4330, plain, (![V_89, V_1033]: (specific(V_89, V_1033) | ~accessible_world(skc14, V_89) | ~entity(skc13, V_1033)))). % 13.11/4.43 tff(c_3445, plain, (![V_155, V_955]: (relname(V_155, V_955) | ~accessible_world(skc20, V_155) | ~forename(skc13, V_955)))). % 13.11/4.43 tff(c_3231, plain, (![V_77, V_921, V_920]: (event(V_77, skf1(V_921)) | ~accessible_world(V_920, V_77) | ~accessible_world(skc20, V_920)))). % 13.11/4.43 tff(c_4027, plain, (![V_95, V_1004]: (unisex(V_95, V_1004) | ~accessible_world(skc14, V_95) | ~eventuality(skc13, V_1004)))). % 13.11/4.43 tff(c_2710, plain, (![V_125, V_791]: (human_person(V_125, skc23) | ~accessible_world(V_791, V_125) | ~accessible_world(skc13, V_791)))). % 13.11/4.43 tff(c_2891, plain, (![V_825, V_783]: (male(V_825, skc17) | ~accessible_world(V_783, V_825) | ~accessible_world(skc13, V_783)))). % 13.11/4.43 tff(c_3383, plain, (![V_107, V_945]: (relation(V_107, V_945) | ~accessible_world(skc20, V_107) | ~proposition(skc13, V_945)))). % 13.11/4.43 tff(c_3317, plain, (![V_128, V_939]: (organism(V_128, V_939) | ~accessible_world(skc20, V_128) | ~human_person(skc13, V_939)))). % 13.11/4.43 tff(c_4451, plain, (![V_89, V_1042]: (specific(V_89, V_1042) | ~accessible_world(skc14, V_89) | ~eventuality(skc13, V_1042)))). % 13.11/4.43 tff(c_2892, plain, (![V_825, V_784]: (male(V_825, skc23) | ~accessible_world(V_784, V_825) | ~accessible_world(skc13, V_784)))). % 13.11/4.43 tff(c_3883, plain, (![V_116, V_994]: (general(V_116, V_994) | ~accessible_world(skc14, V_116) | ~abstraction(skc13, V_994)))). % 13.11/4.43 tff(c_3251, plain, (![V_172, V_925]: (of(V_172, skc22, skc23) | ~accessible_world(V_925, V_172) | ~accessible_world(skc13, V_925)))). % 13.36/4.43 tff(c_3333, plain, (![V_128, V_940]: (organism(V_128, V_940) | ~accessible_world(skc14, V_128) | ~human_person(skc13, V_940)))). % 13.36/4.43 tff(c_4443, plain, (![V_89, V_1041]: (specific(V_89, V_1041) | ~accessible_world(skc20, V_89) | ~eventuality(skc13, V_1041)))). % 13.36/4.43 tff(c_3005, plain, (![V_845, V_816]: (forename(V_845, skc18) | ~accessible_world(V_816, V_845) | ~accessible_world(skc13, V_816)))). % 13.36/4.43 tff(c_3549, plain, (![V_92, V_965]: (nonexistent(V_92, V_965) | ~accessible_world(skc14, V_92) | ~eventuality(skc13, V_965)))). % 13.36/4.43 tff(c_3682, plain, (![V_83, V_974]: (thing(V_83, V_974) | ~accessible_world(skc20, V_83) | ~abstraction(skc13, V_974)))). % 13.36/4.43 tff(c_4145, plain, (![V_83, V_1013]: (thing(V_83, V_1013) | ~accessible_world(skc20, V_83) | ~eventuality(skc13, V_1013)))). % 13.36/4.43 tff(c_3453, plain, (![V_155, V_956]: (relname(V_155, V_956) | ~accessible_world(skc14, V_155) | ~forename(skc13, V_956)))). % 13.36/4.43 tff(c_2672, plain, (![V_125, V_785]: (human_person(V_125, skc17) | ~accessible_world(V_785, V_125) | ~accessible_world(skc13, V_785)))). % 13.36/4.43 tff(c_3265, plain, (![V_164, V_927]: (agent(V_164, skc24, skc23) | ~accessible_world(V_927, V_164) | ~accessible_world(skc14, V_927)))). % 13.36/4.43 tff(c_4322, plain, (![V_89, V_1032]: (specific(V_89, V_1032) | ~accessible_world(skc20, V_89) | ~entity(skc13, V_1032)))). % 13.36/4.43 tff(c_3047, plain, (![V_857, V_756]: (event(V_857, skc24) | ~accessible_world(V_756, V_857) | ~accessible_world(skc14, V_756)))). % 13.36/4.43 tff(c_3742, plain, (![V_134, V_983]: (existent(V_134, V_983) | ~accessible_world(skc20, V_134) | ~entity(skc13, V_983)))). % 13.36/4.43 tff(c_4232, plain, (![V_113, V_1022]: (nonhuman(V_113, V_1022) | ~accessible_world(skc20, V_113) | ~abstraction(skc13, V_1022)))). % 13.36/4.43 tff(c_4019, plain, (![V_95, V_1003]: (unisex(V_95, V_1003) | ~accessible_world(skc20, V_95) | ~eventuality(skc13, V_1003)))). % 13.36/4.43 tff(c_4240, plain, (![V_113, V_1023]: (nonhuman(V_113, V_1023) | ~accessible_world(skc14, V_113) | ~abstraction(skc13, V_1023)))). % 13.36/4.43 tff(c_4593, plain, (![V_83, V_1052]: (thing(V_83, V_1052) | ~accessible_world(skc20, V_83) | ~entity(skc13, V_1052)))). % 13.36/4.43 tff(c_3391, plain, (![V_107, V_946]: (relation(V_107, V_946) | ~accessible_world(skc14, V_107) | ~proposition(skc13, V_946)))). % 13.36/4.43 tff(c_4740, plain, (![V_80, V_1070]: (eventuality(V_80, V_1070) | ~accessible_world(skc14, V_80) | ~event(skc13, V_1070)))). % 13.36/4.43 tff(c_3192, plain, (![V_168, V_910]: (theme(V_168, skc21, skc20) | ~accessible_world(V_910, V_168) | ~accessible_world(skc13, V_910)))). % 13.36/4.43 tff(c_4601, plain, (![V_83, V_1053]: (thing(V_83, V_1053) | ~accessible_world(skc14, V_83) | ~entity(skc13, V_1053)))). % 13.36/4.43 tff(c_3871, plain, (![V_116, V_993]: (general(V_116, V_993) | ~accessible_world(skc20, V_116) | ~abstraction(skc13, V_993)))). % 13.36/4.43 tff(c_4634, plain, (![V_95, V_1062]: (unisex(V_95, V_1062) | ~accessible_world(skc14, V_95) | ~abstraction(skc13, V_1062)))). % 13.36/4.43 tff(c_2779, plain, (![V_80, V_806]: (eventuality(V_80, skc16) | ~accessible_world(V_806, V_80) | ~accessible_world(skc13, V_806)))). % 13.36/4.43 tff(c_4626, plain, (![V_95, V_1061]: (unisex(V_95, V_1061) | ~accessible_world(skc20, V_95) | ~abstraction(skc13, V_1061)))). % 13.36/4.43 tff(c_3690, plain, (![V_83, V_975]: (thing(V_83, V_975) | ~accessible_world(skc14, V_83) | ~abstraction(skc13, V_975)))). % 13.36/4.43 tff(c_4706, plain, (![V_80, V_1069]: (eventuality(V_80, V_1069) | ~accessible_world(skc20, V_80) | ~event(skc13, V_1069)))). % 13.36/4.43 tff(c_3006, plain, (![V_845, V_732]: (forename(V_845, skc22) | ~accessible_world(V_732, V_845) | ~accessible_world(skc13, V_732)))). % 13.36/4.43 tff(c_3541, plain, (![V_92, V_964]: (nonexistent(V_92, V_964) | ~accessible_world(skc20, V_92) | ~eventuality(skc13, V_964)))). % 13.36/4.43 tff(c_3202, plain, (![W_915, V_913, Y_914, U_196]: (W_915=V_913 | ~agent(skc20, Y_914, U_196) | ~theme(skc20, Y_914, W_915) | ~think_believe_consider(skc20, Y_914) | ~think_believe_consider(skc20, skf1(U_196)) | ~theme(skc20, skf1(U_196), V_913) | ~proposition(skc20, W_915) | ~proposition(skc20, V_913) | ~man(skc20, U_196)))). % 13.36/4.43 tff(c_5116, plain, (![V_158, V_731]: (vincent_forename(V_158, skc18) | ~accessible_world(V_731, V_158) | ~accessible_world(skc13, V_731)))). % 13.36/4.43 tff(c_5108, plain, (![V_161, V_817]: (jules_forename(V_161, skc22) | ~accessible_world(V_817, V_161) | ~accessible_world(skc13, V_817)))). % 13.36/4.43 tff(c_2968, plain, (![V_840, V_230, U_229]: (relation(V_840, V_230) | ~accessible_world(U_229, V_840) | ~forename(U_229, V_230)))). % 13.36/4.43 tff(c_2835, plain, (![V_161, V_816]: (jules_forename(V_161, skc18) | ~accessible_world(V_816, V_161) | ~accessible_world(skc13, V_816)))). % 13.36/4.44 tff(c_5062, plain, (![V_813]: (jules_forename(V_813, skc22) | ~accessible_world(skc13, V_813)))). % 13.36/4.44 tff(c_5084, plain, (~think_believe_consider(skc14, skc24))). % 13.36/4.44 tff(c_5065, plain, (jules_forename(skc13, skc22))). % 13.36/4.44 tff(c_5054, plain, (skc25=skc22)). % 13.36/4.44 tff(c_3178, plain, (![W_902]: (skc22=W_902 | ~forename(skc13, W_902) | ~of(skc13, W_902, skc23)))). % 13.36/4.44 tff(c_4967, plain, (![V_1114]: (skc20=V_1114 | ~theme(skc13, skc21, V_1114) | ~proposition(skc13, V_1114)))). % 13.36/4.44 tff(c_2657, plain, (![V_122, V_784]: (man(V_122, skc23) | ~accessible_world(V_784, V_122) | ~accessible_world(skc13, V_784)))). % 13.36/4.44 tff(c_2590, plain, (![V_104, V_774]: (proposition(V_104, skc14) | ~accessible_world(V_774, V_104) | ~accessible_world(skc13, V_774)))). % 13.36/4.44 tff(c_2409, plain, (![V_98, V_736]: (present(V_98, skc15) | ~accessible_world(V_736, V_98) | ~accessible_world(skc13, V_736)))). % 13.36/4.44 tff(c_2487, plain, (![V_74, V_756]: (smoke(V_74, skc24) | ~accessible_world(V_756, V_74) | ~accessible_world(skc14, V_756)))). % 13.36/4.44 tff(c_4847, plain, (![V_1100]: (skc14=V_1100 | ~theme(skc13, skc15, V_1100) | ~proposition(skc13, V_1100)))). % 13.36/4.44 tff(c_3206, plain, (![W_915, V_913, Y_914]: (W_915=V_913 | ~agent(skc13, Y_914, skc23) | ~theme(skc13, Y_914, W_915) | ~think_believe_consider(skc13, Y_914) | ~theme(skc13, skc21, V_913) | ~proposition(skc13, W_915) | ~proposition(skc13, V_913)))). % 13.36/4.44 tff(c_2507, plain, (![V_759, V_264, U_263]: (singleton(V_759, V_264) | ~accessible_world(U_263, V_759) | ~entity(U_263, V_264)))). % 13.36/4.44 tff(c_2413, plain, (![V_98, V_737]: (present(V_98, skc24) | ~accessible_world(V_737, V_98) | ~accessible_world(skc14, V_737)))). % 13.36/4.44 tff(c_2391, plain, (![V_158, V_732]: (vincent_forename(V_158, skc22) | ~accessible_world(V_732, V_158) | ~accessible_world(skc13, V_732)))). % 13.36/4.44 tff(c_4894, plain, (![V_719]: (vincent_forename(V_719, skc18) | ~accessible_world(skc13, V_719)))). % 13.36/4.44 tff(c_4896, plain, (vincent_forename(skc13, skc18))). % 13.36/4.44 tff(c_4885, plain, (skc19=skc18)). % 13.36/4.44 tff(c_3175, plain, (![W_902]: (skc18=W_902 | ~forename(skc13, W_902) | ~of(skc13, W_902, skc17)))). % 13.36/4.44 tff(c_2417, plain, (![V_98, V_738]: (present(V_98, skc21) | ~accessible_world(V_738, V_98) | ~accessible_world(skc13, V_738)))). % 13.36/4.44 tff(c_3209, plain, (![W_915, V_913, Y_914]: (W_915=V_913 | ~agent(skc13, Y_914, skc17) | ~theme(skc13, Y_914, W_915) | ~think_believe_consider(skc13, Y_914) | ~theme(skc13, skc15, V_913) | ~proposition(skc13, W_915) | ~proposition(skc13, V_913)))). % 13.36/4.44 tff(c_3088, plain, (![V_101, V_866]: (think_believe_consider(V_101, skc15) | ~accessible_world(V_866, V_101) | ~accessible_world(skc13, V_866)))). % 13.36/4.44 tff(c_2506, plain, (![V_759, V_210, U_209]: (singleton(V_759, V_210) | ~accessible_world(U_209, V_759) | ~abstraction(U_209, V_210)))). % 13.36/4.44 tff(c_2582, plain, (![V_104, V_773]: (proposition(V_104, skc20) | ~accessible_world(V_773, V_104) | ~accessible_world(skc13, V_773)))). % 13.36/4.44 tff(c_3092, plain, (![V_101, V_867]: (think_believe_consider(V_101, skc21) | ~accessible_world(V_867, V_101) | ~accessible_world(skc13, V_867)))). % 13.36/4.44 tff(c_2505, plain, (![V_759, V_262, U_261]: (singleton(V_759, V_262) | ~accessible_world(U_261, V_759) | ~eventuality(U_261, V_262)))). % 13.36/4.44 tff(c_2688, plain, (![V_787, V_246, U_245]: (impartial(V_787, V_246) | ~accessible_world(U_245, V_787) | ~human_person(U_245, V_246)))). % 13.36/4.44 tff(c_2810, plain, (![V_119, V_811]: (state(V_119, skc16) | ~accessible_world(V_811, V_119) | ~accessible_world(skc13, V_811)))). % 13.36/4.44 tff(c_3074, plain, (![V_77, V_861]: (event(V_77, skc21) | ~accessible_world(V_861, V_77) | ~accessible_world(skc13, V_861)))). % 13.36/4.44 tff(c_2448, plain, (![V_748, V_246, U_245]: (living(V_748, V_246) | ~accessible_world(U_245, V_748) | ~human_person(U_245, V_246)))). % 13.36/4.44 tff(c_3151, plain, (![V_888, U_196]: (agent(V_888, skf1(U_196), U_196) | ~accessible_world(skc20, V_888) | ~man(skc20, U_196)))). % 13.36/4.44 tff(c_2645, plain, (![V_122, V_783]: (man(V_122, skc17) | ~accessible_world(V_783, V_122) | ~accessible_world(skc13, V_783)))). % 13.36/4.44 tff(c_4750, plain, (~accessible_world(skc13, skc13))). % 13.36/4.44 tff(c_3062, plain, (![V_77, V_860]: (event(V_77, skc15) | ~accessible_world(V_860, V_77) | ~accessible_world(skc13, V_860)))). % 13.36/4.44 tff(c_4674, plain, (![V_1067]: (eventuality(skc14, V_1067) | ~event(skc13, V_1067)))). % 13.36/4.44 tff(c_4673, plain, (![V_1067]: (eventuality(skc20, V_1067) | ~event(skc13, V_1067)))). % 13.36/4.44 tff(c_4667, plain, (~accessible_world(skc20, skc13))). % 13.36/4.44 tff(c_2769, plain, (![V_803, V_4, U_3]: (eventuality(V_803, V_4) | ~accessible_world(U_3, V_803) | ~event(U_3, V_4)))). % 13.36/4.44 tff(c_4289, plain, (![V_1026]: (~abstraction(V_1026, skc17) | ~accessible_world(skc14, V_1026)))). % 13.36/4.44 tff(c_4635, plain, (![V_1062]: (~male(skc14, V_1062) | ~abstraction(skc13, V_1062)))). % 13.36/4.44 tff(c_4627, plain, (![V_1061]: (~male(skc20, V_1061) | ~abstraction(skc13, V_1061)))). % 13.36/4.44 tff(c_4619, plain, (![V_1059]: (unisex(skc14, V_1059) | ~abstraction(skc13, V_1059)))). % 13.36/4.44 tff(c_4618, plain, (![V_1059]: (unisex(skc20, V_1059) | ~abstraction(skc13, V_1059)))). % 13.36/4.44 tff(c_2752, plain, (![V_797, V_26, U_25]: (unisex(V_797, V_26) | ~accessible_world(U_25, V_797) | ~abstraction(U_25, V_26)))). % 13.36/4.44 tff(c_4180, plain, (![V_1017]: (~abstraction(V_1017, skc23) | ~accessible_world(skc20, V_1017)))). % 13.36/4.44 tff(c_4307, plain, (![V_1027]: (~abstraction(V_1027, skc17) | ~accessible_world(skc20, V_1027)))). % 13.36/4.44 tff(c_4602, plain, (![V_1053]: (singleton(skc14, V_1053) | ~entity(skc13, V_1053)))). % 13.36/4.44 tff(c_4594, plain, (![V_1052]: (singleton(skc20, V_1052) | ~entity(skc13, V_1052)))). % 13.36/4.44 tff(c_4586, plain, (![V_1050]: (thing(skc14, V_1050) | ~entity(skc13, V_1050)))). % 13.36/4.44 tff(c_4585, plain, (![V_1050]: (thing(skc20, V_1050) | ~entity(skc13, V_1050)))). % 13.36/4.44 tff(c_4579, plain, (~accessible_world(skc14, skc13))). % 13.36/4.44 tff(c_2923, plain, (![V_830, V_38, U_37]: (thing(V_830, V_38) | ~accessible_world(U_37, V_830) | ~entity(U_37, V_38)))). % 13.36/4.44 tff(c_4502, plain, (![V_4]: (~abstraction(skc14, V_4) | ~event(skc13, V_4)))). % 13.36/4.44 tff(c_4487, plain, (![V_4]: (~abstraction(skc20, V_4) | ~event(skc13, V_4)))). % 13.36/4.44 tff(c_4472, plain, (![V_24]: (~eventuality(skc13, V_24) | ~abstraction(skc14, V_24)))). % 13.36/4.44 tff(c_4462, plain, (![V_24]: (~eventuality(skc13, V_24) | ~abstraction(skc20, V_24)))). % 13.36/4.44 tff(c_4452, plain, (![V_1042]: (~general(skc14, V_1042) | ~eventuality(skc13, V_1042)))). % 13.36/4.44 tff(c_4444, plain, (![V_1041]: (~general(skc20, V_1041) | ~eventuality(skc13, V_1041)))). % 13.36/4.44 tff(c_4436, plain, (![V_1039]: (specific(skc14, V_1039) | ~eventuality(skc13, V_1039)))). % 13.36/4.44 tff(c_4435, plain, (![V_1039]: (specific(skc20, V_1039) | ~eventuality(skc13, V_1039)))). % 13.36/4.44 tff(c_2341, plain, (![V_716, V_10, U_9]: (specific(V_716, V_10) | ~accessible_world(U_9, V_716) | ~eventuality(U_9, V_10)))). % 13.36/4.44 tff(c_4351, plain, (![V_24]: (~entity(skc13, V_24) | ~abstraction(skc14, V_24)))). % 13.36/4.44 tff(c_4341, plain, (![V_24]: (~entity(skc13, V_24) | ~abstraction(skc20, V_24)))). % 13.36/4.44 tff(c_4331, plain, (![V_1033]: (~general(skc14, V_1033) | ~entity(skc13, V_1033)))). % 13.36/4.44 tff(c_4323, plain, (![V_1032]: (~general(skc20, V_1032) | ~entity(skc13, V_1032)))). % 13.36/4.44 tff(c_4315, plain, (![V_1030]: (specific(skc14, V_1030) | ~entity(skc13, V_1030)))). % 13.36/4.44 tff(c_4314, plain, (![V_1030]: (specific(skc20, V_1030) | ~entity(skc13, V_1030)))). % 13.36/4.44 tff(c_2342, plain, (![V_716, V_40, U_39]: (specific(V_716, V_40) | ~accessible_world(U_39, V_716) | ~entity(U_39, V_40)))). % 13.36/4.44 tff(c_3724, plain, (![V_979]: (~abstraction(V_979, skc23) | ~accessible_world(skc14, V_979)))). % 13.36/4.44 tff(c_3375, plain, (![V_131]: (entity(V_131, skc17) | ~accessible_world(skc20, V_131)))). % 13.36/4.44 tff(c_3509, plain, (![V_131]: (entity(V_131, skc17) | ~accessible_world(skc14, V_131)))). % 13.36/4.44 tff(c_4241, plain, (![V_1023]: (~human(skc14, V_1023) | ~abstraction(skc13, V_1023)))). % 13.36/4.44 tff(c_4233, plain, (![V_1022]: (~human(skc20, V_1022) | ~abstraction(skc13, V_1022)))). % 13.36/4.44 tff(c_4225, plain, (![V_1020]: (nonhuman(skc14, V_1020) | ~abstraction(skc13, V_1020)))). % 13.36/4.44 tff(c_4224, plain, (![V_1020]: (nonhuman(skc20, V_1020) | ~abstraction(skc13, V_1020)))). % 13.36/4.44 tff(c_4218, plain, (~entity(skc20, skc21))). % 13.36/4.44 tff(c_3029, plain, (![V_853, V_22, U_21]: (nonhuman(V_853, V_22) | ~accessible_world(U_21, V_853) | ~abstraction(U_21, V_22)))). % 13.36/4.44 tff(c_4217, plain, (~entity(skc20, skc15))). % 13.36/4.44 tff(c_3577, plain, (![V_4]: (~entity(skc20, V_4) | ~event(skc13, V_4)))). % 13.36/4.44 tff(c_3368, plain, (![V_131]: (entity(V_131, skc23) | ~accessible_world(skc20, V_131)))). % 13.36/4.44 tff(c_4154, plain, (![V_1014]: (singleton(skc14, V_1014) | ~eventuality(skc13, V_1014)))). % 13.36/4.44 tff(c_4146, plain, (![V_1013]: (singleton(skc20, V_1013) | ~eventuality(skc13, V_1013)))). % 13.36/4.44 tff(c_4138, plain, (![V_1011]: (thing(skc14, V_1011) | ~eventuality(skc13, V_1011)))). % 13.36/4.44 tff(c_4137, plain, (![V_1011]: (thing(skc20, V_1011) | ~eventuality(skc13, V_1011)))). % 13.36/4.44 tff(c_2924, plain, (![V_830, V_6, U_5]: (thing(V_830, V_6) | ~accessible_world(U_5, V_830) | ~eventuality(U_5, V_6)))). % 13.36/4.44 tff(c_4130, plain, (![V_195]: (~abstraction(skc13, skf1(V_195))))). % 13.36/4.44 tff(c_3964, plain, (![V_4]: (~abstraction(skc13, V_4) | ~event(skc20, V_4)))). % 13.36/4.44 tff(c_4094, plain, (~abstraction(skc13, skc24))). % 13.36/4.44 tff(c_3977, plain, (![V_4]: (~abstraction(skc13, V_4) | ~event(skc14, V_4)))). % 13.36/4.45 tff(c_4028, plain, (![V_1004]: (~male(skc14, V_1004) | ~eventuality(skc13, V_1004)))). % 13.36/4.45 tff(c_4020, plain, (![V_1003]: (~male(skc20, V_1003) | ~eventuality(skc13, V_1003)))). % 13.36/4.45 tff(c_4012, plain, (![V_1001]: (unisex(skc14, V_1001) | ~eventuality(skc13, V_1001)))). % 13.36/4.45 tff(c_4011, plain, (![V_1001]: (unisex(skc20, V_1001) | ~eventuality(skc13, V_1001)))). % 13.36/4.45 tff(c_2751, plain, (![V_797, V_14, U_13]: (unisex(V_797, V_14) | ~accessible_world(U_13, V_797) | ~eventuality(U_13, V_14)))). % 13.36/4.45 tff(c_3884, plain, (![V_994]: (~entity(skc14, V_994) | ~abstraction(skc13, V_994)))). % 13.36/4.45 tff(c_3885, plain, (![V_994]: (~eventuality(skc14, V_994) | ~abstraction(skc13, V_994)))). % 13.36/4.45 tff(c_3873, plain, (![V_993]: (~eventuality(skc20, V_993) | ~abstraction(skc13, V_993)))). % 13.36/4.45 tff(c_3951, plain, (~entity(skc14, skc21))). % 13.36/4.45 tff(c_3950, plain, (~entity(skc14, skc15))). % 13.36/4.45 tff(c_3714, plain, (![V_4]: (~entity(skc14, V_4) | ~event(skc13, V_4)))). % 13.36/4.45 tff(c_3872, plain, (![V_993]: (~entity(skc20, V_993) | ~abstraction(skc13, V_993)))). % 13.36/4.45 tff(c_3861, plain, (![V_991]: (general(skc14, V_991) | ~abstraction(skc13, V_991)))). % 13.36/4.45 tff(c_3860, plain, (![V_991]: (general(skc20, V_991) | ~abstraction(skc13, V_991)))). % 13.36/4.45 tff(c_2312, plain, (![V_707, V_24, U_23]: (general(V_707, V_24) | ~accessible_world(U_23, V_707) | ~abstraction(U_23, V_24)))). % 13.36/4.45 tff(c_3854, plain, (~entity(skc13, skc24))). % 13.36/4.45 tff(c_3818, plain, (![V_4]: (~entity(skc13, V_4) | ~event(skc14, V_4)))). % 13.36/4.45 tff(c_3755, plain, (![V_984]: (~eventuality(skc14, V_984) | ~entity(skc13, V_984)))). % 13.36/4.45 tff(c_3804, plain, (![V_195]: (~entity(skc13, skf1(V_195))))). % 13.36/4.45 tff(c_3768, plain, (![V_4]: (~entity(skc13, V_4) | ~event(skc20, V_4)))). % 13.36/4.45 tff(c_3743, plain, (![V_983]: (~eventuality(skc20, V_983) | ~entity(skc13, V_983)))). % 13.36/4.45 tff(c_3731, plain, (![V_981]: (existent(skc14, V_981) | ~entity(skc13, V_981)))). % 13.36/4.45 tff(c_3730, plain, (![V_981]: (existent(skc20, V_981) | ~entity(skc13, V_981)))). % 13.36/4.45 tff(c_2376, plain, (![V_728, V_42, U_41]: (existent(V_728, V_42) | ~accessible_world(U_41, V_728) | ~entity(U_41, V_42)))). % 13.36/4.45 tff(c_3502, plain, (![V_131]: (entity(V_131, skc23) | ~accessible_world(skc14, V_131)))). % 13.36/4.45 tff(c_3713, plain, (~entity(skc14, skc16))). % 13.36/4.45 tff(c_3562, plain, (![V_42]: (~eventuality(skc13, V_42) | ~entity(skc14, V_42)))). % 13.36/4.45 tff(c_3691, plain, (![V_975]: (singleton(skc14, V_975) | ~abstraction(skc13, V_975)))). % 13.36/4.45 tff(c_3683, plain, (![V_974]: (singleton(skc20, V_974) | ~abstraction(skc13, V_974)))). % 13.36/4.45 tff(c_3675, plain, (![V_972]: (thing(skc14, V_972) | ~abstraction(skc13, V_972)))). % 13.36/4.45 tff(c_3674, plain, (![V_972]: (thing(skc20, V_972) | ~abstraction(skc13, V_972)))). % 13.36/4.45 tff(c_2925, plain, (![V_830, V_20, U_19]: (thing(V_830, V_20) | ~accessible_world(U_19, V_830) | ~abstraction(U_19, V_20)))). % 13.36/4.45 tff(c_3518, plain, (![V_959]: (abstraction(skc14, V_959) | ~forename(skc13, V_959)))). % 13.36/4.45 tff(c_3526, plain, (![V_960]: (abstraction(skc20, V_960) | ~forename(skc13, V_960)))). % 13.36/4.45 tff(c_3576, plain, (~entity(skc20, skc16))). % 13.36/4.45 tff(c_3556, plain, (![V_42]: (~eventuality(skc13, V_42) | ~entity(skc20, V_42)))). % 13.36/4.45 tff(c_3550, plain, (![V_965]: (~existent(skc14, V_965) | ~eventuality(skc13, V_965)))). % 13.36/4.45 tff(c_3542, plain, (![V_964]: (~existent(skc20, V_964) | ~eventuality(skc13, V_964)))). % 13.36/4.45 tff(c_3534, plain, (![V_962]: (nonexistent(skc14, V_962) | ~eventuality(skc13, V_962)))). % 13.36/4.45 tff(c_3533, plain, (![V_962]: (nonexistent(skc20, V_962) | ~eventuality(skc13, V_962)))). % 13.36/4.45 tff(c_2866, plain, (![V_821, V_12, U_11]: (nonexistent(V_821, V_12) | ~accessible_world(U_11, V_821) | ~eventuality(U_11, V_12)))). % 13.36/4.45 tff(c_3446, plain, (![V_955]: (relation(skc20, V_955) | ~forename(skc13, V_955)))). % 13.36/4.45 tff(c_3454, plain, (![V_956]: (relation(skc14, V_956) | ~forename(skc13, V_956)))). % 13.36/4.45 tff(c_3496, plain, (entity(skc14, skc17))). % 13.36/4.45 tff(c_3495, plain, (entity(skc14, skc23))). % 13.36/4.45 tff(c_3334, plain, (![V_940]: (entity(skc14, V_940) | ~human_person(skc13, V_940)))). % 13.36/4.45 tff(c_3392, plain, (![V_946]: (abstraction(skc14, V_946) | ~proposition(skc13, V_946)))). % 13.36/4.45 tff(c_3438, plain, (![V_953]: (relname(skc14, V_953) | ~forename(skc13, V_953)))). % 13.36/4.45 tff(c_3437, plain, (![V_953]: (relname(skc20, V_953) | ~forename(skc13, V_953)))). % 13.36/4.45 tff(c_3105, plain, (![V_869, V_54, U_53]: (relname(V_869, V_54) | ~accessible_world(U_53, V_869) | ~forename(U_53, V_54)))). % 13.36/4.45 tff(c_3336, plain, (![V_940]: (living(skc14, V_940) | ~human_person(skc13, V_940)))). % 13.36/4.45 tff(c_3320, plain, (![V_939]: (living(skc20, V_939) | ~human_person(skc13, V_939)))). % 13.36/4.45 tff(c_3319, plain, (![V_939]: (impartial(skc20, V_939) | ~human_person(skc13, V_939)))). % 13.36/4.45 tff(c_3335, plain, (![V_940]: (impartial(skc14, V_940) | ~human_person(skc13, V_940)))). % 13.36/4.45 tff(c_3384, plain, (![V_945]: (abstraction(skc20, V_945) | ~proposition(skc13, V_945)))). % 13.36/4.45 tff(c_3362, plain, (![V_943]: (relation(skc14, V_943) | ~proposition(skc13, V_943)))). % 13.36/4.45 tff(c_3361, plain, (![V_943]: (relation(skc20, V_943) | ~proposition(skc13, V_943)))). % 13.36/4.45 tff(c_3355, plain, (entity(skc20, skc17))). % 13.36/4.45 tff(c_3354, plain, (entity(skc20, skc23))). % 13.36/4.45 tff(c_2969, plain, (![V_840, V_16, U_15]: (relation(V_840, V_16) | ~accessible_world(U_15, V_840) | ~proposition(U_15, V_16)))). % 13.36/4.45 tff(c_3318, plain, (![V_939]: (entity(skc20, V_939) | ~human_person(skc13, V_939)))). % 13.36/4.45 tff(c_3304, plain, (![V_937]: (organism(skc14, V_937) | ~human_person(skc13, V_937)))). % 13.36/4.45 tff(c_3303, plain, (![V_937]: (organism(skc20, V_937) | ~human_person(skc13, V_937)))). % 13.36/4.45 tff(c_3025, plain, (![V_850, V_34, U_33]: (organism(V_850, V_34) | ~accessible_world(U_33, V_850) | ~human_person(U_33, V_34)))). % 13.36/4.45 tff(c_3233, plain, (![V_920, V_921]: (~entity(V_920, skf1(V_921)) | ~accessible_world(skc20, V_920)))). % 13.36/4.45 tff(c_3160, plain, (![V_898]: (be(V_898, skc16, skc17, skc17) | ~accessible_world(skc13, V_898)))). % 13.36/4.45 tff(c_3232, plain, (![V_920, V_921]: (~abstraction(V_920, skf1(V_921)) | ~accessible_world(skc20, V_920)))). % 13.36/4.45 tff(c_3154, plain, (![V_888]: (agent(V_888, skc15, skc17) | ~accessible_world(skc13, V_888)))). % 13.36/4.45 tff(c_3153, plain, (![V_888]: (agent(V_888, skc21, skc23) | ~accessible_world(skc13, V_888)))). % 13.36/4.45 tff(c_3152, plain, (![V_888]: (agent(V_888, skc24, skc23) | ~accessible_world(skc14, V_888)))). % 13.36/4.45 tff(c_3119, plain, (![V_875]: (of(V_875, skc22, skc23) | ~accessible_world(skc13, V_875)))). % 13.36/4.45 tff(c_3118, plain, (![V_875]: (of(V_875, skc18, skc17) | ~accessible_world(skc13, V_875)))). % 13.36/4.45 tff(c_2402, plain, (![V_733, V_193]: (present(V_733, skf1(V_193)) | ~accessible_world(skc20, V_733)))). % 13.36/4.45 tff(c_3048, plain, (![V_857, V_195]: (event(V_857, skf1(V_195)) | ~accessible_world(skc20, V_857)))). % 13.36/4.45 tff(c_3131, plain, (![V_883]: (theme(V_883, skc15, skc14) | ~accessible_world(skc13, V_883)))). % 13.36/4.45 tff(c_2479, plain, (![V_753, V_191]: (smoke(V_753, skf1(V_191)) | ~accessible_world(skc20, V_753)))). % 13.36/4.45 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.36/4.45 tff(c_3132, plain, (![V_883]: (theme(V_883, skc21, skc20) | ~accessible_world(skc13, V_883)))). % 13.36/4.45 tff(c_2881, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc14, V_110)))). % 13.36/4.45 tff(c_2878, plain, (![V_110]: (abstraction(V_110, skc18) | ~accessible_world(skc20, V_110)))). % 13.36/4.45 tff(c_2793, plain, (![V_110]: (abstraction(V_110, skc22) | ~accessible_world(skc20, V_110)))). % 13.36/4.45 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.36/4.45 tff(c_2796, plain, (![V_110]: (abstraction(V_110, skc22) | ~accessible_world(skc14, V_110)))). % 13.36/4.45 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.36/4.45 tff(c_2635, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc14, V_110)))). % 13.36/4.45 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.36/4.45 tff(c_3141, plain, (~abstraction(skc14, skc15))). % 13.36/4.45 tff(c_3140, plain, (~abstraction(skc20, skc15))). % 13.36/4.45 tff(c_3063, plain, (![V_860]: (~abstraction(V_860, skc15) | ~accessible_world(skc13, V_860)))). % 13.36/4.45 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.36/4.45 tff(c_3064, plain, (![V_860]: (~entity(V_860, skc15) | ~accessible_world(skc13, V_860)))). % 13.36/4.45 tff(c_2935, plain, (![U_3]: (~accessible_world(skc13, U_3) | ~event(U_3, skc23)))). % 13.36/4.45 tff(c_2613, plain, (![V_110]: (abstraction(V_110, skc20) | ~accessible_world(skc14, V_110)))). % 13.36/4.45 tff(c_2740, plain, (![V_756]: (~abstraction(V_756, skc24) | ~accessible_world(skc14, V_756)))). % 13.36/4.45 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.36/4.45 tff(c_3076, plain, (![V_861]: (~entity(V_861, skc21) | ~accessible_world(skc13, V_861)))). % 13.36/4.45 tff(c_2915, plain, (![U_3]: (~accessible_world(skc13, U_3) | ~event(U_3, skc17)))). % 13.36/4.45 tff(c_2603, plain, (![V_110]: (abstraction(V_110, skc20) | ~accessible_world(skc20, V_110)))). % 13.36/4.45 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.36/4.45 tff(c_3101, plain, (~abstraction(skc14, skc21))). % 13.36/4.45 tff(c_3100, plain, (~abstraction(skc20, skc21))). % 13.36/4.45 tff(c_3075, plain, (![V_861]: (~abstraction(V_861, skc21) | ~accessible_world(skc13, V_861)))). % 13.36/4.45 tff(c_3084, plain, (![V_863]: (think_believe_consider(V_863, skc21) | ~accessible_world(skc13, V_863)))). % 13.36/4.45 tff(c_3083, plain, (![V_863]: (think_believe_consider(V_863, skc15) | ~accessible_world(skc13, V_863)))). % 13.36/4.45 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.36/4.45 tff(c_2528, plain, (![V_756]: (~entity(V_756, skc24) | ~accessible_world(skc14, V_756)))). % 13.36/4.45 tff(c_3052, plain, (![V_857]: (event(V_857, skc21) | ~accessible_world(skc13, V_857)))). % 13.36/4.45 tff(c_3050, plain, (![V_857]: (event(V_857, skc15) | ~accessible_world(skc13, V_857)))). % 13.36/4.46 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.36/4.46 tff(c_2625, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc20, V_110)))). % 13.36/4.46 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.36/4.46 tff(c_3021, plain, (~abstraction(skc14, skc16))). % 13.36/4.46 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.36/4.46 tff(c_3020, plain, (~abstraction(skc20, skc16))). % 13.36/4.46 tff(c_2781, plain, (![V_806]: (~abstraction(V_806, skc16) | ~accessible_world(skc13, V_806)))). % 13.36/4.46 tff(c_2780, plain, (![V_806]: (~entity(V_806, skc16) | ~accessible_world(skc13, V_806)))). % 13.36/4.46 tff(c_2986, plain, (~abstraction(skc14, skc23))). % 13.36/4.46 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.36/4.46 tff(c_2985, plain, (~abstraction(skc20, skc23))). % 13.36/4.46 tff(c_2684, plain, (![V_786]: (~abstraction(V_786, skc23) | ~accessible_world(skc13, V_786)))). % 13.36/4.46 tff(c_2953, plain, (![V_836]: (human(V_836, skc17) | ~accessible_world(skc13, V_836)))). % 13.36/4.46 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.36/4.46 tff(c_2711, plain, (![V_791]: (entity(V_791, skc23) | ~accessible_world(skc13, V_791)))). % 13.36/4.46 tff(c_2943, plain, (~abstraction(skc20, skc17))). % 13.36/4.46 tff(c_2944, plain, (~abstraction(skc14, skc17))). % 13.36/4.46 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.36/4.46 tff(c_2697, plain, (![V_790]: (~abstraction(V_790, skc17) | ~accessible_world(skc13, V_790)))). % 13.36/4.46 tff(c_2683, plain, (![V_786]: (~eventuality(V_786, skc23) | ~accessible_world(skc13, V_786)))). % 13.36/4.46 tff(c_2433, plain, (![V_742]: (animate(V_742, skc17) | ~accessible_world(skc13, V_742)))). % 13.36/4.46 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.36/4.46 tff(c_2696, plain, (![V_790]: (~eventuality(V_790, skc17) | ~accessible_world(skc13, V_790)))). % 13.36/4.46 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.36/4.46 tff(c_2875, plain, (abstraction(skc14, skc18))). % 13.36/4.46 tff(c_2874, plain, (abstraction(skc20, skc18))). % 13.36/4.46 tff(c_2849, plain, (![V_818]: (abstraction(V_818, skc18) | ~accessible_world(skc13, V_818)))). % 13.36/4.46 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.36/4.46 tff(c_2719, plain, (![V_792]: (entity(V_792, skc17) | ~accessible_world(skc13, V_792)))). % 13.36/4.46 tff(c_2836, plain, (![V_816]: (forename(V_816, skc18) | ~accessible_world(skc13, V_816)))). % 13.36/4.46 tff(c_2827, plain, (![V_813]: (jules_forename(V_813, skc18) | ~accessible_world(skc13, V_813)))). % 13.36/4.46 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.36/4.46 tff(c_2812, plain, (![V_811]: (event(V_811, skc16) | ~accessible_world(skc13, V_811)))). % 13.36/4.46 tff(c_2800, plain, (![V_808]: (state(V_808, skc16) | ~accessible_world(skc13, V_808)))). % 13.36/4.46 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.36/4.46 tff(c_2790, plain, (abstraction(skc14, skc22))). % 13.36/4.46 tff(c_2789, plain, (abstraction(skc20, skc22))). % 13.36/4.46 tff(c_2468, plain, (![V_732]: (abstraction(V_732, skc22) | ~accessible_world(skc13, V_732)))). % 13.36/4.46 tff(c_2768, plain, (![V_803]: (eventuality(V_803, skc16) | ~accessible_world(skc13, V_803)))). % 13.36/4.46 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.36/4.46 tff(c_2713, plain, (![V_791]: (animate(V_791, skc23) | ~accessible_world(skc13, V_791)))). % 13.49/4.46 tff(c_2712, plain, (![V_791]: (human(V_791, skc23) | ~accessible_world(skc13, V_791)))). % 13.49/4.46 tff(c_2741, plain, (![V_195]: (~abstraction(skc20, skf1(V_195))))). % 13.49/4.46 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.49/4.46 tff(c_2745, plain, (~abstraction(skc13, skc21))). % 13.49/4.46 tff(c_2744, plain, (~abstraction(skc14, skc24))). % 13.49/4.46 tff(c_2743, plain, (~abstraction(skc13, skc15))). % 13.49/4.46 tff(c_2443, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 13.49/4.46 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.49/4.46 tff(c_2609, plain, (![V_776]: (human_person(V_776, skc23) | ~accessible_world(skc13, V_776)))). % 13.49/4.46 tff(c_2646, plain, (![V_783]: (male(V_783, skc17) | ~accessible_world(skc13, V_783)))). % 13.49/4.46 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.49/4.46 tff(c_2658, plain, (![V_784]: (male(V_784, skc23) | ~accessible_world(skc13, V_784)))). % 13.49/4.46 tff(c_2647, plain, (![V_783]: (human_person(V_783, skc17) | ~accessible_world(skc13, V_783)))). % 13.49/4.46 tff(c_2632, plain, (![V_780]: (man(V_780, skc23) | ~accessible_world(skc13, V_780)))). % 13.49/4.46 tff(c_2631, plain, (![V_780]: (man(V_780, skc17) | ~accessible_world(skc13, V_780)))). % 13.49/4.46 tff(c_2622, plain, (abstraction(skc14, skc14))). % 13.49/4.46 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.49/4.46 tff(c_2621, plain, (abstraction(skc20, skc14))). % 13.49/4.46 tff(c_2591, plain, (![V_774]: (abstraction(V_774, skc14) | ~accessible_world(skc13, V_774)))). % 13.49/4.46 tff(c_2600, plain, (abstraction(skc14, skc20))). % 13.49/4.46 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.49/4.46 tff(c_2599, plain, (abstraction(skc20, skc20))). % 13.49/4.46 tff(c_2583, plain, (![V_773]: (abstraction(V_773, skc20) | ~accessible_world(skc13, V_773)))). % 13.49/4.46 tff(c_2572, plain, (![V_770]: (proposition(V_770, skc14) | ~accessible_world(skc13, V_770)))). % 13.49/4.46 tff(c_2571, plain, (![V_770]: (proposition(V_770, skc20) | ~accessible_world(skc13, V_770)))). % 13.49/4.46 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.49/4.46 tff(c_2529, plain, (![V_195]: (~entity(skc20, skf1(V_195))))). % 13.49/4.46 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.49/4.46 tff(c_2533, plain, (~entity(skc13, skc21))). % 13.49/4.46 tff(c_2532, plain, (~entity(skc14, skc24))). % 13.49/4.46 tff(c_2531, plain, (~entity(skc13, skc15))). % 13.49/4.46 tff(c_2497, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 13.49/4.46 tff(c_2488, plain, (![V_756]: (event(V_756, skc24) | ~accessible_world(skc14, V_756)))). % 13.49/4.46 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.49/4.46 tff(c_2496, plain, (~entity(skc13, skc16))). % 13.49/4.46 tff(c_2326, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 13.49/4.46 tff(c_2480, plain, (![V_753]: (smoke(V_753, skc24) | ~accessible_world(skc14, V_753)))). % 13.49/4.46 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.49/4.46 tff(c_2473, plain, (abstraction(skc13, skc22))). % 13.49/4.46 tff(c_2470, plain, (abstraction(skc13, skc18))). % 13.49/4.46 tff(c_2362, plain, (![U_722, V_723]: (abstraction(U_722, V_723) | ~forename(U_722, V_723)))). % 13.49/4.46 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.49/4.46 tff(c_2392, plain, (![V_732]: (forename(V_732, skc22) | ~accessible_world(skc13, V_732)))). % 13.49/4.46 tff(c_2442, plain, (~abstraction(skc13, skc16))). % 13.49/4.46 tff(c_973, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.49/4.46 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.49/4.46 tff(c_2308, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.49/4.46 tff(c_2405, plain, (![V_733]: (present(V_733, skc21) | ~accessible_world(skc13, V_733)))). % 13.49/4.46 tff(c_2404, plain, (![V_733]: (present(V_733, skc24) | ~accessible_world(skc14, V_733)))). % 13.49/4.46 tff(c_2403, plain, (![V_733]: (present(V_733, skc15) | ~accessible_world(skc13, V_733)))). % 13.49/4.46 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.49/4.46 tff(c_2357, plain, (![V_719]: (vincent_forename(V_719, skc22) | ~accessible_world(skc13, V_719)))). % 13.49/4.46 tff(c_2372, plain, (abstraction(skc13, skc14))). % 13.49/4.46 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.49/4.46 tff(c_2371, plain, (abstraction(skc13, skc20))). % 13.49/4.46 tff(c_351, plain, (![U_15, V_16]: (abstraction(U_15, V_16) | ~proposition(U_15, V_16)))). % 13.49/4.46 tff(c_370, plain, (![U_261, V_262]: (singleton(U_261, V_262) | ~eventuality(U_261, V_262)))). % 13.49/4.46 tff(c_289, plain, (![U_229, V_230]: (relation(U_229, V_230) | ~forename(U_229, V_230)))). % 13.49/4.46 tff(c_2350, plain, (~event(skc13, skc17))). % 13.49/4.46 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.49/4.46 tff(c_2346, plain, (~event(skc13, skc23))). % 13.49/4.46 tff(c_2335, plain, (~eventuality(skc13, skc17))). % 13.49/4.46 tff(c_2334, plain, (~eventuality(skc13, skc23))). % 13.49/4.46 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.49/4.46 tff(c_356, plain, (![U_257, V_258]: (~male(U_257, V_258) | ~eventuality(U_257, V_258)))). % 13.49/4.46 tff(c_276, plain, (![U_11, V_12]: (~existent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 13.49/4.46 tff(c_2321, plain, (entity(skc13, skc17))). % 13.49/4.46 tff(c_2320, plain, (entity(skc13, skc23))). % 13.49/4.46 tff(c_328, plain, (![U_245, V_246]: (entity(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.49/4.46 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.49/4.46 tff(c_335, plain, (![U_247, V_248]: (~general(U_247, V_248) | ~entity(U_247, V_248)))). % 13.49/4.46 tff(c_329, plain, (![U_245, V_246]: (impartial(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.49/4.46 tff(c_249, plain, (![U_209, V_210]: (singleton(U_209, V_210) | ~abstraction(U_209, V_210)))). % 13.49/4.46 tff(c_220, plain, (![U_196]: (agent(skc20, skf1(U_196), U_196) | ~man(skc20, U_196)))). % 13.49/4.46 tff(c_282, plain, (![U_223, V_224]: (~male(U_223, V_224) | ~abstraction(U_223, V_224)))). % 13.49/4.46 tff(c_2291, plain, (~abstraction(skc13, skc23))). % 13.49/4.46 tff(c_2290, plain, (~abstraction(skc13, skc17))). % 13.49/4.46 tff(c_346, plain, (![U_253, V_254]: (~human(U_253, V_254) | ~abstraction(U_253, V_254)))). % 13.49/4.46 tff(c_375, plain, (![U_263, V_264]: (singleton(U_263, V_264) | ~entity(U_263, V_264)))). % 13.49/4.47 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.49/4.47 tff(c_330, plain, (![U_245, V_246]: (living(U_245, V_246) | ~human_person(U_245, V_246)))). % 13.49/4.47 tff(c_2268, plain, (![V_191]: (smoke(skc20, skf1(V_191))))). % 13.49/4.47 tff(c_1700, plain, (![V_195]: (event(skc20, skf1(V_195))))). % 13.49/4.47 tff(c_341, plain, (![U_251, V_252]: (~general(U_251, V_252) | ~eventuality(U_251, V_252)))). % 13.49/4.47 tff(c_967, plain, (![V_193]: (present(skc20, skf1(V_193))))). % 13.49/4.47 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 13.49/4.47 tff(c_365, plain, (human(skc13, skc17))). % 13.49/4.47 tff(c_364, plain, (human(skc13, skc23))). % 13.49/4.47 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 13.49/4.47 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 13.49/4.47 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 13.49/4.47 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 13.49/4.47 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 13.49/4.47 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 13.49/4.47 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 13.49/4.47 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 13.49/4.47 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 13.49/4.47 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 13.49/4.47 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 13.49/4.47 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 13.49/4.47 tff(c_309, plain, (eventuality(skc13, skc16))). % 13.49/4.47 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 13.49/4.47 tff(c_304, plain, (event(skc13, skc16))). % 13.49/4.47 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 13.49/4.47 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 13.49/4.47 tff(c_298, plain, (male(skc13, skc23))). % 13.49/4.47 tff(c_297, plain, (male(skc13, skc17))). % 13.49/4.47 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 13.49/4.47 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 13.49/4.47 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 13.49/4.47 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 13.49/4.47 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 13.49/4.47 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 13.49/4.47 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 13.49/4.47 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 13.49/4.47 tff(c_260, plain, (animate(skc13, skc17))). % 13.49/4.47 tff(c_259, plain, (animate(skc13, skc23))). % 13.49/4.47 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 13.49/4.47 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 13.49/4.47 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 13.49/4.47 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 13.49/4.47 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 13.49/4.47 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 13.49/4.47 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 13.49/4.47 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 13.49/4.47 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 13.49/4.47 tff(c_229, plain, (human_person(skc13, skc23))). % 13.49/4.47 tff(c_228, plain, (human_person(skc13, skc17))). % 13.49/4.47 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 13.49/4.47 tff(c_212, plain, (be(skc13, skc16, skc17, skc17))). % 13.49/4.47 tff(c_210, plain, (theme(skc13, skc15, skc14))). % 13.49/4.47 tff(c_200, plain, (agent(skc14, skc24, skc23))). % 13.49/4.47 tff(c_202, plain, (theme(skc13, skc21, skc20))). % 13.49/4.47 tff(c_204, plain, (of(skc13, skc18, skc17))). % 13.49/4.47 tff(c_198, plain, (agent(skc13, skc21, skc23))). % 13.49/4.47 tff(c_196, plain, (of(skc13, skc22, skc23))). % 13.49/4.47 tff(c_206, plain, (agent(skc13, skc15, skc17))). % 13.49/4.47 tff(c_174, plain, (man(skc13, skc17))). % 13.49/4.47 tff(c_178, plain, (state(skc13, skc16))). % 13.49/4.47 tff(c_180, plain, (think_believe_consider(skc13, skc15))). % 13.49/4.47 tff(c_182, plain, (present(skc13, skc15))). % 13.49/4.47 tff(c_172, plain, (forename(skc13, skc18))). % 13.49/4.47 tff(c_170, plain, (jules_forename(skc13, skc18))). % 13.49/4.47 tff(c_166, plain, (think_believe_consider(skc13, skc21))). % 13.49/4.47 tff(c_184, plain, (event(skc13, skc15))). % 13.49/4.47 tff(c_146, plain, (event(skc14, skc24))). % 13.49/4.47 tff(c_186, plain, (accessible_world(skc13, skc20))). % 13.49/4.47 tff(c_148, plain, (man(skc13, skc23))). % 13.49/4.47 tff(c_150, plain, (present(skc14, skc24))). % 13.49/4.47 tff(c_152, plain, (smoke(skc14, skc24))). % 13.49/4.47 tff(c_164, plain, (present(skc13, skc21))). % 13.49/4.47 tff(c_188, plain, (proposition(skc13, skc20))). % 13.49/4.47 tff(c_162, plain, (event(skc13, skc21))). % 13.49/4.47 tff(c_160, plain, (vincent_forename(skc13, skc22))). % 13.49/4.47 tff(c_158, plain, (forename(skc13, skc22))). % 13.49/4.47 tff(c_190, plain, (proposition(skc13, skc14))). % 13.49/4.47 tff(c_192, plain, (accessible_world(skc13, skc14))). % 13.49/4.47 tff(c_144, plain, (actual_world(skc13))). % 13.49/4.47 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.49/4.47 %------------------------------------------------------------------------------