%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP227-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 : n009.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.21s 2.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP227-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/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 : n009.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:32:11 EDT 2025 % 0.13/0.34 % CPUTime : % 8.21/2.80 % 8.21/2.80 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.21/2.80 % 8.21/2.80 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.21/2.81 %$ 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.21/2.81 % 8.21/2.81 %Foreground sorts: % 8.21/2.81 % 8.21/2.81 % 8.21/2.81 %Background operators: % 8.21/2.81 % 8.21/2.81 % 8.21/2.81 %Foreground operators: % 8.21/2.81 tff(relation, type, relation: ($i * $i) > $o). % 8.21/2.81 tff(skf4, type, skf4: $i > $i). % 8.21/2.81 tff(forename, type, forename: ($i * $i) > $o). % 8.21/2.81 tff(be, type, be: ($i * $i * $i * $i) > $o). % 8.21/2.81 tff(skc7, type, skc7: $i). % 8.21/2.81 tff(theme, type, theme: ($i * $i * $i) > $o). % 8.21/2.81 tff(living, type, living: ($i * $i) > $o). % 8.21/2.81 tff(human_person, type, human_person: ($i * $i) > $o). % 8.21/2.81 tff(present, type, present: ($i * $i) > $o). % 8.21/2.81 tff(entity, type, entity: ($i * $i) > $o). % 8.21/2.81 tff(skc9, type, skc9: $i). % 8.21/2.81 tff(eventuality, type, eventuality: ($i * $i) > $o). % 8.21/2.81 tff(existent, type, existent: ($i * $i) > $o). % 8.21/2.81 tff(abstraction, type, abstraction: ($i * $i) > $o). % 8.21/2.81 tff(skc8, type, skc8: $i). % 8.21/2.81 tff(proposition, type, proposition: ($i * $i) > $o). % 8.21/2.81 tff(relname, type, relname: ($i * $i) > $o). % 8.21/2.81 tff(singleton, type, singleton: ($i * $i) > $o). % 8.21/2.81 tff(male, type, male: ($i * $i) > $o). % 8.21/2.81 tff(organism, type, organism: ($i * $i) > $o). % 8.21/2.81 tff(animate, type, animate: ($i * $i) > $o). % 8.21/2.81 tff(of, type, of: ($i * $i * $i) > $o). % 8.21/2.81 tff(actual_world, type, actual_world: $i > $o). % 8.21/2.81 tff(agent, type, agent: ($i * $i * $i) > $o). % 8.21/2.81 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 8.21/2.81 tff(general, type, general: ($i * $i) > $o). % 8.21/2.81 tff(smoke, type, smoke: ($i * $i) > $o). % 8.21/2.81 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 8.21/2.81 tff(event, type, event: ($i * $i) > $o). % 8.21/2.81 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 8.21/2.81 tff(state, type, state: ($i * $i) > $o). % 8.21/2.81 tff(thing, type, thing: ($i * $i) > $o). % 8.21/2.81 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 8.21/2.81 tff(human, type, human: ($i * $i) > $o). % 8.21/2.81 tff(skf2, type, skf2: $i > $i). % 8.21/2.81 tff(man, type, man: ($i * $i) > $o). % 8.21/2.81 tff(skc5, type, skc5: $i). % 8.21/2.81 tff(unisex, type, unisex: ($i * $i) > $o). % 8.21/2.81 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 8.21/2.81 tff(skc6, type, skc6: $i). % 8.21/2.81 tff(impartial, type, impartial: ($i * $i) > $o). % 8.21/2.81 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 8.21/2.81 tff(specific, type, specific: ($i * $i) > $o). % 8.21/2.81 % 8.21/2.81 %Saturated clause set: % 8.21/2.81 tff(c_1349, plain, (![Z_698, X2_702, V_701, X1_699, W_705, Y_700, V_631, X_706]: (~actual_world(V_631) | ~man(V_631, skc9) | ~be(V_631, X1_699, skc9, X2_702) | ~forename(V_631, skc8) | ~jules_forename(V_631, skc8) | ~man(V_631, X2_702) | ~state(V_631, X1_699) | ~of(V_631, Y_700, Z_698) | ~man(V_631, Z_698) | ~agent(V_631, X_706, Z_698) | ~forename(V_631, Y_700) | ~vincent_forename(V_631, Y_700) | ~theme(V_631, X_706, V_701) | ~event(V_631, X_706) | ~present(V_631, X_706) | ~think_believe_consider(V_631, X_706) | ~event(V_701, W_705) | ~agent(V_701, W_705, skf4(V_701)) | ~present(V_701, W_705) | ~smoke(V_701, W_705) | ~accessible_world(V_631, V_701) | ~proposition(V_631, V_701) | ~accessible_world(skc5, V_631)))). % 8.21/2.81 tff(c_2624, plain, (![V_1033, V_640]: (skc6=V_1033 | ~think_believe_consider(V_640, skc7) | ~think_believe_consider(V_640, skf2(skc9)) | ~theme(V_640, skf2(skc9), V_1033) | ~proposition(V_640, skc6) | ~proposition(V_640, V_1033) | ~accessible_world(skc6, V_640) | ~accessible_world(skc5, V_640)))). % 8.21/2.81 tff(c_2611, plain, (![W_1019, V_1017, V_648]: (W_1019=V_1017 | ~theme(V_648, skc7, W_1019) | ~think_believe_consider(V_648, skc7) | ~think_believe_consider(V_648, skf2(skc9)) | ~theme(V_648, skf2(skc9), V_1017) | ~proposition(V_648, W_1019) | ~proposition(V_648, V_1017) | ~accessible_world(skc6, V_648) | ~accessible_world(skc5, V_648)))). % 8.21/2.81 tff(c_2608, plain, (![W_1019, V_1017, V_648, U_196]: (W_1019=V_1017 | ~theme(V_648, skf2(U_196), W_1019) | ~think_believe_consider(V_648, skf2(U_196)) | ~theme(V_648, skf2(U_196), V_1017) | ~proposition(V_648, W_1019) | ~proposition(V_648, V_1017) | ~accessible_world(skc6, V_648) | ~man(skc6, U_196)))). % 8.21/2.81 tff(c_2616, plain, (~accessible_world(skc6, skc5))). % 8.21/2.82 tff(c_1327, plain, (![V_687, W_692, X1_690, Y_689, X_686, Z_684, V_631]: (man(V_687, skf4(V_687)) | ~actual_world(V_631) | ~man(V_631, skc9) | ~be(V_631, Z_684, skc9, X1_690) | ~forename(V_631, skc8) | ~jules_forename(V_631, skc8) | ~man(V_631, X1_690) | ~state(V_631, Z_684) | ~of(V_631, X_686, Y_689) | ~man(V_631, Y_689) | ~agent(V_631, W_692, Y_689) | ~forename(V_631, X_686) | ~vincent_forename(V_631, X_686) | ~theme(V_631, W_692, V_687) | ~event(V_631, W_692) | ~present(V_631, W_692) | ~think_believe_consider(V_631, W_692) | ~accessible_world(V_631, V_687) | ~proposition(V_631, V_687) | ~accessible_world(skc5, V_631)))). % 8.21/2.82 tff(c_1673, plain, (![U_774, V_189, Y_188, W_184, V_773]: (W_184=V_189 | ~agent(V_773, Y_188, U_774) | ~theme(V_773, Y_188, W_184) | ~think_believe_consider(V_773, Y_188) | ~think_believe_consider(V_773, skf2(U_774)) | ~theme(V_773, skf2(U_774), V_189) | ~proposition(V_773, W_184) | ~proposition(V_773, V_189) | ~accessible_world(skc6, V_773) | ~man(skc6, U_774)))). % 8.21/2.82 tff(c_2583, plain, (![V_1011, V_640]: (skc6=V_1011 | ~agent(V_640, skc7, skc9) | ~think_believe_consider(V_640, skc7) | ~theme(V_640, skc7, V_1011) | ~proposition(V_640, skc6) | ~proposition(V_640, V_1011) | ~accessible_world(skc5, V_640)))). % 8.21/2.82 tff(c_1278, plain, (![W_679, V_677, V_648, Y_678]: (W_679=V_677 | ~agent(V_648, Y_678, skc9) | ~theme(V_648, Y_678, W_679) | ~think_believe_consider(V_648, Y_678) | ~think_believe_consider(V_648, skc7) | ~theme(V_648, skc7, V_677) | ~proposition(V_648, W_679) | ~proposition(V_648, V_677) | ~accessible_world(skc5, V_648)))). % 8.21/2.82 tff(c_2545, plain, (![V_119, V_996]: (human(V_119, skc9) | ~accessible_world(V_996, V_119) | ~accessible_world(skc6, V_996)))). % 8.21/2.82 tff(c_2529, plain, (![V_122, V_995]: (animate(V_122, skc9) | ~accessible_world(V_995, V_122) | ~accessible_world(skc6, V_995)))). % 8.21/2.82 tff(c_2481, plain, (![V_125, V_992]: (male(V_125, skc9) | ~accessible_world(V_992, V_125) | ~accessible_world(skc6, V_992)))). % 8.21/2.82 tff(c_2506, plain, (![V_101, V_993]: (human_person(V_101, skc9) | ~accessible_world(V_993, V_101) | ~accessible_world(skc6, V_993)))). % 8.21/2.82 tff(c_2453, plain, (![V_155, V_991]: (think_believe_consider(V_155, skc7) | ~accessible_world(V_991, V_155) | ~accessible_world(skc6, V_991)))). % 8.21/2.82 tff(c_2446, plain, (![V_98, V_990]: (man(V_98, skc9) | ~accessible_world(V_990, V_98) | ~accessible_world(skc6, V_990)))). % 8.21/2.82 tff(c_2525, plain, (![U_15]: (~accessible_world(skc6, U_15) | ~event(U_15, skc9)))). % 8.21/2.82 tff(c_2432, plain, (![V_119]: (human(V_119, skc9) | ~accessible_world(skc6, V_119)))). % 8.21/2.82 tff(c_2509, plain, (![V_993]: (animate(V_993, skc9) | ~accessible_world(skc6, V_993)))). % 8.21/2.82 tff(c_2482, plain, (![V_992]: (~eventuality(V_992, skc9) | ~accessible_world(skc6, V_992)))). % 8.21/2.82 tff(c_2447, plain, (![V_990]: (human_person(V_990, skc9) | ~accessible_world(skc6, V_990)))). % 8.21/2.82 tff(c_2448, plain, (![V_990]: (male(V_990, skc9) | ~accessible_world(skc6, V_990)))). % 8.21/2.82 tff(c_2363, plain, (![V_155]: (think_believe_consider(V_155, skc7) | ~accessible_world(skc6, V_155)))). % 8.21/2.82 tff(c_2449, plain, (~think_believe_consider(skc6, skf2(skc9)))). % 8.21/2.82 tff(c_2348, plain, (![V_98]: (man(V_98, skc9) | ~accessible_world(skc6, V_98)))). % 8.21/2.82 tff(c_2418, plain, (~event(skc6, skc9))). % 8.21/2.82 tff(c_2406, plain, (animate(skc6, skc9))). % 8.21/2.82 tff(c_2405, plain, (human(skc6, skc9))). % 8.21/2.82 tff(c_2389, plain, (~eventuality(skc6, skc9))). % 8.21/2.82 tff(c_2349, plain, (human_person(skc6, skc9))). % 8.21/2.82 tff(c_2350, plain, (male(skc6, skc9))). % 8.21/2.82 tff(c_2360, plain, (think_believe_consider(skc6, skc7))). % 8.21/2.82 tff(c_2339, plain, (man(skc6, skc9))). % 8.21/2.82 tff(c_1851, plain, (![W_818, V_819, U_196]: (W_818=V_819 | ~theme(skc6, skf2(U_196), W_818) | ~think_believe_consider(skc6, skf2(U_196)) | ~theme(skc6, skf2(U_196), V_819) | ~proposition(skc6, W_818) | ~proposition(skc6, V_819) | ~man(skc6, U_196)))). % 8.21/2.82 tff(c_2058, plain, (![V_116, V_865, V_864]: (living(V_116, V_865) | ~accessible_world(V_864, V_116) | ~accessible_world(skc6, V_864) | ~human_person(skc5, V_865)))). % 8.21/2.82 tff(c_2096, plain, (![V_83, V_877, V_876]: (singleton(V_83, V_877) | ~accessible_world(V_876, V_83) | ~accessible_world(skc6, V_876) | ~entity(skc5, V_877)))). % 8.21/2.82 tff(c_2100, plain, (![V_113, V_879, V_878]: (impartial(V_113, V_879) | ~accessible_world(V_878, V_113) | ~accessible_world(skc6, V_878) | ~human_person(skc5, V_879)))). % 8.21/2.82 tff(c_2037, plain, (![V_83, V_859, V_858]: (singleton(V_83, V_859) | ~accessible_world(V_858, V_83) | ~accessible_world(skc6, V_858) | ~eventuality(skc5, V_859)))). % 8.21/2.82 tff(c_2041, plain, (![V_83, V_861, V_860]: (singleton(V_83, V_861) | ~accessible_world(V_860, V_83) | ~accessible_world(skc6, V_860) | ~abstraction(skc5, V_861)))). % 8.21/2.82 tff(c_1243, plain, (![W_666, V_631]: (skc8=W_666 | ~entity(V_631, skc9) | ~forename(V_631, W_666) | ~of(V_631, W_666, skc9) | ~forename(V_631, skc8) | ~accessible_world(skc5, V_631)))). % 8.21/2.82 tff(c_2140, plain, (![V_134, V_888, V_887]: (relation(V_134, V_888) | ~accessible_world(V_887, V_134) | ~accessible_world(skc6, V_887) | ~forename(skc5, V_888)))). % 8.21/2.82 tff(c_1887, plain, (![V_110, V_829, V_828]: (existent(V_110, V_829) | ~accessible_world(V_828, V_110) | ~accessible_world(skc6, V_828) | ~entity(skc5, V_829)))). % 8.21/2.82 tff(c_1954, plain, (![V_140, V_843, V_842]: (nonhuman(V_140, V_843) | ~accessible_world(V_842, V_140) | ~accessible_world(skc6, V_842) | ~abstraction(skc5, V_843)))). % 8.21/2.82 tff(c_1946, plain, (![V_89, V_841, V_840]: (nonexistent(V_89, V_841) | ~accessible_world(V_840, V_89) | ~accessible_world(skc6, V_840) | ~eventuality(skc5, V_841)))). % 8.21/2.82 tff(c_1937, plain, (![V_80, V_839, V_838]: (thing(V_80, V_839) | ~accessible_world(V_838, V_80) | ~accessible_world(skc6, V_838) | ~abstraction(skc5, V_839)))). % 8.21/2.82 tff(c_1874, plain, (![V_134, V_827, V_826]: (relation(V_134, V_827) | ~accessible_world(V_826, V_134) | ~accessible_world(skc6, V_826) | ~proposition(skc5, V_827)))). % 8.21/2.82 tff(c_1908, plain, (![V_143, V_831, V_830]: (general(V_143, V_831) | ~accessible_world(V_830, V_143) | ~accessible_world(skc6, V_830) | ~abstraction(skc5, V_831)))). % 8.21/2.82 tff(c_1836, plain, (![V_131, V_817, V_816]: (relname(V_131, V_817) | ~accessible_world(V_816, V_131) | ~accessible_world(skc6, V_816) | ~forename(skc5, V_817)))). % 8.21/2.82 tff(c_1824, plain, (![V_80, V_813, V_812]: (thing(V_80, V_813) | ~accessible_world(V_812, V_80) | ~accessible_world(skc6, V_812) | ~eventuality(skc5, V_813)))). % 8.21/2.82 tff(c_1674, plain, (![V_168, U_774, V_773]: (agent(V_168, skf2(U_774), U_774) | ~accessible_world(V_773, V_168) | ~accessible_world(skc6, V_773) | ~man(skc6, U_774)))). % 8.21/2.82 tff(c_1962, plain, (![V_92, V_845, V_844]: (unisex(V_92, V_845) | ~accessible_world(V_844, V_92) | ~accessible_world(skc6, V_844) | ~abstraction(skc5, V_845)))). % 8.21/2.82 tff(c_1917, plain, (![V_80, V_833, V_832]: (thing(V_80, V_833) | ~accessible_world(V_832, V_80) | ~accessible_world(skc6, V_832) | ~entity(skc5, V_833)))). % 8.21/2.82 tff(c_1814, plain, (![V_104, V_811, V_810]: (organism(V_104, V_811) | ~accessible_world(V_810, V_104) | ~accessible_world(skc6, V_810) | ~human_person(skc5, V_811)))). % 8.21/2.82 tff(c_1783, plain, (![V_77, V_808, V_807]: (eventuality(V_77, V_808) | ~accessible_world(V_807, V_77) | ~accessible_world(skc6, V_807) | ~event(skc5, V_808)))). % 8.21/2.82 tff(c_1858, plain, (![V_86, V_823, V_822]: (specific(V_86, V_823) | ~accessible_world(V_822, V_86) | ~accessible_world(skc6, V_822) | ~eventuality(skc5, V_823)))). % 8.21/2.83 tff(c_1929, plain, (![V_92, V_837, V_836]: (unisex(V_92, V_837) | ~accessible_world(V_836, V_92) | ~accessible_world(skc6, V_836) | ~eventuality(skc5, V_837)))). % 8.21/2.83 tff(c_1866, plain, (![V_86, V_825, V_824]: (specific(V_86, V_825) | ~accessible_world(V_824, V_86) | ~accessible_world(skc6, V_824) | ~entity(skc5, V_825)))). % 8.21/2.83 tff(c_1043, plain, (![V_593, V_525, V_524]: (event(V_593, skf2(V_525)) | ~accessible_world(V_524, V_593) | ~accessible_world(skc6, V_524)))). % 8.21/2.83 tff(c_1188, plain, (![V_168, V_652]: (agent(V_168, skc7, skc9) | ~accessible_world(V_652, V_168) | ~accessible_world(skc5, V_652)))). % 8.21/2.83 tff(c_854, plain, (![V_149, V_525, V_524]: (smoke(V_149, skf2(V_525)) | ~accessible_world(V_524, V_149) | ~accessible_world(skc6, V_524)))). % 8.21/2.83 tff(c_1320, plain, (![V_107, V_683]: (entity(V_107, skc9) | ~accessible_world(V_683, V_107) | ~accessible_world(skc6, V_683)))). % 8.21/2.83 tff(c_1985, plain, (![U_27, V_28]: (~accessible_world(skc6, U_27) | ~eventuality(skc5, V_28) | ~entity(U_27, V_28)))). % 8.21/2.83 tff(c_1998, plain, (![U_49, V_50]: (~accessible_world(skc6, U_49) | ~entity(skc5, V_50) | ~abstraction(U_49, V_50)))). % 8.21/2.83 tff(c_2011, plain, (![U_15, V_16]: (~accessible_world(skc6, U_15) | ~abstraction(skc5, V_16) | ~event(U_15, V_16)))). % 8.21/2.83 tff(c_2024, plain, (![U_49, V_50]: (~accessible_world(skc6, U_49) | ~eventuality(skc5, V_50) | ~abstraction(U_49, V_50)))). % 8.21/2.83 tff(c_2113, plain, (![U_15, V_16]: (~accessible_world(skc6, U_15) | ~entity(skc5, V_16) | ~event(U_15, V_16)))). % 8.21/2.83 tff(c_2141, plain, (![V_887, V_888]: (abstraction(V_887, V_888) | ~accessible_world(skc6, V_887) | ~forename(skc5, V_888)))). % 8.21/2.83 tff(c_1875, plain, (![V_826, V_827]: (abstraction(V_826, V_827) | ~accessible_world(skc6, V_826) | ~proposition(skc5, V_827)))). % 8.21/2.83 tff(c_1133, plain, (![V_164, V_635]: (of(V_164, skc8, skc9) | ~accessible_world(V_635, V_164) | ~accessible_world(skc5, V_635)))). % 8.21/2.83 tff(c_1930, plain, (![V_836, V_837]: (~male(V_836, V_837) | ~accessible_world(skc6, V_836) | ~eventuality(skc5, V_837)))). % 8.21/2.83 tff(c_1817, plain, (![V_810, V_811]: (entity(V_810, V_811) | ~accessible_world(skc6, V_810) | ~human_person(skc5, V_811)))). % 8.21/2.83 tff(c_1837, plain, (![V_816, V_817]: (relation(V_816, V_817) | ~accessible_world(skc6, V_816) | ~forename(skc5, V_817)))). % 8.21/2.83 tff(c_2128, plain, (~event(skc5, skc8))). % 8.21/2.83 tff(c_1090, plain, (![V_152, V_613, V_612]: (present(V_152, skf2(V_613)) | ~accessible_world(V_612, V_152) | ~accessible_world(skc6, V_612)))). % 8.21/2.83 tff(c_2127, plain, (~event(skc5, skc6))). % 8.21/2.83 tff(c_1785, plain, (![V_807, V_808]: (~abstraction(V_807, V_808) | ~accessible_world(skc6, V_807) | ~event(skc5, V_808)))). % 8.21/2.83 tff(c_1888, plain, (![V_828, V_829]: (~eventuality(V_828, V_829) | ~accessible_world(skc6, V_828) | ~entity(skc5, V_829)))). % 8.21/2.83 tff(c_1816, plain, (![V_810, V_811]: (impartial(V_810, V_811) | ~accessible_world(skc6, V_810) | ~human_person(skc5, V_811)))). % 8.21/2.83 tff(c_1393, plain, (![V_83, V_714]: (singleton(V_83, V_714) | ~accessible_world(skc6, V_83) | ~entity(skc5, V_714)))). % 8.21/2.83 tff(c_1910, plain, (![V_830, V_831]: (~entity(V_830, V_831) | ~accessible_world(skc6, V_830) | ~abstraction(skc5, V_831)))). % 8.21/2.83 tff(c_971, plain, (![V_561, V_546]: (animate(V_561, skc9) | ~accessible_world(V_546, V_561) | ~accessible_world(skc5, V_546)))). % 8.21/2.83 tff(c_1177, plain, (![V_172, V_647]: (theme(V_172, skc7, skc6) | ~accessible_world(V_647, V_172) | ~accessible_world(skc5, V_647)))). % 8.21/2.83 tff(c_1081, plain, (![V_608, V_546]: (entity(V_608, skc9) | ~accessible_world(V_546, V_608) | ~accessible_world(skc5, V_546)))). % 8.21/2.83 tff(c_823, plain, (![V_119, V_513]: (human(V_119, skc9) | ~accessible_world(V_513, V_119) | ~accessible_world(skc5, V_513)))). % 8.21/2.83 tff(c_1270, plain, (![V_116, V_674]: (living(V_116, V_674) | ~accessible_world(skc6, V_116) | ~human_person(skc5, V_674)))). % 8.21/2.83 tff(c_1784, plain, (![V_807, V_808]: (~entity(V_807, V_808) | ~accessible_world(skc6, V_807) | ~event(skc5, V_808)))). % 8.21/2.83 tff(c_1938, plain, (![V_838, V_839]: (singleton(V_838, V_839) | ~accessible_world(skc6, V_838) | ~abstraction(skc5, V_839)))). % 8.21/2.83 tff(c_1642, plain, (![V_83, V_763]: (singleton(V_83, V_763) | ~accessible_world(skc6, V_83) | ~eventuality(skc5, V_763)))). % 8.21/2.83 tff(c_1963, plain, (![V_844, V_845]: (~male(V_844, V_845) | ~accessible_world(skc6, V_844) | ~abstraction(skc5, V_845)))). % 8.21/2.83 tff(c_1859, plain, (![V_822, V_823]: (~general(V_822, V_823) | ~accessible_world(skc6, V_822) | ~eventuality(skc5, V_823)))). % 8.21/2.83 tff(c_1909, plain, (![V_830, V_831]: (~eventuality(V_830, V_831) | ~accessible_world(skc6, V_830) | ~abstraction(skc5, V_831)))). % 8.21/2.83 tff(c_1867, plain, (![V_824, V_825]: (~general(V_824, V_825) | ~accessible_world(skc6, V_824) | ~entity(skc5, V_825)))). % 8.21/2.83 tff(c_1947, plain, (![V_840, V_841]: (~existent(V_840, V_841) | ~accessible_world(skc6, V_840) | ~eventuality(skc5, V_841)))). % 8.21/2.83 tff(c_1955, plain, (![V_842, V_843]: (~human(V_842, V_843) | ~accessible_world(skc6, V_842) | ~abstraction(skc5, V_843)))). % 8.21/2.83 tff(c_1555, plain, (![V_92, V_750]: (unisex(V_92, V_750) | ~accessible_world(skc6, V_92) | ~abstraction(skc5, V_750)))). % 8.21/2.83 tff(c_1404, plain, (![V_140, V_718]: (nonhuman(V_140, V_718) | ~accessible_world(skc6, V_140) | ~abstraction(skc5, V_718)))). % 8.21/2.83 tff(c_1543, plain, (![V_89, V_746]: (nonexistent(V_89, V_746) | ~accessible_world(skc6, V_89) | ~eventuality(skc5, V_746)))). % 8.21/2.83 tff(c_1939, plain, (~jules_forename(skc5, skc8))). % 8.21/2.83 tff(c_1653, plain, (![V_80, V_767]: (thing(V_80, V_767) | ~accessible_world(skc6, V_80) | ~abstraction(skc5, V_767)))). % 8.21/2.83 tff(c_1456, plain, (![V_92, V_729]: (unisex(V_92, V_729) | ~accessible_world(skc6, V_92) | ~eventuality(skc5, V_729)))). % 8.21/2.83 tff(c_994, plain, (![V_574, V_544]: (human_person(V_574, skc9) | ~accessible_world(V_544, V_574) | ~accessible_world(skc5, V_544)))). % 8.21/2.83 tff(c_1388, plain, (![V_80, V_713]: (thing(V_80, V_713) | ~accessible_world(skc6, V_80) | ~entity(skc5, V_713)))). % 8.21/2.83 tff(c_1202, plain, (![V_143, V_656]: (general(V_143, V_656) | ~accessible_world(skc6, V_143) | ~abstraction(skc5, V_656)))). % 8.21/2.83 tff(c_1144, plain, (![V_110, V_639]: (existent(V_110, V_639) | ~accessible_world(skc6, V_110) | ~entity(skc5, V_639)))). % 8.21/2.83 tff(c_1519, plain, (![V_134, V_741]: (relation(V_134, V_741) | ~accessible_world(skc6, V_134) | ~proposition(skc5, V_741)))). % 8.21/2.83 tff(c_1342, plain, (![V_86, V_697]: (specific(V_86, V_697) | ~accessible_world(skc6, V_86) | ~entity(skc5, V_697)))). % 8.21/2.83 tff(c_1476, plain, (![V_86, V_734]: (specific(V_86, V_734) | ~accessible_world(skc6, V_86) | ~eventuality(skc5, V_734)))). % 8.21/2.83 tff(c_1279, plain, (![W_679, V_677, Y_678, U_196]: (W_679=V_677 | ~agent(skc6, Y_678, U_196) | ~theme(skc6, Y_678, W_679) | ~think_believe_consider(skc6, Y_678) | ~think_believe_consider(skc6, skf2(U_196)) | ~theme(skc6, skf2(U_196), V_677) | ~proposition(skc6, W_679) | ~proposition(skc6, V_677) | ~man(skc6, U_196)))). % 8.21/2.83 tff(c_1424, plain, (![V_131, V_723]: (relname(V_131, V_723) | ~accessible_world(skc6, V_131) | ~forename(skc5, V_723)))). % 8.21/2.83 tff(c_1015, plain, (![V_583, V_544]: (male(V_583, skc9) | ~accessible_world(V_544, V_583) | ~accessible_world(skc5, V_544)))). % 8.21/2.83 tff(c_1637, plain, (![V_80, V_762]: (thing(V_80, V_762) | ~accessible_world(skc6, V_80) | ~eventuality(skc5, V_762)))). % 8.21/2.83 tff(c_1263, plain, (![V_104, V_673]: (organism(V_104, V_673) | ~accessible_world(skc6, V_104) | ~human_person(skc5, V_673)))). % 8.21/2.83 tff(c_1733, plain, (![V_799]: (skc6=V_799 | ~theme(skc5, skc7, V_799) | ~proposition(skc5, V_799)))). % 8.21/2.83 tff(c_1624, plain, (![V_77, V_758]: (eventuality(V_77, V_758) | ~accessible_world(skc6, V_77) | ~event(skc5, V_758)))). % 8.21/2.83 tff(c_1055, plain, (![V_95, V_596]: (event(V_95, skc7) | ~accessible_world(V_596, V_95) | ~accessible_world(skc5, V_596)))). % 8.21/2.83 tff(c_892, plain, (![V_98, V_544]: (man(V_98, skc9) | ~accessible_world(V_544, V_98) | ~accessible_world(skc5, V_544)))). % 8.21/2.83 tff(c_1086, plain, (![V_152, V_611]: (present(V_152, skc7) | ~accessible_world(V_611, V_152) | ~accessible_world(skc5, V_611)))). % 8.21/2.83 tff(c_1282, plain, (![W_679, V_677, Y_678]: (W_679=V_677 | ~agent(skc5, Y_678, skc9) | ~theme(skc5, Y_678, W_679) | ~think_believe_consider(skc5, Y_678) | ~theme(skc5, skc7, V_677) | ~proposition(skc5, W_679) | ~proposition(skc5, V_677)))). % 8.21/2.83 tff(c_983, plain, (![V_568, V_40, U_39]: (relation(V_568, V_40) | ~accessible_world(U_39, V_568) | ~forename(U_39, V_40)))). % 8.21/2.84 tff(c_1009, plain, (![V_580, V_277, U_276]: (singleton(V_580, V_277) | ~accessible_world(U_276, V_580) | ~eventuality(U_276, V_277)))). % 8.21/2.84 tff(c_869, plain, (![V_530, V_257, U_256]: (living(V_530, V_257) | ~accessible_world(U_256, V_530) | ~human_person(U_256, V_257)))). % 8.21/2.84 tff(c_1034, plain, (![V_161, V_592]: (vincent_forename(V_161, skc8) | ~accessible_world(V_592, V_161) | ~accessible_world(skc5, V_592)))). % 8.21/2.84 tff(c_1099, plain, (![V_155, V_620]: (think_believe_consider(V_155, skc7) | ~accessible_world(V_620, V_155) | ~accessible_world(skc5, V_620)))). % 8.21/2.84 tff(c_1007, plain, (![V_580, V_237, U_236]: (singleton(V_580, V_237) | ~accessible_world(U_236, V_580) | ~abstraction(U_236, V_237)))). % 8.21/2.84 tff(c_1246, plain, (![W_666]: (skc8=W_666 | ~forename(skc5, W_666) | ~of(skc5, W_666, skc9)))). % 8.21/2.84 tff(c_1008, plain, (![V_580, V_253, U_252]: (singleton(V_580, V_253) | ~accessible_world(U_252, V_580) | ~entity(U_252, V_253)))). % 8.21/2.84 tff(c_999, plain, (![V_577, V_257, U_256]: (impartial(V_577, V_257) | ~accessible_world(U_256, V_577) | ~human_person(U_256, V_257)))). % 8.21/2.84 tff(c_1183, plain, (![V_648, U_196]: (agent(V_648, skf2(U_196), U_196) | ~accessible_world(skc6, V_648) | ~man(skc6, U_196)))). % 8.21/2.84 tff(c_901, plain, (![V_128, V_545]: (forename(V_128, skc8) | ~accessible_world(V_545, V_128) | ~accessible_world(skc5, V_545)))). % 8.21/2.84 tff(c_1663, plain, (~accessible_world(skc5, skc5))). % 8.21/2.84 tff(c_1124, plain, (![V_158, V_630]: (proposition(V_158, skc6) | ~accessible_world(V_630, V_158) | ~accessible_world(skc5, V_630)))). % 8.21/2.84 tff(c_1654, plain, (![V_767]: (singleton(skc6, V_767) | ~abstraction(skc5, V_767)))). % 8.21/2.84 tff(c_1646, plain, (![V_765]: (thing(skc6, V_765) | ~abstraction(skc5, V_765)))). % 8.21/2.84 tff(c_1109, plain, (![V_621, V_46, U_45]: (thing(V_621, V_46) | ~accessible_world(U_45, V_621) | ~abstraction(U_45, V_46)))). % 8.21/2.84 tff(c_1638, plain, (![V_762]: (singleton(skc6, V_762) | ~eventuality(skc5, V_762)))). % 8.21/2.84 tff(c_1630, plain, (![V_760]: (thing(skc6, V_760) | ~eventuality(skc5, V_760)))). % 8.21/2.84 tff(c_1107, plain, (![V_621, V_4, U_3]: (thing(V_621, V_4) | ~accessible_world(U_3, V_621) | ~eventuality(U_3, V_4)))). % 8.21/2.84 tff(c_1599, plain, (![V_756]: (eventuality(skc6, V_756) | ~event(skc5, V_756)))). % 8.21/2.84 tff(c_828, plain, (![V_514, V_16, U_15]: (eventuality(V_514, V_16) | ~accessible_world(U_15, V_514) | ~event(U_15, V_16)))). % 8.21/2.84 tff(c_1595, plain, (~entity(skc6, skc7))). % 8.21/2.84 tff(c_1580, plain, (![V_16]: (~entity(skc6, V_16) | ~event(skc5, V_16)))). % 8.21/2.84 tff(c_1566, plain, (![V_28]: (~eventuality(skc5, V_28) | ~entity(skc6, V_28)))). % 8.21/2.84 tff(c_1556, plain, (![V_750]: (~male(skc6, V_750) | ~abstraction(skc5, V_750)))). % 8.21/2.84 tff(c_1544, plain, (![V_746]: (~existent(skc6, V_746) | ~eventuality(skc5, V_746)))). % 8.21/2.84 tff(c_1548, plain, (![V_748]: (unisex(skc6, V_748) | ~abstraction(skc5, V_748)))). % 8.21/2.84 tff(c_801, plain, (![V_505, V_52, U_51]: (unisex(V_505, V_52) | ~accessible_world(U_51, V_505) | ~abstraction(U_51, V_52)))). % 8.21/2.84 tff(c_1536, plain, (![V_744]: (nonexistent(skc6, V_744) | ~eventuality(skc5, V_744)))). % 8.21/2.84 tff(c_1061, plain, (![V_597, V_10, U_9]: (nonexistent(V_597, V_10) | ~accessible_world(U_9, V_597) | ~eventuality(U_9, V_10)))). % 8.21/2.84 tff(c_1520, plain, (![V_741]: (abstraction(skc6, V_741) | ~proposition(skc5, V_741)))). % 8.21/2.84 tff(c_1512, plain, (![V_739]: (relation(skc6, V_739) | ~proposition(skc5, V_739)))). % 8.21/2.84 tff(c_984, plain, (![V_568, V_58, U_57]: (relation(V_568, V_58) | ~accessible_world(U_57, V_568) | ~proposition(U_57, V_58)))). % 8.21/2.84 tff(c_1493, plain, (![V_16]: (~abstraction(skc6, V_16) | ~event(skc5, V_16)))). % 8.21/2.84 tff(c_1487, plain, (![V_50]: (~eventuality(skc5, V_50) | ~abstraction(skc6, V_50)))). % 8.21/2.84 tff(c_1477, plain, (![V_734]: (~general(skc6, V_734) | ~eventuality(skc5, V_734)))). % 8.21/2.84 tff(c_1469, plain, (![V_732]: (specific(skc6, V_732) | ~eventuality(skc5, V_732)))). % 8.21/2.84 tff(c_1022, plain, (![V_586, V_8, U_7]: (specific(V_586, V_8) | ~accessible_world(U_7, V_586) | ~eventuality(U_7, V_8)))). % 8.21/2.84 tff(c_1457, plain, (![V_729]: (~male(skc6, V_729) | ~eventuality(skc5, V_729)))). % 8.21/2.84 tff(c_1449, plain, (![V_727]: (unisex(skc6, V_727) | ~eventuality(skc5, V_727)))). % 8.21/2.84 tff(c_800, plain, (![V_505, V_12, U_11]: (unisex(V_505, V_12) | ~accessible_world(U_11, V_505) | ~eventuality(U_11, V_12)))). % 8.21/2.84 tff(c_1433, plain, (![V_724]: (abstraction(skc6, V_724) | ~forename(skc5, V_724)))). % 8.21/2.84 tff(c_1425, plain, (![V_723]: (relation(skc6, V_723) | ~forename(skc5, V_723)))). % 8.21/2.84 tff(c_1417, plain, (![V_721]: (relname(skc6, V_721) | ~forename(skc5, V_721)))). % 8.21/2.84 tff(c_988, plain, (![V_571, V_40, U_39]: (relname(V_571, V_40) | ~accessible_world(U_39, V_571) | ~forename(U_39, V_40)))). % 8.21/2.84 tff(c_1405, plain, (![V_718]: (~human(skc6, V_718) | ~abstraction(skc5, V_718)))). % 8.21/2.84 tff(c_1397, plain, (![V_716]: (nonhuman(skc6, V_716) | ~abstraction(skc5, V_716)))). % 8.21/2.84 tff(c_977, plain, (![V_565, V_48, U_47]: (nonhuman(V_565, V_48) | ~accessible_world(U_47, V_565) | ~abstraction(U_47, V_48)))). % 8.21/2.84 tff(c_1389, plain, (![V_713]: (singleton(skc6, V_713) | ~entity(skc5, V_713)))). % 8.21/2.84 tff(c_1381, plain, (![V_711]: (thing(skc6, V_711) | ~entity(skc5, V_711)))). % 8.21/2.84 tff(c_1108, plain, (![V_621, V_24, U_23]: (thing(V_621, V_24) | ~accessible_world(U_23, V_621) | ~entity(U_23, V_24)))). % 8.21/2.84 tff(c_1362, plain, (![V_50]: (~entity(skc5, V_50) | ~abstraction(skc6, V_50)))). % 8.21/2.84 tff(c_1343, plain, (![V_697]: (~general(skc6, V_697) | ~entity(skc5, V_697)))). % 8.21/2.84 tff(c_178, plain, (![U_208, X4_215, Z_209, X2_211, X_212, X3_207, Y_213, V_214, W_206, X1_210]: (~actual_world(U_208) | ~of(U_208, X3_207, X4_215) | ~man(U_208, X4_215) | ~be(U_208, X1_210, X4_215, X2_211) | ~forename(U_208, X3_207) | ~jules_forename(U_208, X3_207) | ~man(U_208, X2_211) | ~state(U_208, X1_210) | ~of(U_208, Y_213, Z_209) | ~man(U_208, Z_209) | ~agent(U_208, X_212, Z_209) | ~forename(U_208, Y_213) | ~vincent_forename(U_208, Y_213) | ~theme(U_208, X_212, V_214) | ~event(U_208, X_212) | ~present(U_208, X_212) | ~think_believe_consider(U_208, X_212) | ~event(V_214, W_206) | ~agent(V_214, W_206, skf4(V_214)) | ~present(V_214, W_206) | ~smoke(V_214, W_206) | ~accessible_world(U_208, V_214) | ~proposition(U_208, V_214)))). % 8.21/2.84 tff(c_1335, plain, (![V_695]: (specific(skc6, V_695) | ~entity(skc5, V_695)))). % 8.21/2.84 tff(c_1023, plain, (![V_586, V_26, U_25]: (specific(V_586, V_26) | ~accessible_world(U_25, V_586) | ~entity(U_25, V_26)))). % 8.21/2.84 tff(c_1321, plain, (![V_683]: (~abstraction(V_683, skc9) | ~accessible_world(skc6, V_683)))). % 8.21/2.84 tff(c_176, plain, (![V_205, U_199, X3_198, X1_201, Y_204, Z_200, X_203, W_197, X2_202]: (man(V_205, skf4(V_205)) | ~actual_world(U_199) | ~of(U_199, X2_202, X3_198) | ~man(U_199, X3_198) | ~be(U_199, Z_200, X3_198, X1_201) | ~forename(U_199, X2_202) | ~jules_forename(U_199, X2_202) | ~man(U_199, X1_201) | ~state(U_199, Z_200) | ~of(U_199, X_203, Y_204) | ~man(U_199, Y_204) | ~agent(U_199, W_197, Y_204) | ~forename(U_199, X_203) | ~vincent_forename(U_199, X_203) | ~theme(U_199, W_197, V_205) | ~event(U_199, W_197) | ~present(U_199, W_197) | ~think_believe_consider(U_199, W_197) | ~accessible_world(U_199, V_205) | ~proposition(U_199, V_205)))). % 8.21/2.84 tff(c_1302, plain, (![V_107]: (entity(V_107, skc9) | ~accessible_world(skc6, V_107)))). % 8.21/2.84 tff(c_1265, plain, (![V_673]: (impartial(skc6, V_673) | ~human_person(skc5, V_673)))). % 8.21/2.84 tff(c_1292, plain, (entity(skc6, skc9))). % 8.21/2.84 tff(c_1266, plain, (![V_673]: (entity(skc6, V_673) | ~human_person(skc5, V_673)))). % 8.21/2.84 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.21/2.84 tff(c_1264, plain, (![V_673]: (living(skc6, V_673) | ~human_person(skc5, V_673)))). % 8.21/2.84 tff(c_1250, plain, (![V_671]: (organism(skc6, V_671) | ~human_person(skc5, V_671)))). % 8.21/2.84 tff(c_933, plain, (![V_549, V_20, U_19]: (organism(V_549, V_20) | ~accessible_world(U_19, V_549) | ~human_person(U_19, V_20)))). % 8.21/2.84 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.21/2.84 tff(c_1236, plain, (![V_469]: (~abstraction(skc5, skf2(V_469))))). % 8.21/2.84 tff(c_1211, plain, (![V_16]: (~abstraction(skc5, V_16) | ~event(skc6, V_16)))). % 8.21/2.84 tff(c_1204, plain, (![V_656]: (~entity(skc6, V_656) | ~abstraction(skc5, V_656)))). % 8.21/2.84 tff(c_1203, plain, (![V_656]: (~eventuality(skc6, V_656) | ~abstraction(skc5, V_656)))). % 8.21/2.84 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.21/2.84 tff(c_1192, plain, (![V_654]: (general(skc6, V_654) | ~abstraction(skc5, V_654)))). % 8.21/2.84 tff(c_874, plain, (![V_535, V_50, U_49]: (general(V_535, V_50) | ~accessible_world(U_49, V_535) | ~abstraction(U_49, V_50)))). % 8.21/2.84 tff(c_1184, plain, (![V_648]: (agent(V_648, skc7, skc9) | ~accessible_world(skc5, V_648)))). % 8.21/2.84 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.21/2.84 tff(c_1149, plain, (![V_640]: (theme(V_640, skc7, skc6) | ~accessible_world(skc5, V_640)))). % 8.21/2.84 tff(c_1172, plain, (![V_469]: (~entity(skc5, skf2(V_469))))). % 8.21/2.84 tff(c_1155, plain, (![V_16]: (~entity(skc5, V_16) | ~event(skc6, V_16)))). % 8.21/2.84 tff(c_1145, plain, (![V_639]: (~eventuality(skc6, V_639) | ~entity(skc5, V_639)))). % 8.21/2.84 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.21/2.85 tff(c_1137, plain, (![V_637]: (existent(skc6, V_637) | ~entity(skc5, V_637)))). % 8.21/2.85 tff(c_1113, plain, (![V_624, V_28, U_27]: (existent(V_624, V_28) | ~accessible_world(U_27, V_624) | ~entity(U_27, V_28)))). % 8.21/2.85 tff(c_1129, plain, (![V_631]: (of(V_631, skc8, skc9) | ~accessible_world(skc5, V_631)))). % 8.21/2.85 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.21/2.85 tff(c_1117, plain, (![V_627]: (proposition(V_627, skc6) | ~accessible_world(skc5, V_627)))). % 8.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 tff(c_1094, plain, (![V_614]: (think_believe_consider(V_614, skc7) | ~accessible_world(skc5, V_614)))). % 8.21/2.85 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.21/2.85 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.21/2.85 tff(c_1074, plain, (![V_605, V_193]: (present(V_605, skf2(V_193)) | ~accessible_world(skc6, V_605)))). % 8.21/2.85 tff(c_1075, plain, (![V_605]: (present(V_605, skc7) | ~accessible_world(skc5, V_605)))). % 8.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 tff(c_1067, plain, (~abstraction(skc6, skc7))). % 8.21/2.85 tff(c_1057, plain, (![V_596]: (~abstraction(V_596, skc7) | ~accessible_world(skc5, V_596)))). % 8.21/2.85 tff(c_1056, plain, (![V_596]: (~entity(V_596, skc7) | ~accessible_world(skc5, V_596)))). % 8.21/2.85 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.21/2.85 tff(c_1045, plain, (![V_593]: (event(V_593, skc7) | ~accessible_world(skc5, V_593)))). % 8.21/2.85 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.21/2.85 tff(c_1027, plain, (![V_589]: (vincent_forename(V_589, skc8) | ~accessible_world(skc5, V_589)))). % 8.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 tff(c_963, plain, (![V_137]: (abstraction(V_137, skc6) | ~accessible_world(skc6, V_137)))). % 8.21/2.85 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.21/2.85 tff(c_952, plain, (![V_554]: (abstraction(V_554, skc8) | ~accessible_world(skc6, V_554)))). % 8.21/2.85 tff(c_944, plain, (![U_15]: (~accessible_world(skc5, U_15) | ~event(U_15, skc9)))). % 8.21/2.85 tff(c_960, plain, (abstraction(skc6, skc6))). % 8.21/2.85 tff(c_954, plain, (![V_554]: (abstraction(V_554, skc6) | ~accessible_world(skc5, V_554)))). % 8.21/2.85 tff(c_915, plain, (![V_546]: (animate(V_546, skc9) | ~accessible_world(skc5, V_546)))). % 8.21/2.85 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.21/2.85 tff(c_923, plain, (![V_547]: (~eventuality(V_547, skc9) | ~accessible_world(skc5, V_547)))). % 8.21/2.85 tff(c_913, plain, (![V_546]: (entity(V_546, skc9) | ~accessible_world(skc5, V_546)))). % 8.21/2.85 tff(c_929, plain, (abstraction(skc6, skc8))). % 8.21/2.85 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.21/2.85 tff(c_902, plain, (![V_545]: (abstraction(V_545, skc8) | ~accessible_world(skc5, V_545)))). % 8.21/2.85 tff(c_894, plain, (![V_544]: (male(V_544, skc9) | ~accessible_world(skc5, V_544)))). % 8.21/2.85 tff(c_893, plain, (![V_544]: (human_person(V_544, skc9) | ~accessible_world(skc5, V_544)))). % 8.21/2.85 tff(c_882, plain, (![V_541]: (forename(V_541, skc8) | ~accessible_world(skc5, V_541)))). % 8.21/2.85 tff(c_878, plain, (![V_538]: (man(V_538, skc9) | ~accessible_world(skc5, V_538)))). % 8.21/2.85 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.21/2.85 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.21/2.85 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.21/2.85 tff(c_864, plain, (![V_526, V_527]: (~abstraction(V_526, skf2(V_527)) | ~accessible_world(skc6, V_526)))). % 8.21/2.85 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.21/2.85 tff(c_863, plain, (![V_526, V_527]: (~entity(V_526, skf2(V_527)) | ~accessible_world(skc6, V_526)))). % 8.21/2.85 tff(c_855, plain, (![V_524, V_525]: (event(V_524, skf2(V_525)) | ~accessible_world(skc6, V_524)))). % 8.21/2.85 tff(c_842, plain, (![V_520, V_191]: (smoke(V_520, skf2(V_191)) | ~accessible_world(skc6, V_520)))). % 8.21/2.85 tff(c_847, plain, (~abstraction(skc6, skc9))). % 8.21/2.85 tff(c_824, plain, (![V_513]: (~abstraction(V_513, skc9) | ~accessible_world(skc5, V_513)))). % 8.21/2.85 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.21/2.85 tff(c_836, plain, (![V_469]: (~entity(skc6, skf2(V_469))))). % 8.21/2.85 tff(c_837, plain, (~entity(skc5, skc7))). % 8.21/2.85 tff(c_806, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~event(U_15, V_16)))). % 8.21/2.85 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.21/2.85 tff(c_784, plain, (![V_498]: (human(V_498, skc9) | ~accessible_world(skc5, V_498)))). % 8.21/2.85 tff(c_814, plain, (![V_469]: (~abstraction(skc6, skf2(V_469))))). % 8.21/2.85 tff(c_815, plain, (~abstraction(skc5, skc7))). % 8.21/2.85 tff(c_794, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~event(U_15, V_16)))). % 8.21/2.85 tff(c_294, plain, (![U_27, V_28]: (~eventuality(U_27, V_28) | ~entity(U_27, V_28)))). % 8.21/2.85 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.21/2.85 tff(c_773, plain, (![U_49, V_50]: (~eventuality(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.21/2.85 tff(c_305, plain, (![U_49, V_50]: (~entity(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.21/2.85 tff(c_780, plain, (abstraction(skc5, skc8))). % 8.21/2.85 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.21/2.85 tff(c_749, plain, (![U_477, V_478]: (abstraction(U_477, V_478) | ~forename(U_477, V_478)))). % 8.21/2.85 tff(c_197, plain, (![U_236, V_237]: (singleton(U_236, V_237) | ~abstraction(U_236, V_237)))). % 8.21/2.85 tff(c_229, plain, (![U_256, V_257]: (living(U_256, V_257) | ~human_person(U_256, V_257)))). % 8.21/2.85 tff(c_272, plain, (![U_272, V_273]: (~general(U_272, V_273) | ~eventuality(U_272, V_273)))). % 8.21/2.85 tff(c_230, plain, (![U_256, V_257]: (impartial(U_256, V_257) | ~human_person(U_256, V_257)))). % 8.21/2.85 tff(c_174, plain, (![U_196]: (agent(skc6, skf2(U_196), U_196) | ~man(skc6, U_196)))). % 8.21/2.85 tff(c_217, plain, (![U_252, V_253]: (singleton(U_252, V_253) | ~entity(U_252, V_253)))). % 8.21/2.85 tff(c_765, plain, (entity(skc5, skc9))). % 8.21/2.85 tff(c_231, plain, (![U_256, V_257]: (entity(U_256, V_257) | ~human_person(U_256, V_257)))). % 8.21/2.85 tff(c_267, plain, (![U_47, V_48]: (~human(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.21/2.85 tff(c_754, plain, (abstraction(skc5, skc6))). % 8.21/2.85 tff(c_211, plain, (![U_248, V_249]: (abstraction(U_248, V_249) | ~proposition(U_248, V_249)))). % 8.21/2.85 tff(c_205, plain, (![U_39, V_40]: (relation(U_39, V_40) | ~forename(U_39, V_40)))). % 8.21/2.85 tff(c_743, plain, (~event(skc5, skc9))). % 8.21/2.85 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.21/2.85 tff(c_739, plain, (~eventuality(skc5, skc9))). % 8.21/2.86 tff(c_289, plain, (![U_282, V_283]: (~male(U_282, V_283) | ~eventuality(U_282, V_283)))). % 8.21/2.86 tff(c_733, plain, (![V_469]: (event(skc6, skf2(V_469))))). % 8.21/2.86 tff(c_728, plain, (![V_191]: (smoke(skc6, skf2(V_191))))). % 8.21/2.86 tff(c_445, plain, (![V_193]: (present(skc6, skf2(V_193))))). % 8.21/2.86 tff(c_238, plain, (![U_262, V_263]: (~general(U_262, V_263) | ~entity(U_262, V_263)))). % 8.21/2.86 tff(c_300, plain, (~abstraction(skc5, skc9))). % 8.21/2.86 tff(c_249, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~abstraction(U_51, V_52)))). % 8.21/2.86 tff(c_278, plain, (![U_276, V_277]: (singleton(U_276, V_277) | ~eventuality(U_276, V_277)))). % 8.21/2.86 tff(c_284, plain, (![U_9, V_10]: (~existent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.21/2.86 tff(c_12, plain, (![U_11, V_12]: (unisex(U_11, V_12) | ~eventuality(U_11, V_12)))). % 8.21/2.86 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 8.21/2.86 tff(c_2, plain, (![U_1, V_2]: (eventuality(U_1, V_2) | ~state(U_1, V_2)))). % 8.21/2.86 tff(c_4, plain, (![U_3, V_4]: (thing(U_3, V_4) | ~eventuality(U_3, V_4)))). % 8.21/2.86 tff(c_10, plain, (![U_9, V_10]: (nonexistent(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.21/2.86 tff(c_8, plain, (![U_7, V_8]: (specific(U_7, V_8) | ~eventuality(U_7, V_8)))). % 8.21/2.86 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 8.21/2.86 tff(c_262, plain, (animate(skc5, skc9))). % 8.21/2.86 tff(c_261, plain, (human(skc5, skc9))). % 8.21/2.86 tff(c_254, plain, (human_person(skc5, skc9))). % 8.21/2.86 tff(c_18, plain, (![U_17, V_18]: (human_person(U_17, V_18) | ~man(U_17, V_18)))). % 8.21/2.86 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 8.21/2.86 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~vincent_forename(U_59, V_60)))). % 8.21/2.86 tff(c_26, plain, (![U_25, V_26]: (specific(U_25, V_26) | ~entity(U_25, V_26)))). % 8.21/2.86 tff(c_14, plain, (![U_13, V_14]: (event(U_13, V_14) | ~state(U_13, V_14)))). % 8.21/2.86 tff(c_16, plain, (![U_15, V_16]: (eventuality(U_15, V_16) | ~event(U_15, V_16)))). % 8.21/2.86 tff(c_20, plain, (![U_19, V_20]: (organism(U_19, V_20) | ~human_person(U_19, V_20)))). % 8.21/2.86 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 8.21/2.86 tff(c_24, plain, (![U_23, V_24]: (thing(U_23, V_24) | ~entity(U_23, V_24)))). % 8.21/2.86 tff(c_28, plain, (![U_27, V_28]: (existent(U_27, V_28) | ~entity(U_27, V_28)))). % 8.21/2.86 tff(c_58, plain, (![U_57, V_58]: (relation(U_57, V_58) | ~proposition(U_57, V_58)))). % 8.21/2.86 tff(c_54, plain, (![U_53, V_54]: (forename(U_53, V_54) | ~jules_forename(U_53, V_54)))). % 8.21/2.86 tff(c_42, plain, (![U_41, V_42]: (relation(U_41, V_42) | ~relname(U_41, V_42)))). % 8.21/2.86 tff(c_56, plain, (![U_55, V_56]: (event(U_55, V_56) | ~smoke(U_55, V_56)))). % 8.21/2.86 tff(c_40, plain, (![U_39, V_40]: (relname(U_39, V_40) | ~forename(U_39, V_40)))). % 8.21/2.86 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))). % 8.21/2.86 tff(c_46, plain, (![U_45, V_46]: (thing(U_45, V_46) | ~abstraction(U_45, V_46)))). % 8.21/2.86 tff(c_48, plain, (![U_47, V_48]: (nonhuman(U_47, V_48) | ~abstraction(U_47, V_48)))). % 8.21/2.86 tff(c_50, plain, (![U_49, V_50]: (general(U_49, V_50) | ~abstraction(U_49, V_50)))). % 8.21/2.86 tff(c_190, plain, (male(skc5, skc9))). % 8.21/2.86 tff(c_38, plain, (![U_37, V_38]: (male(U_37, V_38) | ~man(U_37, V_38)))). % 8.21/2.86 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~abstraction(U_51, V_52)))). % 8.21/2.86 tff(c_34, plain, (![U_33, V_34]: (human(U_33, V_34) | ~human_person(U_33, V_34)))). % 8.21/2.86 tff(c_32, plain, (![U_31, V_32]: (living(U_31, V_32) | ~organism(U_31, V_32)))). % 8.21/2.86 tff(c_36, plain, (![U_35, V_36]: (animate(U_35, V_36) | ~human_person(U_35, V_36)))). % 8.21/2.86 tff(c_30, plain, (![U_29, V_30]: (impartial(U_29, V_30) | ~organism(U_29, V_30)))). % 8.21/2.86 tff(c_6, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~thing(U_5, V_6)))). % 8.21/2.86 tff(c_22, plain, (![U_21, V_22]: (entity(U_21, V_22) | ~organism(U_21, V_22)))). % 8.21/2.86 tff(c_166, plain, (theme(skc5, skc7, skc6))). % 8.21/2.86 tff(c_162, plain, (of(skc5, skc8, skc9))). % 8.21/2.86 tff(c_164, plain, (agent(skc5, skc7, skc9))). % 8.21/2.86 tff(c_154, plain, (present(skc5, skc7))). % 8.21/2.86 tff(c_152, plain, (event(skc5, skc7))). % 8.21/2.86 tff(c_150, plain, (vincent_forename(skc5, skc8))). % 8.21/2.86 tff(c_156, plain, (think_believe_consider(skc5, skc7))). % 8.21/2.86 tff(c_148, plain, (forename(skc5, skc8))). % 8.21/2.86 tff(c_146, plain, (man(skc5, skc9))). % 8.21/2.86 tff(c_158, plain, (accessible_world(skc5, skc6))). % 8.21/2.86 tff(c_160, plain, (proposition(skc5, skc6))). % 8.21/2.86 tff(c_144, plain, (actual_world(skc5))). % 8.21/2.86 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.21/2.86 %------------------------------------------------------------------------------