%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP024-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:47:57 PM UTC 2025 % Result : Satisfiable 8.51s 2.91s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP024-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 08:10:02 EDT 2025 % 0.12/0.33 % CPUTime : % 8.51/2.91 % 8.51/2.91 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.51/2.92 % 8.51/2.92 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.51/2.92 %$ theme > of > agent > woman > vincent_forename > unisex > thing > specific > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > mia_forename > man > male > living > impartial > human_person > human > general > forename > female > existent > eventuality > event > entity > desire_want > dance > animate > accessible_world > abstraction > actual_world > #nlpp > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 % 8.51/2.92 % 8.51/2.92 %Foreground sorts: % 8.51/2.92 % 8.51/2.92 % 8.51/2.92 %Background operators: % 8.51/2.92 % 8.51/2.92 % 8.51/2.92 %Foreground operators: % 8.51/2.92 tff(relation, type, relation: ($i * $i) > $o). % 8.51/2.92 tff(forename, type, forename: ($i * $i) > $o). % 8.51/2.92 tff(female, type, female: ($i * $i) > $o). % 8.51/2.92 tff(theme, type, theme: ($i * $i * $i) > $o). % 8.51/2.92 tff(living, type, living: ($i * $i) > $o). % 8.51/2.92 tff(human_person, type, human_person: ($i * $i) > $o). % 8.51/2.92 tff(present, type, present: ($i * $i) > $o). % 8.51/2.92 tff(skc11, type, skc11: $i). % 8.51/2.92 tff(entity, type, entity: ($i * $i) > $o). % 8.51/2.92 tff(skc9, type, skc9: $i). % 8.51/2.92 tff(eventuality, type, eventuality: ($i * $i) > $o). % 8.51/2.92 tff(existent, type, existent: ($i * $i) > $o). % 8.51/2.92 tff(abstraction, type, abstraction: ($i * $i) > $o). % 8.51/2.92 tff(skc8, type, skc8: $i). % 8.51/2.92 tff(proposition, type, proposition: ($i * $i) > $o). % 8.51/2.92 tff(relname, type, relname: ($i * $i) > $o). % 8.51/2.92 tff(skc14, type, skc14: $i). % 8.51/2.92 tff(singleton, type, singleton: ($i * $i) > $o). % 8.51/2.92 tff(skc13, type, skc13: $i). % 8.51/2.92 tff(male, type, male: ($i * $i) > $o). % 8.51/2.92 tff(organism, type, organism: ($i * $i) > $o). % 8.51/2.92 tff(animate, type, animate: ($i * $i) > $o). % 8.51/2.92 tff(of, type, of: ($i * $i * $i) > $o). % 8.51/2.92 tff(actual_world, type, actual_world: $i > $o). % 8.51/2.92 tff(agent, type, agent: ($i * $i * $i) > $o). % 8.51/2.92 tff(general, type, general: ($i * $i) > $o). % 8.51/2.92 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 8.51/2.92 tff(event, type, event: ($i * $i) > $o). % 8.51/2.92 tff(woman, type, woman: ($i * $i) > $o). % 8.51/2.92 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 8.51/2.92 tff(thing, type, thing: ($i * $i) > $o). % 8.51/2.92 tff(dance, type, dance: ($i * $i) > $o). % 8.51/2.92 tff(desire_want, type, desire_want: ($i * $i) > $o). % 8.51/2.92 tff(skc15, type, skc15: $i). % 8.51/2.92 tff(human, type, human: ($i * $i) > $o). % 8.51/2.92 tff(man, type, man: ($i * $i) > $o). % 8.51/2.92 tff(unisex, type, unisex: ($i * $i) > $o). % 8.51/2.92 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 8.51/2.92 tff(impartial, type, impartial: ($i * $i) > $o). % 8.51/2.92 tff(skc12, type, skc12: $i). % 8.51/2.92 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 8.51/2.92 tff(specific, type, specific: ($i * $i) > $o). % 8.51/2.92 tff(skc10, type, skc10: $i). % 8.51/2.92 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 8.51/2.92 % 8.51/2.92 %Saturated clause set: % 8.51/2.93 tff(c_2492, plain, (![V_88, V_712, V_711]: (singleton(V_88, V_712) | ~accessible_world(V_711, V_88) | ~accessible_world(skc10, V_711) | ~entity(skc8, V_712)))). % 8.51/2.93 tff(c_2465, plain, (![V_109, V_706, V_705]: (relation(V_109, V_706) | ~accessible_world(V_705, V_109) | ~accessible_world(skc10, V_705) | ~forename(skc8, V_706)))). % 8.51/2.93 tff(c_2408, plain, (![V_88, V_698, V_697]: (singleton(V_88, V_698) | ~accessible_world(V_697, V_88) | ~accessible_world(skc10, V_697) | ~abstraction(skc8, V_698)))). % 8.51/2.93 tff(c_2596, plain, (![V_145, V_730, V_729]: (impartial(V_145, V_730) | ~accessible_world(V_729, V_145) | ~accessible_world(skc10, V_729) | ~human_person(skc8, V_730)))). % 8.51/2.93 tff(c_2365, plain, (![V_88, V_688, V_687]: (singleton(V_88, V_688) | ~accessible_world(V_687, V_88) | ~accessible_world(skc10, V_687) | ~eventuality(skc8, V_688)))). % 8.51/2.93 tff(c_2369, plain, (![V_148, V_690, V_689]: (living(V_148, V_690) | ~accessible_world(V_689, V_148) | ~accessible_world(skc10, V_689) | ~human_person(skc8, V_690)))). % 8.51/2.93 tff(c_2213, plain, (![V_97, V_666, V_665]: (unisex(V_97, V_666) | ~accessible_world(V_665, V_97) | ~accessible_world(skc10, V_665) | ~abstraction(skc8, V_666)))). % 8.51/2.93 tff(c_2050, plain, (![V_91, V_644, V_643]: (specific(V_91, V_644) | ~accessible_world(V_643, V_91) | ~accessible_world(skc10, V_643) | ~eventuality(skc8, V_644)))). % 8.51/2.93 tff(c_2201, plain, (![V_79, V_664, V_663]: (event(V_79, V_664) | ~accessible_world(V_663, V_79) | ~accessible_world(skc10, V_663) | ~dance(skc8, V_664)))). % 8.51/2.93 tff(c_2070, plain, (![V_91, V_650, V_649]: (specific(V_91, V_650) | ~accessible_world(V_649, V_91) | ~accessible_world(skc10, V_649) | ~entity(skc8, V_650)))). % 8.51/2.93 tff(c_2295, plain, (![V_79, V_674, V_673]: (event(V_79, V_674) | ~accessible_world(V_673, V_79) | ~accessible_world(skc10, V_673) | ~desire_want(skc8, V_674)))). % 8.51/2.93 tff(c_2042, plain, (![V_124, V_642, V_641]: (relname(V_124, V_642) | ~accessible_world(V_641, V_124) | ~accessible_world(skc10, V_641) | ~forename(skc8, V_642)))). % 8.51/2.93 tff(c_2034, plain, (![V_85, V_640, V_639]: (thing(V_85, V_640) | ~accessible_world(V_639, V_85) | ~accessible_world(skc10, V_639) | ~abstraction(skc8, V_640)))). % 8.51/2.93 tff(c_2321, plain, (![V_118, V_678, V_677]: (general(V_118, V_678) | ~accessible_world(V_677, V_118) | ~accessible_world(skc10, V_677) | ~abstraction(skc8, V_678)))). % 8.51/2.93 tff(c_2078, plain, (![V_109, V_652, V_651]: (relation(V_109, V_652) | ~accessible_world(V_651, V_109) | ~accessible_world(skc10, V_651) | ~proposition(skc8, V_652)))). % 8.51/2.93 tff(c_2147, plain, (![V_97, V_660, V_659]: (unisex(V_97, V_660) | ~accessible_world(V_659, V_97) | ~accessible_world(skc10, V_659) | ~eventuality(skc8, V_660)))). % 8.51/2.93 tff(c_2133, plain, (![V_82, V_658, V_657]: (eventuality(V_82, V_658) | ~accessible_world(V_657, V_82) | ~accessible_world(skc10, V_657) | ~event(skc8, V_658)))). % 8.51/2.93 tff(c_2339, plain, (![V_142, V_682, V_681]: (existent(V_142, V_682) | ~accessible_world(V_681, V_142) | ~accessible_world(skc10, V_681) | ~entity(skc8, V_682)))). % 8.51/2.93 tff(c_2228, plain, (![V_136, V_668, V_667]: (organism(V_136, V_668) | ~accessible_world(V_667, V_136) | ~accessible_world(skc10, V_667) | ~human_person(skc8, V_668)))). % 8.51/2.93 tff(c_2238, plain, (![V_115, V_670, V_669]: (nonhuman(V_115, V_670) | ~accessible_world(V_669, V_115) | ~accessible_world(skc10, V_669) | ~abstraction(skc8, V_670)))). % 8.51/2.93 tff(c_2347, plain, (![V_85, V_684, V_683]: (thing(V_85, V_684) | ~accessible_world(V_683, V_85) | ~accessible_world(skc10, V_683) | ~eventuality(skc8, V_684)))). % 8.51/2.93 tff(c_2058, plain, (![V_94, V_646, V_645]: (nonexistent(V_94, V_646) | ~accessible_world(V_645, V_94) | ~accessible_world(skc10, V_645) | ~eventuality(skc8, V_646)))). % 8.51/2.93 tff(c_2865, plain, (![U_15, V_16]: (~accessible_world(skc10, U_15) | ~entity(skc8, V_16) | ~desire_want(U_15, V_16)))). % 8.51/2.93 tff(c_1857, plain, (![V_139, V_582]: (entity(V_139, skc15) | ~accessible_world(V_582, V_139) | ~accessible_world(skc10, V_582)))). % 8.51/2.93 tff(c_2903, plain, (![U_15, V_16]: (~accessible_world(skc10, U_15) | ~abstraction(skc8, V_16) | ~desire_want(U_15, V_16)))). % 8.51/2.93 tff(c_2904, plain, (![U_1, V_2]: (~accessible_world(skc10, U_1) | ~abstraction(skc8, V_2) | ~dance(U_1, V_2)))). % 8.51/2.93 tff(c_2866, plain, (![U_1, V_2]: (~accessible_world(skc10, U_1) | ~entity(skc8, V_2) | ~dance(U_1, V_2)))). % 8.51/2.93 tff(c_1811, plain, (![V_139, V_581]: (entity(V_139, skc12) | ~accessible_world(V_581, V_139) | ~accessible_world(skc10, V_581)))). % 8.51/2.93 tff(c_2361, plain, (![U_3, V_4]: (~accessible_world(skc10, U_3) | ~abstraction(skc8, V_4) | ~event(U_3, V_4)))). % 8.51/2.93 tff(c_2458, plain, (![U_25, V_26]: (~accessible_world(skc10, U_25) | ~entity(skc8, V_26) | ~abstraction(U_25, V_26)))). % 8.51/2.93 tff(c_2246, plain, (![V_85, V_672, V_671]: (thing(V_85, V_672) | ~accessible_world(V_671, V_85) | ~accessible_world(skc10, V_671) | ~entity(skc8, V_672)))). % 8.51/2.93 tff(c_2479, plain, (![U_3, V_4]: (~accessible_world(skc10, U_3) | ~entity(skc8, V_4) | ~event(U_3, V_4)))). % 8.51/2.93 tff(c_2466, plain, (![V_705, V_706]: (abstraction(V_705, V_706) | ~accessible_world(skc10, V_705) | ~forename(skc8, V_706)))). % 8.51/2.93 tff(c_2382, plain, (![U_25, V_26]: (~accessible_world(skc10, U_25) | ~eventuality(skc8, V_26) | ~abstraction(U_25, V_26)))). % 8.51/2.93 tff(c_2509, plain, (![U_45, V_46]: (~accessible_world(skc10, U_45) | ~eventuality(skc8, V_46) | ~entity(U_45, V_46)))). % 8.51/2.93 tff(c_2293, plain, (![V_673, V_674]: (~entity(V_673, V_674) | ~accessible_world(skc10, V_673) | ~desire_want(skc8, V_674)))). % 8.51/2.93 tff(c_763, plain, (![V_151, V_383]: (human(V_151, skc12) | ~accessible_world(V_383, V_151) | ~accessible_world(skc8, V_383)))). % 8.51/2.93 tff(c_2148, plain, (![V_659, V_660]: (~female(V_659, V_660) | ~accessible_world(skc10, V_659) | ~eventuality(skc8, V_660)))). % 8.51/2.93 tff(c_1148, plain, (![W_494, V_456, V_496]: (skc10=W_494 | ~desire_want(V_456, skc9) | ~proposition(V_456, skc10) | ~proposition(V_456, W_494) | ~desire_want(V_456, V_496) | ~theme(V_456, V_496, W_494) | ~accessible_world(skc8, V_456)))). % 8.51/2.93 tff(c_2079, plain, (![V_651, V_652]: (abstraction(V_651, V_652) | ~accessible_world(skc10, V_651) | ~proposition(skc8, V_652)))). % 8.51/2.93 tff(c_2748, plain, (~event(skc8, skc14))). % 8.51/2.94 tff(c_668, plain, (![V_154, V_362]: (animate(V_154, skc12) | ~accessible_world(V_362, V_154) | ~accessible_world(skc8, V_362)))). % 8.51/2.94 tff(c_2727, plain, (~event(skc8, skc10))). % 8.51/2.94 tff(c_2710, plain, (~event(skc8, skc11))). % 8.51/2.94 tff(c_2134, plain, (![V_657, V_658]: (~abstraction(V_657, V_658) | ~accessible_world(skc10, V_657) | ~event(skc8, V_658)))). % 8.51/2.94 tff(c_959, plain, (![V_438, V_334]: (entity(V_438, skc15) | ~accessible_world(V_334, V_438) | ~accessible_world(skc8, V_334)))). % 8.51/2.94 tff(c_2135, plain, (![V_657, V_658]: (~entity(V_657, V_658) | ~accessible_world(skc10, V_657) | ~event(skc8, V_658)))). % 8.51/2.94 tff(c_1121, plain, (![W_483, V_467]: (skc11=W_483 | ~entity(V_467, skc12) | ~forename(V_467, W_483) | ~of(V_467, W_483, skc12) | ~forename(V_467, skc11) | ~accessible_world(skc8, V_467)))). % 8.51/2.94 tff(c_2648, plain, (~desire_want(skc8, skc14))). % 8.51/2.94 tff(c_2647, plain, (~desire_want(skc8, skc10))). % 8.51/2.94 tff(c_2149, plain, (![V_659, V_660]: (~male(V_659, V_660) | ~accessible_world(skc10, V_659) | ~eventuality(skc8, V_660)))). % 8.51/2.94 tff(c_2637, plain, (~desire_want(skc8, skc11))). % 8.51/2.94 tff(c_2294, plain, (![V_673, V_674]: (~abstraction(V_673, V_674) | ~accessible_world(skc10, V_673) | ~desire_want(skc8, V_674)))). % 8.51/2.94 tff(c_1133, plain, (![W_182, V_487]: (skc14=W_182 | ~entity(V_487, skc15) | ~forename(V_487, W_182) | ~of(V_487, W_182, skc15) | ~forename(V_487, skc14) | ~accessible_world(skc8, V_487)))). % 8.51/2.94 tff(c_2215, plain, (![V_665, V_666]: (~male(V_665, V_666) | ~accessible_world(skc10, V_665) | ~abstraction(skc8, V_666)))). % 8.51/2.94 tff(c_2592, plain, (~dance(skc8, skc14))). % 8.51/2.94 tff(c_1766, plain, (![V_145, V_580]: (impartial(V_145, V_580) | ~accessible_world(skc10, V_145) | ~human_person(skc8, V_580)))). % 8.51/2.94 tff(c_2587, plain, (~dance(skc8, skc10))). % 8.51/2.94 tff(c_1109, plain, (![V_169, V_481]: (agent(V_169, skc9, skc12) | ~accessible_world(V_481, V_169) | ~accessible_world(skc8, V_481)))). % 8.51/2.94 tff(c_2586, plain, (~dance(skc8, skc11))). % 8.51/2.94 tff(c_2200, plain, (![V_663, V_664]: (~abstraction(V_663, V_664) | ~accessible_world(skc10, V_663) | ~dance(skc8, V_664)))). % 8.51/2.94 tff(c_2229, plain, (![V_667, V_668]: (entity(V_667, V_668) | ~accessible_world(skc10, V_667) | ~human_person(skc8, V_668)))). % 8.51/2.94 tff(c_960, plain, (![V_438, V_336]: (entity(V_438, skc12) | ~accessible_world(V_336, V_438) | ~accessible_world(skc8, V_336)))). % 8.51/2.94 tff(c_771, plain, (![V_151, V_384]: (human(V_151, skc15) | ~accessible_world(V_384, V_151) | ~accessible_world(skc8, V_384)))). % 8.51/2.94 tff(c_2199, plain, (![V_663, V_664]: (~entity(V_663, V_664) | ~accessible_world(skc10, V_663) | ~dance(skc8, V_664)))). % 8.51/2.94 tff(c_2059, plain, (![V_645, V_646]: (~existent(V_645, V_646) | ~accessible_world(skc10, V_645) | ~eventuality(skc8, V_646)))). % 8.51/2.94 tff(c_1134, plain, (![V_177, V_487]: (of(V_177, skc14, skc15) | ~accessible_world(V_487, V_177) | ~accessible_world(skc8, V_487)))). % 8.51/2.94 tff(c_1570, plain, (![V_88, V_552]: (singleton(V_88, V_552) | ~accessible_world(skc10, V_88) | ~entity(skc8, V_552)))). % 8.51/2.94 tff(c_2214, plain, (![V_665, V_666]: (~female(V_665, V_666) | ~accessible_world(skc10, V_665) | ~abstraction(skc8, V_666)))). % 8.51/2.94 tff(c_2340, plain, (![V_681, V_682]: (~eventuality(V_681, V_682) | ~accessible_world(skc10, V_681) | ~entity(skc8, V_682)))). % 8.51/2.94 tff(c_2043, plain, (![V_641, V_642]: (relation(V_641, V_642) | ~accessible_world(skc10, V_641) | ~forename(skc8, V_642)))). % 8.51/2.94 tff(c_2071, plain, (![V_649, V_650]: (~general(V_649, V_650) | ~accessible_world(skc10, V_649) | ~entity(skc8, V_650)))). % 8.51/2.94 tff(c_2322, plain, (![V_677, V_678]: (~entity(V_677, V_678) | ~accessible_world(skc10, V_677) | ~abstraction(skc8, V_678)))). % 8.51/2.94 tff(c_650, plain, (![V_154, V_356]: (animate(V_154, skc15) | ~accessible_world(V_356, V_154) | ~accessible_world(skc8, V_356)))). % 8.51/2.94 tff(c_2035, plain, (![V_639, V_640]: (singleton(V_639, V_640) | ~accessible_world(skc10, V_639) | ~abstraction(skc8, V_640)))). % 8.51/2.94 tff(c_1138, plain, (![V_169, V_488]: (agent(V_169, skc13, skc12) | ~accessible_world(V_488, V_169) | ~accessible_world(skc10, V_488)))). % 8.51/2.94 tff(c_2239, plain, (![V_669, V_670]: (~human(V_669, V_670) | ~accessible_world(skc10, V_669) | ~abstraction(skc8, V_670)))). % 8.51/2.94 tff(c_2051, plain, (![V_643, V_644]: (~general(V_643, V_644) | ~accessible_world(skc10, V_643) | ~eventuality(skc8, V_644)))). % 8.51/2.94 tff(c_2230, plain, (![V_667, V_668]: (living(V_667, V_668) | ~accessible_world(skc10, V_667) | ~human_person(skc8, V_668)))). % 8.51/2.94 tff(c_2348, plain, (![V_683, V_684]: (singleton(V_683, V_684) | ~accessible_world(skc10, V_683) | ~eventuality(skc8, V_684)))). % 8.51/2.94 tff(c_2323, plain, (![V_677, V_678]: (~eventuality(V_677, V_678) | ~accessible_world(skc10, V_677) | ~abstraction(skc8, V_678)))). % 8.51/2.94 tff(c_1753, plain, (![V_85, V_577]: (thing(V_85, V_577) | ~accessible_world(skc10, V_85) | ~eventuality(skc8, V_577)))). % 8.51/2.94 tff(c_1449, plain, (![V_142, V_536]: (existent(V_142, V_536) | ~accessible_world(skc10, V_142) | ~entity(skc8, V_536)))). % 8.51/2.94 tff(c_679, plain, (![V_364, V_330]: (female(V_364, skc12) | ~accessible_world(V_330, V_364) | ~accessible_world(skc8, V_330)))). % 8.51/2.94 tff(c_1306, plain, (![V_118, V_517]: (general(V_118, V_517) | ~accessible_world(skc10, V_118) | ~abstraction(skc8, V_517)))). % 8.51/2.94 tff(c_1021, plain, (![V_173, V_463]: (theme(V_173, skc9, skc10) | ~accessible_world(V_463, V_173) | ~accessible_world(skc8, V_463)))). % 8.51/2.94 tff(c_1899, plain, (![V_79, V_587]: (event(V_79, V_587) | ~accessible_world(skc10, V_79) | ~desire_want(skc8, V_587)))). % 8.51/2.94 tff(c_1565, plain, (![V_85, V_551]: (thing(V_85, V_551) | ~accessible_world(skc10, V_85) | ~entity(skc8, V_551)))). % 8.51/2.94 tff(c_1581, plain, (![V_115, V_556]: (nonhuman(V_115, V_556) | ~accessible_world(skc10, V_115) | ~abstraction(skc8, V_556)))). % 8.51/2.94 tff(c_1666, plain, (![V_136, V_572]: (organism(V_136, V_572) | ~accessible_world(skc10, V_136) | ~human_person(skc8, V_572)))). % 8.51/2.94 tff(c_999, plain, (![V_97, V_460]: (unisex(V_97, V_460) | ~accessible_world(skc10, V_97) | ~abstraction(skc8, V_460)))). % 8.51/2.94 tff(c_1177, plain, (![V_79, V_497]: (event(V_79, V_497) | ~accessible_world(skc10, V_79) | ~dance(skc8, V_497)))). % 8.51/2.94 tff(c_569, plain, (![V_133, V_336]: (human_person(V_133, skc12) | ~accessible_world(V_336, V_133) | ~accessible_world(skc8, V_336)))). % 8.51/2.94 tff(c_1436, plain, (![V_97, V_535]: (unisex(V_97, V_535) | ~accessible_world(skc10, V_97) | ~eventuality(skc8, V_535)))). % 8.51/2.94 tff(c_1211, plain, (![V_82, V_502]: (eventuality(V_82, V_502) | ~accessible_world(skc10, V_82) | ~event(skc8, V_502)))). % 8.51/2.94 tff(c_1113, plain, (![V_177, V_482]: (of(V_177, skc11, skc12) | ~accessible_world(V_482, V_177) | ~accessible_world(skc8, V_482)))). % 8.51/2.94 tff(c_544, plain, (![V_133, V_334]: (human_person(V_133, skc15) | ~accessible_world(V_334, V_133) | ~accessible_world(skc8, V_334)))). % 8.51/2.94 tff(c_1608, plain, (![V_109, V_561]: (relation(V_109, V_561) | ~accessible_world(skc10, V_109) | ~proposition(skc8, V_561)))). % 8.51/2.94 tff(c_1262, plain, (![V_91, V_511]: (specific(V_91, V_511) | ~accessible_world(skc10, V_91) | ~entity(skc8, V_511)))). % 8.51/2.94 tff(c_904, plain, (![V_417, V_320]: (male(V_417, skc15) | ~accessible_world(V_320, V_417) | ~accessible_world(skc8, V_320)))). % 8.51/2.94 tff(c_1039, plain, (![V_94, V_471]: (nonexistent(V_94, V_471) | ~accessible_world(skc10, V_94) | ~eventuality(skc8, V_471)))). % 8.51/2.94 tff(c_1620, plain, (![V_91, V_565]: (specific(V_91, V_565) | ~accessible_world(skc10, V_91) | ~eventuality(skc8, V_565)))). % 8.51/2.94 tff(c_1344, plain, (![V_124, V_523]: (relname(V_124, V_523) | ~accessible_world(skc10, V_124) | ~forename(skc8, V_523)))). % 8.51/2.95 tff(c_1530, plain, (![V_85, V_545]: (thing(V_85, V_545) | ~accessible_world(skc10, V_85) | ~abstraction(skc8, V_545)))). % 8.51/2.95 tff(c_936, plain, (![V_100, V_432]: (present(V_100, skc9) | ~accessible_world(V_432, V_100) | ~accessible_world(skc8, V_432)))). % 8.51/2.95 tff(c_1127, plain, (![W_483]: (skc11=W_483 | ~forename(skc8, W_483) | ~of(skc8, W_483, skc12)))). % 8.51/2.95 tff(c_503, plain, (![V_121, V_327]: (forename(V_121, skc14) | ~accessible_world(V_327, V_121) | ~accessible_world(skc8, V_327)))). % 8.51/2.95 tff(c_518, plain, (![V_130, V_330]: (woman(V_130, skc12) | ~accessible_world(V_330, V_130) | ~accessible_world(skc8, V_330)))). % 8.51/2.95 tff(c_585, plain, (![V_339, V_42, U_41]: (singleton(V_339, V_42) | ~accessible_world(U_41, V_339) | ~entity(U_41, V_42)))). % 8.51/2.95 tff(c_495, plain, (![V_79, V_323]: (event(V_79, skc13) | ~accessible_world(V_323, V_79) | ~accessible_world(skc10, V_323)))). % 8.51/2.95 tff(c_1124, plain, (![W_483]: (skc14=W_483 | ~forename(skc8, W_483) | ~of(skc8, W_483, skc15)))). % 8.51/2.95 tff(c_801, plain, (![V_160, V_391]: (vincent_forename(V_160, skc14) | ~accessible_world(V_391, V_160) | ~accessible_world(skc8, V_391)))). % 8.51/2.95 tff(c_586, plain, (![V_339, V_22, U_21]: (singleton(V_339, V_22) | ~accessible_world(U_21, V_339) | ~abstraction(U_21, V_22)))). % 8.51/2.95 tff(c_932, plain, (![V_100, V_431]: (present(V_100, skc13) | ~accessible_world(V_431, V_100) | ~accessible_world(skc10, V_431)))). % 8.51/2.95 tff(c_1963, plain, (~agent(skc8, skc9, skc15))). % 8.51/2.95 tff(c_812, plain, (![V_393, V_38, U_37]: (living(V_393, V_38) | ~accessible_world(U_37, V_393) | ~human_person(U_37, V_38)))). % 8.51/2.95 tff(c_453, plain, (![V_145, V_308, U_307]: (impartial(V_145, V_308) | ~accessible_world(U_307, V_145) | ~human_person(U_307, V_308)))). % 8.51/2.95 tff(c_696, plain, (![V_127, V_371]: (mia_forename(V_127, skc11) | ~accessible_world(V_371, V_127) | ~accessible_world(skc8, V_371)))). % 8.51/2.95 tff(c_584, plain, (![V_339, V_6, U_5]: (singleton(V_339, V_6) | ~accessible_world(U_5, V_339) | ~eventuality(U_5, V_6)))). % 8.51/2.95 tff(c_382, plain, (![V_106, V_285]: (proposition(V_106, skc10) | ~accessible_world(V_285, V_106) | ~accessible_world(skc8, V_285)))). % 8.51/2.95 tff(c_947, plain, (![V_76, V_436]: (dance(V_76, skc13) | ~accessible_world(V_436, V_76) | ~accessible_world(skc10, V_436)))). % 8.51/2.95 tff(c_488, plain, (![V_163, V_320]: (man(V_163, skc15) | ~accessible_world(V_320, V_163) | ~accessible_world(skc8, V_320)))). % 8.75/2.95 tff(c_844, plain, (![V_103, V_404]: (desire_want(V_103, skc9) | ~accessible_world(V_404, V_103) | ~accessible_world(skc8, V_404)))). % 8.75/2.95 tff(c_1913, plain, (~accessible_world(skc8, skc8))). % 8.75/2.95 tff(c_1151, plain, (![W_494, V_496]: (skc10=W_494 | ~proposition(skc8, W_494) | ~desire_want(skc8, V_496) | ~theme(skc8, V_496, W_494)))). % 8.75/2.95 tff(c_465, plain, (![V_121, V_314]: (forename(V_121, skc11) | ~accessible_world(V_314, V_121) | ~accessible_world(skc8, V_314)))). % 8.75/2.95 tff(c_1858, plain, (![V_582]: (~dance(V_582, skc15) | ~accessible_world(skc10, V_582)))). % 8.75/2.95 tff(c_1814, plain, (![V_581]: (~abstraction(V_581, skc12) | ~accessible_world(skc10, V_581)))). % 8.75/2.95 tff(c_1859, plain, (![V_582]: (~desire_want(V_582, skc15) | ~accessible_world(skc10, V_582)))). % 8.75/2.95 tff(c_972, plain, (![V_444, V_30, U_29]: (relation(V_444, V_30) | ~accessible_world(U_29, V_444) | ~forename(U_29, V_30)))). % 8.75/2.95 tff(c_1860, plain, (![V_582]: (~abstraction(V_582, skc15) | ~accessible_world(skc10, V_582)))). % 8.75/2.95 tff(c_1813, plain, (![V_581]: (~desire_want(V_581, skc12) | ~accessible_world(skc10, V_581)))). % 8.75/2.95 tff(c_1865, plain, (![V_585]: (event(skc10, V_585) | ~desire_want(skc8, V_585)))). % 8.75/2.95 tff(c_420, plain, (![V_293, V_16, U_15]: (event(V_293, V_16) | ~accessible_world(U_15, V_293) | ~desire_want(U_15, V_16)))). % 8.75/2.95 tff(c_1812, plain, (![V_581]: (~dance(V_581, skc12) | ~accessible_world(skc10, V_581)))). % 8.75/2.95 tff(c_1739, plain, (![V_139]: (entity(V_139, skc15) | ~accessible_world(skc10, V_139)))). % 8.75/2.95 tff(c_1712, plain, (![V_139]: (entity(V_139, skc12) | ~accessible_world(skc10, V_139)))). % 8.75/2.95 tff(c_1669, plain, (![V_572]: (impartial(skc10, V_572) | ~human_person(skc8, V_572)))). % 8.75/2.95 tff(c_1754, plain, (![V_577]: (singleton(skc10, V_577) | ~eventuality(skc8, V_577)))). % 8.75/2.95 tff(c_1668, plain, (![V_572]: (living(skc10, V_572) | ~human_person(skc8, V_572)))). % 8.75/2.95 tff(c_1746, plain, (![V_575]: (thing(skc10, V_575) | ~eventuality(skc8, V_575)))). % 8.75/2.95 tff(c_528, plain, (![V_331, V_6, U_5]: (thing(V_331, V_6) | ~accessible_world(U_5, V_331) | ~eventuality(U_5, V_6)))). % 8.75/2.95 tff(c_1688, plain, (entity(skc10, skc15))). % 8.75/2.95 tff(c_1687, plain, (entity(skc10, skc12))). % 8.75/2.95 tff(c_1667, plain, (![V_572]: (entity(skc10, V_572) | ~human_person(skc8, V_572)))). % 8.77/2.95 tff(c_1653, plain, (![V_570]: (organism(skc10, V_570) | ~human_person(skc8, V_570)))). % 8.77/2.95 tff(c_867, plain, (![V_408, V_38, U_37]: (organism(V_408, V_38) | ~accessible_world(U_37, V_408) | ~human_person(U_37, V_38)))). % 8.77/2.95 tff(c_1643, plain, (![V_26]: (~eventuality(skc8, V_26) | ~abstraction(skc10, V_26)))). % 8.77/2.95 tff(c_1621, plain, (![V_565]: (~general(skc10, V_565) | ~eventuality(skc8, V_565)))). % 8.77/2.95 tff(c_1609, plain, (![V_561]: (abstraction(skc10, V_561) | ~proposition(skc8, V_561)))). % 8.77/2.95 tff(c_1613, plain, (![V_563]: (specific(skc10, V_563) | ~eventuality(skc8, V_563)))). % 8.77/2.95 tff(c_339, plain, (![V_266, V_10, U_9]: (specific(V_266, V_10) | ~accessible_world(U_9, V_266) | ~eventuality(U_9, V_10)))). % 8.77/2.95 tff(c_1601, plain, (![V_559]: (relation(skc10, V_559) | ~proposition(skc8, V_559)))). % 8.77/2.95 tff(c_973, plain, (![V_444, V_18, U_17]: (relation(V_444, V_18) | ~accessible_world(U_17, V_444) | ~proposition(U_17, V_18)))). % 8.77/2.95 tff(c_1582, plain, (![V_556]: (~human(skc10, V_556) | ~abstraction(skc8, V_556)))). % 8.77/2.95 tff(c_1574, plain, (![V_554]: (nonhuman(skc10, V_554) | ~abstraction(skc8, V_554)))). % 8.77/2.95 tff(c_966, plain, (![V_441, V_24, U_23]: (nonhuman(V_441, V_24) | ~accessible_world(U_23, V_441) | ~abstraction(U_23, V_24)))). % 8.77/2.95 tff(c_1566, plain, (![V_551]: (singleton(skc10, V_551) | ~entity(skc8, V_551)))). % 8.77/2.95 tff(c_1558, plain, (![V_549]: (thing(skc10, V_549) | ~entity(skc8, V_549)))). % 8.77/2.95 tff(c_530, plain, (![V_331, V_42, U_41]: (thing(V_331, V_42) | ~accessible_world(U_41, V_331) | ~entity(U_41, V_42)))). % 8.77/2.95 tff(c_1554, plain, (~dance(skc10, skc12))). % 8.77/2.95 tff(c_1553, plain, (~dance(skc10, skc15))). % 8.77/2.95 tff(c_1499, plain, (![V_2]: (~entity(skc8, V_2) | ~dance(skc10, V_2)))). % 8.77/2.95 tff(c_1531, plain, (![V_545]: (singleton(skc10, V_545) | ~abstraction(skc8, V_545)))). % 8.77/2.95 tff(c_1523, plain, (![V_543]: (thing(skc10, V_543) | ~abstraction(skc8, V_543)))). % 8.77/2.95 tff(c_1519, plain, (~desire_want(skc10, skc12))). % 8.77/2.95 tff(c_1518, plain, (~desire_want(skc10, skc15))). % 8.77/2.95 tff(c_529, plain, (![V_331, V_22, U_21]: (thing(V_331, V_22) | ~accessible_world(U_21, V_331) | ~abstraction(U_21, V_22)))). % 8.77/2.95 tff(c_1498, plain, (![V_16]: (~entity(skc8, V_16) | ~desire_want(skc10, V_16)))). % 8.77/2.95 tff(c_1500, plain, (~entity(skc8, skc13))). % 8.77/2.95 tff(c_1476, plain, (![V_4]: (~entity(skc8, V_4) | ~event(skc10, V_4)))). % 8.77/2.95 tff(c_1450, plain, (![V_536]: (~eventuality(skc10, V_536) | ~entity(skc8, V_536)))). % 8.77/2.95 tff(c_1438, plain, (![V_535]: (~male(skc10, V_535) | ~eventuality(skc8, V_535)))). % 8.77/2.95 tff(c_1437, plain, (![V_535]: (~female(skc10, V_535) | ~eventuality(skc8, V_535)))). % 8.77/2.95 tff(c_1426, plain, (![V_533]: (existent(skc10, V_533) | ~entity(skc8, V_533)))). % 8.77/2.95 tff(c_1422, plain, (![V_530]: (unisex(skc10, V_530) | ~eventuality(skc8, V_530)))). % 8.77/2.95 tff(c_613, plain, (![V_346, V_46, U_45]: (existent(V_346, V_46) | ~accessible_world(U_45, V_346) | ~entity(U_45, V_46)))). % 8.77/2.95 tff(c_917, plain, (![V_422, V_14, U_13]: (unisex(V_422, V_14) | ~accessible_world(U_13, V_422) | ~eventuality(U_13, V_14)))). % 8.77/2.95 tff(c_1375, plain, (![V_16]: (~abstraction(skc8, V_16) | ~desire_want(skc10, V_16)))). % 8.77/2.95 tff(c_1376, plain, (![V_2]: (~abstraction(skc8, V_2) | ~dance(skc10, V_2)))). % 8.77/2.95 tff(c_1353, plain, (![V_524]: (abstraction(skc10, V_524) | ~forename(skc8, V_524)))). % 8.77/2.95 tff(c_1377, plain, (~abstraction(skc8, skc13))). % 8.77/2.95 tff(c_1333, plain, (![V_4]: (~abstraction(skc8, V_4) | ~event(skc10, V_4)))). % 8.77/2.96 tff(c_1345, plain, (![V_523]: (relation(skc10, V_523) | ~forename(skc8, V_523)))). % 8.77/2.96 tff(c_1337, plain, (![V_521]: (relname(skc10, V_521) | ~forename(skc8, V_521)))). % 8.77/2.96 tff(c_977, plain, (![V_447, V_30, U_29]: (relname(V_447, V_30) | ~accessible_world(U_29, V_447) | ~forename(U_29, V_30)))). % 8.77/2.96 tff(c_1308, plain, (![V_517]: (~eventuality(skc10, V_517) | ~abstraction(skc8, V_517)))). % 8.77/2.96 tff(c_1307, plain, (![V_517]: (~entity(skc10, V_517) | ~abstraction(skc8, V_517)))). % 8.77/2.96 tff(c_1292, plain, (![V_515]: (general(skc10, V_515) | ~abstraction(skc8, V_515)))). % 8.77/2.96 tff(c_478, plain, (![V_317, V_26, U_25]: (general(V_317, V_26) | ~accessible_world(U_25, V_317) | ~abstraction(U_25, V_26)))). % 8.77/2.96 tff(c_1269, plain, (![V_26]: (~entity(skc8, V_26) | ~abstraction(skc10, V_26)))). % 8.77/2.96 tff(c_1263, plain, (![V_511]: (~general(skc10, V_511) | ~entity(skc8, V_511)))). % 8.77/2.96 tff(c_1255, plain, (![V_509]: (specific(skc10, V_509) | ~entity(skc8, V_509)))). % 8.77/2.96 tff(c_340, plain, (![V_266, V_44, U_43]: (specific(V_266, V_44) | ~accessible_world(U_43, V_266) | ~entity(U_43, V_44)))). % 8.77/2.96 tff(c_1228, plain, (![V_16]: (~abstraction(skc10, V_16) | ~desire_want(skc8, V_16)))). % 8.77/2.96 tff(c_186, plain, (![V_190, U_189, W_191]: (~proposition(skc8, V_190) | ~theme(skc8, U_189, V_190) | ~accessible_world(skc8, V_190) | ~event(V_190, W_191) | ~agent(V_190, W_191, skc15) | ~present(V_190, W_191) | ~dance(V_190, W_191) | ~agent(skc8, U_189, skc15) | ~desire_want(skc8, U_189) | ~present(skc8, U_189)))). % 8.77/2.96 tff(c_1212, plain, (![V_502]: (~abstraction(skc10, V_502) | ~event(skc8, V_502)))). % 8.77/2.96 tff(c_1187, plain, (![V_500]: (eventuality(skc10, V_500) | ~event(skc8, V_500)))). % 8.77/2.96 tff(c_659, plain, (![V_358, V_4, U_3]: (eventuality(V_358, V_4) | ~accessible_world(U_3, V_358) | ~event(U_3, V_4)))). % 8.77/2.96 tff(c_1176, plain, (![V_497]: (~abstraction(skc10, V_497) | ~dance(skc8, V_497)))). % 8.77/2.96 tff(c_1142, plain, (![V_490]: (event(skc10, V_490) | ~dance(skc8, V_490)))). % 8.77/2.96 tff(c_146, plain, (![Y_187, U_185, X_186, V_188, W_184]: (X_186=W_184 | ~theme(U_185, Y_187, X_186) | ~desire_want(U_185, Y_187) | ~proposition(U_185, X_186) | ~proposition(U_185, W_184) | ~desire_want(U_185, V_188) | ~theme(U_185, V_188, W_184)))). % 8.77/2.96 tff(c_421, plain, (![V_293, V_2, U_1]: (event(V_293, V_2) | ~accessible_world(U_1, V_293) | ~dance(U_1, V_2)))). % 8.77/2.96 tff(c_1058, plain, (![V_474]: (agent(V_474, skc13, skc12) | ~accessible_world(skc10, V_474)))). % 8.77/2.96 tff(c_1031, plain, (![V_467]: (of(V_467, skc14, skc15) | ~accessible_world(skc8, V_467)))). % 8.77/2.96 tff(c_144, plain, (![W_182, V_181, U_180, X_183]: (W_182=V_181 | ~entity(U_180, X_183) | ~of(U_180, V_181, X_183) | ~forename(U_180, W_182) | ~of(U_180, W_182, X_183) | ~forename(U_180, V_181)))). % 8.77/2.96 tff(c_1032, plain, (![V_467]: (of(V_467, skc11, skc12) | ~accessible_world(skc8, V_467)))). % 8.77/2.96 tff(c_1059, plain, (![V_474]: (agent(V_474, skc9, skc12) | ~accessible_world(skc8, V_474)))). % 8.77/2.96 tff(c_1075, plain, (![V_2]: (~entity(skc10, V_2) | ~dance(skc8, V_2)))). % 8.77/2.96 tff(c_1074, plain, (![V_16]: (~entity(skc10, V_16) | ~desire_want(skc8, V_16)))). % 8.77/2.96 tff(c_1052, plain, (![V_4]: (~entity(skc10, V_4) | ~event(skc8, V_4)))). % 8.77/2.96 tff(c_138, plain, (![V_169, W_170, X_171, U_168]: (agent(V_169, W_170, X_171) | ~agent(U_168, W_170, X_171) | ~accessible_world(U_168, V_169)))). % 8.77/2.96 tff(c_1046, plain, (![V_46]: (~eventuality(skc8, V_46) | ~entity(skc10, V_46)))). % 8.77/2.96 tff(c_1040, plain, (![V_471]: (~existent(skc10, V_471) | ~eventuality(skc8, V_471)))). % 8.77/2.96 tff(c_1025, plain, (![V_465]: (nonexistent(skc10, V_465) | ~eventuality(skc8, V_465)))). % 8.77/2.96 tff(c_142, plain, (![V_177, W_178, X_179, U_176]: (of(V_177, W_178, X_179) | ~of(U_176, W_178, X_179) | ~accessible_world(U_176, V_177)))). % 8.77/2.96 tff(c_981, plain, (![V_450, V_12, U_11]: (nonexistent(V_450, V_12) | ~accessible_world(U_11, V_450) | ~eventuality(U_11, V_12)))). % 8.77/2.96 tff(c_989, plain, (![V_456]: (theme(V_456, skc9, skc10) | ~accessible_world(skc8, V_456)))). % 8.77/2.96 tff(c_1001, plain, (![V_460]: (~male(skc10, V_460) | ~abstraction(skc8, V_460)))). % 8.77/2.96 tff(c_1000, plain, (![V_460]: (~female(skc10, V_460) | ~abstraction(skc8, V_460)))). % 8.77/2.96 tff(c_985, plain, (![V_454]: (unisex(skc10, V_454) | ~abstraction(skc8, V_454)))). % 8.77/2.96 tff(c_140, plain, (![V_173, W_174, X_175, U_172]: (theme(V_173, W_174, X_175) | ~theme(U_172, W_174, X_175) | ~accessible_world(U_172, V_173)))). % 8.77/2.96 tff(c_918, plain, (![V_422, V_28, U_27]: (unisex(V_422, V_28) | ~accessible_world(U_27, V_422) | ~abstraction(U_27, V_28)))). % 8.77/2.96 tff(c_88, plain, (![V_94, W_95, U_93]: (nonexistent(V_94, W_95) | ~nonexistent(U_93, W_95) | ~accessible_world(U_93, V_94)))). % 8.77/2.96 tff(c_108, plain, (![V_124, W_125, U_123]: (relname(V_124, W_125) | ~relname(U_123, W_125) | ~accessible_world(U_123, V_124)))). % 8.77/2.96 tff(c_98, plain, (![V_109, W_110, U_108]: (relation(V_109, W_110) | ~relation(U_108, W_110) | ~accessible_world(U_108, V_109)))). % 8.77/2.96 tff(c_102, plain, (![V_115, W_116, U_114]: (nonhuman(V_115, W_116) | ~nonhuman(U_114, W_116) | ~accessible_world(U_114, V_115)))). % 8.77/2.96 tff(c_118, plain, (![V_139, W_140, U_138]: (entity(V_139, W_140) | ~entity(U_138, W_140) | ~accessible_world(U_138, V_139)))). % 8.77/2.96 tff(c_827, plain, (![U_15]: (~accessible_world(skc8, U_15) | ~desire_want(U_15, skc12)))). % 8.77/2.96 tff(c_940, plain, (![V_433]: (dance(V_433, skc13) | ~accessible_world(skc10, V_433)))). % 8.77/2.96 tff(c_76, plain, (![V_76, W_77, U_75]: (dance(V_76, W_77) | ~dance(U_75, W_77) | ~accessible_world(U_75, V_76)))). % 8.77/2.96 tff(c_928, plain, (![V_428]: (present(V_428, skc9) | ~accessible_world(skc8, V_428)))). % 8.77/2.96 tff(c_927, plain, (![V_428]: (present(V_428, skc13) | ~accessible_world(skc10, V_428)))). % 8.77/2.96 tff(c_92, plain, (![V_100, W_101, U_99]: (present(V_100, W_101) | ~present(U_99, W_101) | ~accessible_world(U_99, V_100)))). % 8.77/2.96 tff(c_751, plain, (![V_380]: (abstraction(V_380, skc11) | ~accessible_world(skc10, V_380)))). % 8.77/2.96 tff(c_752, plain, (![V_380]: (abstraction(V_380, skc14) | ~accessible_world(skc10, V_380)))). % 8.77/2.96 tff(c_877, plain, (![U_15]: (~accessible_world(skc8, U_15) | ~desire_want(U_15, skc15)))). % 8.77/2.96 tff(c_90, plain, (![V_97, W_98, U_96]: (unisex(V_97, W_98) | ~unisex(U_96, W_98) | ~accessible_world(U_96, V_97)))). % 8.77/2.96 tff(c_893, plain, (![V_334]: (~dance(V_334, skc15) | ~accessible_world(skc8, V_334)))). % 8.77/2.96 tff(c_910, plain, (~abstraction(skc10, skc9))). % 8.77/2.96 tff(c_845, plain, (![V_404]: (~abstraction(V_404, skc9) | ~accessible_world(skc8, V_404)))). % 8.77/2.96 tff(c_136, plain, (![V_166, W_167, U_165]: (male(V_166, W_167) | ~male(U_165, W_167) | ~accessible_world(U_165, V_166)))). % 8.77/2.96 tff(c_894, plain, (![V_336]: (~dance(V_336, skc12) | ~accessible_world(skc8, V_336)))). % 8.77/2.96 tff(c_787, plain, (![V_293]: (~entity(V_293, skc13) | ~accessible_world(skc10, V_293)))). % 8.77/2.96 tff(c_789, plain, (![U_1, V_2]: (~entity(U_1, V_2) | ~dance(U_1, V_2)))). % 8.77/2.96 tff(c_734, plain, (![V_293]: (~abstraction(V_293, skc13) | ~accessible_world(skc10, V_293)))). % 8.77/2.96 tff(c_703, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc15)))). % 8.77/2.96 tff(c_116, plain, (![V_136, W_137, U_135]: (organism(V_136, W_137) | ~organism(U_135, W_137) | ~accessible_world(U_135, V_136)))). % 8.77/2.96 tff(c_788, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~desire_want(U_15, V_16)))). % 8.77/2.96 tff(c_755, plain, (![V_380]: (abstraction(V_380, skc10) | ~accessible_world(skc10, V_380)))). % 8.77/2.96 tff(c_837, plain, (![V_401]: (desire_want(V_401, skc9) | ~accessible_world(skc8, V_401)))). % 8.77/2.96 tff(c_94, plain, (![V_103, W_104, U_102]: (desire_want(V_103, W_104) | ~desire_want(U_102, W_104) | ~accessible_world(U_102, V_103)))). % 8.77/2.96 tff(c_833, plain, (~abstraction(skc8, skc9))). % 8.77/2.96 tff(c_735, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~desire_want(U_15, V_16)))). % 8.77/2.96 tff(c_808, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc12)))). % 8.77/2.96 tff(c_736, plain, (![U_1, V_2]: (~abstraction(U_1, V_2) | ~dance(U_1, V_2)))). % 8.77/2.96 tff(c_124, plain, (![V_148, W_149, U_147]: (living(V_148, W_149) | ~living(U_147, W_149) | ~accessible_world(U_147, V_148)))). % 8.77/2.96 tff(c_555, plain, (![V_335]: (~eventuality(V_335, skc12) | ~accessible_world(skc8, V_335)))). % 8.77/2.96 tff(c_794, plain, (![V_388]: (vincent_forename(V_388, skc14) | ~accessible_world(skc8, V_388)))). % 8.77/2.96 tff(c_790, plain, (~entity(skc10, skc13))). % 8.77/2.96 tff(c_132, plain, (![V_160, W_161, U_159]: (vincent_forename(V_160, W_161) | ~vincent_forename(U_159, W_161) | ~accessible_world(U_159, V_160)))). % 8.77/2.96 tff(c_576, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 8.77/2.96 tff(c_604, plain, (![V_344]: (~female(V_344, skc15) | ~accessible_world(skc8, V_344)))). % 8.77/2.96 tff(c_720, plain, (![V_375]: (human(V_375, skc15) | ~accessible_world(skc8, V_375)))). % 8.77/2.96 tff(c_719, plain, (![V_375]: (human(V_375, skc12) | ~accessible_world(skc8, V_375)))). % 8.77/2.96 tff(c_100, plain, (![V_112, W_113, U_111]: (abstraction(V_112, W_113) | ~abstraction(U_111, W_113) | ~accessible_world(U_111, V_112)))). % 8.77/2.96 tff(c_737, plain, (~abstraction(skc10, skc13))). % 8.77/2.96 tff(c_591, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 8.77/2.96 tff(c_126, plain, (![V_151, W_152, U_150]: (human(V_151, W_152) | ~human(U_150, W_152) | ~accessible_world(U_150, V_151)))). % 8.77/2.97 tff(c_543, plain, (![V_334]: (entity(V_334, skc15) | ~accessible_world(skc8, V_334)))). % 8.77/2.97 tff(c_568, plain, (![V_336]: (entity(V_336, skc12) | ~accessible_world(skc8, V_336)))). % 8.77/2.97 tff(c_602, plain, (![V_344]: (~eventuality(V_344, skc15) | ~accessible_world(skc8, V_344)))). % 8.77/2.97 tff(c_689, plain, (![V_368]: (mia_forename(V_368, skc11) | ~accessible_world(skc8, V_368)))). % 8.77/2.97 tff(c_110, plain, (![V_127, W_128, U_126]: (mia_forename(V_127, W_128) | ~mia_forename(U_126, W_128) | ~accessible_world(U_126, V_127)))). % 8.77/2.97 tff(c_685, plain, (abstraction(skc10, skc11))). % 8.77/2.97 tff(c_637, plain, (![V_298]: (abstraction(V_298, skc11) | ~accessible_world(skc8, V_298)))). % 8.77/2.97 tff(c_673, plain, (abstraction(skc10, skc14))). % 8.77/2.97 tff(c_130, plain, (![V_157, W_158, U_156]: (female(V_157, W_158) | ~female(U_156, W_158) | ~accessible_world(U_156, V_157)))). % 8.77/2.97 tff(c_636, plain, (![V_298]: (abstraction(V_298, skc14) | ~accessible_world(skc8, V_298)))). % 8.77/2.97 tff(c_645, plain, (![V_353]: (animate(V_353, skc12) | ~accessible_world(skc8, V_353)))). % 8.77/2.97 tff(c_664, plain, (~abstraction(skc10, skc15))). % 8.77/2.97 tff(c_603, plain, (![V_344]: (~abstraction(V_344, skc15) | ~accessible_world(skc8, V_344)))). % 8.77/2.97 tff(c_655, plain, (~abstraction(skc10, skc12))). % 8.77/2.97 tff(c_80, plain, (![V_82, W_83, U_81]: (eventuality(V_82, W_83) | ~eventuality(U_81, W_83) | ~accessible_world(U_81, V_82)))). % 8.77/2.97 tff(c_554, plain, (![V_335]: (~abstraction(V_335, skc12) | ~accessible_world(skc8, V_335)))). % 8.77/2.97 tff(c_646, plain, (![V_353]: (animate(V_353, skc15) | ~accessible_world(skc8, V_353)))). % 8.77/2.97 tff(c_639, plain, (abstraction(skc8, skc11))). % 8.77/2.97 tff(c_128, plain, (![V_154, W_155, U_153]: (animate(V_154, W_155) | ~animate(U_153, W_155) | ~accessible_world(U_153, V_154)))). % 8.77/2.97 tff(c_638, plain, (abstraction(skc8, skc14))). % 8.77/2.97 tff(c_368, plain, (![U_276, V_277]: (abstraction(U_276, V_277) | ~forename(U_276, V_277)))). % 8.77/2.97 tff(c_449, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~abstraction(U_25, V_26)))). % 8.77/2.97 tff(c_609, plain, (abstraction(skc10, skc10))). % 8.77/2.97 tff(c_120, plain, (![V_142, W_143, U_141]: (existent(V_142, W_143) | ~existent(U_141, W_143) | ~accessible_world(U_141, V_142)))). % 8.77/2.97 tff(c_394, plain, (![V_280]: (abstraction(V_280, skc10) | ~accessible_world(skc8, V_280)))). % 8.77/2.97 tff(c_489, plain, (![V_320]: (male(V_320, skc15) | ~accessible_world(skc8, V_320)))). % 8.77/2.97 tff(c_345, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~abstraction(U_25, V_26)))). % 8.77/2.97 tff(c_84, plain, (![V_88, W_89, U_87]: (singleton(V_88, W_89) | ~singleton(U_87, W_89) | ~accessible_world(U_87, V_88)))). % 8.77/2.97 tff(c_427, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 8.77/2.97 tff(c_519, plain, (![V_330]: (human_person(V_330, skc12) | ~accessible_world(skc8, V_330)))). % 8.77/2.97 tff(c_520, plain, (![V_330]: (female(V_330, skc12) | ~accessible_world(skc8, V_330)))). % 8.77/2.97 tff(c_490, plain, (![V_320]: (human_person(V_320, skc15) | ~accessible_world(skc8, V_320)))). % 8.77/2.97 tff(c_82, plain, (![V_85, W_86, U_84]: (thing(V_85, W_86) | ~thing(U_84, W_86) | ~accessible_world(U_84, V_85)))). % 8.77/2.97 tff(c_499, plain, (![V_324]: (woman(V_324, skc12) | ~accessible_world(skc8, V_324)))). % 8.77/2.97 tff(c_256, plain, (![U_234, V_235]: (~female(U_234, V_235) | ~abstraction(U_234, V_235)))). % 8.77/2.97 tff(c_433, plain, (![V_298]: (forename(V_298, skc14) | ~accessible_world(skc8, V_298)))). % 8.77/2.97 tff(c_112, plain, (![V_130, W_131, U_129]: (woman(V_130, W_131) | ~woman(U_129, W_131) | ~accessible_world(U_129, V_130)))). % 8.77/2.97 tff(c_422, plain, (![V_293]: (event(V_293, skc13) | ~accessible_world(skc10, V_293)))). % 8.77/2.97 tff(c_286, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 8.77/2.97 tff(c_386, plain, (![V_286]: (man(V_286, skc15) | ~accessible_world(skc8, V_286)))). % 8.77/2.97 tff(c_474, plain, (entity(skc8, skc15))). % 8.77/2.97 tff(c_473, plain, (entity(skc8, skc12))). % 8.77/2.97 tff(c_104, plain, (![V_118, W_119, U_117]: (general(V_118, W_119) | ~general(U_117, W_119) | ~accessible_world(U_117, V_118)))). % 8.77/2.97 tff(c_243, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~human_person(U_37, V_38)))). % 8.77/2.97 tff(c_434, plain, (![V_298]: (forename(V_298, skc11) | ~accessible_world(skc8, V_298)))). % 8.77/2.97 tff(c_288, plain, (![U_41, V_42]: (singleton(U_41, V_42) | ~entity(U_41, V_42)))). % 8.77/2.97 tff(c_114, plain, (![V_133, W_134, U_132]: (human_person(V_133, W_134) | ~human_person(U_132, W_134) | ~accessible_world(U_132, V_133)))). % 8.77/2.97 tff(c_206, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~human_person(U_37, V_38)))). % 8.77/2.97 tff(c_226, plain, (![U_43, V_44]: (~general(U_43, V_44) | ~entity(U_43, V_44)))). % 8.77/2.97 tff(c_287, plain, (![U_21, V_22]: (singleton(U_21, V_22) | ~abstraction(U_21, V_22)))). % 8.77/2.97 tff(c_442, plain, (~abstraction(skc8, skc12))). % 8.77/2.97 tff(c_275, plain, (![U_238, V_239]: (~human(U_238, V_239) | ~abstraction(U_238, V_239)))). % 8.77/2.97 tff(c_106, plain, (![V_121, W_122, U_120]: (forename(V_121, W_122) | ~forename(U_120, W_122) | ~accessible_world(U_120, V_121)))). % 8.77/2.97 tff(c_327, plain, (![U_260, V_261]: (~existent(U_260, V_261) | ~eventuality(U_260, V_261)))). % 8.77/2.97 tff(c_412, plain, (~dance(skc8, skc15))). % 8.77/2.97 tff(c_411, plain, (~desire_want(skc8, skc15))). % 8.77/2.97 tff(c_78, plain, (![V_79, W_80, U_78]: (event(V_79, W_80) | ~event(U_78, W_80) | ~accessible_world(U_78, V_79)))). % 8.77/2.97 tff(c_404, plain, (~event(skc8, skc15))). % 8.77/2.97 tff(c_400, plain, (~eventuality(skc8, skc15))). % 8.77/2.97 tff(c_316, plain, (![U_254, V_255]: (~male(U_254, V_255) | ~eventuality(U_254, V_255)))). % 8.77/2.97 tff(c_395, plain, (abstraction(skc8, skc10))). % 8.77/2.97 tff(c_322, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~proposition(U_17, V_18)))). % 8.77/2.97 tff(c_134, plain, (![V_163, W_164, U_162]: (man(V_163, W_164) | ~man(U_162, W_164) | ~accessible_world(U_162, V_163)))). % 8.77/2.97 tff(c_373, plain, (![V_280]: (proposition(V_280, skc10) | ~accessible_world(skc8, V_280)))). % 8.77/2.97 tff(c_378, plain, (~abstraction(skc8, skc15))). % 8.77/2.97 tff(c_257, plain, (![U_234, V_235]: (~male(U_234, V_235) | ~abstraction(U_234, V_235)))). % 8.77/2.97 tff(c_96, plain, (![V_106, W_107, U_105]: (proposition(V_106, W_107) | ~proposition(U_105, W_107) | ~accessible_world(U_105, V_106)))). % 8.77/2.97 tff(c_211, plain, (![U_37, V_38]: (living(U_37, V_38) | ~human_person(U_37, V_38)))). % 8.77/2.97 tff(c_304, plain, (![U_29, V_30]: (relation(U_29, V_30) | ~forename(U_29, V_30)))). % 8.77/2.97 tff(c_363, plain, (~dance(skc8, skc12))). % 8.77/2.97 tff(c_362, plain, (~desire_want(skc8, skc12))). % 8.77/2.97 tff(c_354, plain, (~event(skc8, skc12))). % 8.77/2.97 tff(c_122, plain, (![V_145, W_146, U_144]: (impartial(V_145, W_146) | ~impartial(U_144, W_146) | ~accessible_world(U_144, V_145)))). % 8.77/2.97 tff(c_350, plain, (~eventuality(skc8, skc12))). % 8.77/2.97 tff(c_315, plain, (![U_254, V_255]: (~female(U_254, V_255) | ~eventuality(U_254, V_255)))). % 8.77/2.97 tff(c_332, plain, (![U_262, V_263]: (~general(U_262, V_263) | ~eventuality(U_262, V_263)))). % 8.77/2.97 tff(c_86, plain, (![V_91, W_92, U_90]: (specific(V_91, W_92) | ~specific(U_90, W_92) | ~accessible_world(U_90, V_91)))). % 8.77/2.97 tff(c_26, plain, (![U_25, V_26]: (general(U_25, V_26) | ~abstraction(U_25, V_26)))). % 8.77/2.97 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 8.77/2.97 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 8.77/2.97 tff(c_20, plain, (![U_19, V_20]: (abstraction(U_19, V_20) | ~relation(U_19, V_20)))). % 8.77/2.97 tff(c_16, plain, (![U_15, V_16]: (event(U_15, V_16) | ~desire_want(U_15, V_16)))). % 8.77/2.97 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 8.77/2.97 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 8.77/2.97 tff(c_18, plain, (![U_17, V_18]: (relation(U_17, V_18) | ~proposition(U_17, V_18)))). % 8.77/2.97 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~dance(U_1, V_2)))). % 8.77/2.97 tff(c_32, plain, (![U_31, V_32]: (relation(U_31, V_32) | ~relname(U_31, V_32)))). % 8.77/2.97 tff(c_34, plain, (![U_33, V_34]: (forename(U_33, V_34) | ~mia_forename(U_33, V_34)))). % 8.77/2.97 tff(c_293, plain, (~female(skc8, skc15))). % 8.77/2.97 tff(c_72, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~female(U_71, V_72)))). % 8.77/2.97 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 8.77/2.97 tff(c_270, plain, (human(skc8, skc12))). % 8.77/2.97 tff(c_24, plain, (![U_23, V_24]: (nonhuman(U_23, V_24) | ~abstraction(U_23, V_24)))). % 8.77/2.97 tff(c_269, plain, (animate(skc8, skc12))). % 8.77/2.97 tff(c_262, plain, (human_person(skc8, skc12))). % 8.77/2.97 tff(c_36, plain, (![U_35, V_36]: (human_person(U_35, V_36) | ~woman(U_35, V_36)))). % 8.77/2.97 tff(c_28, plain, (![U_27, V_28]: (unisex(U_27, V_28) | ~abstraction(U_27, V_28)))). % 8.77/2.97 tff(c_70, plain, (![U_69, V_70]: (~nonhuman(U_69, V_70) | ~human(U_69, V_70)))). % 8.77/2.97 tff(c_74, plain, (![U_73, V_74]: (~existent(U_73, V_74) | ~nonexistent(U_73, V_74)))). % 8.77/2.97 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 8.77/2.97 tff(c_66, plain, (![U_65, V_66]: (~unisex(U_65, V_66) | ~female(U_65, V_66)))). % 8.77/2.97 tff(c_22, plain, (![U_21, V_22]: (thing(U_21, V_22) | ~abstraction(U_21, V_22)))). % 8.77/2.97 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~organism(U_39, V_40)))). % 8.77/2.97 tff(c_64, plain, (![U_63, V_64]: (~unisex(U_63, V_64) | ~male(U_63, V_64)))). % 8.77/2.97 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 8.77/2.98 tff(c_236, plain, (female(skc8, skc12))). % 8.77/2.98 tff(c_56, plain, (![U_55, V_56]: (female(U_55, V_56) | ~woman(U_55, V_56)))). % 8.77/2.98 tff(c_231, plain, (male(skc8, skc15))). % 8.77/2.98 tff(c_62, plain, (![U_61, V_62]: (male(U_61, V_62) | ~man(U_61, V_62)))). % 8.77/2.98 tff(c_68, plain, (![U_67, V_68]: (~specific(U_67, V_68) | ~general(U_67, V_68)))). % 8.77/2.98 tff(c_221, plain, (animate(skc8, skc15))). % 8.77/2.98 tff(c_216, plain, (human(skc8, skc15))). % 8.77/2.98 tff(c_54, plain, (![U_53, V_54]: (animate(U_53, V_54) | ~human_person(U_53, V_54)))). % 8.77/2.98 tff(c_52, plain, (![U_51, V_52]: (human(U_51, V_52) | ~human_person(U_51, V_52)))). % 8.77/2.98 tff(c_50, plain, (![U_49, V_50]: (living(U_49, V_50) | ~organism(U_49, V_50)))). % 8.77/2.98 tff(c_48, plain, (![U_47, V_48]: (impartial(U_47, V_48) | ~organism(U_47, V_48)))). % 8.77/2.98 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 8.77/2.98 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 8.77/2.98 tff(c_194, plain, (human_person(skc8, skc15))). % 8.77/2.98 tff(c_60, plain, (![U_59, V_60]: (human_person(U_59, V_60) | ~man(U_59, V_60)))). % 8.77/2.98 tff(c_30, plain, (![U_29, V_30]: (relname(U_29, V_30) | ~forename(U_29, V_30)))). % 8.77/2.98 tff(c_38, plain, (![U_37, V_38]: (organism(U_37, V_38) | ~human_person(U_37, V_38)))). % 8.77/2.98 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 8.77/2.98 tff(c_176, plain, (of(skc8, skc14, skc15))). % 8.77/2.98 tff(c_184, plain, (theme(skc8, skc9, skc10))). % 8.77/2.98 tff(c_182, plain, (agent(skc10, skc13, skc12))). % 8.77/2.98 tff(c_178, plain, (of(skc8, skc11, skc12))). % 8.77/2.98 tff(c_180, plain, (agent(skc8, skc9, skc12))). % 8.77/2.98 tff(c_164, plain, (proposition(skc8, skc10))). % 8.77/2.98 tff(c_166, plain, (accessible_world(skc8, skc10))). % 8.77/2.98 tff(c_168, plain, (desire_want(skc8, skc9))). % 8.77/2.98 tff(c_172, plain, (forename(skc8, skc14))). % 8.77/2.98 tff(c_162, plain, (mia_forename(skc8, skc11))). % 8.77/2.98 tff(c_160, plain, (forename(skc8, skc11))). % 8.77/2.98 tff(c_150, plain, (man(skc8, skc15))). % 8.77/2.98 tff(c_158, plain, (dance(skc10, skc13))). % 8.77/2.98 tff(c_152, plain, (event(skc10, skc13))). % 8.77/2.98 tff(c_154, plain, (woman(skc8, skc12))). % 8.77/2.98 tff(c_156, plain, (present(skc10, skc13))). % 8.77/2.98 tff(c_170, plain, (present(skc8, skc9))). % 8.77/2.98 tff(c_174, plain, (vincent_forename(skc8, skc14))). % 8.77/2.98 tff(c_148, plain, (actual_world(skc8))). % 8.77/2.98 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.77/2.98 %------------------------------------------------------------------------------