%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP229-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n012.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:41 PM UTC 2025 % Result : Satisfiable 8.37s 2.88s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP229-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 09:33:44 EDT 2025 % 0.13/0.34 % CPUTime : % 8.37/2.88 % 8.37/2.88 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.37/2.88 % 8.37/2.88 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.37/2.89 %$ 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 > skf4 > skf2 > skc9 > skc8 > skc7 > skc6 > skc5 % 8.37/2.89 % 8.37/2.89 %Foreground sorts: % 8.37/2.89 % 8.37/2.89 % 8.37/2.89 %Background operators: % 8.37/2.89 % 8.37/2.89 % 8.37/2.89 %Foreground operators: % 8.37/2.89 tff(relation, type, relation: ($i * $i) > $o). % 8.37/2.89 tff(skf4, type, skf4: $i > $i). % 8.37/2.89 tff(forename, type, forename: ($i * $i) > $o). % 8.37/2.89 tff(be, type, be: ($i * $i * $i * $i) > $o). % 8.37/2.89 tff(skc7, type, skc7: $i). % 8.37/2.89 tff(theme, type, theme: ($i * $i * $i) > $o). % 8.37/2.89 tff(living, type, living: ($i * $i) > $o). % 8.37/2.89 tff(human_person, type, human_person: ($i * $i) > $o). % 8.37/2.89 tff(present, type, present: ($i * $i) > $o). % 8.37/2.89 tff(entity, type, entity: ($i * $i) > $o). % 8.37/2.89 tff(skc9, type, skc9: $i). % 8.37/2.89 tff(eventuality, type, eventuality: ($i * $i) > $o). % 8.37/2.89 tff(existent, type, existent: ($i * $i) > $o). % 8.37/2.89 tff(abstraction, type, abstraction: ($i * $i) > $o). % 8.37/2.89 tff(skc8, type, skc8: $i). % 8.37/2.89 tff(proposition, type, proposition: ($i * $i) > $o). % 8.37/2.89 tff(relname, type, relname: ($i * $i) > $o). % 8.37/2.89 tff(singleton, type, singleton: ($i * $i) > $o). % 8.37/2.89 tff(male, type, male: ($i * $i) > $o). % 8.37/2.89 tff(organism, type, organism: ($i * $i) > $o). % 8.37/2.89 tff(animate, type, animate: ($i * $i) > $o). % 8.37/2.89 tff(of, type, of: ($i * $i * $i) > $o). % 8.37/2.89 tff(actual_world, type, actual_world: $i > $o). % 8.37/2.89 tff(agent, type, agent: ($i * $i * $i) > $o). % 8.37/2.89 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 8.37/2.89 tff(general, type, general: ($i * $i) > $o). % 8.37/2.89 tff(smoke, type, smoke: ($i * $i) > $o). % 8.37/2.89 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 8.37/2.89 tff(event, type, event: ($i * $i) > $o). % 8.37/2.89 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 8.37/2.89 tff(state, type, state: ($i * $i) > $o). % 8.37/2.89 tff(thing, type, thing: ($i * $i) > $o). % 8.37/2.89 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 8.37/2.89 tff(human, type, human: ($i * $i) > $o). % 8.37/2.89 tff(skf2, type, skf2: $i > $i). % 8.37/2.89 tff(man, type, man: ($i * $i) > $o). % 8.37/2.89 tff(skc5, type, skc5: $i). % 8.37/2.89 tff(unisex, type, unisex: ($i * $i) > $o). % 8.37/2.89 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 8.37/2.89 tff(skc6, type, skc6: $i). % 8.37/2.89 tff(impartial, type, impartial: ($i * $i) > $o). % 8.37/2.89 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 8.37/2.89 tff(specific, type, specific: ($i * $i) > $o). % 8.37/2.89 % 8.37/2.89 %Saturated clause set: % 8.37/2.89 tff(c_1349, plain, (![Z_699, V_702, Y_695, X1_697, X_700, V_629, W_701]: (~actual_world(V_629) | ~jules_forename(V_629, skc8) | ~forename(V_629, skc8) | ~be(V_629, X1_697, skc9, skc9) | ~man(V_629, skc9) | ~state(V_629, X1_697) | ~of(V_629, Y_695, Z_699) | ~man(V_629, Z_699) | ~agent(V_629, X_700, Z_699) | ~forename(V_629, Y_695) | ~vincent_forename(V_629, Y_695) | ~theme(V_629, X_700, V_702) | ~event(V_629, X_700) | ~present(V_629, X_700) | ~think_believe_consider(V_629, X_700) | ~event(V_702, W_701) | ~agent(V_702, W_701, skf4(V_702)) | ~present(V_702, W_701) | ~smoke(V_702, W_701) | ~accessible_world(V_629, V_702) | ~proposition(V_629, V_702) | ~accessible_world(skc5, V_629)))). % 8.37/2.89 tff(c_2624, plain, (![V_1028, V_638]: (skc6=V_1028 | ~think_believe_consider(V_638, skc7) | ~think_believe_consider(V_638, skf2(skc9)) | ~theme(V_638, skf2(skc9), V_1028) | ~proposition(V_638, skc6) | ~proposition(V_638, V_1028) | ~accessible_world(skc6, V_638) | ~accessible_world(skc5, V_638)))). % 8.37/2.89 tff(c_2611, plain, (![W_1016, V_1014, V_646]: (W_1016=V_1014 | ~theme(V_646, skc7, W_1016) | ~think_believe_consider(V_646, skc7) | ~think_believe_consider(V_646, skf2(skc9)) | ~theme(V_646, skf2(skc9), V_1014) | ~proposition(V_646, W_1016) | ~proposition(V_646, V_1014) | ~accessible_world(skc6, V_646) | ~accessible_world(skc5, V_646)))). % 8.37/2.89 tff(c_2608, plain, (![W_1016, V_1014, V_646, U_196]: (W_1016=V_1014 | ~theme(V_646, skf2(U_196), W_1016) | ~think_believe_consider(V_646, skf2(U_196)) | ~theme(V_646, skf2(U_196), V_1014) | ~proposition(V_646, W_1016) | ~proposition(V_646, V_1014) | ~accessible_world(skc6, V_646) | ~man(skc6, U_196)))). % 8.37/2.89 tff(c_2616, plain, (~accessible_world(skc6, skc5))). % 8.37/2.89 tff(c_1327, plain, (![Z_688, W_689, V_629, Y_686, V_684, X_683]: (man(V_684, skf4(V_684)) | ~actual_world(V_629) | ~jules_forename(V_629, skc8) | ~forename(V_629, skc8) | ~be(V_629, Z_688, skc9, skc9) | ~man(V_629, skc9) | ~state(V_629, Z_688) | ~of(V_629, X_683, Y_686) | ~man(V_629, Y_686) | ~agent(V_629, W_689, Y_686) | ~forename(V_629, X_683) | ~vincent_forename(V_629, X_683) | ~theme(V_629, W_689, V_684) | ~event(V_629, W_689) | ~present(V_629, W_689) | ~think_believe_consider(V_629, W_689) | ~accessible_world(V_629, V_684) | ~proposition(V_629, V_684) | ~accessible_world(skc5, V_629)))). % 8.37/2.89 tff(c_1673, plain, (![V_769, V_189, Y_188, U_770, W_184]: (W_184=V_189 | ~agent(V_769, Y_188, U_770) | ~theme(V_769, Y_188, W_184) | ~think_believe_consider(V_769, Y_188) | ~think_believe_consider(V_769, skf2(U_770)) | ~theme(V_769, skf2(U_770), V_189) | ~proposition(V_769, W_184) | ~proposition(V_769, V_189) | ~accessible_world(skc6, V_769) | ~man(skc6, U_770)))). % 8.37/2.89 tff(c_2583, plain, (![V_1007, V_638]: (skc6=V_1007 | ~agent(V_638, skc7, skc9) | ~think_believe_consider(V_638, skc7) | ~theme(V_638, skc7, V_1007) | ~proposition(V_638, skc6) | ~proposition(V_638, V_1007) | ~accessible_world(skc5, V_638)))). % 8.37/2.90 tff(c_1278, plain, (![W_677, V_675, V_646, Y_676]: (W_677=V_675 | ~agent(V_646, Y_676, skc9) | ~theme(V_646, Y_676, W_677) | ~think_believe_consider(V_646, Y_676) | ~think_believe_consider(V_646, skc7) | ~theme(V_646, skc7, V_675) | ~proposition(V_646, W_677) | ~proposition(V_646, V_675) | ~accessible_world(skc5, V_646)))). % 8.37/2.90 tff(c_2545, plain, (![V_119, V_992]: (human(V_119, skc9) | ~accessible_world(V_992, V_119) | ~accessible_world(skc6, V_992)))). % 8.37/2.90 tff(c_2529, plain, (![V_122, V_991]: (animate(V_122, skc9) | ~accessible_world(V_991, V_122) | ~accessible_world(skc6, V_991)))). % 8.37/2.90 tff(c_2481, plain, (![V_125, V_988]: (male(V_125, skc9) | ~accessible_world(V_988, V_125) | ~accessible_world(skc6, V_988)))). % 8.37/2.90 tff(c_2506, plain, (![V_101, V_989]: (human_person(V_101, skc9) | ~accessible_world(V_989, V_101) | ~accessible_world(skc6, V_989)))). % 8.37/2.90 tff(c_2453, plain, (![V_155, V_987]: (think_believe_consider(V_155, skc7) | ~accessible_world(V_987, V_155) | ~accessible_world(skc6, V_987)))). % 8.37/2.90 tff(c_2446, plain, (![V_98, V_986]: (man(V_98, skc9) | ~accessible_world(V_986, V_98) | ~accessible_world(skc6, V_986)))). % 8.37/2.90 tff(c_2525, plain, (![U_15]: (~accessible_world(skc6, U_15) | ~event(U_15, skc9)))). % 8.37/2.90 tff(c_2432, plain, (![V_119]: (human(V_119, skc9) | ~accessible_world(skc6, V_119)))). % 8.37/2.90 tff(c_2509, plain, (![V_989]: (animate(V_989, skc9) | ~accessible_world(skc6, V_989)))). % 8.37/2.90 tff(c_2482, plain, (![V_988]: (~eventuality(V_988, skc9) | ~accessible_world(skc6, V_988)))). % 8.37/2.90 tff(c_2447, plain, (![V_986]: (human_person(V_986, skc9) | ~accessible_world(skc6, V_986)))). % 8.37/2.90 tff(c_2448, plain, (![V_986]: (male(V_986, skc9) | ~accessible_world(skc6, V_986)))). % 8.37/2.90 tff(c_2363, plain, (![V_155]: (think_believe_consider(V_155, skc7) | ~accessible_world(skc6, V_155)))). % 8.37/2.90 tff(c_2449, plain, (~think_believe_consider(skc6, skf2(skc9)))). % 8.37/2.90 tff(c_2348, plain, (![V_98]: (man(V_98, skc9) | ~accessible_world(skc6, V_98)))). % 8.37/2.90 tff(c_2418, plain, (~event(skc6, skc9))). % 8.37/2.90 tff(c_2406, plain, (animate(skc6, skc9))). % 8.37/2.90 tff(c_2405, plain, (human(skc6, skc9))). % 8.37/2.90 tff(c_2389, plain, (~eventuality(skc6, skc9))). % 8.37/2.90 tff(c_2349, plain, (human_person(skc6, skc9))). % 8.37/2.90 tff(c_2350, plain, (male(skc6, skc9))). % 8.37/2.90 tff(c_2360, plain, (think_believe_consider(skc6, skc7))). % 8.37/2.90 tff(c_2339, plain, (man(skc6, skc9))). % 8.37/2.90 tff(c_1851, plain, (![W_814, V_815, U_196]: (W_814=V_815 | ~theme(skc6, skf2(U_196), W_814) | ~think_believe_consider(skc6, skf2(U_196)) | ~theme(skc6, skf2(U_196), V_815) | ~proposition(skc6, W_814) | ~proposition(skc6, V_815) | ~man(skc6, U_196)))). % 8.37/2.90 tff(c_2058, plain, (![V_116, V_861, V_860]: (living(V_116, V_861) | ~accessible_world(V_860, V_116) | ~accessible_world(skc6, V_860) | ~human_person(skc5, V_861)))). % 8.37/2.90 tff(c_2096, plain, (![V_83, V_873, V_872]: (singleton(V_83, V_873) | ~accessible_world(V_872, V_83) | ~accessible_world(skc6, V_872) | ~entity(skc5, V_873)))). % 8.37/2.90 tff(c_2100, plain, (![V_113, V_875, V_874]: (impartial(V_113, V_875) | ~accessible_world(V_874, V_113) | ~accessible_world(skc6, V_874) | ~human_person(skc5, V_875)))). % 8.37/2.90 tff(c_2037, plain, (![V_83, V_855, V_854]: (singleton(V_83, V_855) | ~accessible_world(V_854, V_83) | ~accessible_world(skc6, V_854) | ~eventuality(skc5, V_855)))). % 8.37/2.90 tff(c_2041, plain, (![V_83, V_857, V_856]: (singleton(V_83, V_857) | ~accessible_world(V_856, V_83) | ~accessible_world(skc6, V_856) | ~abstraction(skc5, V_857)))). % 8.37/2.90 tff(c_1243, plain, (![W_664, V_629]: (skc8=W_664 | ~entity(V_629, skc9) | ~forename(V_629, W_664) | ~of(V_629, W_664, skc9) | ~forename(V_629, skc8) | ~accessible_world(skc5, V_629)))). % 8.37/2.90 tff(c_2140, plain, (![V_134, V_884, V_883]: (relation(V_134, V_884) | ~accessible_world(V_883, V_134) | ~accessible_world(skc6, V_883) | ~forename(skc5, V_884)))). % 8.37/2.90 tff(c_1887, plain, (![V_110, V_825, V_824]: (existent(V_110, V_825) | ~accessible_world(V_824, V_110) | ~accessible_world(skc6, V_824) | ~entity(skc5, V_825)))). % 8.37/2.90 tff(c_1954, plain, (![V_140, V_839, V_838]: (nonhuman(V_140, V_839) | ~accessible_world(V_838, V_140) | ~accessible_world(skc6, V_838) | ~abstraction(skc5, V_839)))). % 8.37/2.90 tff(c_1946, plain, (![V_89, V_837, V_836]: (nonexistent(V_89, V_837) | ~accessible_world(V_836, V_89) | ~accessible_world(skc6, V_836) | ~eventuality(skc5, V_837)))). % 8.37/2.90 tff(c_1937, plain, (![V_80, V_835, V_834]: (thing(V_80, V_835) | ~accessible_world(V_834, V_80) | ~accessible_world(skc6, V_834) | ~abstraction(skc5, V_835)))). % 8.37/2.90 tff(c_1874, plain, (![V_134, V_823, V_822]: (relation(V_134, V_823) | ~accessible_world(V_822, V_134) | ~accessible_world(skc6, V_822) | ~proposition(skc5, V_823)))). % 8.37/2.90 tff(c_1908, plain, (![V_143, V_827, V_826]: (general(V_143, V_827) | ~accessible_world(V_826, V_143) | ~accessible_world(skc6, V_826) | ~abstraction(skc5, V_827)))). % 8.37/2.90 tff(c_1836, plain, (![V_131, V_813, V_812]: (relname(V_131, V_813) | ~accessible_world(V_812, V_131) | ~accessible_world(skc6, V_812) | ~forename(skc5, V_813)))). % 8.37/2.90 tff(c_1824, plain, (![V_80, V_809, V_808]: (thing(V_80, V_809) | ~accessible_world(V_808, V_80) | ~accessible_world(skc6, V_808) | ~eventuality(skc5, V_809)))). % 8.37/2.90 tff(c_1674, plain, (![V_168, U_770, V_769]: (agent(V_168, skf2(U_770), U_770) | ~accessible_world(V_769, V_168) | ~accessible_world(skc6, V_769) | ~man(skc6, U_770)))). % 8.37/2.90 tff(c_1962, plain, (![V_92, V_841, V_840]: (unisex(V_92, V_841) | ~accessible_world(V_840, V_92) | ~accessible_world(skc6, V_840) | ~abstraction(skc5, V_841)))). % 8.37/2.90 tff(c_1917, plain, (![V_80, V_829, V_828]: (thing(V_80, V_829) | ~accessible_world(V_828, V_80) | ~accessible_world(skc6, V_828) | ~entity(skc5, V_829)))). % 8.37/2.90 tff(c_1814, plain, (![V_104, V_807, V_806]: (organism(V_104, V_807) | ~accessible_world(V_806, V_104) | ~accessible_world(skc6, V_806) | ~human_person(skc5, V_807)))). % 8.37/2.90 tff(c_1783, plain, (![V_77, V_804, V_803]: (eventuality(V_77, V_804) | ~accessible_world(V_803, V_77) | ~accessible_world(skc6, V_803) | ~event(skc5, V_804)))). % 8.37/2.90 tff(c_1858, plain, (![V_86, V_819, V_818]: (specific(V_86, V_819) | ~accessible_world(V_818, V_86) | ~accessible_world(skc6, V_818) | ~eventuality(skc5, V_819)))). % 8.37/2.90 tff(c_1929, plain, (![V_92, V_833, V_832]: (unisex(V_92, V_833) | ~accessible_world(V_832, V_92) | ~accessible_world(skc6, V_832) | ~eventuality(skc5, V_833)))). % 8.37/2.90 tff(c_1866, plain, (![V_86, V_821, V_820]: (specific(V_86, V_821) | ~accessible_world(V_820, V_86) | ~accessible_world(skc6, V_820) | ~entity(skc5, V_821)))). % 8.37/2.90 tff(c_1043, plain, (![V_591, V_523, V_522]: (event(V_591, skf2(V_523)) | ~accessible_world(V_522, V_591) | ~accessible_world(skc6, V_522)))). % 8.37/2.90 tff(c_1188, plain, (![V_168, V_650]: (agent(V_168, skc7, skc9) | ~accessible_world(V_650, V_168) | ~accessible_world(skc5, V_650)))). % 8.37/2.90 tff(c_854, plain, (![V_149, V_523, V_522]: (smoke(V_149, skf2(V_523)) | ~accessible_world(V_522, V_149) | ~accessible_world(skc6, V_522)))). % 8.37/2.90 tff(c_1320, plain, (![V_107, V_681]: (entity(V_107, skc9) | ~accessible_world(V_681, V_107) | ~accessible_world(skc6, V_681)))). % 8.37/2.90 tff(c_1985, plain, (![U_27, V_28]: (~accessible_world(skc6, U_27) | ~eventuality(skc5, V_28) | ~entity(U_27, V_28)))). % 8.37/2.90 tff(c_1998, plain, (![U_49, V_50]: (~accessible_world(skc6, U_49) | ~entity(skc5, V_50) | ~abstraction(U_49, V_50)))). % 8.37/2.90 tff(c_2011, plain, (![U_15, V_16]: (~accessible_world(skc6, U_15) | ~abstraction(skc5, V_16) | ~event(U_15, V_16)))). % 8.37/2.90 tff(c_2024, plain, (![U_49, V_50]: (~accessible_world(skc6, U_49) | ~eventuality(skc5, V_50) | ~abstraction(U_49, V_50)))). % 8.37/2.90 tff(c_2113, plain, (![U_15, V_16]: (~accessible_world(skc6, U_15) | ~entity(skc5, V_16) | ~event(U_15, V_16)))). % 8.37/2.90 tff(c_2141, plain, (![V_883, V_884]: (abstraction(V_883, V_884) | ~accessible_world(skc6, V_883) | ~forename(skc5, V_884)))). % 8.37/2.90 tff(c_1875, plain, (![V_822, V_823]: (abstraction(V_822, V_823) | ~accessible_world(skc6, V_822) | ~proposition(skc5, V_823)))). % 8.37/2.90 tff(c_1133, plain, (![V_164, V_633]: (of(V_164, skc8, skc9) | ~accessible_world(V_633, V_164) | ~accessible_world(skc5, V_633)))). % 8.37/2.90 tff(c_1930, plain, (![V_832, V_833]: (~male(V_832, V_833) | ~accessible_world(skc6, V_832) | ~eventuality(skc5, V_833)))). % 8.37/2.91 tff(c_1817, plain, (![V_806, V_807]: (entity(V_806, V_807) | ~accessible_world(skc6, V_806) | ~human_person(skc5, V_807)))). % 8.37/2.91 tff(c_1837, plain, (![V_812, V_813]: (relation(V_812, V_813) | ~accessible_world(skc6, V_812) | ~forename(skc5, V_813)))). % 8.37/2.91 tff(c_2128, plain, (~event(skc5, skc8))). % 8.37/2.91 tff(c_1090, plain, (![V_152, V_611, V_610]: (present(V_152, skf2(V_611)) | ~accessible_world(V_610, V_152) | ~accessible_world(skc6, V_610)))). % 8.37/2.91 tff(c_2127, plain, (~event(skc5, skc6))). % 8.37/2.91 tff(c_1785, plain, (![V_803, V_804]: (~abstraction(V_803, V_804) | ~accessible_world(skc6, V_803) | ~event(skc5, V_804)))). % 8.37/2.91 tff(c_1888, plain, (![V_824, V_825]: (~eventuality(V_824, V_825) | ~accessible_world(skc6, V_824) | ~entity(skc5, V_825)))). % 8.37/2.91 tff(c_1816, plain, (![V_806, V_807]: (impartial(V_806, V_807) | ~accessible_world(skc6, V_806) | ~human_person(skc5, V_807)))). % 8.37/2.91 tff(c_1393, plain, (![V_83, V_710]: (singleton(V_83, V_710) | ~accessible_world(skc6, V_83) | ~entity(skc5, V_710)))). % 8.37/2.91 tff(c_1910, plain, (![V_826, V_827]: (~entity(V_826, V_827) | ~accessible_world(skc6, V_826) | ~abstraction(skc5, V_827)))). % 8.37/2.91 tff(c_971, plain, (![V_559, V_544]: (animate(V_559, skc9) | ~accessible_world(V_544, V_559) | ~accessible_world(skc5, V_544)))). % 8.37/2.91 tff(c_1177, plain, (![V_172, V_645]: (theme(V_172, skc7, skc6) | ~accessible_world(V_645, V_172) | ~accessible_world(skc5, V_645)))). % 8.37/2.91 tff(c_1081, plain, (![V_606, V_544]: (entity(V_606, skc9) | ~accessible_world(V_544, V_606) | ~accessible_world(skc5, V_544)))). % 8.37/2.91 tff(c_823, plain, (![V_119, V_511]: (human(V_119, skc9) | ~accessible_world(V_511, V_119) | ~accessible_world(skc5, V_511)))). % 8.37/2.91 tff(c_1270, plain, (![V_116, V_672]: (living(V_116, V_672) | ~accessible_world(skc6, V_116) | ~human_person(skc5, V_672)))). % 8.37/2.91 tff(c_1784, plain, (![V_803, V_804]: (~entity(V_803, V_804) | ~accessible_world(skc6, V_803) | ~event(skc5, V_804)))). % 8.37/2.91 tff(c_1938, plain, (![V_834, V_835]: (singleton(V_834, V_835) | ~accessible_world(skc6, V_834) | ~abstraction(skc5, V_835)))). % 8.37/2.91 tff(c_1642, plain, (![V_83, V_759]: (singleton(V_83, V_759) | ~accessible_world(skc6, V_83) | ~eventuality(skc5, V_759)))). % 8.37/2.91 tff(c_1963, plain, (![V_840, V_841]: (~male(V_840, V_841) | ~accessible_world(skc6, V_840) | ~abstraction(skc5, V_841)))). % 8.37/2.91 tff(c_1859, plain, (![V_818, V_819]: (~general(V_818, V_819) | ~accessible_world(skc6, V_818) | ~eventuality(skc5, V_819)))). % 8.37/2.91 tff(c_1909, plain, (![V_826, V_827]: (~eventuality(V_826, V_827) | ~accessible_world(skc6, V_826) | ~abstraction(skc5, V_827)))). % 8.37/2.91 tff(c_1867, plain, (![V_820, V_821]: (~general(V_820, V_821) | ~accessible_world(skc6, V_820) | ~entity(skc5, V_821)))). % 8.37/2.91 tff(c_1947, plain, (![V_836, V_837]: (~existent(V_836, V_837) | ~accessible_world(skc6, V_836) | ~eventuality(skc5, V_837)))). % 8.37/2.91 tff(c_1955, plain, (![V_838, V_839]: (~human(V_838, V_839) | ~accessible_world(skc6, V_838) | ~abstraction(skc5, V_839)))). % 8.37/2.91 tff(c_1555, plain, (![V_92, V_746]: (unisex(V_92, V_746) | ~accessible_world(skc6, V_92) | ~abstraction(skc5, V_746)))). % 8.37/2.91 tff(c_1404, plain, (![V_140, V_714]: (nonhuman(V_140, V_714) | ~accessible_world(skc6, V_140) | ~abstraction(skc5, V_714)))). % 8.37/2.91 tff(c_1543, plain, (![V_89, V_742]: (nonexistent(V_89, V_742) | ~accessible_world(skc6, V_89) | ~eventuality(skc5, V_742)))). % 8.37/2.91 tff(c_1939, plain, (~jules_forename(skc5, skc8))). % 8.37/2.91 tff(c_1653, plain, (![V_80, V_763]: (thing(V_80, V_763) | ~accessible_world(skc6, V_80) | ~abstraction(skc5, V_763)))). % 8.37/2.91 tff(c_1456, plain, (![V_92, V_725]: (unisex(V_92, V_725) | ~accessible_world(skc6, V_92) | ~eventuality(skc5, V_725)))). % 8.37/2.91 tff(c_994, plain, (![V_572, V_542]: (human_person(V_572, skc9) | ~accessible_world(V_542, V_572) | ~accessible_world(skc5, V_542)))). % 8.37/2.91 tff(c_1388, plain, (![V_80, V_709]: (thing(V_80, V_709) | ~accessible_world(skc6, V_80) | ~entity(skc5, V_709)))). % 8.37/2.91 tff(c_1202, plain, (![V_143, V_654]: (general(V_143, V_654) | ~accessible_world(skc6, V_143) | ~abstraction(skc5, V_654)))). % 8.37/2.91 tff(c_1144, plain, (![V_110, V_637]: (existent(V_110, V_637) | ~accessible_world(skc6, V_110) | ~entity(skc5, V_637)))). % 8.37/2.91 tff(c_1519, plain, (![V_134, V_737]: (relation(V_134, V_737) | ~accessible_world(skc6, V_134) | ~proposition(skc5, V_737)))). % 8.37/2.91 tff(c_1342, plain, (![V_86, V_694]: (specific(V_86, V_694) | ~accessible_world(skc6, V_86) | ~entity(skc5, V_694)))). % 8.37/2.91 tff(c_1476, plain, (![V_86, V_730]: (specific(V_86, V_730) | ~accessible_world(skc6, V_86) | ~eventuality(skc5, V_730)))). % 8.37/2.91 tff(c_1279, plain, (![W_677, V_675, Y_676, U_196]: (W_677=V_675 | ~agent(skc6, Y_676, U_196) | ~theme(skc6, Y_676, W_677) | ~think_believe_consider(skc6, Y_676) | ~think_believe_consider(skc6, skf2(U_196)) | ~theme(skc6, skf2(U_196), V_675) | ~proposition(skc6, W_677) | ~proposition(skc6, V_675) | ~man(skc6, U_196)))). % 8.37/2.91 tff(c_1424, plain, (![V_131, V_719]: (relname(V_131, V_719) | ~accessible_world(skc6, V_131) | ~forename(skc5, V_719)))). % 8.37/2.91 tff(c_1015, plain, (![V_581, V_542]: (male(V_581, skc9) | ~accessible_world(V_542, V_581) | ~accessible_world(skc5, V_542)))). % 8.37/2.91 tff(c_1637, plain, (![V_80, V_758]: (thing(V_80, V_758) | ~accessible_world(skc6, V_80) | ~eventuality(skc5, V_758)))). % 8.37/2.91 tff(c_1263, plain, (![V_104, V_671]: (organism(V_104, V_671) | ~accessible_world(skc6, V_104) | ~human_person(skc5, V_671)))). % 8.37/2.91 tff(c_1733, plain, (![V_795]: (skc6=V_795 | ~theme(skc5, skc7, V_795) | ~proposition(skc5, V_795)))). % 8.37/2.91 tff(c_1624, plain, (![V_77, V_754]: (eventuality(V_77, V_754) | ~accessible_world(skc6, V_77) | ~event(skc5, V_754)))). % 8.37/2.91 tff(c_1055, plain, (![V_95, V_594]: (event(V_95, skc7) | ~accessible_world(V_594, V_95) | ~accessible_world(skc5, V_594)))). % 8.37/2.91 tff(c_892, plain, (![V_98, V_542]: (man(V_98, skc9) | ~accessible_world(V_542, V_98) | ~accessible_world(skc5, V_542)))). % 8.37/2.91 tff(c_1086, plain, (![V_152, V_609]: (present(V_152, skc7) | ~accessible_world(V_609, V_152) | ~accessible_world(skc5, V_609)))). % 8.37/2.91 tff(c_1282, plain, (![W_677, V_675, Y_676]: (W_677=V_675 | ~agent(skc5, Y_676, skc9) | ~theme(skc5, Y_676, W_677) | ~think_believe_consider(skc5, Y_676) | ~theme(skc5, skc7, V_675) | ~proposition(skc5, W_677) | ~proposition(skc5, V_675)))). % 8.37/2.91 tff(c_983, plain, (![V_566, V_40, U_39]: (relation(V_566, V_40) | ~accessible_world(U_39, V_566) | ~forename(U_39, V_40)))). % 8.37/2.91 tff(c_1009, plain, (![V_578, V_275, U_274]: (singleton(V_578, V_275) | ~accessible_world(U_274, V_578) | ~eventuality(U_274, V_275)))). % 8.37/2.91 tff(c_869, plain, (![V_528, V_255, U_254]: (living(V_528, V_255) | ~accessible_world(U_254, V_528) | ~human_person(U_254, V_255)))). % 8.37/2.91 tff(c_1034, plain, (![V_161, V_590]: (vincent_forename(V_161, skc8) | ~accessible_world(V_590, V_161) | ~accessible_world(skc5, V_590)))). % 8.37/2.91 tff(c_1099, plain, (![V_155, V_618]: (think_believe_consider(V_155, skc7) | ~accessible_world(V_618, V_155) | ~accessible_world(skc5, V_618)))). % 8.37/2.91 tff(c_1007, plain, (![V_578, V_235, U_234]: (singleton(V_578, V_235) | ~accessible_world(U_234, V_578) | ~abstraction(U_234, V_235)))). % 8.37/2.91 tff(c_1246, plain, (![W_664]: (skc8=W_664 | ~forename(skc5, W_664) | ~of(skc5, W_664, skc9)))). % 8.37/2.91 tff(c_1008, plain, (![V_578, V_251, U_250]: (singleton(V_578, V_251) | ~accessible_world(U_250, V_578) | ~entity(U_250, V_251)))). % 8.37/2.91 tff(c_999, plain, (![V_575, V_255, U_254]: (impartial(V_575, V_255) | ~accessible_world(U_254, V_575) | ~human_person(U_254, V_255)))). % 8.37/2.91 tff(c_1183, plain, (![V_646, U_196]: (agent(V_646, skf2(U_196), U_196) | ~accessible_world(skc6, V_646) | ~man(skc6, U_196)))). % 8.37/2.91 tff(c_901, plain, (![V_128, V_543]: (forename(V_128, skc8) | ~accessible_world(V_543, V_128) | ~accessible_world(skc5, V_543)))). % 8.37/2.91 tff(c_1663, plain, (~accessible_world(skc5, skc5))). % 8.37/2.91 tff(c_1124, plain, (![V_158, V_628]: (proposition(V_158, skc6) | ~accessible_world(V_628, V_158) | ~accessible_world(skc5, V_628)))). % 8.37/2.91 tff(c_1654, plain, (![V_763]: (singleton(skc6, V_763) | ~abstraction(skc5, V_763)))). % 8.37/2.91 tff(c_1646, plain, (![V_761]: (thing(skc6, V_761) | ~abstraction(skc5, V_761)))). % 8.68/2.91 tff(c_1109, plain, (![V_619, V_46, U_45]: (thing(V_619, V_46) | ~accessible_world(U_45, V_619) | ~abstraction(U_45, V_46)))). % 8.68/2.91 tff(c_1638, plain, (![V_758]: (singleton(skc6, V_758) | ~eventuality(skc5, V_758)))). % 8.68/2.91 tff(c_1630, plain, (![V_756]: (thing(skc6, V_756) | ~eventuality(skc5, V_756)))). % 8.68/2.91 tff(c_1107, plain, (![V_619, V_4, U_3]: (thing(V_619, V_4) | ~accessible_world(U_3, V_619) | ~eventuality(U_3, V_4)))). % 8.68/2.91 tff(c_1599, plain, (![V_752]: (eventuality(skc6, V_752) | ~event(skc5, V_752)))). % 8.68/2.91 tff(c_828, plain, (![V_512, V_16, U_15]: (eventuality(V_512, V_16) | ~accessible_world(U_15, V_512) | ~event(U_15, V_16)))). % 8.68/2.91 tff(c_1595, plain, (~entity(skc6, skc7))). % 8.68/2.91 tff(c_1580, plain, (![V_16]: (~entity(skc6, V_16) | ~event(skc5, V_16)))). % 8.68/2.91 tff(c_1566, plain, (![V_28]: (~eventuality(skc5, V_28) | ~entity(skc6, V_28)))). % 8.68/2.91 tff(c_1556, plain, (![V_746]: (~male(skc6, V_746) | ~abstraction(skc5, V_746)))). % 8.68/2.91 tff(c_1544, plain, (![V_742]: (~existent(skc6, V_742) | ~eventuality(skc5, V_742)))). % 8.68/2.91 tff(c_1548, plain, (![V_744]: (unisex(skc6, V_744) | ~abstraction(skc5, V_744)))). % 8.68/2.91 tff(c_801, plain, (![V_503, V_52, U_51]: (unisex(V_503, V_52) | ~accessible_world(U_51, V_503) | ~abstraction(U_51, V_52)))). % 8.68/2.91 tff(c_1536, plain, (![V_740]: (nonexistent(skc6, V_740) | ~eventuality(skc5, V_740)))). % 8.68/2.91 tff(c_1061, plain, (![V_595, V_10, U_9]: (nonexistent(V_595, V_10) | ~accessible_world(U_9, V_595) | ~eventuality(U_9, V_10)))). % 8.68/2.91 tff(c_1520, plain, (![V_737]: (abstraction(skc6, V_737) | ~proposition(skc5, V_737)))). % 8.68/2.92 tff(c_1512, plain, (![V_735]: (relation(skc6, V_735) | ~proposition(skc5, V_735)))). % 8.68/2.92 tff(c_984, plain, (![V_566, V_58, U_57]: (relation(V_566, V_58) | ~accessible_world(U_57, V_566) | ~proposition(U_57, V_58)))). % 8.68/2.92 tff(c_1493, plain, (![V_16]: (~abstraction(skc6, V_16) | ~event(skc5, V_16)))). % 8.68/2.92 tff(c_1487, plain, (![V_50]: (~eventuality(skc5, V_50) | ~abstraction(skc6, V_50)))). % 8.68/2.92 tff(c_1477, plain, (![V_730]: (~general(skc6, V_730) | ~eventuality(skc5, V_730)))). % 8.68/2.92 tff(c_1469, plain, (![V_728]: (specific(skc6, V_728) | ~eventuality(skc5, V_728)))). % 8.68/2.92 tff(c_1022, plain, (![V_584, V_8, U_7]: (specific(V_584, V_8) | ~accessible_world(U_7, V_584) | ~eventuality(U_7, V_8)))). % 8.68/2.92 tff(c_1457, plain, (![V_725]: (~male(skc6, V_725) | ~eventuality(skc5, V_725)))). % 8.68/2.92 tff(c_1449, plain, (![V_723]: (unisex(skc6, V_723) | ~eventuality(skc5, V_723)))). % 8.68/2.92 tff(c_800, plain, (![V_503, V_12, U_11]: (unisex(V_503, V_12) | ~accessible_world(U_11, V_503) | ~eventuality(U_11, V_12)))). % 8.68/2.92 tff(c_1433, plain, (![V_720]: (abstraction(skc6, V_720) | ~forename(skc5, V_720)))). % 8.68/2.92 tff(c_1425, plain, (![V_719]: (relation(skc6, V_719) | ~forename(skc5, V_719)))). % 8.68/2.92 tff(c_1417, plain, (![V_717]: (relname(skc6, V_717) | ~forename(skc5, V_717)))). % 8.68/2.92 tff(c_988, plain, (![V_569, V_40, U_39]: (relname(V_569, V_40) | ~accessible_world(U_39, V_569) | ~forename(U_39, V_40)))). % 8.68/2.92 tff(c_1405, plain, (![V_714]: (~human(skc6, V_714) | ~abstraction(skc5, V_714)))). % 8.68/2.92 tff(c_1397, plain, (![V_712]: (nonhuman(skc6, V_712) | ~abstraction(skc5, V_712)))). % 8.68/2.92 tff(c_977, plain, (![V_563, V_48, U_47]: (nonhuman(V_563, V_48) | ~accessible_world(U_47, V_563) | ~abstraction(U_47, V_48)))). % 8.68/2.92 tff(c_1389, plain, (![V_709]: (singleton(skc6, V_709) | ~entity(skc5, V_709)))). % 8.68/2.92 tff(c_1381, plain, (![V_707]: (thing(skc6, V_707) | ~entity(skc5, V_707)))). % 8.68/2.92 tff(c_1108, plain, (![V_619, V_24, U_23]: (thing(V_619, V_24) | ~accessible_world(U_23, V_619) | ~entity(U_23, V_24)))). % 8.68/2.92 tff(c_1362, plain, (![V_50]: (~entity(skc5, V_50) | ~abstraction(skc6, V_50)))). % 8.68/2.92 tff(c_1343, plain, (![V_694]: (~general(skc6, V_694) | ~entity(skc5, V_694)))). % 8.68/2.92 tff(c_178, plain, (![V_213, Z_208, X_211, Y_212, W_205, U_207, X2_210, X1_209, X3_206]: (~actual_world(U_207) | ~of(U_207, X3_206, X2_210) | ~jules_forename(U_207, X3_206) | ~forename(U_207, X3_206) | ~be(U_207, X1_209, X2_210, X2_210) | ~man(U_207, X2_210) | ~state(U_207, X1_209) | ~of(U_207, Y_212, Z_208) | ~man(U_207, Z_208) | ~agent(U_207, X_211, Z_208) | ~forename(U_207, Y_212) | ~vincent_forename(U_207, Y_212) | ~theme(U_207, X_211, V_213) | ~event(U_207, X_211) | ~present(U_207, X_211) | ~think_believe_consider(U_207, X_211) | ~event(V_213, W_205) | ~agent(V_213, W_205, skf4(V_213)) | ~present(V_213, W_205) | ~smoke(V_213, W_205) | ~accessible_world(U_207, V_213) | ~proposition(U_207, V_213)))). % 8.68/2.92 tff(c_1335, plain, (![V_692]: (specific(skc6, V_692) | ~entity(skc5, V_692)))). % 8.68/2.92 tff(c_1023, plain, (![V_584, V_26, U_25]: (specific(V_584, V_26) | ~accessible_world(U_25, V_584) | ~entity(U_25, V_26)))). % 8.68/2.92 tff(c_1321, plain, (![V_681]: (~abstraction(V_681, skc9) | ~accessible_world(skc6, V_681)))). % 8.68/2.92 tff(c_176, plain, (![X1_200, U_198, X2_201, Y_203, X_202, Z_199, W_197, V_204]: (man(V_204, skf4(V_204)) | ~actual_world(U_198) | ~of(U_198, X2_201, X1_200) | ~jules_forename(U_198, X2_201) | ~forename(U_198, X2_201) | ~be(U_198, Z_199, X1_200, X1_200) | ~man(U_198, X1_200) | ~state(U_198, Z_199) | ~of(U_198, X_202, Y_203) | ~man(U_198, Y_203) | ~agent(U_198, W_197, Y_203) | ~forename(U_198, X_202) | ~vincent_forename(U_198, X_202) | ~theme(U_198, W_197, V_204) | ~event(U_198, W_197) | ~present(U_198, W_197) | ~think_believe_consider(U_198, W_197) | ~accessible_world(U_198, V_204) | ~proposition(U_198, V_204)))). % 8.68/2.92 tff(c_1302, plain, (![V_107]: (entity(V_107, skc9) | ~accessible_world(skc6, V_107)))). % 8.68/2.92 tff(c_1265, plain, (![V_671]: (impartial(skc6, V_671) | ~human_person(skc5, V_671)))). % 8.68/2.92 tff(c_1292, plain, (entity(skc6, skc9))). % 8.68/2.92 tff(c_1266, plain, (![V_671]: (entity(skc6, V_671) | ~human_person(skc5, V_671)))). % 8.68/2.92 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.68/2.92 tff(c_1264, plain, (![V_671]: (living(skc6, V_671) | ~human_person(skc5, V_671)))). % 8.68/2.92 tff(c_1250, plain, (![V_669]: (organism(skc6, V_669) | ~human_person(skc5, V_669)))). % 8.68/2.92 tff(c_933, plain, (![V_547, V_20, U_19]: (organism(V_547, V_20) | ~accessible_world(U_19, V_547) | ~human_person(U_19, V_20)))). % 8.68/2.92 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.68/2.92 tff(c_1236, plain, (![V_467]: (~abstraction(skc5, skf2(V_467))))). % 8.68/2.92 tff(c_1211, plain, (![V_16]: (~abstraction(skc5, V_16) | ~event(skc6, V_16)))). % 8.68/2.92 tff(c_1204, plain, (![V_654]: (~entity(skc6, V_654) | ~abstraction(skc5, V_654)))). % 8.68/2.92 tff(c_1203, plain, (![V_654]: (~eventuality(skc6, V_654) | ~abstraction(skc5, V_654)))). % 8.68/2.92 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.68/2.92 tff(c_1192, plain, (![V_652]: (general(skc6, V_652) | ~abstraction(skc5, V_652)))). % 8.68/2.92 tff(c_874, plain, (![V_533, V_50, U_49]: (general(V_533, V_50) | ~accessible_world(U_49, V_533) | ~abstraction(U_49, V_50)))). % 8.68/2.92 tff(c_1184, plain, (![V_646]: (agent(V_646, skc7, skc9) | ~accessible_world(skc5, V_646)))). % 8.68/2.92 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.68/2.92 tff(c_1149, plain, (![V_638]: (theme(V_638, skc7, skc6) | ~accessible_world(skc5, V_638)))). % 8.68/2.92 tff(c_1172, plain, (![V_467]: (~entity(skc5, skf2(V_467))))). % 8.68/2.92 tff(c_1155, plain, (![V_16]: (~entity(skc5, V_16) | ~event(skc6, V_16)))). % 8.68/2.92 tff(c_1145, plain, (![V_637]: (~eventuality(skc6, V_637) | ~entity(skc5, V_637)))). % 8.68/2.92 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.68/2.92 tff(c_1137, plain, (![V_635]: (existent(skc6, V_635) | ~entity(skc5, V_635)))). % 8.68/2.92 tff(c_1113, plain, (![V_622, V_28, U_27]: (existent(V_622, V_28) | ~accessible_world(U_27, V_622) | ~entity(U_27, V_28)))). % 8.68/2.92 tff(c_1129, plain, (![V_629]: (of(V_629, skc8, skc9) | ~accessible_world(skc5, V_629)))). % 8.68/2.92 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.68/2.92 tff(c_1117, plain, (![V_625]: (proposition(V_625, skc6) | ~accessible_world(skc5, V_625)))). % 8.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 tff(c_1094, plain, (![V_612]: (think_believe_consider(V_612, skc7) | ~accessible_world(skc5, V_612)))). % 8.68/2.92 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.68/2.92 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.68/2.92 tff(c_1074, plain, (![V_603, V_193]: (present(V_603, skf2(V_193)) | ~accessible_world(skc6, V_603)))). % 8.68/2.92 tff(c_1075, plain, (![V_603]: (present(V_603, skc7) | ~accessible_world(skc5, V_603)))). % 8.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 tff(c_1067, plain, (~abstraction(skc6, skc7))). % 8.68/2.92 tff(c_1057, plain, (![V_594]: (~abstraction(V_594, skc7) | ~accessible_world(skc5, V_594)))). % 8.68/2.92 tff(c_1056, plain, (![V_594]: (~entity(V_594, skc7) | ~accessible_world(skc5, V_594)))). % 8.68/2.92 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.68/2.92 tff(c_1045, plain, (![V_591]: (event(V_591, skc7) | ~accessible_world(skc5, V_591)))). % 8.68/2.92 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.68/2.92 tff(c_1027, plain, (![V_587]: (vincent_forename(V_587, skc8) | ~accessible_world(skc5, V_587)))). % 8.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 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.68/2.92 tff(c_963, plain, (![V_137]: (abstraction(V_137, skc6) | ~accessible_world(skc6, V_137)))). % 8.68/2.92 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.68/2.92 tff(c_952, plain, (![V_552]: (abstraction(V_552, skc8) | ~accessible_world(skc6, V_552)))). % 8.68/2.92 tff(c_944, plain, (![U_15]: (~accessible_world(skc5, U_15) | ~event(U_15, skc9)))). % 8.68/2.92 tff(c_960, plain, (abstraction(skc6, skc6))). % 8.68/2.92 tff(c_954, plain, (![V_552]: (abstraction(V_552, skc6) | ~accessible_world(skc5, V_552)))). % 8.68/2.92 tff(c_915, plain, (![V_544]: (animate(V_544, skc9) | ~accessible_world(skc5, V_544)))). % 8.68/2.92 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.68/2.92 tff(c_923, plain, (![V_545]: (~eventuality(V_545, skc9) | ~accessible_world(skc5, V_545)))). % 8.68/2.92 tff(c_913, plain, (![V_544]: (entity(V_544, skc9) | ~accessible_world(skc5, V_544)))). % 8.68/2.92 tff(c_929, plain, (abstraction(skc6, skc8))). % 8.68/2.92 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.68/2.92 tff(c_902, plain, (![V_543]: (abstraction(V_543, skc8) | ~accessible_world(skc5, V_543)))). % 8.68/2.92 tff(c_894, plain, (![V_542]: (male(V_542, skc9) | ~accessible_world(skc5, V_542)))). % 8.68/2.92 tff(c_893, plain, (![V_542]: (human_person(V_542, skc9) | ~accessible_world(skc5, V_542)))). % 8.68/2.93 tff(c_882, plain, (![V_539]: (forename(V_539, skc8) | ~accessible_world(skc5, V_539)))). % 8.68/2.93 tff(c_878, plain, (![V_536]: (man(V_536, skc9) | ~accessible_world(skc5, V_536)))). % 8.68/2.93 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.68/2.93 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.68/2.93 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.68/2.93 tff(c_864, plain, (![V_524, V_525]: (~abstraction(V_524, skf2(V_525)) | ~accessible_world(skc6, V_524)))). % 8.68/2.93 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.68/2.93 tff(c_863, plain, (![V_524, V_525]: (~entity(V_524, skf2(V_525)) | ~accessible_world(skc6, V_524)))). % 8.68/2.93 tff(c_855, plain, (![V_522, V_523]: (event(V_522, skf2(V_523)) | ~accessible_world(skc6, V_522)))). % 8.68/2.93 tff(c_842, plain, (![V_518, V_191]: (smoke(V_518, skf2(V_191)) | ~accessible_world(skc6, V_518)))). % 8.68/2.93 tff(c_847, plain, (~abstraction(skc6, skc9))). % 8.68/2.93 tff(c_824, plain, (![V_511]: (~abstraction(V_511, skc9) | ~accessible_world(skc5, V_511)))). % 8.68/2.93 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.68/2.93 tff(c_836, plain, (![V_467]: (~entity(skc6, skf2(V_467))))). % 8.68/2.93 tff(c_837, plain, (~entity(skc5, skc7))). % 8.68/2.93 tff(c_806, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~event(U_15, V_16)))). % 8.68/2.93 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.68/2.93 tff(c_784, plain, (![V_496]: (human(V_496, skc9) | ~accessible_world(skc5, V_496)))). % 8.68/2.93 tff(c_814, plain, (![V_467]: (~abstraction(skc6, skf2(V_467))))). % 8.68/2.93 tff(c_815, plain, (~abstraction(skc5, skc7))). % 8.68/2.93 tff(c_794, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~event(U_15, V_16)))). % 8.68/2.93 tff(c_294, plain, (![U_27, V_28]: (~eventuality(U_27, V_28) | ~entity(U_27, V_28)))). % 8.68/2.93 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.68/2.93 tff(c_773, plain, (![U_49, V_50]: (~eventuality(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.68/2.93 tff(c_305, plain, (![U_49, V_50]: (~entity(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.68/2.93 tff(c_780, plain, (abstraction(skc5, skc8))). % 8.68/2.93 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.68/2.93 tff(c_749, plain, (![U_475, V_476]: (abstraction(U_475, V_476) | ~forename(U_475, V_476)))). % 8.68/2.93 tff(c_197, plain, (![U_234, V_235]: (singleton(U_234, V_235) | ~abstraction(U_234, V_235)))). % 8.68/2.93 tff(c_229, plain, (![U_254, V_255]: (living(U_254, V_255) | ~human_person(U_254, V_255)))). % 8.68/2.93 tff(c_272, plain, (![U_270, V_271]: (~general(U_270, V_271) | ~eventuality(U_270, V_271)))). % 8.68/2.93 tff(c_230, plain, (![U_254, V_255]: (impartial(U_254, V_255) | ~human_person(U_254, V_255)))). % 8.68/2.93 tff(c_174, plain, (![U_196]: (agent(skc6, skf2(U_196), U_196) | ~man(skc6, U_196)))). % 8.68/2.93 tff(c_217, plain, (![U_250, V_251]: (singleton(U_250, V_251) | ~entity(U_250, V_251)))). % 8.68/2.93 tff(c_765, plain, (entity(skc5, skc9))). % 8.68/2.93 tff(c_231, plain, (![U_254, V_255]: (entity(U_254, V_255) | ~human_person(U_254, V_255)))). % 8.68/2.93 tff(c_267, plain, (![U_47, V_48]: (~human(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.68/2.93 tff(c_754, plain, (abstraction(skc5, skc6))). % 8.68/2.93 tff(c_211, plain, (![U_246, V_247]: (abstraction(U_246, V_247) | ~proposition(U_246, V_247)))). % 8.68/2.93 tff(c_205, plain, (![U_39, V_40]: (relation(U_39, V_40) | ~forename(U_39, V_40)))). % 8.68/2.93 tff(c_743, plain, (~event(skc5, skc9))). % 8.68/2.93 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.68/2.93 tff(c_739, plain, (~eventuality(skc5, skc9))). % 8.68/2.93 tff(c_289, plain, (![U_280, V_281]: (~male(U_280, V_281) | ~eventuality(U_280, V_281)))). % 8.68/2.93 tff(c_733, plain, (![V_467]: (event(skc6, skf2(V_467))))). % 8.68/2.93 tff(c_728, plain, (![V_191]: (smoke(skc6, skf2(V_191))))). % 8.68/2.93 tff(c_445, plain, (![V_193]: (present(skc6, skf2(V_193))))). % 8.68/2.93 tff(c_238, plain, (![U_260, V_261]: (~general(U_260, V_261) | ~entity(U_260, V_261)))). % 8.68/2.93 tff(c_300, plain, (~abstraction(skc5, skc9))). % 8.68/2.93 tff(c_249, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~abstraction(U_51, V_52)))). % 8.68/2.93 tff(c_278, plain, (![U_274, V_275]: (singleton(U_274, V_275) | ~eventuality(U_274, V_275)))). % 8.68/2.93 tff(c_284, plain, (![U_9, V_10]: (~existent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.68/2.93 tff(c_12, plain, (![U_11, V_12]: (unisex(U_11, V_12) | ~eventuality(U_11, V_12)))). % 8.68/2.93 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 8.68/2.93 tff(c_2, plain, (![U_1, V_2]: (eventuality(U_1, V_2) | ~state(U_1, V_2)))). % 8.68/2.93 tff(c_4, plain, (![U_3, V_4]: (thing(U_3, V_4) | ~eventuality(U_3, V_4)))). % 8.68/2.93 tff(c_10, plain, (![U_9, V_10]: (nonexistent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.68/2.93 tff(c_8, plain, (![U_7, V_8]: (specific(U_7, V_8) | ~eventuality(U_7, V_8)))). % 8.68/2.93 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 8.68/2.93 tff(c_262, plain, (animate(skc5, skc9))). % 8.68/2.93 tff(c_261, plain, (human(skc5, skc9))). % 8.68/2.93 tff(c_254, plain, (human_person(skc5, skc9))). % 8.68/2.93 tff(c_18, plain, (![U_17, V_18]: (human_person(U_17, V_18) | ~man(U_17, V_18)))). % 8.68/2.93 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 8.68/2.93 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~vincent_forename(U_59, V_60)))). % 8.68/2.93 tff(c_26, plain, (![U_25, V_26]: (specific(U_25, V_26) | ~entity(U_25, V_26)))). % 8.68/2.93 tff(c_14, plain, (![U_13, V_14]: (event(U_13, V_14) | ~state(U_13, V_14)))). % 8.68/2.93 tff(c_16, plain, (![U_15, V_16]: (eventuality(U_15, V_16) | ~event(U_15, V_16)))). % 8.68/2.93 tff(c_20, plain, (![U_19, V_20]: (organism(U_19, V_20) | ~human_person(U_19, V_20)))). % 8.68/2.93 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 8.68/2.93 tff(c_24, plain, (![U_23, V_24]: (thing(U_23, V_24) | ~entity(U_23, V_24)))). % 8.68/2.93 tff(c_28, plain, (![U_27, V_28]: (existent(U_27, V_28) | ~entity(U_27, V_28)))). % 8.68/2.93 tff(c_58, plain, (![U_57, V_58]: (relation(U_57, V_58) | ~proposition(U_57, V_58)))). % 8.68/2.93 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~jules_forename(U_53, V_54)))). % 8.68/2.93 tff(c_42, plain, (![U_41, V_42]: (relation(U_41, V_42) | ~relname(U_41, V_42)))). % 8.68/2.93 tff(c_56, plain, (![U_55, V_56]: (event(U_55, V_56) | ~smoke(U_55, V_56)))). % 8.68/2.93 tff(c_40, plain, (![U_39, V_40]: (relname(U_39, V_40) | ~forename(U_39, V_40)))). % 8.68/2.93 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))). % 8.68/2.93 tff(c_46, plain, (![U_45, V_46]: (thing(U_45, V_46) | ~abstraction(U_45, V_46)))). % 8.68/2.93 tff(c_48, plain, (![U_47, V_48]: (nonhuman(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.68/2.93 tff(c_50, plain, (![U_49, V_50]: (general(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.68/2.93 tff(c_190, plain, (male(skc5, skc9))). % 8.68/2.93 tff(c_38, plain, (![U_37, V_38]: (male(U_37, V_38) | ~man(U_37, V_38)))). % 8.68/2.93 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~abstraction(U_51, V_52)))). % 8.68/2.93 tff(c_34, plain, (![U_33, V_34]: (human(U_33, V_34) | ~human_person(U_33, V_34)))). % 8.68/2.93 tff(c_32, plain, (![U_31, V_32]: (living(U_31, V_32) | ~organism(U_31, V_32)))). % 8.68/2.93 tff(c_36, plain, (![U_35, V_36]: (animate(U_35, V_36) | ~human_person(U_35, V_36)))). % 8.68/2.93 tff(c_30, plain, (![U_29, V_30]: (impartial(U_29, V_30) | ~organism(U_29, V_30)))). % 8.68/2.93 tff(c_6, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~thing(U_5, V_6)))). % 8.68/2.93 tff(c_22, plain, (![U_21, V_22]: (entity(U_21, V_22) | ~organism(U_21, V_22)))). % 8.68/2.93 tff(c_166, plain, (theme(skc5, skc7, skc6))). % 8.68/2.93 tff(c_162, plain, (of(skc5, skc8, skc9))). % 8.68/2.93 tff(c_164, plain, (agent(skc5, skc7, skc9))). % 8.68/2.93 tff(c_154, plain, (present(skc5, skc7))). % 8.68/2.93 tff(c_152, plain, (event(skc5, skc7))). % 8.68/2.93 tff(c_150, plain, (vincent_forename(skc5, skc8))). % 8.68/2.93 tff(c_156, plain, (think_believe_consider(skc5, skc7))). % 8.68/2.93 tff(c_148, plain, (forename(skc5, skc8))). % 8.68/2.93 tff(c_146, plain, (man(skc5, skc9))). % 8.68/2.93 tff(c_158, plain, (accessible_world(skc5, skc6))). % 8.68/2.93 tff(c_160, plain, (proposition(skc5, skc6))). % 8.68/2.93 tff(c_144, plain, (actual_world(skc5))). % 8.68/2.93 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.68/2.93 %------------------------------------------------------------------------------