%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP023-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 : n011.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 10.10s 3.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : NLP023-1 : TPTP v9.0.0. Released v2.4.0. % 0.00/0.08 % 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.08/0.28 % Computer : n011.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Tue Apr 8 08:09:33 EDT 2025 % 0.08/0.28 % CPUTime : % 10.10/3.65 % 10.10/3.65 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.10/3.66 % 10.10/3.66 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.10/3.67 %$ theme > of > agent > woman > unisex > thing > specific > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > mia_forename > living > impartial > human_person > human > general > forename > female > existent > eventuality > event > entity > desire_want > dance > animate > accessible_world > abstraction > actual_world > #nlpp > skc9 > skc8 > skc7 > skc6 > skc11 > skc10 % 10.10/3.67 % 10.10/3.67 %Foreground sorts: % 10.10/3.67 % 10.10/3.67 % 10.10/3.67 %Background operators: % 10.10/3.67 % 10.10/3.67 % 10.10/3.67 %Foreground operators: % 10.10/3.67 tff(relation, type, relation: ($i * $i) > $o). % 10.10/3.67 tff(forename, type, forename: ($i * $i) > $o). % 10.10/3.67 tff(skc7, type, skc7: $i). % 10.10/3.67 tff(female, type, female: ($i * $i) > $o). % 10.10/3.67 tff(theme, type, theme: ($i * $i * $i) > $o). % 10.10/3.67 tff(living, type, living: ($i * $i) > $o). % 10.10/3.67 tff(human_person, type, human_person: ($i * $i) > $o). % 10.10/3.67 tff(present, type, present: ($i * $i) > $o). % 10.10/3.67 tff(skc11, type, skc11: $i). % 10.10/3.67 tff(entity, type, entity: ($i * $i) > $o). % 10.10/3.67 tff(skc9, type, skc9: $i). % 10.10/3.67 tff(eventuality, type, eventuality: ($i * $i) > $o). % 10.10/3.67 tff(existent, type, existent: ($i * $i) > $o). % 10.10/3.67 tff(abstraction, type, abstraction: ($i * $i) > $o). % 10.10/3.67 tff(skc8, type, skc8: $i). % 10.10/3.67 tff(proposition, type, proposition: ($i * $i) > $o). % 10.10/3.67 tff(relname, type, relname: ($i * $i) > $o). % 10.10/3.67 tff(singleton, type, singleton: ($i * $i) > $o). % 10.10/3.67 tff(organism, type, organism: ($i * $i) > $o). % 10.10/3.67 tff(animate, type, animate: ($i * $i) > $o). % 10.10/3.67 tff(of, type, of: ($i * $i * $i) > $o). % 10.10/3.67 tff(actual_world, type, actual_world: $i > $o). % 10.10/3.67 tff(agent, type, agent: ($i * $i * $i) > $o). % 10.10/3.67 tff(general, type, general: ($i * $i) > $o). % 10.10/3.67 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 10.10/3.67 tff(event, type, event: ($i * $i) > $o). % 10.10/3.67 tff(woman, type, woman: ($i * $i) > $o). % 10.10/3.67 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 10.10/3.67 tff(thing, type, thing: ($i * $i) > $o). % 10.10/3.67 tff(dance, type, dance: ($i * $i) > $o). % 10.10/3.67 tff(desire_want, type, desire_want: ($i * $i) > $o). % 10.10/3.67 tff(human, type, human: ($i * $i) > $o). % 10.10/3.67 tff(unisex, type, unisex: ($i * $i) > $o). % 10.10/3.67 tff(skc6, type, skc6: $i). % 10.10/3.67 tff(impartial, type, impartial: ($i * $i) > $o). % 10.10/3.67 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 10.10/3.67 tff(specific, type, specific: ($i * $i) > $o). % 10.10/3.67 tff(skc10, type, skc10: $i). % 10.10/3.67 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 10.10/3.67 % 10.10/3.67 %Saturated clause set: % 10.10/3.67 tff(c_1906, plain, (![V_135, V_628, V_627]: (impartial(V_135, V_628) | ~accessible_world(V_627, V_135) | ~accessible_world(skc8, V_627) | ~human_person(skc6, V_628)))). % 10.10/3.67 tff(c_1888, plain, (![V_99, V_622, V_621]: (relation(V_99, V_622) | ~accessible_world(V_621, V_99) | ~accessible_world(skc8, V_621) | ~forename(skc6, V_622)))). % 10.10/3.67 tff(c_1962, plain, (![V_78, V_640, V_639]: (singleton(V_78, V_640) | ~accessible_world(V_639, V_78) | ~accessible_world(skc8, V_639) | ~eventuality(skc6, V_640)))). % 10.10/3.67 tff(c_1910, plain, (![V_78, V_630, V_629]: (singleton(V_78, V_630) | ~accessible_world(V_629, V_78) | ~accessible_world(skc8, V_629) | ~abstraction(skc6, V_630)))). % 10.10/3.67 tff(c_2018, plain, (![V_138, V_651, V_650]: (living(V_138, V_651) | ~accessible_world(V_650, V_138) | ~accessible_world(skc8, V_650) | ~human_person(skc6, V_651)))). % 10.10/3.67 tff(c_1877, plain, (![V_78, V_618, V_617]: (singleton(V_78, V_618) | ~accessible_world(V_617, V_78) | ~accessible_world(skc8, V_617) | ~entity(skc6, V_618)))). % 10.10/3.68 tff(c_1795, plain, (![V_87, V_604, V_603]: (unisex(V_87, V_604) | ~accessible_world(V_603, V_87) | ~accessible_world(skc8, V_603) | ~abstraction(skc6, V_604)))). % 10.10/3.68 tff(c_1641, plain, (![V_81, V_584, V_583]: (specific(V_81, V_584) | ~accessible_world(V_583, V_81) | ~accessible_world(skc8, V_583) | ~entity(skc6, V_584)))). % 10.10/3.68 tff(c_1691, plain, (![V_69, V_590, V_589]: (event(V_69, V_590) | ~accessible_world(V_589, V_69) | ~accessible_world(skc8, V_589) | ~desire_want(skc6, V_590)))). % 10.10/3.68 tff(c_1582, plain, (![V_69, V_570, V_569]: (event(V_69, V_570) | ~accessible_world(V_569, V_69) | ~accessible_world(skc8, V_569) | ~dance(skc6, V_570)))). % 10.10/3.68 tff(c_1615, plain, (![V_126, V_576, V_575]: (organism(V_126, V_576) | ~accessible_world(V_575, V_126) | ~accessible_world(skc8, V_575) | ~human_person(skc6, V_576)))). % 10.10/3.68 tff(c_1649, plain, (![V_75, V_586, V_585]: (thing(V_75, V_586) | ~accessible_world(V_585, V_75) | ~accessible_world(skc8, V_585) | ~entity(skc6, V_586)))). % 10.10/3.68 tff(c_1536, plain, (![V_87, V_566, V_565]: (unisex(V_87, V_566) | ~accessible_world(V_565, V_87) | ~accessible_world(skc8, V_565) | ~eventuality(skc6, V_566)))). % 10.10/3.68 tff(c_1733, plain, (![V_72, V_592, V_591]: (eventuality(V_72, V_592) | ~accessible_world(V_591, V_72) | ~accessible_world(skc8, V_591) | ~event(skc6, V_592)))). % 10.10/3.68 tff(c_1593, plain, (![V_75, V_572, V_571]: (thing(V_75, V_572) | ~accessible_world(V_571, V_75) | ~accessible_world(skc8, V_571) | ~abstraction(skc6, V_572)))). % 10.10/3.68 tff(c_1544, plain, (![V_75, V_568, V_567]: (thing(V_75, V_568) | ~accessible_world(V_567, V_75) | ~accessible_world(skc8, V_567) | ~eventuality(skc6, V_568)))). % 10.10/3.68 tff(c_1601, plain, (![V_105, V_574, V_573]: (nonhuman(V_105, V_574) | ~accessible_world(V_573, V_105) | ~accessible_world(skc8, V_573) | ~abstraction(skc6, V_574)))). % 10.43/3.68 tff(c_1765, plain, (![V_99, V_596, V_595]: (relation(V_99, V_596) | ~accessible_world(V_595, V_99) | ~accessible_world(skc8, V_595) | ~proposition(skc6, V_596)))). % 10.43/3.68 tff(c_1756, plain, (![V_108, V_594, V_593]: (general(V_108, V_594) | ~accessible_world(V_593, V_108) | ~accessible_world(skc8, V_593) | ~abstraction(skc6, V_594)))). % 10.43/3.68 tff(c_1633, plain, (![V_84, V_582, V_581]: (nonexistent(V_84, V_582) | ~accessible_world(V_581, V_84) | ~accessible_world(skc8, V_581) | ~eventuality(skc6, V_582)))). % 10.43/3.68 tff(c_1788, plain, (![V_132, V_602, V_601]: (existent(V_132, V_602) | ~accessible_world(V_601, V_132) | ~accessible_world(skc8, V_601) | ~entity(skc6, V_602)))). % 10.43/3.68 tff(c_1528, plain, (![V_114, V_564, V_563]: (relname(V_114, V_564) | ~accessible_world(V_563, V_114) | ~accessible_world(skc8, V_563) | ~forename(skc6, V_564)))). % 10.43/3.68 tff(c_1040, plain, (![V_129, V_458]: (entity(V_129, skc10) | ~accessible_world(V_458, V_129) | ~accessible_world(skc8, V_458)))). % 10.43/3.68 tff(c_2147, plain, (![U_1, V_2]: (~accessible_world(skc8, U_1) | ~entity(skc6, V_2) | ~dance(U_1, V_2)))). % 10.43/3.68 tff(c_2146, plain, (![U_15, V_16]: (~accessible_world(skc8, U_15) | ~entity(skc6, V_16) | ~desire_want(U_15, V_16)))). % 10.43/3.68 tff(c_2180, plain, (![U_15, V_16]: (~accessible_world(skc8, U_15) | ~abstraction(skc6, V_16) | ~desire_want(U_15, V_16)))). % 10.43/3.68 tff(c_2181, plain, (![U_1, V_2]: (~accessible_world(skc8, U_1) | ~abstraction(skc6, V_2) | ~dance(U_1, V_2)))). % 10.43/3.68 tff(c_1520, plain, (![V_81, V_562, V_561]: (specific(V_81, V_562) | ~accessible_world(V_561, V_81) | ~accessible_world(skc8, V_561) | ~eventuality(skc6, V_562)))). % 10.43/3.68 tff(c_1988, plain, (![U_25, V_26]: (~accessible_world(skc8, U_25) | ~entity(skc6, V_26) | ~abstraction(U_25, V_26)))). % 10.43/3.68 tff(c_2014, plain, (![U_3, V_4]: (~accessible_world(skc8, U_3) | ~abstraction(skc6, V_4) | ~event(U_3, V_4)))). % 10.43/3.68 tff(c_1817, plain, (![U_25, V_26]: (~accessible_world(skc8, U_25) | ~eventuality(skc6, V_26) | ~abstraction(U_25, V_26)))). % 10.43/3.68 tff(c_1873, plain, (![U_3, V_4]: (~accessible_world(skc8, U_3) | ~entity(skc6, V_4) | ~event(U_3, V_4)))). % 10.43/3.69 tff(c_1889, plain, (![V_621, V_622]: (abstraction(V_621, V_622) | ~accessible_world(skc8, V_621) | ~forename(skc6, V_622)))). % 10.43/3.69 tff(c_2001, plain, (![U_45, V_46]: (~accessible_world(skc8, U_45) | ~eventuality(skc6, V_46) | ~entity(U_45, V_46)))). % 10.43/3.69 tff(c_448, plain, (![V_141, V_303]: (human(V_141, skc10) | ~accessible_world(V_303, V_141) | ~accessible_world(skc6, V_303)))). % 10.43/3.69 tff(c_1694, plain, (![V_589, V_590]: (~abstraction(V_589, V_590) | ~accessible_world(skc8, V_589) | ~desire_want(skc6, V_590)))). % 10.43/3.69 tff(c_2087, plain, (~desire_want(skc6, skc8))). % 10.43/3.69 tff(c_2072, plain, (~event(skc6, skc8))). % 10.43/3.69 tff(c_2070, plain, (~desire_want(skc6, skc9))). % 10.43/3.69 tff(c_2055, plain, (~event(skc6, skc9))). % 10.43/3.69 tff(c_1735, plain, (![V_591, V_592]: (~abstraction(V_591, V_592) | ~accessible_world(skc8, V_591) | ~event(skc6, V_592)))). % 10.43/3.69 tff(c_1766, plain, (![V_595, V_596]: (abstraction(V_595, V_596) | ~accessible_world(skc8, V_595) | ~proposition(skc6, V_596)))). % 10.43/3.69 tff(c_1734, plain, (![V_591, V_592]: (~entity(V_591, V_592) | ~accessible_world(skc8, V_591) | ~event(skc6, V_592)))). % 10.43/3.69 tff(c_1796, plain, (![V_603, V_604]: (~female(V_603, V_604) | ~accessible_world(skc8, V_603) | ~abstraction(skc6, V_604)))). % 10.43/3.69 tff(c_1617, plain, (![V_575, V_576]: (living(V_575, V_576) | ~accessible_world(skc8, V_575) | ~human_person(skc6, V_576)))). % 10.43/3.69 tff(c_1757, plain, (![V_593, V_594]: (~eventuality(V_593, V_594) | ~accessible_world(skc8, V_593) | ~abstraction(skc6, V_594)))). % 10.43/3.69 tff(c_1634, plain, (![V_581, V_582]: (~existent(V_581, V_582) | ~accessible_world(skc8, V_581) | ~eventuality(skc6, V_582)))). % 10.43/3.69 tff(c_1642, plain, (![V_583, V_584]: (~general(V_583, V_584) | ~accessible_world(skc8, V_583) | ~entity(skc6, V_584)))). % 10.43/3.69 tff(c_875, plain, (![W_434, V_414, V_435]: (skc8=W_434 | ~desire_want(V_414, skc7) | ~proposition(V_414, skc8) | ~proposition(V_414, W_434) | ~desire_want(V_414, V_435) | ~theme(V_414, V_435, W_434) | ~accessible_world(skc6, V_414)))). % 10.43/3.69 tff(c_1963, plain, (~dance(skc6, skc8))). % 10.43/3.69 tff(c_1118, plain, (![V_78, V_475]: (singleton(V_78, V_475) | ~accessible_world(skc8, V_78) | ~eventuality(skc6, V_475)))). % 10.43/3.69 tff(c_1958, plain, (~dance(skc6, skc9))). % 10.43/3.69 tff(c_1585, plain, (![V_569, V_570]: (~abstraction(V_569, V_570) | ~accessible_world(skc8, V_569) | ~dance(skc6, V_570)))). % 10.43/3.69 tff(c_832, plain, (![W_427, V_407]: (skc9=W_427 | ~entity(V_407, skc10) | ~forename(V_407, W_427) | ~of(V_407, W_427, skc10) | ~forename(V_407, skc9) | ~accessible_world(skc6, V_407)))). % 10.43/3.69 tff(c_1584, plain, (![V_569, V_570]: (~entity(V_569, V_570) | ~accessible_world(skc8, V_569) | ~dance(skc6, V_570)))). % 10.43/3.69 tff(c_623, plain, (![V_351, V_327]: (entity(V_351, skc10) | ~accessible_world(V_327, V_351) | ~accessible_world(skc6, V_327)))). % 10.43/3.69 tff(c_1594, plain, (![V_571, V_572]: (singleton(V_571, V_572) | ~accessible_world(skc8, V_571) | ~abstraction(skc6, V_572)))). % 10.43/3.69 tff(c_1618, plain, (![V_575, V_576]: (impartial(V_575, V_576) | ~accessible_world(skc8, V_575) | ~human_person(skc6, V_576)))). % 10.43/3.69 tff(c_1602, plain, (![V_573, V_574]: (~human(V_573, V_574) | ~accessible_world(skc8, V_573) | ~abstraction(skc6, V_574)))). % 10.43/3.69 tff(c_440, plain, (![V_144, V_302]: (animate(V_144, skc10) | ~accessible_world(V_302, V_144) | ~accessible_world(skc6, V_302)))). % 10.43/3.69 tff(c_1157, plain, (![V_99, V_485]: (relation(V_99, V_485) | ~accessible_world(skc8, V_99) | ~forename(skc6, V_485)))). % 10.43/3.69 tff(c_802, plain, (![V_154, V_418]: (theme(V_154, skc7, skc8) | ~accessible_world(V_418, V_154) | ~accessible_world(skc6, V_418)))). % 10.43/3.69 tff(c_1650, plain, (![V_585, V_586]: (singleton(V_585, V_586) | ~accessible_world(skc8, V_585) | ~entity(skc6, V_586)))). % 10.43/3.69 tff(c_1787, plain, (![V_601, V_602]: (~eventuality(V_601, V_602) | ~accessible_world(skc8, V_601) | ~entity(skc6, V_602)))). % 10.43/3.69 tff(c_1693, plain, (![V_589, V_590]: (~entity(V_589, V_590) | ~accessible_world(skc8, V_589) | ~desire_want(skc6, V_590)))). % 10.43/3.69 tff(c_1758, plain, (![V_593, V_594]: (~entity(V_593, V_594) | ~accessible_world(skc8, V_593) | ~abstraction(skc6, V_594)))). % 10.43/3.69 tff(c_1537, plain, (![V_565, V_566]: (~female(V_565, V_566) | ~accessible_world(skc8, V_565) | ~eventuality(skc6, V_566)))). % 10.43/3.69 tff(c_1521, plain, (![V_561, V_562]: (~general(V_561, V_562) | ~accessible_world(skc8, V_561) | ~eventuality(skc6, V_562)))). % 10.43/3.69 tff(c_1616, plain, (![V_575, V_576]: (entity(V_575, V_576) | ~accessible_world(skc8, V_575) | ~human_person(skc6, V_576)))). % 10.43/3.69 tff(c_1197, plain, (![V_87, V_495]: (unisex(V_87, V_495) | ~accessible_world(skc8, V_87) | ~abstraction(skc6, V_495)))). % 10.43/3.70 tff(c_843, plain, (![V_132, V_431]: (existent(V_132, V_431) | ~accessible_world(skc8, V_132) | ~entity(skc6, V_431)))). % 10.43/3.70 tff(c_758, plain, (![V_150, V_402]: (agent(V_150, skc11, skc10) | ~accessible_world(V_402, V_150) | ~accessible_world(skc8, V_402)))). % 10.43/3.70 tff(c_593, plain, (![V_337, V_325]: (female(V_337, skc10) | ~accessible_world(V_325, V_337) | ~accessible_world(skc6, V_325)))). % 10.43/3.70 tff(c_730, plain, (![V_99, V_395]: (relation(V_99, V_395) | ~accessible_world(skc8, V_99) | ~proposition(skc6, V_395)))). % 10.43/3.70 tff(c_1343, plain, (![V_108, V_516]: (general(V_108, V_516) | ~accessible_world(skc8, V_108) | ~abstraction(skc6, V_516)))). % 10.43/3.70 tff(c_1231, plain, (![V_72, V_500]: (eventuality(V_72, V_500) | ~accessible_world(skc8, V_72) | ~event(skc6, V_500)))). % 10.43/3.70 tff(c_920, plain, (![V_69, V_444]: (event(V_69, V_444) | ~accessible_world(skc8, V_69) | ~desire_want(skc6, V_444)))). % 10.43/3.70 tff(c_608, plain, (![V_344, V_293]: (forename(V_344, skc9) | ~accessible_world(V_293, V_344) | ~accessible_world(skc6, V_293)))). % 10.43/3.70 tff(c_1001, plain, (![V_75, V_456]: (thing(V_75, V_456) | ~accessible_world(skc8, V_75) | ~entity(skc6, V_456)))). % 10.43/3.70 tff(c_769, plain, (![V_81, V_406]: (specific(V_81, V_406) | ~accessible_world(skc8, V_81) | ~entity(skc6, V_406)))). % 10.43/3.70 tff(c_1277, plain, (![V_84, V_506]: (nonexistent(V_84, V_506) | ~accessible_world(skc8, V_84) | ~eventuality(skc6, V_506)))). % 10.43/3.70 tff(c_754, plain, (![V_150, V_401]: (agent(V_150, skc7, skc10) | ~accessible_world(V_401, V_150) | ~accessible_world(skc6, V_401)))). % 10.43/3.70 tff(c_656, plain, (![V_369, V_325]: (human_person(V_369, skc10) | ~accessible_world(V_325, V_369) | ~accessible_world(skc6, V_325)))). % 10.43/3.70 tff(c_950, plain, (![V_126, V_449]: (organism(V_126, V_449) | ~accessible_world(skc8, V_126) | ~human_person(skc6, V_449)))). % 10.43/3.70 tff(c_813, plain, (![V_105, V_422]: (nonhuman(V_105, V_422) | ~accessible_world(skc8, V_105) | ~abstraction(skc6, V_422)))). % 10.43/3.70 tff(c_1181, plain, (![V_75, V_490]: (thing(V_75, V_490) | ~accessible_world(skc8, V_75) | ~abstraction(skc6, V_490)))). % 10.43/3.70 tff(c_1310, plain, (![V_69, V_511]: (event(V_69, V_511) | ~accessible_world(skc8, V_69) | ~dance(skc6, V_511)))). % 10.43/3.70 tff(c_1113, plain, (![V_75, V_474]: (thing(V_75, V_474) | ~accessible_world(skc8, V_75) | ~eventuality(skc6, V_474)))). % 10.43/3.70 tff(c_1129, plain, (![V_87, V_479]: (unisex(V_87, V_479) | ~accessible_world(skc8, V_87) | ~eventuality(skc6, V_479)))). % 10.43/3.70 tff(c_1149, plain, (![V_114, V_484]: (relname(V_114, V_484) | ~accessible_world(skc8, V_114) | ~forename(skc6, V_484)))). % 10.43/3.70 tff(c_1066, plain, (![V_81, V_465]: (specific(V_81, V_465) | ~accessible_world(skc8, V_81) | ~eventuality(skc6, V_465)))). % 10.43/3.70 tff(c_794, plain, (![V_158, V_413]: (of(V_158, skc9, skc10) | ~accessible_world(V_413, V_158) | ~accessible_world(skc6, V_413)))). % 10.43/3.70 tff(c_690, plain, (![V_66, V_382]: (dance(V_66, skc11) | ~accessible_world(V_382, V_66) | ~accessible_world(skc8, V_382)))). % 10.43/3.70 tff(c_452, plain, (![V_304, V_38, U_37]: (impartial(V_304, V_38) | ~accessible_world(U_37, V_304) | ~human_person(U_37, V_38)))). % 10.43/3.70 tff(c_835, plain, (![W_427]: (skc9=W_427 | ~forename(skc6, W_427) | ~of(skc6, W_427, skc10)))). % 10.43/3.70 tff(c_473, plain, (![V_309, V_6, U_5]: (singleton(V_309, V_6) | ~accessible_world(U_5, V_309) | ~eventuality(U_5, V_6)))). % 10.43/3.70 tff(c_474, plain, (![V_309, V_42, U_41]: (singleton(V_309, V_42) | ~accessible_world(U_41, V_309) | ~entity(U_41, V_42)))). % 10.43/3.70 tff(c_475, plain, (![V_309, V_229, U_228]: (singleton(V_309, V_229) | ~accessible_world(U_228, V_309) | ~abstraction(U_228, V_229)))). % 10.43/3.70 tff(c_712, plain, (![V_69, V_387]: (event(V_69, skc11) | ~accessible_world(V_387, V_69) | ~accessible_world(skc8, V_387)))). % 10.43/3.70 tff(c_358, plain, (![V_90, V_277]: (present(V_90, skc11) | ~accessible_world(V_277, V_90) | ~accessible_world(skc8, V_277)))). % 10.43/3.70 tff(c_643, plain, (![V_363, V_38, U_37]: (living(V_363, V_38) | ~accessible_world(U_37, V_363) | ~human_person(U_37, V_38)))). % 10.43/3.70 tff(c_616, plain, (![V_348, V_175, U_174]: (relation(V_348, V_175) | ~accessible_world(U_174, V_348) | ~forename(U_174, V_175)))). % 10.43/3.70 tff(c_682, plain, (![V_96, V_381]: (proposition(V_96, skc8) | ~accessible_world(V_381, V_96) | ~accessible_world(skc6, V_381)))). % 10.43/3.70 tff(c_400, plain, (![V_117, V_293]: (mia_forename(V_117, skc9) | ~accessible_world(V_293, V_117) | ~accessible_world(skc6, V_293)))). % 10.43/3.70 tff(c_362, plain, (![V_90, V_278]: (present(V_90, skc7) | ~accessible_world(V_278, V_90) | ~accessible_world(skc6, V_278)))). % 10.43/3.70 tff(c_516, plain, (![V_120, V_325]: (woman(V_120, skc10) | ~accessible_world(V_325, V_120) | ~accessible_world(skc6, V_325)))). % 10.43/3.70 tff(c_1439, plain, (~accessible_world(skc6, skc6))). % 10.43/3.70 tff(c_570, plain, (![V_93, V_333]: (desire_want(V_93, skc7) | ~accessible_world(V_333, V_93) | ~accessible_world(skc6, V_333)))). % 10.43/3.70 tff(c_1398, plain, (![V_16]: (~abstraction(skc6, V_16) | ~desire_want(skc8, V_16)))). % 10.43/3.70 tff(c_1399, plain, (![V_2]: (~abstraction(skc6, V_2) | ~dance(skc8, V_2)))). % 10.43/3.70 tff(c_878, plain, (![W_434, V_435]: (skc8=W_434 | ~proposition(skc6, W_434) | ~desire_want(skc6, V_435) | ~theme(skc6, V_435, W_434)))). % 10.43/3.70 tff(c_1400, plain, (~abstraction(skc6, skc11))). % 10.43/3.70 tff(c_1355, plain, (![V_4]: (~abstraction(skc6, V_4) | ~event(skc8, V_4)))). % 10.43/3.71 tff(c_1345, plain, (![V_516]: (~entity(skc8, V_516) | ~abstraction(skc6, V_516)))). % 10.43/3.71 tff(c_1344, plain, (![V_516]: (~eventuality(skc8, V_516) | ~abstraction(skc6, V_516)))). % 10.43/3.71 tff(c_1325, plain, (![V_514]: (general(skc8, V_514) | ~abstraction(skc6, V_514)))). % 10.43/3.71 tff(c_635, plain, (![V_357, V_26, U_25]: (general(V_357, V_26) | ~accessible_world(U_25, V_357) | ~abstraction(U_25, V_26)))). % 10.43/3.71 tff(c_1288, plain, (![V_46]: (~eventuality(skc6, V_46) | ~entity(skc8, V_46)))). % 10.43/3.71 tff(c_1292, plain, (![V_509]: (event(skc8, V_509) | ~dance(skc6, V_509)))). % 10.43/3.71 tff(c_701, plain, (![V_384, V_2, U_1]: (event(V_384, V_2) | ~accessible_world(U_1, V_384) | ~dance(U_1, V_2)))). % 10.43/3.71 tff(c_1278, plain, (![V_506]: (~existent(skc8, V_506) | ~eventuality(skc6, V_506)))). % 10.43/3.71 tff(c_1270, plain, (![V_504]: (nonexistent(skc8, V_504) | ~eventuality(skc6, V_504)))). % 10.43/3.71 tff(c_423, plain, (![V_297, V_12, U_11]: (nonexistent(V_297, V_12) | ~accessible_world(U_11, V_297) | ~eventuality(U_11, V_12)))). % 10.43/3.71 tff(c_1249, plain, (![V_2]: (~entity(skc8, V_2) | ~dance(skc6, V_2)))). % 10.43/3.71 tff(c_1232, plain, (![V_500]: (~entity(skc8, V_500) | ~event(skc6, V_500)))). % 10.43/3.71 tff(c_1210, plain, (![V_498]: (eventuality(skc8, V_498) | ~event(skc6, V_498)))). % 10.43/3.71 tff(c_497, plain, (![V_317, V_4, U_3]: (eventuality(V_317, V_4) | ~accessible_world(U_3, V_317) | ~event(U_3, V_4)))). % 10.43/3.71 tff(c_1198, plain, (![V_495]: (~female(skc8, V_495) | ~abstraction(skc6, V_495)))). % 10.43/3.71 tff(c_1190, plain, (![V_493]: (unisex(skc8, V_493) | ~abstraction(skc6, V_493)))). % 10.43/3.71 tff(c_631, plain, (![V_354, V_28, U_27]: (unisex(V_354, V_28) | ~accessible_world(U_27, V_354) | ~abstraction(U_27, V_28)))). % 10.43/3.71 tff(c_1182, plain, (![V_490]: (singleton(skc8, V_490) | ~abstraction(skc6, V_490)))). % 10.43/3.71 tff(c_1174, plain, (![V_488]: (thing(skc8, V_488) | ~abstraction(skc6, V_488)))). % 10.43/3.71 tff(c_665, plain, (![V_372, V_22, U_21]: (thing(V_372, V_22) | ~accessible_world(U_21, V_372) | ~abstraction(U_21, V_22)))). % 10.43/3.71 tff(c_1158, plain, (![V_485]: (abstraction(skc8, V_485) | ~forename(skc6, V_485)))). % 10.43/3.71 tff(c_1150, plain, (![V_484]: (relation(skc8, V_484) | ~forename(skc6, V_484)))). % 10.43/3.71 tff(c_1142, plain, (![V_482]: (relname(skc8, V_482) | ~forename(skc6, V_482)))). % 10.43/3.71 tff(c_287, plain, (![V_238, V_30, U_29]: (relname(V_238, V_30) | ~accessible_world(U_29, V_238) | ~forename(U_29, V_30)))). % 10.43/3.71 tff(c_1130, plain, (![V_479]: (~female(skc8, V_479) | ~eventuality(skc6, V_479)))). % 10.43/3.71 tff(c_1122, plain, (![V_477]: (unisex(skc8, V_477) | ~eventuality(skc6, V_477)))). % 10.43/3.71 tff(c_630, plain, (![V_354, V_14, U_13]: (unisex(V_354, V_14) | ~accessible_world(U_13, V_354) | ~eventuality(U_13, V_14)))). % 10.43/3.71 tff(c_1114, plain, (![V_474]: (singleton(skc8, V_474) | ~eventuality(skc6, V_474)))). % 10.43/3.71 tff(c_1106, plain, (![V_472]: (thing(skc8, V_472) | ~eventuality(skc6, V_472)))). % 10.43/3.71 tff(c_666, plain, (![V_372, V_6, U_5]: (thing(V_372, V_6) | ~accessible_world(U_5, V_372) | ~eventuality(U_5, V_6)))). % 10.43/3.71 tff(c_1095, plain, (![V_2]: (~abstraction(skc8, V_2) | ~dance(skc6, V_2)))). % 10.43/3.71 tff(c_1042, plain, (![V_458]: (~desire_want(V_458, skc10) | ~accessible_world(skc8, V_458)))). % 10.43/3.71 tff(c_1079, plain, (![V_4]: (~abstraction(skc8, V_4) | ~event(skc6, V_4)))). % 10.43/3.71 tff(c_1073, plain, (![V_26]: (~eventuality(skc6, V_26) | ~abstraction(skc8, V_26)))). % 10.43/3.71 tff(c_1067, plain, (![V_465]: (~general(skc8, V_465) | ~eventuality(skc6, V_465)))). % 10.43/3.71 tff(c_1059, plain, (![V_463]: (specific(skc8, V_463) | ~eventuality(skc6, V_463)))). % 10.43/3.71 tff(c_649, plain, (![V_366, V_10, U_9]: (specific(V_366, V_10) | ~accessible_world(U_9, V_366) | ~eventuality(U_9, V_10)))). % 10.43/3.71 tff(c_1041, plain, (![V_458]: (~dance(V_458, skc10) | ~accessible_world(skc8, V_458)))). % 10.43/3.71 tff(c_1043, plain, (![V_458]: (~abstraction(V_458, skc10) | ~accessible_world(skc8, V_458)))). % 10.43/3.71 tff(c_925, plain, (![V_444]: (~abstraction(skc8, V_444) | ~desire_want(skc6, V_444)))). % 10.43/3.71 tff(c_979, plain, (![V_129]: (entity(V_129, skc10) | ~accessible_world(skc8, V_129)))). % 10.43/3.71 tff(c_1002, plain, (![V_456]: (singleton(skc8, V_456) | ~entity(skc6, V_456)))). % 10.43/3.71 tff(c_994, plain, (![V_454]: (thing(skc8, V_454) | ~entity(skc6, V_454)))). % 10.43/3.71 tff(c_667, plain, (![V_372, V_42, U_41]: (thing(V_372, V_42) | ~accessible_world(U_41, V_372) | ~entity(U_41, V_42)))). % 10.43/3.71 tff(c_953, plain, (![V_449]: (impartial(skc8, V_449) | ~human_person(skc6, V_449)))). % 10.43/3.71 tff(c_952, plain, (![V_449]: (living(skc8, V_449) | ~human_person(skc6, V_449)))). % 10.43/3.71 tff(c_963, plain, (entity(skc8, skc10))). % 10.43/3.71 tff(c_951, plain, (![V_449]: (entity(skc8, V_449) | ~human_person(skc6, V_449)))). % 10.43/3.72 tff(c_937, plain, (![V_447]: (organism(skc8, V_447) | ~human_person(skc6, V_447)))). % 10.43/3.72 tff(c_718, plain, (![V_388, V_38, U_37]: (organism(V_388, V_38) | ~accessible_world(U_37, V_388) | ~human_person(U_37, V_38)))). % 10.43/3.72 tff(c_924, plain, (![V_444]: (~entity(skc8, V_444) | ~desire_want(skc6, V_444)))). % 10.43/3.72 tff(c_902, plain, (![V_442]: (event(skc8, V_442) | ~desire_want(skc6, V_442)))). % 10.43/3.72 tff(c_898, plain, (~desire_want(skc8, skc10))). % 10.43/3.72 tff(c_700, plain, (![V_384, V_16, U_15]: (event(V_384, V_16) | ~accessible_world(U_15, V_384) | ~desire_want(U_15, V_16)))). % 10.43/3.72 tff(c_867, plain, (![V_16]: (~entity(skc6, V_16) | ~desire_want(skc8, V_16)))). % 10.43/3.72 tff(c_888, plain, (~dance(skc8, skc10))). % 10.43/3.72 tff(c_868, plain, (![V_2]: (~entity(skc6, V_2) | ~dance(skc8, V_2)))). % 10.43/3.72 tff(c_869, plain, (~entity(skc6, skc11))). % 10.43/3.72 tff(c_130, plain, (![X_167, W_165, V_169, U_166, Y_168]: (X_167=W_165 | ~theme(U_166, Y_168, X_167) | ~desire_want(U_166, Y_168) | ~proposition(U_166, X_167) | ~proposition(U_166, W_165) | ~desire_want(U_166, V_169) | ~theme(U_166, V_169, W_165)))). % 10.43/3.72 tff(c_849, plain, (![V_4]: (~entity(skc6, V_4) | ~event(skc8, V_4)))). % 10.43/3.72 tff(c_842, plain, (![V_431]: (~eventuality(skc8, V_431) | ~entity(skc6, V_431)))). % 10.43/3.72 tff(c_826, plain, (![V_425]: (existent(skc8, V_425) | ~entity(skc6, V_425)))). % 10.43/3.72 tff(c_128, plain, (![W_163, V_162, U_161, X_164]: (W_163=V_162 | ~entity(U_161, X_164) | ~of(U_161, V_162, X_164) | ~forename(U_161, W_163) | ~of(U_161, W_163, X_164) | ~forename(U_161, V_162)))). % 10.43/3.72 tff(c_321, plain, (![V_259, V_46, U_45]: (existent(V_259, V_46) | ~accessible_world(U_45, V_259) | ~entity(U_45, V_46)))). % 10.43/3.72 tff(c_814, plain, (![V_422]: (~human(skc8, V_422) | ~abstraction(skc6, V_422)))). % 10.43/3.72 tff(c_806, plain, (![V_420]: (nonhuman(skc8, V_420) | ~abstraction(skc6, V_420)))). % 10.43/3.72 tff(c_639, plain, (![V_360, V_24, U_23]: (nonhuman(V_360, V_24) | ~accessible_world(U_23, V_360) | ~abstraction(U_23, V_24)))). % 10.43/3.72 tff(c_798, plain, (![V_414]: (theme(V_414, skc7, skc8) | ~accessible_world(skc6, V_414)))). % 10.43/3.72 tff(c_124, plain, (![V_154, W_155, X_156, U_153]: (theme(V_154, W_155, X_156) | ~theme(U_153, W_155, X_156) | ~accessible_world(U_153, V_154)))). % 10.43/3.72 tff(c_774, plain, (![V_407]: (of(V_407, skc9, skc10) | ~accessible_world(skc6, V_407)))). % 10.43/3.72 tff(c_780, plain, (![V_26]: (~entity(skc6, V_26) | ~abstraction(skc8, V_26)))). % 10.43/3.72 tff(c_770, plain, (![V_406]: (~general(skc8, V_406) | ~entity(skc6, V_406)))). % 10.43/3.72 tff(c_126, plain, (![V_158, W_159, X_160, U_157]: (of(V_158, W_159, X_160) | ~of(U_157, W_159, X_160) | ~accessible_world(U_157, V_158)))). % 10.43/3.72 tff(c_762, plain, (![V_404]: (specific(skc8, V_404) | ~entity(skc6, V_404)))). % 10.43/3.72 tff(c_650, plain, (![V_366, V_44, U_43]: (specific(V_366, V_44) | ~accessible_world(U_43, V_366) | ~entity(U_43, V_44)))). % 10.43/3.72 tff(c_738, plain, (![V_396]: (agent(V_396, skc11, skc10) | ~accessible_world(skc8, V_396)))). % 10.43/3.72 tff(c_737, plain, (![V_396]: (agent(V_396, skc7, skc10) | ~accessible_world(skc6, V_396)))). % 10.43/3.72 tff(c_731, plain, (![V_395]: (abstraction(skc8, V_395) | ~proposition(skc6, V_395)))). % 10.43/3.72 tff(c_122, plain, (![V_150, W_151, X_152, U_149]: (agent(V_150, W_151, X_152) | ~agent(U_149, W_151, X_152) | ~accessible_world(U_149, V_150)))). % 10.43/3.72 tff(c_723, plain, (![V_393]: (relation(skc8, V_393) | ~proposition(skc6, V_393)))). % 10.43/3.72 tff(c_617, plain, (![V_348, V_18, U_17]: (relation(V_348, V_18) | ~accessible_world(U_17, V_348) | ~proposition(U_17, V_18)))). % 10.43/3.72 tff(c_713, plain, (![V_387]: (~entity(V_387, skc11) | ~accessible_world(skc8, V_387)))). % 10.43/3.72 tff(c_106, plain, (![V_126, W_127, U_125]: (organism(V_126, W_127) | ~organism(U_125, W_127) | ~accessible_world(U_125, V_126)))). % 10.43/3.72 tff(c_702, plain, (![V_384]: (event(V_384, skc11) | ~accessible_world(skc8, V_384)))). % 10.43/3.72 tff(c_68, plain, (![V_69, W_70, U_68]: (event(V_69, W_70) | ~event(U_68, W_70) | ~accessible_world(U_68, V_69)))). % 10.43/3.72 tff(c_691, plain, (![V_382]: (~abstraction(V_382, skc11) | ~accessible_world(skc8, V_382)))). % 10.43/3.72 tff(c_675, plain, (![V_378]: (dance(V_378, skc11) | ~accessible_world(skc8, V_378)))). % 10.43/3.72 tff(c_671, plain, (![V_375]: (proposition(V_375, skc8) | ~accessible_world(skc6, V_375)))). % 10.43/3.72 tff(c_66, plain, (![V_66, W_67, U_65]: (dance(V_66, W_67) | ~dance(U_65, W_67) | ~accessible_world(U_65, V_66)))). % 10.43/3.72 tff(c_86, plain, (![V_96, W_97, U_95]: (proposition(V_96, W_97) | ~proposition(U_95, W_97) | ~accessible_world(U_95, V_96)))). % 10.43/3.72 tff(c_72, plain, (![V_75, W_76, U_74]: (thing(V_75, W_76) | ~thing(U_74, W_76) | ~accessible_world(U_74, V_75)))). % 10.43/3.72 tff(c_104, plain, (![V_123, W_124, U_122]: (human_person(V_123, W_124) | ~human_person(U_122, W_124) | ~accessible_world(U_122, V_123)))). % 10.43/3.72 tff(c_76, plain, (![V_81, W_82, U_80]: (specific(V_81, W_82) | ~specific(U_80, W_82) | ~accessible_world(U_80, V_81)))). % 10.43/3.72 tff(c_114, plain, (![V_138, W_139, U_137]: (living(V_138, W_139) | ~living(U_137, W_139) | ~accessible_world(U_137, V_138)))). % 10.43/3.72 tff(c_92, plain, (![V_105, W_106, U_104]: (nonhuman(V_105, W_106) | ~nonhuman(U_104, W_106) | ~accessible_world(U_104, V_105)))). % 10.43/3.72 tff(c_94, plain, (![V_108, W_109, U_107]: (general(V_108, W_109) | ~general(U_107, W_109) | ~accessible_world(U_107, V_108)))). % 10.43/3.72 tff(c_80, plain, (![V_87, W_88, U_86]: (unisex(V_87, W_88) | ~unisex(U_86, W_88) | ~accessible_world(U_86, V_87)))). % 10.43/3.73 tff(c_108, plain, (![V_129, W_130, U_128]: (entity(V_129, W_130) | ~entity(U_128, W_130) | ~accessible_world(U_128, V_129)))). % 10.43/3.73 tff(c_88, plain, (![V_99, W_100, U_98]: (relation(V_99, W_100) | ~relation(U_98, W_100) | ~accessible_world(U_98, V_99)))). % 10.43/3.73 tff(c_460, plain, (![V_102]: (abstraction(V_102, skc8) | ~accessible_world(skc8, V_102)))). % 10.43/3.73 tff(c_96, plain, (![V_111, W_112, U_110]: (forename(V_111, W_112) | ~forename(U_110, W_112) | ~accessible_world(U_110, V_111)))). % 10.43/3.73 tff(c_602, plain, (~abstraction(skc8, skc7))). % 10.43/3.73 tff(c_571, plain, (![V_333]: (~abstraction(V_333, skc7) | ~accessible_world(skc6, V_333)))). % 10.43/3.73 tff(c_586, plain, (![U_15]: (~accessible_world(skc6, U_15) | ~desire_want(U_15, skc10)))). % 10.43/3.73 tff(c_587, plain, (![U_1]: (~accessible_world(skc6, U_1) | ~dance(U_1, skc10)))). % 10.43/3.73 tff(c_478, plain, (![V_102]: (abstraction(V_102, skc9) | ~accessible_world(skc8, V_102)))). % 10.43/3.73 tff(c_120, plain, (![V_147, W_148, U_146]: (female(V_147, W_148) | ~female(U_146, W_148) | ~accessible_world(U_146, V_147)))). % 10.43/3.73 tff(c_546, plain, (![U_3]: (~accessible_world(skc6, U_3) | ~event(U_3, skc10)))). % 10.43/3.73 tff(c_418, plain, (![U_1, V_2]: (~abstraction(U_1, V_2) | ~dance(U_1, V_2)))). % 10.43/3.73 tff(c_563, plain, (![V_330]: (desire_want(V_330, skc7) | ~accessible_world(skc6, V_330)))). % 10.43/3.73 tff(c_84, plain, (![V_93, W_94, U_92]: (desire_want(V_93, W_94) | ~desire_want(U_92, W_94) | ~accessible_world(U_92, V_93)))). % 10.43/3.73 tff(c_538, plain, (![V_327]: (entity(V_327, skc10) | ~accessible_world(skc6, V_327)))). % 10.43/3.73 tff(c_527, plain, (![V_326]: (~eventuality(V_326, skc10) | ~accessible_world(skc6, V_326)))). % 10.43/3.73 tff(c_518, plain, (![V_325]: (human_person(V_325, skc10) | ~accessible_world(skc6, V_325)))). % 10.43/3.73 tff(c_517, plain, (![V_325]: (female(V_325, skc10) | ~accessible_world(skc6, V_325)))). % 10.43/3.73 tff(c_506, plain, (![V_322]: (woman(V_322, skc10) | ~accessible_world(skc6, V_322)))). % 10.43/3.73 tff(c_102, plain, (![V_120, W_121, U_119]: (woman(V_120, W_121) | ~woman(U_119, W_121) | ~accessible_world(U_119, V_120)))). % 10.43/3.73 tff(c_435, plain, (![U_1, V_2]: (~entity(U_1, V_2) | ~dance(U_1, V_2)))). % 10.43/3.73 tff(c_493, plain, (~abstraction(skc6, skc7))). % 10.43/3.73 tff(c_70, plain, (![V_72, W_73, U_71]: (eventuality(V_72, W_73) | ~eventuality(U_71, W_73) | ~accessible_world(U_71, V_72)))). % 10.43/3.73 tff(c_417, plain, (![U_15, V_16]: (~abstraction(U_15, V_16) | ~desire_want(U_15, V_16)))). % 10.43/3.73 tff(c_434, plain, (![U_15, V_16]: (~entity(U_15, V_16) | ~desire_want(U_15, V_16)))). % 10.43/3.73 tff(c_483, plain, (~abstraction(skc8, skc10))). % 10.43/3.73 tff(c_447, plain, (![V_303]: (~abstraction(V_303, skc10) | ~accessible_world(skc6, V_303)))). % 10.43/3.73 tff(c_465, plain, (abstraction(skc8, skc9))). % 10.43/3.73 tff(c_74, plain, (![V_78, W_79, U_77]: (singleton(V_78, W_79) | ~singleton(U_77, W_79) | ~accessible_world(U_77, V_78)))). % 10.43/3.73 tff(c_406, plain, (![V_294]: (abstraction(V_294, skc9) | ~accessible_world(skc6, V_294)))). % 10.43/3.73 tff(c_457, plain, (abstraction(skc8, skc8))). % 10.43/3.73 tff(c_366, plain, (![V_279]: (abstraction(V_279, skc8) | ~accessible_world(skc6, V_279)))). % 10.43/3.73 tff(c_112, plain, (![V_135, W_136, U_134]: (impartial(V_135, W_136) | ~impartial(U_134, W_136) | ~accessible_world(U_134, V_135)))). % 10.43/3.73 tff(c_299, plain, (![V_241]: (human(V_241, skc10) | ~accessible_world(skc6, V_241)))). % 10.43/3.73 tff(c_311, plain, (![V_252]: (animate(V_252, skc10) | ~accessible_world(skc6, V_252)))). % 10.43/3.73 tff(c_436, plain, (~entity(skc8, skc11))). % 10.43/3.73 tff(c_376, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 10.43/3.73 tff(c_419, plain, (~abstraction(skc8, skc11))). % 10.43/3.73 tff(c_78, plain, (![V_84, W_85, U_83]: (nonexistent(V_84, W_85) | ~nonexistent(U_83, W_85) | ~accessible_world(U_83, V_84)))). % 10.43/3.73 tff(c_371, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 10.43/3.73 tff(c_401, plain, (![V_293]: (forename(V_293, skc9) | ~accessible_world(skc6, V_293)))). % 10.43/3.73 tff(c_393, plain, (![V_290]: (mia_forename(V_290, skc9) | ~accessible_world(skc6, V_290)))). % 10.43/3.73 tff(c_100, plain, (![V_117, W_118, U_116]: (mia_forename(V_117, W_118) | ~mia_forename(U_116, W_118) | ~accessible_world(U_116, V_117)))). % 10.43/3.73 tff(c_386, plain, (abstraction(skc6, skc9))). % 10.43/3.73 tff(c_342, plain, (![U_270, V_271]: (abstraction(U_270, V_271) | ~forename(U_270, V_271)))). % 10.43/3.73 tff(c_331, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~abstraction(U_25, V_26)))). % 10.43/3.73 tff(c_337, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 10.43/3.73 tff(c_354, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~abstraction(U_25, V_26)))). % 10.43/3.73 tff(c_90, plain, (![V_102, W_103, U_101]: (abstraction(V_102, W_103) | ~abstraction(U_101, W_103) | ~accessible_world(U_101, V_102)))). % 10.43/3.73 tff(c_349, plain, (![V_272]: (present(V_272, skc7) | ~accessible_world(skc6, V_272)))). % 10.43/3.73 tff(c_348, plain, (![V_272]: (present(V_272, skc11) | ~accessible_world(skc8, V_272)))). % 10.43/3.73 tff(c_227, plain, (![U_9, V_10]: (~general(U_9, V_10) | ~eventuality(U_9, V_10)))). % 10.43/3.73 tff(c_82, plain, (![V_90, W_91, U_89]: (present(V_90, W_91) | ~present(U_89, W_91) | ~accessible_world(U_89, V_90)))). % 10.43/3.73 tff(c_172, plain, (![U_174, V_175]: (relation(U_174, V_175) | ~forename(U_174, V_175)))). % 10.43/3.73 tff(c_269, plain, (![U_232, V_233]: (~existent(U_232, V_233) | ~eventuality(U_232, V_233)))). % 10.43/3.73 tff(c_206, plain, (![U_37, V_38]: (living(U_37, V_38) | ~human_person(U_37, V_38)))). % 10.43/3.73 tff(c_228, plain, (![U_43, V_44]: (~general(U_43, V_44) | ~entity(U_43, V_44)))). % 10.43/3.73 tff(c_233, plain, (![U_27, V_28]: (~female(U_27, V_28) | ~abstraction(U_27, V_28)))). % 10.43/3.73 tff(c_110, plain, (![V_132, W_133, U_131]: (existent(V_132, W_133) | ~existent(U_131, W_133) | ~accessible_world(U_131, V_132)))). % 10.43/3.73 tff(c_248, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 10.43/3.73 tff(c_316, plain, (entity(skc6, skc10))). % 10.43/3.73 tff(c_254, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~human_person(U_37, V_38)))). % 10.43/3.73 tff(c_118, plain, (![V_144, W_145, U_143]: (animate(V_144, W_145) | ~animate(U_143, W_145) | ~accessible_world(U_143, V_144)))). % 10.43/3.73 tff(c_307, plain, (~abstraction(skc6, skc10))). % 10.43/3.73 tff(c_213, plain, (![U_23, V_24]: (~human(U_23, V_24) | ~abstraction(U_23, V_24)))). % 10.43/3.73 tff(c_249, plain, (![U_41, V_42]: (singleton(U_41, V_42) | ~entity(U_41, V_42)))). % 10.43/3.73 tff(c_186, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~human_person(U_37, V_38)))). % 10.43/3.73 tff(c_259, plain, (![U_228, V_229]: (singleton(U_228, V_229) | ~abstraction(U_228, V_229)))). % 10.43/3.73 tff(c_116, plain, (![V_141, W_142, U_140]: (human(V_141, W_142) | ~human(U_140, W_142) | ~accessible_world(U_140, V_141)))). % 10.43/3.73 tff(c_295, plain, (~dance(skc6, skc10))). % 10.43/3.73 tff(c_294, plain, (~desire_want(skc6, skc10))). % 10.43/3.73 tff(c_283, plain, (~event(skc6, skc10))). % 10.43/3.73 tff(c_98, plain, (![V_114, W_115, U_113]: (relname(V_114, W_115) | ~relname(U_113, W_115) | ~accessible_world(U_113, V_114)))). % 10.43/3.74 tff(c_279, plain, (~eventuality(skc6, skc10))). % 10.43/3.74 tff(c_264, plain, (![U_230, V_231]: (~female(U_230, V_231) | ~eventuality(U_230, V_231)))). % 10.43/3.74 tff(c_274, plain, (abstraction(skc6, skc8))). % 10.43/3.74 tff(c_240, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~proposition(U_17, V_18)))). % 10.43/3.74 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 10.43/3.74 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 10.43/3.74 tff(c_22, plain, (![U_21, V_22]: (thing(U_21, V_22) | ~abstraction(U_21, V_22)))). % 10.43/3.74 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~organism(U_39, V_40)))). % 10.43/3.74 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 10.43/3.74 tff(c_20, plain, (![U_19, V_20]: (abstraction(U_19, V_20) | ~relation(U_19, V_20)))). % 10.43/3.74 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 10.43/3.74 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 10.43/3.74 tff(c_58, plain, (![U_57, V_58]: (~unisex(U_57, V_58) | ~female(U_57, V_58)))). % 10.43/3.74 tff(c_60, plain, (![U_59, V_60]: (~specific(U_59, V_60) | ~general(U_59, V_60)))). % 10.43/3.74 tff(c_219, plain, (human(skc6, skc10))). % 10.43/3.74 tff(c_52, plain, (![U_51, V_52]: (human(U_51, V_52) | ~human_person(U_51, V_52)))). % 10.43/3.74 tff(c_64, plain, (![U_63, V_64]: (~existent(U_63, V_64) | ~nonexistent(U_63, V_64)))). % 10.43/3.74 tff(c_62, plain, (![U_61, V_62]: (~nonhuman(U_61, V_62) | ~human(U_61, V_62)))). % 10.43/3.74 tff(c_16, plain, (![U_15, V_16]: (event(U_15, V_16) | ~desire_want(U_15, V_16)))). % 10.43/3.74 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 10.43/3.74 tff(c_50, plain, (![U_49, V_50]: (living(U_49, V_50) | ~organism(U_49, V_50)))). % 10.43/3.74 tff(c_201, plain, (female(skc6, skc10))). % 10.43/3.74 tff(c_56, plain, (![U_55, V_56]: (female(U_55, V_56) | ~woman(U_55, V_56)))). % 10.43/3.74 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~dance(U_1, V_2)))). % 10.43/3.74 tff(c_195, plain, (animate(skc6, skc10))). % 10.43/3.74 tff(c_54, plain, (![U_53, V_54]: (animate(U_53, V_54) | ~human_person(U_53, V_54)))). % 10.43/3.74 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 10.43/3.74 tff(c_24, plain, (![U_23, V_24]: (nonhuman(U_23, V_24) | ~abstraction(U_23, V_24)))). % 10.43/3.74 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 10.43/3.74 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 10.43/3.74 tff(c_48, plain, (![U_47, V_48]: (impartial(U_47, V_48) | ~organism(U_47, V_48)))). % 10.43/3.74 tff(c_18, plain, (![U_17, V_18]: (relation(U_17, V_18) | ~proposition(U_17, V_18)))). % 10.43/3.74 tff(c_28, plain, (![U_27, V_28]: (unisex(U_27, V_28) | ~abstraction(U_27, V_28)))). % 10.43/3.74 tff(c_26, plain, (![U_25, V_26]: (general(U_25, V_26) | ~abstraction(U_25, V_26)))). % 10.43/3.74 tff(c_177, plain, (human_person(skc6, skc10))). % 10.43/3.74 tff(c_38, plain, (![U_37, V_38]: (organism(U_37, V_38) | ~human_person(U_37, V_38)))). % 10.43/3.74 tff(c_36, plain, (![U_35, V_36]: (human_person(U_35, V_36) | ~woman(U_35, V_36)))). % 10.43/3.74 tff(c_30, plain, (![U_29, V_30]: (relname(U_29, V_30) | ~forename(U_29, V_30)))). % 10.43/3.74 tff(c_32, plain, (![U_31, V_32]: (relation(U_31, V_32) | ~relname(U_31, V_32)))). % 10.43/3.74 tff(c_34, plain, (![U_33, V_34]: (forename(U_33, V_34) | ~mia_forename(U_33, V_34)))). % 10.43/3.74 tff(c_156, plain, (agent(skc6, skc7, skc10))). % 10.43/3.74 tff(c_158, plain, (agent(skc8, skc11, skc10))). % 10.43/3.74 tff(c_160, plain, (theme(skc6, skc7, skc8))). % 10.43/3.74 tff(c_154, plain, (of(skc6, skc9, skc10))). % 10.43/3.74 tff(c_138, plain, (present(skc8, skc11))). % 10.43/3.74 tff(c_136, plain, (woman(skc6, skc10))). % 10.43/3.74 tff(c_150, plain, (desire_want(skc6, skc7))). % 10.43/3.74 tff(c_134, plain, (event(skc8, skc11))). % 10.43/3.74 tff(c_148, plain, (accessible_world(skc6, skc8))). % 10.43/3.74 tff(c_152, plain, (present(skc6, skc7))). % 10.43/3.74 tff(c_140, plain, (dance(skc8, skc11))). % 10.43/3.74 tff(c_142, plain, (forename(skc6, skc9))). % 10.43/3.74 tff(c_144, plain, (mia_forename(skc6, skc9))). % 10.43/3.74 tff(c_146, plain, (proposition(skc6, skc8))). % 10.43/3.74 tff(c_132, plain, (actual_world(skc6))). % 10.43/3.74 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.43/3.74 %------------------------------------------------------------------------------