%------------------------------------------------------------------------------
% 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 : n015.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 : CounterSatisfiable 8.77s 2.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP024+1 : TPTP v9.0.0. Released v2.4.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n015.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 08:10:05 EDT 2025
% 0.13/0.34 % CPUTime :
% 8.77/2.99
% 8.77/2.99 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.77/2.99
% 8.77/2.99 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.77/3.00 %$ 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 > #skF_7 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_8 > #skF_4
% 8.77/3.00
% 8.77/3.00 %Foreground sorts:
% 8.77/3.00
% 8.77/3.00
% 8.77/3.00 %Background operators:
% 8.77/3.00
% 8.77/3.00
% 8.77/3.00 %Foreground operators:
% 8.77/3.00 tff(relation, type, relation: ($i * $i) > $o).
% 8.77/3.00 tff(forename, type, forename: ($i * $i) > $o).
% 8.77/3.00 tff(female, type, female: ($i * $i) > $o).
% 8.77/3.00 tff(theme, type, theme: ($i * $i * $i) > $o).
% 8.77/3.00 tff(living, type, living: ($i * $i) > $o).
% 8.77/3.00 tff(human_person, type, human_person: ($i * $i) > $o).
% 8.77/3.00 tff(present, type, present: ($i * $i) > $o).
% 8.77/3.00 tff(entity, type, entity: ($i * $i) > $o).
% 8.77/3.00 tff(eventuality, type, eventuality: ($i * $i) > $o).
% 8.77/3.00 tff(existent, type, existent: ($i * $i) > $o).
% 8.77/3.00 tff(abstraction, type, abstraction: ($i * $i) > $o).
% 8.77/3.00 tff(proposition, type, proposition: ($i * $i) > $o).
% 8.77/3.00 tff(relname, type, relname: ($i * $i) > $o).
% 8.77/3.00 tff(singleton, type, singleton: ($i * $i) > $o).
% 8.77/3.00 tff(male, type, male: ($i * $i) > $o).
% 8.77/3.00 tff(organism, type, organism: ($i * $i) > $o).
% 8.77/3.00 tff(animate, type, animate: ($i * $i) > $o).
% 8.77/3.00 tff(of, type, of: ($i * $i * $i) > $o).
% 8.77/3.00 tff('#skF_7', type, '#skF_7': $i).
% 8.77/3.00 tff(actual_world, type, actual_world: $i > $o).
% 8.77/3.00 tff(agent, type, agent: ($i * $i * $i) > $o).
% 8.77/3.00 tff('#skF_5', type, '#skF_5': $i).
% 8.77/3.00 tff(general, type, general: ($i * $i) > $o).
% 8.77/3.00 tff('#skF_6', type, '#skF_6': $i).
% 8.77/3.00 tff(nonhuman, type, nonhuman: ($i * $i) > $o).
% 8.77/3.00 tff('#skF_2', type, '#skF_2': $i).
% 8.77/3.00 tff('#skF_3', type, '#skF_3': $i).
% 8.77/3.00 tff(event, type, event: ($i * $i) > $o).
% 8.77/3.00 tff('#skF_1', type, '#skF_1': $i).
% 8.77/3.00 tff(woman, type, woman: ($i * $i) > $o).
% 8.77/3.00 tff(nonexistent, type, nonexistent: ($i * $i) > $o).
% 8.77/3.00 tff(thing, type, thing: ($i * $i) > $o).
% 8.77/3.00 tff(dance, type, dance: ($i * $i) > $o).
% 8.77/3.00 tff(desire_want, type, desire_want: ($i * $i) > $o).
% 8.77/3.00 tff('#skF_8', type, '#skF_8': $i).
% 8.77/3.00 tff(human, type, human: ($i * $i) > $o).
% 8.77/3.00 tff(man, type, man: ($i * $i) > $o).
% 8.77/3.00 tff('#skF_4', type, '#skF_4': $i).
% 8.77/3.00 tff(unisex, type, unisex: ($i * $i) > $o).
% 8.77/3.00 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o).
% 8.77/3.00 tff(impartial, type, impartial: ($i * $i) > $o).
% 8.77/3.00 tff(accessible_world, type, accessible_world: ($i * $i) > $o).
% 8.77/3.00 tff(specific, type, specific: ($i * $i) > $o).
% 8.77/3.00 tff(mia_forename, type, mia_forename: ($i * $i) > $o).
% 8.77/3.00
% 8.77/3.00 %Saturated clause set:
% 8.77/3.01 tff(c_2425, plain, (![W_138, V_723, W_722]: (relation(W_138, V_723) | ~accessible_world(W_722, W_138) | ~accessible_world('#skF_6', W_722) | ~forename('#skF_1', V_723)))).
% 8.77/3.01 tff(c_2559, plain, (![W_167, V_738, W_737]: (singleton(W_167, V_738) | ~accessible_world(W_737, W_167) | ~accessible_world('#skF_6', W_737) | ~eventuality('#skF_1', V_738)))).
% 8.77/3.01 tff(c_2695, plain, (![W_167, V_764, W_763]: (singleton(W_167, V_764) | ~accessible_world(W_763, W_167) | ~accessible_world('#skF_6', W_763) | ~abstraction('#skF_1', V_764)))).
% 8.77/3.01 tff(c_2363, plain, (![W_167, V_715, W_714]: (singleton(W_167, V_715) | ~accessible_world(W_714, W_167) | ~accessible_world('#skF_6', W_714) | ~entity('#skF_1', V_715)))).
% 8.77/3.01 tff(c_2687, plain, (![W_99, V_760, W_759]: (living(W_99, V_760) | ~accessible_world(W_759, W_99) | ~accessible_world('#skF_6', W_759) | ~human_person('#skF_1', V_760)))).
% 8.77/3.01 tff(c_2639, plain, (![W_102, V_748, W_747]: (impartial(W_102, V_748) | ~accessible_world(W_747, W_102) | ~accessible_world('#skF_6', W_747) | ~human_person('#skF_1', V_748)))).
% 8.77/3.01 tff(c_2023, plain, (![W_164, V_665, W_664]: (specific(W_164, V_665) | ~accessible_world(W_664, W_164) | ~accessible_world('#skF_6', W_664) | ~eventuality('#skF_1', V_665)))).
% 8.77/3.01 tff(c_2109, plain, (![W_132, V_677, W_676]: (nonhuman(W_132, V_677) | ~accessible_world(W_676, W_132) | ~accessible_world('#skF_6', W_676) | ~abstraction('#skF_1', V_677)))).
% 8.77/3.01 tff(c_2117, plain, (![W_170, V_679, W_678]: (thing(W_170, V_679) | ~accessible_world(W_678, W_170) | ~accessible_world('#skF_6', W_678) | ~eventuality('#skF_1', V_679)))).
% 8.77/3.01 tff(c_2069, plain, (![W_176, V_667, W_666]: (event(W_176, V_667) | ~accessible_world(W_666, W_176) | ~accessible_world('#skF_6', W_666) | ~dance('#skF_1', V_667)))).
% 8.77/3.01 tff(c_2215, plain, (![W_161, V_691, W_690]: (nonexistent(W_161, V_691) | ~accessible_world(W_690, W_161) | ~accessible_world('#skF_6', W_690) | ~eventuality('#skF_1', V_691)))).
% 8.77/3.01 tff(c_2101, plain, (![W_164, V_675, W_674]: (specific(W_164, V_675) | ~accessible_world(W_674, W_164) | ~accessible_world('#skF_6', W_674) | ~entity('#skF_1', V_675)))).
% 8.77/3.01 tff(c_2128, plain, (![W_158, V_681, W_680]: (unisex(W_158, V_681) | ~accessible_world(W_680, W_158) | ~accessible_world('#skF_6', W_680) | ~abstraction('#skF_1', V_681)))).
% 8.77/3.01 tff(c_2143, plain, (![W_111, V_683, W_682]: (organism(W_111, V_683) | ~accessible_world(W_682, W_111) | ~accessible_world('#skF_6', W_682) | ~human_person('#skF_1', V_683)))).
% 8.77/3.01 tff(c_2301, plain, (![W_173, V_699, W_698]: (eventuality(W_173, V_699) | ~accessible_world(W_698, W_173) | ~accessible_world('#skF_6', W_698) | ~event('#skF_1', V_699)))).
% 8.77/3.01 tff(c_2240, plain, (![W_129, V_695, W_694]: (general(W_129, V_695) | ~accessible_world(W_694, W_129) | ~accessible_world('#skF_6', W_694) | ~abstraction('#skF_1', V_695)))).
% 8.77/3.01 tff(c_2254, plain, (![W_105, V_697, W_696]: (existent(W_105, V_697) | ~accessible_world(W_696, W_105) | ~accessible_world('#skF_6', W_696) | ~entity('#skF_1', V_697)))).
% 8.77/3.01 tff(c_2312, plain, (![W_170, V_701, W_700]: (thing(W_170, V_701) | ~accessible_world(W_700, W_170) | ~accessible_world('#skF_6', W_700) | ~entity('#skF_1', V_701)))).
% 8.77/3.01 tff(c_2203, plain, (![W_176, V_689, W_688]: (event(W_176, V_689) | ~accessible_world(W_688, W_176) | ~accessible_world('#skF_6', W_688) | ~desire_want('#skF_1', V_689)))).
% 8.77/3.01 tff(c_2323, plain, (![W_158, V_703, W_702]: (unisex(W_158, V_703) | ~accessible_world(W_702, W_158) | ~accessible_world('#skF_6', W_702) | ~eventuality('#skF_1', V_703)))).
% 8.77/3.01 tff(c_2849, plain, (![U_47, V_48]: (~accessible_world('#skF_6', U_47) | ~abstraction('#skF_1', V_48) | ~desire_want(U_47, V_48)))).
% 8.77/3.01 tff(c_1665, plain, (![W_108, W_582]: (entity(W_108, '#skF_2') | ~accessible_world(W_582, W_108) | ~accessible_world('#skF_6', W_582)))).
% 8.77/3.01 tff(c_2089, plain, (![W_170, V_671, W_670]: (thing(W_170, V_671) | ~accessible_world(W_670, W_170) | ~accessible_world('#skF_6', W_670) | ~abstraction('#skF_1', V_671)))).
% 8.77/3.01 tff(c_2882, plain, (![U_47, V_48]: (~accessible_world('#skF_6', U_47) | ~entity('#skF_1', V_48) | ~desire_want(U_47, V_48)))).
% 8.77/3.01 tff(c_2883, plain, (![U_61, V_62]: (~accessible_world('#skF_6', U_61) | ~entity('#skF_1', V_62) | ~dance(U_61, V_62)))).
% 8.77/3.01 tff(c_1629, plain, (![W_108, W_581]: (entity(W_108, '#skF_4') | ~accessible_world(W_581, W_108) | ~accessible_world('#skF_6', W_581)))).
% 8.77/3.01 tff(c_2153, plain, (![W_138, V_685, W_684]: (relation(W_138, V_685) | ~accessible_world(W_684, W_138) | ~accessible_world('#skF_6', W_684) | ~proposition('#skF_1', V_685)))).
% 8.77/3.01 tff(c_2850, plain, (![U_61, V_62]: (~accessible_world('#skF_6', U_61) | ~abstraction('#skF_1', V_62) | ~dance(U_61, V_62)))).
% 8.77/3.01 tff(c_2355, plain, (![U_59, V_60]: (~accessible_world('#skF_6', U_59) | ~entity('#skF_1', V_60) | ~event(U_59, V_60)))).
% 8.77/3.01 tff(c_2572, plain, (![U_59, V_60]: (~accessible_world('#skF_6', U_59) | ~abstraction('#skF_1', V_60) | ~event(U_59, V_60)))).
% 8.77/3.01 tff(c_2652, plain, (![U_37, V_38]: (~accessible_world('#skF_6', U_37) | ~eventuality('#skF_1', V_38) | ~abstraction(U_37, V_38)))).
% 8.77/3.01 tff(c_2669, plain, (![U_37, V_38]: (~accessible_world('#skF_6', U_37) | ~entity('#skF_1', V_38) | ~abstraction(U_37, V_38)))).
% 9.20/3.01 tff(c_2081, plain, (![W_123, V_669, W_668]: (relname(W_123, V_669) | ~accessible_world(W_668, W_123) | ~accessible_world('#skF_6', W_668) | ~forename('#skF_1', V_669)))).
% 9.20/3.01 tff(c_2426, plain, (![W_722, V_723]: (abstraction(W_722, V_723) | ~accessible_world('#skF_6', W_722) | ~forename('#skF_1', V_723)))).
% 9.20/3.01 tff(c_2683, plain, (![U_17, V_18]: (~accessible_world('#skF_6', U_17) | ~eventuality('#skF_1', V_18) | ~entity(U_17, V_18)))).
% 9.20/3.01 tff(c_913, plain, (![W_463, W_458]: (entity(W_463, '#skF_4') | ~accessible_world(W_458, W_463) | ~accessible_world('#skF_1', W_458)))).
% 9.20/3.01 tff(c_765, plain, (![W_93, W_421]: (animate(W_93, '#skF_2') | ~accessible_world(W_421, W_93) | ~accessible_world('#skF_1', W_421)))).
% 9.20/3.01 tff(c_761, plain, (![W_93, W_420]: (animate(W_93, '#skF_4') | ~accessible_world(W_420, W_93) | ~accessible_world('#skF_1', W_420)))).
% 9.20/3.01 tff(c_2071, plain, (![W_666, V_667]: (~abstraction(W_666, V_667) | ~accessible_world('#skF_6', W_666) | ~dance('#skF_1', V_667)))).
% 9.20/3.01 tff(c_2146, plain, (![W_682, V_683]: (entity(W_682, V_683) | ~accessible_world('#skF_6', W_682) | ~human_person('#skF_1', V_683)))).
% 9.20/3.01 tff(c_2325, plain, (![W_702, V_703]: (~male(W_702, V_703) | ~accessible_world('#skF_6', W_702) | ~eventuality('#skF_1', V_703)))).
% 9.20/3.01 tff(c_2072, plain, (![W_666, V_667]: (~entity(W_666, V_667) | ~accessible_world('#skF_6', W_666) | ~dance('#skF_1', V_667)))).
% 9.20/3.02 tff(c_2130, plain, (![W_680, V_681]: (~male(W_680, V_681) | ~accessible_world('#skF_6', W_680) | ~abstraction('#skF_1', V_681)))).
% 9.20/3.02 tff(c_2129, plain, (![W_680, V_681]: (~female(W_680, V_681) | ~accessible_world('#skF_6', W_680) | ~abstraction('#skF_1', V_681)))).
% 9.20/3.02 tff(c_1374, plain, (![W_167, V_554]: (singleton(W_167, V_554) | ~accessible_world('#skF_6', W_167) | ~abstraction('#skF_1', V_554)))).
% 9.20/3.02 tff(c_736, plain, (![W_96, W_414]: (human(W_96, '#skF_4') | ~accessible_world(W_414, W_96) | ~accessible_world('#skF_1', W_414)))).
% 9.20/3.02 tff(c_1448, plain, (![W_99, V_564]: (living(W_99, V_564) | ~accessible_world('#skF_6', W_99) | ~human_person('#skF_1', V_564)))).
% 9.20/3.02 tff(c_2216, plain, (![W_690, V_691]: (~existent(W_690, V_691) | ~accessible_world('#skF_6', W_690) | ~eventuality('#skF_1', V_691)))).
% 9.20/3.02 tff(c_2154, plain, (![W_684, V_685]: (abstraction(W_684, V_685) | ~accessible_world('#skF_6', W_684) | ~proposition('#skF_1', V_685)))).
% 9.20/3.02 tff(c_2102, plain, (![W_674, V_675]: (~general(W_674, V_675) | ~accessible_world('#skF_6', W_674) | ~entity('#skF_1', V_675)))).
% 9.20/3.02 tff(c_744, plain, (![W_96, W_415]: (human(W_96, '#skF_2') | ~accessible_world(W_415, W_96) | ~accessible_world('#skF_1', W_415)))).
% 9.20/3.02 tff(c_2024, plain, (![W_664, V_665]: (~general(W_664, V_665) | ~accessible_world('#skF_6', W_664) | ~eventuality('#skF_1', V_665)))).
% 9.20/3.03 tff(c_1452, plain, (![W_102, V_565]: (impartial(W_102, V_565) | ~accessible_world('#skF_6', W_102) | ~human_person('#skF_1', V_565)))).
% 9.20/3.03 tff(c_928, plain, (![W_108, W_466]: (entity(W_108, '#skF_2') | ~accessible_world(W_466, W_108) | ~accessible_world('#skF_1', W_466)))).
% 9.20/3.03 tff(c_2206, plain, (![W_688, V_689]: (~entity(W_688, V_689) | ~accessible_world('#skF_6', W_688) | ~desire_want('#skF_1', V_689)))).
% 9.20/3.03 tff(c_2303, plain, (![W_698, V_699]: (~entity(W_698, V_699) | ~accessible_world('#skF_6', W_698) | ~event('#skF_1', V_699)))).
% 9.20/3.03 tff(c_2241, plain, (![W_694, V_695]: (~eventuality(W_694, V_695) | ~accessible_world('#skF_6', W_694) | ~abstraction('#skF_1', V_695)))).
% 9.20/3.03 tff(c_2118, plain, (![W_678, V_679]: (singleton(W_678, V_679) | ~accessible_world('#skF_6', W_678) | ~eventuality('#skF_1', V_679)))).
% 9.20/3.03 tff(c_2205, plain, (![W_688, V_689]: (~abstraction(W_688, V_689) | ~accessible_world('#skF_6', W_688) | ~desire_want('#skF_1', V_689)))).
% 9.20/3.03 tff(c_1367, plain, (![X_553, X_517, V_549]: (X_553='#skF_6' | ~proposition(X_517, '#skF_6') | ~desire_want(X_517, '#skF_7') | ~theme(X_517, V_549, X_553) | ~proposition(X_517, X_553) | ~desire_want(X_517, V_549) | ~accessible_world('#skF_1', X_517)))).
% 9.20/3.03 tff(c_1250, plain, (![W_533, X_500]: (W_533='#skF_3' | ~forename(X_500, '#skF_3') | ~of(X_500, W_533, '#skF_2') | ~forename(X_500, W_533) | ~entity(X_500, '#skF_2') | ~accessible_world('#skF_1', X_500)))).
% 9.20/3.03 tff(c_2500, plain, (~dance('#skF_1', '#skF_6'))).
% 9.20/3.03 tff(c_1251, plain, (![W_533, X_500]: (W_533='#skF_5' | ~forename(X_500, '#skF_5') | ~of(X_500, W_533, '#skF_4') | ~forename(X_500, W_533) | ~entity(X_500, '#skF_4') | ~accessible_world('#skF_1', X_500)))).
% 9.20/3.03 tff(c_2499, plain, (~desire_want('#skF_1', '#skF_6'))).
% 9.20/3.03 tff(c_2484, plain, (~dance('#skF_1', '#skF_5'))).
% 9.20/3.03 tff(c_2483, plain, (~desire_want('#skF_1', '#skF_5'))).
% 9.20/3.04 tff(c_2468, plain, (~event('#skF_1', '#skF_6'))).
% 9.20/3.04 tff(c_2467, plain, (~event('#skF_1', '#skF_5'))).
% 9.20/3.04 tff(c_2462, plain, (~dance('#skF_1', '#skF_3'))).
% 9.20/3.04 tff(c_1082, plain, (![X_87, X_505]: (of(X_87, '#skF_3', '#skF_2') | ~accessible_world(X_505, X_87) | ~accessible_world('#skF_1', X_505)))).
% 9.20/3.04 tff(c_2461, plain, (~desire_want('#skF_1', '#skF_3'))).
% 9.20/3.04 tff(c_2446, plain, (~event('#skF_1', '#skF_3'))).
% 9.20/3.04 tff(c_2302, plain, (![W_698, V_699]: (~abstraction(W_698, V_699) | ~accessible_world('#skF_6', W_698) | ~event('#skF_1', V_699)))).
% 9.20/3.04 tff(c_1544, plain, (![W_138, V_571]: (relation(W_138, V_571) | ~accessible_world('#skF_6', W_138) | ~forename('#skF_1', V_571)))).
% 9.20/3.04 tff(c_1011, plain, (![X_152, X_490]: (agent(X_152, '#skF_8', '#skF_4') | ~accessible_world(X_490, X_152) | ~accessible_world('#skF_6', X_490)))).
% 9.20/3.04 tff(c_2110, plain, (![W_676, V_677]: (~human(W_676, V_677) | ~accessible_world('#skF_6', W_676) | ~abstraction('#skF_1', V_677)))).
% 9.20/3.04 tff(c_2242, plain, (![W_694, V_695]: (~entity(W_694, V_695) | ~accessible_world('#skF_6', W_694) | ~abstraction('#skF_1', V_695)))).
% 9.20/3.04 tff(c_2313, plain, (![W_700, V_701]: (singleton(W_700, V_701) | ~accessible_world('#skF_6', W_700) | ~entity('#skF_1', V_701)))).
% 9.20/3.04 tff(c_1007, plain, (![X_152, X_489]: (agent(X_152, '#skF_7', '#skF_4') | ~accessible_world(X_489, X_152) | ~accessible_world('#skF_1', X_489)))).
% 9.20/3.04 tff(c_2255, plain, (![W_696, V_697]: (~eventuality(W_696, V_697) | ~accessible_world('#skF_6', W_696) | ~entity('#skF_1', V_697)))).
% 9.20/3.04 tff(c_2324, plain, (![W_702, V_703]: (~female(W_702, V_703) | ~accessible_world('#skF_6', W_702) | ~eventuality('#skF_1', V_703)))).
% 9.20/3.04 tff(c_818, plain, (![W_90, W_439]: (female(W_90, '#skF_4') | ~accessible_world(W_439, W_90) | ~accessible_world('#skF_1', W_439)))).
% 9.20/3.04 tff(c_989, plain, (![W_479, W_470]: (human_person(W_479, '#skF_2') | ~accessible_world(W_470, W_479) | ~accessible_world('#skF_1', W_470)))).
% 9.20/3.04 tff(c_1709, plain, (![W_158, V_599]: (unisex(W_158, V_599) | ~accessible_world('#skF_6', W_158) | ~eventuality('#skF_1', V_599)))).
% 9.20/3.04 tff(c_1682, plain, (![W_170, V_589]: (thing(W_170, V_589) | ~accessible_world('#skF_6', W_170) | ~entity('#skF_1', V_589)))).
% 9.20/3.04 tff(c_1406, plain, (![W_173, V_558]: (eventuality(W_173, V_558) | ~accessible_world('#skF_6', W_173) | ~event('#skF_1', V_558)))).
% 9.20/3.04 tff(c_1806, plain, (![W_105, V_622]: (existent(W_105, V_622) | ~accessible_world('#skF_6', W_105) | ~entity('#skF_1', V_622)))).
% 9.20/3.04 tff(c_1145, plain, (![W_129, V_514]: (general(W_129, V_514) | ~accessible_world('#skF_6', W_129) | ~abstraction('#skF_1', V_514)))).
% 9.20/3.04 tff(c_1078, plain, (![X_87, X_504]: (of(X_87, '#skF_5', '#skF_4') | ~accessible_world(X_504, X_87) | ~accessible_world('#skF_1', X_504)))).
% 9.20/3.04 tff(c_1579, plain, (![W_161, V_576]: (nonexistent(W_161, V_576) | ~accessible_world('#skF_6', W_161) | ~eventuality('#skF_1', V_576)))).
% 9.20/3.04 tff(c_1107, plain, (![W_176, V_509]: (event(W_176, V_509) | ~accessible_world('#skF_6', W_176) | ~desire_want('#skF_1', V_509)))).
% 9.20/3.04 tff(c_649, plain, (![W_77, W_385]: (male(W_77, '#skF_2') | ~accessible_world(W_385, W_77) | ~accessible_world('#skF_1', W_385)))).
% 9.20/3.04 tff(c_1336, plain, (![W_138, V_543]: (relation(W_138, V_543) | ~accessible_world('#skF_6', W_138) | ~proposition('#skF_1', V_543)))).
% 9.20/3.04 tff(c_1441, plain, (![W_111, V_563]: (organism(W_111, V_563) | ~accessible_world('#skF_6', W_111) | ~human_person('#skF_1', V_563)))).
% 9.20/3.04 tff(c_1761, plain, (![W_158, V_612]: (unisex(W_158, V_612) | ~accessible_world('#skF_6', W_158) | ~abstraction('#skF_1', V_612)))).
% 9.20/3.04 tff(c_1730, plain, (![W_170, V_604]: (thing(W_170, V_604) | ~accessible_world('#skF_6', W_170) | ~eventuality('#skF_1', V_604)))).
% 9.20/3.04 tff(c_1794, plain, (![W_132, V_621]: (nonhuman(W_132, V_621) | ~accessible_world('#skF_6', W_132) | ~abstraction('#skF_1', V_621)))).
% 9.20/3.04 tff(c_1229, plain, (![W_164, V_528]: (specific(W_164, V_528) | ~accessible_world('#skF_6', W_164) | ~entity('#skF_1', V_528)))).
% 9.20/3.04 tff(c_1200, plain, (![X_145, X_522]: (theme(X_145, '#skF_7', '#skF_6') | ~accessible_world(X_522, X_145) | ~accessible_world('#skF_1', X_522)))).
% 9.20/3.04 tff(c_1360, plain, (![W_170, V_548]: (thing(W_170, V_548) | ~accessible_world('#skF_6', W_170) | ~abstraction('#skF_1', V_548)))).
% 9.20/3.04 tff(c_1536, plain, (![W_123, V_570]: (relname(W_123, V_570) | ~accessible_world('#skF_6', W_123) | ~forename('#skF_1', V_570)))).
% 9.20/3.04 tff(c_1305, plain, (![W_176, V_538]: (event(W_176, V_538) | ~accessible_world('#skF_6', W_176) | ~dance('#skF_1', V_538)))).
% 9.20/3.04 tff(c_1022, plain, (![W_164, V_494]: (specific(W_164, V_494) | ~accessible_world('#skF_6', W_164) | ~eventuality('#skF_1', V_494)))).
% 9.20/3.04 tff(c_990, plain, (![W_479, W_457]: (human_person(W_479, '#skF_4') | ~accessible_world(W_457, W_479) | ~accessible_world('#skF_1', W_457)))).
% 9.20/3.04 tff(c_714, plain, (![W_176, W_405]: (event(W_176, '#skF_8') | ~accessible_world(W_405, W_176) | ~accessible_world('#skF_6', W_405)))).
% 9.20/3.04 tff(c_434, plain, (![W_167, V_323, U_322]: (singleton(W_167, V_323) | ~accessible_world(U_322, W_167) | ~entity(U_322, V_323)))).
% 9.20/3.04 tff(c_945, plain, (![W_80, W_470]: (man(W_80, '#skF_2') | ~accessible_world(W_470, W_80) | ~accessible_world('#skF_1', W_470)))).
% 9.20/3.04 tff(c_466, plain, (![W_167, V_337, U_336]: (singleton(W_167, V_337) | ~accessible_world(U_336, W_167) | ~abstraction(U_336, V_337)))).
% 9.20/3.05 tff(c_415, plain, (![W_126, W_314]: (forename(W_126, '#skF_3') | ~accessible_world(W_314, W_126) | ~accessible_world('#skF_1', W_314)))).
% 9.20/3.05 tff(c_1257, plain, (![W_533]: (W_533='#skF_3' | ~of('#skF_1', W_533, '#skF_2') | ~forename('#skF_1', W_533)))).
% 9.20/3.05 tff(c_776, plain, (![W_155, W_425]: (present(W_155, '#skF_7') | ~accessible_world(W_425, W_155) | ~accessible_world('#skF_1', W_425)))).
% 9.20/3.05 tff(c_411, plain, (![W_167, V_313, U_312]: (singleton(W_167, V_313) | ~accessible_world(U_312, W_167) | ~eventuality(U_312, V_313)))).
% 9.20/3.05 tff(c_978, plain, (![W_476, V_265, U_264]: (relation(W_476, V_265) | ~accessible_world(U_264, W_476) | ~forename(U_264, V_265)))).
% 9.20/3.05 tff(c_386, plain, (![W_126, W_306]: (forename(W_126, '#skF_5') | ~accessible_world(W_306, W_126) | ~accessible_world('#skF_1', W_306)))).
% 9.20/3.05 tff(c_971, plain, (![W_83, W_475]: (vincent_forename(W_83, '#skF_3') | ~accessible_world(W_475, W_83) | ~accessible_world('#skF_1', W_475)))).
% 9.20/3.05 tff(c_1254, plain, (![W_533]: (W_533='#skF_5' | ~of('#skF_1', W_533, '#skF_4') | ~forename('#skF_1', W_533)))).
% 9.20/3.05 tff(c_996, plain, (![W_482, V_26, U_25]: (living(W_482, V_26) | ~accessible_world(U_25, W_482) | ~human_person(U_25, V_26)))).
% 9.20/3.05 tff(c_684, plain, (![W_392, V_277, U_276]: (impartial(W_392, V_277) | ~accessible_world(U_276, W_392) | ~human_person(U_276, V_277)))).
% 9.20/3.05 tff(c_1370, plain, (![X_553, V_549]: (X_553='#skF_6' | ~theme('#skF_1', V_549, X_553) | ~proposition('#skF_1', X_553) | ~desire_want('#skF_1', V_549)))).
% 9.20/3.05 tff(c_1859, plain, (![V_62]: (~entity('#skF_1', V_62) | ~dance('#skF_6', V_62)))).
% 9.20/3.05 tff(c_1858, plain, (![V_48]: (~entity('#skF_1', V_48) | ~desire_want('#skF_6', V_48)))).
% 9.20/3.05 tff(c_1860, plain, (~entity('#skF_1', '#skF_8'))).
% 9.20/3.05 tff(c_1832, plain, (![V_60]: (~entity('#skF_1', V_60) | ~event('#skF_6', V_60)))).
% 9.20/3.05 tff(c_1807, plain, (![V_622]: (~eventuality('#skF_6', V_622) | ~entity('#skF_1', V_622)))).
% 9.20/3.05 tff(c_1795, plain, (![V_621]: (~human('#skF_6', V_621) | ~abstraction('#skF_1', V_621)))).
% 9.20/3.05 tff(c_1787, plain, (![V_619]: (existent('#skF_6', V_619) | ~entity('#skF_1', V_619)))).
% 9.20/3.05 tff(c_1783, plain, (![V_616]: (nonhuman('#skF_6', V_616) | ~abstraction('#skF_1', V_616)))).
% 9.20/3.05 tff(c_636, plain, (![W_382, V_18, U_17]: (existent(W_382, V_18) | ~accessible_world(U_17, W_382) | ~entity(U_17, V_18)))).
% 9.20/3.05 tff(c_722, plain, (![W_408, V_40, U_39]: (nonhuman(W_408, V_40) | ~accessible_world(U_39, W_408) | ~abstraction(U_39, V_40)))).
% 9.20/3.05 tff(c_1763, plain, (![V_612]: (~male('#skF_6', V_612) | ~abstraction('#skF_1', V_612)))).
% 9.20/3.05 tff(c_1762, plain, (![V_612]: (~female('#skF_6', V_612) | ~abstraction('#skF_1', V_612)))).
% 9.20/3.05 tff(c_1751, plain, (![V_610]: (unisex('#skF_6', V_610) | ~abstraction('#skF_1', V_610)))).
% 9.20/3.05 tff(c_798, plain, (![W_431, V_36, U_35]: (unisex(W_431, V_36) | ~accessible_world(U_35, W_431) | ~abstraction(U_35, V_36)))).
% 9.20/3.05 tff(c_858, plain, (![W_120, W_453]: (mia_forename(W_120, '#skF_5') | ~accessible_world(W_453, W_120) | ~accessible_world('#skF_1', W_453)))).
% 9.20/3.05 tff(c_1731, plain, (![V_604]: (singleton('#skF_6', V_604) | ~eventuality('#skF_1', V_604)))).
% 9.20/3.05 tff(c_1711, plain, (![V_599]: (~male('#skF_6', V_599) | ~eventuality('#skF_1', V_599)))).
% 9.20/3.05 tff(c_1723, plain, (![V_602]: (thing('#skF_6', V_602) | ~eventuality('#skF_1', V_602)))).
% 9.20/3.05 tff(c_628, plain, (![W_376, V_58, U_57]: (thing(W_376, V_58) | ~accessible_world(U_57, W_376) | ~eventuality(U_57, V_58)))).
% 9.20/3.05 tff(c_1710, plain, (![V_599]: (~female('#skF_6', V_599) | ~eventuality('#skF_1', V_599)))).
% 9.20/3.05 tff(c_1699, plain, (![V_597]: (unisex('#skF_6', V_597) | ~eventuality('#skF_1', V_597)))).
% 9.20/3.05 tff(c_799, plain, (![W_431, V_50, U_49]: (unisex(W_431, V_50) | ~accessible_world(U_49, W_431) | ~eventuality(U_49, V_50)))).
% 9.20/3.05 tff(c_1666, plain, (![W_582]: (~desire_want(W_582, '#skF_2') | ~accessible_world('#skF_6', W_582)))).
% 9.20/3.05 tff(c_1667, plain, (![W_582]: (~dance(W_582, '#skF_2') | ~accessible_world('#skF_6', W_582)))).
% 9.20/3.05 tff(c_791, plain, (![W_179, W_430]: (dance(W_179, '#skF_8') | ~accessible_world(W_430, W_179) | ~accessible_world('#skF_6', W_430)))).
% 9.20/3.05 tff(c_1632, plain, (![W_581]: (~abstraction(W_581, '#skF_4') | ~accessible_world('#skF_6', W_581)))).
% 9.20/3.05 tff(c_1683, plain, (![V_589]: (singleton('#skF_6', V_589) | ~entity('#skF_1', V_589)))).
% 9.20/3.05 tff(c_1675, plain, (![V_587]: (thing('#skF_6', V_587) | ~entity('#skF_1', V_587)))).
% 9.20/3.05 tff(c_626, plain, (![W_376, V_22, U_21]: (thing(W_376, V_22) | ~accessible_world(U_21, W_376) | ~entity(U_21, V_22)))).
% 9.20/3.05 tff(c_1631, plain, (![W_581]: (~dance(W_581, '#skF_4') | ~accessible_world('#skF_6', W_581)))).
% 9.20/3.05 tff(c_1668, plain, (![W_582]: (~abstraction(W_582, '#skF_2') | ~accessible_world('#skF_6', W_582)))).
% 9.20/3.05 tff(c_1630, plain, (![W_581]: (~desire_want(W_581, '#skF_4') | ~accessible_world('#skF_6', W_581)))).
% 9.20/3.05 tff(c_1499, plain, (![W_108]: (entity(W_108, '#skF_2') | ~accessible_world('#skF_6', W_108)))).
% 9.20/3.05 tff(c_1526, plain, (![W_108]: (entity(W_108, '#skF_4') | ~accessible_world('#skF_6', W_108)))).
% 9.20/3.05 tff(c_873, plain, (![W_117, W_457]: (woman(W_117, '#skF_4') | ~accessible_world(W_457, W_117) | ~accessible_world('#skF_1', W_457)))).
% 9.20/3.05 tff(c_1586, plain, (![V_18]: (~eventuality('#skF_1', V_18) | ~entity('#skF_6', V_18)))).
% 9.20/3.05 tff(c_1580, plain, (![V_576]: (~existent('#skF_6', V_576) | ~eventuality('#skF_1', V_576)))).
% 9.20/3.05 tff(c_1572, plain, (![V_574]: (nonexistent('#skF_6', V_574) | ~eventuality('#skF_1', V_574)))).
% 9.20/3.05 tff(c_847, plain, (![W_447, V_52, U_51]: (nonexistent(W_447, V_52) | ~accessible_world(U_51, W_447) | ~eventuality(U_51, V_52)))).
% 9.20/3.06 tff(c_1545, plain, (![V_571]: (abstraction('#skF_6', V_571) | ~forename('#skF_1', V_571)))).
% 9.20/3.06 tff(c_1537, plain, (![V_570]: (relation('#skF_6', V_570) | ~forename('#skF_1', V_570)))).
% 9.20/3.06 tff(c_1527, plain, (~desire_want('#skF_6', '#skF_4'))).
% 9.20/3.06 tff(c_1528, plain, (~dance('#skF_6', '#skF_4'))).
% 9.20/3.06 tff(c_1501, plain, (~dance('#skF_6', '#skF_2'))).
% 9.20/3.06 tff(c_1475, plain, (![V_568]: (relname('#skF_6', V_568) | ~forename('#skF_1', V_568)))).
% 9.20/3.06 tff(c_1500, plain, (~desire_want('#skF_6', '#skF_2'))).
% 9.20/3.06 tff(c_1471, plain, (entity('#skF_6', '#skF_4'))).
% 9.20/3.06 tff(c_1470, plain, (entity('#skF_6', '#skF_2'))).
% 9.20/3.06 tff(c_905, plain, (![W_460, V_34, U_33]: (relname(W_460, V_34) | ~accessible_world(U_33, W_460) | ~forename(U_33, V_34)))).
% 9.20/3.06 tff(c_1444, plain, (![V_563]: (entity('#skF_6', V_563) | ~human_person('#skF_1', V_563)))).
% 9.20/3.06 tff(c_1443, plain, (![V_563]: (impartial('#skF_6', V_563) | ~human_person('#skF_1', V_563)))).
% 9.20/3.06 tff(c_1442, plain, (![V_563]: (living('#skF_6', V_563) | ~human_person('#skF_1', V_563)))).
% 9.20/3.06 tff(c_1428, plain, (![V_561]: (organism('#skF_6', V_561) | ~human_person('#skF_1', V_561)))).
% 9.20/3.06 tff(c_842, plain, (![W_443, V_26, U_25]: (organism(W_443, V_26) | ~accessible_world(U_25, W_443) | ~human_person(U_25, V_26)))).
% 9.20/3.06 tff(c_1408, plain, (![V_558]: (~entity('#skF_6', V_558) | ~event('#skF_1', V_558)))).
% 9.20/3.06 tff(c_1378, plain, (![V_556]: (eventuality('#skF_6', V_556) | ~event('#skF_1', V_556)))).
% 9.20/3.06 tff(c_593, plain, (![W_366, V_60, U_59]: (eventuality(W_366, V_60) | ~accessible_world(U_59, W_366) | ~event(U_59, V_60)))).
% 9.20/3.06 tff(c_1361, plain, (![V_548]: (singleton('#skF_6', V_548) | ~abstraction('#skF_1', V_548)))).
% 9.20/3.06 tff(c_146, plain, (![Y_189, V_186, X_188, W_187, U_185]: (Y_189=X_188 | ~theme(U_185, W_187, Y_189) | ~proposition(U_185, Y_189) | ~desire_want(U_185, W_187) | ~theme(U_185, V_186, X_188) | ~proposition(U_185, X_188) | ~desire_want(U_185, V_186)))).
% 9.20/3.06 tff(c_1353, plain, (![V_546]: (thing('#skF_6', V_546) | ~abstraction('#skF_1', V_546)))).
% 9.20/3.06 tff(c_627, plain, (![W_376, V_42, U_41]: (thing(W_376, V_42) | ~accessible_world(U_41, W_376) | ~abstraction(U_41, V_42)))).
% 9.20/3.06 tff(c_1337, plain, (![V_543]: (abstraction('#skF_6', V_543) | ~proposition('#skF_1', V_543)))).
% 9.20/3.06 tff(c_1329, plain, (![V_541]: (relation('#skF_6', V_541) | ~proposition('#skF_1', V_541)))).
% 9.20/3.06 tff(c_979, plain, (![W_476, V_46, U_45]: (relation(W_476, V_46) | ~accessible_world(U_45, W_476) | ~proposition(U_45, V_46)))).
% 9.20/3.06 tff(c_1310, plain, (![V_538]: (~entity('#skF_6', V_538) | ~dance('#skF_1', V_538)))).
% 9.20/3.06 tff(c_1280, plain, (![V_536]: (event('#skF_6', V_536) | ~dance('#skF_1', V_536)))).
% 9.20/3.06 tff(c_703, plain, (![W_402, V_62, U_61]: (event(W_402, V_62) | ~accessible_world(U_61, W_402) | ~dance(U_61, V_62)))).
% 9.20/3.06 tff(c_1240, plain, (![V_38]: (~entity('#skF_1', V_38) | ~abstraction('#skF_6', V_38)))).
% 9.20/3.06 tff(c_144, plain, (![U_180, X_184, V_181, W_182]: (~of(U_180, X_184, V_181) | X_184=W_182 | ~forename(U_180, X_184) | ~of(U_180, W_182, V_181) | ~forename(U_180, W_182) | ~entity(U_180, V_181)))).
% 9.20/3.06 tff(c_1230, plain, (![V_528]: (~general('#skF_6', V_528) | ~entity('#skF_1', V_528)))).
% 9.20/3.06 tff(c_1222, plain, (![V_526]: (specific('#skF_6', V_526) | ~entity('#skF_1', V_526)))).
% 9.20/3.06 tff(c_503, plain, (![W_344, V_20, U_19]: (specific(W_344, V_20) | ~accessible_world(U_19, W_344) | ~entity(U_19, V_20)))).
% 9.20/3.06 tff(c_1195, plain, (![V_62]: (~abstraction('#skF_1', V_62) | ~dance('#skF_6', V_62)))).
% 9.20/3.06 tff(c_1194, plain, (![V_48]: (~abstraction('#skF_1', V_48) | ~desire_want('#skF_6', V_48)))).
% 9.20/3.06 tff(c_1172, plain, (![X_517]: (theme(X_517, '#skF_7', '#skF_6') | ~accessible_world('#skF_1', X_517)))).
% 9.20/3.06 tff(c_1196, plain, (~abstraction('#skF_1', '#skF_8'))).
% 9.20/3.06 tff(c_1153, plain, (![V_60]: (~abstraction('#skF_1', V_60) | ~event('#skF_6', V_60)))).
% 9.20/3.06 tff(c_120, plain, (![X_145, U_142, V_143, W_144]: (theme(X_145, U_142, V_143) | ~theme(W_144, U_142, V_143) | ~accessible_world(W_144, X_145)))).
% 9.20/3.06 tff(c_1147, plain, (![V_514]: (~entity('#skF_6', V_514) | ~abstraction('#skF_1', V_514)))).
% 9.20/3.06 tff(c_1146, plain, (![V_514]: (~eventuality('#skF_6', V_514) | ~abstraction('#skF_1', V_514)))).
% 9.20/3.06 tff(c_1131, plain, (![V_512]: (general('#skF_6', V_512) | ~abstraction('#skF_1', V_512)))).
% 9.20/3.06 tff(c_690, plain, (![W_397, V_38, U_37]: (general(W_397, V_38) | ~accessible_world(U_37, W_397) | ~abstraction(U_37, V_38)))).
% 9.20/3.06 tff(c_1112, plain, (![V_509]: (~entity('#skF_6', V_509) | ~desire_want('#skF_1', V_509)))).
% 9.20/3.06 tff(c_1086, plain, (![V_507]: (event('#skF_6', V_507) | ~desire_want('#skF_1', V_507)))).
% 9.20/3.06 tff(c_702, plain, (![W_402, V_48, U_47]: (event(W_402, V_48) | ~accessible_world(U_47, W_402) | ~desire_want(U_47, V_48)))).
% 9.20/3.06 tff(c_1074, plain, (![X_500]: (of(X_500, '#skF_3', '#skF_2') | ~accessible_world('#skF_1', X_500)))).
% 9.20/3.06 tff(c_1073, plain, (![X_500]: (of(X_500, '#skF_5', '#skF_4') | ~accessible_world('#skF_1', X_500)))).
% 9.20/3.06 tff(c_82, plain, (![X_87, U_84, V_85, W_86]: (of(X_87, U_84, V_85) | ~of(W_86, U_84, V_85) | ~accessible_world(W_86, X_87)))).
% 9.20/3.06 tff(c_1051, plain, (![V_62]: (~abstraction('#skF_6', V_62) | ~dance('#skF_1', V_62)))).
% 9.20/3.06 tff(c_1050, plain, (![V_48]: (~abstraction('#skF_6', V_48) | ~desire_want('#skF_1', V_48)))).
% 9.20/3.06 tff(c_1035, plain, (![V_60]: (~abstraction('#skF_6', V_60) | ~event('#skF_1', V_60)))).
% 9.20/3.06 tff(c_1029, plain, (![V_38]: (~eventuality('#skF_1', V_38) | ~abstraction('#skF_6', V_38)))).
% 9.20/3.06 tff(c_1023, plain, (![V_494]: (~general('#skF_6', V_494) | ~eventuality('#skF_1', V_494)))).
% 9.20/3.06 tff(c_1015, plain, (![V_492]: (specific('#skF_6', V_492) | ~eventuality('#skF_1', V_492)))).
% 9.20/3.06 tff(c_504, plain, (![W_344, V_54, U_53]: (specific(W_344, V_54) | ~accessible_world(U_53, W_344) | ~eventuality(U_53, V_54)))).
% 9.20/3.06 tff(c_1003, plain, (![X_485]: (agent(X_485, '#skF_8', '#skF_4') | ~accessible_world('#skF_6', X_485)))).
% 9.20/3.07 tff(c_1002, plain, (![X_485]: (agent(X_485, '#skF_7', '#skF_4') | ~accessible_world('#skF_1', X_485)))).
% 9.20/3.07 tff(c_124, plain, (![X_152, U_149, V_150, W_151]: (agent(X_152, U_149, V_150) | ~agent(W_151, U_149, V_150) | ~accessible_world(W_151, X_152)))).
% 9.20/3.07 tff(c_90, plain, (![W_99, U_97, V_98]: (living(W_99, U_97) | ~living(V_98, U_97) | ~accessible_world(V_98, W_99)))).
% 9.20/3.07 tff(c_100, plain, (![W_114, U_112, V_113]: (human_person(W_114, U_112) | ~human_person(V_113, U_112) | ~accessible_world(V_113, W_114)))).
% 9.20/3.07 tff(c_116, plain, (![W_138, U_136, V_137]: (relation(W_138, U_136) | ~relation(V_137, U_136) | ~accessible_world(V_137, W_138)))).
% 9.20/3.07 tff(c_964, plain, (![W_472]: (vincent_forename(W_472, '#skF_3') | ~accessible_world('#skF_1', W_472)))).
% 9.20/3.07 tff(c_80, plain, (![W_83, U_81, V_82]: (vincent_forename(W_83, U_81) | ~vincent_forename(V_82, U_81) | ~accessible_world(V_82, W_83)))).
% 9.20/3.07 tff(c_947, plain, (![W_470]: (human_person(W_470, '#skF_2') | ~accessible_world('#skF_1', W_470)))).
% 9.20/3.07 tff(c_935, plain, (![W_467]: (man(W_467, '#skF_2') | ~accessible_world('#skF_1', W_467)))).
% 9.20/3.07 tff(c_78, plain, (![W_80, U_78, V_79]: (man(W_80, U_78) | ~man(V_79, U_78) | ~accessible_world(V_79, W_80)))).
% 9.20/3.07 tff(c_915, plain, (![W_463]: (entity(W_463, '#skF_2') | ~accessible_world('#skF_1', W_463)))).
% 9.20/3.07 tff(c_96, plain, (![W_108, U_106, V_107]: (entity(W_108, U_106) | ~entity(V_107, U_106) | ~accessible_world(V_107, W_108)))).
% 9.20/3.07 tff(c_106, plain, (![W_123, U_121, V_122]: (relname(W_123, U_121) | ~relname(V_122, U_121) | ~accessible_world(V_122, W_123)))).
% 9.20/3.07 tff(c_886, plain, (![W_458]: (entity(W_458, '#skF_4') | ~accessible_world('#skF_1', W_458)))).
% 9.20/3.07 tff(c_875, plain, (![W_457]: (human_person(W_457, '#skF_4') | ~accessible_world('#skF_1', W_457)))).
% 9.20/3.07 tff(c_863, plain, (![W_454]: (woman(W_454, '#skF_4') | ~accessible_world('#skF_1', W_454)))).
% 9.20/3.07 tff(c_102, plain, (![W_117, U_115, V_116]: (woman(W_117, U_115) | ~woman(V_116, U_115) | ~accessible_world(V_116, W_117)))).
% 9.20/3.07 tff(c_851, plain, (![W_450]: (mia_forename(W_450, '#skF_5') | ~accessible_world('#skF_1', W_450)))).
% 9.20/3.07 tff(c_104, plain, (![W_120, U_118, V_119]: (mia_forename(W_120, U_118) | ~mia_forename(V_119, U_118) | ~accessible_world(V_119, W_120)))).
% 9.20/3.07 tff(c_130, plain, (![W_161, U_159, V_160]: (nonexistent(W_161, U_159) | ~nonexistent(V_160, U_159) | ~accessible_world(V_160, W_161)))).
% 9.20/3.07 tff(c_837, plain, (![U_61]: (~accessible_world('#skF_1', U_61) | ~dance(U_61, '#skF_4')))).
% 9.20/3.07 tff(c_98, plain, (![W_111, U_109, V_110]: (organism(W_111, U_109) | ~organism(V_110, U_109) | ~accessible_world(V_110, W_111)))).
% 9.20/3.07 tff(c_836, plain, (![U_47]: (~accessible_world('#skF_1', U_47) | ~desire_want(U_47, '#skF_4')))).
% 9.20/3.07 tff(c_826, plain, (![U_59]: (~accessible_world('#skF_1', U_59) | ~event(U_59, '#skF_4')))).
% 9.20/3.07 tff(c_820, plain, (![W_439]: (~eventuality(W_439, '#skF_4') | ~accessible_world('#skF_1', W_439)))).
% 9.20/3.07 tff(c_808, plain, (![W_436]: (female(W_436, '#skF_4') | ~accessible_world('#skF_1', W_436)))).
% 9.20/3.07 tff(c_84, plain, (![W_90, U_88, V_89]: (female(W_90, U_88) | ~female(V_89, U_88) | ~accessible_world(V_89, W_90)))).
% 9.20/3.07 tff(c_784, plain, (![W_155, W_429]: (present(W_155, '#skF_8') | ~accessible_world(W_429, W_155) | ~accessible_world('#skF_6', W_429)))).
% 9.20/3.07 tff(c_128, plain, (![W_158, U_156, V_157]: (unisex(W_158, U_156) | ~unisex(V_157, U_156) | ~accessible_world(V_157, W_158)))).
% 9.20/3.07 tff(c_780, plain, (![W_426]: (dance(W_426, '#skF_8') | ~accessible_world('#skF_6', W_426)))).
% 9.20/3.07 tff(c_772, plain, (![W_422]: (present(W_422, '#skF_8') | ~accessible_world('#skF_6', W_422)))).
% 9.20/3.07 tff(c_142, plain, (![W_179, U_177, V_178]: (dance(W_179, U_177) | ~dance(V_178, U_177) | ~accessible_world(V_178, W_179)))).
% 9.20/3.07 tff(c_771, plain, (![W_422]: (present(W_422, '#skF_7') | ~accessible_world('#skF_1', W_422)))).
% 9.20/3.07 tff(c_126, plain, (![W_155, U_153, V_154]: (present(W_155, U_153) | ~present(V_154, U_153) | ~accessible_world(V_154, W_155)))).
% 9.20/3.07 tff(c_757, plain, (![W_417]: (animate(W_417, '#skF_2') | ~accessible_world('#skF_1', W_417)))).
% 9.20/3.07 tff(c_756, plain, (![W_417]: (animate(W_417, '#skF_4') | ~accessible_world('#skF_1', W_417)))).
% 9.20/3.07 tff(c_86, plain, (![W_93, U_91, V_92]: (animate(W_93, U_91) | ~animate(V_92, U_91) | ~accessible_world(V_92, W_93)))).
% 9.20/3.07 tff(c_750, plain, (~abstraction('#skF_6', '#skF_4'))).
% 9.20/3.07 tff(c_737, plain, (![W_414]: (~abstraction(W_414, '#skF_4') | ~accessible_world('#skF_1', W_414)))).
% 9.20/3.07 tff(c_729, plain, (![W_411]: (human(W_411, '#skF_2') | ~accessible_world('#skF_1', W_411)))).
% 9.20/3.07 tff(c_728, plain, (![W_411]: (human(W_411, '#skF_4') | ~accessible_world('#skF_1', W_411)))).
% 9.20/3.07 tff(c_88, plain, (![W_96, U_94, V_95]: (human(W_96, U_94) | ~human(V_95, U_94) | ~accessible_world(V_95, W_96)))).
% 9.20/3.07 tff(c_112, plain, (![W_132, U_130, V_131]: (nonhuman(W_132, U_130) | ~nonhuman(V_131, U_130) | ~accessible_world(V_131, W_132)))).
% 9.20/3.07 tff(c_716, plain, (![W_405]: (~entity(W_405, '#skF_8') | ~accessible_world('#skF_6', W_405)))).
% 9.20/3.07 tff(c_715, plain, (![W_405]: (~abstraction(W_405, '#skF_8') | ~accessible_world('#skF_6', W_405)))).
% 9.20/3.07 tff(c_704, plain, (![W_402]: (event(W_402, '#skF_8') | ~accessible_world('#skF_6', W_402)))).
% 9.20/3.07 tff(c_140, plain, (![W_176, U_174, V_175]: (event(W_176, U_174) | ~event(V_175, U_174) | ~accessible_world(V_175, W_176)))).
% 9.20/3.07 tff(c_419, plain, (![W_148, W_315]: (desire_want(W_148, '#skF_7') | ~accessible_world(W_315, W_148) | ~accessible_world('#skF_1', W_315)))).
% 9.20/3.07 tff(c_110, plain, (![W_129, U_127, V_128]: (general(W_129, U_127) | ~general(V_128, U_127) | ~accessible_world(V_128, W_129)))).
% 9.20/3.07 tff(c_680, plain, (![U_61]: (~accessible_world('#skF_1', U_61) | ~dance(U_61, '#skF_2')))).
% 9.20/3.07 tff(c_679, plain, (![U_47]: (~accessible_world('#skF_1', U_47) | ~desire_want(U_47, '#skF_2')))).
% 9.20/3.07 tff(c_92, plain, (![W_102, U_100, V_101]: (impartial(W_102, U_100) | ~impartial(V_101, U_100) | ~accessible_world(V_101, W_102)))).
% 9.20/3.07 tff(c_669, plain, (![U_59]: (~accessible_world('#skF_1', U_59) | ~event(U_59, '#skF_2')))).
% 9.20/3.07 tff(c_651, plain, (![W_385]: (~eventuality(W_385, '#skF_2') | ~accessible_world('#skF_1', W_385)))).
% 9.20/3.07 tff(c_663, plain, (~accessible_world('#skF_1', '#skF_1'))).
% 9.20/3.07 tff(c_652, plain, (![W_385]: (~female(W_385, '#skF_2') | ~accessible_world('#skF_1', W_385)))).
% 9.20/3.07 tff(c_456, plain, (![W_141, W_333]: (proposition(W_141, '#skF_6') | ~accessible_world(W_333, W_141) | ~accessible_world('#skF_1', W_333)))).
% 9.20/3.07 tff(c_657, plain, (~abstraction('#skF_6', '#skF_2'))).
% 9.20/3.07 tff(c_650, plain, (![W_385]: (~abstraction(W_385, '#skF_2') | ~accessible_world('#skF_1', W_385)))).
% 9.20/3.07 tff(c_632, plain, (![W_379]: (male(W_379, '#skF_2') | ~accessible_world('#skF_1', W_379)))).
% 9.20/3.07 tff(c_94, plain, (![W_105, U_103, V_104]: (existent(W_105, U_103) | ~existent(V_104, U_103) | ~accessible_world(V_104, W_105)))).
% 9.20/3.07 tff(c_76, plain, (![W_77, U_75, V_76]: (male(W_77, U_75) | ~male(V_76, U_75) | ~accessible_world(V_76, W_77)))).
% 9.20/3.07 tff(c_136, plain, (![W_170, U_168, V_169]: (thing(W_170, U_168) | ~thing(V_169, U_168) | ~accessible_world(V_169, W_170)))).
% 9.20/3.07 tff(c_561, plain, (![W_135]: (abstraction(W_135, '#skF_3') | ~accessible_world('#skF_6', W_135)))).
% 9.20/3.07 tff(c_617, plain, (~abstraction('#skF_6', '#skF_7'))).
% 9.20/3.07 tff(c_610, plain, (![W_309]: (~abstraction(W_309, '#skF_7') | ~accessible_world('#skF_1', W_309)))).
% 9.20/3.07 tff(c_553, plain, (![W_135]: (abstraction(W_135, '#skF_5') | ~accessible_world('#skF_6', W_135)))).
% 9.20/3.07 tff(c_611, plain, (~abstraction('#skF_1', '#skF_7'))).
% 9.20/3.07 tff(c_572, plain, (![U_47, V_48]: (~abstraction(U_47, V_48) | ~desire_want(U_47, V_48)))).
% 9.20/3.08 tff(c_530, plain, (![U_47, V_48]: (~entity(U_47, V_48) | ~desire_want(U_47, V_48)))).
% 9.20/3.08 tff(c_138, plain, (![W_173, U_171, V_172]: (eventuality(W_173, U_171) | ~eventuality(V_172, U_171) | ~accessible_world(V_172, W_173)))).
% 9.20/3.08 tff(c_531, plain, (![U_61, V_62]: (~entity(U_61, V_62) | ~dance(U_61, V_62)))).
% 9.20/3.08 tff(c_547, plain, (![W_355]: (abstraction(W_355, '#skF_6') | ~accessible_world('#skF_6', W_355)))).
% 9.20/3.08 tff(c_573, plain, (![U_61, V_62]: (~abstraction(U_61, V_62) | ~dance(U_61, V_62)))).
% 9.20/3.08 tff(c_574, plain, (~abstraction('#skF_6', '#skF_8'))).
% 9.20/3.08 tff(c_519, plain, (![U_59, V_60]: (~abstraction(U_59, V_60) | ~event(U_59, V_60)))).
% 9.20/3.08 tff(c_558, plain, (abstraction('#skF_6', '#skF_3'))).
% 9.20/3.08 tff(c_494, plain, (![W_299]: (abstraction(W_299, '#skF_3') | ~accessible_world('#skF_1', W_299)))).
% 9.20/3.08 tff(c_537, plain, (abstraction('#skF_6', '#skF_5'))).
% 9.20/3.08 tff(c_114, plain, (![W_135, U_133, V_134]: (abstraction(W_135, U_133) | ~abstraction(V_134, U_133) | ~accessible_world(V_134, W_135)))).
% 9.20/3.08 tff(c_495, plain, (![W_299]: (abstraction(W_299, '#skF_5') | ~accessible_world('#skF_1', W_299)))).
% 9.20/3.08 tff(c_532, plain, (~entity('#skF_6', '#skF_8'))).
% 9.20/3.08 tff(c_509, plain, (![U_59, V_60]: (~entity(U_59, V_60) | ~event(U_59, V_60)))).
% 9.20/3.08 tff(c_462, plain, (![U_37, V_38]: (~eventuality(U_37, V_38) | ~abstraction(U_37, V_38)))).
% 9.20/3.08 tff(c_514, plain, (abstraction('#skF_6', '#skF_6'))).
% 9.20/3.08 tff(c_457, plain, (![W_333]: (abstraction(W_333, '#skF_6') | ~accessible_world('#skF_1', W_333)))).
% 9.20/3.08 tff(c_424, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~entity(U_17, V_18)))).
% 9.20/3.08 tff(c_497, plain, (abstraction('#skF_1', '#skF_5'))).
% 9.20/3.08 tff(c_496, plain, (abstraction('#skF_1', '#skF_3'))).
% 9.20/3.08 tff(c_132, plain, (![W_164, U_162, V_163]: (specific(W_164, U_162) | ~specific(V_163, U_162) | ~accessible_world(V_163, W_164)))).
% 9.20/3.08 tff(c_443, plain, (![U_327, V_328]: (abstraction(U_327, V_328) | ~forename(U_327, V_328)))).
% 9.20/3.08 tff(c_448, plain, (![U_37, V_38]: (~entity(U_37, V_38) | ~abstraction(U_37, V_38)))).
% 9.20/3.08 tff(c_266, plain, (![U_35, V_36]: (~male(U_35, V_36) | ~abstraction(U_35, V_36)))).
% 9.20/3.08 tff(c_216, plain, (![U_240, V_241]: (singleton(U_240, V_241) | ~abstraction(U_240, V_241)))).
% 9.20/3.08 tff(c_242, plain, (![U_53, V_54]: (~general(U_53, V_54) | ~eventuality(U_53, V_54)))).
% 9.20/3.08 tff(c_438, plain, (![W_324]: (proposition(W_324, '#skF_6') | ~accessible_world('#skF_1', W_324)))).
% 9.20/3.08 tff(c_282, plain, (![U_276, V_277]: (impartial(U_276, V_277) | ~human_person(U_276, V_277)))).
% 9.20/3.08 tff(c_258, plain, (![U_266, V_267]: (~general(U_266, V_267) | ~entity(U_266, V_267)))).
% 9.20/3.08 tff(c_253, plain, (![U_264, V_265]: (relation(U_264, V_265) | ~forename(U_264, V_265)))).
% 9.20/3.08 tff(c_118, plain, (![W_141, U_139, V_140]: (proposition(W_141, U_139) | ~proposition(V_140, U_139) | ~accessible_world(V_140, W_141)))).
% 9.20/3.08 tff(c_272, plain, (![U_270, V_271]: (singleton(U_270, V_271) | ~entity(U_270, V_271)))).
% 9.20/3.08 tff(c_334, plain, (![U_25, V_26]: (living(U_25, V_26) | ~human_person(U_25, V_26)))).
% 9.20/3.08 tff(c_296, plain, (![U_35, V_36]: (~female(U_35, V_36) | ~abstraction(U_35, V_36)))).
% 9.20/3.08 tff(c_221, plain, (![U_51, V_52]: (~existent(U_51, V_52) | ~eventuality(U_51, V_52)))).
% 9.20/3.08 tff(c_407, plain, (![W_309]: (desire_want(W_309, '#skF_7') | ~accessible_world('#skF_1', W_309)))).
% 9.20/3.08 tff(c_367, plain, (![W_299]: (forename(W_299, '#skF_3') | ~accessible_world('#skF_1', W_299)))).
% 9.20/3.08 tff(c_205, plain, (![U_57, V_58]: (singleton(U_57, V_58) | ~eventuality(U_57, V_58)))).
% 9.20/3.08 tff(c_403, plain, (~dance('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_402, plain, (~desire_want('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_122, plain, (![W_148, U_146, V_147]: (desire_want(W_148, U_146) | ~desire_want(V_147, U_146) | ~accessible_world(V_147, W_148)))).
% 9.20/3.08 tff(c_395, plain, (~event('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_391, plain, (~eventuality('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_267, plain, (![U_49, V_50]: (~male(U_49, V_50) | ~eventuality(U_49, V_50)))).
% 9.20/3.08 tff(c_382, plain, (~abstraction('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_381, plain, (~abstraction('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_368, plain, (![W_299]: (forename(W_299, '#skF_5') | ~accessible_world('#skF_1', W_299)))).
% 9.20/3.08 tff(c_230, plain, (![U_39, V_40]: (~human(U_39, V_40) | ~abstraction(U_39, V_40)))).
% 9.20/3.08 tff(c_373, plain, (abstraction('#skF_1', '#skF_6'))).
% 9.20/3.08 tff(c_210, plain, (![U_236, V_237]: (abstraction(U_236, V_237) | ~proposition(U_236, V_237)))).
% 9.20/3.08 tff(c_108, plain, (![W_126, U_124, V_125]: (forename(W_126, U_124) | ~forename(V_125, U_124) | ~accessible_world(V_125, W_126)))).
% 9.20/3.08 tff(c_361, plain, (~dance('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_360, plain, (~desire_want('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_353, plain, (~event('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_349, plain, (~eventuality('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_297, plain, (![U_49, V_50]: (~female(U_49, V_50) | ~eventuality(U_49, V_50)))).
% 9.20/3.08 tff(c_134, plain, (![W_167, U_165, V_166]: (singleton(W_167, U_165) | ~singleton(V_166, U_165) | ~accessible_world(V_166, W_167)))).
% 9.20/3.08 tff(c_343, plain, (entity('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_342, plain, (entity('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_283, plain, (![U_276, V_277]: (entity(U_276, V_277) | ~human_person(U_276, V_277)))).
% 9.20/3.08 tff(c_14, plain, (![U_13, V_14]: (living(U_13, V_14) | ~organism(U_13, V_14)))).
% 9.20/3.08 tff(c_329, plain, (female('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_8, plain, (![U_7, V_8]: (female(U_7, V_8) | ~woman(U_7, V_8)))).
% 9.20/3.08 tff(c_324, plain, (animate('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_323, plain, (animate('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_10, plain, (![U_9, V_10]: (animate(U_9, V_10) | ~human_person(U_9, V_10)))).
% 9.20/3.08 tff(c_315, plain, (~female('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_306, plain, (human('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_305, plain, (human('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_311, plain, (male('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_2, plain, (![U_1, V_2]: (male(U_1, V_2) | ~man(U_1, V_2)))).
% 9.20/3.08 tff(c_12, plain, (![U_11, V_12]: (human(U_11, V_12) | ~human_person(U_11, V_12)))).
% 9.20/3.08 tff(c_72, plain, (![U_71, V_72]: (~female(U_71, V_72) | ~unisex(U_71, V_72)))).
% 9.20/3.08 tff(c_288, plain, (human_person('#skF_1', '#skF_2'))).
% 9.20/3.08 tff(c_4, plain, (![U_3, V_4]: (human_person(U_3, V_4) | ~man(U_3, V_4)))).
% 9.20/3.08 tff(c_26, plain, (![U_25, V_26]: (organism(U_25, V_26) | ~human_person(U_25, V_26)))).
% 9.20/3.08 tff(c_18, plain, (![U_17, V_18]: (existent(U_17, V_18) | ~entity(U_17, V_18)))).
% 9.20/3.08 tff(c_16, plain, (![U_15, V_16]: (impartial(U_15, V_16) | ~organism(U_15, V_16)))).
% 9.20/3.08 tff(c_22, plain, (![U_21, V_22]: (thing(U_21, V_22) | ~entity(U_21, V_22)))).
% 9.20/3.08 tff(c_74, plain, (![U_73, V_74]: (~male(U_73, V_74) | ~unisex(U_73, V_74)))).
% 9.20/3.08 tff(c_20, plain, (![U_19, V_20]: (specific(U_19, V_20) | ~entity(U_19, V_20)))).
% 9.20/3.08 tff(c_34, plain, (![U_33, V_34]: (relname(U_33, V_34) | ~forename(U_33, V_34)))).
% 9.20/3.08 tff(c_24, plain, (![U_23, V_24]: (entity(U_23, V_24) | ~organism(U_23, V_24)))).
% 9.20/3.08 tff(c_247, plain, (human_person('#skF_1', '#skF_4'))).
% 9.20/3.08 tff(c_28, plain, (![U_27, V_28]: (human_person(U_27, V_28) | ~woman(U_27, V_28)))).
% 9.20/3.08 tff(c_70, plain, (![U_69, V_70]: (~general(U_69, V_70) | ~specific(U_69, V_70)))).
% 9.20/3.08 tff(c_6, plain, (![U_5, V_6]: (forename(U_5, V_6) | ~vincent_forename(U_5, V_6)))).
% 9.20/3.08 tff(c_32, plain, (![U_31, V_32]: (relation(U_31, V_32) | ~relname(U_31, V_32)))).
% 9.20/3.08 tff(c_68, plain, (![U_67, V_68]: (~human(U_67, V_68) | ~nonhuman(U_67, V_68)))).
% 9.20/3.08 tff(c_48, plain, (![U_47, V_48]: (event(U_47, V_48) | ~desire_want(U_47, V_48)))).
% 9.20/3.08 tff(c_66, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~male(U_65, V_66)))).
% 9.20/3.08 tff(c_36, plain, (![U_35, V_36]: (unisex(U_35, V_36) | ~abstraction(U_35, V_36)))).
% 9.20/3.09 tff(c_40, plain, (![U_39, V_40]: (nonhuman(U_39, V_40) | ~abstraction(U_39, V_40)))).
% 9.20/3.09 tff(c_64, plain, (![U_63, V_64]: (~nonexistent(U_63, V_64) | ~existent(U_63, V_64)))).
% 9.20/3.09 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~abstraction(U_41, V_42)))).
% 9.20/3.09 tff(c_62, plain, (![U_61, V_62]: (event(U_61, V_62) | ~dance(U_61, V_62)))).
% 9.20/3.09 tff(c_46, plain, (![U_45, V_46]: (relation(U_45, V_46) | ~proposition(U_45, V_46)))).
% 9.20/3.09 tff(c_56, plain, (![U_55, V_56]: (singleton(U_55, V_56) | ~thing(U_55, V_56)))).
% 9.20/3.09 tff(c_54, plain, (![U_53, V_54]: (specific(U_53, V_54) | ~eventuality(U_53, V_54)))).
% 9.20/3.09 tff(c_50, plain, (![U_49, V_50]: (unisex(U_49, V_50) | ~eventuality(U_49, V_50)))).
% 9.20/3.09 tff(c_58, plain, (![U_57, V_58]: (thing(U_57, V_58) | ~eventuality(U_57, V_58)))).
% 9.20/3.09 tff(c_60, plain, (![U_59, V_60]: (eventuality(U_59, V_60) | ~event(U_59, V_60)))).
% 9.20/3.09 tff(c_52, plain, (![U_51, V_52]: (nonexistent(U_51, V_52) | ~eventuality(U_51, V_52)))).
% 9.20/3.09 tff(c_30, plain, (![U_29, V_30]: (forename(U_29, V_30) | ~mia_forename(U_29, V_30)))).
% 9.20/3.09 tff(c_38, plain, (![U_37, V_38]: (general(U_37, V_38) | ~abstraction(U_37, V_38)))).
% 9.20/3.09 tff(c_44, plain, (![U_43, V_44]: (abstraction(U_43, V_44) | ~relation(U_43, V_44)))).
% 9.20/3.09 tff(c_148, plain, (![X3_211, X5_214, X4_212]: (~dance(X3_211, X5_214) | ~present(X3_211, X5_214) | ~agent(X3_211, X5_214, '#skF_2') | ~event(X3_211, X5_214) | ~accessible_world('#skF_1', X3_211) | ~agent('#skF_1', X4_212, '#skF_2') | ~desire_want('#skF_1', X4_212) | ~theme('#skF_1', X4_212, X3_211) | ~present('#skF_1', X4_212) | ~proposition('#skF_1', X3_211)))).
% 9.20/3.09 tff(c_164, plain, (theme('#skF_1', '#skF_7', '#skF_6'))).
% 9.20/3.09 tff(c_176, plain, (of('#skF_1', '#skF_5', '#skF_4'))).
% 9.20/3.09 tff(c_160, plain, (agent('#skF_1', '#skF_7', '#skF_4'))).
% 9.20/3.09 tff(c_154, plain, (agent('#skF_6', '#skF_8', '#skF_4'))).
% 9.20/3.09 tff(c_184, plain, (of('#skF_1', '#skF_3', '#skF_2'))).
% 9.20/3.09 tff(c_182, plain, (man('#skF_1', '#skF_2'))).
% 9.20/3.09 tff(c_166, plain, (present('#skF_1', '#skF_7'))).
% 9.20/3.09 tff(c_168, plain, (proposition('#skF_1', '#skF_6'))).
% 9.20/3.09 tff(c_178, plain, (forename('#skF_1', '#skF_3'))).
% 9.20/3.09 tff(c_162, plain, (desire_want('#skF_1', '#skF_7'))).
% 9.20/3.09 tff(c_174, plain, (woman('#skF_1', '#skF_4'))).
% 9.20/3.09 tff(c_150, plain, (dance('#skF_6', '#skF_8'))).
% 9.20/3.09 tff(c_158, plain, (accessible_world('#skF_1', '#skF_6'))).
% 9.20/3.09 tff(c_152, plain, (present('#skF_6', '#skF_8'))).
% 9.20/3.09 tff(c_170, plain, (forename('#skF_1', '#skF_5'))).
% 9.20/3.09 tff(c_156, plain, (event('#skF_6', '#skF_8'))).
% 9.20/3.09 tff(c_172, plain, (mia_forename('#skF_1', '#skF_5'))).
% 9.20/3.09 tff(c_180, plain, (vincent_forename('#skF_1', '#skF_3'))).
% 9.20/3.09 tff(c_186, plain, (actual_world('#skF_1'))).
% 9.20/3.09 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.20/3.09
%------------------------------------------------------------------------------