%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP025-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:47:57 PM UTC 2025 % Result : Satisfiable 16.55s 5.83s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP025-1 : TPTP v9.0.0. Released v2.4.0. % 0.12/0.13 % 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.34 % Computer : n013.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:10:17 EDT 2025 % 0.12/0.34 % CPUTime : % 16.49/5.83 % 16.55/5.83 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.55/5.83 % 16.55/5.83 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.55/5.84 %$ theme > of > agent > woman > vincent_forename > unisex > thing > specific > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > mia_forename > man > male > living > impartial > human_person > human > general > forename > female > existent > eventuality > event > entity > desire_want > dance > animate > accessible_world > abstraction > actual_world > skf5 > skf4 > skf3 > #nlpp > skc9 > skc8 > skc7 > skc6 > skc11 > skc10 % 16.55/5.84 % 16.55/5.84 %Foreground sorts: % 16.55/5.84 % 16.55/5.84 % 16.55/5.84 %Background operators: % 16.55/5.84 % 16.55/5.84 % 16.55/5.84 %Foreground operators: % 16.55/5.84 tff(skf3, type, skf3: ($i * $i) > $i). % 16.55/5.84 tff(relation, type, relation: ($i * $i) > $o). % 16.55/5.84 tff(forename, type, forename: ($i * $i) > $o). % 16.55/5.84 tff(skc7, type, skc7: $i). % 16.55/5.84 tff(female, type, female: ($i * $i) > $o). % 16.55/5.84 tff(theme, type, theme: ($i * $i * $i) > $o). % 16.55/5.84 tff(living, type, living: ($i * $i) > $o). % 16.55/5.84 tff(human_person, type, human_person: ($i * $i) > $o). % 16.55/5.84 tff(present, type, present: ($i * $i) > $o). % 16.55/5.84 tff(skc11, type, skc11: $i). % 16.55/5.84 tff(entity, type, entity: ($i * $i) > $o). % 16.55/5.84 tff(skc9, type, skc9: $i). % 16.55/5.84 tff(eventuality, type, eventuality: ($i * $i) > $o). % 16.55/5.84 tff(existent, type, existent: ($i * $i) > $o). % 16.55/5.84 tff(abstraction, type, abstraction: ($i * $i) > $o). % 16.55/5.84 tff(skc8, type, skc8: $i). % 16.55/5.84 tff(proposition, type, proposition: ($i * $i) > $o). % 16.55/5.84 tff(relname, type, relname: ($i * $i) > $o). % 16.55/5.84 tff(skf5, type, skf5: ($i * $i) > $i). % 16.55/5.84 tff(singleton, type, singleton: ($i * $i) > $o). % 16.55/5.84 tff(male, type, male: ($i * $i) > $o). % 16.55/5.84 tff(organism, type, organism: ($i * $i) > $o). % 16.55/5.84 tff(animate, type, animate: ($i * $i) > $o). % 16.55/5.84 tff(of, type, of: ($i * $i * $i) > $o). % 16.55/5.84 tff(actual_world, type, actual_world: $i > $o). % 16.55/5.84 tff(agent, type, agent: ($i * $i * $i) > $o). % 16.55/5.84 tff(general, type, general: ($i * $i) > $o). % 16.55/5.84 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 16.55/5.84 tff(event, type, event: ($i * $i) > $o). % 16.55/5.84 tff(woman, type, woman: ($i * $i) > $o). % 16.55/5.84 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 16.55/5.84 tff(thing, type, thing: ($i * $i) > $o). % 16.55/5.84 tff(dance, type, dance: ($i * $i) > $o). % 16.55/5.84 tff(desire_want, type, desire_want: ($i * $i) > $o). % 16.55/5.84 tff(human, type, human: ($i * $i) > $o). % 16.55/5.84 tff(man, type, man: ($i * $i) > $o). % 16.55/5.84 tff(unisex, type, unisex: ($i * $i) > $o). % 16.55/5.84 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 16.55/5.84 tff(skc6, type, skc6: $i). % 16.55/5.84 tff(impartial, type, impartial: ($i * $i) > $o). % 16.55/5.84 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 16.55/5.84 tff(specific, type, specific: ($i * $i) > $o). % 16.55/5.84 tff(skf4, type, skf4: ($i * $i) > $i). % 16.55/5.84 tff(skc10, type, skc10: $i). % 16.55/5.84 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 16.55/5.84 % 16.55/5.84 %Saturated clause set: % 16.55/5.84 tff(c_4521, plain, (![W_1277, X3_1275, V_523, V_1278]: (agent(skf4(W_1277, X3_1275), skf5(X3_1275, W_1277), W_1277) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1278, W_1277) | ~man(V_523, W_1277) | ~forename(V_523, V_1278) | ~vincent_forename(V_523, V_1278) | ~accessible_world(skc6, V_523)))). % 16.55/5.84 tff(c_4408, plain, (![V_523, W_1259, V_1261]: (theme(V_523, skf3(V_523, W_1259), skf4(W_1259, V_523)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1261, W_1259) | ~man(V_523, W_1259) | ~forename(V_523, V_1261) | ~vincent_forename(V_523, V_1261) | ~accessible_world(skc6, V_523)))). % 16.55/5.84 tff(c_4190, plain, (![W_1228, X3_1230, V_523, V_1226]: (dance(skf4(W_1228, X3_1230), skf5(X3_1230, W_1228)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1226, W_1228) | ~man(V_523, W_1228) | ~forename(V_523, V_1226) | ~vincent_forename(V_523, V_1226) | ~accessible_world(skc6, V_523)))). % 16.55/5.84 tff(c_4315, plain, (![W_1246, X3_1244, V_523, V_1242]: (event(skf4(W_1246, X3_1244), skf5(X3_1244, W_1246)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1242, W_1246) | ~man(V_523, W_1246) | ~forename(V_523, V_1242) | ~vincent_forename(V_523, V_1242) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_7587, plain, (![V_482]: (~actual_world(V_482) | ~mia_forename(V_482, skc9) | ~proposition(V_482, skc8) | ~accessible_world(V_482, skc8) | ~desire_want(V_482, skc7) | ~present(V_482, skc7) | ~man(V_482, skc10) | ~forename(V_482, skc9) | ~vincent_forename(V_482, skc9) | ~accessible_world(skc6, V_482)))). % 16.55/5.85 tff(c_3462, plain, (![V_1097, X_1096, W_1100, V_1098, V_534]: (theme(V_1097, skf3(V_1097, W_1100), skf4(W_1100, V_1097)) | ~actual_world(V_1097) | ~woman(V_1097, skc10) | ~agent(V_1097, X_1096, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1097, skc9) | ~mia_forename(V_1097, skc9) | ~proposition(V_1097, V_534) | ~theme(V_1097, X_1096, V_534) | ~accessible_world(V_1097, V_534) | ~desire_want(V_1097, X_1096) | ~present(V_1097, X_1096) | ~of(V_1097, V_1098, W_1100) | ~man(V_1097, W_1100) | ~forename(V_1097, V_1098) | ~vincent_forename(V_1097, V_1098) | ~accessible_world(skc6, V_1097) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_4080, plain, (![W_1210, X3_1209, V_523, V_1211]: (present(skf4(W_1210, X3_1209), skf5(X3_1209, W_1210)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1211, W_1210) | ~man(V_523, W_1210) | ~forename(V_523, V_1211) | ~vincent_forename(V_523, V_1211) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_3553, plain, (![V_1117, X3_1118, V_1123, W_1122, X_1121, V_534]: (agent(skf4(W_1122, X3_1118), skf5(X3_1118, W_1122), W_1122) | ~actual_world(V_1117) | ~woman(V_1117, skc10) | ~agent(V_1117, X_1121, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1117, skc9) | ~mia_forename(V_1117, skc9) | ~proposition(V_1117, V_534) | ~theme(V_1117, X_1121, V_534) | ~accessible_world(V_1117, V_534) | ~desire_want(V_1117, X_1121) | ~present(V_1117, X_1121) | ~of(V_1117, V_1123, W_1122) | ~man(V_1117, W_1122) | ~forename(V_1117, V_1123) | ~vincent_forename(V_1117, V_1123) | ~accessible_world(skc6, V_1117) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_3939, plain, (![V_523, W_1191, V_1193]: (agent(V_523, skf3(V_523, W_1191), W_1191) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1193, W_1191) | ~man(V_523, W_1191) | ~forename(V_523, V_1193) | ~vincent_forename(V_523, V_1193) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_3463, plain, (![V_1097, X_1096, W_1100, V_1098, V_534]: (theme(V_1097, skf3(V_1097, W_1100), skf4(W_1100, V_1097)) | ~actual_world(V_1097) | ~woman(V_1097, skc10) | ~agent(V_1097, X_1096, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1097, skc9) | ~mia_forename(V_1097, skc9) | ~proposition(V_1097, V_534) | ~theme(V_1097, X_1096, V_534) | ~accessible_world(V_1097, V_534) | ~desire_want(V_1097, X_1096) | ~present(V_1097, X_1096) | ~of(V_1097, V_1098, W_1100) | ~man(V_1097, W_1100) | ~forename(V_1097, V_1098) | ~vincent_forename(V_1097, V_1098) | ~accessible_world(skc6, V_1097) | ~accessible_world(skc8, V_534)))). % 16.55/5.85 tff(c_3719, plain, (![V_523, X3_1162, V_1161, W_1159]: (desire_want(V_523, skf3(V_523, X3_1162)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1161, W_1159) | ~man(V_523, W_1159) | ~forename(V_523, V_1161) | ~vincent_forename(V_523, V_1161) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_3554, plain, (![V_1117, X3_1118, V_1123, W_1122, X_1121, V_534]: (agent(skf4(W_1122, X3_1118), skf5(X3_1118, W_1122), W_1122) | ~actual_world(V_1117) | ~woman(V_1117, skc10) | ~agent(V_1117, X_1121, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1117, skc9) | ~mia_forename(V_1117, skc9) | ~proposition(V_1117, V_534) | ~theme(V_1117, X_1121, V_534) | ~accessible_world(V_1117, V_534) | ~desire_want(V_1117, X_1121) | ~present(V_1117, X_1121) | ~of(V_1117, V_1123, W_1122) | ~man(V_1117, W_1122) | ~forename(V_1117, V_1123) | ~vincent_forename(V_1117, V_1123) | ~accessible_world(skc6, V_1117) | ~accessible_world(skc8, V_534)))). % 16.55/5.85 tff(c_3659, plain, (![V_523, X3_1139, V_1137, W_1140]: (present(V_523, skf3(V_523, X3_1139)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1137, W_1140) | ~man(V_523, W_1140) | ~forename(V_523, V_1137) | ~vincent_forename(V_523, V_1137) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_3340, plain, (![W_1071, V_1074, X3_1073, X_1077, V_1072, V_534]: (dance(skf4(W_1071, X3_1073), skf5(X3_1073, W_1071)) | ~actual_world(V_1072) | ~woman(V_1072, skc10) | ~agent(V_1072, X_1077, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1072, skc9) | ~mia_forename(V_1072, skc9) | ~proposition(V_1072, V_534) | ~theme(V_1072, X_1077, V_534) | ~accessible_world(V_1072, V_534) | ~desire_want(V_1072, X_1077) | ~present(V_1072, X_1077) | ~of(V_1072, V_1074, W_1071) | ~man(V_1072, W_1071) | ~forename(V_1072, V_1074) | ~vincent_forename(V_1072, V_1074) | ~accessible_world(skc6, V_1072) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_3187, plain, (![X_1048, W_1049, V_1051, X3_1054, V_1050, V_534]: (event(skf4(W_1049, X3_1054), skf5(X3_1054, W_1049)) | ~actual_world(V_1050) | ~woman(V_1050, skc10) | ~agent(V_1050, X_1048, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1050, skc9) | ~mia_forename(V_1050, skc9) | ~proposition(V_1050, V_534) | ~theme(V_1050, X_1048, V_534) | ~accessible_world(V_1050, V_534) | ~desire_want(V_1050, X_1048) | ~present(V_1050, X_1048) | ~of(V_1050, V_1051, W_1049) | ~man(V_1050, W_1049) | ~forename(V_1050, V_1051) | ~vincent_forename(V_1050, V_1051) | ~accessible_world(skc6, V_1050) | ~accessible_world(skc8, V_534)))). % 16.55/5.85 tff(c_6958, plain, (~accessible_world(skc8, skc8))). % 16.55/5.85 tff(c_3062, plain, (![X_1035, V_1037, X3_1034, W_1038, V_1036, V_534]: (present(skf4(W_1038, X3_1034), skf5(X3_1034, W_1038)) | ~actual_world(V_1037) | ~woman(V_1037, skc10) | ~agent(V_1037, X_1035, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1037, skc9) | ~mia_forename(V_1037, skc9) | ~proposition(V_1037, V_534) | ~theme(V_1037, X_1035, V_534) | ~accessible_world(V_1037, V_534) | ~desire_want(V_1037, X_1035) | ~present(V_1037, X_1035) | ~of(V_1037, V_1036, W_1038) | ~man(V_1037, W_1038) | ~forename(V_1037, V_1036) | ~vincent_forename(V_1037, V_1036) | ~accessible_world(skc6, V_1037) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_3186, plain, (![X_1048, W_1049, V_1051, X3_1054, V_1050, V_534]: (event(skf4(W_1049, X3_1054), skf5(X3_1054, W_1049)) | ~actual_world(V_1050) | ~woman(V_1050, skc10) | ~agent(V_1050, X_1048, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1050, skc9) | ~mia_forename(V_1050, skc9) | ~proposition(V_1050, V_534) | ~theme(V_1050, X_1048, V_534) | ~accessible_world(V_1050, V_534) | ~desire_want(V_1050, X_1048) | ~present(V_1050, X_1048) | ~of(V_1050, V_1051, W_1049) | ~man(V_1050, W_1049) | ~forename(V_1050, V_1051) | ~vincent_forename(V_1050, V_1051) | ~accessible_world(skc6, V_1050) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_3840, plain, (![V_523, W_1175, V_1177]: (proposition(V_523, skf4(W_1175, V_523)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_1177, W_1175) | ~man(V_523, W_1175) | ~forename(V_523, V_1177) | ~vincent_forename(V_523, V_1177) | ~accessible_world(skc6, V_523)))). % 16.55/5.85 tff(c_3341, plain, (![W_1071, V_1074, X3_1073, X_1077, V_1072, V_534]: (dance(skf4(W_1071, X3_1073), skf5(X3_1073, W_1071)) | ~actual_world(V_1072) | ~woman(V_1072, skc10) | ~agent(V_1072, X_1077, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1072, skc9) | ~mia_forename(V_1072, skc9) | ~proposition(V_1072, V_534) | ~theme(V_1072, X_1077, V_534) | ~accessible_world(V_1072, V_534) | ~desire_want(V_1072, X_1077) | ~present(V_1072, X_1077) | ~of(V_1072, V_1074, W_1071) | ~man(V_1072, W_1071) | ~forename(V_1072, V_1074) | ~vincent_forename(V_1072, V_1074) | ~accessible_world(skc6, V_1072) | ~accessible_world(skc8, V_534)))). % 16.55/5.85 tff(c_3063, plain, (![X_1035, V_1037, X3_1034, W_1038, V_1036, V_534]: (present(skf4(W_1038, X3_1034), skf5(X3_1034, W_1038)) | ~actual_world(V_1037) | ~woman(V_1037, skc10) | ~agent(V_1037, X_1035, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1037, skc9) | ~mia_forename(V_1037, skc9) | ~proposition(V_1037, V_534) | ~theme(V_1037, X_1035, V_534) | ~accessible_world(V_1037, V_534) | ~desire_want(V_1037, X_1035) | ~present(V_1037, X_1035) | ~of(V_1037, V_1036, W_1038) | ~man(V_1037, W_1038) | ~forename(V_1037, V_1036) | ~vincent_forename(V_1037, V_1036) | ~accessible_world(skc6, V_1037) | ~accessible_world(skc8, V_534)))). % 16.55/5.85 tff(c_2991, plain, (![X_1024, V_1021, W_1025, V_1020, V_534]: (agent(V_1021, skf3(V_1021, W_1025), W_1025) | ~actual_world(V_1021) | ~woman(V_1021, skc10) | ~agent(V_1021, X_1024, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1021, skc9) | ~mia_forename(V_1021, skc9) | ~proposition(V_1021, V_534) | ~theme(V_1021, X_1024, V_534) | ~accessible_world(V_1021, V_534) | ~desire_want(V_1021, X_1024) | ~present(V_1021, X_1024) | ~of(V_1021, V_1020, W_1025) | ~man(V_1021, W_1025) | ~forename(V_1021, V_1020) | ~vincent_forename(V_1021, V_1020) | ~accessible_world(skc6, V_1021) | ~accessible_world(skc6, V_534)))). % 16.55/5.85 tff(c_2992, plain, (![X_1024, V_1021, W_1025, V_1020, V_534]: (agent(V_1021, skf3(V_1021, W_1025), W_1025) | ~actual_world(V_1021) | ~woman(V_1021, skc10) | ~agent(V_1021, X_1024, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1021, skc9) | ~mia_forename(V_1021, skc9) | ~proposition(V_1021, V_534) | ~theme(V_1021, X_1024, V_534) | ~accessible_world(V_1021, V_534) | ~desire_want(V_1021, X_1024) | ~present(V_1021, X_1024) | ~of(V_1021, V_1020, W_1025) | ~man(V_1021, W_1025) | ~forename(V_1021, V_1020) | ~vincent_forename(V_1021, V_1020) | ~accessible_world(skc6, V_1021) | ~accessible_world(skc8, V_534)))). % 16.55/5.86 tff(c_2510, plain, (![V_978, W_977, V_979, X_982, V_534]: (accessible_world(V_979, skf4(W_977, V_979)) | ~actual_world(V_979) | ~woman(V_979, skc10) | ~agent(V_979, X_982, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_979, skc9) | ~mia_forename(V_979, skc9) | ~proposition(V_979, V_534) | ~theme(V_979, X_982, V_534) | ~accessible_world(V_979, V_534) | ~desire_want(V_979, X_982) | ~present(V_979, X_982) | ~of(V_979, V_978, W_977) | ~man(V_979, W_977) | ~forename(V_979, V_978) | ~vincent_forename(V_979, V_978) | ~accessible_world(skc6, V_979) | ~accessible_world(skc8, V_534)))). % 16.55/5.86 tff(c_2509, plain, (![V_978, W_977, V_979, X_982, V_534]: (accessible_world(V_979, skf4(W_977, V_979)) | ~actual_world(V_979) | ~woman(V_979, skc10) | ~agent(V_979, X_982, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_979, skc9) | ~mia_forename(V_979, skc9) | ~proposition(V_979, V_534) | ~theme(V_979, X_982, V_534) | ~accessible_world(V_979, V_534) | ~desire_want(V_979, X_982) | ~present(V_979, X_982) | ~of(V_979, V_978, W_977) | ~man(V_979, W_977) | ~forename(V_979, V_978) | ~vincent_forename(V_979, V_978) | ~accessible_world(skc6, V_979) | ~accessible_world(skc6, V_534)))). % 16.55/5.86 tff(c_2822, plain, (![W_991, V_993, X_994, X3_995, V_992, V_534]: (present(V_993, skf3(V_993, X3_995)) | ~actual_world(V_993) | ~woman(V_993, skc10) | ~agent(V_993, X_994, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_993, skc9) | ~mia_forename(V_993, skc9) | ~proposition(V_993, V_534) | ~theme(V_993, X_994, V_534) | ~accessible_world(V_993, V_534) | ~desire_want(V_993, X_994) | ~present(V_993, X_994) | ~of(V_993, V_992, W_991) | ~man(V_993, W_991) | ~forename(V_993, V_992) | ~vincent_forename(V_993, V_992) | ~accessible_world(skc6, V_993) | ~accessible_world(skc8, V_534)))). % 16.55/5.86 tff(c_2838, plain, (![V_1001, V_1000, X_998, W_999, V_534]: (proposition(V_1000, skf4(W_999, V_1000)) | ~actual_world(V_1000) | ~woman(V_1000, skc10) | ~agent(V_1000, X_998, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1000, skc9) | ~mia_forename(V_1000, skc9) | ~proposition(V_1000, V_534) | ~theme(V_1000, X_998, V_534) | ~accessible_world(V_1000, V_534) | ~desire_want(V_1000, X_998) | ~present(V_1000, X_998) | ~of(V_1000, V_1001, W_999) | ~man(V_1000, W_999) | ~forename(V_1000, V_1001) | ~vincent_forename(V_1000, V_1001) | ~accessible_world(skc6, V_1000) | ~accessible_world(skc6, V_534)))). % 16.55/5.86 tff(c_2821, plain, (![W_991, V_993, X_994, X3_995, V_992, V_534]: (present(V_993, skf3(V_993, X3_995)) | ~actual_world(V_993) | ~woman(V_993, skc10) | ~agent(V_993, X_994, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_993, skc9) | ~mia_forename(V_993, skc9) | ~proposition(V_993, V_534) | ~theme(V_993, X_994, V_534) | ~accessible_world(V_993, V_534) | ~desire_want(V_993, X_994) | ~present(V_993, X_994) | ~of(V_993, V_992, W_991) | ~man(V_993, W_991) | ~forename(V_993, V_992) | ~vincent_forename(V_993, V_992) | ~accessible_world(skc6, V_993) | ~accessible_world(skc6, V_534)))). % 16.55/5.86 tff(c_5955, plain, (~proposition(skc6, skc7))). % 16.55/5.86 tff(c_2906, plain, (![W_1013, V_1008, X3_1011, V_1009, X_1012, V_534]: (desire_want(V_1009, skf3(V_1009, X3_1011)) | ~actual_world(V_1009) | ~woman(V_1009, skc10) | ~agent(V_1009, X_1012, skc10) | ~event(V_534, skc7) | ~present(V_534, skc7) | ~dance(V_534, skc7) | ~forename(V_1009, skc9) | ~mia_forename(V_1009, skc9) | ~proposition(V_1009, V_534) | ~theme(V_1009, X_1012, V_534) | ~accessible_world(V_1009, V_534) | ~desire_want(V_1009, X_1012) | ~present(V_1009, X_1012) | ~of(V_1009, V_1008, W_1013) | ~man(V_1009, W_1013) | ~forename(V_1009, V_1008) | ~vincent_forename(V_1009, V_1008) | ~accessible_world(skc6, V_1009) | ~accessible_world(skc6, V_534)))). % 16.55/5.86 tff(c_5938, plain, (~proposition(skc6, skc10))). % 16.55/5.86 tff(c_5937, plain, (~proposition(skc6, skc11))). % 16.55/5.86 tff(c_2839, plain, (![V_1001, V_1000, X_998, W_999, V_534]: (proposition(V_1000, skf4(W_999, V_1000)) | ~actual_world(V_1000) | ~woman(V_1000, skc10) | ~agent(V_1000, X_998, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1000, skc9) | ~mia_forename(V_1000, skc9) | ~proposition(V_1000, V_534) | ~theme(V_1000, X_998, V_534) | ~accessible_world(V_1000, V_534) | ~desire_want(V_1000, X_998) | ~present(V_1000, X_998) | ~of(V_1000, V_1001, W_999) | ~man(V_1000, W_999) | ~forename(V_1000, V_1001) | ~vincent_forename(V_1000, V_1001) | ~accessible_world(skc6, V_1000) | ~accessible_world(skc8, V_534)))). % 16.55/5.86 tff(c_5778, plain, (![V_567]: (~human_person(skc6, V_567) | ~event(skc6, V_567)))). % 16.55/5.86 tff(c_5743, plain, (![V_527]: (~human_person(skc6, V_527) | ~dance(skc6, V_527)))). % 16.55/5.86 tff(c_2907, plain, (![W_1013, V_1008, X3_1011, V_1009, X_1012, V_534]: (desire_want(V_1009, skf3(V_1009, X3_1011)) | ~actual_world(V_1009) | ~woman(V_1009, skc10) | ~agent(V_1009, X_1012, skc10) | ~event(V_534, skc11) | ~present(V_534, skc11) | ~dance(V_534, skc11) | ~forename(V_1009, skc9) | ~mia_forename(V_1009, skc9) | ~proposition(V_1009, V_534) | ~theme(V_1009, X_1012, V_534) | ~accessible_world(V_1009, V_534) | ~desire_want(V_1009, X_1012) | ~present(V_1009, X_1012) | ~of(V_1009, V_1008, W_1013) | ~man(V_1009, W_1013) | ~forename(V_1009, V_1008) | ~vincent_forename(V_1009, V_1008) | ~accessible_world(skc6, V_1009) | ~accessible_world(skc8, V_534)))). % 16.55/5.86 tff(c_5732, plain, (![V_678]: (~human_person(skc6, V_678) | ~desire_want(skc6, V_678)))). % 16.55/5.86 tff(c_5662, plain, (~human_person(skc6, skc7))). % 16.55/5.86 tff(c_5604, plain, (~human_person(skc6, skc11))). % 16.55/5.86 tff(c_4644, plain, (~dance(skc6, skc7))). % 16.55/5.86 tff(c_3557, plain, (![V_1117, X3_1118, V_1123, W_1122, X_1121]: (agent(skf4(W_1122, X3_1118), skf5(X3_1118, W_1122), W_1122) | ~actual_world(V_1117) | ~woman(V_1117, skc10) | ~agent(V_1117, X_1121, skc10) | ~forename(V_1117, skc9) | ~mia_forename(V_1117, skc9) | ~proposition(V_1117, skc8) | ~theme(V_1117, X_1121, skc8) | ~accessible_world(V_1117, skc8) | ~desire_want(V_1117, X_1121) | ~present(V_1117, X_1121) | ~of(V_1117, V_1123, W_1122) | ~man(V_1117, W_1122) | ~forename(V_1117, V_1123) | ~vincent_forename(V_1117, V_1123) | ~accessible_world(skc6, V_1117)))). % 16.55/5.86 tff(c_3466, plain, (![V_1097, W_1100, X_1096, V_1098]: (theme(V_1097, skf3(V_1097, W_1100), skf4(W_1100, V_1097)) | ~actual_world(V_1097) | ~woman(V_1097, skc10) | ~agent(V_1097, X_1096, skc10) | ~forename(V_1097, skc9) | ~mia_forename(V_1097, skc9) | ~proposition(V_1097, skc8) | ~theme(V_1097, X_1096, skc8) | ~accessible_world(V_1097, skc8) | ~desire_want(V_1097, X_1096) | ~present(V_1097, X_1096) | ~of(V_1097, V_1098, W_1100) | ~man(V_1097, W_1100) | ~forename(V_1097, V_1098) | ~vincent_forename(V_1097, V_1098) | ~accessible_world(skc6, V_1097)))). % 16.55/5.86 tff(c_3190, plain, (![X_1048, W_1049, V_1051, X3_1054, V_1050]: (event(skf4(W_1049, X3_1054), skf5(X3_1054, W_1049)) | ~actual_world(V_1050) | ~woman(V_1050, skc10) | ~agent(V_1050, X_1048, skc10) | ~forename(V_1050, skc9) | ~mia_forename(V_1050, skc9) | ~proposition(V_1050, skc8) | ~theme(V_1050, X_1048, skc8) | ~accessible_world(V_1050, skc8) | ~desire_want(V_1050, X_1048) | ~present(V_1050, X_1048) | ~of(V_1050, V_1051, W_1049) | ~man(V_1050, W_1049) | ~forename(V_1050, V_1051) | ~vincent_forename(V_1050, V_1051) | ~accessible_world(skc6, V_1050)))). % 16.55/5.86 tff(c_3344, plain, (![W_1071, V_1074, X3_1073, X_1077, V_1072]: (dance(skf4(W_1071, X3_1073), skf5(X3_1073, W_1071)) | ~actual_world(V_1072) | ~woman(V_1072, skc10) | ~agent(V_1072, X_1077, skc10) | ~forename(V_1072, skc9) | ~mia_forename(V_1072, skc9) | ~proposition(V_1072, skc8) | ~theme(V_1072, X_1077, skc8) | ~accessible_world(V_1072, skc8) | ~desire_want(V_1072, X_1077) | ~present(V_1072, X_1077) | ~of(V_1072, V_1074, W_1071) | ~man(V_1072, W_1071) | ~forename(V_1072, V_1074) | ~vincent_forename(V_1072, V_1074) | ~accessible_world(skc6, V_1072)))). % 16.55/5.86 tff(c_3066, plain, (![X_1035, V_1037, X3_1034, W_1038, V_1036]: (present(skf4(W_1038, X3_1034), skf5(X3_1034, W_1038)) | ~actual_world(V_1037) | ~woman(V_1037, skc10) | ~agent(V_1037, X_1035, skc10) | ~forename(V_1037, skc9) | ~mia_forename(V_1037, skc9) | ~proposition(V_1037, skc8) | ~theme(V_1037, X_1035, skc8) | ~accessible_world(V_1037, skc8) | ~desire_want(V_1037, X_1035) | ~present(V_1037, X_1035) | ~of(V_1037, V_1036, W_1038) | ~man(V_1037, W_1038) | ~forename(V_1037, V_1036) | ~vincent_forename(V_1037, V_1036) | ~accessible_world(skc6, V_1037)))). % 16.55/5.86 tff(c_2995, plain, (![V_1021, W_1025, X_1024, V_1020]: (agent(V_1021, skf3(V_1021, W_1025), W_1025) | ~actual_world(V_1021) | ~woman(V_1021, skc10) | ~agent(V_1021, X_1024, skc10) | ~forename(V_1021, skc9) | ~mia_forename(V_1021, skc9) | ~proposition(V_1021, skc8) | ~theme(V_1021, X_1024, skc8) | ~accessible_world(V_1021, skc8) | ~desire_want(V_1021, X_1024) | ~present(V_1021, X_1024) | ~of(V_1021, V_1020, W_1025) | ~man(V_1021, W_1025) | ~forename(V_1021, V_1020) | ~vincent_forename(V_1021, V_1020) | ~accessible_world(skc6, V_1021)))). % 16.55/5.86 tff(c_2842, plain, (![V_1000, W_999, X_998, V_1001]: (proposition(V_1000, skf4(W_999, V_1000)) | ~actual_world(V_1000) | ~woman(V_1000, skc10) | ~agent(V_1000, X_998, skc10) | ~forename(V_1000, skc9) | ~mia_forename(V_1000, skc9) | ~proposition(V_1000, skc8) | ~theme(V_1000, X_998, skc8) | ~accessible_world(V_1000, skc8) | ~desire_want(V_1000, X_998) | ~present(V_1000, X_998) | ~of(V_1000, V_1001, W_999) | ~man(V_1000, W_999) | ~forename(V_1000, V_1001) | ~vincent_forename(V_1000, V_1001) | ~accessible_world(skc6, V_1000)))). % 16.55/5.86 tff(c_2910, plain, (![W_1013, V_1008, X3_1011, V_1009, X_1012]: (desire_want(V_1009, skf3(V_1009, X3_1011)) | ~actual_world(V_1009) | ~woman(V_1009, skc10) | ~agent(V_1009, X_1012, skc10) | ~forename(V_1009, skc9) | ~mia_forename(V_1009, skc9) | ~proposition(V_1009, skc8) | ~theme(V_1009, X_1012, skc8) | ~accessible_world(V_1009, skc8) | ~desire_want(V_1009, X_1012) | ~present(V_1009, X_1012) | ~of(V_1009, V_1008, W_1013) | ~man(V_1009, W_1013) | ~forename(V_1009, V_1008) | ~vincent_forename(V_1009, V_1008) | ~accessible_world(skc6, V_1009)))). % 16.55/5.86 tff(c_2825, plain, (![W_991, V_993, X_994, X3_995, V_992]: (present(V_993, skf3(V_993, X3_995)) | ~actual_world(V_993) | ~woman(V_993, skc10) | ~agent(V_993, X_994, skc10) | ~forename(V_993, skc9) | ~mia_forename(V_993, skc9) | ~proposition(V_993, skc8) | ~theme(V_993, X_994, skc8) | ~accessible_world(V_993, skc8) | ~desire_want(V_993, X_994) | ~present(V_993, X_994) | ~of(V_993, V_992, W_991) | ~man(V_993, W_991) | ~forename(V_993, V_992) | ~vincent_forename(V_993, V_992) | ~accessible_world(skc6, V_993)))). % 16.55/5.86 tff(c_1323, plain, (![V_541, V_698, Y_697, X1_700, W_701, X3_696, X_694]: (agent(skf4(W_701, X3_696), skf5(X3_696, W_701), W_701) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_694, skc10) | ~event(Y_697, X1_700) | ~agent(Y_697, X1_700, skc10) | ~present(Y_697, X1_700) | ~dance(Y_697, X1_700) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_697) | ~theme(V_541, X_694, Y_697) | ~accessible_world(V_541, Y_697) | ~desire_want(V_541, X_694) | ~present(V_541, X_694) | ~of(V_541, V_698, W_701) | ~man(V_541, W_701) | ~forename(V_541, V_698) | ~vincent_forename(V_541, V_698) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1280, plain, (![V_689, V_541, X_685, W_686, X1_688, Y_687]: (theme(V_541, skf3(V_541, W_686), skf4(W_686, V_541)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_685, skc10) | ~event(Y_687, X1_688) | ~agent(Y_687, X1_688, skc10) | ~present(Y_687, X1_688) | ~dance(Y_687, X1_688) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_687) | ~theme(V_541, X_685, Y_687) | ~accessible_world(V_541, Y_687) | ~desire_want(V_541, X_685) | ~present(V_541, X_685) | ~of(V_541, V_689, W_686) | ~man(V_541, W_686) | ~forename(V_541, V_689) | ~vincent_forename(V_541, V_689) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1181, plain, (![X_639, V_541, Y_644, W_638, X3_640, X1_637, V_642]: (dance(skf4(W_638, X3_640), skf5(X3_640, W_638)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_639, skc10) | ~event(Y_644, X1_637) | ~agent(Y_644, X1_637, skc10) | ~present(Y_644, X1_637) | ~dance(Y_644, X1_637) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_644) | ~theme(V_541, X_639, Y_644) | ~accessible_world(V_541, Y_644) | ~desire_want(V_541, X_639) | ~present(V_541, X_639) | ~of(V_541, V_642, W_638) | ~man(V_541, W_638) | ~forename(V_541, V_642) | ~vincent_forename(V_541, V_642) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1228, plain, (![X1_669, V_541, X3_672, X_670, W_668, V_665, Y_671]: (event(skf4(W_668, X3_672), skf5(X3_672, W_668)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_670, skc10) | ~event(Y_671, X1_669) | ~agent(Y_671, X1_669, skc10) | ~present(Y_671, X1_669) | ~dance(Y_671, X1_669) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_671) | ~theme(V_541, X_670, Y_671) | ~accessible_world(V_541, Y_671) | ~desire_want(V_541, X_670) | ~present(V_541, X_670) | ~of(V_541, V_665, W_668) | ~man(V_541, W_668) | ~forename(V_541, V_665) | ~vincent_forename(V_541, V_665) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1206, plain, (![V_541, Y_657, X3_652, W_650, X_658, V_654, X1_656]: (present(skf4(W_650, X3_652), skf5(X3_652, W_650)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_658, skc10) | ~event(Y_657, X1_656) | ~agent(Y_657, X1_656, skc10) | ~present(Y_657, X1_656) | ~dance(Y_657, X1_656) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_657) | ~theme(V_541, X_658, Y_657) | ~accessible_world(V_541, Y_657) | ~desire_want(V_541, X_658) | ~present(V_541, X_658) | ~of(V_541, V_654, W_650) | ~man(V_541, W_650) | ~forename(V_541, V_654) | ~vincent_forename(V_541, V_654) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1152, plain, (![V_541, Y_629, W_628, X1_633, V_631, X_627]: (agent(V_541, skf3(V_541, W_628), W_628) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_627, skc10) | ~event(Y_629, X1_633) | ~agent(Y_629, X1_633, skc10) | ~present(Y_629, X1_633) | ~dance(Y_629, X1_633) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_629) | ~theme(V_541, X_627, Y_629) | ~accessible_world(V_541, Y_629) | ~desire_want(V_541, X_627) | ~present(V_541, X_627) | ~of(V_541, V_631, W_628) | ~man(V_541, W_628) | ~forename(V_541, V_631) | ~vincent_forename(V_541, V_631) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1068, plain, (![X_606, V_541, X3_604, X1_610, W_602, Y_605, V_603]: (desire_want(V_541, skf3(V_541, X3_604)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_606, skc10) | ~event(Y_605, X1_610) | ~agent(Y_605, X1_610, skc10) | ~present(Y_605, X1_610) | ~dance(Y_605, X1_610) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_605) | ~theme(V_541, X_606, Y_605) | ~accessible_world(V_541, Y_605) | ~desire_want(V_541, X_606) | ~present(V_541, X_606) | ~of(V_541, V_603, W_602) | ~man(V_541, W_602) | ~forename(V_541, V_603) | ~vincent_forename(V_541, V_603) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_990, plain, (![V_541, Y_577, W_580, X1_576, X_579, V_578]: (proposition(V_541, skf4(W_580, V_541)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_579, skc10) | ~event(Y_577, X1_576) | ~agent(Y_577, X1_576, skc10) | ~present(Y_577, X1_576) | ~dance(Y_577, X1_576) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_577) | ~theme(V_541, X_579, Y_577) | ~accessible_world(V_541, Y_577) | ~desire_want(V_541, X_579) | ~present(V_541, X_579) | ~of(V_541, V_578, W_580) | ~man(V_541, W_580) | ~forename(V_541, V_578) | ~vincent_forename(V_541, V_578) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_1023, plain, (![X_586, V_541, X1_584, X3_587, V_592, Y_589, W_590]: (present(V_541, skf3(V_541, X3_587)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_586, skc10) | ~event(Y_589, X1_584) | ~agent(Y_589, X1_584, skc10) | ~present(Y_589, X1_584) | ~dance(Y_589, X1_584) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_589) | ~theme(V_541, X_586, Y_589) | ~accessible_world(V_541, Y_589) | ~desire_want(V_541, X_586) | ~present(V_541, X_586) | ~of(V_541, V_592, W_590) | ~man(V_541, W_590) | ~forename(V_541, V_592) | ~vincent_forename(V_541, V_592) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_2811, plain, (~vincent_forename(skc8, skc9))). % 16.55/5.86 tff(c_2522, plain, (![V_523, W_984, V_986]: (accessible_world(V_523, skf4(W_984, V_523)) | ~actual_world(V_523) | ~woman(V_523, skc10) | ~agent(V_523, skc7, skc10) | ~forename(V_523, skc9) | ~mia_forename(V_523, skc9) | ~proposition(V_523, skc8) | ~accessible_world(V_523, skc8) | ~desire_want(V_523, skc7) | ~present(V_523, skc7) | ~of(V_523, V_986, W_984) | ~man(V_523, W_984) | ~forename(V_523, V_986) | ~vincent_forename(V_523, V_986) | ~accessible_world(skc6, V_523)))). % 16.55/5.86 tff(c_2513, plain, (![V_979, W_977, X_982, V_978]: (accessible_world(V_979, skf4(W_977, V_979)) | ~actual_world(V_979) | ~woman(V_979, skc10) | ~agent(V_979, X_982, skc10) | ~forename(V_979, skc9) | ~mia_forename(V_979, skc9) | ~proposition(V_979, skc8) | ~theme(V_979, X_982, skc8) | ~accessible_world(V_979, skc8) | ~desire_want(V_979, X_982) | ~present(V_979, X_982) | ~of(V_979, V_978, W_977) | ~man(V_979, W_977) | ~forename(V_979, V_978) | ~vincent_forename(V_979, V_978) | ~accessible_world(skc6, V_979)))). % 16.55/5.86 tff(c_1097, plain, (![V_541, X1_617, X_622, V_619, Y_618, W_623]: (accessible_world(V_541, skf4(W_623, V_541)) | ~actual_world(V_541) | ~woman(V_541, skc10) | ~agent(V_541, X_622, skc10) | ~event(Y_618, X1_617) | ~agent(Y_618, X1_617, skc10) | ~present(Y_618, X1_617) | ~dance(Y_618, X1_617) | ~forename(V_541, skc9) | ~mia_forename(V_541, skc9) | ~proposition(V_541, Y_618) | ~theme(V_541, X_622, Y_618) | ~accessible_world(V_541, Y_618) | ~desire_want(V_541, X_622) | ~present(V_541, X_622) | ~of(V_541, V_619, W_623) | ~man(V_541, W_623) | ~forename(V_541, V_619) | ~vincent_forename(V_541, V_619) | ~accessible_world(skc6, V_541)))). % 16.55/5.86 tff(c_2055, plain, (![V_148, V_830, V_829]: (living(V_148, V_830) | ~accessible_world(V_829, V_148) | ~accessible_world(skc8, V_829) | ~human_person(skc6, V_830)))). % 16.55/5.86 tff(c_2100, plain, (![V_109, V_840, V_839]: (relation(V_109, V_840) | ~accessible_world(V_839, V_109) | ~accessible_world(skc8, V_839) | ~forename(skc6, V_840)))). % 16.55/5.86 tff(c_2171, plain, (![V_88, V_856, V_855]: (singleton(V_88, V_856) | ~accessible_world(V_855, V_88) | ~accessible_world(skc8, V_855) | ~eventuality(skc6, V_856)))). % 16.55/5.86 tff(c_928, plain, (![W_561, V_523, V_563]: (skc8=W_561 | ~desire_want(V_523, skc7) | ~proposition(V_523, skc8) | ~proposition(V_523, W_561) | ~desire_want(V_523, V_563) | ~theme(V_523, V_563, W_561) | ~accessible_world(skc6, V_523)))). % 16.55/5.86 tff(c_2085, plain, (![V_145, V_836, V_835]: (impartial(V_145, V_836) | ~accessible_world(V_835, V_145) | ~accessible_world(skc8, V_835) | ~human_person(skc6, V_836)))). % 16.55/5.86 tff(c_2210, plain, (![V_88, V_866, V_865]: (singleton(V_88, V_866) | ~accessible_world(V_865, V_88) | ~accessible_world(skc8, V_865) | ~abstraction(skc6, V_866)))). % 16.55/5.86 tff(c_1994, plain, (![V_88, V_820, V_819]: (singleton(V_88, V_820) | ~accessible_world(V_819, V_88) | ~accessible_world(skc8, V_819) | ~entity(skc6, V_820)))). % 16.55/5.86 tff(c_1713, plain, (![V_97, V_786, V_785]: (unisex(V_97, V_786) | ~accessible_world(V_785, V_97) | ~accessible_world(skc8, V_785) | ~abstraction(skc6, V_786)))). % 16.55/5.86 tff(c_1807, plain, (![V_118, V_796, V_795]: (general(V_118, V_796) | ~accessible_world(V_795, V_118) | ~accessible_world(skc8, V_795) | ~abstraction(skc6, V_796)))). % 16.55/5.86 tff(c_1935, plain, (![V_79, V_812, V_811]: (event(V_79, V_812) | ~accessible_world(V_811, V_79) | ~accessible_world(skc8, V_811) | ~desire_want(skc6, V_812)))). % 16.55/5.87 tff(c_1959, plain, (![V_91, V_816, V_815]: (specific(V_91, V_816) | ~accessible_world(V_815, V_91) | ~accessible_world(skc8, V_815) | ~entity(skc6, V_816)))). % 16.55/5.87 tff(c_1849, plain, (![V_124, V_806, V_805]: (relname(V_124, V_806) | ~accessible_world(V_805, V_124) | ~accessible_world(skc8, V_805) | ~forename(skc6, V_806)))). % 16.55/5.87 tff(c_1829, plain, (![V_142, V_800, V_799]: (existent(V_142, V_800) | ~accessible_world(V_799, V_142) | ~accessible_world(skc8, V_799) | ~entity(skc6, V_800)))). % 16.55/5.87 tff(c_889, plain, (![W_552, V_541]: (skc9=W_552 | ~entity(V_541, skc10) | ~forename(V_541, W_552) | ~of(V_541, W_552, skc10) | ~forename(V_541, skc9) | ~accessible_world(skc6, V_541)))). % 16.55/5.87 tff(c_1674, plain, (![V_91, V_778, V_777]: (specific(V_91, V_778) | ~accessible_world(V_777, V_91) | ~accessible_world(skc8, V_777) | ~eventuality(skc6, V_778)))). % 16.55/5.87 tff(c_1737, plain, (![V_115, V_790, V_789]: (nonhuman(V_115, V_790) | ~accessible_world(V_789, V_115) | ~accessible_world(skc8, V_789) | ~abstraction(skc6, V_790)))). % 16.55/5.87 tff(c_1682, plain, (![V_85, V_780, V_779]: (thing(V_85, V_780) | ~accessible_world(V_779, V_85) | ~accessible_world(skc8, V_779) | ~abstraction(skc6, V_780)))). % 16.55/5.87 tff(c_1816, plain, (![V_109, V_798, V_797]: (relation(V_109, V_798) | ~accessible_world(V_797, V_109) | ~accessible_world(skc8, V_797) | ~proposition(skc6, V_798)))). % 16.55/5.87 tff(c_1786, plain, (![V_85, V_794, V_793]: (thing(V_85, V_794) | ~accessible_world(V_793, V_85) | ~accessible_world(skc8, V_793) | ~entity(skc6, V_794)))). % 16.55/5.87 tff(c_1841, plain, (![V_94, V_804, V_803]: (nonexistent(V_94, V_804) | ~accessible_world(V_803, V_94) | ~accessible_world(skc8, V_803) | ~eventuality(skc6, V_804)))). % 16.55/5.87 tff(c_1778, plain, (![V_79, V_792, V_791]: (event(V_79, V_792) | ~accessible_world(V_791, V_79) | ~accessible_world(skc8, V_791) | ~dance(skc6, V_792)))). % 16.55/5.87 tff(c_1887, plain, (![V_82, V_808, V_807]: (eventuality(V_82, V_808) | ~accessible_world(V_807, V_82) | ~accessible_world(skc8, V_807) | ~event(skc6, V_808)))). % 16.55/5.87 tff(c_1690, plain, (![V_85, V_782, V_781]: (thing(V_85, V_782) | ~accessible_world(V_781, V_85) | ~accessible_world(skc8, V_781) | ~eventuality(skc6, V_782)))). % 16.55/5.87 tff(c_1701, plain, (![V_97, V_784, V_783]: (unisex(V_97, V_784) | ~accessible_world(V_783, V_97) | ~accessible_world(skc8, V_783) | ~eventuality(skc6, V_784)))). % 16.55/5.87 tff(c_1949, plain, (![V_136, V_814, V_813]: (organism(V_136, V_814) | ~accessible_world(V_813, V_136) | ~accessible_world(skc8, V_813) | ~human_person(skc6, V_814)))). % 16.55/5.87 tff(c_865, plain, (![V_177, V_546]: (of(V_177, skc9, skc10) | ~accessible_world(V_546, V_177) | ~accessible_world(skc6, V_546)))). % 16.55/5.87 tff(c_853, plain, (![V_169, V_540]: (agent(V_169, skc11, skc10) | ~accessible_world(V_540, V_169) | ~accessible_world(skc8, V_540)))). % 16.55/5.87 tff(c_818, plain, (![V_173, V_530]: (theme(V_173, skc7, skc8) | ~accessible_world(V_530, V_173) | ~accessible_world(skc6, V_530)))). % 16.55/5.87 tff(c_861, plain, (![V_169, V_545]: (agent(V_169, skc7, skc10) | ~accessible_world(V_545, V_169) | ~accessible_world(skc6, V_545)))). % 16.55/5.87 tff(c_2307, plain, (![U_1, V_2]: (~accessible_world(skc8, U_1) | ~entity(skc6, V_2) | ~dance(U_1, V_2)))). % 16.55/5.87 tff(c_2308, plain, (![U_15, V_16]: (~accessible_world(skc8, U_15) | ~entity(skc6, V_16) | ~desire_want(U_15, V_16)))). % 16.55/5.87 tff(c_1481, plain, (![V_139, V_712]: (entity(V_139, skc10) | ~accessible_world(V_712, V_139) | ~accessible_world(skc8, V_712)))). % 16.55/5.87 tff(c_2273, plain, (![U_1, V_2]: (~accessible_world(skc8, U_1) | ~abstraction(skc6, V_2) | ~dance(U_1, V_2)))). % 16.55/5.87 tff(c_2274, plain, (![U_15, V_16]: (~accessible_world(skc8, U_15) | ~abstraction(skc6, V_16) | ~desire_want(U_15, V_16)))). % 16.55/5.87 tff(c_2081, plain, (![U_45, V_46]: (~accessible_world(skc8, U_45) | ~eventuality(skc6, V_46) | ~entity(U_45, V_46)))). % 16.55/5.87 tff(c_2149, plain, (![U_25, V_26]: (~accessible_world(skc8, U_25) | ~entity(skc6, V_26) | ~abstraction(U_25, V_26)))). % 16.55/5.87 tff(c_2206, plain, (![U_3, V_4]: (~accessible_world(skc8, U_3) | ~entity(skc6, V_4) | ~event(U_3, V_4)))). % 16.55/5.87 tff(c_2101, plain, (![V_839, V_840]: (abstraction(V_839, V_840) | ~accessible_world(skc8, V_839) | ~forename(skc6, V_840)))). % 16.55/5.87 tff(c_2127, plain, (![U_3, V_4]: (~accessible_world(skc8, U_3) | ~abstraction(skc6, V_4) | ~event(U_3, V_4)))). % 16.55/5.87 tff(c_2223, plain, (![U_25, V_26]: (~accessible_world(skc8, U_25) | ~eventuality(skc6, V_26) | ~abstraction(U_25, V_26)))). % 16.55/5.87 tff(c_1808, plain, (![V_795, V_796]: (~entity(V_795, V_796) | ~accessible_world(skc8, V_795) | ~abstraction(skc6, V_796)))). % 16.55/5.87 tff(c_1714, plain, (![V_785, V_786]: (~male(V_785, V_786) | ~accessible_world(skc8, V_785) | ~abstraction(skc6, V_786)))). % 16.55/5.87 tff(c_1675, plain, (![V_777, V_778]: (~general(V_777, V_778) | ~accessible_world(skc8, V_777) | ~eventuality(skc6, V_778)))). % 16.55/5.87 tff(c_1683, plain, (![V_779, V_780]: (singleton(V_779, V_780) | ~accessible_world(skc8, V_779) | ~abstraction(skc6, V_780)))). % 16.55/5.87 tff(c_1830, plain, (![V_799, V_800]: (~eventuality(V_799, V_800) | ~accessible_world(skc8, V_799) | ~entity(skc6, V_800)))). % 16.55/5.87 tff(c_1776, plain, (![V_791, V_792]: (~entity(V_791, V_792) | ~accessible_world(skc8, V_791) | ~dance(skc6, V_792)))). % 16.55/5.87 tff(c_1702, plain, (![V_783, V_784]: (~male(V_783, V_784) | ~accessible_world(skc8, V_783) | ~eventuality(skc6, V_784)))). % 16.55/5.87 tff(c_599, plain, (![V_449, V_423]: (human(V_449, skc10) | ~accessible_world(V_423, V_449) | ~accessible_world(skc6, V_423)))). % 16.55/5.87 tff(c_1691, plain, (![V_781, V_782]: (singleton(V_781, V_782) | ~accessible_world(skc8, V_781) | ~eventuality(skc6, V_782)))). % 16.55/5.87 tff(c_1777, plain, (![V_791, V_792]: (~abstraction(V_791, V_792) | ~accessible_world(skc8, V_791) | ~dance(skc6, V_792)))). % 16.55/5.87 tff(c_772, plain, (![V_517, V_423]: (entity(V_517, skc10) | ~accessible_world(V_423, V_517) | ~accessible_world(skc6, V_423)))). % 16.55/5.87 tff(c_1960, plain, (![V_815, V_816]: (~general(V_815, V_816) | ~accessible_world(skc8, V_815) | ~entity(skc6, V_816)))). % 16.55/5.87 tff(c_1715, plain, (![V_785, V_786]: (~female(V_785, V_786) | ~accessible_world(skc8, V_785) | ~abstraction(skc6, V_786)))). % 16.55/5.87 tff(c_1809, plain, (![V_795, V_796]: (~eventuality(V_795, V_796) | ~accessible_world(skc8, V_795) | ~abstraction(skc6, V_796)))). % 16.55/5.87 tff(c_1703, plain, (![V_783, V_784]: (~female(V_783, V_784) | ~accessible_world(skc8, V_783) | ~eventuality(skc6, V_784)))). % 16.55/5.87 tff(c_486, plain, (![V_154, V_419]: (animate(V_154, skc10) | ~accessible_world(V_419, V_154) | ~accessible_world(skc6, V_419)))). % 16.55/5.87 tff(c_1850, plain, (![V_805, V_806]: (relation(V_805, V_806) | ~accessible_world(skc8, V_805) | ~forename(skc6, V_806)))). % 16.55/5.87 tff(c_1952, plain, (![V_813, V_814]: (entity(V_813, V_814) | ~accessible_world(skc8, V_813) | ~human_person(skc6, V_814)))). % 16.55/5.87 tff(c_1951, plain, (![V_813, V_814]: (impartial(V_813, V_814) | ~accessible_world(skc8, V_813) | ~human_person(skc6, V_814)))). % 16.55/5.87 tff(c_1842, plain, (![V_803, V_804]: (~existent(V_803, V_804) | ~accessible_world(skc8, V_803) | ~eventuality(skc6, V_804)))). % 16.55/5.87 tff(c_1889, plain, (![V_807, V_808]: (~entity(V_807, V_808) | ~accessible_world(skc8, V_807) | ~event(skc6, V_808)))). % 16.55/5.87 tff(c_1396, plain, (![V_148, V_709]: (living(V_148, V_709) | ~accessible_world(skc8, V_148) | ~human_person(skc6, V_709)))). % 16.55/5.87 tff(c_1738, plain, (![V_789, V_790]: (~human(V_789, V_790) | ~accessible_world(skc8, V_789) | ~abstraction(skc6, V_790)))). % 16.55/5.87 tff(c_1934, plain, (![V_811, V_812]: (~abstraction(V_811, V_812) | ~accessible_world(skc8, V_811) | ~desire_want(skc6, V_812)))). % 16.55/5.87 tff(c_1933, plain, (![V_811, V_812]: (~entity(V_811, V_812) | ~accessible_world(skc8, V_811) | ~desire_want(skc6, V_812)))). % 16.55/5.87 tff(c_1817, plain, (![V_797, V_798]: (abstraction(V_797, V_798) | ~accessible_world(skc8, V_797) | ~proposition(skc6, V_798)))). % 16.55/5.87 tff(c_2011, plain, (~desire_want(skc6, skc8))). % 16.55/5.87 tff(c_2010, plain, (~dance(skc6, skc8))). % 16.55/5.87 tff(c_1995, plain, (~event(skc6, skc8))). % 16.55/5.87 tff(c_1787, plain, (![V_793, V_794]: (singleton(V_793, V_794) | ~accessible_world(skc8, V_793) | ~entity(skc6, V_794)))). % 16.55/5.87 tff(c_1990, plain, (~desire_want(skc6, skc9))). % 16.55/5.87 tff(c_1989, plain, (~dance(skc6, skc9))). % 16.55/5.87 tff(c_1974, plain, (~event(skc6, skc9))). % 16.55/5.87 tff(c_1890, plain, (![V_807, V_808]: (~abstraction(V_807, V_808) | ~accessible_world(skc8, V_807) | ~event(skc6, V_808)))). % 16.55/5.87 tff(c_1000, plain, (![V_91, V_581]: (specific(V_91, V_581) | ~accessible_world(skc8, V_91) | ~entity(skc6, V_581)))). % 16.55/5.87 tff(c_1389, plain, (![V_136, V_708]: (organism(V_136, V_708) | ~accessible_world(skc8, V_136) | ~human_person(skc6, V_708)))). % 16.55/5.87 tff(c_1270, plain, (![V_79, V_678]: (event(V_79, V_678) | ~accessible_world(skc8, V_79) | ~desire_want(skc6, V_678)))). % 16.55/5.87 tff(c_503, plain, (![V_133, V_423]: (human_person(V_133, skc10) | ~accessible_world(V_423, V_133) | ~accessible_world(skc6, V_423)))). % 16.55/5.87 tff(c_949, plain, (![V_82, V_567]: (eventuality(V_82, V_567) | ~accessible_world(skc8, V_82) | ~event(skc6, V_567)))). % 16.55/5.87 tff(c_1037, plain, (![V_124, V_596]: (relname(V_124, V_596) | ~accessible_world(skc8, V_124) | ~forename(skc6, V_596)))). % 16.55/5.87 tff(c_876, plain, (![V_94, V_550]: (nonexistent(V_94, V_550) | ~accessible_world(skc8, V_94) | ~eventuality(skc6, V_550)))). % 16.55/5.87 tff(c_574, plain, (![V_157, V_446]: (female(V_157, skc10) | ~accessible_world(V_446, V_157) | ~accessible_world(skc6, V_446)))). % 16.55/5.87 tff(c_1111, plain, (![V_142, V_624]: (existent(V_142, V_624) | ~accessible_world(skc8, V_142) | ~entity(skc6, V_624)))). % 16.55/5.87 tff(c_836, plain, (![V_109, V_538]: (relation(V_109, V_538) | ~accessible_world(skc8, V_109) | ~proposition(skc6, V_538)))). % 16.55/5.87 tff(c_1297, plain, (![V_118, V_690]: (general(V_118, V_690) | ~accessible_world(skc8, V_118) | ~abstraction(skc6, V_690)))). % 16.55/5.87 tff(c_1238, plain, (![V_85, V_673]: (thing(V_85, V_673) | ~accessible_world(skc8, V_85) | ~entity(skc6, V_673)))). % 16.55/5.87 tff(c_800, plain, (![V_79, V_527]: (event(V_79, V_527) | ~accessible_world(skc8, V_79) | ~dance(skc6, V_527)))). % 16.55/5.87 tff(c_1078, plain, (![V_115, V_611]: (nonhuman(V_115, V_611) | ~accessible_world(skc8, V_115) | ~abstraction(skc6, V_611)))). % 16.55/5.87 tff(c_1730, plain, (~vincent_forename(skc6, skc9))). % 16.55/5.87 tff(c_1650, plain, (![V_592, W_590]: (~of(skc6, V_592, W_590) | ~man(skc6, W_590) | ~forename(skc6, V_592) | ~vincent_forename(skc6, V_592)))). % 16.55/5.87 tff(c_1198, plain, (![V_97, V_649]: (unisex(V_97, V_649) | ~accessible_world(skc8, V_97) | ~abstraction(skc6, V_649)))). % 16.55/5.87 tff(c_1545, plain, (![V_97, V_730]: (unisex(V_97, V_730) | ~accessible_world(skc8, V_97) | ~eventuality(skc6, V_730)))). % 16.55/5.88 tff(c_1558, plain, (![V_85, V_734]: (thing(V_85, V_734) | ~accessible_world(skc8, V_85) | ~eventuality(skc6, V_734)))). % 16.55/5.88 tff(c_1525, plain, (![V_85, V_724]: (thing(V_85, V_724) | ~accessible_world(skc8, V_85) | ~abstraction(skc6, V_724)))). % 16.55/5.88 tff(c_1497, plain, (![V_91, V_718]: (specific(V_91, V_718) | ~accessible_world(skc8, V_91) | ~eventuality(skc6, V_718)))). % 16.55/5.88 tff(c_382, plain, (![V_145, V_378, U_377]: (impartial(V_145, V_378) | ~accessible_world(U_377, V_145) | ~human_person(U_377, V_378)))). % 16.55/5.88 tff(c_744, plain, (![V_504, V_282, U_281]: (singleton(V_504, V_282) | ~accessible_world(U_281, V_504) | ~entity(U_281, V_282)))). % 16.55/5.88 tff(c_395, plain, (![V_79, V_384]: (event(V_79, skc11) | ~accessible_world(V_384, V_79) | ~accessible_world(skc8, V_384)))). % 16.55/5.88 tff(c_647, plain, (![V_103, V_474]: (desire_want(V_103, skc7) | ~accessible_world(V_474, V_103) | ~accessible_world(skc6, V_474)))). % 16.55/5.88 tff(c_371, plain, (![V_76, V_370]: (dance(V_76, skc11) | ~accessible_world(V_370, V_76) | ~accessible_world(skc8, V_370)))). % 16.55/5.88 tff(c_621, plain, (![V_100, V_461]: (present(V_100, skc7) | ~accessible_world(V_461, V_100) | ~accessible_world(skc6, V_461)))). % 16.55/5.88 tff(c_892, plain, (![W_552]: (skc9=W_552 | ~forename(skc6, W_552) | ~of(skc6, W_552, skc10)))). % 16.55/5.88 tff(c_386, plain, (![V_379, V_38, U_37]: (living(V_379, V_38) | ~accessible_world(U_37, V_379) | ~human_person(U_37, V_38)))). % 16.55/5.88 tff(c_685, plain, (![V_130, V_488]: (woman(V_130, skc10) | ~accessible_world(V_488, V_130) | ~accessible_world(skc6, V_488)))). % 16.55/5.88 tff(c_715, plain, (![V_121, V_497]: (forename(V_121, skc9) | ~accessible_world(V_497, V_121) | ~accessible_world(skc6, V_497)))). % 16.55/5.88 tff(c_617, plain, (![V_100, V_460]: (present(V_100, skc11) | ~accessible_world(V_460, V_100) | ~accessible_world(skc8, V_460)))). % 16.55/5.88 tff(c_757, plain, (![V_127, V_510]: (mia_forename(V_127, skc9) | ~accessible_world(V_510, V_127) | ~accessible_world(skc6, V_510)))). % 16.55/5.88 tff(c_764, plain, (![V_511, V_320, U_319]: (relation(V_511, V_320) | ~accessible_world(U_319, V_511) | ~forename(U_319, V_320)))). % 16.55/5.88 tff(c_931, plain, (![W_561, V_563]: (skc8=W_561 | ~proposition(skc6, W_561) | ~desire_want(skc6, V_563) | ~theme(skc6, V_563, W_561)))). % 16.55/5.88 tff(c_745, plain, (![V_504, V_334, U_333]: (singleton(V_504, V_334) | ~accessible_world(U_333, V_504) | ~abstraction(U_333, V_334)))). % 16.55/5.88 tff(c_1581, plain, (~accessible_world(skc6, skc6))). % 16.55/5.88 tff(c_698, plain, (![V_106, V_492]: (proposition(V_106, skc8) | ~accessible_world(V_492, V_106) | ~accessible_world(skc6, V_492)))). % 16.55/5.88 tff(c_746, plain, (![V_504, V_342, U_341]: (singleton(V_504, V_342) | ~accessible_world(U_341, V_504) | ~eventuality(U_341, V_342)))). % 16.55/5.88 tff(c_1559, plain, (![V_734]: (singleton(skc8, V_734) | ~eventuality(skc6, V_734)))). % 16.55/5.88 tff(c_1547, plain, (![V_730]: (~female(skc8, V_730) | ~eventuality(skc6, V_730)))). % 16.55/5.88 tff(c_1546, plain, (![V_730]: (~male(skc8, V_730) | ~eventuality(skc6, V_730)))). % 16.55/5.88 tff(c_1551, plain, (![V_732]: (thing(skc8, V_732) | ~eventuality(skc6, V_732)))). % 16.55/5.88 tff(c_665, plain, (![V_479, V_6, U_5]: (thing(V_479, V_6) | ~accessible_world(U_5, V_479) | ~eventuality(U_5, V_6)))). % 16.55/5.88 tff(c_1535, plain, (![V_728]: (unisex(skc8, V_728) | ~eventuality(skc6, V_728)))). % 16.55/5.88 tff(c_433, plain, (![V_405, V_14, U_13]: (unisex(V_405, V_14) | ~accessible_world(U_13, V_405) | ~eventuality(U_13, V_14)))). % 16.55/5.88 tff(c_1484, plain, (![V_712]: (~abstraction(V_712, skc10) | ~accessible_world(skc8, V_712)))). % 16.55/5.88 tff(c_1526, plain, (![V_724]: (singleton(skc8, V_724) | ~abstraction(skc6, V_724)))). % 16.55/5.88 tff(c_1518, plain, (![V_722]: (thing(skc8, V_722) | ~abstraction(skc6, V_722)))). % 16.55/5.88 tff(c_666, plain, (![V_479, V_22, U_21]: (thing(V_479, V_22) | ~accessible_world(U_21, V_479) | ~abstraction(U_21, V_22)))). % 16.55/5.88 tff(c_1508, plain, (![V_26]: (~eventuality(skc6, V_26) | ~abstraction(skc8, V_26)))). % 16.55/5.88 tff(c_1498, plain, (![V_718]: (~general(skc8, V_718) | ~eventuality(skc6, V_718)))). % 16.55/5.88 tff(c_1490, plain, (![V_716]: (specific(skc8, V_716) | ~eventuality(skc6, V_716)))). % 16.55/5.88 tff(c_635, plain, (![V_468, V_10, U_9]: (specific(V_468, V_10) | ~accessible_world(U_9, V_468) | ~eventuality(U_9, V_10)))). % 16.55/5.88 tff(c_1483, plain, (![V_712]: (~dance(V_712, skc10) | ~accessible_world(skc8, V_712)))). % 16.55/5.88 tff(c_1482, plain, (![V_712]: (~desire_want(V_712, skc10) | ~accessible_world(skc8, V_712)))). % 16.55/5.88 tff(c_1434, plain, (![V_139]: (entity(V_139, skc10) | ~accessible_world(skc8, V_139)))). % 16.55/5.88 tff(c_1410, plain, (entity(skc8, skc10))). % 16.55/5.88 tff(c_1392, plain, (![V_708]: (entity(skc8, V_708) | ~human_person(skc6, V_708)))). % 16.55/5.88 tff(c_1391, plain, (![V_708]: (impartial(skc8, V_708) | ~human_person(skc6, V_708)))). % 16.55/5.88 tff(c_1390, plain, (![V_708]: (living(skc8, V_708) | ~human_person(skc6, V_708)))). % 16.55/5.88 tff(c_1376, plain, (![V_706]: (organism(skc8, V_706) | ~human_person(skc6, V_706)))). % 16.55/5.88 tff(c_530, plain, (![V_429, V_38, U_37]: (organism(V_429, V_38) | ~accessible_world(U_37, V_429) | ~human_person(U_37, V_38)))). % 16.55/5.88 tff(c_1353, plain, (![V_16]: (~abstraction(skc6, V_16) | ~desire_want(skc8, V_16)))). % 16.55/5.88 tff(c_1352, plain, (![V_2]: (~abstraction(skc6, V_2) | ~dance(skc8, V_2)))). % 16.55/5.88 tff(c_1354, plain, (~abstraction(skc6, skc11))). % 16.55/5.88 tff(c_1317, plain, (![V_4]: (~abstraction(skc6, V_4) | ~event(skc8, V_4)))). % 16.55/5.88 tff(c_194, plain, (![X1_262, U_260, Y_265, Z_261, X_264, X2_263, V_266, W_258, X3_259]: (agent(skf4(W_258, X3_259), skf5(X3_259, W_258), W_258) | ~actual_world(U_260) | ~of(U_260, Z_261, X2_263) | ~woman(U_260, X2_263) | ~agent(U_260, X_264, X2_263) | ~event(Y_265, X1_262) | ~agent(Y_265, X1_262, X2_263) | ~present(Y_265, X1_262) | ~dance(Y_265, X1_262) | ~forename(U_260, Z_261) | ~mia_forename(U_260, Z_261) | ~proposition(U_260, Y_265) | ~theme(U_260, X_264, Y_265) | ~accessible_world(U_260, Y_265) | ~desire_want(U_260, X_264) | ~present(U_260, X_264) | ~of(U_260, V_266, W_258) | ~man(U_260, W_258) | ~forename(U_260, V_266) | ~vincent_forename(U_260, V_266)))). % 16.55/5.88 tff(c_1299, plain, (![V_690]: (~eventuality(skc8, V_690) | ~abstraction(skc6, V_690)))). % 16.55/5.88 tff(c_1298, plain, (![V_690]: (~entity(skc8, V_690) | ~abstraction(skc6, V_690)))). % 16.55/5.88 tff(c_1274, plain, (![V_680]: (general(skc8, V_680) | ~abstraction(skc6, V_680)))). % 16.55/5.88 tff(c_196, plain, (![U_268, V_274, Z_269, X2_271, X1_270, X_272, Y_273, W_267]: (theme(U_268, skf3(U_268, W_267), skf4(W_267, U_268)) | ~actual_world(U_268) | ~of(U_268, Z_269, X2_271) | ~woman(U_268, X2_271) | ~agent(U_268, X_272, X2_271) | ~event(Y_273, X1_270) | ~agent(Y_273, X1_270, X2_271) | ~present(Y_273, X1_270) | ~dance(Y_273, X1_270) | ~forename(U_268, Z_269) | ~mia_forename(U_268, Z_269) | ~proposition(U_268, Y_273) | ~theme(U_268, X_272, Y_273) | ~accessible_world(U_268, Y_273) | ~desire_want(U_268, X_272) | ~present(U_268, X_272) | ~of(U_268, V_274, W_267) | ~man(U_268, W_267) | ~forename(U_268, V_274) | ~vincent_forename(U_268, V_274)))). % 16.55/5.88 tff(c_416, plain, (![V_396, V_26, U_25]: (general(V_396, V_26) | ~accessible_world(U_25, V_396) | ~abstraction(U_25, V_26)))). % 16.55/5.88 tff(c_1247, plain, (![V_676]: (event(skc8, V_676) | ~desire_want(skc6, V_676)))). % 16.55/5.88 tff(c_366, plain, (![V_367, V_16, U_15]: (event(V_367, V_16) | ~accessible_world(U_15, V_367) | ~desire_want(U_15, V_16)))). % 16.55/5.88 tff(c_1239, plain, (![V_673]: (singleton(skc8, V_673) | ~entity(skc6, V_673)))). % 16.55/5.88 tff(c_1222, plain, (![V_662]: (thing(skc8, V_662) | ~entity(skc6, V_662)))). % 16.55/5.88 tff(c_188, plain, (![Y_238, X2_236, X_237, Z_234, V_239, X3_232, W_231, U_233, X1_235]: (event(skf4(W_231, X3_232), skf5(X3_232, W_231)) | ~actual_world(U_233) | ~of(U_233, Z_234, X2_236) | ~woman(U_233, X2_236) | ~agent(U_233, X_237, X2_236) | ~event(Y_238, X1_235) | ~agent(Y_238, X1_235, X2_236) | ~present(Y_238, X1_235) | ~dance(Y_238, X1_235) | ~forename(U_233, Z_234) | ~mia_forename(U_233, Z_234) | ~proposition(U_233, Y_238) | ~theme(U_233, X_237, Y_238) | ~accessible_world(U_233, Y_238) | ~desire_want(U_233, X_237) | ~present(U_233, X_237) | ~of(U_233, V_239, W_231) | ~man(U_233, W_231) | ~forename(U_233, V_239) | ~vincent_forename(U_233, V_239)))). % 16.55/5.88 tff(c_667, plain, (![V_479, V_42, U_41]: (thing(V_479, V_42) | ~accessible_world(U_41, V_479) | ~entity(U_41, V_42)))). % 16.55/5.88 tff(c_1200, plain, (![V_649]: (~female(skc8, V_649) | ~abstraction(skc6, V_649)))). % 16.55/5.88 tff(c_1199, plain, (![V_649]: (~male(skc8, V_649) | ~abstraction(skc6, V_649)))). % 16.55/5.88 tff(c_192, plain, (![X1_253, W_249, V_257, X_255, Y_256, Z_252, X2_254, X3_250, U_251]: (present(skf4(W_249, X3_250), skf5(X3_250, W_249)) | ~actual_world(U_251) | ~of(U_251, Z_252, X2_254) | ~woman(U_251, X2_254) | ~agent(U_251, X_255, X2_254) | ~event(Y_256, X1_253) | ~agent(Y_256, X1_253, X2_254) | ~present(Y_256, X1_253) | ~dance(Y_256, X1_253) | ~forename(U_251, Z_252) | ~mia_forename(U_251, Z_252) | ~proposition(U_251, Y_256) | ~theme(U_251, X_255, Y_256) | ~accessible_world(U_251, Y_256) | ~desire_want(U_251, X_255) | ~present(U_251, X_255) | ~of(U_251, V_257, W_249) | ~man(U_251, W_249) | ~forename(U_251, V_257) | ~vincent_forename(U_251, V_257)))). % 16.55/5.88 tff(c_1188, plain, (![V_647]: (unisex(skc8, V_647) | ~abstraction(skc6, V_647)))). % 16.55/5.88 tff(c_434, plain, (![V_405, V_28, U_27]: (unisex(V_405, V_28) | ~accessible_world(U_27, V_405) | ~abstraction(U_27, V_28)))). % 16.55/5.88 tff(c_1175, plain, (~desire_want(skc8, skc10))). % 16.55/5.88 tff(c_190, plain, (![Y_247, U_242, X3_241, X1_244, Z_243, W_240, X_246, X2_245, V_248]: (dance(skf4(W_240, X3_241), skf5(X3_241, W_240)) | ~actual_world(U_242) | ~of(U_242, Z_243, X2_245) | ~woman(U_242, X2_245) | ~agent(U_242, X_246, X2_245) | ~event(Y_247, X1_244) | ~agent(Y_247, X1_244, X2_245) | ~present(Y_247, X1_244) | ~dance(Y_247, X1_244) | ~forename(U_242, Z_243) | ~mia_forename(U_242, Z_243) | ~proposition(U_242, Y_247) | ~theme(U_242, X_246, Y_247) | ~accessible_world(U_242, Y_247) | ~desire_want(U_242, X_246) | ~present(U_242, X_246) | ~of(U_242, V_248, W_240) | ~man(U_242, W_240) | ~forename(U_242, V_248) | ~vincent_forename(U_242, V_248)))). % 16.55/5.88 tff(c_1145, plain, (![V_16]: (~entity(skc6, V_16) | ~desire_want(skc8, V_16)))). % 16.55/5.88 tff(c_1165, plain, (~dance(skc8, skc10))). % 16.55/5.88 tff(c_1144, plain, (![V_2]: (~entity(skc6, V_2) | ~dance(skc8, V_2)))). % 16.55/5.88 tff(c_186, plain, (![U_224, X_228, X2_227, X1_226, V_230, Y_229, Z_225, W_223]: (agent(U_224, skf3(U_224, W_223), W_223) | ~actual_world(U_224) | ~of(U_224, Z_225, X2_227) | ~woman(U_224, X2_227) | ~agent(U_224, X_228, X2_227) | ~event(Y_229, X1_226) | ~agent(Y_229, X1_226, X2_227) | ~present(Y_229, X1_226) | ~dance(Y_229, X1_226) | ~forename(U_224, Z_225) | ~mia_forename(U_224, Z_225) | ~proposition(U_224, Y_229) | ~theme(U_224, X_228, Y_229) | ~accessible_world(U_224, Y_229) | ~desire_want(U_224, X_228) | ~present(U_224, X_228) | ~of(U_224, V_230, W_223) | ~man(U_224, W_223) | ~forename(U_224, V_230) | ~vincent_forename(U_224, V_230)))). % 16.55/5.88 tff(c_1146, plain, (~entity(skc6, skc11))). % 16.55/5.88 tff(c_1122, plain, (![V_4]: (~entity(skc6, V_4) | ~event(skc8, V_4)))). % 16.55/5.88 tff(c_1112, plain, (![V_624]: (~eventuality(skc8, V_624) | ~entity(skc6, V_624)))). % 16.55/5.88 tff(c_1091, plain, (![V_614]: (existent(skc8, V_614) | ~entity(skc6, V_614)))). % 16.55/5.88 tff(c_182, plain, (![W_207, U_208, Z_209, X2_211, X_212, Y_213, V_214, X1_210]: (accessible_world(U_208, skf4(W_207, U_208)) | ~actual_world(U_208) | ~of(U_208, Z_209, X2_211) | ~woman(U_208, X2_211) | ~agent(U_208, X_212, X2_211) | ~event(Y_213, X1_210) | ~agent(Y_213, X1_210, X2_211) | ~present(Y_213, X1_210) | ~dance(Y_213, X1_210) | ~forename(U_208, Z_209) | ~mia_forename(U_208, Z_209) | ~proposition(U_208, Y_213) | ~theme(U_208, X_212, Y_213) | ~accessible_world(U_208, Y_213) | ~desire_want(U_208, X_212) | ~present(U_208, X_212) | ~of(U_208, V_214, W_207) | ~man(U_208, W_207) | ~forename(U_208, V_214) | ~vincent_forename(U_208, V_214)))). % 16.55/5.88 tff(c_606, plain, (![V_454, V_46, U_45]: (existent(V_454, V_46) | ~accessible_world(U_45, V_454) | ~entity(U_45, V_46)))). % 16.55/5.88 tff(c_1079, plain, (![V_611]: (~human(skc8, V_611) | ~abstraction(skc6, V_611)))). % 16.55/5.88 tff(c_1062, plain, (![V_600]: (nonhuman(skc8, V_600) | ~abstraction(skc6, V_600)))). % 16.55/5.88 tff(c_180, plain, (![Y_205, X_204, X2_203, U_200, V_206, Z_201, X1_202, X3_199, W_198]: (desire_want(U_200, skf3(U_200, X3_199)) | ~actual_world(U_200) | ~of(U_200, Z_201, X2_203) | ~woman(U_200, X2_203) | ~agent(U_200, X_204, X2_203) | ~event(Y_205, X1_202) | ~agent(Y_205, X1_202, X2_203) | ~present(Y_205, X1_202) | ~dance(Y_205, X1_202) | ~forename(U_200, Z_201) | ~mia_forename(U_200, Z_201) | ~proposition(U_200, Y_205) | ~theme(U_200, X_204, Y_205) | ~accessible_world(U_200, Y_205) | ~desire_want(U_200, X_204) | ~present(U_200, X_204) | ~of(U_200, V_206, W_198) | ~man(U_200, W_198) | ~forename(U_200, V_206) | ~vincent_forename(U_200, V_206)))). % 16.55/5.88 tff(c_657, plain, (![V_476, V_24, U_23]: (nonhuman(V_476, V_24) | ~accessible_world(U_23, V_476) | ~abstraction(U_23, V_24)))). % 16.55/5.88 tff(c_1046, plain, (![V_597]: (abstraction(skc8, V_597) | ~forename(skc6, V_597)))). % 16.55/5.88 tff(c_1038, plain, (![V_596]: (relation(skc8, V_596) | ~forename(skc6, V_596)))). % 16.55/5.88 tff(c_1030, plain, (![V_594]: (relname(skc8, V_594) | ~forename(skc6, V_594)))). % 16.55/5.88 tff(c_629, plain, (![V_465, V_30, U_29]: (relname(V_465, V_30) | ~accessible_world(U_29, V_465) | ~forename(U_29, V_30)))). % 16.55/5.88 tff(c_178, plain, (![X1_193, Y_196, V_197, X_195, X3_190, W_189, Z_192, U_191, X2_194]: (present(U_191, skf3(U_191, X3_190)) | ~actual_world(U_191) | ~of(U_191, Z_192, X2_194) | ~woman(U_191, X2_194) | ~agent(U_191, X_195, X2_194) | ~event(Y_196, X1_193) | ~agent(Y_196, X1_193, X2_194) | ~present(Y_196, X1_193) | ~dance(Y_196, X1_193) | ~forename(U_191, Z_192) | ~mia_forename(U_191, Z_192) | ~proposition(U_191, Y_196) | ~theme(U_191, X_195, Y_196) | ~accessible_world(U_191, Y_196) | ~desire_want(U_191, X_195) | ~present(U_191, X_195) | ~of(U_191, V_197, W_189) | ~man(U_191, W_189) | ~forename(U_191, V_197) | ~vincent_forename(U_191, V_197)))). % 16.55/5.88 tff(c_1007, plain, (![V_26]: (~entity(skc6, V_26) | ~abstraction(skc8, V_26)))). % 16.55/5.88 tff(c_1001, plain, (![V_581]: (~general(skc8, V_581) | ~entity(skc6, V_581)))). % 16.55/5.88 tff(c_984, plain, (![V_571]: (specific(skc8, V_571) | ~entity(skc6, V_571)))). % 16.55/5.89 tff(c_184, plain, (![X2_219, W_215, X1_218, V_222, Z_217, Y_221, X_220, U_216]: (proposition(U_216, skf4(W_215, U_216)) | ~actual_world(U_216) | ~of(U_216, Z_217, X2_219) | ~woman(U_216, X2_219) | ~agent(U_216, X_220, X2_219) | ~event(Y_221, X1_218) | ~agent(Y_221, X1_218, X2_219) | ~present(Y_221, X1_218) | ~dance(Y_221, X1_218) | ~forename(U_216, Z_217) | ~mia_forename(U_216, Z_217) | ~proposition(U_216, Y_221) | ~theme(U_216, X_220, Y_221) | ~accessible_world(U_216, Y_221) | ~desire_want(U_216, X_220) | ~present(U_216, X_220) | ~of(U_216, V_222, W_215) | ~man(U_216, W_215) | ~forename(U_216, V_222) | ~vincent_forename(U_216, V_222)))). % 16.55/5.89 tff(c_636, plain, (![V_468, V_44, U_43]: (specific(V_468, V_44) | ~accessible_world(U_43, V_468) | ~entity(U_43, V_44)))). % 16.55/5.89 tff(c_970, plain, (![V_16]: (~abstraction(skc8, V_16) | ~desire_want(skc6, V_16)))). % 16.55/5.89 tff(c_954, plain, (![V_567]: (~abstraction(skc8, V_567) | ~event(skc6, V_567)))). % 16.55/5.89 tff(c_935, plain, (![V_565]: (eventuality(skc8, V_565) | ~event(skc6, V_565)))). % 16.55/5.89 tff(c_625, plain, (![V_462, V_4, U_3]: (eventuality(V_462, V_4) | ~accessible_world(U_3, V_462) | ~event(U_3, V_4)))). % 16.55/5.89 tff(c_146, plain, (![Y_187, U_185, X_186, V_188, W_184]: (X_186=W_184 | ~theme(U_185, Y_187, X_186) | ~desire_want(U_185, Y_187) | ~proposition(U_185, X_186) | ~proposition(U_185, W_184) | ~desire_want(U_185, V_188) | ~theme(U_185, V_188, W_184)))). % 16.55/5.89 tff(c_914, plain, (![V_16]: (~entity(skc8, V_16) | ~desire_want(skc6, V_16)))). % 16.55/5.89 tff(c_898, plain, (![V_4]: (~entity(skc8, V_4) | ~event(skc6, V_4)))). % 16.55/5.89 tff(c_883, plain, (![V_46]: (~eventuality(skc6, V_46) | ~entity(skc8, V_46)))). % 16.55/5.89 tff(c_144, 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)))). % 16.55/5.89 tff(c_877, plain, (![V_550]: (~existent(skc8, V_550) | ~eventuality(skc6, V_550)))). % 16.55/5.89 tff(c_869, plain, (![V_548]: (nonexistent(skc8, V_548) | ~eventuality(skc6, V_548)))). % 16.55/5.89 tff(c_675, plain, (![V_485, V_12, U_11]: (nonexistent(V_485, V_12) | ~accessible_world(U_11, V_485) | ~eventuality(U_11, V_12)))). % 16.55/5.89 tff(c_857, plain, (![V_541]: (of(V_541, skc9, skc10) | ~accessible_world(skc6, V_541)))). % 16.55/5.89 tff(c_829, plain, (![V_534]: (agent(V_534, skc7, skc10) | ~accessible_world(skc6, V_534)))). % 16.55/5.89 tff(c_142, plain, (![V_177, W_178, X_179, U_176]: (of(V_177, W_178, X_179) | ~of(U_176, W_178, X_179) | ~accessible_world(U_176, V_177)))). % 16.55/5.89 tff(c_828, plain, (![V_534]: (agent(V_534, skc11, skc10) | ~accessible_world(skc8, V_534)))). % 16.55/5.89 tff(c_837, plain, (![V_538]: (abstraction(skc8, V_538) | ~proposition(skc6, V_538)))). % 16.55/5.89 tff(c_822, plain, (![V_532]: (relation(skc8, V_532) | ~proposition(skc6, V_532)))). % 16.55/5.89 tff(c_138, plain, (![V_169, W_170, X_171, U_168]: (agent(V_169, W_170, X_171) | ~agent(U_168, W_170, X_171) | ~accessible_world(U_168, V_169)))). % 16.55/5.89 tff(c_765, plain, (![V_511, V_18, U_17]: (relation(V_511, V_18) | ~accessible_world(U_17, V_511) | ~proposition(U_17, V_18)))). % 16.55/5.89 tff(c_781, plain, (![V_523]: (theme(V_523, skc7, skc8) | ~accessible_world(skc6, V_523)))). % 16.55/5.89 tff(c_799, plain, (![V_527]: (~abstraction(skc8, V_527) | ~dance(skc6, V_527)))). % 16.55/5.89 tff(c_798, plain, (![V_527]: (~entity(skc8, V_527) | ~dance(skc6, V_527)))). % 16.55/5.89 tff(c_777, plain, (![V_521]: (event(skc8, V_521) | ~dance(skc6, V_521)))). % 16.55/5.89 tff(c_140, plain, (![V_173, W_174, X_175, U_172]: (theme(V_173, W_174, X_175) | ~theme(U_172, W_174, X_175) | ~accessible_world(U_172, V_173)))). % 16.55/5.89 tff(c_365, plain, (![V_367, V_2, U_1]: (event(V_367, V_2) | ~accessible_world(U_1, V_367) | ~dance(U_1, V_2)))). % 16.55/5.89 tff(c_118, plain, (![V_139, W_140, U_138]: (entity(V_139, W_140) | ~entity(U_138, W_140) | ~accessible_world(U_138, V_139)))). % 16.55/5.89 tff(c_132, plain, (![V_160, W_161, U_159]: (vincent_forename(V_160, W_161) | ~vincent_forename(U_159, W_161) | ~accessible_world(U_159, V_160)))). % 16.55/5.89 tff(c_98, plain, (![V_109, W_110, U_108]: (relation(V_109, W_110) | ~relation(U_108, W_110) | ~accessible_world(U_108, V_109)))). % 16.55/5.89 tff(c_750, plain, (![V_507]: (mia_forename(V_507, skc9) | ~accessible_world(skc6, V_507)))). % 16.55/5.89 tff(c_110, plain, (![V_127, W_128, U_126]: (mia_forename(V_127, W_128) | ~mia_forename(U_126, W_128) | ~accessible_world(U_126, V_127)))). % 16.55/5.89 tff(c_84, plain, (![V_88, W_89, U_87]: (singleton(V_88, W_89) | ~singleton(U_87, W_89) | ~accessible_world(U_87, V_88)))). % 16.55/5.89 tff(c_731, plain, (![V_499]: (abstraction(V_499, skc9) | ~accessible_world(skc8, V_499)))). % 16.55/5.89 tff(c_732, plain, (![V_499]: (abstraction(V_499, skc8) | ~accessible_world(skc8, V_499)))). % 16.55/5.89 tff(c_100, plain, (![V_112, W_113, U_111]: (abstraction(V_112, W_113) | ~abstraction(U_111, W_113) | ~accessible_world(U_111, V_112)))). % 16.55/5.89 tff(c_721, plain, (abstraction(skc8, skc9))). % 16.55/5.89 tff(c_716, plain, (![V_497]: (abstraction(V_497, skc9) | ~accessible_world(skc6, V_497)))). % 16.55/5.89 tff(c_708, plain, (![V_494]: (forename(V_494, skc9) | ~accessible_world(skc6, V_494)))). % 16.55/5.89 tff(c_106, plain, (![V_121, W_122, U_120]: (forename(V_121, W_122) | ~forename(U_120, W_122) | ~accessible_world(U_120, V_121)))). % 16.55/5.89 tff(c_704, plain, (abstraction(skc8, skc8))). % 16.55/5.89 tff(c_699, plain, (![V_492]: (abstraction(V_492, skc8) | ~accessible_world(skc6, V_492)))). % 16.55/5.89 tff(c_691, plain, (![V_489]: (proposition(V_489, skc8) | ~accessible_world(skc6, V_489)))). % 16.55/5.89 tff(c_96, plain, (![V_106, W_107, U_105]: (proposition(V_106, W_107) | ~proposition(U_105, W_107) | ~accessible_world(U_105, V_106)))). % 16.55/5.89 tff(c_671, plain, (![V_482]: (woman(V_482, skc10) | ~accessible_world(skc6, V_482)))). % 16.55/5.89 tff(c_88, plain, (![V_94, W_95, U_93]: (nonexistent(V_94, W_95) | ~nonexistent(U_93, W_95) | ~accessible_world(U_93, V_94)))). % 16.55/5.89 tff(c_112, plain, (![V_130, W_131, U_129]: (woman(V_130, W_131) | ~woman(U_129, W_131) | ~accessible_world(U_129, V_130)))). % 16.55/5.89 tff(c_82, plain, (![V_85, W_86, U_84]: (thing(V_85, W_86) | ~thing(U_84, W_86) | ~accessible_world(U_84, V_85)))). % 16.55/5.89 tff(c_653, plain, (~abstraction(skc8, skc7))). % 16.55/5.89 tff(c_102, plain, (![V_115, W_116, U_114]: (nonhuman(V_115, W_116) | ~nonhuman(U_114, W_116) | ~accessible_world(U_114, V_115)))). % 16.55/5.89 tff(c_648, plain, (![V_474]: (~abstraction(V_474, skc7) | ~accessible_world(skc6, V_474)))). % 16.55/5.89 tff(c_640, plain, (![V_471]: (desire_want(V_471, skc7) | ~accessible_world(skc6, V_471)))). % 16.55/5.89 tff(c_94, plain, (![V_103, W_104, U_102]: (desire_want(V_103, W_104) | ~desire_want(U_102, W_104) | ~accessible_world(U_102, V_103)))). % 16.55/5.89 tff(c_86, plain, (![V_91, W_92, U_90]: (specific(V_91, W_92) | ~specific(U_90, W_92) | ~accessible_world(U_90, V_91)))). % 16.55/5.89 tff(c_108, plain, (![V_124, W_125, U_123]: (relname(V_124, W_125) | ~relname(U_123, W_125) | ~accessible_world(U_123, V_124)))). % 16.55/5.89 tff(c_80, plain, (![V_82, W_83, U_81]: (eventuality(V_82, W_83) | ~eventuality(U_81, W_83) | ~accessible_world(U_81, V_82)))). % 16.55/5.89 tff(c_613, plain, (![V_457]: (present(V_457, skc7) | ~accessible_world(skc6, V_457)))). % 16.55/5.89 tff(c_612, plain, (![V_457]: (present(V_457, skc11) | ~accessible_world(skc8, V_457)))). % 16.55/5.89 tff(c_92, plain, (![V_100, W_101, U_99]: (present(V_100, W_101) | ~present(U_99, W_101) | ~accessible_world(U_99, V_100)))). % 16.55/5.89 tff(c_120, plain, (![V_142, W_143, U_141]: (existent(V_142, W_143) | ~existent(U_141, W_143) | ~accessible_world(U_141, V_142)))). % 16.55/5.89 tff(c_593, plain, (![U_15]: (~accessible_world(skc6, U_15) | ~desire_want(U_15, skc10)))). % 16.55/5.89 tff(c_592, plain, (![U_1]: (~accessible_world(skc6, U_1) | ~dance(U_1, skc10)))). % 16.55/5.89 tff(c_126, plain, (![V_151, W_152, U_150]: (human(V_151, W_152) | ~human(U_150, W_152) | ~accessible_world(U_150, V_151)))). % 16.55/5.89 tff(c_582, plain, (![U_3]: (~accessible_world(skc6, U_3) | ~event(U_3, skc10)))). % 16.55/5.89 tff(c_576, plain, (![V_446]: (~eventuality(V_446, skc10) | ~accessible_world(skc6, V_446)))). % 16.55/5.89 tff(c_564, plain, (![V_443]: (female(V_443, skc10) | ~accessible_world(skc6, V_443)))). % 16.55/5.89 tff(c_130, plain, (![V_157, W_158, U_156]: (female(V_157, W_158) | ~female(U_156, W_158) | ~accessible_world(U_156, V_157)))). % 16.55/5.89 tff(c_560, plain, (~abstraction(skc8, skc10))). % 16.55/5.89 tff(c_516, plain, (![V_425]: (~abstraction(V_425, skc10) | ~accessible_world(skc6, V_425)))). % 16.55/5.89 tff(c_458, plain, (![V_367]: (~abstraction(V_367, skc11) | ~accessible_world(skc8, V_367)))). % 16.55/5.89 tff(c_481, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~desire_want(U_15, V_16)))). % 16.55/5.89 tff(c_136, plain, (![V_166, W_167, U_165]: (male(V_166, W_167) | ~male(U_165, W_167) | ~accessible_world(U_165, V_166)))). % 16.55/5.89 tff(c_480, plain, (![U_1, V_2]: (~entity(U_1, V_2) | ~dance(U_1, V_2)))). % 16.55/5.89 tff(c_535, plain, (~abstraction(skc6, skc7))). % 16.55/5.89 tff(c_460, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~desire_want(U_15, V_16)))). % 16.55/5.89 tff(c_116, plain, (![V_136, W_137, U_135]: (organism(V_136, W_137) | ~organism(U_135, W_137) | ~accessible_world(U_135, V_136)))). % 16.55/5.89 tff(c_479, plain, (![V_367]: (~entity(V_367, skc11) | ~accessible_world(skc8, V_367)))). % 16.55/5.89 tff(c_459, plain, (![U_1, V_2]: (~abstraction(U_1, V_2) | ~dance(U_1, V_2)))). % 16.55/5.89 tff(c_506, plain, (![V_423]: (human(V_423, skc10) | ~accessible_world(skc6, V_423)))). % 16.55/5.89 tff(c_504, plain, (![V_423]: (entity(V_423, skc10) | ~accessible_world(skc6, V_423)))). % 16.55/5.89 tff(c_490, plain, (![V_420]: (human_person(V_420, skc10) | ~accessible_world(skc6, V_420)))). % 16.55/5.89 tff(c_114, plain, (![V_133, W_134, U_132]: (human_person(V_133, W_134) | ~human_person(U_132, W_134) | ~accessible_world(U_132, V_133)))). % 16.55/5.89 tff(c_465, plain, (![V_414]: (animate(V_414, skc10) | ~accessible_world(skc6, V_414)))). % 16.55/5.89 tff(c_482, plain, (~entity(skc8, skc11))). % 16.55/5.89 tff(c_444, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 16.55/5.89 tff(c_128, plain, (![V_154, W_155, U_153]: (animate(V_154, W_155) | ~animate(U_153, W_155) | ~accessible_world(U_153, V_154)))). % 16.55/5.89 tff(c_461, plain, (~abstraction(skc8, skc11))). % 16.55/5.89 tff(c_427, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 16.55/5.89 tff(c_342, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 16.55/5.89 tff(c_439, plain, (abstraction(skc6, skc9))). % 16.55/5.89 tff(c_377, plain, (![U_373, V_374]: (abstraction(U_373, V_374) | ~forename(U_373, V_374)))). % 16.55/5.89 tff(c_90, plain, (![V_97, W_98, U_96]: (unisex(V_97, W_98) | ~unisex(U_96, W_98) | ~accessible_world(U_96, V_97)))). % 16.55/5.89 tff(c_352, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~abstraction(U_25, V_26)))). % 16.55/5.89 tff(c_412, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~abstraction(U_25, V_26)))). % 16.55/5.89 tff(c_307, plain, (![U_343, V_344]: (~male(U_343, V_344) | ~eventuality(U_343, V_344)))). % 16.55/5.89 tff(c_104, plain, (![V_118, W_119, U_117]: (general(V_118, W_119) | ~general(U_117, W_119) | ~accessible_world(U_117, V_118)))). % 16.55/5.89 tff(c_222, plain, (![U_43, V_44]: (~general(U_43, V_44) | ~entity(U_43, V_44)))). % 16.55/5.89 tff(c_407, plain, (abstraction(skc6, skc8))). % 16.55/5.89 tff(c_294, plain, (![U_339, V_340]: (abstraction(U_339, V_340) | ~proposition(U_339, V_340)))). % 16.55/5.89 tff(c_204, plain, (![U_281, V_282]: (singleton(U_281, V_282) | ~entity(U_281, V_282)))). % 16.55/5.89 tff(c_281, plain, (![U_329, V_330]: (~female(U_329, V_330) | ~abstraction(U_329, V_330)))). % 16.55/5.89 tff(c_134, plain, (![V_163, W_164, U_162]: (man(V_163, W_164) | ~man(U_162, W_164) | ~accessible_world(U_162, V_163)))). % 16.55/5.89 tff(c_367, plain, (![V_367]: (event(V_367, skc11) | ~accessible_world(skc8, V_367)))). % 16.55/5.89 tff(c_391, plain, (entity(skc6, skc10))). % 16.55/5.89 tff(c_215, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~human_person(U_37, V_38)))). % 16.55/5.89 tff(c_124, plain, (![V_148, W_149, U_147]: (living(V_148, W_149) | ~living(U_147, W_149) | ~accessible_world(U_147, V_148)))). % 16.55/5.89 tff(c_245, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~human_person(U_37, V_38)))). % 16.55/5.90 tff(c_280, plain, (![U_329, V_330]: (~male(U_329, V_330) | ~abstraction(U_329, V_330)))). % 16.55/5.90 tff(c_260, plain, (![U_319, V_320]: (relation(U_319, V_320) | ~forename(U_319, V_320)))). % 16.55/5.90 tff(c_287, plain, (![U_333, V_334]: (singleton(U_333, V_334) | ~abstraction(U_333, V_334)))). % 16.55/5.90 tff(c_347, plain, (![V_360]: (dance(V_360, skc11) | ~accessible_world(skc8, V_360)))). % 16.55/5.90 tff(c_78, plain, (![V_79, W_80, U_78]: (event(V_79, W_80) | ~event(U_78, W_80) | ~accessible_world(U_78, V_79)))). % 16.55/5.90 tff(c_357, plain, (~abstraction(skc6, skc10))). % 16.55/5.90 tff(c_271, plain, (![U_325, V_326]: (~human(U_325, V_326) | ~abstraction(U_325, V_326)))). % 16.55/5.90 tff(c_318, plain, (![U_347, V_348]: (~general(U_347, V_348) | ~eventuality(U_347, V_348)))). % 16.55/5.90 tff(c_76, plain, (![V_76, W_77, U_75]: (dance(V_76, W_77) | ~dance(U_75, W_77) | ~accessible_world(U_75, V_76)))). % 16.55/5.90 tff(c_254, plain, (![U_37, V_38]: (living(U_37, V_38) | ~human_person(U_37, V_38)))). % 16.55/5.90 tff(c_313, plain, (![U_345, V_346]: (~existent(U_345, V_346) | ~eventuality(U_345, V_346)))). % 16.55/5.90 tff(c_299, plain, (![U_341, V_342]: (singleton(U_341, V_342) | ~eventuality(U_341, V_342)))). % 16.55/5.90 tff(c_335, plain, (~desire_want(skc6, skc10))). % 16.55/5.90 tff(c_334, plain, (~dance(skc6, skc10))). % 16.55/5.90 tff(c_122, plain, (![V_145, W_146, U_144]: (impartial(V_145, W_146) | ~impartial(U_144, W_146) | ~accessible_world(U_144, V_145)))). % 16.55/5.90 tff(c_327, plain, (~event(skc6, skc10))). % 16.55/5.90 tff(c_323, plain, (~eventuality(skc6, skc10))). % 16.55/5.90 tff(c_308, plain, (![U_343, V_344]: (~female(U_343, V_344) | ~eventuality(U_343, V_344)))). % 16.55/5.90 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 16.55/5.90 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 16.55/5.90 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 16.55/5.90 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 16.55/5.90 tff(c_18, plain, (![U_17, V_18]: (relation(U_17, V_18) | ~proposition(U_17, V_18)))). % 16.55/5.90 tff(c_26, plain, (![U_25, V_26]: (general(U_25, V_26) | ~abstraction(U_25, V_26)))). % 16.55/5.90 tff(c_20, plain, (![U_19, V_20]: (abstraction(U_19, V_20) | ~relation(U_19, V_20)))). % 16.55/5.90 tff(c_22, plain, (![U_21, V_22]: (thing(U_21, V_22) | ~abstraction(U_21, V_22)))). % 16.55/5.90 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 16.55/5.90 tff(c_28, plain, (![U_27, V_28]: (unisex(U_27, V_28) | ~abstraction(U_27, V_28)))). % 16.55/5.90 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~dance(U_1, V_2)))). % 16.55/5.90 tff(c_24, plain, (![U_23, V_24]: (nonhuman(U_23, V_24) | ~abstraction(U_23, V_24)))). % 16.55/5.90 tff(c_266, plain, (female(skc6, skc10))). % 16.55/5.90 tff(c_56, plain, (![U_55, V_56]: (female(U_55, V_56) | ~woman(U_55, V_56)))). % 16.55/5.90 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 16.55/5.90 tff(c_30, plain, (![U_29, V_30]: (relname(U_29, V_30) | ~forename(U_29, V_30)))). % 16.55/5.90 tff(c_62, plain, (![U_61, V_62]: (male(U_61, V_62) | ~man(U_61, V_62)))). % 16.55/5.90 tff(c_50, plain, (![U_49, V_50]: (living(U_49, V_50) | ~organism(U_49, V_50)))). % 16.55/5.90 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 16.55/5.90 tff(c_74, plain, (![U_73, V_74]: (~existent(U_73, V_74) | ~nonexistent(U_73, V_74)))). % 16.55/5.90 tff(c_70, plain, (![U_69, V_70]: (~nonhuman(U_69, V_70) | ~human(U_69, V_70)))). % 16.55/5.90 tff(c_60, plain, (![U_59, V_60]: (human_person(U_59, V_60) | ~man(U_59, V_60)))). % 16.55/5.90 tff(c_48, plain, (![U_47, V_48]: (impartial(U_47, V_48) | ~organism(U_47, V_48)))). % 16.55/5.90 tff(c_64, plain, (![U_63, V_64]: (~unisex(U_63, V_64) | ~male(U_63, V_64)))). % 16.55/5.90 tff(c_34, plain, (![U_33, V_34]: (forename(U_33, V_34) | ~mia_forename(U_33, V_34)))). % 16.55/5.90 tff(c_233, plain, (animate(skc6, skc10))). % 16.55/5.90 tff(c_54, plain, (![U_53, V_54]: (animate(U_53, V_54) | ~human_person(U_53, V_54)))). % 16.55/5.90 tff(c_228, plain, (human(skc6, skc10))). % 16.55/5.90 tff(c_52, plain, (![U_51, V_52]: (human(U_51, V_52) | ~human_person(U_51, V_52)))). % 16.55/5.90 tff(c_72, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~female(U_71, V_72)))). % 16.55/5.90 tff(c_68, plain, (![U_67, V_68]: (~specific(U_67, V_68) | ~general(U_67, V_68)))). % 16.55/5.90 tff(c_32, plain, (![U_31, V_32]: (relation(U_31, V_32) | ~relname(U_31, V_32)))). % 16.55/5.90 tff(c_66, plain, (![U_65, V_66]: (~unisex(U_65, V_66) | ~female(U_65, V_66)))). % 16.55/5.90 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~organism(U_39, V_40)))). % 16.55/5.90 tff(c_210, plain, (human_person(skc6, skc10))). % 16.55/5.90 tff(c_36, plain, (![U_35, V_36]: (human_person(U_35, V_36) | ~woman(U_35, V_36)))). % 16.55/5.90 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 16.55/5.90 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 16.55/5.90 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 16.55/5.90 tff(c_38, plain, (![U_37, V_38]: (organism(U_37, V_38) | ~human_person(U_37, V_38)))). % 16.55/5.90 tff(c_16, plain, (![U_15, V_16]: (event(U_15, V_16) | ~desire_want(U_15, V_16)))). % 16.55/5.90 tff(c_170, plain, (of(skc6, skc9, skc10))). % 16.55/5.90 tff(c_174, plain, (agent(skc8, skc11, skc10))). % 16.55/5.90 tff(c_172, plain, (agent(skc6, skc7, skc10))). % 16.55/5.90 tff(c_176, plain, (theme(skc6, skc7, skc8))). % 16.55/5.90 tff(c_156, plain, (dance(skc8, skc11))). % 16.55/5.90 tff(c_154, plain, (present(skc8, skc11))). % 16.55/5.90 tff(c_152, plain, (woman(skc6, skc10))). % 16.55/5.90 tff(c_168, plain, (present(skc6, skc7))). % 16.55/5.90 tff(c_150, plain, (event(skc8, skc11))). % 16.55/5.90 tff(c_158, plain, (forename(skc6, skc9))). % 16.55/5.90 tff(c_160, plain, (mia_forename(skc6, skc9))). % 16.55/5.90 tff(c_162, plain, (proposition(skc6, skc8))). % 16.55/5.90 tff(c_164, plain, (accessible_world(skc6, skc8))). % 16.55/5.90 tff(c_166, plain, (desire_want(skc6, skc7))). % 16.55/5.90 tff(c_148, plain, (actual_world(skc6))). % 16.55/5.90 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.55/5.90 %------------------------------------------------------------------------------