%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP244-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n026.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.35s 4.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : NLP244-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 09:45:23 EDT 2025 % 0.12/0.33 % CPUTime : % 12.35/4.18 % 12.35/4.19 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.35/4.19 % 12.35/4.19 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.35/4.20 %$ 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 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 > skc14 % 12.35/4.20 % 12.35/4.20 %Foreground sorts: % 12.35/4.20 % 12.35/4.20 % 12.35/4.20 %Background operators: % 12.35/4.20 % 12.35/4.20 % 12.35/4.20 %Foreground operators: % 12.35/4.20 tff(skc16, type, skc16: $i). % 12.35/4.20 tff(relation, type, relation: ($i * $i) > $o). % 12.35/4.20 tff(forename, type, forename: ($i * $i) > $o). % 12.35/4.20 tff(be, type, be: ($i * $i * $i * $i) > $o). % 12.35/4.20 tff(theme, type, theme: ($i * $i * $i) > $o). % 12.35/4.20 tff(living, type, living: ($i * $i) > $o). % 12.35/4.20 tff(human_person, type, human_person: ($i * $i) > $o). % 12.35/4.20 tff(present, type, present: ($i * $i) > $o). % 12.35/4.20 tff(entity, type, entity: ($i * $i) > $o). % 12.35/4.20 tff(skc18, type, skc18: $i). % 12.35/4.20 tff(eventuality, type, eventuality: ($i * $i) > $o). % 12.35/4.20 tff(existent, type, existent: ($i * $i) > $o). % 12.35/4.20 tff(abstraction, type, abstraction: ($i * $i) > $o). % 12.35/4.20 tff(skc25, type, skc25: $i). % 12.35/4.20 tff(skf1, type, skf1: $i > $i). % 12.35/4.20 tff(proposition, type, proposition: ($i * $i) > $o). % 12.35/4.20 tff(relname, type, relname: ($i * $i) > $o). % 12.35/4.20 tff(skc14, type, skc14: $i). % 12.35/4.20 tff(singleton, type, singleton: ($i * $i) > $o). % 12.35/4.20 tff(skc17, type, skc17: $i). % 12.35/4.20 tff(male, type, male: ($i * $i) > $o). % 12.35/4.20 tff(organism, type, organism: ($i * $i) > $o). % 12.35/4.20 tff(animate, type, animate: ($i * $i) > $o). % 12.35/4.20 tff(of, type, of: ($i * $i * $i) > $o). % 12.35/4.20 tff(actual_world, type, actual_world: $i > $o). % 12.35/4.20 tff(agent, type, agent: ($i * $i * $i) > $o). % 12.35/4.20 tff(skc26, type, skc26: $i). % 12.35/4.20 tff(skc24, type, skc24: $i). % 12.35/4.20 tff(skc20, type, skc20: $i). % 12.35/4.20 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 12.35/4.20 tff(general, type, general: ($i * $i) > $o). % 12.35/4.20 tff(smoke, type, smoke: ($i * $i) > $o). % 12.35/4.20 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 12.35/4.20 tff(skc23, type, skc23: $i). % 12.35/4.20 tff(event, type, event: ($i * $i) > $o). % 12.35/4.20 tff(skc21, type, skc21: $i). % 12.35/4.20 tff(skc22, type, skc22: $i). % 12.35/4.20 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 12.35/4.20 tff(skc27, type, skc27: $i). % 12.35/4.20 tff(state, type, state: ($i * $i) > $o). % 12.35/4.20 tff(thing, type, thing: ($i * $i) > $o). % 12.35/4.20 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 12.35/4.20 tff(skc15, type, skc15: $i). % 12.35/4.20 tff(human, type, human: ($i * $i) > $o). % 12.35/4.20 tff(man, type, man: ($i * $i) > $o). % 12.35/4.20 tff(unisex, type, unisex: ($i * $i) > $o). % 12.35/4.20 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 12.35/4.20 tff(impartial, type, impartial: ($i * $i) > $o). % 12.35/4.20 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 12.35/4.20 tff(specific, type, specific: ($i * $i) > $o). % 12.35/4.20 tff(skc19, type, skc19: $i). % 12.35/4.20 % 12.35/4.20 %Saturated clause set: % 12.35/4.20 tff(c_7571, plain, (![V_146, V_1415]: (animate(V_146, skc22) | ~accessible_world(V_1415, V_146) | ~accessible_world(skc24, V_1415)))). % 12.35/4.20 tff(c_7596, plain, (![V_143, V_1416]: (human(V_143, skc22) | ~accessible_world(V_1416, V_143) | ~accessible_world(skc24, V_1416)))). % 12.35/4.20 tff(c_7564, plain, (![V_125, V_1414]: (human_person(V_125, skc22) | ~accessible_world(V_1414, V_125) | ~accessible_world(skc24, V_1414)))). % 12.35/4.20 tff(c_7529, plain, (![V_149, V_1413]: (male(V_149, skc22) | ~accessible_world(V_1413, V_149) | ~accessible_world(skc24, V_1413)))). % 12.35/4.20 tff(c_7481, plain, (![V_122, V_1412]: (man(V_122, skc22) | ~accessible_world(V_1412, V_122) | ~accessible_world(skc24, V_1412)))). % 12.35/4.20 tff(c_7623, plain, (![U_3]: (~accessible_world(skc24, U_3) | ~event(U_3, skc22)))). % 12.35/4.20 tff(c_7531, plain, (![V_1413]: (~eventuality(V_1413, skc22) | ~accessible_world(skc24, V_1413)))). % 12.35/4.20 tff(c_7566, plain, (![V_1414]: (human(V_1414, skc22) | ~accessible_world(skc24, V_1414)))). % 12.35/4.20 tff(c_7567, plain, (![V_1414]: (animate(V_1414, skc22) | ~accessible_world(skc24, V_1414)))). % 12.35/4.20 tff(c_7394, plain, (![V_125]: (human_person(V_125, skc22) | ~accessible_world(skc24, V_125)))). % 12.35/4.20 tff(c_7431, plain, (![V_149]: (male(V_149, skc22) | ~accessible_world(skc24, V_149)))). % 12.35/4.20 tff(c_7379, plain, (![V_122]: (man(V_122, skc22) | ~accessible_world(skc24, V_122)))). % 12.35/4.20 tff(c_7471, plain, (~event(skc24, skc22))). % 12.35/4.20 tff(c_7433, plain, (~eventuality(skc24, skc22))). % 12.35/4.20 tff(c_7397, plain, (human(skc24, skc22))). % 12.35/4.20 tff(c_7398, plain, (animate(skc24, skc22))). % 12.35/4.20 tff(c_7381, plain, (male(skc24, skc22))). % 12.35/4.20 tff(c_7380, plain, (human_person(skc24, skc22))). % 12.35/4.20 tff(c_7369, plain, (![W_1394, V_1391, V_673]: (W_1394=V_1391 | ~theme(V_673, skc23, W_1394) | ~think_believe_consider(V_673, skc23) | ~think_believe_consider(V_673, skf1(skc22)) | ~theme(V_673, skf1(skc22), V_1391) | ~proposition(V_673, W_1394) | ~proposition(V_673, V_1391) | ~accessible_world(skc24, V_673) | ~accessible_world(skc15, V_673)))). % 12.35/4.20 tff(c_7370, plain, (man(skc24, skc22))). % 12.35/4.20 tff(c_7356, plain, (![V_1405, V_662]: (skc15=V_1405 | ~think_believe_consider(V_662, skc16) | ~think_believe_consider(V_662, skf1(skc18)) | ~theme(V_662, skf1(skc18), V_1405) | ~proposition(V_662, skc15) | ~proposition(V_662, V_1405) | ~accessible_world(skc24, V_662) | ~accessible_world(skc14, V_662)))). % 12.35/4.20 tff(c_7328, plain, (![W_1394, V_1391, V_673]: (W_1394=V_1391 | ~theme(V_673, skc16, W_1394) | ~think_believe_consider(V_673, skc16) | ~think_believe_consider(V_673, skf1(skc18)) | ~theme(V_673, skf1(skc18), V_1391) | ~proposition(V_673, W_1394) | ~proposition(V_673, V_1391) | ~accessible_world(skc24, V_673) | ~accessible_world(skc14, V_673)))). % 12.35/4.20 tff(c_7346, plain, (![V_1400, V_662]: (skc24=V_1400 | ~think_believe_consider(V_662, skc25) | ~think_believe_consider(V_662, skf1(skc27)) | ~theme(V_662, skf1(skc27), V_1400) | ~proposition(V_662, skc24) | ~proposition(V_662, V_1400) | ~accessible_world(skc24, V_662) | ~accessible_world(skc14, V_662)))). % 12.35/4.20 tff(c_7331, plain, (![W_1394, V_1391, V_673]: (W_1394=V_1391 | ~theme(V_673, skc25, W_1394) | ~think_believe_consider(V_673, skc25) | ~think_believe_consider(V_673, skf1(skc27)) | ~theme(V_673, skf1(skc27), V_1391) | ~proposition(V_673, W_1394) | ~proposition(V_673, V_1391) | ~accessible_world(skc24, V_673) | ~accessible_world(skc14, V_673)))). % 12.35/4.20 tff(c_7324, plain, (![W_1394, V_1391, V_673, U_196]: (W_1394=V_1391 | ~theme(V_673, skf1(U_196), W_1394) | ~think_believe_consider(V_673, skf1(U_196)) | ~theme(V_673, skf1(U_196), V_1391) | ~proposition(V_673, W_1394) | ~proposition(V_673, V_1391) | ~accessible_world(skc24, V_673) | ~man(skc24, U_196)))). % 12.35/4.20 tff(c_3915, plain, (![V_865, V_189, Y_188, U_866, W_184]: (W_184=V_189 | ~agent(V_865, Y_188, U_866) | ~theme(V_865, Y_188, W_184) | ~think_believe_consider(V_865, Y_188) | ~think_believe_consider(V_865, skf1(U_866)) | ~theme(V_865, skf1(U_866), V_189) | ~proposition(V_865, W_184) | ~proposition(V_865, V_189) | ~accessible_world(skc24, V_865) | ~man(skc24, U_866)))). % 12.35/4.20 tff(c_7306, plain, (~accessible_world(skc15, skc24))). % 12.35/4.20 tff(c_7295, plain, (![V_1382, V_662]: (skc15=V_1382 | ~agent(V_662, skc16, skc22) | ~think_believe_consider(V_662, skc16) | ~think_believe_consider(V_662, skc23) | ~theme(V_662, skc23, V_1382) | ~proposition(V_662, skc15) | ~proposition(V_662, V_1382) | ~accessible_world(skc15, V_662) | ~accessible_world(skc14, V_662)))). % 12.35/4.20 tff(c_7294, plain, (![V_1382, V_662]: (skc24=V_1382 | ~agent(V_662, skc25, skc22) | ~think_believe_consider(V_662, skc25) | ~think_believe_consider(V_662, skc23) | ~theme(V_662, skc23, V_1382) | ~proposition(V_662, skc24) | ~proposition(V_662, V_1382) | ~accessible_world(skc15, V_662) | ~accessible_world(skc14, V_662)))). % 12.35/4.20 tff(c_7302, plain, (![V_662]: (~agent(V_662, skc16, skc27) | ~think_believe_consider(V_662, skc16) | ~think_believe_consider(V_662, skc25) | ~proposition(V_662, skc15) | ~proposition(V_662, skc24) | ~accessible_world(skc14, V_662)))). % 12.35/4.20 tff(c_2284, plain, (![W_184, V_189, V_712, Y_188]: (W_184=V_189 | ~agent(V_712, Y_188, skc22) | ~theme(V_712, Y_188, W_184) | ~think_believe_consider(V_712, Y_188) | ~think_believe_consider(V_712, skc23) | ~theme(V_712, skc23, V_189) | ~proposition(V_712, W_184) | ~proposition(V_712, V_189) | ~accessible_world(skc15, V_712)))). % 12.35/4.20 tff(c_7254, plain, (![V_1373, V_662]: (skc15=V_1373 | ~agent(V_662, skc16, skc27) | ~think_believe_consider(V_662, skc16) | ~think_believe_consider(V_662, skc25) | ~theme(V_662, skc25, V_1373) | ~proposition(V_662, skc15) | ~proposition(V_662, V_1373) | ~accessible_world(skc14, V_662)))). % 12.35/4.21 tff(c_7253, plain, (![V_1373, V_662]: (skc24=V_1373 | ~agent(V_662, skc25, skc27) | ~think_believe_consider(V_662, skc25) | ~theme(V_662, skc25, V_1373) | ~proposition(V_662, skc24) | ~proposition(V_662, V_1373) | ~accessible_world(skc14, V_662)))). % 12.35/4.21 tff(c_7243, plain, (![V_662]: (~agent(V_662, skc25, skc18) | ~think_believe_consider(V_662, skc25) | ~think_believe_consider(V_662, skc16) | ~proposition(V_662, skc24) | ~proposition(V_662, skc15) | ~accessible_world(skc14, V_662)))). % 12.35/4.21 tff(c_2270, plain, (![W_184, V_189, V_710, Y_188]: (W_184=V_189 | ~agent(V_710, Y_188, skc27) | ~theme(V_710, Y_188, W_184) | ~think_believe_consider(V_710, Y_188) | ~think_believe_consider(V_710, skc25) | ~theme(V_710, skc25, V_189) | ~proposition(V_710, W_184) | ~proposition(V_710, V_189) | ~accessible_world(skc14, V_710)))). % 12.35/4.21 tff(c_7212, plain, (![V_1365, V_662]: (skc24=V_1365 | ~agent(V_662, skc25, skc18) | ~think_believe_consider(V_662, skc25) | ~think_believe_consider(V_662, skc16) | ~theme(V_662, skc16, V_1365) | ~proposition(V_662, skc24) | ~proposition(V_662, V_1365) | ~accessible_world(skc14, V_662)))). % 12.35/4.21 tff(c_7213, plain, (![V_1365, V_662]: (skc15=V_1365 | ~agent(V_662, skc16, skc18) | ~think_believe_consider(V_662, skc16) | ~theme(V_662, skc16, V_1365) | ~proposition(V_662, skc15) | ~proposition(V_662, V_1365) | ~accessible_world(skc14, V_662)))). % 12.35/4.21 tff(c_2277, plain, (![W_184, V_189, V_711, Y_188]: (W_184=V_189 | ~agent(V_711, Y_188, skc18) | ~theme(V_711, Y_188, W_184) | ~think_believe_consider(V_711, Y_188) | ~think_believe_consider(V_711, skc16) | ~theme(V_711, skc16, V_189) | ~proposition(V_711, W_184) | ~proposition(V_711, V_189) | ~accessible_world(skc14, V_711)))). % 12.35/4.21 tff(c_6819, plain, (![V_143, V_1329]: (human(V_143, skc27) | ~accessible_world(V_1329, V_143) | ~accessible_world(skc24, V_1329)))). % 12.35/4.21 tff(c_7102, plain, (![V_146, V_1343]: (animate(V_146, skc18) | ~accessible_world(V_1343, V_146) | ~accessible_world(skc24, V_1343)))). % 12.35/4.21 tff(c_6824, plain, (![V_146, V_1330]: (animate(V_146, skc27) | ~accessible_world(V_1330, V_146) | ~accessible_world(skc24, V_1330)))). % 12.35/4.21 tff(c_7097, plain, (![V_143, V_1342]: (human(V_143, skc18) | ~accessible_world(V_1342, V_143) | ~accessible_world(skc24, V_1342)))). % 12.35/4.21 tff(c_7070, plain, (![V_149, V_1341]: (male(V_149, skc18) | ~accessible_world(V_1341, V_149) | ~accessible_world(skc24, V_1341)))). % 12.35/4.21 tff(c_7021, plain, (![V_125, V_1340]: (human_person(V_125, skc18) | ~accessible_world(V_1340, V_125) | ~accessible_world(skc24, V_1340)))). % 12.35/4.21 tff(c_6716, plain, (![V_125, V_1326]: (human_person(V_125, skc27) | ~accessible_world(V_1326, V_125) | ~accessible_world(skc24, V_1326)))). % 12.35/4.21 tff(c_6988, plain, (![V_101, V_1339]: (think_believe_consider(V_101, skc16) | ~accessible_world(V_1339, V_101) | ~accessible_world(skc24, V_1339)))). % 12.35/4.21 tff(c_6969, plain, (![V_122, V_1338]: (man(V_122, skc18) | ~accessible_world(V_1338, V_122) | ~accessible_world(skc24, V_1338)))). % 12.35/4.21 tff(c_7129, plain, (![U_3]: (~accessible_world(skc24, U_3) | ~event(U_3, skc18)))). % 12.35/4.21 tff(c_7072, plain, (![V_1341]: (~eventuality(V_1341, skc18) | ~accessible_world(skc24, V_1341)))). % 12.35/4.21 tff(c_7103, plain, (~think_believe_consider(skc24, skf1(skc18)))). % 12.35/4.21 tff(c_7024, plain, (![V_1340]: (animate(V_1340, skc18) | ~accessible_world(skc24, V_1340)))). % 12.35/4.21 tff(c_7023, plain, (![V_1340]: (human(V_1340, skc18) | ~accessible_world(skc24, V_1340)))). % 12.35/4.21 tff(c_6919, plain, (![V_149]: (male(V_149, skc18) | ~accessible_world(skc24, V_149)))). % 12.35/4.21 tff(c_6970, plain, (![V_1338]: (human_person(V_1338, skc18) | ~accessible_world(skc24, V_1338)))). % 12.35/4.21 tff(c_6984, plain, (![V_101]: (think_believe_consider(V_101, skc16) | ~accessible_world(skc24, V_101)))). % 12.35/4.21 tff(c_6981, plain, (think_believe_consider(skc24, skc16))). % 12.35/4.21 tff(c_6868, plain, (![V_122]: (man(V_122, skc18) | ~accessible_world(skc24, V_122)))). % 12.35/4.21 tff(c_6940, plain, (~event(skc24, skc18))). % 12.35/4.21 tff(c_6885, plain, (human(skc24, skc18))). % 12.35/4.21 tff(c_6921, plain, (~eventuality(skc24, skc18))). % 12.35/4.21 tff(c_6886, plain, (animate(skc24, skc18))). % 12.35/4.21 tff(c_6870, plain, (male(skc24, skc18))). % 12.35/4.21 tff(c_6869, plain, (human_person(skc24, skc18))). % 12.35/4.21 tff(c_6859, plain, (man(skc24, skc18))). % 12.35/4.21 tff(c_6765, plain, (![V_149, V_1327]: (male(V_149, skc27) | ~accessible_world(V_1327, V_149) | ~accessible_world(skc24, V_1327)))). % 12.35/4.21 tff(c_6677, plain, (![V_122, V_1324]: (man(V_122, skc27) | ~accessible_world(V_1324, V_122) | ~accessible_world(skc24, V_1324)))). % 12.35/4.21 tff(c_6683, plain, (![V_101, V_1325]: (think_believe_consider(V_101, skc25) | ~accessible_world(V_1325, V_101) | ~accessible_world(skc24, V_1325)))). % 12.35/4.21 tff(c_6793, plain, (![U_3]: (~accessible_world(skc24, U_3) | ~event(U_3, skc27)))). % 12.35/4.21 tff(c_6638, plain, (![V_146]: (animate(V_146, skc27) | ~accessible_world(skc24, V_146)))). % 12.35/4.21 tff(c_6718, plain, (![V_1326]: (human(V_1326, skc27) | ~accessible_world(skc24, V_1326)))). % 12.35/4.21 tff(c_6794, plain, (~think_believe_consider(skc24, skf1(skc27)))). % 12.35/4.21 tff(c_6767, plain, (![V_1327]: (~eventuality(V_1327, skc27) | ~accessible_world(skc24, V_1327)))). % 12.35/4.21 tff(c_6679, plain, (![V_1324]: (male(V_1324, skc27) | ~accessible_world(skc24, V_1324)))). % 12.35/4.21 tff(c_6678, plain, (![V_1324]: (human_person(V_1324, skc27) | ~accessible_world(skc24, V_1324)))). % 12.35/4.21 tff(c_6667, plain, (![V_101]: (think_believe_consider(V_101, skc25) | ~accessible_world(skc24, V_101)))). % 12.35/4.21 tff(c_6563, plain, (![V_122]: (man(V_122, skc27) | ~accessible_world(skc24, V_122)))). % 12.35/4.21 tff(c_6664, plain, (think_believe_consider(skc24, skc25))). % 12.35/4.21 tff(c_6654, plain, (~event(skc24, skc27))). % 12.35/4.21 tff(c_6616, plain, (~eventuality(skc24, skc27))). % 12.35/4.21 tff(c_6581, plain, (animate(skc24, skc27))). % 12.35/4.21 tff(c_6580, plain, (human(skc24, skc27))). % 12.35/4.21 tff(c_6565, plain, (male(skc24, skc27))). % 12.35/4.21 tff(c_6564, plain, (human_person(skc24, skc27))). % 12.35/4.21 tff(c_6554, plain, (man(skc24, skc27))). % 12.35/4.21 tff(c_4242, plain, (![W_918, V_919, U_196]: (W_918=V_919 | ~theme(skc24, skf1(U_196), W_918) | ~think_believe_consider(skc24, skf1(U_196)) | ~theme(skc24, skf1(U_196), V_919) | ~proposition(skc24, W_918) | ~proposition(skc24, V_919) | ~man(skc24, U_196)))). % 12.35/4.21 tff(c_2291, plain, (![W_182, V_713]: (skc21=W_182 | ~entity(V_713, skc22) | ~forename(V_713, W_182) | ~of(V_713, W_182, skc22) | ~forename(V_713, skc21) | ~accessible_world(skc14, V_713)))). % 12.35/4.21 tff(c_5436, plain, (![V_86, V_1103, V_1102]: (singleton(V_86, V_1103) | ~accessible_world(V_1102, V_86) | ~accessible_world(skc24, V_1102) | ~eventuality(skc14, V_1103)))). % 12.35/4.21 tff(c_5132, plain, (![V_86, V_1056, V_1055]: (singleton(V_86, V_1056) | ~accessible_world(V_1055, V_86) | ~accessible_world(skc15, V_1055) | ~eventuality(skc14, V_1056)))). % 12.35/4.21 tff(c_5104, plain, (![V_140, V_1048, V_1047]: (living(V_140, V_1048) | ~accessible_world(V_1047, V_140) | ~accessible_world(skc24, V_1047) | ~human_person(skc14, V_1048)))). % 12.35/4.21 tff(c_5171, plain, (![V_107, V_1062, V_1061]: (relation(V_107, V_1062) | ~accessible_world(V_1061, V_107) | ~accessible_world(skc24, V_1061) | ~forename(skc14, V_1062)))). % 12.35/4.21 tff(c_5348, plain, (![V_137, V_1093, V_1092]: (impartial(V_137, V_1093) | ~accessible_world(V_1092, V_137) | ~accessible_world(skc15, V_1092) | ~human_person(skc14, V_1093)))). % 12.35/4.21 tff(c_5197, plain, (![V_140, V_1071, V_1070]: (living(V_140, V_1071) | ~accessible_world(V_1070, V_140) | ~accessible_world(skc15, V_1070) | ~human_person(skc14, V_1071)))). % 12.35/4.22 tff(c_5356, plain, (![V_137, V_1097, V_1096]: (impartial(V_137, V_1097) | ~accessible_world(V_1096, V_137) | ~accessible_world(skc24, V_1096) | ~human_person(skc14, V_1097)))). % 12.35/4.22 tff(c_2333, plain, (![W_182, V_722]: (skc19=W_182 | ~entity(V_722, skc18) | ~forename(V_722, W_182) | ~of(V_722, W_182, skc18) | ~forename(V_722, skc19) | ~accessible_world(skc14, V_722)))). % 12.35/4.22 tff(c_5273, plain, (![V_86, V_1081, V_1080]: (singleton(V_86, V_1081) | ~accessible_world(V_1080, V_86) | ~accessible_world(skc24, V_1080) | ~entity(skc14, V_1081)))). % 12.35/4.22 tff(c_5127, plain, (![V_107, V_1054, V_1053]: (relation(V_107, V_1054) | ~accessible_world(V_1053, V_107) | ~accessible_world(skc15, V_1053) | ~forename(skc14, V_1054)))). % 12.35/4.22 tff(c_5352, plain, (![V_86, V_1095, V_1094]: (singleton(V_86, V_1095) | ~accessible_world(V_1094, V_86) | ~accessible_world(skc15, V_1094) | ~entity(skc14, V_1095)))). % 12.35/4.22 tff(c_5185, plain, (![V_86, V_1066, V_1065]: (singleton(V_86, V_1066) | ~accessible_world(V_1065, V_86) | ~accessible_world(skc24, V_1065) | ~abstraction(skc14, V_1066)))). % 12.35/4.22 tff(c_4973, plain, (![V_86, V_1040, V_1039]: (singleton(V_86, V_1040) | ~accessible_world(V_1039, V_86) | ~accessible_world(skc15, V_1039) | ~abstraction(skc14, V_1040)))). % 12.35/4.22 tff(c_4777, plain, (![V_128, V_995, V_994]: (organism(V_128, V_995) | ~accessible_world(V_994, V_128) | ~accessible_world(skc15, V_994) | ~human_person(skc14, V_995)))). % 12.35/4.22 tff(c_4546, plain, (![V_89, V_958, V_957]: (specific(V_89, V_958) | ~accessible_world(V_957, V_89) | ~accessible_world(skc15, V_957) | ~entity(skc14, V_958)))). % 12.35/4.22 tff(c_4754, plain, (![V_128, V_991, V_990]: (organism(V_128, V_991) | ~accessible_world(V_990, V_128) | ~accessible_world(skc24, V_990) | ~human_person(skc14, V_991)))). % 12.35/4.22 tff(c_4827, plain, (![V_92, V_1007, V_1006]: (nonexistent(V_92, V_1007) | ~accessible_world(V_1006, V_92) | ~accessible_world(skc24, V_1006) | ~eventuality(skc14, V_1007)))). % 12.35/4.22 tff(c_2263, plain, (![W_182, V_709]: (skc26=W_182 | ~entity(V_709, skc27) | ~forename(V_709, W_182) | ~of(V_709, W_182, skc27) | ~forename(V_709, skc26) | ~accessible_world(skc14, V_709)))). % 12.35/4.22 tff(c_4538, plain, (![V_134, V_956, V_955]: (existent(V_134, V_956) | ~accessible_world(V_955, V_134) | ~accessible_world(skc15, V_955) | ~entity(skc14, V_956)))). % 12.35/4.22 tff(c_4835, plain, (![V_107, V_1009, V_1008]: (relation(V_107, V_1009) | ~accessible_world(V_1008, V_107) | ~accessible_world(skc24, V_1008) | ~proposition(skc14, V_1009)))). % 12.35/4.22 tff(c_4607, plain, (![V_89, V_975, V_974]: (specific(V_89, V_975) | ~accessible_world(V_974, V_89) | ~accessible_world(skc15, V_974) | ~eventuality(skc14, V_975)))). % 12.35/4.22 tff(c_4731, plain, (![V_80, V_987, V_986]: (eventuality(V_80, V_987) | ~accessible_world(V_986, V_80) | ~accessible_world(skc24, V_986) | ~event(skc14, V_987)))). % 12.35/4.22 tff(c_4787, plain, (![V_92, V_997, V_996]: (nonexistent(V_92, V_997) | ~accessible_world(V_996, V_92) | ~accessible_world(skc15, V_996) | ~eventuality(skc14, V_997)))). % 12.35/4.22 tff(c_4591, plain, (![V_83, V_970, V_969]: (thing(V_83, V_970) | ~accessible_world(V_969, V_83) | ~accessible_world(skc24, V_969) | ~eventuality(skc14, V_970)))). % 12.35/4.22 tff(c_4425, plain, (![V_116, V_948, V_947]: (general(V_116, V_948) | ~accessible_world(V_947, V_116) | ~accessible_world(skc24, V_947) | ~abstraction(skc14, V_948)))). % 12.35/4.22 tff(c_4866, plain, (![V_155, V_1018, V_1017]: (relname(V_155, V_1018) | ~accessible_world(V_1017, V_155) | ~accessible_world(skc24, V_1017) | ~forename(skc14, V_1018)))). % 12.35/4.22 tff(c_4811, plain, (![V_83, V_1003, V_1002]: (thing(V_83, V_1003) | ~accessible_world(V_1002, V_83) | ~accessible_world(skc24, V_1002) | ~abstraction(skc14, V_1003)))). % 12.35/4.22 tff(c_4803, plain, (![V_155, V_1001, V_1000]: (relname(V_155, V_1001) | ~accessible_world(V_1000, V_155) | ~accessible_world(skc15, V_1000) | ~forename(skc14, V_1001)))). % 12.35/4.22 tff(c_4819, plain, (![V_95, V_1005, V_1004]: (unisex(V_95, V_1005) | ~accessible_world(V_1004, V_95) | ~accessible_world(skc24, V_1004) | ~abstraction(skc14, V_1005)))). % 12.35/4.22 tff(c_4882, plain, (![V_83, V_1022, V_1021]: (thing(V_83, V_1022) | ~accessible_world(V_1021, V_83) | ~accessible_world(skc15, V_1021) | ~eventuality(skc14, V_1022)))). % 12.35/4.22 tff(c_4583, plain, (![V_95, V_968, V_967]: (unisex(V_95, V_968) | ~accessible_world(V_967, V_95) | ~accessible_world(skc15, V_967) | ~eventuality(skc14, V_968)))). % 12.35/4.22 tff(c_4968, plain, (![V_95, V_1038, V_1037]: (unisex(V_95, V_1038) | ~accessible_world(V_1037, V_95) | ~accessible_world(skc24, V_1037) | ~eventuality(skc14, V_1038)))). % 12.35/4.22 tff(c_4890, plain, (![V_89, V_1024, V_1023]: (specific(V_89, V_1024) | ~accessible_world(V_1023, V_89) | ~accessible_world(skc24, V_1023) | ~eventuality(skc14, V_1024)))). % 12.35/4.22 tff(c_4503, plain, (![V_80, V_950, V_949]: (eventuality(V_80, V_950) | ~accessible_world(V_949, V_80) | ~accessible_world(skc15, V_949) | ~event(skc14, V_950)))). % 12.35/4.22 tff(c_4906, plain, (![V_113, V_1028, V_1027]: (nonhuman(V_113, V_1028) | ~accessible_world(V_1027, V_113) | ~accessible_world(skc24, V_1027) | ~abstraction(skc14, V_1028)))). % 12.35/4.22 tff(c_4795, plain, (![V_83, V_999, V_998]: (thing(V_83, V_999) | ~accessible_world(V_998, V_83) | ~accessible_world(skc15, V_998) | ~entity(skc14, V_999)))). % 12.35/4.22 tff(c_3916, plain, (![V_164, U_866, V_865]: (agent(V_164, skf1(U_866), U_866) | ~accessible_world(V_865, V_164) | ~accessible_world(skc24, V_865) | ~man(skc24, U_866)))). % 12.35/4.22 tff(c_4858, plain, (![V_95, V_1016, V_1015]: (unisex(V_95, V_1016) | ~accessible_world(V_1015, V_95) | ~accessible_world(skc15, V_1015) | ~abstraction(skc14, V_1016)))). % 12.35/4.22 tff(c_4513, plain, (![V_113, V_952, V_951]: (nonhuman(V_113, V_952) | ~accessible_world(V_951, V_113) | ~accessible_world(skc15, V_951) | ~abstraction(skc14, V_952)))). % 12.35/4.22 tff(c_4554, plain, (![V_83, V_960, V_959]: (thing(V_83, V_960) | ~accessible_world(V_959, V_83) | ~accessible_world(skc24, V_959) | ~entity(skc14, V_960)))). % 12.35/4.22 tff(c_4898, plain, (![V_83, V_1026, V_1025]: (thing(V_83, V_1026) | ~accessible_world(V_1025, V_83) | ~accessible_world(skc15, V_1025) | ~abstraction(skc14, V_1026)))). % 12.35/4.22 tff(c_4959, plain, (![V_116, V_1036, V_1035]: (general(V_116, V_1036) | ~accessible_world(V_1035, V_116) | ~accessible_world(skc15, V_1035) | ~abstraction(skc14, V_1036)))). % 12.35/4.22 tff(c_4640, plain, (![V_89, V_981, V_980]: (specific(V_89, V_981) | ~accessible_world(V_980, V_89) | ~accessible_world(skc24, V_980) | ~entity(skc14, V_981)))). % 12.35/4.22 tff(c_4874, plain, (![V_107, V_1020, V_1019]: (relation(V_107, V_1020) | ~accessible_world(V_1019, V_107) | ~accessible_world(skc15, V_1019) | ~proposition(skc14, V_1020)))). % 12.35/4.22 tff(c_4625, plain, (![V_134, V_977, V_976]: (existent(V_134, V_977) | ~accessible_world(V_976, V_134) | ~accessible_world(skc24, V_976) | ~entity(skc14, V_977)))). % 12.35/4.22 tff(c_6205, plain, (~agent(skc14, skc25, skc18))). % 12.35/4.22 tff(c_2964, plain, (![V_131, V_782]: (entity(V_131, skc27) | ~accessible_world(V_782, V_131) | ~accessible_world(skc15, V_782)))). % 12.35/4.22 tff(c_3019, plain, (![V_131, V_792]: (entity(V_131, skc18) | ~accessible_world(V_792, V_131) | ~accessible_world(skc24, V_792)))). % 12.35/4.22 tff(c_2948, plain, (![V_131, V_780]: (entity(V_131, skc18) | ~accessible_world(V_780, V_131) | ~accessible_world(skc15, V_780)))). % 12.35/4.22 tff(c_3011, plain, (![V_131, V_791]: (entity(V_131, skc22) | ~accessible_world(V_791, V_131) | ~accessible_world(skc15, V_791)))). % 12.35/4.22 tff(c_2956, plain, (![V_131, V_781]: (entity(V_131, skc27) | ~accessible_world(V_781, V_131) | ~accessible_world(skc24, V_781)))). % 12.35/4.22 tff(c_2972, plain, (![V_131, V_783]: (entity(V_131, skc22) | ~accessible_world(V_783, V_131) | ~accessible_world(skc24, V_783)))). % 12.35/4.22 tff(c_6149, plain, (![U_1171]: (~accessible_world(skc15, U_1171) | ~entity(U_1171, skc17)))). % 12.35/4.22 tff(c_5294, plain, (![U_41, V_42]: (~accessible_world(skc15, U_41) | ~eventuality(skc14, V_42) | ~entity(U_41, V_42)))). % 12.35/4.22 tff(c_6129, plain, (~agent(skc14, skc16, skc27))). % 12.35/4.22 tff(c_5329, plain, (![U_3, V_4]: (~accessible_world(skc24, U_3) | ~entity(skc14, V_4) | ~event(U_3, V_4)))). % 12.35/4.22 tff(c_5172, plain, (![V_1061, V_1062]: (abstraction(V_1061, V_1062) | ~accessible_world(skc24, V_1061) | ~forename(skc14, V_1062)))). % 12.35/4.22 tff(c_5026, plain, (![U_3, V_4]: (~accessible_world(skc15, U_3) | ~abstraction(skc14, V_4) | ~event(U_3, V_4)))). % 12.35/4.22 tff(c_5128, plain, (![V_1053, V_1054]: (abstraction(V_1053, V_1054) | ~accessible_world(skc15, V_1053) | ~forename(skc14, V_1054)))). % 12.35/4.22 tff(c_6042, plain, (![U_1158]: (~accessible_world(skc24, U_1158) | ~entity(U_1158, skc17)))). % 12.35/4.22 tff(c_5377, plain, (![U_23, V_24]: (~accessible_world(skc15, U_23) | ~entity(skc14, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.22 tff(c_5595, plain, (![U_41, V_42]: (~accessible_world(skc24, U_41) | ~eventuality(skc14, V_42) | ~entity(U_41, V_42)))). % 12.35/4.22 tff(c_5243, plain, (![U_23, V_24]: (~accessible_world(skc24, U_23) | ~eventuality(skc14, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.22 tff(c_5764, plain, (![U_23, V_24]: (~accessible_world(skc24, U_23) | ~entity(skc14, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.22 tff(c_5616, plain, (![U_23, V_24]: (~accessible_world(skc15, U_23) | ~eventuality(skc14, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.22 tff(c_5742, plain, (![U_3, V_4]: (~accessible_world(skc24, U_3) | ~abstraction(skc14, V_4) | ~event(U_3, V_4)))). % 12.35/4.22 tff(c_5566, plain, (![U_3, V_4]: (~accessible_world(skc15, U_3) | ~entity(skc14, V_4) | ~event(U_3, V_4)))). % 12.35/4.22 tff(c_1936, plain, (![V_622, V_592]: (human(V_622, skc27) | ~accessible_world(V_592, V_622) | ~accessible_world(skc14, V_592)))). % 12.35/4.22 tff(c_4584, plain, (![V_967, V_968]: (~male(V_967, V_968) | ~accessible_world(skc15, V_967) | ~eventuality(skc14, V_968)))). % 12.35/4.22 tff(c_4514, plain, (![V_951, V_952]: (~human(V_951, V_952) | ~accessible_world(skc15, V_951) | ~abstraction(skc14, V_952)))). % 12.35/4.22 tff(c_4501, plain, (![V_949, V_950]: (~entity(V_949, V_950) | ~accessible_world(skc15, V_949) | ~event(skc14, V_950)))). % 12.35/4.22 tff(c_2347, plain, (![V_179, V_728]: (be(V_179, skc17, skc18, skc18) | ~accessible_world(V_728, V_179) | ~accessible_world(skc14, V_728)))). % 12.35/4.23 tff(c_4730, plain, (![V_986, V_987]: (~abstraction(V_986, V_987) | ~accessible_world(skc24, V_986) | ~event(skc14, V_987)))). % 12.35/4.23 tff(c_1977, plain, (![V_627, V_591]: (animate(V_627, skc22) | ~accessible_world(V_591, V_627) | ~accessible_world(skc14, V_591)))). % 12.35/4.23 tff(c_4836, plain, (![V_1008, V_1009]: (abstraction(V_1008, V_1009) | ~accessible_world(skc24, V_1008) | ~proposition(skc14, V_1009)))). % 12.35/4.23 tff(c_4641, plain, (![V_980, V_981]: (~general(V_980, V_981) | ~accessible_world(skc24, V_980) | ~entity(skc14, V_981)))). % 12.35/4.23 tff(c_4427, plain, (![V_947, V_948]: (~eventuality(V_947, V_948) | ~accessible_world(skc24, V_947) | ~abstraction(skc14, V_948)))). % 12.35/4.23 tff(c_5713, plain, (~event(skc14, skc15))). % 12.35/4.23 tff(c_2045, plain, (![V_131, V_637]: (entity(V_131, skc22) | ~accessible_world(V_637, V_131) | ~accessible_world(skc14, V_637)))). % 12.35/4.23 tff(c_5703, plain, (~event(skc14, skc24))). % 12.35/4.23 tff(c_5695, plain, (~event(skc14, skc26))). % 12.35/4.23 tff(c_2338, plain, (![V_168, V_723]: (theme(V_168, skc25, skc24) | ~accessible_world(V_723, V_168) | ~accessible_world(skc14, V_723)))). % 12.35/4.23 tff(c_5694, plain, (~event(skc14, skc21))). % 12.35/4.23 tff(c_5693, plain, (~event(skc14, skc19))). % 12.35/4.23 tff(c_4502, plain, (![V_949, V_950]: (~abstraction(V_949, V_950) | ~accessible_world(skc15, V_949) | ~event(skc14, V_950)))). % 12.35/4.23 tff(c_2285, plain, (![V_164, V_712]: (agent(V_164, skc23, skc22) | ~accessible_world(V_712, V_164) | ~accessible_world(skc15, V_712)))). % 12.35/4.23 tff(c_4755, plain, (![V_990, V_991]: (entity(V_990, V_991) | ~accessible_world(skc24, V_990) | ~human_person(skc14, V_991)))). % 12.35/4.23 tff(c_4608, plain, (![V_974, V_975]: (~general(V_974, V_975) | ~accessible_world(skc15, V_974) | ~eventuality(skc14, V_975)))). % 12.35/4.23 tff(c_4828, plain, (![V_1006, V_1007]: (~existent(V_1006, V_1007) | ~accessible_world(skc24, V_1006) | ~eventuality(skc14, V_1007)))). % 12.35/4.23 tff(c_2037, plain, (![V_143, V_636]: (human(V_143, skc22) | ~accessible_world(V_636, V_143) | ~accessible_world(skc14, V_636)))). % 12.35/4.23 tff(c_4539, plain, (![V_955, V_956]: (~eventuality(V_955, V_956) | ~accessible_world(skc15, V_955) | ~entity(skc14, V_956)))). % 12.35/4.23 tff(c_4778, plain, (![V_994, V_995]: (entity(V_994, V_995) | ~accessible_world(skc15, V_994) | ~human_person(skc14, V_995)))). % 12.35/4.23 tff(c_4426, plain, (![V_947, V_948]: (~entity(V_947, V_948) | ~accessible_world(skc24, V_947) | ~abstraction(skc14, V_948)))). % 12.35/4.23 tff(c_2292, plain, (![V_172, V_713]: (of(V_172, skc21, skc22) | ~accessible_world(V_713, V_172) | ~accessible_world(skc14, V_713)))). % 12.35/4.23 tff(c_3486, plain, (![V_86, V_838]: (singleton(V_86, V_838) | ~accessible_world(skc24, V_86) | ~eventuality(skc14, V_838)))). % 12.35/4.23 tff(c_4729, plain, (![V_986, V_987]: (~entity(V_986, V_987) | ~accessible_world(skc24, V_986) | ~event(skc14, V_987)))). % 12.35/4.23 tff(c_4547, plain, (![V_957, V_958]: (~general(V_957, V_958) | ~accessible_world(skc15, V_957) | ~entity(skc14, V_958)))). % 12.35/4.23 tff(c_2757, plain, (![V_137, V_763]: (impartial(V_137, V_763) | ~accessible_world(skc24, V_137) | ~human_person(skc14, V_763)))). % 12.35/4.23 tff(c_4796, plain, (![V_998, V_999]: (singleton(V_998, V_999) | ~accessible_world(skc15, V_998) | ~entity(skc14, V_999)))). % 12.35/4.23 tff(c_4780, plain, (![V_994, V_995]: (impartial(V_994, V_995) | ~accessible_world(skc15, V_994) | ~human_person(skc14, V_995)))). % 12.35/4.23 tff(c_1935, plain, (![V_622, V_593]: (human(V_622, skc18) | ~accessible_world(V_593, V_622) | ~accessible_world(skc14, V_593)))). % 12.35/4.23 tff(c_2271, plain, (![V_164, V_710]: (agent(V_164, skc25, skc27) | ~accessible_world(V_710, V_164) | ~accessible_world(skc14, V_710)))). % 12.35/4.23 tff(c_4626, plain, (![V_976, V_977]: (~eventuality(V_976, V_977) | ~accessible_world(skc24, V_976) | ~entity(skc14, V_977)))). % 12.35/4.23 tff(c_1978, plain, (![V_627, V_593]: (animate(V_627, skc18) | ~accessible_world(V_593, V_627) | ~accessible_world(skc14, V_593)))). % 12.35/4.23 tff(c_4788, plain, (![V_996, V_997]: (~existent(V_996, V_997) | ~accessible_world(skc15, V_996) | ~eventuality(skc14, V_997)))). % 12.35/4.23 tff(c_3156, plain, (![V_86, V_810]: (singleton(V_86, V_810) | ~accessible_world(skc24, V_86) | ~entity(skc14, V_810)))). % 12.35/4.23 tff(c_4875, plain, (![V_1019, V_1020]: (abstraction(V_1019, V_1020) | ~accessible_world(skc15, V_1019) | ~proposition(skc14, V_1020)))). % 12.35/4.23 tff(c_4907, plain, (![V_1027, V_1028]: (~human(V_1027, V_1028) | ~accessible_world(skc24, V_1027) | ~abstraction(skc14, V_1028)))). % 12.35/4.23 tff(c_4891, plain, (![V_1023, V_1024]: (~general(V_1023, V_1024) | ~accessible_world(skc24, V_1023) | ~eventuality(skc14, V_1024)))). % 12.35/4.23 tff(c_4859, plain, (![V_1015, V_1016]: (~male(V_1015, V_1016) | ~accessible_world(skc15, V_1015) | ~abstraction(skc14, V_1016)))). % 12.35/4.23 tff(c_2753, plain, (![V_140, V_762]: (living(V_140, V_762) | ~accessible_world(skc15, V_140) | ~human_person(skc14, V_762)))). % 12.35/4.23 tff(c_2322, plain, (![V_74, V_720, V_719]: (smoke(V_74, skf1(V_720)) | ~accessible_world(V_719, V_74) | ~accessible_world(skc24, V_719)))). % 12.35/4.23 tff(c_3004, plain, (![V_86, V_790]: (singleton(V_86, V_790) | ~accessible_world(skc24, V_86) | ~abstraction(skc14, V_790)))). % 12.35/4.23 tff(c_1587, plain, (![V_131, V_565]: (entity(V_131, skc18) | ~accessible_world(V_565, V_131) | ~accessible_world(skc14, V_565)))). % 12.35/4.23 tff(c_4867, plain, (![V_1017, V_1018]: (relation(V_1017, V_1018) | ~accessible_world(skc24, V_1017) | ~forename(skc14, V_1018)))). % 12.35/4.23 tff(c_4820, plain, (![V_1004, V_1005]: (~male(V_1004, V_1005) | ~accessible_world(skc24, V_1004) | ~abstraction(skc14, V_1005)))). % 12.35/4.23 tff(c_1979, plain, (![V_627, V_592]: (animate(V_627, skc27) | ~accessible_world(V_592, V_627) | ~accessible_world(skc14, V_592)))). % 12.35/4.23 tff(c_4883, plain, (![V_1021, V_1022]: (singleton(V_1021, V_1022) | ~accessible_world(skc15, V_1021) | ~eventuality(skc14, V_1022)))). % 12.35/4.23 tff(c_4804, plain, (![V_1000, V_1001]: (relation(V_1000, V_1001) | ~accessible_world(skc15, V_1000) | ~forename(skc14, V_1001)))). % 12.35/4.23 tff(c_2327, plain, (![V_168, V_721]: (theme(V_168, skc16, skc15) | ~accessible_world(V_721, V_168) | ~accessible_world(skc14, V_721)))). % 12.35/4.23 tff(c_1878, plain, (![V_131, V_615]: (entity(V_131, skc27) | ~accessible_world(V_615, V_131) | ~accessible_world(skc14, V_615)))). % 12.35/4.23 tff(c_2652, plain, (![V_140, V_754]: (living(V_140, V_754) | ~accessible_world(skc24, V_140) | ~human_person(skc14, V_754)))). % 12.35/4.23 tff(c_4960, plain, (![V_1035, V_1036]: (~entity(V_1035, V_1036) | ~accessible_world(skc15, V_1035) | ~abstraction(skc14, V_1036)))). % 12.35/4.23 tff(c_4961, plain, (![V_1035, V_1036]: (~eventuality(V_1035, V_1036) | ~accessible_world(skc15, V_1035) | ~abstraction(skc14, V_1036)))). % 12.35/4.23 tff(c_4969, plain, (![V_1037, V_1038]: (~male(V_1037, V_1038) | ~accessible_world(skc24, V_1037) | ~eventuality(skc14, V_1038)))). % 12.35/4.23 tff(c_4899, plain, (![V_1025, V_1026]: (singleton(V_1025, V_1026) | ~accessible_world(skc15, V_1025) | ~abstraction(skc14, V_1026)))). % 12.35/4.23 tff(c_2895, plain, (![V_95, V_777]: (unisex(V_95, V_777) | ~accessible_world(skc24, V_95) | ~eventuality(skc14, V_777)))). % 12.35/4.23 tff(c_3708, plain, (![V_116, V_858]: (general(V_116, V_858) | ~accessible_world(skc15, V_116) | ~abstraction(skc14, V_858)))). % 12.35/4.23 tff(c_1497, plain, (![V_149, V_548]: (male(V_149, skc22) | ~accessible_world(V_548, V_149) | ~accessible_world(skc14, V_548)))). % 12.35/4.23 tff(c_2278, plain, (![V_164, V_711]: (agent(V_164, skc16, skc18) | ~accessible_world(V_711, V_164) | ~accessible_world(skc14, V_711)))). % 12.35/4.23 tff(c_2117, plain, (![V_653, V_583]: (human_person(V_653, skc18) | ~accessible_world(V_583, V_653) | ~accessible_world(skc14, V_583)))). % 12.35/4.23 tff(c_2748, plain, (![V_113, V_761]: (nonhuman(V_113, V_761) | ~accessible_world(skc24, V_113) | ~abstraction(skc14, V_761)))). % 12.35/4.23 tff(c_2987, plain, (![V_83, V_787]: (thing(V_83, V_787) | ~accessible_world(skc15, V_83) | ~abstraction(skc14, V_787)))). % 12.35/4.23 tff(c_2410, plain, (![V_89, V_740]: (specific(V_89, V_740) | ~accessible_world(skc24, V_89) | ~eventuality(skc14, V_740)))). % 12.35/4.23 tff(c_3469, plain, (![V_83, V_835]: (thing(V_83, V_835) | ~accessible_world(skc15, V_83) | ~eventuality(skc14, V_835)))). % 12.35/4.23 tff(c_3246, plain, (![V_107, V_816]: (relation(V_107, V_816) | ~accessible_world(skc15, V_107) | ~proposition(skc14, V_816)))). % 12.35/4.23 tff(c_2371, plain, (![V_155, V_733]: (relname(V_155, V_733) | ~accessible_world(skc24, V_155) | ~forename(skc14, V_733)))). % 12.35/4.23 tff(c_2815, plain, (![V_95, V_769]: (unisex(V_95, V_769) | ~accessible_world(skc15, V_95) | ~abstraction(skc14, V_769)))). % 12.35/4.23 tff(c_2315, plain, (![V_77, V_718, V_717]: (event(V_77, skf1(V_718)) | ~accessible_world(V_717, V_77) | ~accessible_world(skc24, V_717)))). % 12.35/4.23 tff(c_1381, plain, (![V_77, V_525]: (event(V_77, skc17) | ~accessible_world(V_525, V_77) | ~accessible_world(skc14, V_525)))). % 12.35/4.23 tff(c_3254, plain, (![V_107, V_817]: (relation(V_107, V_817) | ~accessible_world(skc24, V_107) | ~proposition(skc14, V_817)))). % 12.35/4.23 tff(c_3082, plain, (![V_92, V_799]: (nonexistent(V_92, V_799) | ~accessible_world(skc24, V_92) | ~eventuality(skc14, V_799)))). % 12.35/4.23 tff(c_2823, plain, (![V_95, V_770]: (unisex(V_95, V_770) | ~accessible_world(skc24, V_95) | ~abstraction(skc14, V_770)))). % 12.35/4.23 tff(c_2995, plain, (![V_83, V_788]: (thing(V_83, V_788) | ~accessible_world(skc24, V_83) | ~abstraction(skc14, V_788)))). % 12.35/4.23 tff(c_2363, plain, (![V_155, V_732]: (relname(V_155, V_732) | ~accessible_world(skc15, V_155) | ~forename(skc14, V_732)))). % 12.35/4.23 tff(c_3139, plain, (![V_83, V_807]: (thing(V_83, V_807) | ~accessible_world(skc15, V_83) | ~entity(skc14, V_807)))). % 12.35/4.23 tff(c_3074, plain, (![V_92, V_798]: (nonexistent(V_92, V_798) | ~accessible_world(skc15, V_92) | ~eventuality(skc14, V_798)))). % 12.35/4.23 tff(c_2601, plain, (![V_128, V_751]: (organism(V_128, V_751) | ~accessible_world(skc15, V_128) | ~human_person(skc14, V_751)))). % 12.35/4.23 tff(c_2264, plain, (![V_172, V_709]: (of(V_172, skc26, skc27) | ~accessible_world(V_709, V_172) | ~accessible_world(skc14, V_709)))). % 12.35/4.23 tff(c_2617, plain, (![V_128, V_752]: (organism(V_128, V_752) | ~accessible_world(skc24, V_128) | ~human_person(skc14, V_752)))). % 12.35/4.23 tff(c_2118, plain, (![V_653, V_584]: (human_person(V_653, skc27) | ~accessible_world(V_584, V_653) | ~accessible_world(skc14, V_584)))). % 12.35/4.23 tff(c_3562, plain, (![V_80, V_845]: (eventuality(V_80, V_845) | ~accessible_world(skc24, V_80) | ~event(skc14, V_845)))). % 12.35/4.23 tff(c_1509, plain, (![V_149, V_549]: (male(V_149, skc27) | ~accessible_world(V_549, V_149) | ~accessible_world(skc14, V_549)))). % 12.35/4.23 tff(c_1893, plain, (![V_616, V_578]: (forename(V_616, skc26) | ~accessible_world(V_578, V_616) | ~accessible_world(skc14, V_578)))). % 12.35/4.23 tff(c_3323, plain, (![V_89, V_824]: (specific(V_89, V_824) | ~accessible_world(skc24, V_89) | ~entity(skc14, V_824)))). % 12.35/4.23 tff(c_2119, plain, (![V_653, V_585]: (human_person(V_653, skc22) | ~accessible_world(V_585, V_653) | ~accessible_world(skc14, V_585)))). % 12.35/4.23 tff(c_3592, plain, (![V_134, V_850]: (existent(V_134, V_850) | ~accessible_world(skc24, V_134) | ~entity(skc14, V_850)))). % 12.35/4.23 tff(c_2402, plain, (![V_89, V_739]: (specific(V_89, V_739) | ~accessible_world(skc15, V_89) | ~eventuality(skc14, V_739)))). % 12.35/4.23 tff(c_2303, plain, (![V_98, V_716, V_715]: (present(V_98, skf1(V_716)) | ~accessible_world(V_715, V_98) | ~accessible_world(skc24, V_715)))). % 12.35/4.23 tff(c_3477, plain, (![V_83, V_836]: (thing(V_83, V_836) | ~accessible_world(skc24, V_83) | ~eventuality(skc14, V_836)))). % 12.35/4.23 tff(c_2887, plain, (![V_95, V_776]: (unisex(V_95, V_776) | ~accessible_world(skc15, V_95) | ~eventuality(skc14, V_776)))). % 12.35/4.23 tff(c_1448, plain, (![V_80, V_538]: (eventuality(V_80, skc17) | ~accessible_world(V_538, V_80) | ~accessible_world(skc14, V_538)))). % 12.35/4.23 tff(c_4280, plain, (![V_158, V_577]: (vincent_forename(V_158, skc19) | ~accessible_world(V_577, V_158) | ~accessible_world(skc14, V_577)))). % 12.35/4.23 tff(c_1521, plain, (![V_149, V_550]: (male(V_149, skc18) | ~accessible_world(V_550, V_149) | ~accessible_world(skc14, V_550)))). % 12.35/4.24 tff(c_3147, plain, (![V_83, V_808]: (thing(V_83, V_808) | ~accessible_world(skc24, V_83) | ~entity(skc14, V_808)))). % 12.35/4.24 tff(c_3315, plain, (![V_89, V_823]: (specific(V_89, V_823) | ~accessible_world(skc15, V_89) | ~entity(skc14, V_823)))). % 12.35/4.24 tff(c_3580, plain, (![V_134, V_849]: (existent(V_134, V_849) | ~accessible_world(skc15, V_134) | ~entity(skc14, V_849)))). % 12.35/4.24 tff(c_2334, plain, (![V_172, V_722]: (of(V_172, skc19, skc18) | ~accessible_world(V_722, V_172) | ~accessible_world(skc14, V_722)))). % 12.35/4.24 tff(c_2740, plain, (![V_113, V_760]: (nonhuman(V_113, V_760) | ~accessible_world(skc15, V_113) | ~abstraction(skc14, V_760)))). % 12.35/4.24 tff(c_3529, plain, (![V_80, V_844]: (eventuality(V_80, V_844) | ~accessible_world(skc15, V_80) | ~event(skc14, V_844)))). % 12.35/4.24 tff(c_3688, plain, (![V_116, V_857]: (general(V_116, V_857) | ~accessible_world(skc24, V_116) | ~abstraction(skc14, V_857)))). % 12.35/4.24 tff(c_1739, plain, (![V_122, V_585]: (man(V_122, skc22) | ~accessible_world(V_585, V_122) | ~accessible_world(skc14, V_585)))). % 12.35/4.24 tff(c_1752, plain, (![V_101, V_589]: (think_believe_consider(V_101, skc16) | ~accessible_world(V_589, V_101) | ~accessible_world(skc14, V_589)))). % 12.35/4.24 tff(c_2028, plain, (![V_632, V_232, U_231]: (relation(V_632, V_232) | ~accessible_world(U_231, V_632) | ~forename(U_231, V_232)))). % 12.35/4.24 tff(c_2225, plain, (![W_687]: (skc19=W_687 | ~forename(skc14, W_687) | ~of(skc14, W_687, skc18)))). % 12.35/4.24 tff(c_2063, plain, (![V_98, V_641]: (present(V_98, skc16) | ~accessible_world(V_641, V_98) | ~accessible_world(skc14, V_641)))). % 12.35/4.24 tff(c_1905, plain, (![V_152, V_619]: (forename(V_152, skc21) | ~accessible_world(V_619, V_152) | ~accessible_world(skc14, V_619)))). % 12.35/4.24 tff(c_1715, plain, (![V_122, V_583]: (man(V_122, skc18) | ~accessible_world(V_583, V_122) | ~accessible_world(skc14, V_583)))). % 12.35/4.24 tff(c_1689, plain, (![V_158, V_578]: (vincent_forename(V_158, skc26) | ~accessible_world(V_578, V_158) | ~accessible_world(skc14, V_578)))). % 12.35/4.24 tff(c_1443, plain, (![V_104, V_537]: (proposition(V_104, skc15) | ~accessible_world(V_537, V_104) | ~accessible_world(skc14, V_537)))). % 12.35/4.24 tff(c_1531, plain, (![V_551, V_6, U_5]: (singleton(V_551, V_6) | ~accessible_world(U_5, V_551) | ~eventuality(U_5, V_6)))). % 12.35/4.24 tff(c_4288, plain, (![V_574]: (vincent_forename(V_574, skc19) | ~accessible_world(skc14, V_574)))). % 12.35/4.24 tff(c_4292, plain, (vincent_forename(skc14, skc19))). % 12.35/4.24 tff(c_4278, plain, (skc20=skc19)). % 12.35/4.24 tff(c_1569, plain, (![V_74, V_560]: (smoke(V_74, skc23) | ~accessible_world(V_560, V_74) | ~accessible_world(skc15, V_560)))). % 12.35/4.24 tff(c_2241, plain, (![W_698, V_696, Y_697, U_196]: (W_698=V_696 | ~agent(skc24, Y_697, U_196) | ~theme(skc24, Y_697, W_698) | ~think_believe_consider(skc24, Y_697) | ~think_believe_consider(skc24, skf1(U_196)) | ~theme(skc24, skf1(U_196), V_696) | ~proposition(skc24, W_698) | ~proposition(skc24, V_696) | ~man(skc24, U_196)))). % 12.35/4.24 tff(c_2228, plain, (![W_687]: (skc26=W_687 | ~forename(skc14, W_687) | ~of(skc14, W_687, skc27)))). % 12.35/4.24 tff(c_2219, plain, (![W_687]: (skc21=W_687 | ~forename(skc14, W_687) | ~of(skc14, W_687, skc22)))). % 12.35/4.24 tff(c_2071, plain, (![V_98, V_643]: (present(V_98, skc23) | ~accessible_world(V_643, V_98) | ~accessible_world(skc15, V_643)))). % 12.35/4.24 tff(c_2145, plain, (![V_161, V_660]: (jules_forename(V_161, skc19) | ~accessible_world(V_660, V_161) | ~accessible_world(skc14, V_660)))). % 12.35/4.24 tff(c_2094, plain, (![V_649, V_34, U_33]: (impartial(V_649, V_34) | ~accessible_world(U_33, V_649) | ~human_person(U_33, V_34)))). % 12.35/4.24 tff(c_1362, plain, (![V_77, V_519]: (event(V_77, skc16) | ~accessible_world(V_519, V_77) | ~accessible_world(skc14, V_519)))). % 12.35/4.24 tff(c_1435, plain, (![V_104, V_536]: (proposition(V_104, skc24) | ~accessible_world(V_536, V_104) | ~accessible_world(skc14, V_536)))). % 12.35/4.24 tff(c_4145, plain, (~think_believe_consider(skc15, skc23))). % 12.35/4.24 tff(c_1358, plain, (![V_140, V_518, U_517]: (living(V_140, V_518) | ~accessible_world(U_517, V_140) | ~human_person(U_517, V_518)))). % 12.35/4.24 tff(c_1756, plain, (![V_101, V_590]: (think_believe_consider(V_101, skc25) | ~accessible_world(V_590, V_101) | ~accessible_world(skc14, V_590)))). % 12.35/4.24 tff(c_1727, plain, (![V_122, V_584]: (man(V_122, skc27) | ~accessible_world(V_584, V_122) | ~accessible_world(skc14, V_584)))). % 12.35/4.24 tff(c_1334, plain, (![V_119, V_509]: (state(V_119, skc17) | ~accessible_world(V_509, V_119) | ~accessible_world(skc14, V_509)))). % 12.35/4.24 tff(c_1913, plain, (![V_152, V_620]: (forename(V_152, skc19) | ~accessible_world(V_620, V_152) | ~accessible_world(skc14, V_620)))). % 12.35/4.24 tff(c_1370, plain, (![V_77, V_521]: (event(V_77, skc23) | ~accessible_world(V_521, V_77) | ~accessible_world(skc15, V_521)))). % 12.35/4.24 tff(c_4061, plain, (![V_884]: (skc15=V_884 | ~theme(skc14, skc16, V_884) | ~proposition(skc14, V_884)))). % 12.35/4.24 tff(c_4012, plain, (![V_871]: (skc24=V_871 | ~theme(skc14, skc25, V_871) | ~proposition(skc14, V_871)))). % 12.35/4.24 tff(c_1366, plain, (![V_77, V_520]: (event(V_77, skc25) | ~accessible_world(V_520, V_77) | ~accessible_world(skc14, V_520)))). % 12.35/4.24 tff(c_2245, plain, (![W_698, V_696, Y_697]: (W_698=V_696 | ~agent(skc14, Y_697, skc18) | ~theme(skc14, Y_697, W_698) | ~think_believe_consider(skc14, Y_697) | ~theme(skc14, skc16, V_696) | ~proposition(skc14, W_698) | ~proposition(skc14, V_696)))). % 12.35/4.24 tff(c_2067, plain, (![V_98, V_642]: (present(V_98, skc25) | ~accessible_world(V_642, V_98) | ~accessible_world(skc14, V_642)))). % 12.35/4.24 tff(c_1532, plain, (![V_551, V_38, U_37]: (singleton(V_551, V_38) | ~accessible_world(U_37, V_551) | ~entity(U_37, V_38)))). % 12.35/4.24 tff(c_4027, plain, (~accessible_world(skc14, skc14))). % 12.35/4.24 tff(c_2153, plain, (![V_161, V_661]: (jules_forename(V_161, skc21) | ~accessible_world(V_661, V_161) | ~accessible_world(skc14, V_661)))). % 12.35/4.24 tff(c_1533, plain, (![V_551, V_20, U_19]: (singleton(V_551, V_20) | ~accessible_world(U_19, V_551) | ~abstraction(U_19, V_20)))). % 12.35/4.24 tff(c_2248, plain, (![W_698, V_696, Y_697]: (W_698=V_696 | ~agent(skc14, Y_697, skc27) | ~theme(skc14, Y_697, W_698) | ~think_believe_consider(skc14, Y_697) | ~theme(skc14, skc25, V_696) | ~proposition(skc14, W_698) | ~proposition(skc14, V_696)))). % 12.35/4.24 tff(c_3989, plain, (~abstraction(skc14, skc23))). % 12.35/4.24 tff(c_3764, plain, (![V_4]: (~abstraction(skc14, V_4) | ~event(skc15, V_4)))). % 12.35/4.24 tff(c_3952, plain, (![V_195]: (~abstraction(skc14, skf1(V_195))))). % 12.35/4.24 tff(c_3845, plain, (![V_4]: (~abstraction(skc14, V_4) | ~event(skc24, V_4)))). % 12.35/4.24 tff(c_2195, plain, (![V_673, U_196]: (agent(V_673, skf1(U_196), U_196) | ~accessible_world(skc24, V_673) | ~man(skc24, U_196)))). % 12.35/4.24 tff(c_3689, plain, (![V_857]: (~entity(skc24, V_857) | ~abstraction(skc14, V_857)))). % 12.35/4.24 tff(c_3690, plain, (![V_857]: (~eventuality(skc24, V_857) | ~abstraction(skc14, V_857)))). % 12.35/4.24 tff(c_3709, plain, (![V_858]: (~entity(skc15, V_858) | ~abstraction(skc14, V_858)))). % 12.35/4.24 tff(c_3710, plain, (![V_858]: (~eventuality(skc15, V_858) | ~abstraction(skc14, V_858)))). % 12.35/4.24 tff(c_3746, plain, (![V_195]: (~entity(skc14, skf1(V_195))))). % 12.35/4.24 tff(c_3627, plain, (![V_4]: (~entity(skc14, V_4) | ~event(skc24, V_4)))). % 12.35/4.24 tff(c_3669, plain, (![V_855]: (general(skc15, V_855) | ~abstraction(skc14, V_855)))). % 12.35/4.24 tff(c_3670, plain, (![V_855]: (general(skc24, V_855) | ~abstraction(skc14, V_855)))). % 12.35/4.24 tff(c_3663, plain, (~entity(skc14, skc23))). % 12.35/4.24 tff(c_1844, plain, (![V_605, V_24, U_23]: (general(V_605, V_24) | ~accessible_world(U_23, V_605) | ~abstraction(U_23, V_24)))). % 12.35/4.24 tff(c_3610, plain, (![V_4]: (~entity(skc14, V_4) | ~event(skc15, V_4)))). % 12.35/4.24 tff(c_3593, plain, (![V_850]: (~eventuality(skc24, V_850) | ~entity(skc14, V_850)))). % 12.35/4.24 tff(c_3581, plain, (![V_849]: (~eventuality(skc15, V_849) | ~entity(skc14, V_849)))). % 12.35/4.24 tff(c_3569, plain, (![V_847]: (existent(skc24, V_847) | ~entity(skc14, V_847)))). % 12.35/4.24 tff(c_3568, plain, (![V_847]: (existent(skc15, V_847) | ~entity(skc14, V_847)))). % 12.35/4.24 tff(c_1580, plain, (![V_562, V_42, U_41]: (existent(V_562, V_42) | ~accessible_world(U_41, V_562) | ~entity(U_41, V_42)))). % 12.35/4.24 tff(c_3496, plain, (![V_842]: (eventuality(skc24, V_842) | ~event(skc14, V_842)))). % 12.35/4.24 tff(c_3495, plain, (![V_842]: (eventuality(skc15, V_842) | ~event(skc14, V_842)))). % 12.35/4.24 tff(c_3489, plain, (~accessible_world(skc24, skc14))). % 12.35/4.24 tff(c_1376, plain, (![V_522, V_4, U_3]: (eventuality(V_522, V_4) | ~accessible_world(U_3, V_522) | ~event(U_3, V_4)))). % 12.35/4.24 tff(c_2965, plain, (![V_782]: (~abstraction(V_782, skc27) | ~accessible_world(skc15, V_782)))). % 12.35/4.24 tff(c_2957, plain, (![V_781]: (~abstraction(V_781, skc27) | ~accessible_world(skc24, V_781)))). % 12.35/4.24 tff(c_3478, plain, (![V_836]: (singleton(skc24, V_836) | ~eventuality(skc14, V_836)))). % 12.35/4.24 tff(c_3470, plain, (![V_835]: (singleton(skc15, V_835) | ~eventuality(skc14, V_835)))). % 12.35/4.24 tff(c_3462, plain, (![V_833]: (thing(skc24, V_833) | ~eventuality(skc14, V_833)))). % 12.35/4.24 tff(c_3461, plain, (![V_833]: (thing(skc15, V_833) | ~eventuality(skc14, V_833)))). % 12.35/4.24 tff(c_1258, plain, (![V_479, V_6, U_5]: (thing(V_479, V_6) | ~accessible_world(U_5, V_479) | ~eventuality(U_5, V_6)))). % 12.35/4.24 tff(c_3012, plain, (![V_791]: (~abstraction(V_791, skc22) | ~accessible_world(skc15, V_791)))). % 12.35/4.24 tff(c_3020, plain, (![V_792]: (~abstraction(V_792, skc18) | ~accessible_world(skc24, V_792)))). % 12.35/4.24 tff(c_2973, plain, (![V_783]: (~abstraction(V_783, skc22) | ~accessible_world(skc24, V_783)))). % 12.35/4.24 tff(c_3336, plain, (![V_24]: (~entity(skc14, V_24) | ~abstraction(skc24, V_24)))). % 12.35/4.24 tff(c_3330, plain, (![V_24]: (~entity(skc14, V_24) | ~abstraction(skc15, V_24)))). % 12.35/4.24 tff(c_3324, plain, (![V_824]: (~general(skc24, V_824) | ~entity(skc14, V_824)))). % 12.35/4.24 tff(c_3316, plain, (![V_823]: (~general(skc15, V_823) | ~entity(skc14, V_823)))). % 12.35/4.24 tff(c_3308, plain, (![V_821]: (specific(skc24, V_821) | ~entity(skc14, V_821)))). % 12.35/4.24 tff(c_3307, plain, (![V_821]: (specific(skc15, V_821) | ~entity(skc14, V_821)))). % 12.35/4.24 tff(c_1486, plain, (![V_545, V_40, U_39]: (specific(V_545, V_40) | ~accessible_world(U_39, V_545) | ~entity(U_39, V_40)))). % 12.35/4.24 tff(c_3255, plain, (![V_817]: (abstraction(skc24, V_817) | ~proposition(skc14, V_817)))). % 12.35/4.24 tff(c_3247, plain, (![V_816]: (abstraction(skc15, V_816) | ~proposition(skc14, V_816)))). % 12.35/4.24 tff(c_3239, plain, (![V_814]: (relation(skc24, V_814) | ~proposition(skc14, V_814)))). % 12.35/4.24 tff(c_3238, plain, (![V_814]: (relation(skc15, V_814) | ~proposition(skc14, V_814)))). % 12.35/4.24 tff(c_3231, plain, (~entity(skc24, skc16))). % 12.35/4.24 tff(c_3232, plain, (~entity(skc24, skc25))). % 12.35/4.24 tff(c_2029, plain, (![V_632, V_16, U_15]: (relation(V_632, V_16) | ~accessible_world(U_15, V_632) | ~proposition(U_15, V_16)))). % 12.35/4.24 tff(c_3124, plain, (![V_4]: (~entity(skc24, V_4) | ~event(skc14, V_4)))). % 12.35/4.24 tff(c_3194, plain, (~entity(skc15, skc25))). % 12.35/4.24 tff(c_3193, plain, (~entity(skc15, skc16))). % 12.35/4.24 tff(c_3109, plain, (![V_4]: (~entity(skc15, V_4) | ~event(skc14, V_4)))). % 12.35/4.24 tff(c_3148, plain, (![V_808]: (singleton(skc24, V_808) | ~entity(skc14, V_808)))). % 12.35/4.24 tff(c_3140, plain, (![V_807]: (singleton(skc15, V_807) | ~entity(skc14, V_807)))). % 12.35/4.24 tff(c_3132, plain, (![V_805]: (thing(skc24, V_805) | ~entity(skc14, V_805)))). % 12.35/4.24 tff(c_3131, plain, (![V_805]: (thing(skc15, V_805) | ~entity(skc14, V_805)))). % 12.35/4.24 tff(c_1256, plain, (![V_479, V_38, U_37]: (thing(V_479, V_38) | ~accessible_world(U_37, V_479) | ~entity(U_37, V_38)))). % 12.35/4.24 tff(c_3125, plain, (~entity(skc24, skc17))). % 12.35/4.24 tff(c_3095, plain, (![V_42]: (~eventuality(skc14, V_42) | ~entity(skc24, V_42)))). % 12.35/4.24 tff(c_3110, plain, (~entity(skc15, skc17))). % 12.35/4.24 tff(c_3089, plain, (![V_42]: (~eventuality(skc14, V_42) | ~entity(skc15, V_42)))). % 12.35/4.24 tff(c_3083, plain, (![V_799]: (~existent(skc24, V_799) | ~eventuality(skc14, V_799)))). % 12.35/4.24 tff(c_3075, plain, (![V_798]: (~existent(skc15, V_798) | ~eventuality(skc14, V_798)))). % 12.35/4.25 tff(c_3067, plain, (![V_796]: (nonexistent(skc24, V_796) | ~eventuality(skc14, V_796)))). % 12.35/4.25 tff(c_3066, plain, (![V_796]: (nonexistent(skc15, V_796) | ~eventuality(skc14, V_796)))). % 12.35/4.25 tff(c_3060, plain, (~accessible_world(skc15, skc14))). % 12.35/4.25 tff(c_2075, plain, (![V_644, V_12, U_11]: (nonexistent(V_644, V_12) | ~accessible_world(U_11, V_644) | ~eventuality(U_11, V_12)))). % 12.35/4.25 tff(c_2949, plain, (![V_780]: (~abstraction(V_780, skc18) | ~accessible_world(skc15, V_780)))). % 12.35/4.25 tff(c_2542, plain, (![V_4]: (~abstraction(skc24, V_4) | ~event(skc14, V_4)))). % 12.35/4.25 tff(c_2725, plain, (![V_131]: (entity(V_131, skc18) | ~accessible_world(skc24, V_131)))). % 12.35/4.25 tff(c_2658, plain, (![V_131]: (entity(V_131, skc22) | ~accessible_world(skc15, V_131)))). % 12.35/4.25 tff(c_2996, plain, (![V_788]: (singleton(skc24, V_788) | ~abstraction(skc14, V_788)))). % 12.35/4.25 tff(c_2988, plain, (![V_787]: (singleton(skc15, V_787) | ~abstraction(skc14, V_787)))). % 12.35/4.25 tff(c_2980, plain, (![V_785]: (thing(skc24, V_785) | ~abstraction(skc14, V_785)))). % 12.35/4.25 tff(c_2979, plain, (![V_785]: (thing(skc15, V_785) | ~abstraction(skc14, V_785)))). % 12.35/4.25 tff(c_1257, plain, (![V_479, V_20, U_19]: (thing(V_479, V_20) | ~accessible_world(U_19, V_479) | ~abstraction(U_19, V_20)))). % 12.35/4.25 tff(c_2718, plain, (![V_131]: (entity(V_131, skc22) | ~accessible_world(skc24, V_131)))). % 12.35/4.25 tff(c_2672, plain, (![V_131]: (entity(V_131, skc27) | ~accessible_world(skc15, V_131)))). % 12.35/4.25 tff(c_2732, plain, (![V_131]: (entity(V_131, skc27) | ~accessible_world(skc24, V_131)))). % 12.35/4.25 tff(c_2665, plain, (![V_131]: (entity(V_131, skc18) | ~accessible_world(skc15, V_131)))). % 12.35/4.25 tff(c_2896, plain, (![V_777]: (~male(skc24, V_777) | ~eventuality(skc14, V_777)))). % 12.35/4.25 tff(c_2888, plain, (![V_776]: (~male(skc15, V_776) | ~eventuality(skc14, V_776)))). % 12.35/4.25 tff(c_2880, plain, (![V_774]: (unisex(skc24, V_774) | ~eventuality(skc14, V_774)))). % 12.35/4.25 tff(c_2879, plain, (![V_774]: (unisex(skc15, V_774) | ~eventuality(skc14, V_774)))). % 12.35/4.25 tff(c_1813, plain, (![V_600, V_14, U_13]: (unisex(V_600, V_14) | ~accessible_world(U_13, V_600) | ~eventuality(U_13, V_14)))). % 12.35/4.25 tff(c_2824, plain, (![V_770]: (~male(skc24, V_770) | ~abstraction(skc14, V_770)))). % 12.35/4.25 tff(c_2816, plain, (![V_769]: (~male(skc15, V_769) | ~abstraction(skc14, V_769)))). % 12.35/4.25 tff(c_2808, plain, (![V_767]: (unisex(skc24, V_767) | ~abstraction(skc14, V_767)))). % 12.35/4.25 tff(c_2807, plain, (![V_767]: (unisex(skc15, V_767) | ~abstraction(skc14, V_767)))). % 12.35/4.25 tff(c_1812, plain, (![V_600, V_26, U_25]: (unisex(V_600, V_26) | ~accessible_world(U_25, V_600) | ~abstraction(U_25, V_26)))). % 12.35/4.25 tff(c_2749, plain, (![V_761]: (~human(skc24, V_761) | ~abstraction(skc14, V_761)))). % 12.35/4.25 tff(c_2741, plain, (![V_760]: (~human(skc15, V_760) | ~abstraction(skc14, V_760)))). % 12.35/4.25 tff(c_2620, plain, (![V_752]: (impartial(skc24, V_752) | ~human_person(skc14, V_752)))). % 12.35/4.25 tff(c_2603, plain, (![V_751]: (living(skc15, V_751) | ~human_person(skc14, V_751)))). % 12.35/4.25 tff(c_2712, plain, (![V_758]: (nonhuman(skc24, V_758) | ~abstraction(skc14, V_758)))). % 12.35/4.25 tff(c_2711, plain, (![V_758]: (nonhuman(skc15, V_758) | ~abstraction(skc14, V_758)))). % 12.35/4.25 tff(c_2704, plain, (entity(skc24, skc27))). % 12.35/4.25 tff(c_2705, plain, (entity(skc24, skc18))). % 12.35/4.25 tff(c_2703, plain, (entity(skc24, skc22))). % 12.35/4.25 tff(c_1311, plain, (![V_504, V_22, U_21]: (nonhuman(V_504, V_22) | ~accessible_world(U_21, V_504) | ~abstraction(U_21, V_22)))). % 12.35/4.25 tff(c_2618, plain, (![V_752]: (entity(skc24, V_752) | ~human_person(skc14, V_752)))). % 12.35/4.25 tff(c_2604, plain, (![V_751]: (impartial(skc15, V_751) | ~human_person(skc14, V_751)))). % 12.35/4.25 tff(c_2647, plain, (entity(skc15, skc27))). % 12.35/4.25 tff(c_2648, plain, (entity(skc15, skc18))). % 12.35/4.25 tff(c_2646, plain, (entity(skc15, skc22))). % 12.35/4.25 tff(c_2619, plain, (![V_752]: (living(skc24, V_752) | ~human_person(skc14, V_752)))). % 12.35/4.25 tff(c_2602, plain, (![V_751]: (entity(skc15, V_751) | ~human_person(skc14, V_751)))). % 12.35/4.25 tff(c_2588, plain, (![V_749]: (organism(skc24, V_749) | ~human_person(skc14, V_749)))). % 12.35/4.25 tff(c_2587, plain, (![V_749]: (organism(skc15, V_749) | ~human_person(skc14, V_749)))). % 12.35/4.25 tff(c_1799, plain, (![V_594, V_34, U_33]: (organism(V_594, V_34) | ~accessible_world(U_33, V_594) | ~human_person(U_33, V_34)))). % 12.35/4.25 tff(c_2437, plain, (![V_4]: (~abstraction(skc15, V_4) | ~event(skc14, V_4)))). % 12.35/4.25 tff(c_2423, plain, (![V_24]: (~eventuality(skc14, V_24) | ~abstraction(skc24, V_24)))). % 12.35/4.25 tff(c_2380, plain, (![V_734]: (abstraction(skc15, V_734) | ~forename(skc14, V_734)))). % 12.35/4.25 tff(c_2388, plain, (![V_735]: (abstraction(skc24, V_735) | ~forename(skc14, V_735)))). % 12.35/4.25 tff(c_2417, plain, (![V_24]: (~eventuality(skc14, V_24) | ~abstraction(skc15, V_24)))). % 12.35/4.25 tff(c_2411, plain, (![V_740]: (~general(skc24, V_740) | ~eventuality(skc14, V_740)))). % 12.35/4.25 tff(c_2403, plain, (![V_739]: (~general(skc15, V_739) | ~eventuality(skc14, V_739)))). % 12.35/4.25 tff(c_2395, plain, (![V_737]: (specific(skc24, V_737) | ~eventuality(skc14, V_737)))). % 12.35/4.25 tff(c_2394, plain, (![V_737]: (specific(skc15, V_737) | ~eventuality(skc14, V_737)))). % 12.35/4.25 tff(c_1487, plain, (![V_545, V_10, U_9]: (specific(V_545, V_10) | ~accessible_world(U_9, V_545) | ~eventuality(U_9, V_10)))). % 12.35/4.25 tff(c_2372, plain, (![V_733]: (relation(skc24, V_733) | ~forename(skc14, V_733)))). % 12.35/4.25 tff(c_2364, plain, (![V_732]: (relation(skc15, V_732) | ~forename(skc14, V_732)))). % 12.35/4.25 tff(c_2356, plain, (![V_730]: (relname(skc24, V_730) | ~forename(skc14, V_730)))). % 12.35/4.25 tff(c_2355, plain, (![V_730]: (relname(skc15, V_730) | ~forename(skc14, V_730)))). % 12.35/4.25 tff(c_1861, plain, (![V_610, V_54, U_53]: (relname(V_610, V_54) | ~accessible_world(U_53, V_610) | ~forename(U_53, V_54)))). % 12.35/4.25 tff(c_2205, plain, (![V_684]: (be(V_684, skc17, skc18, skc18) | ~accessible_world(skc14, V_684)))). % 12.35/4.25 tff(c_2313, plain, (![V_717, V_718]: (~abstraction(V_717, skf1(V_718)) | ~accessible_world(skc24, V_717)))). % 12.35/4.25 tff(c_2314, plain, (![V_717, V_718]: (~entity(V_717, skf1(V_718)) | ~accessible_world(skc24, V_717)))). % 12.35/4.25 tff(c_2161, plain, (![V_662]: (theme(V_662, skc25, skc24) | ~accessible_world(skc14, V_662)))). % 12.35/4.25 tff(c_2175, plain, (![V_668]: (of(V_668, skc19, skc18) | ~accessible_world(skc14, V_668)))). % 12.35/4.25 tff(c_2160, plain, (![V_662]: (theme(V_662, skc16, skc15) | ~accessible_world(skc14, V_662)))). % 12.35/4.25 tff(c_1561, plain, (![V_557, V_191]: (smoke(V_557, skf1(V_191)) | ~accessible_world(skc24, V_557)))). % 12.35/4.25 tff(c_1349, plain, (![V_512, V_195]: (event(V_512, skf1(V_195)) | ~accessible_world(skc24, V_512)))). % 12.35/4.25 tff(c_2056, plain, (![V_638, V_193]: (present(V_638, skf1(V_193)) | ~accessible_world(skc24, V_638)))). % 12.35/4.25 tff(c_2173, plain, (![V_668]: (of(V_668, skc21, skc22) | ~accessible_world(skc14, V_668)))). % 12.35/4.25 tff(c_2196, plain, (![V_673]: (agent(V_673, skc23, skc22) | ~accessible_world(skc15, V_673)))). % 12.35/4.25 tff(c_2197, plain, (![V_673]: (agent(V_673, skc16, skc18) | ~accessible_world(skc14, V_673)))). % 12.35/4.25 tff(c_2198, plain, (![V_673]: (agent(V_673, skc25, skc27) | ~accessible_world(skc14, V_673)))). % 12.35/4.25 tff(c_2176, plain, (![V_668]: (of(V_668, skc26, skc27) | ~accessible_world(skc14, V_668)))). % 12.35/4.25 tff(c_1942, plain, (![V_110]: (abstraction(V_110, skc21) | ~accessible_world(skc24, V_110)))). % 12.35/4.25 tff(c_1945, plain, (![V_110]: (abstraction(V_110, skc21) | ~accessible_world(skc15, V_110)))). % 12.35/4.25 tff(c_1985, plain, (![V_110]: (abstraction(V_110, skc19) | ~accessible_world(skc24, V_110)))). % 12.35/4.25 tff(c_1828, plain, (![V_110]: (abstraction(V_110, skc26) | ~accessible_world(skc24, V_110)))). % 12.35/4.25 tff(c_1963, plain, (![V_110]: (abstraction(V_110, skc19) | ~accessible_world(skc15, V_110)))). % 12.35/4.25 tff(c_1825, plain, (![V_110]: (abstraction(V_110, skc26) | ~accessible_world(skc15, V_110)))). % 12.35/4.25 tff(c_1651, plain, (![V_569]: (abstraction(V_569, skc15) | ~accessible_world(skc15, V_569)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1621, plain, (![V_512]: (~entity(V_512, skc16) | ~accessible_world(skc14, V_512)))). % 12.35/4.25 tff(c_1649, plain, (![V_569]: (abstraction(V_569, skc24) | ~accessible_world(skc15, V_569)))). % 12.35/4.25 tff(c_1951, plain, (![U_3]: (~accessible_world(skc14, U_3) | ~event(U_3, skc18)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_2015, plain, (![V_512]: (~abstraction(V_512, skc23) | ~accessible_world(skc15, V_512)))). % 12.35/4.25 tff(c_1648, plain, (![V_569]: (abstraction(V_569, skc24) | ~accessible_world(skc24, V_569)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1650, plain, (![V_569]: (abstraction(V_569, skc15) | ~accessible_world(skc24, V_569)))). % 12.35/4.25 tff(c_1619, plain, (![V_512]: (~entity(V_512, skc23) | ~accessible_world(skc15, V_512)))). % 12.35/4.25 tff(c_1576, plain, (![U_3]: (~accessible_world(skc14, U_3) | ~event(U_3, skc27)))). % 12.35/4.25 tff(c_2185, plain, (~abstraction(skc24, skc25))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_2184, plain, (~abstraction(skc15, skc25))). % 12.35/4.25 tff(c_2016, plain, (![V_512]: (~abstraction(V_512, skc25) | ~accessible_world(skc14, V_512)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1620, plain, (![V_512]: (~entity(V_512, skc25) | ~accessible_world(skc14, V_512)))). % 12.35/4.25 tff(c_2081, plain, (![U_3]: (~accessible_world(skc14, U_3) | ~event(U_3, skc22)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_2138, plain, (![V_657]: (jules_forename(V_657, skc21) | ~accessible_world(skc14, V_657)))). % 12.35/4.25 tff(c_2137, plain, (![V_657]: (jules_forename(V_657, skc19) | ~accessible_world(skc14, V_657)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_2131, plain, (~abstraction(skc24, skc16))). % 12.35/4.25 tff(c_2130, plain, (~abstraction(skc15, skc16))). % 12.35/4.25 tff(c_2017, plain, (![V_512]: (~abstraction(V_512, skc16) | ~accessible_world(skc14, V_512)))). % 12.35/4.25 tff(c_2103, plain, (~abstraction(skc24, skc22))). % 12.35/4.25 tff(c_2102, plain, (~abstraction(skc15, skc22))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1498, plain, (![V_548]: (~abstraction(V_548, skc22) | ~accessible_world(skc14, V_548)))). % 12.35/4.25 tff(c_2090, plain, (~abstraction(skc24, skc27))). % 12.35/4.25 tff(c_2089, plain, (~abstraction(skc15, skc27))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1510, plain, (![V_549]: (~abstraction(V_549, skc27) | ~accessible_world(skc14, V_549)))). % 12.35/4.25 tff(c_1499, plain, (![V_548]: (~eventuality(V_548, skc22) | ~accessible_world(skc14, V_548)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_2059, plain, (![V_638]: (present(V_638, skc23) | ~accessible_world(skc15, V_638)))). % 12.35/4.25 tff(c_2058, plain, (![V_638]: (present(V_638, skc25) | ~accessible_world(skc14, V_638)))). % 12.35/4.25 tff(c_2057, plain, (![V_638]: (present(V_638, skc16) | ~accessible_world(skc14, V_638)))). % 12.35/4.25 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)))). % 12.35/4.25 tff(c_1404, plain, (![V_528]: (entity(V_528, skc22) | ~accessible_world(skc14, V_528)))). % 12.35/4.25 tff(c_1938, plain, (![V_622]: (human(V_622, skc22) | ~accessible_world(skc14, V_622)))). % 12.35/4.25 tff(c_2018, plain, (![V_195]: (~abstraction(skc24, skf1(V_195))))). % 12.35/4.26 tff(c_2021, plain, (~abstraction(skc14, skc25))). % 12.35/4.26 tff(c_2022, plain, (~abstraction(skc15, skc23))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_2020, plain, (~abstraction(skc14, skc16))). % 12.35/4.26 tff(c_1470, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 12.35/4.26 tff(c_1960, plain, (abstraction(skc24, skc19))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1959, plain, (abstraction(skc15, skc19))). % 12.35/4.26 tff(c_1914, plain, (![V_620]: (abstraction(V_620, skc19) | ~accessible_world(skc14, V_620)))). % 12.35/4.26 tff(c_1523, plain, (![V_550]: (~eventuality(V_550, skc18) | ~accessible_world(skc14, V_550)))). % 12.35/4.26 tff(c_1922, plain, (abstraction(skc15, skc21))). % 12.35/4.26 tff(c_1923, plain, (abstraction(skc24, skc21))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1906, plain, (![V_619]: (abstraction(V_619, skc21) | ~accessible_world(skc14, V_619)))). % 12.35/4.26 tff(c_1898, plain, (![V_616]: (forename(V_616, skc19) | ~accessible_world(skc14, V_616)))). % 12.35/4.26 tff(c_1897, plain, (![V_616]: (forename(V_616, skc21) | ~accessible_world(skc14, V_616)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1780, plain, (![V_592]: (entity(V_592, skc27) | ~accessible_world(skc14, V_592)))). % 12.35/4.26 tff(c_1871, plain, (~abstraction(skc24, skc17))). % 12.35/4.26 tff(c_1870, plain, (~abstraction(skc15, skc17))). % 12.35/4.26 tff(c_1469, plain, (![V_522]: (~abstraction(V_522, skc17) | ~accessible_world(skc14, V_522)))). % 12.35/4.26 tff(c_1769, plain, (![V_591]: (animate(V_591, skc22) | ~accessible_world(skc14, V_591)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1794, plain, (![V_593]: (human(V_593, skc18) | ~accessible_world(skc14, V_593)))). % 12.35/4.26 tff(c_1781, plain, (![V_592]: (human(V_592, skc27) | ~accessible_world(skc14, V_592)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1822, plain, (abstraction(skc24, skc26))). % 12.35/4.26 tff(c_1821, plain, (abstraction(skc15, skc26))). % 12.35/4.26 tff(c_1804, plain, (![V_597]: (abstraction(V_597, skc26) | ~accessible_world(skc14, V_597)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1795, plain, (![V_593]: (animate(V_593, skc18) | ~accessible_world(skc14, V_593)))). % 12.35/4.26 tff(c_1782, plain, (![V_592]: (animate(V_592, skc27) | ~accessible_world(skc14, V_592)))). % 12.35/4.26 tff(c_1690, plain, (![V_578]: (forename(V_578, skc26) | ~accessible_world(skc14, V_578)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1716, plain, (![V_583]: (human_person(V_583, skc18) | ~accessible_world(skc14, V_583)))). % 12.35/4.26 tff(c_1728, plain, (![V_584]: (human_person(V_584, skc27) | ~accessible_world(skc14, V_584)))). % 12.35/4.26 tff(c_1740, plain, (![V_585]: (human_person(V_585, skc22) | ~accessible_world(skc14, V_585)))). % 12.35/4.26 tff(c_1748, plain, (![V_586]: (think_believe_consider(V_586, skc25) | ~accessible_world(skc14, V_586)))). % 12.35/4.26 tff(c_1747, plain, (![V_586]: (think_believe_consider(V_586, skc16) | ~accessible_world(skc14, V_586)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1705, plain, (![V_580]: (man(V_580, skc22) | ~accessible_world(skc14, V_580)))). % 12.35/4.26 tff(c_1704, plain, (![V_580]: (man(V_580, skc27) | ~accessible_world(skc14, V_580)))). % 12.35/4.26 tff(c_1703, plain, (![V_580]: (man(V_580, skc18) | ~accessible_world(skc14, V_580)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1674, plain, (![V_574]: (vincent_forename(V_574, skc26) | ~accessible_world(skc14, V_574)))). % 12.35/4.26 tff(c_1666, plain, (~abstraction(skc15, skc18))). % 12.35/4.26 tff(c_1667, plain, (~abstraction(skc24, skc18))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1522, plain, (![V_550]: (~abstraction(V_550, skc18) | ~accessible_world(skc14, V_550)))). % 12.35/4.26 tff(c_1622, plain, (![V_195]: (~entity(skc24, skf1(V_195))))). % 12.35/4.26 tff(c_1626, plain, (~entity(skc15, skc23))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1625, plain, (~entity(skc14, skc25))). % 12.35/4.26 tff(c_1624, plain, (~entity(skc14, skc16))). % 12.35/4.26 tff(c_1545, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 12.35/4.26 tff(c_1544, plain, (![V_522]: (~entity(V_522, skc17) | ~accessible_world(skc14, V_522)))). % 12.35/4.26 tff(c_1403, plain, (![V_528]: (entity(V_528, skc18) | ~accessible_world(skc14, V_528)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1511, plain, (![V_549]: (~eventuality(V_549, skc27) | ~accessible_world(skc14, V_549)))). % 12.35/4.26 tff(c_1562, plain, (![V_557]: (smoke(V_557, skc23) | ~accessible_world(skc15, V_557)))). % 12.35/4.26 tff(c_1555, plain, (abstraction(skc24, skc24))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1554, plain, (abstraction(skc15, skc24))). % 12.35/4.26 tff(c_1436, plain, (![V_536]: (abstraction(V_536, skc24) | ~accessible_world(skc14, V_536)))). % 12.35/4.26 tff(c_1546, plain, (~entity(skc14, skc17))). % 12.35/4.26 tff(c_1288, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1458, plain, (![V_539]: (male(V_539, skc18) | ~accessible_world(skc14, V_539)))). % 12.35/4.26 tff(c_1456, plain, (![V_539]: (male(V_539, skc27) | ~accessible_world(skc14, V_539)))). % 12.35/4.26 tff(c_1457, plain, (![V_539]: (male(V_539, skc22) | ~accessible_world(skc14, V_539)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1480, plain, (abstraction(skc24, skc15))). % 12.35/4.26 tff(c_1479, plain, (abstraction(skc15, skc15))). % 12.35/4.26 tff(c_1444, plain, (![V_537]: (abstraction(V_537, skc15) | ~accessible_world(skc14, V_537)))). % 12.35/4.26 tff(c_1471, plain, (~abstraction(skc14, skc17))). % 12.35/4.26 tff(c_1263, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1377, plain, (![V_522]: (eventuality(V_522, skc17) | ~accessible_world(skc14, V_522)))). % 12.35/4.26 tff(c_1428, plain, (![V_533]: (proposition(V_533, skc15) | ~accessible_world(skc14, V_533)))). % 12.35/4.26 tff(c_1427, plain, (![V_533]: (proposition(V_533, skc24) | ~accessible_world(skc14, V_533)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1421, plain, (abstraction(skc14, skc19))). % 12.35/4.26 tff(c_1420, plain, (abstraction(skc14, skc21))). % 12.35/4.26 tff(c_1419, plain, (abstraction(skc14, skc26))). % 12.35/4.26 tff(c_1268, plain, (![U_484, V_485]: (abstraction(U_484, V_485) | ~forename(U_484, V_485)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1283, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 12.35/4.26 tff(c_1336, plain, (![V_509]: (event(V_509, skc17) | ~accessible_world(skc14, V_509)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1353, plain, (![V_512]: (event(V_512, skc23) | ~accessible_world(skc15, V_512)))). % 12.35/4.26 tff(c_1352, plain, (![V_512]: (event(V_512, skc25) | ~accessible_world(skc14, V_512)))). % 12.35/4.26 tff(c_1351, plain, (![V_512]: (event(V_512, skc16) | ~accessible_world(skc14, V_512)))). % 12.35/4.26 tff(c_330, plain, (![U_33, V_34]: (living(U_33, V_34) | ~human_person(U_33, V_34)))). % 12.35/4.26 tff(c_392, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_295, plain, (![U_33, V_34]: (impartial(U_33, V_34) | ~human_person(U_33, V_34)))). % 12.35/4.26 tff(c_1305, plain, (![V_497]: (state(V_497, skc17) | ~accessible_world(skc14, V_497)))). % 12.35/4.26 tff(c_273, plain, (![U_223, V_224]: (~male(U_223, V_224) | ~abstraction(U_223, V_224)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_390, plain, (![U_37, V_38]: (singleton(U_37, V_38) | ~entity(U_37, V_38)))). % 12.35/4.26 tff(c_391, plain, (![U_19, V_20]: (singleton(U_19, V_20) | ~abstraction(U_19, V_20)))). % 12.35/4.26 tff(c_1300, plain, (~abstraction(skc14, skc22))). % 12.35/4.26 tff(c_1301, plain, (~abstraction(skc14, skc18))). % 12.35/4.26 tff(c_1299, plain, (~abstraction(skc14, skc27))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_280, plain, (![U_21, V_22]: (~human(U_21, V_22) | ~abstraction(U_21, V_22)))). % 12.35/4.26 tff(c_290, plain, (![U_233, V_234]: (~existent(U_233, V_234) | ~eventuality(U_233, V_234)))). % 12.35/4.26 tff(c_318, plain, (![U_241, V_242]: (~general(U_241, V_242) | ~entity(U_241, V_242)))). % 12.35/4.26 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)))). % 12.35/4.26 tff(c_1277, plain, (abstraction(skc14, skc15))). % 12.35/4.26 tff(c_1276, plain, (abstraction(skc14, skc24))). % 12.35/4.26 tff(c_323, plain, (![U_243, V_244]: (abstraction(U_243, V_244) | ~proposition(U_243, V_244)))). % 12.35/4.26 tff(c_285, plain, (![U_231, V_232]: (relation(U_231, V_232) | ~forename(U_231, V_232)))). % 12.35/4.26 tff(c_260, plain, (![U_213, V_214]: (~general(U_213, V_214) | ~eventuality(U_213, V_214)))). % 12.74/4.26 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)))). % 12.74/4.26 tff(c_1243, plain, (~event(skc14, skc22))). % 12.74/4.26 tff(c_1247, plain, (~event(skc14, skc18))). % 12.74/4.26 tff(c_1239, plain, (~event(skc14, skc27))). % 12.74/4.26 tff(c_222, plain, (![U_196]: (agent(skc24, skf1(U_196), U_196) | ~man(skc24, U_196)))). % 12.74/4.26 tff(c_1235, plain, (~eventuality(skc14, skc18))). % 12.74/4.26 tff(c_1234, plain, (~eventuality(skc14, skc22))). % 12.74/4.26 tff(c_1233, plain, (~eventuality(skc14, skc27))). % 12.74/4.26 tff(c_268, plain, (![U_221, V_222]: (~male(U_221, V_222) | ~eventuality(U_221, V_222)))). % 12.74/4.26 tff(c_1210, plain, (![V_191]: (smoke(skc24, skf1(V_191))))). % 12.74/4.26 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)))). % 12.74/4.26 tff(c_1109, plain, (![V_193]: (present(skc24, skf1(V_193))))). % 12.74/4.26 tff(c_729, plain, (![V_195]: (event(skc24, skf1(V_195))))). % 12.74/4.26 tff(c_405, plain, (entity(skc14, skc27))). % 12.74/4.26 tff(c_406, plain, (entity(skc14, skc18))). % 12.74/4.26 tff(c_404, plain, (entity(skc14, skc22))). % 12.74/4.26 tff(c_336, plain, (![U_33, V_34]: (entity(U_33, V_34) | ~human_person(U_33, V_34)))). % 12.74/4.26 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 12.74/4.26 tff(c_358, plain, (animate(skc14, skc18))). % 12.74/4.26 tff(c_366, plain, (animate(skc14, skc27))). % 12.74/4.26 tff(c_365, plain, (human(skc14, skc27))). % 12.74/4.26 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 12.74/4.26 tff(c_373, plain, (human(skc14, skc22))). % 12.74/4.26 tff(c_374, plain, (animate(skc14, skc22))). % 12.74/4.26 tff(c_379, plain, (eventuality(skc14, skc17))). % 12.74/4.26 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 12.74/4.27 tff(c_357, plain, (human(skc14, skc18))). % 12.74/4.27 tff(c_350, plain, (human_person(skc14, skc22))). % 12.74/4.27 tff(c_349, plain, (human_person(skc14, skc27))). % 12.74/4.27 tff(c_348, plain, (human_person(skc14, skc18))). % 12.74/4.27 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 12.74/4.27 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 12.74/4.27 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 12.74/4.27 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 12.74/4.27 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 12.74/4.27 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 12.74/4.27 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 12.74/4.27 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 12.74/4.27 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 12.74/4.27 tff(c_313, plain, (event(skc14, skc17))). % 12.74/4.27 tff(c_307, plain, (male(skc14, skc27))). % 12.74/4.27 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 12.74/4.27 tff(c_308, plain, (male(skc14, skc22))). % 12.74/4.27 tff(c_306, plain, (male(skc14, skc18))). % 12.74/4.27 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 12.74/4.27 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 12.74/4.27 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 12.74/4.27 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 12.74/4.27 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 12.74/4.27 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 12.74/4.27 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 12.74/4.27 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 12.74/4.27 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 12.74/4.27 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 12.74/4.27 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 12.74/4.27 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 12.74/4.27 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 12.74/4.27 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 12.74/4.27 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 12.74/4.27 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 12.74/4.27 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 12.74/4.27 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 12.74/4.27 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 12.74/4.27 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 12.74/4.27 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 12.74/4.27 tff(c_214, plain, (be(skc14, skc17, skc18, skc18))). % 12.74/4.27 tff(c_212, plain, (theme(skc14, skc16, skc15))). % 12.74/4.27 tff(c_202, plain, (of(skc14, skc21, skc22))). % 12.74/4.27 tff(c_204, plain, (agent(skc15, skc23, skc22))). % 12.74/4.27 tff(c_208, plain, (of(skc14, skc19, skc18))). % 12.74/4.27 tff(c_200, plain, (theme(skc14, skc25, skc24))). % 12.74/4.27 tff(c_198, plain, (of(skc14, skc26, skc27))). % 12.74/4.27 tff(c_210, plain, (agent(skc14, skc16, skc18))). % 12.74/4.27 tff(c_196, plain, (agent(skc14, skc25, skc27))). % 12.74/4.27 tff(c_176, plain, (state(skc14, skc17))). % 12.74/4.27 tff(c_178, plain, (event(skc14, skc16))). % 12.74/4.27 tff(c_180, plain, (present(skc14, skc16))). % 12.74/4.27 tff(c_182, plain, (think_believe_consider(skc14, skc16))). % 12.74/4.27 tff(c_184, plain, (accessible_world(skc14, skc15))). % 12.74/4.27 tff(c_170, plain, (man(skc14, skc18))). % 12.74/4.27 tff(c_192, plain, (proposition(skc14, skc24))). % 12.74/4.27 tff(c_168, plain, (jules_forename(skc14, skc19))). % 12.74/4.27 tff(c_146, plain, (man(skc14, skc27))). % 12.74/4.27 tff(c_148, plain, (vincent_forename(skc14, skc26))). % 12.74/4.27 tff(c_186, plain, (proposition(skc14, skc15))). % 12.74/4.27 tff(c_150, plain, (forename(skc14, skc26))). % 12.74/4.27 tff(c_188, plain, (forename(skc14, skc21))). % 12.74/4.27 tff(c_154, plain, (present(skc14, skc25))). % 12.74/4.27 tff(c_152, plain, (think_believe_consider(skc14, skc25))). % 12.74/4.27 tff(c_166, plain, (forename(skc14, skc19))). % 12.74/4.27 tff(c_164, plain, (smoke(skc15, skc23))). % 12.74/4.27 tff(c_162, plain, (present(skc15, skc23))). % 12.74/4.27 tff(c_156, plain, (event(skc14, skc25))). % 12.74/4.27 tff(c_158, plain, (event(skc15, skc23))). % 12.74/4.27 tff(c_160, plain, (man(skc14, skc22))). % 12.74/4.27 tff(c_190, plain, (jules_forename(skc14, skc21))). % 12.74/4.27 tff(c_194, plain, (accessible_world(skc14, skc24))). % 12.74/4.27 tff(c_144, plain, (actual_world(skc14))). % 12.74/4.27 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.74/4.27 %------------------------------------------------------------------------------