%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP225-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 8.44s 2.93s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP225-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n021.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 09:31:13 EDT 2025 % 0.13/0.33 % CPUTime : % 8.44/2.93 % 8.44/2.93 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.44/2.93 % 8.44/2.93 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.44/2.94 %$ 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 % 8.44/2.94 % 8.44/2.94 %Foreground sorts: % 8.44/2.94 % 8.44/2.94 % 8.44/2.94 %Background operators: % 8.44/2.94 % 8.44/2.94 % 8.44/2.94 %Foreground operators: % 8.44/2.94 tff(relation, type, relation: ($i * $i) > $o). % 8.44/2.94 tff(forename, type, forename: ($i * $i) > $o). % 8.44/2.94 tff(be, type, be: ($i * $i * $i * $i) > $o). % 8.44/2.94 tff(theme, type, theme: ($i * $i * $i) > $o). % 8.44/2.94 tff(living, type, living: ($i * $i) > $o). % 8.44/2.94 tff(human_person, type, human_person: ($i * $i) > $o). % 8.44/2.94 tff(present, type, present: ($i * $i) > $o). % 8.44/2.94 tff(skc11, type, skc11: $i). % 8.44/2.94 tff(entity, type, entity: ($i * $i) > $o). % 8.44/2.94 tff(skc9, type, skc9: $i). % 8.44/2.94 tff(eventuality, type, eventuality: ($i * $i) > $o). % 8.44/2.94 tff(existent, type, existent: ($i * $i) > $o). % 8.44/2.94 tff(abstraction, type, abstraction: ($i * $i) > $o). % 8.44/2.94 tff(skf1, type, skf1: $i > $i). % 8.44/2.94 tff(skc8, type, skc8: $i). % 8.44/2.94 tff(proposition, type, proposition: ($i * $i) > $o). % 8.44/2.94 tff(relname, type, relname: ($i * $i) > $o). % 8.44/2.94 tff(skc14, type, skc14: $i). % 8.44/2.94 tff(singleton, type, singleton: ($i * $i) > $o). % 8.44/2.94 tff(skc13, type, skc13: $i). % 8.44/2.94 tff(male, type, male: ($i * $i) > $o). % 8.44/2.94 tff(organism, type, organism: ($i * $i) > $o). % 8.44/2.94 tff(animate, type, animate: ($i * $i) > $o). % 8.44/2.94 tff(of, type, of: ($i * $i * $i) > $o). % 8.44/2.94 tff(actual_world, type, actual_world: $i > $o). % 8.44/2.94 tff(agent, type, agent: ($i * $i * $i) > $o). % 8.44/2.94 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 8.44/2.94 tff(general, type, general: ($i * $i) > $o). % 8.44/2.94 tff(smoke, type, smoke: ($i * $i) > $o). % 8.44/2.94 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 8.44/2.94 tff(event, type, event: ($i * $i) > $o). % 8.44/2.94 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 8.44/2.94 tff(state, type, state: ($i * $i) > $o). % 8.44/2.94 tff(thing, type, thing: ($i * $i) > $o). % 8.44/2.94 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 8.44/2.94 tff(skc15, type, skc15: $i). % 8.44/2.94 tff(human, type, human: ($i * $i) > $o). % 8.44/2.94 tff(man, type, man: ($i * $i) > $o). % 8.44/2.94 tff(unisex, type, unisex: ($i * $i) > $o). % 8.44/2.94 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 8.44/2.94 tff(impartial, type, impartial: ($i * $i) > $o). % 8.44/2.94 tff(skc12, type, skc12: $i). % 8.44/2.94 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 8.44/2.94 tff(specific, type, specific: ($i * $i) > $o). % 8.44/2.94 tff(skc10, type, skc10: $i). % 8.44/2.94 % 8.44/2.94 %Saturated clause set: % 8.44/2.94 tff(c_3055, plain, (![V_990, V_606]: (skc11=V_990 | ~think_believe_consider(V_606, skc12) | ~think_believe_consider(V_606, skf1(skc10)) | ~theme(V_606, skf1(skc10), V_990) | ~proposition(V_606, skc11) | ~proposition(V_606, V_990) | ~accessible_world(skc11, V_606) | ~accessible_world(skc8, V_606)))). % 8.44/2.94 tff(c_3049, plain, (![W_902, V_900, V_595]: (W_902=V_900 | ~theme(V_595, skc12, W_902) | ~think_believe_consider(V_595, skc12) | ~think_believe_consider(V_595, skf1(skc10)) | ~theme(V_595, skf1(skc10), V_900) | ~proposition(V_595, W_902) | ~proposition(V_595, V_900) | ~accessible_world(skc11, V_595) | ~accessible_world(skc8, V_595)))). % 8.44/2.94 tff(c_3032, plain, (![V_984, V_606]: (skc11=V_984 | ~agent(V_606, skc12, skc10) | ~think_believe_consider(V_606, skc12) | ~theme(V_606, skc12, V_984) | ~proposition(V_606, skc11) | ~proposition(V_606, V_984) | ~accessible_world(skc8, V_606)))). % 8.44/2.94 tff(c_1547, plain, (![W_646, V_644, V_595, Y_645]: (W_646=V_644 | ~agent(V_595, Y_645, skc10) | ~theme(V_595, Y_645, W_646) | ~think_believe_consider(V_595, Y_645) | ~think_believe_consider(V_595, skc12) | ~theme(V_595, skc12, V_644) | ~proposition(V_595, W_646) | ~proposition(V_595, V_644) | ~accessible_world(skc8, V_595)))). % 8.44/2.94 tff(c_2684, plain, (![W_902, V_900, V_595, U_196]: (W_902=V_900 | ~theme(V_595, skf1(U_196), W_902) | ~think_believe_consider(V_595, skf1(U_196)) | ~theme(V_595, skf1(U_196), V_900) | ~proposition(V_595, W_902) | ~proposition(V_595, V_900) | ~accessible_world(skc11, V_595) | ~man(skc11, U_196)))). % 8.44/2.95 tff(c_2991, plain, (![V_122, V_965]: (animate(V_122, skc10) | ~accessible_world(V_965, V_122) | ~accessible_world(skc11, V_965)))). % 8.44/2.95 tff(c_2986, plain, (![V_119, V_964]: (human(V_119, skc10) | ~accessible_world(V_964, V_119) | ~accessible_world(skc11, V_964)))). % 8.44/2.95 tff(c_2925, plain, (![V_125, V_961]: (male(V_125, skc10) | ~accessible_world(V_961, V_125) | ~accessible_world(skc11, V_961)))). % 8.44/2.95 tff(c_3010, plain, (~accessible_world(skc11, skc8))). % 8.44/2.95 tff(c_2950, plain, (![V_101, V_962]: (human_person(V_101, skc10) | ~accessible_world(V_962, V_101) | ~accessible_world(skc11, V_962)))). % 8.44/2.95 tff(c_2891, plain, (![V_98, V_959]: (man(V_98, skc10) | ~accessible_world(V_959, V_98) | ~accessible_world(skc11, V_959)))). % 8.44/2.95 tff(c_2897, plain, (![V_155, V_960]: (think_believe_consider(V_155, skc12) | ~accessible_world(V_960, V_155) | ~accessible_world(skc11, V_960)))). % 8.44/2.95 tff(c_2969, plain, (![U_15]: (~accessible_world(skc11, U_15) | ~event(U_15, skc10)))). % 8.44/2.95 tff(c_2856, plain, (![V_122]: (animate(V_122, skc10) | ~accessible_world(skc11, V_122)))). % 8.44/2.95 tff(c_2952, plain, (![V_962]: (human(V_962, skc10) | ~accessible_world(skc11, V_962)))). % 8.44/2.95 tff(c_2970, plain, (~think_believe_consider(skc11, skf1(skc10)))). % 8.44/2.95 tff(c_2927, plain, (![V_961]: (~eventuality(V_961, skc10) | ~accessible_world(skc11, V_961)))). % 8.44/2.95 tff(c_2892, plain, (![V_959]: (human_person(V_959, skc10) | ~accessible_world(skc11, V_959)))). % 8.44/2.95 tff(c_2893, plain, (![V_959]: (male(V_959, skc10) | ~accessible_world(skc11, V_959)))). % 8.44/2.95 tff(c_2881, plain, (![V_155]: (think_believe_consider(V_155, skc12) | ~accessible_world(skc11, V_155)))). % 8.44/2.95 tff(c_2793, plain, (![V_98]: (man(V_98, skc10) | ~accessible_world(skc11, V_98)))). % 8.44/2.95 tff(c_2878, plain, (think_believe_consider(skc11, skc12))). % 8.44/2.95 tff(c_2868, plain, (~event(skc11, skc10))). % 8.44/2.95 tff(c_2838, plain, (~eventuality(skc11, skc10))). % 8.44/2.95 tff(c_2811, plain, (animate(skc11, skc10))). % 8.44/2.95 tff(c_2810, plain, (human(skc11, skc10))). % 8.44/2.95 tff(c_2795, plain, (male(skc11, skc10))). % 8.44/2.95 tff(c_2794, plain, (human_person(skc11, skc10))). % 8.44/2.95 tff(c_2784, plain, (man(skc11, skc10))). % 8.44/2.95 tff(c_2342, plain, (![V_116, V_812, V_811]: (living(V_116, V_812) | ~accessible_world(V_811, V_116) | ~accessible_world(skc11, V_811) | ~human_person(skc8, V_812)))). % 8.44/2.95 tff(c_2337, plain, (![V_134, V_810, V_809]: (relation(V_134, V_810) | ~accessible_world(V_809, V_134) | ~accessible_world(skc11, V_809) | ~forename(skc8, V_810)))). % 8.44/2.95 tff(c_2507, plain, (![V_83, V_851, V_850]: (singleton(V_83, V_851) | ~accessible_world(V_850, V_83) | ~accessible_world(skc11, V_850) | ~abstraction(skc8, V_851)))). % 8.44/2.95 tff(c_2346, plain, (![V_83, V_814, V_813]: (singleton(V_83, V_814) | ~accessible_world(V_813, V_83) | ~accessible_world(skc11, V_813) | ~entity(skc8, V_814)))). % 8.44/2.95 tff(c_2359, plain, (![V_83, V_820, V_819]: (singleton(V_83, V_820) | ~accessible_world(V_819, V_83) | ~accessible_world(skc11, V_819) | ~eventuality(skc8, V_820)))). % 8.44/2.95 tff(c_2490, plain, (![V_113, V_847, V_846]: (impartial(V_113, V_847) | ~accessible_world(V_846, V_113) | ~accessible_world(skc11, V_846) | ~human_person(skc8, V_847)))). % 8.44/2.95 tff(c_2152, plain, (![V_86, V_770, V_769]: (specific(V_86, V_770) | ~accessible_world(V_769, V_86) | ~accessible_world(skc11, V_769) | ~entity(skc8, V_770)))). % 8.44/2.95 tff(c_2136, plain, (![V_110, V_766, V_765]: (existent(V_110, V_766) | ~accessible_world(V_765, V_110) | ~accessible_world(skc11, V_765) | ~entity(skc8, V_766)))). % 8.44/2.95 tff(c_2191, plain, (![V_77, V_772, V_771]: (eventuality(V_77, V_772) | ~accessible_world(V_771, V_77) | ~accessible_world(skc11, V_771) | ~event(skc8, V_772)))). % 8.44/2.95 tff(c_2726, plain, (![W_631, V_613]: (skc13=W_631 | ~entity(V_613, skc10) | ~forename(V_613, W_631) | ~of(V_613, W_631, skc10) | ~forename(V_613, skc13) | ~accessible_world(skc8, V_613)))). % 8.44/2.95 tff(c_2272, plain, (![V_92, V_793, V_792]: (unisex(V_92, V_793) | ~accessible_world(V_792, V_92) | ~accessible_world(skc11, V_792) | ~eventuality(skc8, V_793)))). % 8.44/2.95 tff(c_2231, plain, (![V_140, V_778, V_777]: (nonhuman(V_140, V_778) | ~accessible_world(V_777, V_140) | ~accessible_world(skc11, V_777) | ~abstraction(skc8, V_778)))). % 8.44/2.95 tff(c_2201, plain, (![V_134, V_774, V_773]: (relation(V_134, V_774) | ~accessible_world(V_773, V_134) | ~accessible_world(skc11, V_773) | ~proposition(skc8, V_774)))). % 8.44/2.95 tff(c_2310, plain, (![V_104, V_801, V_800]: (organism(V_104, V_801) | ~accessible_world(V_800, V_104) | ~accessible_world(skc11, V_800) | ~human_person(skc8, V_801)))). % 8.44/2.95 tff(c_2325, plain, (![V_80, V_806, V_805]: (thing(V_80, V_806) | ~accessible_world(V_805, V_80) | ~accessible_world(skc11, V_805) | ~entity(skc8, V_806)))). % 8.44/2.95 tff(c_2248, plain, (![V_89, V_785, V_784]: (nonexistent(V_89, V_785) | ~accessible_world(V_784, V_89) | ~accessible_world(skc11, V_784) | ~eventuality(skc8, V_785)))). % 8.44/2.95 tff(c_2144, plain, (![V_80, V_768, V_767]: (thing(V_80, V_768) | ~accessible_world(V_767, V_80) | ~accessible_world(skc11, V_767) | ~abstraction(skc8, V_768)))). % 8.44/2.95 tff(c_2222, plain, (![V_143, V_776, V_775]: (general(V_143, V_776) | ~accessible_world(V_775, V_143) | ~accessible_world(skc11, V_775) | ~abstraction(skc8, V_776)))). % 8.44/2.95 tff(c_2280, plain, (![V_131, V_795, V_794]: (relname(V_131, V_795) | ~accessible_world(V_794, V_131) | ~accessible_world(skc11, V_794) | ~forename(skc8, V_795)))). % 8.44/2.95 tff(c_1954, plain, (![U_718, V_189, Y_188, W_184, V_717]: (W_184=V_189 | ~agent(V_717, Y_188, U_718) | ~theme(V_717, Y_188, W_184) | ~think_believe_consider(V_717, Y_188) | ~think_believe_consider(V_717, skf1(U_718)) | ~theme(V_717, skf1(U_718), V_189) | ~proposition(V_717, W_184) | ~proposition(V_717, V_189) | ~accessible_world(skc11, V_717) | ~man(skc11, U_718)))). % 8.44/2.95 tff(c_2256, plain, (![V_92, V_787, V_786]: (unisex(V_92, V_787) | ~accessible_world(V_786, V_92) | ~accessible_world(skc11, V_786) | ~abstraction(skc8, V_787)))). % 8.44/2.95 tff(c_2288, plain, (![V_86, V_797, V_796]: (specific(V_86, V_797) | ~accessible_world(V_796, V_86) | ~accessible_world(skc11, V_796) | ~eventuality(skc8, V_797)))). % 8.44/2.95 tff(c_2296, plain, (![V_80, V_799, V_798]: (thing(V_80, V_799) | ~accessible_world(V_798, V_80) | ~accessible_world(skc11, V_798) | ~eventuality(skc8, V_799)))). % 8.44/2.95 tff(c_1451, plain, (![V_179, V_626]: (be(V_179, skc9, skc10, skc10) | ~accessible_world(V_626, V_179) | ~accessible_world(skc8, V_626)))). % 8.44/2.95 tff(c_2654, plain, (![V_164, V_619]: (of(V_164, skc13, skc10) | ~accessible_world(V_619, V_164) | ~accessible_world(skc8, V_619)))). % 8.44/2.95 tff(c_1152, plain, (![V_526, V_501, V_500]: (event(V_526, skf1(V_501)) | ~accessible_world(V_500, V_526) | ~accessible_world(skc11, V_500)))). % 8.44/2.96 tff(c_1367, plain, (![V_168, V_602]: (agent(V_168, skc12, skc10) | ~accessible_world(V_602, V_168) | ~accessible_world(skc8, V_602)))). % 8.44/2.96 tff(c_1661, plain, (![V_107, V_667]: (entity(V_107, skc10) | ~accessible_world(V_667, V_107) | ~accessible_world(skc11, V_667)))). % 8.44/2.96 tff(c_2406, plain, (![U_15, V_16]: (~accessible_world(skc11, U_15) | ~abstraction(skc8, V_16) | ~event(U_15, V_16)))). % 8.44/2.96 tff(c_2338, plain, (![V_809, V_810]: (abstraction(V_809, V_810) | ~accessible_world(skc11, V_809) | ~forename(skc8, V_810)))). % 8.44/2.96 tff(c_2503, plain, (![U_49, V_50]: (~accessible_world(skc11, U_49) | ~eventuality(skc8, V_50) | ~abstraction(U_49, V_50)))). % 8.44/2.96 tff(c_2611, plain, (![U_869]: (~accessible_world(skc11, U_869) | ~entity(U_869, skc9)))). % 8.44/2.96 tff(c_2560, plain, (![U_27, V_28]: (~accessible_world(skc11, U_27) | ~eventuality(skc8, V_28) | ~entity(U_27, V_28)))). % 8.44/2.96 tff(c_2420, plain, (![U_49, V_50]: (~accessible_world(skc11, U_49) | ~entity(skc8, V_50) | ~abstraction(U_49, V_50)))). % 8.44/2.96 tff(c_2532, plain, (![U_15, V_16]: (~accessible_world(skc11, U_15) | ~entity(skc8, V_16) | ~event(U_15, V_16)))). % 8.68/2.96 tff(c_2273, plain, (![V_792, V_793]: (~male(V_792, V_793) | ~accessible_world(skc11, V_792) | ~eventuality(skc8, V_793)))). % 8.68/2.96 tff(c_2249, plain, (![V_784, V_785]: (~existent(V_784, V_785) | ~accessible_world(skc11, V_784) | ~eventuality(skc8, V_785)))). % 8.68/2.96 tff(c_2003, plain, (![W_726, V_727, U_196]: (W_726=V_727 | ~theme(skc11, skf1(U_196), W_726) | ~think_believe_consider(skc11, skf1(U_196)) | ~theme(skc11, skf1(U_196), V_727) | ~proposition(skc11, W_726) | ~proposition(skc11, V_727) | ~man(skc11, U_196)))). % 8.68/2.96 tff(c_2192, plain, (![V_771, V_772]: (~entity(V_771, V_772) | ~accessible_world(skc11, V_771) | ~event(skc8, V_772)))). % 8.68/2.96 tff(c_2137, plain, (![V_765, V_766]: (~eventuality(V_765, V_766) | ~accessible_world(skc11, V_765) | ~entity(skc8, V_766)))). % 8.68/2.96 tff(c_1019, plain, (![V_107, V_489]: (entity(V_107, skc10) | ~accessible_world(V_489, V_107) | ~accessible_world(skc8, V_489)))). % 8.68/2.96 tff(c_2145, plain, (![V_767, V_768]: (singleton(V_767, V_768) | ~accessible_world(skc11, V_767) | ~abstraction(skc8, V_768)))). % 8.68/2.96 tff(c_2289, plain, (![V_796, V_797]: (~general(V_796, V_797) | ~accessible_world(skc11, V_796) | ~eventuality(skc8, V_797)))). % 8.68/2.96 tff(c_2313, plain, (![V_800, V_801]: (impartial(V_800, V_801) | ~accessible_world(skc11, V_800) | ~human_person(skc8, V_801)))). % 8.68/2.96 tff(c_2471, plain, (![V_843]: (skc11=V_843 | ~theme(skc8, skc12, V_843) | ~proposition(skc8, V_843)))). % 8.68/2.96 tff(c_1551, plain, (![W_646, V_644, Y_645]: (W_646=V_644 | ~agent(skc8, Y_645, skc10) | ~theme(skc8, Y_645, W_646) | ~think_believe_consider(skc8, Y_645) | ~theme(skc8, skc12, V_644) | ~proposition(skc8, W_646) | ~proposition(skc8, V_644)))). % 8.68/2.96 tff(c_2257, plain, (![V_786, V_787]: (~male(V_786, V_787) | ~accessible_world(skc11, V_786) | ~abstraction(skc8, V_787)))). % 8.68/2.96 tff(c_2224, plain, (![V_775, V_776]: (~entity(V_775, V_776) | ~accessible_world(skc11, V_775) | ~abstraction(skc8, V_776)))). % 8.68/2.96 tff(c_1198, plain, (![V_536, V_475]: (animate(V_536, skc10) | ~accessible_world(V_475, V_536) | ~accessible_world(skc8, V_475)))). % 8.68/2.96 tff(c_2232, plain, (![V_777, V_778]: (~human(V_777, V_778) | ~accessible_world(skc11, V_777) | ~abstraction(skc8, V_778)))). % 8.68/2.96 tff(c_2153, plain, (![V_769, V_770]: (~general(V_769, V_770) | ~accessible_world(skc11, V_769) | ~entity(skc8, V_770)))). % 8.68/2.96 tff(c_2223, plain, (![V_775, V_776]: (~eventuality(V_775, V_776) | ~accessible_world(skc11, V_775) | ~abstraction(skc8, V_776)))). % 8.72/2.97 tff(c_1955, plain, (![V_168, U_718, V_717]: (agent(V_168, skf1(U_718), U_718) | ~accessible_world(V_717, V_168) | ~accessible_world(skc11, V_717) | ~man(skc11, U_718)))). % 8.72/2.97 tff(c_2382, plain, (~event(skc8, skc13))). % 8.72/2.97 tff(c_1049, plain, (![V_497, V_475]: (human(V_497, skc10) | ~accessible_world(V_475, V_497) | ~accessible_world(skc8, V_475)))). % 8.72/2.97 tff(c_2377, plain, (~event(skc8, skc11))). % 8.72/2.97 tff(c_2193, plain, (![V_771, V_772]: (~abstraction(V_771, V_772) | ~accessible_world(skc11, V_771) | ~event(skc8, V_772)))). % 8.72/2.97 tff(c_1432, plain, (![V_172, V_618]: (theme(V_172, skc12, skc11) | ~accessible_world(V_618, V_172) | ~accessible_world(skc8, V_618)))). % 8.72/2.97 tff(c_2297, plain, (![V_798, V_799]: (singleton(V_798, V_799) | ~accessible_world(skc11, V_798) | ~eventuality(skc8, V_799)))). % 8.72/2.97 tff(c_2202, plain, (![V_773, V_774]: (abstraction(V_773, V_774) | ~accessible_world(skc11, V_773) | ~proposition(skc8, V_774)))). % 8.72/2.97 tff(c_2311, plain, (![V_800, V_801]: (entity(V_800, V_801) | ~accessible_world(skc11, V_800) | ~human_person(skc8, V_801)))). % 8.72/2.97 tff(c_2326, plain, (![V_805, V_806]: (singleton(V_805, V_806) | ~accessible_world(skc11, V_805) | ~entity(skc8, V_806)))). % 8.72/2.97 tff(c_2312, plain, (![V_800, V_801]: (living(V_800, V_801) | ~accessible_world(skc11, V_800) | ~human_person(skc8, V_801)))). % 8.72/2.97 tff(c_1694, plain, (![V_134, V_677]: (relation(V_134, V_677) | ~accessible_world(skc11, V_134) | ~forename(skc8, V_677)))). % 8.72/2.97 tff(c_1249, plain, (![V_552, V_524]: (eventuality(V_552, skc9) | ~accessible_world(V_524, V_552) | ~accessible_world(skc8, V_524)))). % 8.72/2.97 tff(c_1773, plain, (![V_80, V_692]: (thing(V_80, V_692) | ~accessible_world(skc11, V_80) | ~entity(skc8, V_692)))). % 8.72/2.97 tff(c_1057, plain, (![V_149, V_501, V_500]: (smoke(V_149, skf1(V_501)) | ~accessible_world(V_500, V_149) | ~accessible_world(skc11, V_500)))). % 8.72/2.97 tff(c_1592, plain, (![V_104, V_657]: (organism(V_104, V_657) | ~accessible_world(skc11, V_104) | ~human_person(skc8, V_657)))). % 8.72/2.97 tff(c_1570, plain, (![V_80, V_652]: (thing(V_80, V_652) | ~accessible_world(skc11, V_80) | ~eventuality(skc8, V_652)))). % 8.72/2.97 tff(c_1464, plain, (![V_86, V_630]: (specific(V_86, V_630) | ~accessible_world(skc11, V_86) | ~eventuality(skc8, V_630)))). % 8.72/2.97 tff(c_1674, plain, (![V_131, V_672]: (relname(V_131, V_672) | ~accessible_world(skc11, V_131) | ~forename(skc8, V_672)))). % 8.72/2.97 tff(c_1793, plain, (![V_92, V_698]: (unisex(V_92, V_698) | ~accessible_world(skc11, V_92) | ~eventuality(skc8, V_698)))). % 8.72/2.97 tff(c_1177, plain, (![V_95, V_530]: (event(V_95, skc9) | ~accessible_world(V_530, V_95) | ~accessible_world(skc8, V_530)))). % 8.72/2.97 tff(c_966, plain, (![V_101, V_475]: (human_person(V_101, skc10) | ~accessible_world(V_475, V_101) | ~accessible_world(skc8, V_475)))). % 8.72/2.97 tff(c_1538, plain, (![V_92, V_641]: (unisex(V_92, V_641) | ~accessible_world(skc11, V_92) | ~abstraction(skc8, V_641)))). % 8.72/2.97 tff(c_1888, plain, (![V_89, V_712]: (nonexistent(V_89, V_712) | ~accessible_world(skc11, V_89) | ~eventuality(skc8, V_712)))). % 8.72/2.97 tff(c_1083, plain, (![V_152, V_511, V_510]: (present(V_152, skf1(V_511)) | ~accessible_world(V_510, V_152) | ~accessible_world(skc11, V_510)))). % 8.72/2.97 tff(c_1239, plain, (![V_125, V_551]: (male(V_125, skc10) | ~accessible_world(V_551, V_125) | ~accessible_world(skc8, V_551)))). % 8.72/2.98 tff(c_1686, plain, (![V_140, V_676]: (nonhuman(V_140, V_676) | ~accessible_world(skc11, V_140) | ~abstraction(skc8, V_676)))). % 8.72/2.98 tff(c_1875, plain, (![V_143, V_708]: (general(V_143, V_708) | ~accessible_world(skc11, V_143) | ~abstraction(skc8, V_708)))). % 8.72/2.98 tff(c_1737, plain, (![V_134, V_683]: (relation(V_134, V_683) | ~accessible_world(skc11, V_134) | ~proposition(skc8, V_683)))). % 8.72/2.98 tff(c_1827, plain, (![V_77, V_703]: (eventuality(V_77, V_703) | ~accessible_world(skc11, V_77) | ~event(skc8, V_703)))). % 8.72/2.98 tff(c_1627, plain, (![V_86, V_663]: (specific(V_86, V_663) | ~accessible_world(skc11, V_86) | ~entity(skc8, V_663)))). % 8.72/2.98 tff(c_1761, plain, (![V_80, V_688]: (thing(V_80, V_688) | ~accessible_world(skc11, V_80) | ~abstraction(skc8, V_688)))). % 8.72/2.98 tff(c_1382, plain, (![V_110, V_610]: (existent(V_110, V_610) | ~accessible_world(skc11, V_110) | ~entity(skc8, V_610)))). % 8.72/2.98 tff(c_1209, plain, (![V_541, V_260, U_259]: (living(V_541, V_260) | ~accessible_world(U_259, V_541) | ~human_person(U_259, V_260)))). % 8.72/2.98 tff(c_913, plain, (![V_83, V_458, U_457]: (singleton(V_83, V_458) | ~accessible_world(U_457, V_83) | ~eventuality(U_457, V_458)))). % 8.72/2.98 tff(c_1333, plain, (![V_161, V_591]: (vincent_forename(V_161, skc13) | ~accessible_world(V_591, V_161) | ~accessible_world(skc8, V_591)))). % 8.72/2.98 tff(c_2108, plain, (![V_146, V_575]: (jules_forename(V_146, skc13) | ~accessible_world(V_575, V_146) | ~accessible_world(skc8, V_575)))). % 8.72/2.98 tff(c_1165, plain, (![V_95, V_529]: (event(V_95, skc12) | ~accessible_world(V_529, V_95) | ~accessible_world(skc8, V_529)))). % 8.72/2.98 tff(c_1190, plain, (![V_532, V_228, U_227]: (relation(V_532, V_228) | ~accessible_world(U_227, V_532) | ~forename(U_227, V_228)))). % 8.72/2.98 tff(c_1106, plain, (![V_128, V_518]: (forename(V_128, skc13) | ~accessible_world(V_518, V_128) | ~accessible_world(skc8, V_518)))). % 8.72/2.98 tff(c_1227, plain, (![V_98, V_550]: (man(V_98, skc10) | ~accessible_world(V_550, V_98) | ~accessible_world(skc8, V_550)))). % 8.72/2.98 tff(c_1318, plain, (![V_582, V_260, U_259]: (impartial(V_582, V_260) | ~accessible_world(U_259, V_582) | ~human_person(U_259, V_260)))). % 8.72/2.98 tff(c_1282, plain, (![V_155, V_567]: (think_believe_consider(V_155, skc12) | ~accessible_world(V_567, V_155) | ~accessible_world(skc8, V_567)))). % 8.72/2.98 tff(c_2051, plain, (![V_572]: (jules_forename(V_572, skc13) | ~accessible_world(skc8, V_572)))). % 8.72/2.98 tff(c_2058, plain, (jules_forename(skc8, skc13))). % 8.72/2.98 tff(c_2043, plain, (skc15=skc13)). % 8.72/2.98 tff(c_1482, plain, (![W_631]: (skc13=W_631 | ~forename(skc8, W_631) | ~of(skc8, W_631, skc10)))). % 8.72/2.98 tff(c_1131, plain, (![V_74, V_524]: (state(V_74, skc9) | ~accessible_world(V_524, V_74) | ~accessible_world(skc8, V_524)))). % 8.72/2.98 tff(c_895, plain, (![V_83, V_447, U_446]: (singleton(V_83, V_447) | ~accessible_world(U_446, V_83) | ~entity(U_446, V_447)))). % 8.72/2.98 tff(c_1079, plain, (![V_152, V_509]: (present(V_152, skc12) | ~accessible_world(V_509, V_152) | ~accessible_world(skc8, V_509)))). % 8.72/2.98 tff(c_1548, plain, (![W_646, V_644, Y_645, U_196]: (W_646=V_644 | ~agent(skc11, Y_645, U_196) | ~theme(skc11, Y_645, W_646) | ~think_believe_consider(skc11, Y_645) | ~think_believe_consider(skc11, skf1(U_196)) | ~theme(skc11, skf1(U_196), V_644) | ~proposition(skc11, W_646) | ~proposition(skc11, V_644) | ~man(skc11, U_196)))). % 8.72/2.98 tff(c_1989, plain, (~accessible_world(skc8, skc8))). % 8.72/2.98 tff(c_1273, plain, (![V_158, V_563]: (proposition(V_158, skc11) | ~accessible_world(V_563, V_158) | ~accessible_world(skc8, V_563)))). % 8.72/2.98 tff(c_909, plain, (![V_83, V_456, U_455]: (singleton(V_83, V_456) | ~accessible_world(U_455, V_83) | ~abstraction(U_455, V_456)))). % 8.72/2.98 tff(c_1979, plain, (![V_195]: (~abstraction(skc8, skf1(V_195))))). % 8.72/2.98 tff(c_1933, plain, (![V_16]: (~abstraction(skc8, V_16) | ~event(skc11, V_16)))). % 8.72/2.98 tff(c_1359, plain, (![V_595, U_196]: (agent(V_595, skf1(U_196), U_196) | ~accessible_world(skc11, V_595) | ~man(skc11, U_196)))). % 8.72/2.98 tff(c_1916, plain, (![V_28]: (~eventuality(skc8, V_28) | ~entity(skc11, V_28)))). % 8.72/2.98 tff(c_1876, plain, (![V_708]: (~eventuality(skc11, V_708) | ~abstraction(skc8, V_708)))). % 8.72/2.98 tff(c_1889, plain, (![V_712]: (~existent(skc11, V_712) | ~eventuality(skc8, V_712)))). % 8.72/2.98 tff(c_1877, plain, (![V_708]: (~entity(skc11, V_708) | ~abstraction(skc8, V_708)))). % 8.72/2.98 tff(c_1881, plain, (![V_710]: (nonexistent(skc11, V_710) | ~eventuality(skc8, V_710)))). % 8.72/2.98 tff(c_1037, plain, (![V_492, V_10, U_9]: (nonexistent(V_492, V_10) | ~accessible_world(U_9, V_492) | ~eventuality(U_9, V_10)))). % 8.72/2.98 tff(c_1857, plain, (![V_706]: (general(skc11, V_706) | ~abstraction(skc8, V_706)))). % 8.72/2.98 tff(c_1852, plain, (~entity(skc11, skc9))). % 8.72/2.98 tff(c_1853, plain, (~entity(skc11, skc12))). % 8.72/2.98 tff(c_1006, plain, (![V_484, V_50, U_49]: (general(V_484, V_50) | ~accessible_world(U_49, V_484) | ~abstraction(U_49, V_50)))). % 8.72/2.98 tff(c_1828, plain, (![V_703]: (~entity(skc11, V_703) | ~event(skc8, V_703)))). % 8.72/2.98 tff(c_1806, plain, (![V_701]: (eventuality(skc11, V_701) | ~event(skc8, V_701)))). % 8.72/2.98 tff(c_1250, plain, (![V_552, V_16, U_15]: (eventuality(V_552, V_16) | ~accessible_world(U_15, V_552) | ~event(U_15, V_16)))). % 8.72/2.98 tff(c_1794, plain, (![V_698]: (~male(skc11, V_698) | ~eventuality(skc8, V_698)))). % 8.72/2.99 tff(c_1786, plain, (![V_696]: (unisex(skc11, V_696) | ~eventuality(skc8, V_696)))). % 8.72/2.99 tff(c_1293, plain, (![V_569, V_12, U_11]: (unisex(V_569, V_12) | ~accessible_world(U_11, V_569) | ~eventuality(U_11, V_12)))). % 8.72/2.99 tff(c_1774, plain, (![V_692]: (singleton(skc11, V_692) | ~entity(skc8, V_692)))). % 8.72/2.99 tff(c_1762, plain, (![V_688]: (singleton(skc11, V_688) | ~abstraction(skc8, V_688)))). % 8.72/2.99 tff(c_1766, plain, (![V_690]: (thing(skc11, V_690) | ~entity(skc8, V_690)))). % 8.72/2.99 tff(c_987, plain, (![V_478, V_24, U_23]: (thing(V_478, V_24) | ~accessible_world(U_23, V_478) | ~entity(U_23, V_24)))). % 8.72/2.99 tff(c_1754, plain, (![V_686]: (thing(skc11, V_686) | ~abstraction(skc8, V_686)))). % 8.72/2.99 tff(c_988, plain, (![V_478, V_46, U_45]: (thing(V_478, V_46) | ~accessible_world(U_45, V_478) | ~abstraction(U_45, V_46)))). % 8.72/2.99 tff(c_1738, plain, (![V_683]: (abstraction(skc11, V_683) | ~proposition(skc8, V_683)))). % 8.72/2.99 tff(c_1730, plain, (![V_681]: (relation(skc11, V_681) | ~proposition(skc8, V_681)))). % 8.72/2.99 tff(c_1191, plain, (![V_532, V_58, U_57]: (relation(V_532, V_58) | ~accessible_world(U_57, V_532) | ~proposition(U_57, V_58)))). % 8.72/2.99 tff(c_1695, plain, (![V_677]: (abstraction(skc11, V_677) | ~forename(skc8, V_677)))). % 8.72/2.99 tff(c_1687, plain, (![V_676]: (~human(skc11, V_676) | ~abstraction(skc8, V_676)))). % 8.72/2.99 tff(c_1675, plain, (![V_672]: (relation(skc11, V_672) | ~forename(skc8, V_672)))). % 8.72/2.99 tff(c_1679, plain, (![V_674]: (nonhuman(skc11, V_674) | ~abstraction(skc8, V_674)))). % 8.72/2.99 tff(c_1262, plain, (![V_557, V_48, U_47]: (nonhuman(V_557, V_48) | ~accessible_world(U_47, V_557) | ~abstraction(U_47, V_48)))). % 8.72/2.99 tff(c_1667, plain, (![V_670]: (relname(skc11, V_670) | ~forename(skc8, V_670)))). % 8.72/2.99 tff(c_1310, plain, (![V_576, V_40, U_39]: (relname(V_576, V_40) | ~accessible_world(U_39, V_576) | ~forename(U_39, V_40)))). % 8.72/2.99 tff(c_1662, plain, (![V_667]: (~abstraction(V_667, skc10) | ~accessible_world(skc11, V_667)))). % 8.72/2.99 tff(c_1611, plain, (![V_107]: (entity(V_107, skc10) | ~accessible_world(skc11, V_107)))). % 8.72/2.99 tff(c_1638, plain, (![V_50]: (~entity(skc8, V_50) | ~abstraction(skc11, V_50)))). % 8.72/2.99 tff(c_1628, plain, (![V_663]: (~general(skc11, V_663) | ~entity(skc8, V_663)))). % 8.72/2.99 tff(c_1595, plain, (![V_657]: (impartial(skc11, V_657) | ~human_person(skc8, V_657)))). % 8.72/2.99 tff(c_1620, plain, (![V_661]: (specific(skc11, V_661) | ~entity(skc8, V_661)))). % 8.72/2.99 tff(c_935, plain, (![V_465, V_26, U_25]: (specific(V_465, V_26) | ~accessible_world(U_25, V_465) | ~entity(U_25, V_26)))). % 8.72/2.99 tff(c_1594, plain, (![V_657]: (living(skc11, V_657) | ~human_person(skc8, V_657)))). % 8.72/2.99 tff(c_1605, plain, (entity(skc11, skc10))). % 8.72/2.99 tff(c_1593, plain, (![V_657]: (entity(skc11, V_657) | ~human_person(skc8, V_657)))). % 8.72/2.99 tff(c_1579, plain, (![V_655]: (organism(skc11, V_655) | ~human_person(skc8, V_655)))). % 8.72/2.99 tff(c_1314, plain, (![V_579, V_20, U_19]: (organism(V_579, V_20) | ~accessible_world(U_19, V_579) | ~human_person(U_19, V_20)))). % 8.72/2.99 tff(c_1571, plain, (![V_652]: (singleton(skc11, V_652) | ~eventuality(skc8, V_652)))). % 8.72/2.99 tff(c_1563, plain, (![V_650]: (thing(skc11, V_650) | ~eventuality(skc8, V_650)))). % 8.72/2.99 tff(c_986, plain, (![V_478, V_4, U_3]: (thing(V_478, V_4) | ~accessible_world(U_3, V_478) | ~eventuality(U_3, V_4)))). % 8.72/2.99 tff(c_1539, plain, (![V_641]: (~male(skc11, V_641) | ~abstraction(skc8, V_641)))). % 8.72/2.99 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)))). % 8.72/2.99 tff(c_1531, plain, (![V_639]: (unisex(skc11, V_639) | ~abstraction(skc8, V_639)))). % 8.72/2.99 tff(c_1294, plain, (![V_569, V_52, U_51]: (unisex(V_569, V_52) | ~accessible_world(U_51, V_569) | ~abstraction(U_51, V_52)))). % 8.72/2.99 tff(c_1502, plain, (![V_16]: (~abstraction(skc11, V_16) | ~event(skc8, V_16)))). % 8.72/2.99 tff(c_1488, plain, (![V_50]: (~eventuality(skc8, V_50) | ~abstraction(skc11, V_50)))). % 8.72/2.99 tff(c_1465, plain, (![V_630]: (~general(skc11, V_630) | ~eventuality(skc8, V_630)))). % 8.72/2.99 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)))). % 8.72/2.99 tff(c_1457, plain, (![V_628]: (specific(skc11, V_628) | ~eventuality(skc8, V_628)))). % 8.72/2.99 tff(c_934, plain, (![V_465, V_8, U_7]: (specific(V_465, V_8) | ~accessible_world(U_7, V_465) | ~eventuality(U_7, V_8)))). % 8.72/2.99 tff(c_1444, plain, (![V_625]: (be(V_625, skc9, skc10, skc10) | ~accessible_world(skc8, V_625)))). % 8.72/2.99 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)))). % 8.72/2.99 tff(c_1427, plain, (![V_613]: (of(V_613, skc13, skc10) | ~accessible_world(skc8, V_613)))). % 8.72/2.99 tff(c_1375, plain, (![V_606]: (theme(V_606, skc12, skc11) | ~accessible_world(skc8, V_606)))). % 8.72/2.99 tff(c_1420, plain, (![V_195]: (~entity(skc8, skf1(V_195))))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1396, plain, (![V_16]: (~entity(skc8, V_16) | ~event(skc11, V_16)))). % 8.72/3.00 tff(c_1383, plain, (![V_610]: (~eventuality(skc11, V_610) | ~entity(skc8, V_610)))). % 8.72/3.00 tff(c_1371, plain, (![V_604]: (existent(skc11, V_604) | ~entity(skc8, V_604)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1322, plain, (![V_585, V_28, U_27]: (existent(V_585, V_28) | ~accessible_world(U_27, V_585) | ~entity(U_27, V_28)))). % 8.72/3.00 tff(c_1360, plain, (![V_595]: (agent(V_595, skc12, skc10) | ~accessible_world(skc8, V_595)))). % 8.72/3.00 tff(c_1349, plain, (![V_592]: (abstraction(V_592, skc13) | ~accessible_world(skc11, V_592)))). % 8.72/3.00 tff(c_1348, plain, (![V_592]: (abstraction(V_592, skc11) | ~accessible_world(skc11, V_592)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1326, plain, (![V_588]: (vincent_forename(V_588, skc13) | ~accessible_world(skc8, V_588)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1287, plain, (abstraction(skc11, skc11))). % 8.72/3.00 tff(c_1274, plain, (![V_563]: (abstraction(V_563, skc11) | ~accessible_world(skc8, V_563)))). % 8.72/3.00 tff(c_1278, plain, (![V_564]: (think_believe_consider(V_564, skc12) | ~accessible_world(skc8, V_564)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1266, plain, (![V_560]: (proposition(V_560, skc11) | ~accessible_world(skc8, V_560)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1257, plain, (![U_15]: (~accessible_world(skc8, U_15) | ~event(U_15, skc10)))). % 8.72/3.00 tff(c_1241, plain, (![V_551]: (~eventuality(V_551, skc10) | ~accessible_world(skc8, V_551)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1213, plain, (![V_544]: (male(V_544, skc10) | ~accessible_world(skc8, V_544)))). % 8.72/3.00 tff(c_1217, plain, (![V_547]: (man(V_547, skc10) | ~accessible_world(skc8, V_547)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1205, plain, (~abstraction(skc11, skc12))). % 8.72/3.00 tff(c_1166, plain, (![V_529]: (~abstraction(V_529, skc12) | ~accessible_world(skc8, V_529)))). % 8.72/3.00 tff(c_1167, plain, (![V_529]: (~entity(V_529, skc12) | ~accessible_world(skc8, V_529)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1141, plain, (![V_525]: (~entity(V_525, skc9) | ~accessible_world(skc8, V_525)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1184, plain, (~abstraction(skc11, skc9))). % 8.72/3.00 tff(c_1142, plain, (![V_525]: (~abstraction(V_525, skc9) | ~accessible_world(skc8, V_525)))). % 8.72/3.00 tff(c_1154, plain, (![V_526]: (event(V_526, skc9) | ~accessible_world(skc8, V_526)))). % 8.72/3.00 tff(c_1155, plain, (![V_526]: (event(V_526, skc12) | ~accessible_world(skc8, V_526)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1132, plain, (![V_524]: (eventuality(V_524, skc9) | ~accessible_world(skc8, V_524)))). % 8.72/3.00 tff(c_1121, plain, (![V_521]: (state(V_521, skc9) | ~accessible_world(skc8, V_521)))). % 8.72/3.00 tff(c_1117, plain, (abstraction(skc11, skc13))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1107, plain, (![V_518]: (abstraction(V_518, skc13) | ~accessible_world(skc8, V_518)))). % 8.72/3.00 tff(c_1091, plain, (![V_514]: (forename(V_514, skc13) | ~accessible_world(skc8, V_514)))). % 8.72/3.00 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)))). % 8.72/3.00 tff(c_1067, plain, (![V_502, V_503]: (~entity(V_502, skf1(V_503)) | ~accessible_world(skc11, V_502)))). % 8.72/3.00 tff(c_1074, plain, (![V_506, V_193]: (present(V_506, skf1(V_193)) | ~accessible_world(skc11, V_506)))). % 8.72/3.00 tff(c_1075, plain, (![V_506]: (present(V_506, skc12) | ~accessible_world(skc8, V_506)))). % 8.87/3.00 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)))). % 8.87/3.00 tff(c_1066, plain, (![V_502, V_503]: (~abstraction(V_502, skf1(V_503)) | ~accessible_world(skc11, V_502)))). % 8.87/3.00 tff(c_1058, plain, (![V_500, V_501]: (event(V_500, skf1(V_501)) | ~accessible_world(skc11, V_500)))). % 8.87/3.00 tff(c_905, plain, (![V_452, V_191]: (smoke(V_452, skf1(V_191)) | ~accessible_world(skc11, V_452)))). % 8.87/3.00 tff(c_1043, plain, (~abstraction(skc11, skc10))). % 8.87/3.00 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)))). % 8.87/3.01 tff(c_1020, plain, (![V_489]: (~abstraction(V_489, skc10) | ~accessible_world(skc8, V_489)))). % 8.87/3.01 tff(c_1031, plain, (![V_195]: (~abstraction(skc11, skf1(V_195))))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_1033, plain, (~abstraction(skc8, skc12))). % 8.87/3.01 tff(c_927, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~event(U_15, V_16)))). % 8.87/3.01 tff(c_967, plain, (![V_475]: (entity(V_475, skc10) | ~accessible_world(skc8, V_475)))). % 8.87/3.01 tff(c_968, plain, (![V_475]: (human(V_475, skc10) | ~accessible_world(skc8, V_475)))). % 8.87/3.01 tff(c_969, plain, (![V_475]: (animate(V_475, skc10) | ~accessible_world(skc8, V_475)))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_999, plain, (![V_195]: (~entity(skc11, skf1(V_195))))). % 8.87/3.01 tff(c_1001, plain, (~entity(skc8, skc12))). % 8.87/3.01 tff(c_977, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~event(U_15, V_16)))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_978, plain, (~entity(skc8, skc9))). % 8.87/3.01 tff(c_890, plain, (![U_27, V_28]: (~eventuality(U_27, V_28) | ~entity(U_27, V_28)))). % 8.87/3.01 tff(c_876, plain, (![V_436]: (human_person(V_436, skc10) | ~accessible_world(skc8, V_436)))). % 8.87/3.01 tff(c_949, plain, (abstraction(skc8, skc13))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_919, plain, (![U_461, V_462]: (abstraction(U_461, V_462) | ~forename(U_461, V_462)))). % 8.87/3.01 tff(c_331, plain, (![U_49, V_50]: (~entity(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.87/3.01 tff(c_928, plain, (~abstraction(skc8, skc9))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_336, plain, (![U_49, V_50]: (~eventuality(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.87/3.01 tff(c_240, plain, (![U_227, V_228]: (relation(U_227, V_228) | ~forename(U_227, V_228)))). % 8.87/3.01 tff(c_319, plain, (![U_259, V_260]: (living(U_259, V_260) | ~human_person(U_259, V_260)))). % 8.87/3.01 tff(c_296, plain, (![U_251, V_252]: (singleton(U_251, V_252) | ~eventuality(U_251, V_252)))). % 8.87/3.01 tff(c_210, plain, (![U_209, V_210]: (singleton(U_209, V_210) | ~abstraction(U_209, V_210)))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_320, plain, (![U_259, V_260]: (impartial(U_259, V_260) | ~human_person(U_259, V_260)))). % 8.87/3.01 tff(c_233, plain, (![U_221, V_222]: (~male(U_221, V_222) | ~abstraction(U_221, V_222)))). % 8.87/3.01 tff(c_281, plain, (![U_245, V_246]: (singleton(U_245, V_246) | ~entity(U_245, V_246)))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_291, plain, (![U_249, V_250]: (~existent(U_249, V_250) | ~eventuality(U_249, V_250)))). % 8.87/3.01 tff(c_885, plain, (~event(skc8, skc10))). % 8.87/3.01 tff(c_881, plain, (~eventuality(skc8, skc10))). % 8.87/3.01 tff(c_276, plain, (![U_243, V_244]: (~male(U_243, V_244) | ~eventuality(U_243, V_244)))). % 8.87/3.01 tff(c_872, plain, (entity(skc8, skc10))). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_318, plain, (![U_259, V_260]: (entity(U_259, V_260) | ~human_person(U_259, V_260)))). % 8.87/3.01 tff(c_867, plain, (abstraction(skc8, skc11))). % 8.87/3.01 tff(c_215, plain, (![U_211, V_212]: (abstraction(U_211, V_212) | ~proposition(U_211, V_212)))). % 8.87/3.01 tff(c_186, plain, (![U_196]: (agent(skc11, skf1(U_196), U_196) | ~man(skc11, U_196)))). % 8.87/3.01 tff(c_561, plain, (be(skc8, skc9, skc10, skc10))). % 8.87/3.01 tff(c_849, plain, (![V_193]: (present(skc11, skf1(V_193))))). % 8.87/3.01 tff(c_767, plain, (![V_191]: (smoke(skc11, skf1(V_191))))). % 8.87/3.01 tff(c_563, plain, (agent(skc8, skc12, skc10))). % 8.87/3.01 tff(c_562, plain, (of(skc8, skc13, skc10))). % 8.87/3.01 tff(c_550, plain, (![V_195]: (event(skc11, skf1(V_195))))). % 8.87/3.01 tff(c_555, plain, (skc14=skc10)). % 8.87/3.01 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)))). % 8.87/3.01 tff(c_344, plain, (~abstraction(skc8, skc10))). % 8.87/3.01 tff(c_227, plain, (![U_47, V_48]: (~human(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.87/3.01 tff(c_326, plain, (![U_263, V_264]: (~general(U_263, V_264) | ~eventuality(U_263, V_264)))). % 8.87/3.01 tff(c_306, plain, (![U_255, V_256]: (~general(U_255, V_256) | ~entity(U_255, V_256)))). % 8.87/3.01 tff(c_8, plain, (![U_7, V_8]: (specific(U_7, V_8) | ~eventuality(U_7, V_8)))). % 8.87/3.01 tff(c_16, plain, (![U_15, V_16]: (eventuality(U_15, V_16) | ~event(U_15, V_16)))). % 8.87/3.01 tff(c_20, plain, (![U_19, V_20]: (organism(U_19, V_20) | ~human_person(U_19, V_20)))). % 8.87/3.01 tff(c_28, plain, (![U_27, V_28]: (existent(U_27, V_28) | ~entity(U_27, V_28)))). % 8.87/3.01 tff(c_26, plain, (![U_25, V_26]: (specific(U_25, V_26) | ~entity(U_25, V_26)))). % 8.87/3.01 tff(c_301, plain, (eventuality(skc8, skc9))). % 8.87/3.01 tff(c_2, plain, (![U_1, V_2]: (eventuality(U_1, V_2) | ~state(U_1, V_2)))). % 8.87/3.01 tff(c_4, plain, (![U_3, V_4]: (thing(U_3, V_4) | ~eventuality(U_3, V_4)))). % 8.87/3.01 tff(c_10, plain, (![U_9, V_10]: (nonexistent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.87/3.01 tff(c_286, plain, (event(skc8, skc9))). % 8.87/3.01 tff(c_14, plain, (![U_13, V_14]: (event(U_13, V_14) | ~state(U_13, V_14)))). % 8.87/3.01 tff(c_24, plain, (![U_23, V_24]: (thing(U_23, V_24) | ~entity(U_23, V_24)))). % 8.87/3.01 tff(c_12, plain, (![U_11, V_12]: (unisex(U_11, V_12) | ~eventuality(U_11, V_12)))). % 8.87/3.01 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 8.87/3.01 tff(c_269, plain, (human(skc8, skc10))). % 8.87/3.01 tff(c_22, plain, (![U_21, V_22]: (entity(U_21, V_22) | ~organism(U_21, V_22)))). % 8.87/3.01 tff(c_34, plain, (![U_33, V_34]: (human(U_33, V_34) | ~human_person(U_33, V_34)))). % 8.87/3.01 tff(c_256, plain, (animate(skc8, skc10))). % 8.87/3.01 tff(c_251, plain, (human_person(skc8, skc10))). % 8.87/3.01 tff(c_18, plain, (![U_17, V_18]: (human_person(U_17, V_18) | ~man(U_17, V_18)))). % 8.87/3.01 tff(c_36, plain, (![U_35, V_36]: (animate(U_35, V_36) | ~human_person(U_35, V_36)))). % 8.87/3.01 tff(c_32, plain, (![U_31, V_32]: (living(U_31, V_32) | ~organism(U_31, V_32)))). % 8.87/3.01 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 8.87/3.01 tff(c_40, plain, (![U_39, V_40]: (relname(U_39, V_40) | ~forename(U_39, V_40)))). % 8.87/3.01 tff(c_42, plain, (![U_41, V_42]: (relation(U_41, V_42) | ~relname(U_41, V_42)))). % 8.87/3.01 tff(c_50, plain, (![U_49, V_50]: (general(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.87/3.01 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~abstraction(U_51, V_52)))). % 8.87/3.01 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 8.87/3.01 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 8.87/3.01 tff(c_48, plain, (![U_47, V_48]: (nonhuman(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.87/3.01 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~vincent_forename(U_59, V_60)))). % 8.87/3.01 tff(c_58, plain, (![U_57, V_58]: (relation(U_57, V_58) | ~proposition(U_57, V_58)))). % 8.87/3.02 tff(c_46, plain, (![U_45, V_46]: (thing(U_45, V_46) | ~abstraction(U_45, V_46)))). % 8.87/3.02 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~jules_forename(U_53, V_54)))). % 8.87/3.02 tff(c_56, plain, (![U_55, V_56]: (event(U_55, V_56) | ~smoke(U_55, V_56)))). % 8.87/3.02 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))). % 8.87/3.02 tff(c_6, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~thing(U_5, V_6)))). % 8.87/3.02 tff(c_195, plain, (male(skc8, skc10))). % 8.87/3.02 tff(c_38, plain, (![U_37, V_38]: (male(U_37, V_38) | ~man(U_37, V_38)))). % 8.87/3.02 tff(c_30, plain, (![U_29, V_30]: (impartial(U_29, V_30) | ~organism(U_29, V_30)))). % 8.87/3.02 tff(c_176, plain, (theme(skc8, skc12, skc11))). % 8.87/3.02 tff(c_164, plain, (accessible_world(skc8, skc11))). % 8.87/3.02 tff(c_162, plain, (proposition(skc8, skc11))). % 8.87/3.02 tff(c_160, plain, (event(skc8, skc12))). % 8.87/3.02 tff(c_166, plain, (man(skc8, skc10))). % 8.87/3.02 tff(c_158, plain, (present(skc8, skc12))). % 8.87/3.02 tff(c_152, plain, (vincent_forename(skc8, skc13))). % 8.87/3.02 tff(c_154, plain, (forename(skc8, skc13))). % 8.87/3.02 tff(c_156, plain, (think_believe_consider(skc8, skc12))). % 8.87/3.02 tff(c_168, plain, (state(skc8, skc9))). % 8.87/3.02 tff(c_144, plain, (actual_world(skc8))). % 8.87/3.02 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.87/3.02 %------------------------------------------------------------------------------