%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP226-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 : n021.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:40 PM UTC 2025 % Result : Satisfiable 9.43s 3.37s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP226-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 : n021.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 09:31:58 EDT 2025 % 0.12/0.34 % CPUTime : % 9.43/3.36 % 9.43/3.37 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.43/3.37 % 9.43/3.37 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.84/3.38 %$ 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 > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 % 9.84/3.38 % 9.84/3.38 %Foreground sorts: % 9.84/3.38 % 9.84/3.38 % 9.84/3.38 %Background operators: % 9.84/3.38 % 9.84/3.38 % 9.84/3.38 %Foreground operators: % 9.84/3.38 tff(relation, type, relation: ($i * $i) > $o). % 9.84/3.38 tff(forename, type, forename: ($i * $i) > $o). % 9.84/3.38 tff(be, type, be: ($i * $i * $i * $i) > $o). % 9.84/3.38 tff(theme, type, theme: ($i * $i * $i) > $o). % 9.84/3.38 tff(living, type, living: ($i * $i) > $o). % 9.84/3.38 tff(human_person, type, human_person: ($i * $i) > $o). % 9.84/3.38 tff(present, type, present: ($i * $i) > $o). % 9.84/3.38 tff(skc11, type, skc11: $i). % 9.84/3.38 tff(entity, type, entity: ($i * $i) > $o). % 9.84/3.38 tff(skc9, type, skc9: $i). % 9.84/3.38 tff(eventuality, type, eventuality: ($i * $i) > $o). % 9.84/3.38 tff(existent, type, existent: ($i * $i) > $o). % 9.84/3.38 tff(abstraction, type, abstraction: ($i * $i) > $o). % 9.84/3.38 tff(skf1, type, skf1: $i > $i). % 9.84/3.38 tff(skc8, type, skc8: $i). % 9.84/3.38 tff(proposition, type, proposition: ($i * $i) > $o). % 9.84/3.38 tff(relname, type, relname: ($i * $i) > $o). % 9.84/3.38 tff(skc14, type, skc14: $i). % 9.84/3.38 tff(singleton, type, singleton: ($i * $i) > $o). % 9.84/3.38 tff(skc13, type, skc13: $i). % 9.84/3.38 tff(male, type, male: ($i * $i) > $o). % 9.84/3.38 tff(organism, type, organism: ($i * $i) > $o). % 9.84/3.38 tff(animate, type, animate: ($i * $i) > $o). % 9.84/3.38 tff(of, type, of: ($i * $i * $i) > $o). % 9.84/3.38 tff(actual_world, type, actual_world: $i > $o). % 9.84/3.38 tff(agent, type, agent: ($i * $i * $i) > $o). % 9.84/3.38 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 9.84/3.38 tff(general, type, general: ($i * $i) > $o). % 9.84/3.38 tff(smoke, type, smoke: ($i * $i) > $o). % 9.84/3.38 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 9.84/3.38 tff(event, type, event: ($i * $i) > $o). % 9.84/3.38 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 9.84/3.38 tff(state, type, state: ($i * $i) > $o). % 9.84/3.38 tff(thing, type, thing: ($i * $i) > $o). % 9.84/3.38 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 9.84/3.38 tff(skc15, type, skc15: $i). % 9.84/3.38 tff(human, type, human: ($i * $i) > $o). % 9.84/3.38 tff(man, type, man: ($i * $i) > $o). % 9.84/3.38 tff(unisex, type, unisex: ($i * $i) > $o). % 9.84/3.38 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 9.84/3.38 tff(impartial, type, impartial: ($i * $i) > $o). % 9.84/3.38 tff(skc12, type, skc12: $i). % 9.84/3.38 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 9.84/3.38 tff(specific, type, specific: ($i * $i) > $o). % 9.84/3.38 tff(skc10, type, skc10: $i). % 9.84/3.38 % 9.84/3.38 %Saturated clause set: % 9.84/3.39 tff(c_4035, plain, (![V_1216, V_817]: (skc12=V_1216 | ~think_believe_consider(V_817, skc13) | ~think_believe_consider(V_817, skf1(skc15)) | ~theme(V_817, skf1(skc15), V_1216) | ~proposition(V_817, skc12) | ~proposition(V_817, V_1216) | ~accessible_world(skc12, V_817) | ~accessible_world(skc8, V_817)))). % 9.84/3.39 tff(c_4023, plain, (![W_1210, V_1208, V_808]: (W_1210=V_1208 | ~theme(V_808, skc13, W_1210) | ~think_believe_consider(V_808, skc13) | ~think_believe_consider(V_808, skf1(skc15)) | ~theme(V_808, skf1(skc15), V_1208) | ~proposition(V_808, W_1210) | ~proposition(V_808, V_1208) | ~accessible_world(skc12, V_808) | ~accessible_world(skc8, V_808)))). % 9.84/3.39 tff(c_4020, plain, (![W_1210, V_1208, V_808, U_196]: (W_1210=V_1208 | ~theme(V_808, skf1(U_196), W_1210) | ~think_believe_consider(V_808, skf1(U_196)) | ~theme(V_808, skf1(U_196), V_1208) | ~proposition(V_808, W_1210) | ~proposition(V_808, V_1208) | ~accessible_world(skc12, V_808) | ~man(skc12, U_196)))). % 9.84/3.39 tff(c_4028, plain, (~accessible_world(skc12, skc8))). % 9.84/3.39 tff(c_2877, plain, (![U_928, V_189, Y_188, V_927, W_184]: (W_184=V_189 | ~agent(V_927, Y_188, U_928) | ~theme(V_927, Y_188, W_184) | ~think_believe_consider(V_927, Y_188) | ~think_believe_consider(V_927, skf1(U_928)) | ~theme(V_927, skf1(U_928), V_189) | ~proposition(V_927, W_184) | ~proposition(V_927, V_189) | ~accessible_world(skc12, V_927) | ~man(skc12, U_928)))). % 9.84/3.39 tff(c_3995, plain, (![V_1201, V_817]: (skc12=V_1201 | ~agent(V_817, skc13, skc15) | ~think_believe_consider(V_817, skc13) | ~theme(V_817, skc13, V_1201) | ~proposition(V_817, skc12) | ~proposition(V_817, V_1201) | ~accessible_world(skc8, V_817)))). % 9.84/3.39 tff(c_2375, plain, (![W_854, V_852, V_808, Y_853]: (W_854=V_852 | ~agent(V_808, Y_853, skc15) | ~theme(V_808, Y_853, W_854) | ~think_believe_consider(V_808, Y_853) | ~think_believe_consider(V_808, skc13) | ~theme(V_808, skc13, V_852) | ~proposition(V_808, W_854) | ~proposition(V_808, V_852) | ~accessible_world(skc8, V_808)))). % 9.84/3.39 tff(c_3936, plain, (![V_119, V_1184]: (human(V_119, skc15) | ~accessible_world(V_1184, V_119) | ~accessible_world(skc12, V_1184)))). % 9.84/3.39 tff(c_3941, plain, (![V_122, V_1185]: (animate(V_122, skc15) | ~accessible_world(V_1185, V_122) | ~accessible_world(skc12, V_1185)))). % 9.84/3.39 tff(c_3870, plain, (![V_101, V_1181]: (human_person(V_101, skc15) | ~accessible_world(V_1181, V_101) | ~accessible_world(skc12, V_1181)))). % 9.84/3.39 tff(c_3918, plain, (![V_125, V_1183]: (male(V_125, skc15) | ~accessible_world(V_1183, V_125) | ~accessible_world(skc12, V_1183)))). % 9.84/3.39 tff(c_3845, plain, (![V_98, V_1180]: (man(V_98, skc15) | ~accessible_world(V_1180, V_98) | ~accessible_world(skc12, V_1180)))). % 9.84/3.39 tff(c_3890, plain, (![V_155, V_1182]: (think_believe_consider(V_155, skc13) | ~accessible_world(V_1182, V_155) | ~accessible_world(skc12, V_1182)))). % 9.84/3.39 tff(c_3958, plain, (![U_15]: (~accessible_world(skc12, U_15) | ~event(U_15, skc15)))). % 9.84/3.39 tff(c_3919, plain, (![V_1183]: (~eventuality(V_1183, skc15) | ~accessible_world(skc12, V_1183)))). % 9.84/3.39 tff(c_3942, plain, (~think_believe_consider(skc12, skf1(skc15)))). % 9.84/3.39 tff(c_3873, plain, (![V_1181]: (animate(V_1181, skc15) | ~accessible_world(skc12, V_1181)))). % 9.84/3.39 tff(c_3872, plain, (![V_1181]: (human(V_1181, skc15) | ~accessible_world(skc12, V_1181)))). % 9.84/3.39 tff(c_3803, plain, (![V_125]: (male(V_125, skc15) | ~accessible_world(skc12, V_125)))). % 9.84/3.39 tff(c_3886, plain, (![V_155]: (think_believe_consider(V_155, skc13) | ~accessible_world(skc12, V_155)))). % 9.84/3.39 tff(c_3883, plain, (think_believe_consider(skc12, skc13))). % 9.84/3.40 tff(c_3774, plain, (![V_101]: (human_person(V_101, skc15) | ~accessible_world(skc12, V_101)))). % 9.84/3.40 tff(c_3760, plain, (![V_98]: (man(V_98, skc15) | ~accessible_world(skc12, V_98)))). % 9.84/3.40 tff(c_3835, plain, (~event(skc12, skc15))). % 9.84/3.40 tff(c_3804, plain, (~eventuality(skc12, skc15))). % 9.84/3.40 tff(c_3778, plain, (animate(skc12, skc15))). % 9.84/3.40 tff(c_3777, plain, (human(skc12, skc15))). % 9.84/3.40 tff(c_3762, plain, (male(skc12, skc15))). % 9.84/3.40 tff(c_3761, plain, (human_person(skc12, skc15))). % 9.84/3.40 tff(c_3751, plain, (man(skc12, skc15))). % 9.84/3.40 tff(c_3002, plain, (![W_966, V_967, U_196]: (W_966=V_967 | ~theme(skc12, skf1(U_196), W_966) | ~think_believe_consider(skc12, skf1(U_196)) | ~theme(skc12, skf1(U_196), V_967) | ~proposition(skc12, W_966) | ~proposition(skc12, V_967) | ~man(skc12, U_196)))). % 9.84/3.40 tff(c_2340, plain, (![W_841, V_828]: (skc14=W_841 | ~entity(V_828, skc15) | ~forename(V_828, W_841) | ~of(V_828, W_841, skc15) | ~forename(V_828, skc14) | ~accessible_world(skc8, V_828)))). % 9.84/3.40 tff(c_3347, plain, (![V_83, V_1046, V_1045]: (singleton(V_83, V_1046) | ~accessible_world(V_1045, V_83) | ~accessible_world(skc12, V_1045) | ~abstraction(skc8, V_1046)))). % 9.84/3.40 tff(c_3399, plain, (![V_83, V_1058, V_1057]: (singleton(V_83, V_1058) | ~accessible_world(V_1057, V_83) | ~accessible_world(skc12, V_1057) | ~eventuality(skc8, V_1058)))). % 9.84/3.40 tff(c_3447, plain, (![V_134, V_1077, V_1076]: (relation(V_134, V_1077) | ~accessible_world(V_1076, V_134) | ~accessible_world(skc12, V_1076) | ~forename(skc8, V_1077)))). % 9.84/3.40 tff(c_3366, plain, (![V_116, V_1050, V_1049]: (living(V_116, V_1050) | ~accessible_world(V_1049, V_116) | ~accessible_world(skc12, V_1049) | ~human_person(skc8, V_1050)))). % 9.84/3.40 tff(c_3410, plain, (![V_83, V_1063, V_1062]: (singleton(V_83, V_1063) | ~accessible_world(V_1062, V_83) | ~accessible_world(skc12, V_1062) | ~entity(skc8, V_1063)))). % 9.84/3.40 tff(c_2339, plain, (![W_841, V_828]: (skc11=W_841 | ~entity(V_828, skc10) | ~forename(V_828, W_841) | ~of(V_828, W_841, skc10) | ~forename(V_828, skc11) | ~accessible_world(skc8, V_828)))). % 9.84/3.40 tff(c_3414, plain, (![V_113, V_1065, V_1064]: (impartial(V_113, V_1065) | ~accessible_world(V_1064, V_113) | ~accessible_world(skc12, V_1064) | ~human_person(skc8, V_1065)))). % 9.84/3.40 tff(c_3152, plain, (![V_86, V_1003, V_1002]: (specific(V_86, V_1003) | ~accessible_world(V_1002, V_86) | ~accessible_world(skc12, V_1002) | ~eventuality(skc8, V_1003)))). % 9.84/3.40 tff(c_3095, plain, (![V_80, V_988, V_987]: (thing(V_80, V_988) | ~accessible_world(V_987, V_80) | ~accessible_world(skc12, V_987) | ~abstraction(skc8, V_988)))). % 9.84/3.40 tff(c_3122, plain, (![V_104, V_995, V_994]: (organism(V_104, V_995) | ~accessible_world(V_994, V_104) | ~accessible_world(skc12, V_994) | ~human_person(skc8, V_995)))). % 9.98/3.40 tff(c_3210, plain, (![V_140, V_1017, V_1016]: (nonhuman(V_140, V_1017) | ~accessible_world(V_1016, V_140) | ~accessible_world(skc12, V_1016) | ~abstraction(skc8, V_1017)))). % 9.98/3.40 tff(c_3239, plain, (![V_110, V_1025, V_1024]: (existent(V_110, V_1025) | ~accessible_world(V_1024, V_110) | ~accessible_world(skc12, V_1024) | ~entity(skc8, V_1025)))). % 9.98/3.40 tff(c_3202, plain, (![V_92, V_1015, V_1014]: (unisex(V_92, V_1015) | ~accessible_world(V_1014, V_92) | ~accessible_world(skc12, V_1014) | ~eventuality(skc8, V_1015)))). % 9.98/3.40 tff(c_3066, plain, (![V_77, V_982, V_981]: (eventuality(V_77, V_982) | ~accessible_world(V_981, V_77) | ~accessible_world(skc12, V_981) | ~event(skc8, V_982)))). % 9.98/3.40 tff(c_3132, plain, (![V_131, V_997, V_996]: (relname(V_131, V_997) | ~accessible_world(V_996, V_131) | ~accessible_world(skc12, V_996) | ~forename(skc8, V_997)))). % 9.98/3.41 tff(c_2878, plain, (![V_168, U_928, V_927]: (agent(V_168, skf1(U_928), U_928) | ~accessible_world(V_927, V_168) | ~accessible_world(skc12, V_927) | ~man(skc12, U_928)))). % 9.98/3.41 tff(c_3185, plain, (![V_143, V_1009, V_1008]: (general(V_143, V_1009) | ~accessible_world(V_1008, V_143) | ~accessible_world(skc12, V_1008) | ~abstraction(skc8, V_1009)))). % 9.98/3.41 tff(c_3108, plain, (![V_134, V_993, V_992]: (relation(V_134, V_993) | ~accessible_world(V_992, V_134) | ~accessible_world(skc12, V_992) | ~proposition(skc8, V_993)))). % 9.98/3.41 tff(c_3087, plain, (![V_80, V_986, V_985]: (thing(V_80, V_986) | ~accessible_world(V_985, V_80) | ~accessible_world(skc12, V_985) | ~entity(skc8, V_986)))). % 9.98/3.41 tff(c_3144, plain, (![V_89, V_1001, V_1000]: (nonexistent(V_89, V_1001) | ~accessible_world(V_1000, V_89) | ~accessible_world(skc12, V_1000) | ~eventuality(skc8, V_1001)))). % 9.98/3.41 tff(c_3160, plain, (![V_92, V_1005, V_1004]: (unisex(V_92, V_1005) | ~accessible_world(V_1004, V_92) | ~accessible_world(skc12, V_1004) | ~abstraction(skc8, V_1005)))). % 9.98/3.41 tff(c_3218, plain, (![V_80, V_1019, V_1018]: (thing(V_80, V_1019) | ~accessible_world(V_1018, V_80) | ~accessible_world(skc12, V_1018) | ~eventuality(skc8, V_1019)))). % 9.98/3.41 tff(c_3079, plain, (![V_86, V_984, V_983]: (specific(V_86, V_984) | ~accessible_world(V_983, V_86) | ~accessible_world(skc12, V_983) | ~entity(skc8, V_984)))). % 9.98/3.41 tff(c_2770, plain, (![V_107, V_907]: (entity(V_107, skc10) | ~accessible_world(V_907, V_107) | ~accessible_world(skc12, V_907)))). % 9.98/3.41 tff(c_2752, plain, (![V_107, V_906]: (entity(V_107, skc15) | ~accessible_world(V_906, V_107) | ~accessible_world(skc12, V_906)))). % 9.98/3.41 tff(c_2353, plain, (![V_179, V_845]: (be(V_179, skc9, skc10, skc10) | ~accessible_world(V_845, V_179) | ~accessible_world(skc8, V_845)))). % 9.98/3.41 tff(c_3461, plain, (![U_49, V_50]: (~accessible_world(skc12, U_49) | ~entity(skc8, V_50) | ~abstraction(U_49, V_50)))). % 9.98/3.41 tff(c_3612, plain, (![U_1096]: (~accessible_world(skc12, U_1096) | ~entity(U_1096, skc9)))). % 9.98/3.41 tff(c_3428, plain, (![U_27, V_28]: (~accessible_world(skc12, U_27) | ~eventuality(skc8, V_28) | ~entity(U_27, V_28)))). % 9.98/3.41 tff(c_3277, plain, (![U_15, V_16]: (~accessible_world(skc12, U_15) | ~entity(skc8, V_16) | ~event(U_15, V_16)))). % 9.98/3.41 tff(c_3338, plain, (![U_49, V_50]: (~accessible_world(skc12, U_49) | ~eventuality(skc8, V_50) | ~abstraction(U_49, V_50)))). % 9.98/3.41 tff(c_3448, plain, (![V_1076, V_1077]: (abstraction(V_1076, V_1077) | ~accessible_world(skc12, V_1076) | ~forename(skc8, V_1077)))). % 9.98/3.41 tff(c_3518, plain, (![U_15, V_16]: (~accessible_world(skc12, U_15) | ~abstraction(skc8, V_16) | ~event(U_15, V_16)))). % 9.98/3.41 tff(c_3069, plain, (![V_981, V_982]: (~entity(V_981, V_982) | ~accessible_world(skc12, V_981) | ~event(skc8, V_982)))). % 9.98/3.41 tff(c_3186, plain, (![V_1008, V_1009]: (~eventuality(V_1008, V_1009) | ~accessible_world(skc12, V_1008) | ~abstraction(skc8, V_1009)))). % 9.98/3.41 tff(c_2325, plain, (![V_164, V_839]: (of(V_164, skc14, skc15) | ~accessible_world(V_839, V_164) | ~accessible_world(skc8, V_839)))). % 9.98/3.41 tff(c_3187, plain, (![V_1008, V_1009]: (~entity(V_1008, V_1009) | ~accessible_world(skc12, V_1008) | ~abstraction(skc8, V_1009)))). % 9.98/3.41 tff(c_3080, plain, (![V_983, V_984]: (~general(V_983, V_984) | ~accessible_world(skc12, V_983) | ~entity(skc8, V_984)))). % 9.98/3.41 tff(c_3133, plain, (![V_996, V_997]: (relation(V_996, V_997) | ~accessible_world(skc12, V_996) | ~forename(skc8, V_997)))). % 9.98/3.41 tff(c_2029, plain, (![V_749, V_686]: (animate(V_749, skc15) | ~accessible_world(V_686, V_749) | ~accessible_world(skc8, V_686)))). % 9.98/3.41 tff(c_2030, plain, (![V_749, V_680]: (animate(V_749, skc10) | ~accessible_world(V_680, V_749) | ~accessible_world(skc8, V_680)))). % 9.98/3.41 tff(c_2197, plain, (![V_168, V_813]: (agent(V_168, skc13, skc15) | ~accessible_world(V_813, V_168) | ~accessible_world(skc8, V_813)))). % 9.98/3.41 tff(c_3145, plain, (![V_1000, V_1001]: (~existent(V_1000, V_1001) | ~accessible_world(skc12, V_1000) | ~eventuality(skc8, V_1001)))). % 9.98/3.41 tff(c_3109, plain, (![V_992, V_993]: (abstraction(V_992, V_993) | ~accessible_world(skc12, V_992) | ~proposition(skc8, V_993)))). % 9.98/3.41 tff(c_2675, plain, (![V_113, V_898]: (impartial(V_113, V_898) | ~accessible_world(skc12, V_113) | ~human_person(skc8, V_898)))). % 9.98/3.41 tff(c_2871, plain, (![V_83, V_926]: (singleton(V_83, V_926) | ~accessible_world(skc12, V_83) | ~entity(skc8, V_926)))). % 9.98/3.41 tff(c_2053, plain, (![V_95, V_758, V_757]: (event(V_95, skf1(V_758)) | ~accessible_world(V_757, V_95) | ~accessible_world(skc12, V_757)))). % 9.98/3.41 tff(c_3401, plain, (~event(skc8, skc12))). % 9.98/3.42 tff(c_3400, plain, (~event(skc8, skc14))). % 9.98/3.42 tff(c_3395, plain, (~event(skc8, skc11))). % 9.98/3.42 tff(c_3219, plain, (![V_1018, V_1019]: (singleton(V_1018, V_1019) | ~accessible_world(skc12, V_1018) | ~eventuality(skc8, V_1019)))). % 9.98/3.42 tff(c_3070, plain, (![V_981, V_982]: (~abstraction(V_981, V_982) | ~accessible_world(skc12, V_981) | ~event(skc8, V_982)))). % 9.98/3.42 tff(c_1857, plain, (![V_107, V_706]: (entity(V_107, skc10) | ~accessible_world(V_706, V_107) | ~accessible_world(skc8, V_706)))). % 9.98/3.42 tff(c_2232, plain, (![V_172, V_823]: (theme(V_172, skc13, skc12) | ~accessible_world(V_823, V_172) | ~accessible_world(skc8, V_823)))). % 9.98/3.42 tff(c_3124, plain, (![V_994, V_995]: (living(V_994, V_995) | ~accessible_world(skc12, V_994) | ~human_person(skc8, V_995)))). % 9.98/3.42 tff(c_3123, plain, (![V_994, V_995]: (entity(V_994, V_995) | ~accessible_world(skc12, V_994) | ~human_person(skc8, V_995)))). % 9.98/3.42 tff(c_2588, plain, (![V_83, V_886]: (singleton(V_83, V_886) | ~accessible_world(skc12, V_83) | ~abstraction(skc8, V_886)))). % 9.98/3.42 tff(c_1849, plain, (![V_107, V_705]: (entity(V_107, skc15) | ~accessible_world(V_705, V_107) | ~accessible_world(skc8, V_705)))). % 9.98/3.42 tff(c_3153, plain, (![V_1002, V_1003]: (~general(V_1002, V_1003) | ~accessible_world(skc12, V_1002) | ~eventuality(skc8, V_1003)))). % 9.98/3.42 tff(c_2139, plain, (![V_792, V_680]: (human(V_792, skc10) | ~accessible_world(V_680, V_792) | ~accessible_world(skc8, V_680)))). % 9.98/3.42 tff(c_3161, plain, (![V_1004, V_1005]: (~male(V_1004, V_1005) | ~accessible_world(skc12, V_1004) | ~abstraction(skc8, V_1005)))). % 9.98/3.42 tff(c_2138, plain, (![V_792, V_686]: (human(V_792, skc15) | ~accessible_world(V_686, V_792) | ~accessible_world(skc8, V_686)))). % 9.98/3.42 tff(c_3203, plain, (![V_1014, V_1015]: (~male(V_1014, V_1015) | ~accessible_world(skc12, V_1014) | ~eventuality(skc8, V_1015)))). % 9.98/3.42 tff(c_2109, plain, (![V_149, V_782, V_781]: (smoke(V_149, skf1(V_782)) | ~accessible_world(V_781, V_149) | ~accessible_world(skc12, V_781)))). % 9.98/3.42 tff(c_3240, plain, (![V_1024, V_1025]: (~eventuality(V_1024, V_1025) | ~accessible_world(skc12, V_1024) | ~entity(skc8, V_1025)))). % 9.98/3.42 tff(c_3211, plain, (![V_1016, V_1017]: (~human(V_1016, V_1017) | ~accessible_world(skc12, V_1016) | ~abstraction(skc8, V_1017)))). % 9.98/3.42 tff(c_2800, plain, (![V_110, V_917]: (existent(V_110, V_917) | ~accessible_world(skc12, V_110) | ~entity(skc8, V_917)))). % 9.98/3.42 tff(c_2010, plain, (![V_744, V_671]: (human_person(V_744, skc15) | ~accessible_world(V_671, V_744) | ~accessible_world(skc8, V_671)))). % 9.98/3.42 tff(c_1970, plain, (![V_77, V_735]: (eventuality(V_77, skc9) | ~accessible_world(V_735, V_77) | ~accessible_world(skc8, V_735)))). % 9.98/3.42 tff(c_2181, plain, (![V_80, V_807]: (thing(V_80, V_807) | ~accessible_world(skc12, V_80) | ~eventuality(skc8, V_807)))). % 9.98/3.42 tff(c_2541, plain, (![V_140, V_879]: (nonhuman(V_140, V_879) | ~accessible_world(skc12, V_140) | ~abstraction(skc8, V_879)))). % 9.98/3.42 tff(c_2529, plain, (![V_92, V_875]: (unisex(V_92, V_875) | ~accessible_world(skc12, V_92) | ~eventuality(skc8, V_875)))). % 9.98/3.42 tff(c_1825, plain, (![V_95, V_699]: (event(V_95, skc9) | ~accessible_world(V_699, V_95) | ~accessible_world(skc8, V_699)))). % 9.98/3.42 tff(c_2329, plain, (![V_164, V_840]: (of(V_164, skc11, skc10) | ~accessible_world(V_840, V_164) | ~accessible_world(skc8, V_840)))). % 9.98/3.42 tff(c_2418, plain, (![V_143, V_861]: (general(V_143, V_861) | ~accessible_world(skc12, V_143) | ~abstraction(skc8, V_861)))). % 9.98/3.42 tff(c_2011, plain, (![V_744, V_672]: (human_person(V_744, skc10) | ~accessible_world(V_672, V_744) | ~accessible_world(skc8, V_672)))). % 9.98/3.42 tff(c_2212, plain, (![V_92, V_821]: (unisex(V_92, V_821) | ~accessible_world(skc12, V_92) | ~abstraction(skc8, V_821)))). % 9.98/3.42 tff(c_2366, plain, (![V_86, V_849]: (specific(V_86, V_849) | ~accessible_world(skc12, V_86) | ~eventuality(skc8, V_849)))). % 9.98/3.42 tff(c_2599, plain, (![V_89, V_890]: (nonexistent(V_89, V_890) | ~accessible_world(skc12, V_89) | ~eventuality(skc8, V_890)))). % 9.98/3.42 tff(c_2084, plain, (![V_771, V_672]: (male(V_771, skc10) | ~accessible_world(V_672, V_771) | ~accessible_world(skc8, V_672)))). % 9.98/3.42 tff(c_2703, plain, (![V_131, V_903]: (relname(V_131, V_903) | ~accessible_world(skc12, V_131) | ~forename(skc8, V_903)))). % 9.98/3.42 tff(c_2623, plain, (![V_104, V_895]: (organism(V_104, V_895) | ~accessible_world(skc12, V_104) | ~human_person(skc8, V_895)))). % 9.98/3.42 tff(c_2784, plain, (![V_134, V_913]: (relation(V_134, V_913) | ~accessible_world(skc12, V_134) | ~proposition(skc8, V_913)))). % 9.98/3.42 tff(c_2057, plain, (![V_152, V_760, V_759]: (present(V_152, skf1(V_760)) | ~accessible_world(V_759, V_152) | ~accessible_world(skc12, V_759)))). % 9.98/3.42 tff(c_2583, plain, (![V_80, V_885]: (thing(V_80, V_885) | ~accessible_world(skc12, V_80) | ~abstraction(skc8, V_885)))). % 9.98/3.42 tff(c_2866, plain, (![V_80, V_925]: (thing(V_80, V_925) | ~accessible_world(skc12, V_80) | ~entity(skc8, V_925)))). % 9.98/3.42 tff(c_2448, plain, (![V_86, V_866]: (specific(V_86, V_866) | ~accessible_world(skc12, V_86) | ~entity(skc8, V_866)))). % 9.98/3.42 tff(c_2254, plain, (![V_77, V_827]: (eventuality(V_77, V_827) | ~accessible_world(skc12, V_77) | ~event(skc8, V_827)))). % 9.98/3.42 tff(c_2083, plain, (![V_771, V_671]: (male(V_771, skc15) | ~accessible_world(V_671, V_771) | ~accessible_world(skc8, V_671)))). % 9.98/3.42 tff(c_1683, plain, (![V_98, V_671]: (man(V_98, skc15) | ~accessible_world(V_671, V_98) | ~accessible_world(skc8, V_671)))). % 9.98/3.42 tff(c_2066, plain, (![V_761, V_246, U_245]: (singleton(V_761, V_246) | ~accessible_world(U_245, V_761) | ~entity(U_245, V_246)))). % 9.98/3.42 tff(c_1642, plain, (![V_158, V_658]: (proposition(V_158, skc12) | ~accessible_world(V_658, V_158) | ~accessible_world(skc8, V_658)))). % 9.98/3.43 tff(c_1752, plain, (![V_128, V_684]: (forename(V_128, skc14) | ~accessible_world(V_684, V_128) | ~accessible_world(skc8, V_684)))). % 9.98/3.43 tff(c_2376, plain, (![W_854, V_852, Y_853, U_196]: (W_854=V_852 | ~agent(skc12, Y_853, U_196) | ~theme(skc12, Y_853, W_854) | ~think_believe_consider(skc12, Y_853) | ~think_believe_consider(skc12, skf1(U_196)) | ~theme(skc12, skf1(U_196), V_852) | ~proposition(skc12, W_854) | ~proposition(skc12, V_852) | ~man(skc12, U_196)))). % 9.98/3.43 tff(c_2041, plain, (![V_155, V_756]: (think_believe_consider(V_155, skc13) | ~accessible_world(V_756, V_155) | ~accessible_world(skc8, V_756)))). % 9.98/3.43 tff(c_1997, plain, (![V_74, V_742]: (state(V_74, skc9) | ~accessible_world(V_742, V_74) | ~accessible_world(skc8, V_742)))). % 9.98/3.43 tff(c_1756, plain, (![V_128, V_685]: (forename(V_128, skc11) | ~accessible_world(V_685, V_128) | ~accessible_world(skc8, V_685)))). % 9.98/3.43 tff(c_1885, plain, (![V_709, V_228, U_227]: (relation(V_709, V_228) | ~accessible_world(U_227, V_709) | ~forename(U_227, V_228)))). % 9.98/3.43 tff(c_2930, plain, (![V_946]: (skc12=V_946 | ~theme(skc8, skc13, V_946) | ~proposition(skc8, V_946)))). % 9.98/3.43 tff(c_2067, plain, (![V_761, V_252, U_251]: (singleton(V_761, V_252) | ~accessible_world(U_251, V_761) | ~eventuality(U_251, V_252)))). % 9.98/3.43 tff(c_1695, plain, (![V_98, V_672]: (man(V_98, skc10) | ~accessible_world(V_672, V_98) | ~accessible_world(skc8, V_672)))). % 9.98/3.43 tff(c_2343, plain, (![W_841]: (skc11=W_841 | ~forename(skc8, W_841) | ~of(skc8, W_841, skc10)))). % 9.98/3.43 tff(c_1648, plain, (![V_152, V_661]: (present(V_152, skc13) | ~accessible_world(V_661, V_152) | ~accessible_world(skc8, V_661)))). % 9.98/3.43 tff(c_2379, plain, (![W_854, V_852, Y_853]: (W_854=V_852 | ~agent(skc8, Y_853, skc15) | ~theme(skc8, Y_853, W_854) | ~think_believe_consider(skc8, Y_853) | ~theme(skc8, skc13, V_852) | ~proposition(skc8, W_854) | ~proposition(skc8, V_852)))). % 9.98/3.43 tff(c_1820, plain, (![V_146, V_698]: (jules_forename(V_146, skc11) | ~accessible_world(V_698, V_146) | ~accessible_world(skc8, V_698)))). % 9.98/3.43 tff(c_2346, plain, (![W_841]: (skc14=W_841 | ~forename(skc8, W_841) | ~of(skc8, W_841, skc15)))). % 9.98/3.43 tff(c_1901, plain, (![V_715, V_260, U_259]: (impartial(V_715, V_260) | ~accessible_world(U_259, V_715) | ~human_person(U_259, V_260)))). % 9.98/3.43 tff(c_2065, plain, (![V_761, V_210, U_209]: (singleton(V_761, V_210) | ~accessible_world(U_209, V_761) | ~abstraction(U_209, V_210)))). % 9.98/3.43 tff(c_2114, plain, (![V_783, V_260, U_259]: (living(V_783, V_260) | ~accessible_world(U_259, V_783) | ~human_person(U_259, V_260)))). % 9.98/3.43 tff(c_1809, plain, (![V_95, V_694]: (event(V_95, skc13) | ~accessible_world(V_694, V_95) | ~accessible_world(skc8, V_694)))). % 9.98/3.43 tff(c_2883, plain, (~accessible_world(skc8, skc8))). % 9.98/3.43 tff(c_2093, plain, (![V_161, V_774]: (vincent_forename(V_161, skc14) | ~accessible_world(V_774, V_161) | ~accessible_world(skc8, V_774)))). % 9.98/3.43 tff(c_2188, plain, (![V_808, U_196]: (agent(V_808, skf1(U_196), U_196) | ~accessible_world(skc12, V_808) | ~man(skc12, U_196)))). % 9.98/3.43 tff(c_2867, plain, (![V_925]: (singleton(skc12, V_925) | ~entity(skc8, V_925)))). % 9.98/3.43 tff(c_2859, plain, (![V_923]: (thing(skc12, V_923) | ~entity(skc8, V_923)))). % 9.98/3.43 tff(c_2123, plain, (![V_786, V_24, U_23]: (thing(V_786, V_24) | ~accessible_world(U_23, V_786) | ~entity(U_23, V_24)))). % 9.98/3.43 tff(c_2854, plain, (![V_195]: (~entity(skc8, skf1(V_195))))). % 9.98/3.43 tff(c_2830, plain, (![V_16]: (~entity(skc8, V_16) | ~event(skc12, V_16)))). % 9.98/3.43 tff(c_2801, plain, (![V_917]: (~eventuality(skc12, V_917) | ~entity(skc8, V_917)))). % 9.98/3.43 tff(c_2785, plain, (![V_913]: (abstraction(skc12, V_913) | ~proposition(skc8, V_913)))). % 9.98/3.43 tff(c_2789, plain, (![V_915]: (existent(skc12, V_915) | ~entity(skc8, V_915)))). % 9.98/3.43 tff(c_1652, plain, (![V_662, V_28, U_27]: (existent(V_662, V_28) | ~accessible_world(U_27, V_662) | ~entity(U_27, V_28)))). % 9.98/3.43 tff(c_2777, plain, (![V_911]: (relation(skc12, V_911) | ~proposition(skc8, V_911)))). % 9.98/3.43 tff(c_1886, plain, (![V_709, V_58, U_57]: (relation(V_709, V_58) | ~accessible_world(U_57, V_709) | ~proposition(U_57, V_58)))). % 9.98/3.43 tff(c_2771, plain, (![V_907]: (~abstraction(V_907, skc10) | ~accessible_world(skc12, V_907)))). % 9.98/3.43 tff(c_2753, plain, (![V_906]: (~abstraction(V_906, skc15) | ~accessible_world(skc12, V_906)))). % 9.98/3.43 tff(c_2655, plain, (![V_107]: (entity(V_107, skc10) | ~accessible_world(skc12, V_107)))). % 9.98/3.43 tff(c_2670, plain, (![V_107]: (entity(V_107, skc15) | ~accessible_world(skc12, V_107)))). % 9.98/3.43 tff(c_2712, plain, (![V_904]: (abstraction(skc12, V_904) | ~forename(skc8, V_904)))). % 9.98/3.43 tff(c_2704, plain, (![V_903]: (relation(skc12, V_903) | ~forename(skc8, V_903)))). % 9.98/3.43 tff(c_2696, plain, (![V_901]: (relname(skc12, V_901) | ~forename(skc8, V_901)))). % 9.98/3.43 tff(c_2098, plain, (![V_775, V_40, U_39]: (relname(V_775, V_40) | ~accessible_world(U_39, V_775) | ~forename(U_39, V_40)))). % 9.98/3.43 tff(c_2606, plain, (![V_28]: (~eventuality(skc8, V_28) | ~entity(skc12, V_28)))). % 9.98/3.43 tff(c_2626, plain, (![V_895]: (impartial(skc12, V_895) | ~human_person(skc8, V_895)))). % 9.98/3.43 tff(c_2645, plain, (entity(skc12, skc15))). % 9.98/3.43 tff(c_2625, plain, (![V_895]: (living(skc12, V_895) | ~human_person(skc8, V_895)))). % 9.98/3.43 tff(c_2644, plain, (entity(skc12, skc10))). % 9.98/3.43 tff(c_2624, plain, (![V_895]: (entity(skc12, V_895) | ~human_person(skc8, V_895)))). % 9.98/3.43 tff(c_2610, plain, (![V_893]: (organism(skc12, V_893) | ~human_person(skc8, V_893)))). % 9.98/3.43 tff(c_1622, plain, (![V_648, V_20, U_19]: (organism(V_648, V_20) | ~accessible_world(U_19, V_648) | ~human_person(U_19, V_20)))). % 9.98/3.43 tff(c_2600, plain, (![V_890]: (~existent(skc12, V_890) | ~eventuality(skc8, V_890)))). % 9.98/3.43 tff(c_2592, plain, (![V_888]: (nonexistent(skc12, V_888) | ~eventuality(skc8, V_888)))). % 9.98/3.44 tff(c_1710, plain, (![V_675, V_10, U_9]: (nonexistent(V_675, V_10) | ~accessible_world(U_9, V_675) | ~eventuality(U_9, V_10)))). % 9.98/3.44 tff(c_2584, plain, (![V_885]: (singleton(skc12, V_885) | ~abstraction(skc8, V_885)))). % 9.98/3.44 tff(c_2576, plain, (![V_883]: (thing(skc12, V_883) | ~abstraction(skc8, V_883)))). % 9.98/3.44 tff(c_2124, plain, (![V_786, V_46, U_45]: (thing(V_786, V_46) | ~accessible_world(U_45, V_786) | ~abstraction(U_45, V_46)))). % 9.98/3.44 tff(c_2542, plain, (![V_879]: (~human(skc12, V_879) | ~abstraction(skc8, V_879)))). % 9.98/3.44 tff(c_2530, plain, (![V_875]: (~male(skc12, V_875) | ~eventuality(skc8, V_875)))). % 9.98/3.44 tff(c_2534, plain, (![V_877]: (nonhuman(skc12, V_877) | ~abstraction(skc8, V_877)))). % 9.98/3.44 tff(c_1947, plain, (![V_728, V_48, U_47]: (nonhuman(V_728, V_48) | ~accessible_world(U_47, V_728) | ~abstraction(U_47, V_48)))). % 9.98/3.44 tff(c_2522, plain, (![V_873]: (unisex(skc12, V_873) | ~eventuality(skc8, V_873)))). % 10.15/3.44 tff(c_2166, plain, (![V_798, V_12, U_11]: (unisex(V_798, V_12) | ~accessible_world(U_11, V_798) | ~eventuality(U_11, V_12)))). % 10.15/3.44 tff(c_2474, plain, (![V_50]: (~entity(skc8, V_50) | ~abstraction(skc12, V_50)))). % 10.15/3.44 tff(c_2498, plain, (![V_195]: (~abstraction(skc8, skf1(V_195))))). % 10.15/3.44 tff(c_2437, plain, (![V_16]: (~abstraction(skc8, V_16) | ~event(skc12, V_16)))). % 10.15/3.44 tff(c_2449, plain, (![V_866]: (~general(skc12, V_866) | ~entity(skc8, V_866)))). % 10.15/3.44 tff(c_2420, plain, (![V_861]: (~entity(skc12, V_861) | ~abstraction(skc8, V_861)))). % 10.15/3.44 tff(c_2441, plain, (![V_864]: (specific(skc12, V_864) | ~entity(skc8, V_864)))). % 10.15/3.44 tff(c_1930, plain, (![V_721, V_26, U_25]: (specific(V_721, V_26) | ~accessible_world(U_25, V_721) | ~entity(U_25, V_26)))). % 10.15/3.44 tff(c_2419, plain, (![V_861]: (~eventuality(skc12, V_861) | ~abstraction(skc8, V_861)))). % 10.15/3.44 tff(c_2404, plain, (![V_859]: (general(skc12, V_859) | ~abstraction(skc8, V_859)))). % 10.15/3.44 tff(c_2128, plain, (![V_789, V_50, U_49]: (general(V_789, V_50) | ~accessible_world(U_49, V_789) | ~abstraction(U_49, V_50)))). % 10.15/3.44 tff(c_2385, plain, (![V_50]: (~eventuality(skc8, V_50) | ~abstraction(skc12, V_50)))). % 10.15/3.44 tff(c_2367, plain, (![V_849]: (~general(skc12, V_849) | ~eventuality(skc8, V_849)))). % 10.15/3.44 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)))). % 10.15/3.44 tff(c_2359, plain, (![V_847]: (specific(skc12, V_847) | ~eventuality(skc8, V_847)))). % 10.15/3.44 tff(c_1929, plain, (![V_721, V_8, U_7]: (specific(V_721, V_8) | ~accessible_world(U_7, V_721) | ~eventuality(U_7, V_8)))). % 10.15/3.44 tff(c_2297, plain, (![V_837]: (be(V_837, skc9, skc10, skc10) | ~accessible_world(skc8, V_837)))). % 10.15/3.44 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)))). % 10.15/3.44 tff(c_2268, plain, (![V_828]: (of(V_828, skc11, skc10) | ~accessible_world(skc8, V_828)))). % 10.15/3.44 tff(c_2269, plain, (![V_828]: (of(V_828, skc14, skc15) | ~accessible_world(skc8, V_828)))). % 10.15/3.44 tff(c_2262, plain, (![V_827]: (~abstraction(skc12, V_827) | ~event(skc8, V_827)))). % 10.15/3.44 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)))). % 10.15/3.44 tff(c_2293, plain, (~entity(skc12, skc13))). % 10.15/3.44 tff(c_2292, plain, (~entity(skc12, skc9))). % 10.15/3.44 tff(c_2261, plain, (![V_827]: (~entity(skc12, V_827) | ~event(skc8, V_827)))). % 10.15/3.44 tff(c_132, plain, (![V_164, W_165, X_166, U_163]: (of(V_164, W_165, X_166) | ~of(U_163, W_165, X_166) | ~accessible_world(U_163, V_164)))). % 10.15/3.44 tff(c_2236, plain, (![V_825]: (eventuality(skc12, V_825) | ~event(skc8, V_825)))). % 10.15/3.44 tff(c_1959, plain, (![V_732, V_16, U_15]: (eventuality(V_732, V_16) | ~accessible_world(U_15, V_732) | ~event(U_15, V_16)))). % 10.15/3.44 tff(c_2205, plain, (![V_817]: (theme(V_817, skc13, skc12) | ~accessible_world(skc8, V_817)))). % 10.15/3.44 tff(c_2213, plain, (![V_821]: (~male(skc12, V_821) | ~abstraction(skc8, V_821)))). % 10.15/3.44 tff(c_2201, plain, (![V_815]: (unisex(skc12, V_815) | ~abstraction(skc8, V_815)))). % 10.15/3.44 tff(c_136, plain, (![V_172, W_173, X_174, U_171]: (theme(V_172, W_173, X_174) | ~theme(U_171, W_173, X_174) | ~accessible_world(U_171, V_172)))). % 10.15/3.44 tff(c_2167, plain, (![V_798, V_52, U_51]: (unisex(V_798, V_52) | ~accessible_world(U_51, V_798) | ~abstraction(U_51, V_52)))). % 10.15/3.44 tff(c_2189, plain, (![V_808]: (agent(V_808, skc13, skc15) | ~accessible_world(skc8, V_808)))). % 10.15/3.44 tff(c_2182, plain, (![V_807]: (singleton(skc12, V_807) | ~eventuality(skc8, V_807)))). % 10.15/3.44 tff(c_134, plain, (![V_168, W_169, X_170, U_167]: (agent(V_168, W_169, X_170) | ~agent(U_167, W_169, X_170) | ~accessible_world(U_167, V_168)))). % 10.15/3.44 tff(c_2174, plain, (![V_805]: (thing(skc12, V_805) | ~eventuality(skc8, V_805)))). % 10.15/3.44 tff(c_2122, plain, (![V_786, V_4, U_3]: (thing(V_786, V_4) | ~accessible_world(U_3, V_786) | ~eventuality(U_3, V_4)))). % 10.15/3.44 tff(c_2155, plain, (![V_795]: (abstraction(V_795, skc11) | ~accessible_world(skc12, V_795)))). % 10.15/3.44 tff(c_2156, plain, (![V_795]: (abstraction(V_795, skc14) | ~accessible_world(skc12, V_795)))). % 10.15/3.44 tff(c_2159, plain, (![V_795]: (abstraction(V_795, skc12) | ~accessible_world(skc12, V_795)))). % 10.15/3.44 tff(c_84, plain, (![V_92, W_93, U_91]: (unisex(V_92, W_93) | ~unisex(U_91, W_93) | ~accessible_world(U_91, V_92)))). % 10.15/3.44 tff(c_114, plain, (![V_137, W_138, U_136]: (abstraction(V_137, W_138) | ~abstraction(U_136, W_138) | ~accessible_world(U_136, V_137)))). % 10.15/3.44 tff(c_102, plain, (![V_119, W_120, U_118]: (human(V_119, W_120) | ~human(U_118, W_120) | ~accessible_world(U_118, V_119)))). % 10.15/3.45 tff(c_118, plain, (![V_143, W_144, U_142]: (general(V_143, W_144) | ~general(U_142, W_144) | ~accessible_world(U_142, V_143)))). % 10.15/3.45 tff(c_76, plain, (![V_80, W_81, U_79]: (thing(V_80, W_81) | ~thing(U_79, W_81) | ~accessible_world(U_79, V_80)))). % 10.15/3.45 tff(c_100, plain, (![V_116, W_117, U_115]: (living(V_116, W_117) | ~living(U_115, W_117) | ~accessible_world(U_115, V_116)))). % 10.15/3.45 tff(c_2102, plain, (![V_778, V_191]: (smoke(V_778, skf1(V_191)) | ~accessible_world(skc12, V_778)))). % 10.15/3.45 tff(c_122, plain, (![V_149, W_150, U_148]: (smoke(V_149, W_150) | ~smoke(U_148, W_150) | ~accessible_world(U_148, V_149)))). % 10.15/3.45 tff(c_110, plain, (![V_131, W_132, U_130]: (relname(V_131, W_132) | ~relname(U_130, W_132) | ~accessible_world(U_130, V_131)))). % 10.15/3.45 tff(c_2073, plain, (![V_768]: (vincent_forename(V_768, skc14) | ~accessible_world(skc8, V_768)))). % 10.15/3.45 tff(c_106, plain, (![V_125, W_126, U_124]: (male(V_125, W_126) | ~male(U_124, W_126) | ~accessible_world(U_124, V_125)))). % 10.15/3.45 tff(c_130, plain, (![V_161, W_162, U_160]: (vincent_forename(V_161, W_162) | ~vincent_forename(U_160, W_162) | ~accessible_world(U_160, V_161)))). % 10.15/3.45 tff(c_2052, plain, (![V_757, V_758]: (~entity(V_757, skf1(V_758)) | ~accessible_world(skc12, V_757)))). % 10.15/3.45 tff(c_2051, plain, (![V_757, V_758]: (~abstraction(V_757, skf1(V_758)) | ~accessible_world(skc12, V_757)))). % 10.15/3.45 tff(c_78, plain, (![V_83, W_84, U_82]: (singleton(V_83, W_84) | ~singleton(U_82, W_84) | ~accessible_world(U_82, V_83)))). % 10.15/3.45 tff(c_1632, plain, (![V_651, V_193]: (present(V_651, skf1(V_193)) | ~accessible_world(skc12, V_651)))). % 10.15/3.45 tff(c_1803, plain, (![V_691, V_195]: (event(V_691, skf1(V_195)) | ~accessible_world(skc12, V_691)))). % 10.15/3.45 tff(c_2037, plain, (![V_753]: (think_believe_consider(V_753, skc13) | ~accessible_world(skc8, V_753)))). % 10.15/3.45 tff(c_126, plain, (![V_155, W_156, U_154]: (think_believe_consider(V_155, W_156) | ~think_believe_consider(U_154, W_156) | ~accessible_world(U_154, V_155)))). % 10.15/3.45 tff(c_1876, plain, (![V_691]: (~entity(V_691, skc13) | ~accessible_world(skc8, V_691)))). % 10.15/3.45 tff(c_104, plain, (![V_122, W_123, U_121]: (animate(V_122, W_123) | ~animate(U_121, W_123) | ~accessible_world(U_121, V_122)))). % 10.15/3.45 tff(c_2019, plain, (~abstraction(skc12, skc13))). % 10.15/3.45 tff(c_1919, plain, (![V_691]: (~abstraction(V_691, skc13) | ~accessible_world(skc8, V_691)))). % 10.15/3.45 tff(c_1937, plain, (![U_15]: (~accessible_world(skc8, U_15) | ~event(U_15, skc15)))). % 10.15/3.45 tff(c_90, plain, (![V_101, W_102, U_100]: (human_person(V_101, W_102) | ~human_person(U_100, W_102) | ~accessible_world(U_100, V_101)))). % 10.15/3.45 tff(c_1953, plain, (![U_15]: (~accessible_world(skc8, U_15) | ~event(U_15, skc10)))). % 10.15/3.45 tff(c_1987, plain, (![V_739]: (state(V_739, skc9) | ~accessible_world(skc8, V_739)))). % 10.15/3.45 tff(c_1983, plain, (~abstraction(skc12, skc9))). % 10.15/3.45 tff(c_72, plain, (![V_74, W_75, U_73]: (state(V_74, W_75) | ~state(U_73, W_75) | ~accessible_world(U_73, V_74)))). % 10.15/3.45 tff(c_1972, plain, (![V_735]: (~abstraction(V_735, skc9) | ~accessible_world(skc8, V_735)))). % 10.15/3.45 tff(c_1971, plain, (![V_735]: (~entity(V_735, skc9) | ~accessible_world(skc8, V_735)))). % 10.15/3.45 tff(c_1977, plain, (~abstraction(skc12, skc10))). % 10.15/3.45 tff(c_1719, plain, (![V_678]: (~abstraction(V_678, skc10) | ~accessible_world(skc8, V_678)))). % 10.15/3.45 tff(c_1960, plain, (![V_732]: (eventuality(V_732, skc9) | ~accessible_world(skc8, V_732)))). % 10.15/3.45 tff(c_74, plain, (![V_77, W_78, U_76]: (eventuality(V_77, W_78) | ~eventuality(U_76, W_78) | ~accessible_world(U_76, V_77)))). % 10.15/3.45 tff(c_1718, plain, (![V_678]: (~eventuality(V_678, skc10) | ~accessible_world(skc8, V_678)))). % 10.15/3.45 tff(c_1943, plain, (~abstraction(skc12, skc15))). % 10.15/3.45 tff(c_116, plain, (![V_140, W_141, U_139]: (nonhuman(V_140, W_141) | ~nonhuman(U_139, W_141) | ~accessible_world(U_139, V_140)))). % 10.15/3.45 tff(c_1728, plain, (![V_679]: (~abstraction(V_679, skc15) | ~accessible_world(skc8, V_679)))). % 10.15/3.45 tff(c_1769, plain, (![V_686]: (animate(V_686, skc15) | ~accessible_world(skc8, V_686)))). % 10.15/3.45 tff(c_1727, plain, (![V_679]: (~eventuality(V_679, skc15) | ~accessible_world(skc8, V_679)))). % 10.15/3.45 tff(c_1741, plain, (![V_680]: (animate(V_680, skc10) | ~accessible_world(skc8, V_680)))). % 10.15/3.45 tff(c_80, plain, (![V_86, W_87, U_85]: (specific(V_86, W_87) | ~specific(U_85, W_87) | ~accessible_world(U_85, V_86)))). % 10.15/3.45 tff(c_1920, plain, (![V_195]: (~abstraction(skc12, skf1(V_195))))). % 10.15/3.45 tff(c_1922, plain, (~abstraction(skc8, skc13))). % 10.15/3.45 tff(c_1660, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~event(U_15, V_16)))). % 10.15/3.45 tff(c_98, plain, (![V_113, W_114, U_112]: (impartial(V_113, W_114) | ~impartial(U_112, W_114) | ~accessible_world(U_112, V_113)))). % 10.15/3.45 tff(c_1897, plain, (abstraction(skc12, skc11))). % 10.15/3.45 tff(c_1792, plain, (![V_681]: (abstraction(V_681, skc11) | ~accessible_world(skc8, V_681)))). % 10.15/3.45 tff(c_1768, plain, (![V_686]: (human(V_686, skc15) | ~accessible_world(skc8, V_686)))). % 10.15/3.45 tff(c_1877, plain, (![V_195]: (~entity(skc12, skf1(V_195))))). % 10.15/3.45 tff(c_1879, plain, (~entity(skc8, skc13))). % 10.15/3.45 tff(c_112, plain, (![V_134, W_135, U_133]: (relation(V_134, W_135) | ~relation(U_133, W_135) | ~accessible_world(U_133, V_134)))). % 10.15/3.45 tff(c_1705, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~event(U_15, V_16)))). % 10.15/3.45 tff(c_1842, plain, (![V_702]: (entity(V_702, skc10) | ~accessible_world(skc8, V_702)))). % 10.15/3.45 tff(c_1767, plain, (![V_686]: (entity(V_686, skc15) | ~accessible_world(skc8, V_686)))). % 10.15/3.45 tff(c_94, plain, (![V_107, W_108, U_106]: (entity(V_107, W_108) | ~entity(U_106, W_108) | ~accessible_world(U_106, V_107)))). % 10.15/3.45 tff(c_1835, plain, (abstraction(skc12, skc14))). % 10.15/3.45 tff(c_1793, plain, (![V_681]: (abstraction(V_681, skc14) | ~accessible_world(skc8, V_681)))). % 10.15/3.45 tff(c_1740, plain, (![V_680]: (human(V_680, skc10) | ~accessible_world(skc8, V_680)))). % 10.15/3.45 tff(c_1804, plain, (![V_691]: (event(V_691, skc9) | ~accessible_world(skc8, V_691)))). % 10.15/3.45 tff(c_1813, plain, (![V_695]: (jules_forename(V_695, skc11) | ~accessible_world(skc8, V_695)))). % 10.15/3.45 tff(c_120, plain, (![V_146, W_147, U_145]: (jules_forename(V_146, W_147) | ~jules_forename(U_145, W_147) | ~accessible_world(U_145, V_146)))). % 10.15/3.46 tff(c_1805, plain, (![V_691]: (event(V_691, skc13) | ~accessible_world(skc8, V_691)))). % 10.15/3.46 tff(c_1795, plain, (abstraction(skc8, skc11))). % 10.15/3.46 tff(c_1794, plain, (abstraction(skc8, skc14))). % 10.15/3.46 tff(c_86, plain, (![V_95, W_96, U_94]: (event(V_95, W_96) | ~event(U_94, W_96) | ~accessible_world(U_94, V_95)))). % 10.15/3.46 tff(c_1576, plain, (![U_632, V_633]: (abstraction(U_632, V_633) | ~forename(U_632, V_633)))). % 10.15/3.46 tff(c_331, plain, (![U_49, V_50]: (~entity(U_49, V_50) | ~abstraction(U_49, V_50)))). % 10.15/3.46 tff(c_1684, plain, (![V_671]: (human_person(V_671, skc15) | ~accessible_world(skc8, V_671)))). % 10.15/3.46 tff(c_1748, plain, (![V_681]: (forename(V_681, skc11) | ~accessible_world(skc8, V_681)))). % 10.15/3.46 tff(c_1747, plain, (![V_681]: (forename(V_681, skc14) | ~accessible_world(skc8, V_681)))). % 10.15/3.46 tff(c_108, plain, (![V_128, W_129, U_127]: (forename(V_128, W_129) | ~forename(U_127, W_129) | ~accessible_world(U_127, V_128)))). % 10.15/3.46 tff(c_1696, plain, (![V_672]: (human_person(V_672, skc10) | ~accessible_world(skc8, V_672)))). % 10.15/3.46 tff(c_1685, plain, (![V_671]: (male(V_671, skc15) | ~accessible_world(skc8, V_671)))). % 10.15/3.46 tff(c_1697, plain, (![V_672]: (male(V_672, skc10) | ~accessible_world(skc8, V_672)))). % 10.15/3.46 tff(c_82, plain, (![V_89, W_90, U_88]: (nonexistent(V_89, W_90) | ~nonexistent(U_88, W_90) | ~accessible_world(U_88, V_89)))). % 10.15/3.46 tff(c_1706, plain, (~entity(skc8, skc9))). % 10.15/3.46 tff(c_1605, plain, (![U_27, V_28]: (~eventuality(U_27, V_28) | ~entity(U_27, V_28)))). % 10.15/3.46 tff(c_1673, plain, (![V_668]: (man(V_668, skc10) | ~accessible_world(skc8, V_668)))). % 10.15/3.46 tff(c_1672, plain, (![V_668]: (man(V_668, skc15) | ~accessible_world(skc8, V_668)))). % 10.15/3.46 tff(c_1666, plain, (abstraction(skc12, skc12))). % 10.15/3.46 tff(c_88, plain, (![V_98, W_99, U_97]: (man(V_98, W_99) | ~man(U_97, W_99) | ~accessible_world(U_97, V_98)))). % 10.15/3.46 tff(c_1643, plain, (![V_658]: (abstraction(V_658, skc12) | ~accessible_world(skc8, V_658)))). % 10.15/3.46 tff(c_1661, plain, (~abstraction(skc8, skc9))). % 10.15/3.46 tff(c_336, plain, (![U_49, V_50]: (~eventuality(U_49, V_50) | ~abstraction(U_49, V_50)))). % 10.15/3.46 tff(c_96, plain, (![V_110, W_111, U_109]: (existent(V_110, W_111) | ~existent(U_109, W_111) | ~accessible_world(U_109, V_110)))). % 10.15/3.46 tff(c_1633, plain, (![V_651]: (present(V_651, skc13) | ~accessible_world(skc8, V_651)))). % 10.15/3.46 tff(c_210, plain, (![U_209, V_210]: (singleton(U_209, V_210) | ~abstraction(U_209, V_210)))). % 10.15/3.46 tff(c_1600, plain, (![V_641]: (proposition(V_641, skc12) | ~accessible_world(skc8, V_641)))). % 10.15/3.46 tff(c_281, plain, (![U_245, V_246]: (singleton(U_245, V_246) | ~entity(U_245, V_246)))). % 10.15/3.46 tff(c_320, plain, (![U_259, V_260]: (impartial(U_259, V_260) | ~human_person(U_259, V_260)))). % 10.15/3.46 tff(c_124, plain, (![V_152, W_153, U_151]: (present(V_152, W_153) | ~present(U_151, W_153) | ~accessible_world(U_151, V_152)))). % 10.15/3.46 tff(c_1626, plain, (~event(skc8, skc15))). % 10.15/3.46 tff(c_1618, plain, (~event(skc8, skc10))). % 10.15/3.46 tff(c_1614, plain, (~eventuality(skc8, skc15))). % 10.15/3.46 tff(c_92, plain, (![V_104, W_105, U_103]: (organism(V_104, W_105) | ~organism(U_103, W_105) | ~accessible_world(U_103, V_104)))). % 10.15/3.46 tff(c_1613, plain, (~eventuality(skc8, skc10))). % 10.15/3.46 tff(c_276, plain, (![U_243, V_244]: (~male(U_243, V_244) | ~eventuality(U_243, V_244)))). % 10.15/3.46 tff(c_291, plain, (![U_249, V_250]: (~existent(U_249, V_250) | ~eventuality(U_249, V_250)))). % 10.15/3.46 tff(c_1596, plain, (entity(skc8, skc15))). % 10.15/3.46 tff(c_1595, plain, (entity(skc8, skc10))). % 10.15/3.46 tff(c_128, plain, (![V_158, W_159, U_157]: (proposition(V_158, W_159) | ~proposition(U_157, W_159) | ~accessible_world(U_157, V_158)))). % 10.15/3.46 tff(c_318, plain, (![U_259, V_260]: (entity(U_259, V_260) | ~human_person(U_259, V_260)))). % 10.15/3.46 tff(c_233, plain, (![U_221, V_222]: (~male(U_221, V_222) | ~abstraction(U_221, V_222)))). % 10.15/3.46 tff(c_296, plain, (![U_251, V_252]: (singleton(U_251, V_252) | ~eventuality(U_251, V_252)))). % 10.15/3.46 tff(c_186, plain, (![U_196]: (agent(skc12, skf1(U_196), U_196) | ~man(skc12, U_196)))). % 10.15/3.46 tff(c_240, plain, (![U_227, V_228]: (relation(U_227, V_228) | ~forename(U_227, V_228)))). % 10.15/3.46 tff(c_1570, plain, (![V_193]: (present(skc12, skf1(V_193))))). % 10.15/3.46 tff(c_1293, plain, (![V_191]: (smoke(skc12, skf1(V_191))))). % 10.15/3.46 tff(c_774, plain, (abstraction(skc8, skc12))). % 10.15/3.46 tff(c_215, plain, (![U_211, V_212]: (abstraction(U_211, V_212) | ~proposition(U_211, V_212)))). % 10.15/3.46 tff(c_319, plain, (![U_259, V_260]: (living(U_259, V_260) | ~human_person(U_259, V_260)))). % 10.15/3.46 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)))). % 10.15/3.46 tff(c_761, plain, (![V_195]: (event(skc12, skf1(V_195))))). % 10.15/3.46 tff(c_345, plain, (~abstraction(skc8, skc10))). % 10.15/3.46 tff(c_344, plain, (~abstraction(skc8, skc15))). % 10.15/3.46 tff(c_227, plain, (![U_47, V_48]: (~human(U_47, V_48) | ~abstraction(U_47, V_48)))). % 10.15/3.46 tff(c_326, plain, (![U_263, V_264]: (~general(U_263, V_264) | ~eventuality(U_263, V_264)))). % 10.15/3.46 tff(c_306, plain, (![U_255, V_256]: (~general(U_255, V_256) | ~entity(U_255, V_256)))). % 10.15/3.46 tff(c_8, plain, (![U_7, V_8]: (specific(U_7, V_8) | ~eventuality(U_7, V_8)))). % 10.15/3.46 tff(c_16, plain, (![U_15, V_16]: (eventuality(U_15, V_16) | ~event(U_15, V_16)))). % 10.15/3.46 tff(c_20, plain, (![U_19, V_20]: (organism(U_19, V_20) | ~human_person(U_19, V_20)))). % 10.15/3.46 tff(c_28, plain, (![U_27, V_28]: (existent(U_27, V_28) | ~entity(U_27, V_28)))). % 10.15/3.46 tff(c_26, plain, (![U_25, V_26]: (specific(U_25, V_26) | ~entity(U_25, V_26)))). % 10.15/3.46 tff(c_301, plain, (eventuality(skc8, skc9))). % 10.15/3.46 tff(c_2, plain, (![U_1, V_2]: (eventuality(U_1, V_2) | ~state(U_1, V_2)))). % 10.15/3.46 tff(c_4, plain, (![U_3, V_4]: (thing(U_3, V_4) | ~eventuality(U_3, V_4)))). % 10.15/3.46 tff(c_10, plain, (![U_9, V_10]: (nonexistent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 10.15/3.46 tff(c_286, plain, (event(skc8, skc9))). % 10.15/3.46 tff(c_14, plain, (![U_13, V_14]: (event(U_13, V_14) | ~state(U_13, V_14)))). % 10.15/3.46 tff(c_24, plain, (![U_23, V_24]: (thing(U_23, V_24) | ~entity(U_23, V_24)))). % 10.15/3.46 tff(c_12, plain, (![U_11, V_12]: (unisex(U_11, V_12) | ~eventuality(U_11, V_12)))). % 10.15/3.46 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 10.15/3.46 tff(c_269, plain, (human(skc8, skc15))). % 10.15/3.46 tff(c_268, plain, (human(skc8, skc10))). % 10.15/3.46 tff(c_22, plain, (![U_21, V_22]: (entity(U_21, V_22) | ~organism(U_21, V_22)))). % 10.15/3.46 tff(c_34, plain, (![U_33, V_34]: (human(U_33, V_34) | ~human_person(U_33, V_34)))). % 10.15/3.46 tff(c_260, plain, (animate(skc8, skc10))). % 10.15/3.47 tff(c_256, plain, (animate(skc8, skc15))). % 10.15/3.47 tff(c_252, plain, (human_person(skc8, skc10))). % 10.15/3.47 tff(c_251, plain, (human_person(skc8, skc15))). % 10.15/3.47 tff(c_18, plain, (![U_17, V_18]: (human_person(U_17, V_18) | ~man(U_17, V_18)))). % 10.15/3.47 tff(c_36, plain, (![U_35, V_36]: (animate(U_35, V_36) | ~human_person(U_35, V_36)))). % 10.15/3.47 tff(c_32, plain, (![U_31, V_32]: (living(U_31, V_32) | ~organism(U_31, V_32)))). % 10.15/3.47 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 10.15/3.47 tff(c_40, plain, (![U_39, V_40]: (relname(U_39, V_40) | ~forename(U_39, V_40)))). % 10.15/3.47 tff(c_42, plain, (![U_41, V_42]: (relation(U_41, V_42) | ~relname(U_41, V_42)))). % 10.15/3.47 tff(c_50, plain, (![U_49, V_50]: (general(U_49, V_50) | ~abstraction(U_49, V_50)))). % 10.15/3.47 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~abstraction(U_51, V_52)))). % 10.15/3.47 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 10.15/3.47 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 10.15/3.47 tff(c_48, plain, (![U_47, V_48]: (nonhuman(U_47, V_48) | ~abstraction(U_47, V_48)))). % 10.15/3.47 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~vincent_forename(U_59, V_60)))). % 10.15/3.47 tff(c_58, plain, (![U_57, V_58]: (relation(U_57, V_58) | ~proposition(U_57, V_58)))). % 10.15/3.47 tff(c_46, plain, (![U_45, V_46]: (thing(U_45, V_46) | ~abstraction(U_45, V_46)))). % 10.15/3.47 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~jules_forename(U_53, V_54)))). % 10.15/3.47 tff(c_56, plain, (![U_55, V_56]: (event(U_55, V_56) | ~smoke(U_55, V_56)))). % 10.15/3.47 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))). % 10.15/3.47 tff(c_6, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~thing(U_5, V_6)))). % 10.15/3.47 tff(c_196, plain, (male(skc8, skc10))). % 10.15/3.47 tff(c_195, plain, (male(skc8, skc15))). % 10.15/3.47 tff(c_38, plain, (![U_37, V_38]: (male(U_37, V_38) | ~man(U_37, V_38)))). % 10.15/3.47 tff(c_30, plain, (![U_29, V_30]: (impartial(U_29, V_30) | ~organism(U_29, V_30)))). % 10.15/3.47 tff(c_178, plain, (be(skc8, skc9, skc10, skc10))). % 10.15/3.47 tff(c_174, plain, (theme(skc8, skc13, skc12))). % 10.15/3.47 tff(c_172, plain, (agent(skc8, skc13, skc15))). % 10.15/3.47 tff(c_176, plain, (of(skc8, skc11, skc10))). % 10.15/3.47 tff(c_170, plain, (of(skc8, skc14, skc15))). % 10.15/3.47 tff(c_164, plain, (state(skc8, skc9))). % 10.15/3.47 tff(c_148, plain, (forename(skc8, skc14))). % 10.15/3.47 tff(c_146, plain, (man(skc8, skc15))). % 10.15/3.47 tff(c_162, plain, (man(skc8, skc10))). % 10.15/3.47 tff(c_160, plain, (forename(skc8, skc11))). % 10.15/3.47 tff(c_166, plain, (accessible_world(skc8, skc12))). % 10.15/3.47 tff(c_158, plain, (jules_forename(skc8, skc11))). % 10.15/3.47 tff(c_150, plain, (vincent_forename(skc8, skc14))). % 10.15/3.47 tff(c_152, plain, (event(skc8, skc13))). % 10.15/3.47 tff(c_154, plain, (present(skc8, skc13))). % 10.15/3.47 tff(c_156, plain, (think_believe_consider(skc8, skc13))). % 10.15/3.47 tff(c_168, plain, (proposition(skc8, skc12))). % 10.15/3.47 tff(c_144, plain, (actual_world(skc8))). % 10.15/3.47 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.15/3.47 %------------------------------------------------------------------------------