%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP024-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n010.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 17.77s 8.20s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP024-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n010.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:09:48 EDT 2025 % 0.13/0.34 % CPUTime : % 17.77/8.19 % 17.77/8.20 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.77/8.20 % 17.77/8.20 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.77/8.21 %$ tuple > ifeq4 > ifeq3 > ifeq2 > ifeq > theme > of > agent > woman > vincent_forename > unisex > tuple2 > 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 > #nlpp > actual_world > true > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 > b > a % 17.77/8.21 % 17.77/8.21 %Foreground sorts: % 17.77/8.21 % 17.77/8.21 % 17.77/8.21 %Background operators: % 17.77/8.21 % 17.77/8.21 % 17.77/8.21 %Foreground operators: % 17.77/8.21 tff(agent, type, agent: ($i * $i * $i) > $i). % 17.77/8.21 tff(proposition, type, proposition: ($i * $i) > $i). % 17.77/8.21 tff(specific, type, specific: ($i * $i) > $i). % 17.77/8.21 tff(organism, type, organism: ($i * $i) > $i). % 17.77/8.21 tff(woman, type, woman: ($i * $i) > $i). % 17.77/8.21 tff(impartial, type, impartial: ($i * $i) > $i). % 17.77/8.21 tff(skc11, type, skc11: $i). % 17.77/8.21 tff(a, type, a: $i). % 17.77/8.21 tff(skc9, type, skc9: $i). % 17.77/8.21 tff(eventuality, type, eventuality: ($i * $i) > $i). % 17.77/8.21 tff(theme, type, theme: ($i * $i * $i) > $i). % 17.77/8.21 tff(human_person, type, human_person: ($i * $i) > $i). % 17.77/8.21 tff(skc8, type, skc8: $i). % 17.77/8.21 tff(relname, type, relname: ($i * $i) > $i). % 17.77/8.21 tff(skc14, type, skc14: $i). % 17.77/8.21 tff(skc13, type, skc13: $i). % 17.77/8.21 tff(thing, type, thing: ($i * $i) > $i). % 17.77/8.21 tff(unisex, type, unisex: ($i * $i) > $i). % 17.77/8.21 tff(abstraction, type, abstraction: ($i * $i) > $i). % 17.77/8.21 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 17.77/8.21 tff(relation, type, relation: ($i * $i) > $i). % 17.77/8.21 tff(tuple2, type, tuple2: ($i * $i) > $i). % 17.77/8.21 tff(actual_world, type, actual_world: $i > $i). % 17.77/8.21 tff(of, type, of: ($i * $i * $i) > $i). % 17.77/8.21 tff(present, type, present: ($i * $i) > $i). % 17.77/8.21 tff(b, type, b: $i). % 17.77/8.21 tff(desire_want, type, desire_want: ($i * $i) > $i). % 17.77/8.21 tff(animate, type, animate: ($i * $i) > $i). % 17.77/8.21 tff(human, type, human: ($i * $i) > $i). % 17.77/8.21 tff(tuple, type, tuple: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i). % 17.77/8.21 tff(dance, type, dance: ($i * $i) > $i). % 17.77/8.21 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 17.77/8.21 tff(skc15, type, skc15: $i). % 17.77/8.21 tff(mia_forename, type, mia_forename: ($i * $i) > $i). % 17.77/8.21 tff(ifeq4, type, ifeq4: ($i * $i * $i * $i) > $i). % 17.77/8.21 tff(existent, type, existent: ($i * $i) > $i). % 17.77/8.21 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 17.77/8.21 tff(forename, type, forename: ($i * $i) > $i). % 17.77/8.21 tff(female, type, female: ($i * $i) > $i). % 17.77/8.21 tff(true, type, true: $i). % 17.77/8.21 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 17.77/8.21 tff(male, type, male: ($i * $i) > $i). % 17.77/8.21 tff(skc12, type, skc12: $i). % 17.77/8.21 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 17.77/8.21 tff(entity, type, entity: ($i * $i) > $i). % 17.77/8.21 tff(skc10, type, skc10: $i). % 17.77/8.21 tff(singleton, type, singleton: ($i * $i) > $i). % 17.77/8.21 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 17.77/8.21 tff(event, type, event: ($i * $i) > $i). % 17.77/8.21 tff(man, type, man: ($i * $i) > $i). % 17.77/8.21 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 17.77/8.21 tff(general, type, general: ($i * $i) > $i). % 17.77/8.21 tff(living, type, living: ($i * $i) > $i). % 17.77/8.21 % 17.77/8.21 %Saturated clause set: % 17.77/8.21 tff(c_3724, plain, (![U_411]: (ifeq(tuple(dance(skc8, skc9), true, desire_want(skc8, U_411), proposition(skc8, skc8), accessible_world(skc8, skc8), true, present(skc8, U_411), agent(skc8, skc9, skc15), agent(skc8, U_411, skc15), theme(skc8, U_411, skc8)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.21 tff(c_14436, plain, (![U_844]: (ifeq(tuple(dance(skc10, skc9), true, desire_want(skc8, U_844), true, true, true, present(skc8, U_844), agent(skc10, skc9, skc15), agent(skc8, U_844, skc15), theme(skc8, U_844, skc10)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.21 tff(c_14790, plain, (ifeq(tuple(dance(skc8, skc9), true, true, proposition(skc8, skc8), accessible_world(skc8, skc8), true, true, agent(skc8, skc9, skc15), agent(skc8, skc9, skc15), theme(skc8, skc9, skc8)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b)). % 17.77/8.21 tff(c_13743, plain, (ifeq(tuple(dance(skc10, skc9), true, true, true, true, true, true, agent(skc10, skc9, skc15), agent(skc8, skc9, skc15), true), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b)). % 17.77/8.21 tff(c_3969, plain, (![Y_187, V_188, W_184]: (ifeq4(theme(skc10, Y_187, skc10), true, ifeq4(theme(skc10, V_188, W_184), true, ifeq4(proposition(skc10, W_184), true, ifeq4(desire_want(skc10, Y_187), true, ifeq4(desire_want(skc10, V_188), true, skc10, W_184), W_184), W_184), W_184), W_184)=W_184))). % 17.77/8.21 tff(c_14999, plain, (![Y_874, V_876]: (ifeq4(theme(skc10, Y_874, skc10), true, ifeq4(theme(skc10, V_876, skc10), true, ifeq4(desire_want(skc10, Y_874), true, ifeq4(desire_want(skc10, V_876), true, skc10, skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.21 tff(c_3970, plain, (![Y_187, X_186, V_188]: (ifeq4(theme(skc10, Y_187, X_186), true, ifeq4(theme(skc10, V_188, skc10), true, ifeq4(proposition(skc10, X_186), true, ifeq4(desire_want(skc10, Y_187), true, ifeq4(desire_want(skc10, V_188), true, X_186, skc10), skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.21 tff(c_14927, plain, (![Y_869, W_871]: (ifeq4(theme(skc10, Y_869, skc10), true, ifeq4(theme(skc10, skc9, W_871), true, ifeq4(proposition(skc10, W_871), true, ifeq4(desire_want(skc10, Y_869), true, skc10, W_871), W_871), W_871), W_871)=W_871))). % 17.77/8.21 tff(c_3635, plain, (![Y_402, X_403, W_404]: (ifeq4(theme(skc10, Y_402, X_403), true, ifeq4(theme(skc10, skc9, W_404), true, ifeq4(proposition(skc10, X_403), true, ifeq4(proposition(skc10, W_404), true, ifeq4(desire_want(skc10, Y_402), true, X_403, W_404), W_404), W_404), W_404), W_404)=W_404))). % 17.77/8.21 tff(c_14832, plain, (![X_862, W_864]: (ifeq4(theme(skc10, skc9, X_862), true, ifeq4(theme(skc10, skc9, W_864), true, ifeq4(proposition(skc10, X_862), true, ifeq4(proposition(skc10, W_864), true, X_862, W_864), W_864), W_864), W_864)=W_864))). % 17.77/8.21 tff(c_14831, plain, (![X_862, V_863]: (ifeq4(theme(skc10, skc9, X_862), true, ifeq4(theme(skc10, V_863, skc10), true, ifeq4(proposition(skc10, X_862), true, ifeq4(desire_want(skc10, V_863), true, X_862, skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.21 tff(c_3634, plain, (![X_403, V_406, W_404]: (ifeq4(theme(skc10, skc9, X_403), true, ifeq4(theme(skc10, V_406, W_404), true, ifeq4(proposition(skc10, X_403), true, ifeq4(proposition(skc10, W_404), true, ifeq4(desire_want(skc10, V_406), true, X_403, W_404), W_404), W_404), W_404), W_404)=W_404))). % 17.77/8.21 tff(c_13744, plain, (ifeq(tuple(true, true, true, true, true, true, true, agent(skc10, skc13, skc15), agent(skc8, skc9, skc15), true), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b)). % 17.77/8.21 tff(c_3725, plain, (![V_409, W_410]: (ifeq(tuple(dance(V_409, W_410), event(V_409, W_410), true, proposition(skc8, V_409), accessible_world(skc8, V_409), present(V_409, W_410), true, agent(V_409, W_410, skc15), agent(skc8, skc9, skc15), theme(skc8, skc9, V_409)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.21 tff(c_5174, plain, (![W_181, V_183]: (ifeq4(of(skc10, W_181, skc15), true, ifeq4(of(skc10, V_183, skc15), true, ifeq4(forename(skc10, W_181), true, ifeq4(forename(skc10, V_183), true, W_181, V_183), V_183), V_183), V_183)=V_183))). % 17.77/8.21 tff(c_5108, plain, (![W_181, V_183]: (ifeq4(of(skc10, W_181, skc12), true, ifeq4(of(skc10, V_183, skc12), true, ifeq4(forename(skc10, W_181), true, ifeq4(forename(skc10, V_183), true, W_181, V_183), V_183), V_183), V_183)=V_183))). % 17.77/8.21 tff(c_3562, plain, (![W_398, V_400]: (ifeq4(of(skc8, W_398, skc15), true, ifeq4(of(skc8, V_400, skc15), true, ifeq4(forename(skc8, W_398), true, ifeq4(forename(skc8, V_400), true, W_398, V_400), V_400), V_400), V_400)=V_400))). % 17.77/8.21 tff(c_3561, plain, (![W_398, V_400]: (ifeq4(of(skc8, W_398, skc12), true, ifeq4(of(skc8, V_400, skc12), true, ifeq4(forename(skc8, W_398), true, ifeq4(forename(skc8, V_400), true, W_398, V_400), V_400), V_400), V_400)=V_400))). % 17.77/8.21 tff(c_14580, plain, (![W_849]: (ifeq4(of(skc10, W_849, skc12), true, ifeq4(of(skc10, skc14, skc12), true, ifeq4(forename(skc10, W_849), true, W_849, skc14), skc14), skc14)=skc14))). % 17.77/8.21 tff(c_4121, plain, (![W_181, X_182]: (ifeq4(of(skc10, W_181, X_182), true, ifeq4(of(skc10, skc14, X_182), true, ifeq4(entity(skc10, X_182), true, ifeq4(forename(skc10, W_181), true, W_181, skc14), skc14), skc14), skc14)=skc14))). % 17.77/8.21 tff(c_14505, plain, (![W_846]: (ifeq4(of(skc10, W_846, skc15), true, ifeq4(of(skc10, skc11, skc15), true, ifeq4(forename(skc10, W_846), true, W_846, skc11), skc11), skc11)=skc11))). % 17.77/8.21 tff(c_3882, plain, (![W_181, X_182]: (ifeq4(of(skc10, W_181, X_182), true, ifeq4(of(skc10, skc11, X_182), true, ifeq4(entity(skc10, X_182), true, ifeq4(forename(skc10, W_181), true, W_181, skc11), skc11), skc11), skc11)=skc11))). % 17.77/8.21 tff(c_14243, plain, (![V_835]: (ifeq4(of(skc10, skc14, skc12), true, ifeq4(of(skc10, V_835, skc12), true, ifeq4(forename(skc10, V_835), true, skc14, V_835), V_835), V_835)=V_835))). % 17.77/8.21 tff(c_3721, plain, (![W_410, U_411]: (ifeq(tuple(dance(skc10, W_410), event(skc10, W_410), desire_want(skc8, U_411), true, true, present(skc10, W_410), present(skc8, U_411), agent(skc10, W_410, skc15), agent(skc8, U_411, skc15), theme(skc8, U_411, skc10)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.21 tff(c_14306, plain, (![V_838]: (ifeq4(of(skc10, skc11, skc15), true, ifeq4(of(skc10, V_838, skc15), true, ifeq4(forename(skc10, V_838), true, skc11, V_838), V_838), V_838)=V_838))). % 17.77/8.21 tff(c_14377, plain, (ifeq4(of(skc10, skc11, skc15), true, ifeq4(of(skc10, skc11, skc15), true, skc11, skc11), skc11)=skc11)). % 17.77/8.21 tff(c_14309, plain, (![X_837]: (ifeq4(of(skc10, skc11, X_837), true, ifeq4(of(skc10, skc11, X_837), true, ifeq4(entity(skc10, X_837), true, skc11, skc11), skc11), skc11)=skc11))). % 17.77/8.21 tff(c_14308, plain, (![X_837]: (ifeq4(of(skc10, skc11, X_837), true, ifeq4(of(skc10, skc14, X_837), true, ifeq4(entity(skc10, X_837), true, skc11, skc14), skc14), skc14)=skc14))). % 17.77/8.21 tff(c_14245, plain, (![X_834]: (ifeq4(of(skc10, skc14, X_834), true, ifeq4(of(skc10, skc11, X_834), true, ifeq4(entity(skc10, X_834), true, skc14, skc11), skc11), skc11)=skc11))). % 17.77/8.22 tff(c_3881, plain, (![X_182, V_183]: (ifeq4(of(skc10, skc11, X_182), true, ifeq4(of(skc10, V_183, X_182), true, ifeq4(entity(skc10, X_182), true, ifeq4(forename(skc10, V_183), true, skc11, V_183), V_183), V_183), V_183)=V_183))). % 17.77/8.22 tff(c_14268, plain, (ifeq4(of(skc10, skc14, skc12), true, ifeq4(of(skc10, skc14, skc12), true, skc14, skc14), skc14)=skc14)). % 17.77/8.22 tff(c_14244, plain, (![X_834]: (ifeq4(of(skc10, skc14, X_834), true, ifeq4(of(skc10, skc14, X_834), true, ifeq4(entity(skc10, X_834), true, skc14, skc14), skc14), skc14)=skc14))). % 17.77/8.22 tff(c_4120, plain, (![X_182, V_183]: (ifeq4(of(skc10, skc14, X_182), true, ifeq4(of(skc10, V_183, X_182), true, ifeq4(entity(skc10, X_182), true, ifeq4(forename(skc10, V_183), true, skc14, V_183), V_183), V_183), V_183)=V_183))). % 17.77/8.22 tff(c_13317, plain, (![X_788, V_789]: (ifeq4(theme(skc8, skc9, X_788), true, ifeq4(theme(skc8, V_789, skc10), true, ifeq4(proposition(skc8, X_788), true, ifeq4(desire_want(skc8, V_789), true, X_788, skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.22 tff(c_13126, plain, (![Y_777, W_779]: (ifeq4(theme(skc8, Y_777, skc10), true, ifeq4(theme(skc8, skc9, W_779), true, ifeq4(proposition(skc8, W_779), true, ifeq4(desire_want(skc8, Y_777), true, skc10, W_779), W_779), W_779), W_779)=W_779))). % 17.77/8.22 tff(c_13124, plain, (![Y_777, V_778]: (ifeq4(theme(skc8, Y_777, skc10), true, ifeq4(theme(skc8, V_778, skc10), true, ifeq4(desire_want(skc8, Y_777), true, ifeq4(desire_want(skc8, V_778), true, skc10, skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.22 tff(c_13602, plain, (![X_802, W_804]: (ifeq4(theme(skc8, skc9, X_802), true, ifeq4(theme(skc8, skc9, W_804), true, ifeq4(proposition(skc8, X_802), true, ifeq4(proposition(skc8, W_804), true, X_802, W_804), W_804), W_804), W_804)=W_804))). % 17.77/8.22 tff(c_12374, plain, (![V_739]: (ifeq4(of(skc8, skc14, skc12), true, ifeq4(of(skc8, V_739, skc12), true, ifeq4(forename(skc8, V_739), true, skc14, V_739), V_739), V_739)=V_739))). % 17.77/8.22 tff(c_12954, plain, (![W_768]: (ifeq4(of(skc8, W_768, skc15), true, ifeq4(of(skc8, skc11, skc15), true, ifeq4(forename(skc8, W_768), true, W_768, skc11), skc11), skc11)=skc11))). % 17.77/8.22 tff(c_12560, plain, (![V_749]: (ifeq4(of(skc8, skc11, skc15), true, ifeq4(of(skc8, V_749, skc15), true, ifeq4(forename(skc8, V_749), true, skc11, V_749), V_749), V_749)=V_749))). % 17.77/8.22 tff(c_12752, plain, (![W_758]: (ifeq4(of(skc8, W_758, skc12), true, ifeq4(of(skc8, skc14, skc12), true, ifeq4(forename(skc8, W_758), true, W_758, skc14), skc14), skc14)=skc14))). % 17.77/8.22 tff(c_12565, plain, (![X_748]: (ifeq4(of(skc8, skc11, X_748), true, ifeq4(of(skc8, skc14, X_748), true, ifeq4(entity(skc8, X_748), true, skc11, skc14), skc14), skc14)=skc14))). % 17.77/8.22 tff(c_12959, plain, (![X_769]: (ifeq4(of(skc8, skc14, X_769), true, ifeq4(of(skc8, skc11, X_769), true, ifeq4(entity(skc8, X_769), true, skc14, skc11), skc11), skc11)=skc11))). % 17.77/8.22 tff(c_3719, plain, (![U_411]: (ifeq(tuple(true, true, desire_want(skc8, U_411), true, true, true, present(skc8, U_411), agent(skc10, skc13, skc15), agent(skc8, U_411, skc15), theme(skc8, U_411, skc10)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.22 tff(c_13900, plain, (ifeq4(of(skc8, skc14, skc12), true, ifeq4(of(skc8, skc14, skc12), true, skc14, skc14), skc14)=skc14)). % 17.77/8.22 tff(c_12758, plain, (![X_759]: (ifeq4(of(skc8, skc14, X_759), true, ifeq4(of(skc8, skc14, X_759), true, ifeq4(entity(skc8, X_759), true, skc14, skc14), skc14), skc14)=skc14))). % 17.77/8.22 tff(c_13874, plain, (ifeq4(of(skc8, skc11, skc15), true, ifeq4(of(skc8, skc11, skc15), true, skc11, skc11), skc11)=skc11)). % 17.77/8.22 tff(c_12958, plain, (![X_769]: (ifeq4(of(skc8, skc11, X_769), true, ifeq4(of(skc8, skc11, X_769), true, ifeq4(entity(skc8, X_769), true, skc11, skc11), skc11), skc11)=skc11))). % 17.77/8.22 tff(c_13828, plain, (![X_815]: (ifeq4(theme(skc10, skc9, X_815), true, ifeq4(proposition(skc10, X_815), true, X_815, skc10), skc10)=skc10))). % 17.77/8.22 tff(c_6029, plain, (![Y_187, X_186]: (ifeq4(theme(skc10, Y_187, X_186), true, ifeq4(proposition(skc10, X_186), true, ifeq4(desire_want(skc10, Y_187), true, X_186, skc10), skc10), skc10)=skc10))). % 17.77/8.22 tff(c_13767, plain, (![W_811]: (ifeq4(theme(skc10, skc9, W_811), true, ifeq4(proposition(skc10, W_811), true, skc10, W_811), W_811)=W_811))). % 17.77/8.22 tff(c_13766, plain, (![V_810]: (ifeq4(theme(skc10, V_810, skc10), true, ifeq4(desire_want(skc10, V_810), true, skc10, skc10), skc10)=skc10))). % 17.77/8.22 tff(c_6028, plain, (![V_188, W_184]: (ifeq4(theme(skc10, V_188, W_184), true, ifeq4(proposition(skc10, W_184), true, ifeq4(desire_want(skc10, V_188), true, skc10, W_184), W_184), W_184)=W_184))). % 17.77/8.22 tff(c_3717, plain, (![W_410]: (ifeq(tuple(dance(skc10, W_410), event(skc10, W_410), true, true, true, present(skc10, W_410), true, agent(skc10, W_410, skc15), agent(skc8, skc9, skc15), true), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 17.77/8.22 tff(c_13714, plain, (ifeq4(of(skc10, skc14, skc12), true, skc14, skc11)=skc11)). % 17.77/8.22 tff(c_6159, plain, (![W_181]: (ifeq4(of(skc10, W_181, skc12), true, ifeq4(forename(skc10, W_181), true, W_181, skc11), skc11)=skc11))). % 17.77/8.22 tff(c_13681, plain, (ifeq4(of(skc10, skc14, skc12), true, skc11, skc14)=skc14)). % 17.77/8.22 tff(c_6158, plain, (![V_183]: (ifeq4(of(skc10, V_183, skc12), true, ifeq4(forename(skc10, V_183), true, skc11, V_183), V_183)=V_183))). % 17.77/8.22 tff(c_13657, plain, (ifeq4(of(skc10, skc11, skc15), true, skc14, skc11)=skc11)). % 17.77/8.22 tff(c_6123, plain, (![V_183]: (ifeq4(of(skc10, V_183, skc15), true, ifeq4(forename(skc10, V_183), true, skc14, V_183), V_183)=V_183))). % 17.77/8.22 tff(c_13622, plain, (ifeq4(of(skc10, skc11, skc15), true, skc11, skc14)=skc14)). % 17.77/8.22 tff(c_6124, plain, (![W_181]: (ifeq4(of(skc10, W_181, skc15), true, ifeq4(forename(skc10, W_181), true, W_181, skc14), skc14)=skc14))). % 17.77/8.22 tff(c_3640, plain, (![X_403, V_406, W_404]: (ifeq4(theme(skc8, skc9, X_403), true, ifeq4(theme(skc8, V_406, W_404), true, ifeq4(proposition(skc8, X_403), true, ifeq4(proposition(skc8, W_404), true, ifeq4(desire_want(skc8, V_406), true, X_403, W_404), W_404), W_404), W_404), W_404)=W_404))). % 17.77/8.22 tff(c_3565, plain, (![V_400]: (ifeq4(of(skc8, V_400, skc12), true, ifeq4(forename(skc8, V_400), true, skc11, V_400), V_400)=V_400))). % 17.77/8.22 tff(c_12755, plain, (![W_758]: (ifeq4(of(skc8, W_758, skc15), true, ifeq4(forename(skc8, W_758), true, W_758, skc14), skc14)=skc14))). % 17.77/8.22 tff(c_3641, plain, (![Y_402, X_403, W_404]: (ifeq4(theme(skc8, Y_402, X_403), true, ifeq4(theme(skc8, skc9, W_404), true, ifeq4(proposition(skc8, X_403), true, ifeq4(proposition(skc8, W_404), true, ifeq4(desire_want(skc8, Y_402), true, X_403, W_404), W_404), W_404), W_404), W_404)=W_404))). % 17.77/8.22 tff(c_12957, plain, (![W_768]: (ifeq4(of(skc8, W_768, skc12), true, ifeq4(forename(skc8, W_768), true, W_768, skc11), skc11)=skc11))). % 17.77/8.22 tff(c_12376, plain, (![V_739]: (ifeq4(of(skc8, V_739, skc15), true, ifeq4(forename(skc8, V_739), true, skc14, V_739), V_739)=V_739))). % 17.77/8.22 tff(c_6154, plain, (![U_176]: (ifeq3(of(U_176, skc11, skc12), true, ifeq3(accessible_world(U_176, skc10), true, true, true), true)=true))). % 17.77/8.22 tff(c_13367, plain, (![V_792]: (ifeq3(accessible_world(skc10, V_792), true, of(V_792, skc11, skc12), true)=true))). % 17.77/8.22 tff(c_13324, plain, (![V_790]: (ifeq3(accessible_world(skc10, V_790), true, theme(V_790, skc9, skc10), true)=true))). % 17.77/8.22 tff(c_3639, plain, (![Y_402, X_403, V_406]: (ifeq4(theme(skc8, Y_402, X_403), true, ifeq4(theme(skc8, V_406, skc10), true, ifeq4(proposition(skc8, X_403), true, ifeq4(desire_want(skc8, Y_402), true, ifeq4(desire_want(skc8, V_406), true, X_403, skc10), skc10), skc10), skc10), skc10)=skc10))). % 17.77/8.22 tff(c_13244, plain, (![V_785]: (ifeq3(accessible_world(skc10, V_785), true, agent(V_785, skc9, skc12), true)=true))). % 17.77/8.22 tff(c_6119, plain, (![U_176]: (ifeq3(of(U_176, skc14, skc15), true, ifeq3(accessible_world(U_176, skc10), true, true, true), true)=true))). % 17.77/8.22 tff(c_6057, plain, (![U_168]: (ifeq3(agent(U_168, skc9, skc12), true, ifeq3(accessible_world(U_168, skc10), true, true, true), true)=true))). % 17.77/8.22 tff(c_6024, plain, (![U_172]: (ifeq3(theme(U_172, skc9, skc10), true, ifeq3(accessible_world(U_172, skc10), true, true, true), true)=true))). % 17.77/8.22 tff(c_13132, plain, (![V_780]: (ifeq3(accessible_world(skc10, V_780), true, of(V_780, skc14, skc15), true)=true))). % 17.77/8.22 tff(c_3638, plain, (![Y_402, V_406, W_404]: (ifeq4(theme(skc8, Y_402, skc10), true, ifeq4(theme(skc8, V_406, W_404), true, ifeq4(proposition(skc8, W_404), true, ifeq4(desire_want(skc8, Y_402), true, ifeq4(desire_want(skc8, V_406), true, skc10, W_404), W_404), W_404), W_404), W_404)=W_404))). % 17.77/8.22 tff(c_12171, plain, (![Y_727]: (ifeq4(theme(skc8, Y_727, skc10), true, ifeq4(desire_want(skc8, Y_727), true, skc10, skc10), skc10)=skc10))). % 17.77/8.22 tff(c_11988, plain, (![W_717]: (ifeq4(theme(skc8, skc9, W_717), true, ifeq4(proposition(skc8, W_717), true, skc10, W_717), W_717)=W_717))). % 17.77/8.22 tff(c_12172, plain, (![X_728]: (ifeq4(theme(skc8, skc9, X_728), true, ifeq4(proposition(skc8, X_728), true, X_728, skc10), skc10)=skc10))). % 17.77/8.22 tff(c_5966, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc14), true, true, true), true)=true))). % 17.77/8.22 tff(c_5934, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc11), true, true, true), true)=true))). % 17.77/8.22 tff(c_5810, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc12), true, true, true), true)=true))). % 17.77/8.22 tff(c_5657, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc14), true, true, true), true)=true))). % 17.77/8.22 tff(c_12955, plain, (ifeq4(of(skc8, skc11, skc15), true, skc14, skc11)=skc11)). % 17.77/8.22 tff(c_3568, plain, (![W_398, X_399]: (ifeq4(of(skc8, W_398, X_399), true, ifeq4(of(skc8, skc11, X_399), true, ifeq4(entity(skc8, X_399), true, ifeq4(forename(skc8, W_398), true, W_398, skc11), skc11), skc11), skc11)=skc11))). % 17.77/8.22 tff(c_5713, plain, (![U_96]: (ifeq3(accessible_world(U_96, skc10), true, ifeq3(unisex(U_96, skc14), true, true, true), true)=true))). % 17.77/8.22 tff(c_5866, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_5754, plain, (![U_114]: (ifeq3(accessible_world(U_114, skc10), true, ifeq3(nonhuman(U_114, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_5838, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_5626, plain, (![U_114]: (ifeq3(accessible_world(U_114, skc10), true, ifeq3(nonhuman(U_114, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_5589, plain, (![U_96]: (ifeq3(accessible_world(U_96, skc10), true, ifeq3(unisex(U_96, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_5229, plain, (![U_141]: (ifeq3(accessible_world(U_141, skc10), true, ifeq3(existent(U_141, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_5379, plain, (![U_111]: (ifeq3(accessible_world(U_111, skc10), true, ifeq3(abstraction(U_111, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_12756, plain, (ifeq4(of(skc8, skc14, skc12), true, skc11, skc14)=skc14)). % 17.77/8.23 tff(c_3570, plain, (![W_398, X_399]: (ifeq4(of(skc8, W_398, X_399), true, ifeq4(of(skc8, skc14, X_399), true, ifeq4(entity(skc8, X_399), true, ifeq4(forename(skc8, W_398), true, W_398, skc14), skc14), skc14), skc14)=skc14))). % 17.77/8.23 tff(c_3579, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_5289, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc10), true, ifeq3(singleton(U_87, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_5420, plain, (![U_111]: (ifeq3(accessible_world(U_111, skc10), true, ifeq3(abstraction(U_111, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_5532, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_5494, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_5198, plain, (![U_141]: (ifeq3(accessible_world(U_141, skc10), true, ifeq3(existent(U_141, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_2992, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc8), true, ifeq3(singleton(U_87, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_2806, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc8), true, ifeq3(singleton(U_87, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_12561, plain, (ifeq4(of(skc8, skc11, skc15), true, skc11, skc14)=skc14)). % 17.77/8.23 tff(c_3567, plain, (![X_399, V_400]: (ifeq4(of(skc8, skc11, X_399), true, ifeq4(of(skc8, V_400, X_399), true, ifeq4(entity(skc8, X_399), true, ifeq4(forename(skc8, V_400), true, skc11, V_400), V_400), V_400), V_400)=V_400))). % 17.77/8.23 tff(c_2912, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc8), true, ifeq3(singleton(U_87, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_2858, plain, (![U_87]: (ifeq3(accessible_world(U_87, skc8), true, ifeq3(singleton(U_87, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_3380, plain, (![U_93]: (ifeq3(accessible_world(U_93, skc10), true, ifeq3(nonexistent(U_93, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_3468, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_4898, plain, (![U_147]: (ifeq3(accessible_world(U_147, skc10), true, ifeq3(living(U_147, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_5062, plain, (![U_147]: (ifeq3(accessible_world(U_147, skc10), true, ifeq3(living(U_147, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_5039, plain, (![U_90]: (ifeq3(accessible_world(U_90, skc10), true, ifeq3(specific(U_90, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_4756, plain, (![U_96]: (ifeq3(accessible_world(U_96, skc10), true, ifeq3(unisex(U_96, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_12378, plain, (ifeq4(of(skc8, skc14, skc12), true, skc14, skc11)=skc11)). % 17.77/8.23 tff(c_3569, plain, (![X_399, V_400]: (ifeq4(of(skc8, skc14, X_399), true, ifeq4(of(skc8, V_400, X_399), true, ifeq4(entity(skc8, X_399), true, ifeq4(forename(skc8, V_400), true, skc14, V_400), V_400), V_400), V_400)=V_400))). % 17.77/8.23 tff(c_4610, plain, (![U_108]: (ifeq3(accessible_world(U_108, skc10), true, ifeq3(relation(U_108, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_4926, plain, (![U_144]: (ifeq3(accessible_world(U_144, skc10), true, ifeq3(impartial(U_144, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_4793, plain, (![U_108]: (ifeq3(accessible_world(U_108, skc10), true, ifeq3(relation(U_108, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_4675, plain, (![U_117]: (ifeq3(accessible_world(U_117, skc10), true, ifeq3(general(U_117, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_5005, plain, (![U_90]: (ifeq3(accessible_world(U_90, skc10), true, ifeq3(specific(U_90, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_5159, plain, (![U_138]: (ifeq3(accessible_world(U_138, skc10), true, ifeq3(entity(U_138, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_5093, plain, (![U_138]: (ifeq3(accessible_world(U_138, skc10), true, ifeq3(entity(U_138, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_4847, plain, (![U_117]: (ifeq3(accessible_world(U_117, skc10), true, ifeq3(general(U_117, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_4868, plain, (![U_117]: (ifeq3(accessible_world(U_117, skc10), true, ifeq3(general(U_117, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_3637, plain, (![Y_402, X_403]: (ifeq4(theme(skc8, Y_402, X_403), true, ifeq4(proposition(skc8, X_403), true, ifeq4(desire_want(skc8, Y_402), true, X_403, skc10), skc10), skc10)=skc10))). % 17.77/8.23 tff(c_4644, plain, (![U_114]: (ifeq3(accessible_world(U_114, skc10), true, ifeq3(nonhuman(U_114, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_4719, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc10), true, ifeq3(thing(U_84, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_4986, plain, (![U_144]: (ifeq3(accessible_world(U_144, skc10), true, ifeq3(impartial(U_144, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_3320, plain, (![U_96]: (ifeq3(accessible_world(U_96, skc10), true, ifeq3(unisex(U_96, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_3434, plain, (![U_90]: (ifeq3(accessible_world(U_90, skc10), true, ifeq3(specific(U_90, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_2587, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc8), true, ifeq3(thing(U_84, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_2201, plain, (![U_323]: (ifeq3(accessible_world(U_323, skc8), true, ifeq3(specific(U_323, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_2435, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc8), true, ifeq3(thing(U_84, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_2826, plain, (![U_353]: (ifeq3(accessible_world(U_353, skc8), true, ifeq3(existent(U_353, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_3636, plain, (![V_406, W_404]: (ifeq4(theme(skc8, V_406, W_404), true, ifeq4(proposition(skc8, W_404), true, ifeq4(desire_want(skc8, V_406), true, skc10, W_404), W_404), W_404)=W_404))). % 17.77/8.23 tff(c_2241, plain, (![U_117]: (ifeq3(accessible_world(U_117, skc8), true, ifeq3(general(U_117, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_2685, plain, (![U_90]: (ifeq3(accessible_world(U_90, skc8), true, ifeq3(specific(U_90, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_2717, plain, (![U_347]: (ifeq3(accessible_world(U_347, skc8), true, ifeq3(singleton(U_347, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_2711, plain, (![U_347]: (ifeq3(accessible_world(U_347, skc8), true, ifeq3(singleton(U_347, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_2648, plain, (![U_96]: (ifeq3(accessible_world(U_96, skc8), true, ifeq3(unisex(U_96, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_2178, plain, (![U_114]: (ifeq3(accessible_world(U_114, skc8), true, ifeq3(nonhuman(U_114, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_1991, plain, (![U_117]: (ifeq3(accessible_world(U_117, skc8), true, ifeq3(general(U_117, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_11817, plain, (![V_707]: (ifeq3(accessible_world(skc8, V_707), true, of(V_707, skc14, skc15), true)=true))). % 17.77/8.23 tff(c_2832, plain, (![U_353]: (ifeq3(accessible_world(U_353, skc8), true, ifeq3(existent(U_353, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_2330, plain, (![U_329]: (ifeq3(accessible_world(U_329, skc8), true, ifeq3(unisex(U_329, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_2303, plain, (![U_114]: (ifeq3(accessible_world(U_114, skc8), true, ifeq3(nonhuman(U_114, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_2141, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc8), true, ifeq3(thing(U_84, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_2525, plain, (![U_84]: (ifeq3(accessible_world(U_84, skc8), true, ifeq3(thing(U_84, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_4476, plain, (![U_135]: (ifeq3(accessible_world(U_135, skc10), true, ifeq3(organism(U_135, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_4523, plain, (![U_123]: (ifeq3(accessible_world(U_123, skc10), true, ifeq3(relname(U_123, skc14), true, true, true), true)=true))). % 17.77/8.23 tff(c_4144, plain, (![U_111]: (ifeq3(accessible_world(U_111, skc10), true, ifeq3(abstraction(U_111, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_4360, plain, (![U_153]: (ifeq3(accessible_world(U_153, skc10), true, ifeq3(animate(U_153, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_3359, plain, (![U_385]: (ifeq3(of(U_385, skc14, skc15), true, ifeq3(accessible_world(U_385, skc8), true, true, true), true)=true))). % 17.77/8.23 tff(c_4562, plain, (![U_150]: (ifeq3(accessible_world(U_150, skc10), true, ifeq3(human(U_150, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_3252, plain, (![U_81]: (ifeq3(accessible_world(U_81, skc10), true, ifeq3(eventuality(U_81, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_4435, plain, (![U_135]: (ifeq3(accessible_world(U_135, skc10), true, ifeq3(organism(U_135, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_4325, plain, (![U_150]: (ifeq3(accessible_world(U_150, skc10), true, ifeq3(human(U_150, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_4407, plain, (![U_153]: (ifeq3(accessible_world(U_153, skc10), true, ifeq3(animate(U_153, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_4026, plain, (![U_123]: (ifeq3(accessible_world(U_123, skc10), true, ifeq3(relname(U_123, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_2275, plain, (![U_326]: (ifeq3(accessible_world(U_326, skc8), true, ifeq3(abstraction(U_326, skc11), true, true, true), true)=true))). % 17.77/8.23 tff(c_2632, plain, (![U_344]: (ifeq3(accessible_world(U_344, skc8), true, ifeq3(entity(U_344, skc15), true, true, true), true)=true))). % 17.77/8.23 tff(c_3103, plain, (![U_372]: (ifeq3(accessible_world(U_372, skc8), true, ifeq3(living(U_372, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_3419, plain, (![U_389]: (ifeq3(agent(U_389, skc9, skc12), true, ifeq3(accessible_world(U_389, skc8), true, true, true), true)=true))). % 17.77/8.23 tff(c_2207, plain, (![U_323]: (ifeq3(accessible_world(U_323, skc8), true, ifeq3(specific(U_323, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_3284, plain, (![U_382]: (ifeq3(accessible_world(U_382, skc8), true, ifeq3(impartial(U_382, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_1899, plain, (![U_308]: (ifeq3(accessible_world(U_308, skc8), true, ifeq3(thing(U_308, skc9), true, true, true), true)=true))). % 17.77/8.23 tff(c_2626, plain, (![U_344]: (ifeq3(accessible_world(U_344, skc8), true, ifeq3(entity(U_344, skc12), true, true, true), true)=true))). % 17.77/8.23 tff(c_1911, plain, (![U_308]: (ifeq3(accessible_world(U_308, skc8), true, ifeq3(thing(U_308, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_1678, plain, (![U_296]: (ifeq3(accessible_world(U_296, skc8), true, ifeq3(nonhuman(U_296, skc10), true, true, true), true)=true))). % 17.77/8.23 tff(c_2723, plain, (![U_347]: (ifeq3(accessible_world(U_347, skc10), true, ifeq3(singleton(U_347, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_11301, plain, (![V_678]: (ifeq3(accessible_world(skc8, V_678), true, agent(V_678, skc9, skc12), true)=true))). % 17.77/8.24 tff(c_1962, plain, (![U_311]: (ifeq3(accessible_world(U_311, skc8), true, ifeq3(general(U_311, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_1829, plain, (![U_93]: (ifeq3(accessible_world(U_93, skc8), true, ifeq3(nonexistent(U_93, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_2342, plain, (![U_329]: (ifeq3(accessible_world(U_329, skc8), true, ifeq3(unisex(U_329, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_3097, plain, (![U_372]: (ifeq3(accessible_world(U_372, skc8), true, ifeq3(living(U_372, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_2263, plain, (![U_326]: (ifeq3(accessible_world(U_326, skc8), true, ifeq3(abstraction(U_326, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_3290, plain, (![U_382]: (ifeq3(accessible_world(U_382, skc8), true, ifeq3(impartial(U_382, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_2336, plain, (![U_329]: (ifeq3(accessible_world(U_329, skc8), true, ifeq3(unisex(U_329, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_11145, plain, (![V_669]: (ifeq3(accessible_world(skc8, V_669), true, theme(V_669, skc9, skc10), true)=true))). % 17.77/8.24 tff(c_4232, plain, (![U_156]: (ifeq3(accessible_world(U_156, skc10), true, ifeq3(female(U_156, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_3778, plain, (![U_132]: (ifeq3(accessible_world(U_132, skc10), true, ifeq3(human_person(U_132, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_3992, plain, (![U_108]: (ifeq3(accessible_world(U_108, skc10), true, ifeq3(relation(U_108, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_4266, plain, (![U_132]: (ifeq3(accessible_world(U_132, skc10), true, ifeq3(human_person(U_132, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_3905, plain, (![U_165]: (ifeq3(accessible_world(U_165, skc10), true, ifeq3(male(U_165, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_3201, plain, (![U_78]: (ifeq3(accessible_world(U_78, skc10), true, ifeq3(event(U_78, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_4108, plain, (![U_120]: (ifeq3(accessible_world(U_120, skc10), true, ifeq3(forename(U_120, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_10977, plain, (![V_660]: (ifeq3(accessible_world(skc10, V_660), true, agent(V_660, skc13, skc12), true)=true))). % 17.77/8.24 tff(c_3869, plain, (![U_120]: (ifeq3(accessible_world(U_120, skc10), true, ifeq3(forename(U_120, skc11), true, true, true), true)=true))). % 17.77/8.24 tff(c_1905, plain, (![U_308]: (ifeq3(accessible_world(U_308, skc10), true, ifeq3(thing(U_308, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_1857, plain, (![U_305]: (ifeq3(accessible_world(U_305, skc8), true, ifeq3(animate(U_305, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_2124, plain, (![U_320]: (ifeq3(accessible_world(U_320, skc8), true, ifeq3(relation(U_320, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_2493, plain, (![U_338]: (ifeq3(accessible_world(U_338, skc8), true, ifeq3(human(U_338, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_3164, plain, (![U_376]: (ifeq3(accessible_world(U_376, skc8), true, ifeq3(eventuality(U_376, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_1780, plain, (![U_302]: (ifeq3(accessible_world(U_302, skc10), true, ifeq3(nonexistent(U_302, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_1630, plain, (![U_293]: (ifeq3(accessible_world(U_293, skc8), true, ifeq3(organism(U_293, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_2348, plain, (![U_329]: (ifeq3(accessible_world(U_329, skc10), true, ifeq3(unisex(U_329, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_3497, plain, (![U_393]: (ifeq3(theme(U_393, skc9, skc10), true, ifeq3(accessible_world(U_393, skc8), true, true, true), true)=true))). % 17.77/8.24 tff(c_2213, plain, (![U_323]: (ifeq3(accessible_world(U_323, skc10), true, ifeq3(specific(U_323, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_2499, plain, (![U_338]: (ifeq3(accessible_world(U_338, skc8), true, ifeq3(human(U_338, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_1851, plain, (![U_305]: (ifeq3(accessible_world(U_305, skc8), true, ifeq3(animate(U_305, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_1624, plain, (![U_293]: (ifeq3(accessible_world(U_293, skc8), true, ifeq3(organism(U_293, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_2269, plain, (![U_326]: (ifeq3(accessible_world(U_326, skc8), true, ifeq3(abstraction(U_326, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_2118, plain, (![U_320]: (ifeq3(accessible_world(U_320, skc8), true, ifeq3(relation(U_320, skc11), true, true, true), true)=true))). % 17.77/8.24 tff(c_3835, plain, (![U_126]: (ifeq3(accessible_world(U_126, skc10), true, ifeq3(mia_forename(U_126, skc11), true, true, true), true)=true))). % 17.77/8.24 tff(c_3081, plain, (![U_99]: (ifeq3(present(U_99, skc9), true, ifeq3(accessible_world(U_99, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_4201, plain, (![U_129]: (ifeq3(accessible_world(U_129, skc10), true, ifeq3(woman(U_129, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_3365, plain, (![U_385]: (ifeq3(of(U_385, skc11, skc12), true, ifeq3(accessible_world(U_385, skc8), true, true, true), true)=true))). % 17.77/8.24 tff(c_3747, plain, (![U_162]: (ifeq3(accessible_world(U_162, skc10), true, ifeq3(man(U_162, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_3145, plain, (![U_102]: (ifeq3(accessible_world(U_102, skc10), true, ifeq3(desire_want(U_102, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_4074, plain, (![U_159]: (ifeq3(accessible_world(U_159, skc10), true, ifeq3(vincent_forename(U_159, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_10525, plain, (![V_635]: (ifeq3(accessible_world(skc10, V_635), true, present(V_635, skc9), true)=true))). % 17.77/8.24 tff(c_3962, plain, (![U_105]: (ifeq3(accessible_world(U_105, skc10), true, ifeq3(proposition(U_105, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_10455, plain, (![V_632]: (ifeq3(accessible_world(skc8, V_632), true, of(V_632, skc11, skc12), true)=true))). % 17.77/8.24 tff(c_2112, plain, (![U_320]: (ifeq3(accessible_world(U_320, skc8), true, ifeq3(relation(U_320, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_2565, plain, (![U_341]: (ifeq3(accessible_world(U_341, skc8), true, ifeq3(event(U_341, skc9), true, true, true), true)=true))). % 17.77/8.24 tff(c_1733, plain, (![U_299]: (ifeq3(accessible_world(U_299, skc8), true, ifeq3(male(U_299, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_3170, plain, (![U_376]: (ifeq3(accessible_world(U_376, skc10), true, ifeq3(eventuality(U_376, skc13), true, true, true), true)=true))). % 17.77/8.24 tff(c_2772, plain, (![U_350]: (ifeq3(accessible_world(U_350, skc8), true, ifeq3(human_person(U_350, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_2766, plain, (![U_350]: (ifeq3(accessible_world(U_350, skc8), true, ifeq3(human_person(U_350, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_2463, plain, (![U_335]: (ifeq3(accessible_world(U_335, skc8), true, ifeq3(relname(U_335, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_2469, plain, (![U_335]: (ifeq3(accessible_world(U_335, skc8), true, ifeq3(relname(U_335, skc11), true, true, true), true)=true))). % 17.77/8.24 tff(c_2878, plain, (![U_356]: (ifeq3(accessible_world(U_356, skc8), true, ifeq3(female(U_356, skc12), true, true, true), true)=true))). % 17.77/8.24 tff(c_3413, plain, (![U_389]: (ifeq3(agent(U_389, skc13, skc12), true, ifeq3(accessible_world(U_389, skc10), true, true, true), true)=true))). % 17.77/8.24 tff(c_10254, plain, (![W_620]: (ifeq3(male(skc8, W_620), true, male(skc10, W_620), true)=true))). % 17.77/8.24 tff(c_10211, plain, (![W_618]: (ifeq3(female(skc8, W_618), true, female(skc10, W_618), true)=true))). % 17.77/8.24 tff(c_10159, plain, (![W_616]: (ifeq3(event(skc8, W_616), true, event(skc10, W_616), true)=true))). % 17.77/8.24 tff(c_10117, plain, (![W_614]: (ifeq3(proposition(skc8, W_614), true, proposition(skc10, W_614), true)=true))). % 17.77/8.24 tff(c_5592, plain, (ifeq2(tuple2(true, male(skc10, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5716, plain, (ifeq2(tuple2(true, male(skc10, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5595, plain, (ifeq2(tuple2(true, female(skc10, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5719, plain, (ifeq2(tuple2(true, female(skc10, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5757, plain, (ifeq2(tuple2(true, human(skc10, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_10046, plain, (![V_612]: (ifeq3(accessible_world(skc8, V_612), true, present(V_612, skc9), true)=true))). % 17.77/8.24 tff(c_5629, plain, (ifeq2(tuple2(true, human(skc10, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5232, plain, (ifeq2(tuple2(nonexistent(skc10, skc12), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5201, plain, (ifeq2(tuple2(nonexistent(skc10, skc15), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4871, plain, (ifeq2(tuple2(specific(skc10, skc11), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4678, plain, (ifeq2(tuple2(specific(skc10, skc10), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4647, plain, (ifeq2(tuple2(true, human(skc10, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4762, plain, (ifeq2(tuple2(true, female(skc10, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3437, plain, (ifeq2(tuple2(true, general(skc10, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5008, plain, (ifeq2(tuple2(true, general(skc10, skc12)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3227, plain, (![U_379]: (ifeq3(accessible_world(U_379, skc8), true, ifeq3(mia_forename(U_379, skc11), true, true, true), true)=true))). % 17.77/8.24 tff(c_4850, plain, (ifeq2(tuple2(specific(skc10, skc14), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5042, plain, (ifeq2(tuple2(true, general(skc10, skc15)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3323, plain, (ifeq2(tuple2(true, male(skc10, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4759, plain, (ifeq2(tuple2(true, male(skc10, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3383, plain, (ifeq2(tuple2(true, existent(skc10, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3326, plain, (ifeq2(tuple2(true, female(skc10, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2654, plain, (ifeq2(tuple2(true, female(skc8, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_9908, plain, (![W_609]: (ifeq3(forename(skc8, W_609), true, forename(skc10, W_609), true)=true))). % 17.77/8.24 tff(c_1994, plain, (ifeq2(tuple2(specific(skc8, skc11), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2036, plain, (ifeq2(tuple2(nonexistent(skc8, skc12), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2244, plain, (ifeq2(tuple2(specific(skc8, skc14), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2077, plain, (ifeq2(tuple2(true, male(skc8, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2688, plain, (ifeq2(tuple2(true, general(skc8, skc12)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2080, plain, (ifeq2(tuple2(true, female(skc8, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2306, plain, (ifeq2(tuple2(true, human(skc8, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2651, plain, (ifeq2(tuple2(true, male(skc8, skc14)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2747, plain, (ifeq2(tuple2(nonexistent(skc8, skc15), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_2065, plain, (![U_317]: (ifeq3(accessible_world(U_317, skc8), true, ifeq3(vincent_forename(U_317, skc14), true, true, true), true)=true))). % 17.77/8.24 tff(c_2181, plain, (ifeq2(tuple2(true, human(skc8, skc11)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_1940, plain, (ifeq2(tuple2(true, general(skc8, skc15)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4328, plain, (ifeq2(tuple2(nonhuman(skc10, skc12), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_4565, plain, (ifeq2(tuple2(nonhuman(skc10, skc15), true), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_1479, plain, (ifeq2(tuple2(true, human(skc8, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_1745, plain, (ifeq2(tuple2(true, male(skc8, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_1792, plain, (ifeq2(tuple2(true, male(skc8, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_3016, plain, (![U_365]: (ifeq3(accessible_world(U_365, skc8), true, ifeq3(man(U_365, skc15), true, true, true), true)=true))). % 17.77/8.24 tff(c_5972, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc14), true)=true))). % 17.77/8.24 tff(c_1701, plain, (ifeq2(tuple2(true, general(skc8, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.24 tff(c_5940, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc11), true)=true))). % 17.77/8.24 tff(c_9739, plain, (![W_603]: (ifeq3(dance(skc8, W_603), true, dance(skc10, W_603), true)=true))). % 17.77/8.24 tff(c_5635, plain, (![V_115]: (ifeq3(accessible_world(skc10, V_115), true, nonhuman(V_115, skc14), true)=true))). % 17.77/8.24 tff(c_5763, plain, (![V_115]: (ifeq3(accessible_world(skc10, V_115), true, nonhuman(V_115, skc11), true)=true))). % 17.77/8.24 tff(c_5881, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc11), true)=true))). % 17.77/8.25 tff(c_5816, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc12), true)=true))). % 17.77/8.25 tff(c_5604, plain, (![V_97]: (ifeq3(accessible_world(skc10, V_97), true, unisex(V_97, skc11), true)=true))). % 17.77/8.25 tff(c_1795, plain, (ifeq2(tuple2(true, female(skc8, skc10)), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_9638, plain, (ifeq3(unisex(skc8, skc13), true, true, true)=true)). % 17.77/8.25 tff(c_9559, plain, (![W_596]: (ifeq3(unisex(skc8, W_596), true, unisex(skc10, W_596), true)=true))). % 17.77/8.25 tff(c_5672, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc14), true)=true))). % 17.77/8.25 tff(c_5844, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc15), true)=true))). % 17.77/8.25 tff(c_5728, plain, (![V_97]: (ifeq3(accessible_world(skc10, V_97), true, unisex(V_97, skc14), true)=true))). % 17.77/8.25 tff(c_5238, plain, (![V_142]: (ifeq3(accessible_world(skc10, V_142), true, existent(V_142, skc12), true)=true))). % 17.77/8.25 tff(c_5547, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc15), true)=true))). % 17.77/8.25 tff(c_1881, plain, (ifeq2(tuple2(specific(skc8, skc10), true), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_9454, plain, (ifeq3(singleton(skc8, skc13), true, true, true)=true)). % 17.77/8.25 tff(c_9347, plain, (![W_589]: (ifeq3(singleton(skc8, W_589), true, singleton(skc10, W_589), true)=true))). % 17.77/8.25 tff(c_5207, plain, (![V_142]: (ifeq3(accessible_world(skc10, V_142), true, existent(V_142, skc15), true)=true))). % 17.77/8.25 tff(c_5438, plain, (![V_112]: (ifeq3(accessible_world(skc10, V_112), true, abstraction(V_112, skc14), true)=true))). % 17.77/8.25 tff(c_5397, plain, (![V_112]: (ifeq3(accessible_world(skc10, V_112), true, abstraction(V_112, skc11), true)=true))). % 17.77/8.25 tff(c_5295, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc10), true)=true))). % 17.77/8.25 tff(c_3585, plain, (![V_88]: (ifeq3(accessible_world(skc10, V_88), true, singleton(V_88, skc9), true)=true))). % 17.77/8.25 tff(c_1748, plain, (ifeq2(tuple2(true, female(skc8, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_5509, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc12), true)=true))). % 17.77/8.25 tff(c_9178, plain, (![W_581]: (ifeq3(abstraction(skc8, W_581), true, abstraction(skc10, W_581), true)=true))). % 17.77/8.25 tff(c_2998, plain, (![V_88]: (ifeq3(accessible_world(skc8, V_88), true, singleton(V_88, skc15), true)=true))). % 17.77/8.25 tff(c_2812, plain, (![V_88]: (ifeq3(accessible_world(skc8, V_88), true, singleton(V_88, skc14), true)=true))). % 17.77/8.25 tff(c_2918, plain, (![V_88]: (ifeq3(accessible_world(skc8, V_88), true, singleton(V_88, skc12), true)=true))). % 17.77/8.25 tff(c_2864, plain, (![V_88]: (ifeq3(accessible_world(skc8, V_88), true, singleton(V_88, skc11), true)=true))). % 17.77/8.25 tff(c_3389, plain, (![V_94]: (ifeq3(accessible_world(skc10, V_94), true, nonexistent(V_94, skc9), true)=true))). % 17.77/8.25 tff(c_1832, plain, (ifeq2(tuple2(true, existent(skc8, skc9)), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_4932, plain, (![V_145]: (ifeq3(accessible_world(skc10, V_145), true, impartial(V_145, skc15), true)=true))). % 17.77/8.25 tff(c_8993, plain, (![W_573]: (ifeq3(nonhuman(skc8, W_573), true, nonhuman(skc10, W_573), true)=true))). % 17.77/8.25 tff(c_4878, plain, (![V_118]: (ifeq3(accessible_world(skc10, V_118), true, general(V_118, skc11), true)=true))). % 17.77/8.25 tff(c_3446, plain, (![V_91]: (ifeq3(accessible_world(skc10, V_91), true, specific(V_91, skc9), true)=true))). % 17.77/8.25 tff(c_5109, plain, (![V_139]: (ifeq3(accessible_world(skc10, V_139), true, entity(V_139, skc12), true)=true))). % 17.77/8.25 tff(c_4653, plain, (![V_115]: (ifeq3(accessible_world(skc10, V_115), true, nonhuman(V_115, skc10), true)=true))). % 17.77/8.25 tff(c_5018, plain, (![V_91]: (ifeq3(accessible_world(skc10, V_91), true, specific(V_91, skc12), true)=true))). % 17.77/8.25 tff(c_3908, plain, (ifeq2(tuple2(unisex(skc10, skc15), true), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_8898, plain, (ifeq3(nonexistent(skc8, skc13), true, true, true)=true)). % 17.77/8.25 tff(c_8861, plain, (![W_566]: (ifeq3(nonexistent(skc8, W_566), true, nonexistent(skc10, W_566), true)=true))). % 17.77/8.25 tff(c_4992, plain, (![V_145]: (ifeq3(accessible_world(skc10, V_145), true, impartial(V_145, skc12), true)=true))). % 17.77/8.25 tff(c_4771, plain, (![V_97]: (ifeq3(accessible_world(skc10, V_97), true, unisex(V_97, skc10), true)=true))). % 17.77/8.25 tff(c_5052, plain, (![V_91]: (ifeq3(accessible_world(skc10, V_91), true, specific(V_91, skc15), true)=true))). % 17.77/8.25 tff(c_5068, plain, (![V_148]: (ifeq3(accessible_world(skc10, V_148), true, living(V_148, skc12), true)=true))). % 17.77/8.25 tff(c_4622, plain, (![V_109]: (ifeq3(accessible_world(skc10, V_109), true, relation(V_109, skc11), true)=true))). % 17.77/8.25 tff(c_3911, plain, (ifeq2(tuple2(female(skc10, skc15), true), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_4734, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc10), true)=true))). % 17.77/8.25 tff(c_5175, plain, (![V_139]: (ifeq3(accessible_world(skc10, V_139), true, entity(V_139, skc15), true)=true))). % 17.77/8.25 tff(c_4904, plain, (![V_148]: (ifeq3(accessible_world(skc10, V_148), true, living(V_148, skc15), true)=true))). % 17.77/8.25 tff(c_1562, plain, (![U_290]: (ifeq3(accessible_world(U_290, skc8), true, ifeq3(forename(U_290, skc11), true, true, true), true)=true))). % 17.77/8.25 tff(c_4805, plain, (![V_109]: (ifeq3(accessible_world(skc10, V_109), true, relation(V_109, skc14), true)=true))). % 17.77/8.25 tff(c_3483, plain, (![V_85]: (ifeq3(accessible_world(skc10, V_85), true, thing(V_85, skc9), true)=true))). % 17.77/8.25 tff(c_4857, plain, (![V_118]: (ifeq3(accessible_world(skc10, V_118), true, general(V_118, skc14), true)=true))). % 17.77/8.25 tff(c_3335, plain, (![V_97]: (ifeq3(accessible_world(skc10, V_97), true, unisex(V_97, skc9), true)=true))). % 17.77/8.25 tff(c_4684, plain, (![V_118]: (ifeq3(accessible_world(skc10, V_118), true, general(V_118, skc10), true)=true))). % 17.77/8.25 tff(c_4235, plain, (ifeq2(tuple2(unisex(skc10, skc12), true), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_2312, plain, (![V_115]: (ifeq3(accessible_world(skc8, V_115), true, nonhuman(V_115, skc14), true)=true))). % 17.77/8.25 tff(c_2354, plain, (![V_330]: (ifeq3(accessible_world(skc8, V_330), true, unisex(V_330, skc11), true)=true))). % 17.77/8.25 tff(c_2697, plain, (![V_91]: (ifeq3(accessible_world(skc8, V_91), true, specific(V_91, skc12), true)=true))). % 17.77/8.25 tff(c_2934, plain, (![U_359]: (ifeq3(accessible_world(U_359, skc8), true, ifeq3(desire_want(U_359, skc9), true, true, true), true)=true))). % 17.77/8.25 tff(c_2219, plain, (![V_324]: (ifeq3(accessible_world(skc8, V_324), true, specific(V_324, skc15), true)=true))). % 17.77/8.25 tff(c_2729, plain, (![V_348]: (ifeq3(accessible_world(skc8, V_348), true, singleton(V_348, skc10), true)=true))). % 17.77/8.25 tff(c_2450, plain, (![V_85]: (ifeq3(accessible_world(skc8, V_85), true, thing(V_85, skc14), true)=true))). % 17.77/8.25 tff(c_2663, plain, (![V_97]: (ifeq3(accessible_world(skc8, V_97), true, unisex(V_97, skc14), true)=true))). % 17.77/8.25 tff(c_2000, plain, (![V_118]: (ifeq3(accessible_world(skc8, V_118), true, general(V_118, skc11), true)=true))). % 17.77/8.25 tff(c_4238, plain, (ifeq2(tuple2(true, male(skc10, skc12)), tuple2(true, true), a, b)=b)). % 17.77/8.25 tff(c_2156, plain, (![V_85]: (ifeq3(accessible_world(skc8, V_85), true, thing(V_85, skc12), true)=true))). % 17.77/8.25 tff(c_8394, plain, (![W_540]: (ifeq3(entity(skc8, W_540), true, entity(skc10, W_540), true)=true))). % 17.77/8.25 tff(c_2540, plain, (![V_85]: (ifeq3(accessible_world(skc8, V_85), true, thing(V_85, skc15), true)=true))). % 17.77/8.25 tff(c_2187, plain, (![V_115]: (ifeq3(accessible_world(skc8, V_115), true, nonhuman(V_115, skc11), true)=true))). % 17.77/8.25 tff(c_2602, plain, (![V_85]: (ifeq3(accessible_world(skc8, V_85), true, thing(V_85, skc11), true)=true))). % 17.77/8.25 tff(c_8314, plain, (ifeq3(event(skc8, skc13), true, true, true)=true)). % 18.06/8.25 tff(c_2730, plain, (![V_348]: (ifeq3(accessible_world(skc8, V_348), true, singleton(V_348, skc9), true)=true))). % 18.06/8.25 tff(c_2838, plain, (![V_354]: (ifeq3(accessible_world(skc8, V_354), true, existent(V_354, skc15), true)=true))). % 18.06/8.25 tff(c_2839, plain, (![V_354]: (ifeq3(accessible_world(skc8, V_354), true, existent(V_354, skc12), true)=true))). % 18.06/8.25 tff(c_2571, plain, (![U_341]: (ifeq3(accessible_world(U_341, skc10), true, ifeq3(event(U_341, skc13), true, true, true), true)=true))). % 18.06/8.25 tff(c_2250, plain, (![V_118]: (ifeq3(accessible_world(skc8, V_118), true, general(V_118, skc14), true)=true))). % 18.06/8.25 tff(c_4491, plain, (![V_136]: (ifeq3(accessible_world(skc10, V_136), true, organism(V_136, skc12), true)=true))). % 18.06/8.25 tff(c_4450, plain, (![V_136]: (ifeq3(accessible_world(skc10, V_136), true, organism(V_136, skc15), true)=true))). % 18.06/8.25 tff(c_4571, plain, (![V_151]: (ifeq3(accessible_world(skc10, V_151), true, human(V_151, skc15), true)=true))). % 18.06/8.25 tff(c_4334, plain, (![V_151]: (ifeq3(accessible_world(skc10, V_151), true, human(V_151, skc12), true)=true))). % 18.06/8.25 tff(c_1355, plain, (ifeq2(tuple2(true, female(skc10, skc13)), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_4366, plain, (![V_154]: (ifeq3(accessible_world(skc10, V_154), true, animate(V_154, skc15), true)=true))). % 18.06/8.25 tff(c_8088, plain, (![W_525]: (ifeq3(animate(skc8, W_525), true, animate(skc10, W_525), true)=true))). % 18.06/8.25 tff(c_3270, plain, (![V_82]: (ifeq3(accessible_world(skc10, V_82), true, eventuality(V_82, skc9), true)=true))). % 18.06/8.25 tff(c_4035, plain, (![V_124]: (ifeq3(accessible_world(skc10, V_124), true, relname(V_124, skc11), true)=true))). % 18.06/8.25 tff(c_4413, plain, (![V_154]: (ifeq3(accessible_world(skc10, V_154), true, animate(V_154, skc12), true)=true))). % 18.06/8.25 tff(c_4162, plain, (![V_112]: (ifeq3(accessible_world(skc10, V_112), true, abstraction(V_112, skc10), true)=true))). % 18.06/8.25 tff(c_4532, plain, (![V_124]: (ifeq3(accessible_world(skc10, V_124), true, relname(V_124, skc14), true)=true))). % 18.06/8.25 tff(c_1440, plain, (ifeq2(tuple2(nonhuman(skc8, skc15), true), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_2281, plain, (![V_327]: (ifeq3(accessible_world(skc8, V_327), true, abstraction(V_327, skc14), true)=true))). % 18.06/8.25 tff(c_7931, plain, (![W_517]: (ifeq3(existent(skc8, W_517), true, existent(skc10, W_517), true)=true))). % 18.06/8.25 tff(c_2220, plain, (![V_324]: (ifeq3(accessible_world(skc8, V_324), true, specific(V_324, skc9), true)=true))). % 18.06/8.25 tff(c_3109, plain, (![V_373]: (ifeq3(accessible_world(skc8, V_373), true, living(V_373, skc15), true)=true))). % 18.06/8.25 tff(c_1838, plain, (![V_94]: (ifeq3(accessible_world(skc8, V_94), true, nonexistent(V_94, skc9), true)=true))). % 18.06/8.25 tff(c_3110, plain, (![V_373]: (ifeq3(accessible_world(skc8, V_373), true, living(V_373, skc12), true)=true))). % 18.06/8.25 tff(c_1919, plain, (![V_309]: (ifeq3(accessible_world(skc8, V_309), true, thing(V_309, skc10), true)=true))). % 18.06/8.25 tff(c_1437, plain, (ifeq2(tuple2(nonhuman(skc8, skc12), true), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_2638, plain, (![V_345]: (ifeq3(accessible_world(skc8, V_345), true, entity(V_345, skc12), true)=true))). % 18.06/8.25 tff(c_7754, plain, (![W_509]: (ifeq3(human_person(skc8, W_509), true, human_person(skc10, W_509), true)=true))). % 18.06/8.25 tff(c_3297, plain, (![V_383]: (ifeq3(accessible_world(skc8, V_383), true, impartial(V_383, skc15), true)=true))). % 18.06/8.25 tff(c_1917, plain, (![V_309]: (ifeq3(accessible_world(skc8, V_309), true, thing(V_309, skc9), true)=true))). % 18.06/8.25 tff(c_2283, plain, (![V_327]: (ifeq3(accessible_world(skc8, V_327), true, abstraction(V_327, skc11), true)=true))). % 18.06/8.25 tff(c_1684, plain, (![V_297]: (ifeq3(accessible_world(skc8, V_297), true, nonhuman(V_297, skc10), true)=true))). % 18.06/8.25 tff(c_3296, plain, (![V_383]: (ifeq3(accessible_world(skc8, V_383), true, impartial(V_383, skc12), true)=true))). % 18.06/8.25 tff(c_1528, plain, (ifeq2(tuple2(true, general(skc10, skc13)), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_2731, plain, (![V_348]: (ifeq3(accessible_world(skc10, V_348), true, singleton(V_348, skc13), true)=true))). % 18.06/8.25 tff(c_7601, plain, (![W_501]: (ifeq3(woman(skc8, W_501), true, woman(skc10, W_501), true)=true))). % 18.06/8.25 tff(c_2639, plain, (![V_345]: (ifeq3(accessible_world(skc8, V_345), true, entity(V_345, skc15), true)=true))). % 18.06/8.25 tff(c_1968, plain, (![V_312]: (ifeq3(accessible_world(skc8, V_312), true, general(V_312, skc10), true)=true))). % 18.06/8.25 tff(c_2355, plain, (![V_330]: (ifeq3(accessible_world(skc8, V_330), true, unisex(V_330, skc10), true)=true))). % 18.06/8.25 tff(c_2356, plain, (![V_330]: (ifeq3(accessible_world(skc8, V_330), true, unisex(V_330, skc9), true)=true))). % 18.06/8.25 tff(c_4122, plain, (![V_121]: (ifeq3(accessible_world(skc10, V_121), true, forename(V_121, skc14), true)=true))). % 18.06/8.25 tff(c_1471, plain, (ifeq2(tuple2(true, existent(skc10, skc13)), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_4284, plain, (![V_133]: (ifeq3(accessible_world(skc10, V_133), true, human_person(V_133, skc12), true)=true))). % 18.06/8.25 tff(c_7432, plain, (![W_493]: (ifeq3(living(skc8, W_493), true, living(skc10, W_493), true)=true))). % 18.06/8.25 tff(c_3213, plain, (![V_79]: (ifeq3(accessible_world(skc10, V_79), true, event(V_79, skc9), true)=true))). % 18.06/8.25 tff(c_3796, plain, (![V_133]: (ifeq3(accessible_world(skc10, V_133), true, human_person(V_133, skc15), true)=true))). % 18.06/8.25 tff(c_3917, plain, (![V_166]: (ifeq3(accessible_world(skc10, V_166), true, male(V_166, skc15), true)=true))). % 18.06/8.25 tff(c_4244, plain, (![V_157]: (ifeq3(accessible_world(skc10, V_157), true, female(V_157, skc12), true)=true))). % 18.06/8.25 tff(c_4004, plain, (![V_109]: (ifeq3(accessible_world(skc10, V_109), true, relation(V_109, skc10), true)=true))). % 18.06/8.25 tff(c_1398, plain, (ifeq2(tuple2(true, male(skc10, skc13)), tuple2(true, true), a, b)=b)). % 18.06/8.25 tff(c_3883, plain, (![V_121]: (ifeq3(accessible_world(skc10, V_121), true, forename(V_121, skc11), true)=true))). % 18.06/8.25 tff(c_7303, plain, (![V_485]: (ifeq3(accessible_world(skc10, V_485), true, present(V_485, skc13), true)=true))). % 18.06/8.26 tff(c_2132, plain, (![V_321]: (ifeq3(accessible_world(skc8, V_321), true, relation(V_321, skc14), true)=true))). % 18.06/8.26 tff(c_1864, plain, (![V_306]: (ifeq3(accessible_world(skc8, V_306), true, animate(V_306, skc15), true)=true))). % 18.06/8.26 tff(c_1786, plain, (![V_303]: (ifeq3(accessible_world(skc10, V_303), true, nonexistent(V_303, skc13), true)=true))). % 18.06/8.26 tff(c_2282, plain, (![V_327]: (ifeq3(accessible_world(skc8, V_327), true, abstraction(V_327, skc10), true)=true))). % 18.06/8.26 tff(c_2221, plain, (![V_324]: (ifeq3(accessible_world(skc10, V_324), true, specific(V_324, skc13), true)=true))). % 18.06/8.26 tff(c_1358, plain, (ifeq2(tuple2(unisex(skc8, skc12), true), tuple2(true, true), a, b)=b)). % 18.06/8.26 tff(c_3176, plain, (![V_377]: (ifeq3(accessible_world(skc8, V_377), true, eventuality(V_377, skc9), true)=true))). % 18.06/8.26 tff(c_2506, plain, (![V_339]: (ifeq3(accessible_world(skc8, V_339), true, human(V_339, skc15), true)=true))). % 18.06/8.26 tff(c_1637, plain, (![V_294]: (ifeq3(accessible_world(skc8, V_294), true, organism(V_294, skc15), true)=true))). % 18.06/8.26 tff(c_3036, plain, (![U_368]: (ifeq3(accessible_world(U_368, skc8), true, ifeq3(woman(U_368, skc12), true, true, true), true)=true))). % 18.06/8.26 tff(c_1918, plain, (![V_309]: (ifeq3(accessible_world(skc10, V_309), true, thing(V_309, skc13), true)=true))). % 18.06/8.26 tff(c_1636, plain, (![V_294]: (ifeq3(accessible_world(skc8, V_294), true, organism(V_294, skc12), true)=true))). % 18.06/8.26 tff(c_2505, plain, (![V_339]: (ifeq3(accessible_world(skc8, V_339), true, human(V_339, skc12), true)=true))). % 18.06/8.26 tff(c_2131, plain, (![V_321]: (ifeq3(accessible_world(skc8, V_321), true, relation(V_321, skc11), true)=true))). % 18.06/8.26 tff(c_1863, plain, (![V_306]: (ifeq3(accessible_world(skc8, V_306), true, animate(V_306, skc12), true)=true))). % 18.06/8.26 tff(c_1401, plain, (ifeq2(tuple2(unisex(skc8, skc15), true), tuple2(true, true), a, b)=b)). % 18.06/8.26 tff(c_2357, plain, (![V_330]: (ifeq3(accessible_world(skc10, V_330), true, unisex(V_330, skc13), true)=true))). % 18.06/8.26 tff(c_7003, plain, (![W_468]: (ifeq3(desire_want(skc8, W_468), true, desire_want(skc10, W_468), true)=true))). % 18.06/8.26 tff(c_3842, plain, (![V_127]: (ifeq3(accessible_world(skc10, V_127), true, mia_forename(V_127, skc11), true)=true))). % 18.06/8.26 tff(c_3971, plain, (![V_106]: (ifeq3(accessible_world(skc10, V_106), true, proposition(V_106, skc10), true)=true))). % 18.06/8.26 tff(c_4211, plain, (![V_130]: (ifeq3(accessible_world(skc10, V_130), true, woman(V_130, skc12), true)=true))). % 18.06/8.26 tff(c_4081, plain, (![V_160]: (ifeq3(accessible_world(skc10, V_160), true, vincent_forename(V_160, skc14), true)=true))). % 18.06/8.26 tff(c_3757, plain, (![V_163]: (ifeq3(accessible_world(skc10, V_163), true, man(V_163, skc15), true)=true))). % 18.06/8.26 tff(c_1298, plain, (ifeq2(tuple2(true, male(skc8, skc12)), tuple2(true, true), a, b)=b)). % 18.06/8.26 tff(c_3152, plain, (![V_103]: (ifeq3(accessible_world(skc10, V_103), true, desire_want(V_103, skc9), true)=true))). % 18.06/8.26 tff(c_6866, plain, (![W_460]: (ifeq3(mia_forename(skc8, W_460), true, mia_forename(skc10, W_460), true)=true))). % 18.06/8.26 tff(c_2475, plain, (![V_336]: (ifeq3(accessible_world(skc8, V_336), true, relname(V_336, skc14), true)=true))). % 18.06/8.26 tff(c_3177, plain, (![V_377]: (ifeq3(accessible_world(skc10, V_377), true, eventuality(V_377, skc13), true)=true))). % 18.06/8.26 tff(c_2884, plain, (![V_357]: (ifeq3(accessible_world(skc8, V_357), true, female(V_357, skc12), true)=true))). % 18.06/8.26 tff(c_1739, plain, (![V_300]: (ifeq3(accessible_world(skc8, V_300), true, male(V_300, skc15), true)=true))). % 18.06/8.26 tff(c_2577, plain, (![V_342]: (ifeq3(accessible_world(skc8, V_342), true, event(V_342, skc9), true)=true))). % 18.06/8.26 tff(c_1301, plain, (ifeq2(tuple2(female(skc8, skc15), true), tuple2(true, true), a, b)=b)). % 18.06/8.26 tff(c_2778, plain, (![V_351]: (ifeq3(accessible_world(skc8, V_351), true, human_person(V_351, skc12), true)=true))). % 18.06/8.26 tff(c_6713, plain, (![W_452]: (ifeq3(man(skc8, W_452), true, man(skc10, W_452), true)=true))). % 18.06/8.26 tff(c_2476, plain, (![V_336]: (ifeq3(accessible_world(skc8, V_336), true, relname(V_336, skc11), true)=true))). % 18.06/8.26 tff(c_2779, plain, (![V_351]: (ifeq3(accessible_world(skc8, V_351), true, human_person(V_351, skc15), true)=true))). % 18.06/8.26 tff(c_2130, plain, (![V_321]: (ifeq3(accessible_world(skc8, V_321), true, relation(V_321, skc10), true)=true))). % 18.06/8.26 tff(c_6633, plain, (ifeq3(dance(skc8, skc13), true, true, true)=true)). % 18.06/8.26 tff(c_6606, plain, (ifeq3(thing(skc8, skc13), true, true, true)=true)). % 18.06/8.26 tff(c_6502, plain, (![W_447]: (ifeq3(thing(skc8, W_447), true, thing(skc10, W_447), true)=true))). % 18.06/8.26 tff(c_6402, plain, (![W_443]: (ifeq3(relname(skc8, W_443), true, relname(skc10, W_443), true)=true))). % 18.06/8.26 tff(c_5784, plain, (![W_432]: (ifeq3(vincent_forename(skc8, W_432), true, vincent_forename(skc10, W_432), true)=true))). % 18.06/8.26 tff(c_5449, plain, (![W_429]: (ifeq3(impartial(skc8, W_429), true, impartial(skc10, W_429), true)=true))). % 18.06/8.26 tff(c_6370, plain, (ifeq3(specific(skc8, skc13), true, true, true)=true)). % 18.06/8.26 tff(c_4971, plain, (![W_425]: (ifeq3(specific(skc8, W_425), true, specific(skc10, W_425), true)=true))). % 18.06/8.26 tff(c_4814, plain, (![W_424]: (ifeq3(general(skc8, W_424), true, general(skc10, W_424), true)=true))). % 18.06/8.26 tff(c_5344, plain, (![W_428]: (ifeq3(relation(skc8, W_428), true, relation(skc10, W_428), true)=true))). % 18.06/8.26 tff(c_5263, plain, (![W_427]: (ifeq3(organism(skc8, W_427), true, organism(skc10, W_427), true)=true))). % 18.06/8.26 tff(c_6209, plain, (ifeq3(eventuality(skc8, skc13), true, true, true)=true)). % 18.06/8.26 tff(c_2389, plain, (![U_332]: (ifeq3(accessible_world(U_332, skc10), true, ifeq3(dance(U_332, skc13), true, true, true), true)=true))). % 18.06/8.26 tff(c_5118, plain, (![W_426]: (ifeq3(eventuality(skc8, W_426), true, eventuality(skc10, W_426), true)=true))). % 18.06/8.26 tff(c_6067, plain, (![W_435]: (ifeq3(human(skc8, W_435), true, human(skc10, W_435), true)=true))). % 18.06/8.26 tff(c_6130, plain, (of(skc10, skc11, skc12)=true)). % 18.06/8.26 tff(c_6095, plain, (of(skc10, skc14, skc15)=true)). % 18.06/8.26 tff(c_6039, plain, (agent(skc10, skc9, skc12)=true)). % 18.06/8.26 tff(c_4695, plain, (ifeq3(agent(skc8, skc13, skc12), true, true, true)=true)). % 18.06/8.26 tff(c_6000, plain, (theme(skc10, skc9, skc10)=true)). % 18.06/8.26 tff(c_5601, plain, (ifeq3(eventuality(skc10, skc11), true, true, true)=true)). % 18.06/8.26 tff(c_1568, plain, (![U_290]: (ifeq3(accessible_world(U_290, skc8), true, ifeq3(forename(U_290, skc14), true, true, true), true)=true))). % 18.06/8.26 tff(c_5951, plain, (singleton(skc10, skc14)=true)). % 18.06/8.26 tff(c_5669, plain, (ifeq3(entity(skc10, skc14), true, true, true)=true)). % 18.06/8.26 tff(c_5919, plain, (singleton(skc10, skc11)=true)). % 18.06/8.26 tff(c_5878, plain, (ifeq3(entity(skc10, skc11), true, true, true)=true)). % 18.06/8.26 tff(c_5725, plain, (ifeq3(eventuality(skc10, skc14), true, true, true)=true)). % 18.06/8.26 tff(c_2966, plain, (![U_362]: (ifeq3(present(U_362, skc9), true, ifeq3(accessible_world(U_362, skc8), true, true, true), true)=true))). % 18.06/8.26 tff(c_5851, plain, (thing(skc10, skc11)=true)). % 18.06/8.26 tff(c_5823, plain, (singleton(skc10, skc15)=true)). % 18.06/8.26 tff(c_5795, plain, (singleton(skc10, skc12)=true)). % 18.06/8.26 tff(c_5500, plain, (ifeq3(abstraction(skc10, skc12), true, true, true)=true)). % 18.06/8.26 tff(c_5739, plain, (nonhuman(skc10, skc11)=true)). % 18.06/8.26 tff(c_5538, plain, (ifeq3(abstraction(skc10, skc15), true, true, true)=true)). % 18.06/8.26 tff(c_5698, plain, (unisex(skc10, skc14)=true)). % 18.06/8.26 tff(c_2957, plain, (![U_362]: (ifeq3(present(U_362, skc13), true, ifeq3(accessible_world(U_362, skc10), true, true, true), true)=true))). % 18.06/8.26 tff(c_5642, plain, (thing(skc10, skc14)=true)). % 18.06/8.26 tff(c_5611, plain, (nonhuman(skc10, skc14)=true)). % 18.06/8.26 tff(c_5574, plain, (unisex(skc10, skc11)=true)). % 18.06/8.26 tff(c_5565, plain, (ifeq3(accessible_world(skc10, skc8), true, true, true)=true)). % 18.06/8.26 tff(c_2013, plain, (![U_314]: (ifeq3(accessible_world(U_314, skc8), true, ifeq3(proposition(U_314, skc10), true, true, true), true)=true))). % 18.06/8.26 tff(c_5517, plain, (thing(skc10, skc15)=true)). % 18.06/8.26 tff(c_5479, plain, (thing(skc10, skc12)=true)). % 18.06/8.26 tff(c_5405, plain, (abstraction(skc10, skc14)=true)). % 18.06/8.26 tff(c_5364, plain, (abstraction(skc10, skc11)=true)). % 18.06/8.26 tff(c_4796, plain, (ifeq3(proposition(skc10, skc14), true, true, true)=true)). % 18.06/8.26 tff(c_5048, plain, (ifeq3(eventuality(skc10, skc15), true, true, true)=true)). % 18.06/8.26 tff(c_4731, plain, (ifeq3(entity(skc10, skc10), true, true, true)=true)). % 18.06/8.26 tff(c_4613, plain, (ifeq3(proposition(skc10, skc11), true, true, true)=true)). % 18.06/8.26 tff(c_4768, plain, (ifeq3(eventuality(skc10, skc10), true, true, true)=true)). % 18.06/8.26 tff(c_5014, plain, (ifeq3(eventuality(skc10, skc12), true, true, true)=true)). % 18.06/8.26 tff(c_5274, plain, (singleton(skc10, skc10)=true)). % 18.06/8.26 tff(c_5214, plain, (existent(skc10, skc12)=true)). % 18.06/8.26 tff(c_5183, plain, (existent(skc10, skc15)=true)). % 18.06/8.26 tff(c_5141, plain, (entity(skc10, skc15)=true)). % 18.06/8.26 tff(c_5075, plain, (entity(skc10, skc12)=true)). % 18.06/8.26 tff(c_5023, plain, (living(skc10, skc12)=true)). % 18.06/8.26 tff(c_4976, plain, (specific(skc10, skc15)=true)). % 18.06/8.26 tff(c_4975, plain, (specific(skc10, skc12)=true)). % 18.06/8.26 tff(c_4939, plain, (impartial(skc10, skc12)=true)). % 18.06/8.26 tff(c_4911, plain, (impartial(skc10, skc15)=true)). % 18.06/8.26 tff(c_4883, plain, (living(skc10, skc15)=true)). % 18.06/8.26 tff(c_4836, plain, (general(skc10, skc11)=true)). % 18.06/8.26 tff(c_4835, plain, (general(skc10, skc14)=true)). % 18.06/8.26 tff(c_4778, plain, (relation(skc10, skc14)=true)). % 18.06/8.26 tff(c_4741, plain, (unisex(skc10, skc10)=true)). % 18.06/8.26 tff(c_4704, plain, (thing(skc10, skc10)=true)). % 18.06/8.26 tff(c_3425, plain, (![W_390, X_391]: (ifeq3(agent(skc8, W_390, X_391), true, agent(skc10, W_390, X_391), true)=true))). % 18.06/8.26 tff(c_4660, plain, (general(skc10, skc10)=true)). % 18.06/8.26 tff(c_4629, plain, (nonhuman(skc10, skc10)=true)). % 18.06/8.26 tff(c_4595, plain, (relation(skc10, skc11)=true)). % 18.06/8.26 tff(c_3371, plain, (![W_386, X_387]: (ifeq3(of(skc8, W_386, X_387), true, of(skc10, W_386, X_387), true)=true))). % 18.06/8.26 tff(c_3781, plain, (ifeq3(woman(skc10, skc15), true, true, true)=true)). % 18.06/8.26 tff(c_4547, plain, (human(skc10, skc15)=true)). % 18.06/8.26 tff(c_3878, plain, (ifeq3(vincent_forename(skc10, skc11), true, true, true)=true)). % 18.06/8.26 tff(c_4275, plain, (ifeq3(man(skc10, skc12), true, true, true)=true)). % 18.06/8.26 tff(c_4508, plain, (relname(skc10, skc14)=true)). % 18.06/8.26 tff(c_3503, plain, (![W_394, X_395]: (ifeq3(theme(skc8, W_394, X_395), true, theme(skc10, W_394, X_395), true)=true))). % 18.06/8.26 tff(c_4461, plain, (organism(skc10, skc12)=true)). % 18.06/8.26 tff(c_4111, plain, (ifeq3(mia_forename(skc10, skc14), true, true, true)=true)). % 18.06/8.26 tff(c_4420, plain, (organism(skc10, skc15)=true)). % 18.06/8.26 tff(c_4373, plain, (animate(skc10, skc12)=true)). % 18.06/8.26 tff(c_1574, plain, (![V_291]: (ifeq3(accessible_world(skc8, V_291), true, forename(V_291, skc11), true)=true))). % 18.06/8.26 tff(c_4345, plain, (animate(skc10, skc15)=true)). % 18.06/8.26 tff(c_4001, plain, (ifeq3(relname(skc10, skc10), true, true, true)=true)). % 18.06/8.26 tff(c_4310, plain, (human(skc10, skc12)=true)). % 18.06/8.26 tff(c_1575, plain, (![V_291]: (ifeq3(accessible_world(skc8, V_291), true, forename(V_291, skc14), true)=true))). % 18.06/8.26 tff(c_4251, plain, (human_person(skc10, skc12)=true)). % 18.06/8.26 tff(c_4217, plain, (female(skc10, skc12)=true)). % 18.06/8.26 tff(c_4183, plain, (woman(skc10, skc12)=true)). % 18.06/8.26 tff(c_3042, plain, (![V_369]: (ifeq3(accessible_world(skc8, V_369), true, woman(V_369, skc12), true)=true))). % 18.06/8.26 tff(c_4129, plain, (abstraction(skc10, skc10)=true)). % 18.06/8.26 tff(c_4087, plain, (forename(skc10, skc14)=true)). % 18.06/8.26 tff(c_4056, plain, (vincent_forename(skc10, skc14)=true)). % 18.06/8.26 tff(c_2071, plain, (![V_318]: (ifeq3(accessible_world(skc8, V_318), true, vincent_forename(V_318, skc14), true)=true))). % 18.06/8.26 tff(c_4011, plain, (relname(skc10, skc11)=true)). % 18.06/8.26 tff(c_3977, plain, (relation(skc10, skc10)=true)). % 18.06/8.26 tff(c_3938, plain, (proposition(skc10, skc10)=true)). % 18.06/8.26 tff(c_2019, plain, (![V_315]: (ifeq3(accessible_world(skc8, V_315), true, proposition(V_315, skc10), true)=true))). % 18.06/8.26 tff(c_3890, plain, (male(skc10, skc15)=true)). % 18.06/8.26 tff(c_3848, plain, (forename(skc10, skc11)=true)). % 18.06/8.26 tff(c_3817, plain, (mia_forename(skc10, skc11)=true)). % 18.06/8.26 tff(c_3233, plain, (![V_380]: (ifeq3(accessible_world(skc8, V_380), true, mia_forename(V_380, skc11), true)=true))). % 18.06/8.26 tff(c_3763, plain, (human_person(skc10, skc15)=true)). % 18.06/8.26 tff(c_3729, plain, (man(skc10, skc15)=true)). % 18.06/8.27 tff(c_194, plain, (![V_201, W_202, U_203]: (ifeq(tuple(dance(V_201, W_202), event(V_201, W_202), desire_want(skc8, U_203), proposition(skc8, V_201), accessible_world(skc8, V_201), present(V_201, W_202), present(skc8, U_203), agent(V_201, W_202, skc15), agent(skc8, U_203, skc15), theme(skc8, U_203, V_201)), tuple(true, true, true, true, true, true, true, true, true, true), a, b)=b))). % 18.06/8.27 tff(c_3022, plain, (![V_366]: (ifeq3(accessible_world(skc8, V_366), true, man(V_366, skc15), true)=true))). % 18.06/8.27 tff(c_2395, plain, (![V_333]: (ifeq3(accessible_world(skc10, V_333), true, dance(V_333, skc13), true)=true))). % 18.06/8.27 tff(c_3598, plain, (ifeq3(accessible_world(skc10, skc10), true, true, true)=true)). % 18.06/8.27 tff(c_142, plain, (![Y_187, U_185, X_186, V_188, W_184]: (ifeq4(theme(U_185, Y_187, X_186), true, ifeq4(theme(U_185, V_188, W_184), true, ifeq4(proposition(U_185, X_186), true, ifeq4(proposition(U_185, W_184), true, ifeq4(desire_want(U_185, Y_187), true, ifeq4(desire_want(U_185, V_188), true, X_186, W_184), W_184), W_184), W_184), W_184), W_184)=W_184))). % 18.06/8.27 tff(c_2578, plain, (![V_342]: (ifeq3(accessible_world(skc10, V_342), true, event(V_342, skc13), true)=true))). % 18.06/8.27 tff(c_3515, plain, (singleton(skc10, skc9)=true)). % 18.06/8.27 tff(c_140, plain, (![U_180, W_181, X_182, V_183]: (ifeq4(of(U_180, W_181, X_182), true, ifeq4(of(U_180, V_183, X_182), true, ifeq4(entity(U_180, X_182), true, ifeq4(forename(U_180, W_181), true, ifeq4(forename(U_180, V_183), true, W_181, V_183), V_183), V_183), V_183), V_183)=V_183))). % 18.06/8.27 tff(c_3480, plain, (ifeq3(entity(skc10, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_3329, plain, (ifeq3(abstraction(skc10, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_136, plain, (![U_172, W_173, X_174, V_175]: (ifeq3(theme(U_172, W_173, X_174), true, ifeq3(accessible_world(U_172, V_175), true, theme(V_175, W_173, X_174), true), true)=true))). % 18.06/8.27 tff(c_3453, plain, (thing(skc10, skc9)=true)). % 18.06/8.27 tff(c_3396, plain, (specific(skc10, skc9)=true)). % 18.06/8.27 tff(c_134, plain, (![U_168, W_169, X_170, V_171]: (ifeq3(agent(U_168, W_169, X_170), true, ifeq3(accessible_world(U_168, V_171), true, agent(V_171, W_169, X_170), true), true)=true))). % 18.06/8.27 tff(c_3342, plain, (nonexistent(skc10, skc9)=true)). % 18.06/8.27 tff(c_138, plain, (![U_176, W_177, X_178, V_179]: (ifeq3(of(U_176, W_177, X_178), true, ifeq3(accessible_world(U_176, V_179), true, of(V_179, W_177, X_178), true), true)=true))). % 18.06/8.27 tff(c_3305, plain, (unisex(skc10, skc9)=true)). % 18.06/8.27 tff(c_3210, plain, (ifeq3(dance(skc10, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_118, plain, (![U_144, V_145, W_146]: (ifeq3(accessible_world(U_144, V_145), true, ifeq3(impartial(U_144, W_146), true, impartial(V_145, W_146), true), true)=true))). % 18.06/8.27 tff(c_3237, plain, (eventuality(skc10, skc9)=true)). % 18.06/8.27 tff(c_106, plain, (![U_126, V_127, W_128]: (ifeq3(accessible_world(U_126, V_127), true, ifeq3(mia_forename(U_126, W_128), true, mia_forename(V_127, W_128), true), true)=true))). % 18.06/8.27 tff(c_3186, plain, (event(skc10, skc9)=true)). % 18.06/8.27 tff(c_3121, plain, (ifeq3(accessible_world(skc8, skc8), true, true, true)=true)). % 18.06/8.27 tff(c_76, plain, (![U_81, V_82, W_83]: (ifeq3(accessible_world(U_81, V_82), true, ifeq3(eventuality(U_81, W_83), true, eventuality(V_82, W_83), true), true)=true))). % 18.06/8.27 tff(c_3127, plain, (desire_want(skc10, skc9)=true)). % 18.06/8.27 tff(c_2937, plain, (![V_360]: (ifeq3(accessible_world(skc8, V_360), true, desire_want(V_360, skc9), true)=true))). % 18.06/8.27 tff(c_120, plain, (![U_147, V_148, W_149]: (ifeq3(accessible_world(U_147, V_148), true, ifeq3(living(U_147, W_149), true, living(V_148, W_149), true), true)=true))). % 18.06/8.27 tff(c_3063, plain, (present(skc10, skc9)=true)). % 18.06/8.27 tff(c_3050, plain, (ifeq3(present(skc8, skc13), true, true, true)=true)). % 18.06/8.27 tff(c_2969, plain, (![W_363]: (ifeq3(present(skc8, W_363), true, present(skc10, W_363), true)=true))). % 18.06/8.27 tff(c_108, plain, (![U_129, V_130, W_131]: (ifeq3(accessible_world(U_129, V_130), true, ifeq3(woman(U_129, W_131), true, woman(V_130, W_131), true), true)=true))). % 18.06/8.27 tff(c_130, plain, (![U_162, V_163, W_164]: (ifeq3(accessible_world(U_162, V_163), true, ifeq3(man(U_162, W_164), true, man(V_163, W_164), true), true)=true))). % 18.06/8.27 tff(c_2531, plain, (ifeq3(abstraction(skc8, skc15), true, true, true)=true)). % 18.06/8.27 tff(c_2977, plain, (singleton(skc8, skc15)=true)). % 18.06/8.27 tff(c_2447, plain, (ifeq3(entity(skc8, skc14), true, true, true)=true)). % 18.06/8.27 tff(c_88, plain, (![U_99, W_100, V_101]: (ifeq3(present(U_99, W_100), true, ifeq3(accessible_world(U_99, V_101), true, present(V_101, W_100), true), true)=true))). % 18.06/8.27 tff(c_2599, plain, (ifeq3(entity(skc8, skc11), true, true, true)=true)). % 18.06/8.27 tff(c_2438, plain, (ifeq3(eventuality(skc8, skc14), true, true, true)=true)). % 18.06/8.27 tff(c_90, plain, (![U_102, V_103, W_104]: (ifeq3(accessible_world(U_102, V_103), true, ifeq3(desire_want(U_102, W_104), true, desire_want(V_103, W_104), true), true)=true))). % 18.06/8.27 tff(c_2897, plain, (singleton(skc8, skc12)=true)). % 18.06/8.27 tff(c_2590, plain, (ifeq3(eventuality(skc8, skc11), true, true, true)=true)). % 18.06/8.27 tff(c_2147, plain, (ifeq3(abstraction(skc8, skc12), true, true, true)=true)). % 18.06/8.27 tff(c_126, plain, (![U_156, V_157, W_158]: (ifeq3(accessible_world(U_156, V_157), true, ifeq3(female(U_156, W_158), true, female(V_157, W_158), true), true)=true))). % 18.06/8.27 tff(c_2843, plain, (singleton(skc8, skc11)=true)). % 18.06/8.27 tff(c_116, plain, (![U_141, V_142, W_143]: (ifeq3(accessible_world(U_141, V_142), true, ifeq3(existent(U_141, W_143), true, existent(V_142, W_143), true), true)=true))). % 18.06/8.27 tff(c_2791, plain, (singleton(skc8, skc14)=true)). % 18.06/8.27 tff(c_1946, plain, (ifeq3(eventuality(skc8, skc15), true, true, true)=true)). % 18.06/8.27 tff(c_2694, plain, (ifeq3(eventuality(skc8, skc12), true, true, true)=true)). % 18.06/8.27 tff(c_110, plain, (![U_132, V_133, W_134]: (ifeq3(accessible_world(U_132, V_133), true, ifeq3(human_person(U_132, W_134), true, human_person(V_133, W_134), true), true)=true))). % 18.06/8.27 tff(c_2735, plain, (existent(skc8, skc15)=true)). % 18.06/8.27 tff(c_80, plain, (![U_87, V_88, W_89]: (ifeq3(accessible_world(U_87, V_88), true, ifeq3(singleton(U_87, W_89), true, singleton(V_88, W_89), true), true)=true))). % 18.06/8.27 tff(c_2670, plain, (specific(skc8, skc12)=true)). % 18.06/8.27 tff(c_2609, plain, (unisex(skc8, skc14)=true)). % 18.06/8.27 tff(c_114, plain, (![U_138, V_139, W_140]: (ifeq3(accessible_world(U_138, V_139), true, ifeq3(entity(U_138, W_140), true, entity(V_139, W_140), true), true)=true))). % 18.06/8.27 tff(c_2548, plain, (thing(skc8, skc11)=true)). % 18.06/8.27 tff(c_74, plain, (![U_78, V_79, W_80]: (ifeq3(accessible_world(U_78, V_79), true, ifeq3(event(U_78, W_80), true, event(V_79, W_80), true), true)=true))). % 18.06/8.27 tff(c_2510, plain, (thing(skc8, skc15)=true)). % 18.06/8.27 tff(c_122, plain, (![U_150, V_151, W_152]: (ifeq3(accessible_world(U_150, V_151), true, ifeq3(human(U_150, W_152), true, human(V_151, W_152), true), true)=true))). % 18.06/8.27 tff(c_1516, plain, (ifeq3(entity(skc8, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_104, plain, (![U_123, V_124, W_125]: (ifeq3(accessible_world(U_123, V_124), true, ifeq3(relname(U_123, W_125), true, relname(V_124, W_125), true), true)=true))). % 18.06/8.27 tff(c_2420, plain, (thing(skc8, skc14)=true)). % 18.06/8.27 tff(c_2399, plain, (singleton(skc8, skc10)=true)). % 18.06/8.27 tff(c_72, plain, (![U_75, V_76, W_77]: (ifeq3(accessible_world(U_75, V_76), true, ifeq3(dance(U_75, W_77), true, dance(V_76, W_77), true), true)=true))). % 18.06/8.27 tff(c_2361, plain, (singleton(skc8, skc9)=true)). % 18.06/8.27 tff(c_86, plain, (![U_96, V_97, W_98]: (ifeq3(accessible_world(U_96, V_97), true, ifeq3(unisex(U_96, W_98), true, unisex(V_97, W_98), true), true)=true))). % 18.06/8.27 tff(c_1179, plain, (ifeq3(entity(skc8, skc10), true, true, true)=true)). % 18.06/8.27 tff(c_2288, plain, (nonhuman(skc8, skc14)=true)). % 18.06/8.27 tff(c_96, plain, (![U_111, V_112, W_113]: (ifeq3(accessible_world(U_111, V_112), true, ifeq3(abstraction(U_111, W_113), true, abstraction(V_112, W_113), true), true)=true))). % 18.06/8.27 tff(c_2226, plain, (general(skc8, skc14)=true)). % 18.06/8.27 tff(c_82, plain, (![U_90, V_91, W_92]: (ifeq3(accessible_world(U_90, V_91), true, ifeq3(specific(U_90, W_92), true, specific(V_91, W_92), true), true)=true))). % 18.06/8.27 tff(c_2163, plain, (nonhuman(skc8, skc11)=true)). % 18.06/8.27 tff(c_2095, plain, (thing(skc8, skc12)=true)). % 18.06/8.27 tff(c_94, plain, (![U_108, V_109, W_110]: (ifeq3(accessible_world(U_108, V_109), true, ifeq3(relation(U_108, W_110), true, relation(V_109, W_110), true), true)=true))). % 18.06/8.27 tff(c_2048, plain, (unisex(skc8, skc11)=true)). % 18.06/8.27 tff(c_128, plain, (![U_159, V_160, W_161]: (ifeq3(accessible_world(U_159, V_160), true, ifeq3(vincent_forename(U_159, W_161), true, vincent_forename(V_160, W_161), true), true)=true))). % 18.06/8.27 tff(c_2024, plain, (existent(skc8, skc12)=true)). % 18.06/8.27 tff(c_92, plain, (![U_105, V_106, W_107]: (ifeq3(accessible_world(U_105, V_106), true, ifeq3(proposition(U_105, W_107), true, proposition(V_106, W_107), true), true)=true))). % 18.06/8.27 tff(c_1976, plain, (general(skc8, skc11)=true)). % 18.06/8.27 tff(c_1751, plain, (ifeq3(abstraction(skc8, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_100, plain, (![U_117, V_118, W_119]: (ifeq3(accessible_world(U_117, V_118), true, ifeq3(general(U_117, W_119), true, general(V_118, W_119), true), true)=true))). % 18.06/8.27 tff(c_1928, plain, (specific(skc8, skc15)=true)). % 18.06/8.27 tff(c_1801, plain, (ifeq3(eventuality(skc8, skc10), true, true, true)=true)). % 18.06/8.27 tff(c_78, plain, (![U_84, V_85, W_86]: (ifeq3(accessible_world(U_84, V_85), true, ifeq3(thing(U_84, W_86), true, thing(V_85, W_86), true), true)=true))). % 18.06/8.27 tff(c_1869, plain, (general(skc8, skc10)=true)). % 18.06/8.27 tff(c_124, plain, (![U_153, V_154, W_155]: (ifeq3(accessible_world(U_153, V_154), true, ifeq3(animate(U_153, W_155), true, animate(V_154, W_155), true), true)=true))). % 18.06/8.27 tff(c_1814, plain, (nonexistent(skc8, skc9)=true)). % 18.06/8.27 tff(c_1056, plain, (ifeq3(proposition(skc8, skc14), true, true, true)=true)). % 18.06/8.27 tff(c_1763, plain, (unisex(skc8, skc10)=true)). % 18.06/8.27 tff(c_84, plain, (![U_93, V_94, W_95]: (ifeq3(accessible_world(U_93, V_94), true, ifeq3(nonexistent(U_93, W_95), true, nonexistent(V_94, W_95), true), true)=true))). % 18.06/8.27 tff(c_1716, plain, (unisex(skc8, skc9)=true)). % 18.06/8.27 tff(c_132, plain, (![U_165, V_166, W_167]: (ifeq3(accessible_world(U_165, V_166), true, ifeq3(male(U_165, W_167), true, male(V_166, W_167), true), true)=true))). % 18.06/8.27 tff(c_1689, plain, (specific(skc8, skc9)=true)). % 18.06/8.27 tff(c_98, plain, (![U_114, V_115, W_116]: (ifeq3(accessible_world(U_114, V_115), true, ifeq3(nonhuman(U_114, W_116), true, nonhuman(V_115, W_116), true), true)=true))). % 18.06/8.27 tff(c_1642, plain, (entity(skc8, skc12)=true)). % 18.06/8.27 tff(c_112, plain, (![U_135, V_136, W_137]: (ifeq3(accessible_world(U_135, V_136), true, ifeq3(organism(U_135, W_137), true, organism(V_136, W_137), true), true)=true))). % 18.06/8.27 tff(c_1585, plain, (abstraction(skc8, skc14)=true)). % 18.06/8.27 tff(c_1053, plain, (ifeq3(proposition(skc8, skc11), true, true, true)=true)). % 18.06/8.27 tff(c_102, plain, (![U_120, V_121, W_122]: (ifeq3(accessible_world(U_120, V_121), true, ifeq3(forename(U_120, W_122), true, forename(V_121, W_122), true), true)=true))). % 18.06/8.27 tff(c_1535, plain, (living(skc8, skc15)=true)). % 18.06/8.27 tff(c_186, plain, (![U_193, V_194]: (ifeq2(tuple2(specific(U_193, V_194), general(U_193, V_194)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1495, plain, (thing(skc8, skc9)=true)). % 18.06/8.27 tff(c_1246, plain, (ifeq3(entity(skc10, skc13), true, true, true)=true)). % 18.06/8.27 tff(c_1461, plain, (nonhuman(skc8, skc10)=true)). % 18.06/8.27 tff(c_192, plain, (![U_199, V_200]: (ifeq2(tuple2(nonexistent(U_199, V_200), existent(U_199, V_200)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1423, plain, (singleton(skc10, skc13)=true)). % 18.06/8.27 tff(c_188, plain, (![U_195, V_196]: (ifeq2(tuple2(nonhuman(U_195, V_196), human(U_195, V_196)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1283, plain, (ifeq3(abstraction(skc10, skc13), true, true, true)=true)). % 18.06/8.27 tff(c_1388, plain, (nonexistent(skc10, skc13)=true)). % 18.06/8.27 tff(c_182, plain, (![U_189, V_190]: (ifeq2(tuple2(unisex(U_189, V_190), male(U_189, V_190)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1341, plain, (thing(skc10, skc13)=true)). % 18.06/8.27 tff(c_184, plain, (![U_191, V_192]: (ifeq2(tuple2(unisex(U_191, V_192), female(U_191, V_192)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1308, plain, (eventuality(skc8, skc9)=true)). % 18.06/8.27 tff(c_190, plain, (![U_197, V_198]: (ifeq2(tuple2(female(U_197, V_198), male(U_197, V_198)), tuple2(true, true), a, b)=b))). % 18.06/8.27 tff(c_1271, plain, (unisex(skc10, skc13)=true)). % 18.06/8.27 tff(c_32, plain, (![U_35, V_36]: (ifeq3(abstraction(U_35, V_36), true, nonhuman(U_35, V_36), true)=true))). % 18.06/8.27 tff(c_1234, plain, (specific(skc10, skc13)=true)). % 18.06/8.27 tff(c_1201, plain, (eventuality(skc10, skc13)=true)). % 18.06/8.27 tff(c_12, plain, (![U_15, V_16]: (ifeq3(event(U_15, V_16), true, eventuality(U_15, V_16), true)=true))). % 18.06/8.27 tff(c_1158, plain, (thing(skc8, skc10)=true)). % 18.06/8.27 tff(c_34, plain, (![U_37, V_38]: (ifeq3(abstraction(U_37, V_38), true, general(U_37, V_38), true)=true))). % 18.06/8.27 tff(c_1083, plain, (ifeq3(relname(skc8, skc10), true, true, true)=true)). % 18.06/8.27 tff(c_1114, plain, (abstraction(skc8, skc10)=true)). % 18.06/8.27 tff(c_1102, plain, (ifeq3(mia_forename(skc8, skc14), true, true, true)=true)). % 18.06/8.27 tff(c_42, plain, (![U_45, V_46]: (ifeq3(mia_forename(U_45, V_46), true, forename(U_45, V_46), true)=true))). % 18.06/8.27 tff(c_1065, plain, (relation(skc8, skc10)=true)). % 18.06/8.27 tff(c_26, plain, (![U_29, V_30]: (ifeq3(proposition(U_29, V_30), true, relation(U_29, V_30), true)=true))). % 18.06/8.27 tff(c_1022, plain, (abstraction(skc8, skc11)=true)). % 18.06/8.27 tff(c_994, plain, (impartial(skc8, skc12)=true)). % 18.06/8.27 tff(c_14, plain, (![U_17, V_18]: (ifeq3(eventuality(U_17, V_18), true, thing(U_17, V_18), true)=true))). % 18.06/8.27 tff(c_960, plain, (living(skc8, skc12)=true)). % 18.06/8.27 tff(c_28, plain, (![U_31, V_32]: (ifeq3(relation(U_31, V_32), true, abstraction(U_31, V_32), true)=true))). % 18.06/8.27 tff(c_930, plain, (entity(skc8, skc15)=true)). % 18.06/8.27 tff(c_30, plain, (![U_33, V_34]: (ifeq3(abstraction(U_33, V_34), true, thing(U_33, V_34), true)=true))). % 18.06/8.27 tff(c_902, plain, (relation(skc8, skc11)=true)). % 18.06/8.27 tff(c_731, plain, (ifeq3(woman(skc8, skc15), true, true, true)=true)). % 18.06/8.27 tff(c_52, plain, (![U_55, V_56]: (ifeq3(entity(U_55, V_56), true, specific(U_55, V_56), true)=true))). % 18.06/8.27 tff(c_870, plain, (relation(skc8, skc14)=true)). % 18.06/8.27 tff(c_833, plain, (organism(skc8, skc12)=true)). % 18.06/8.27 tff(c_16, plain, (![U_19, V_20]: (ifeq3(thing(U_19, V_20), true, singleton(U_19, V_20), true)=true))). % 18.06/8.27 tff(c_805, plain, (human(skc8, skc12)=true)). % 18.06/8.27 tff(c_36, plain, (![U_39, V_40]: (ifeq3(abstraction(U_39, V_40), true, unisex(U_39, V_40), true)=true))). % 18.06/8.27 tff(c_758, plain, (ifeq3(man(skc8, skc12), true, true, true)=true)). % 18.06/8.27 tff(c_780, plain, (animate(skc8, skc12)=true)). % 18.06/8.27 tff(c_18, plain, (![U_21, V_22]: (ifeq3(eventuality(U_21, V_22), true, specific(U_21, V_22), true)=true))). % 18.06/8.27 tff(c_740, plain, (human_person(skc8, skc12)=true)). % 18.06/8.27 tff(c_44, plain, (![U_47, V_48]: (ifeq3(woman(U_47, V_48), true, human_person(U_47, V_48), true)=true))). % 18.06/8.27 tff(c_703, plain, (relname(skc8, skc14)=true)). % 18.06/8.27 tff(c_672, plain, (relname(skc8, skc11)=true)). % 18.06/8.27 tff(c_20, plain, (![U_23, V_24]: (ifeq3(eventuality(U_23, V_24), true, nonexistent(U_23, V_24), true)=true))). % 18.06/8.27 tff(c_638, plain, (impartial(skc8, skc15)=true)). % 18.06/8.27 tff(c_38, plain, (![U_41, V_42]: (ifeq3(forename(U_41, V_42), true, relname(U_41, V_42), true)=true))). % 18.06/8.27 tff(c_608, plain, (organism(skc8, skc15)=true)). % 18.06/8.27 tff(c_46, plain, (![U_49, V_50]: (ifeq3(human_person(U_49, V_50), true, organism(U_49, V_50), true)=true))). % 18.06/8.27 tff(c_50, plain, (![U_53, V_54]: (ifeq3(entity(U_53, V_54), true, thing(U_53, V_54), true)=true))). % 18.06/8.27 tff(c_578, plain, (ifeq3(dance(skc8, skc9), true, true, true)=true)). % 18.06/8.27 tff(c_556, plain, (event(skc8, skc9)=true)). % 18.06/8.27 tff(c_22, plain, (![U_25, V_26]: (ifeq3(eventuality(U_25, V_26), true, unisex(U_25, V_26), true)=true))). % 18.06/8.27 tff(c_543, plain, (ifeq3(desire_want(skc10, skc13), true, true, true)=true)). % 18.06/8.27 tff(c_24, plain, (![U_27, V_28]: (ifeq3(desire_want(U_27, V_28), true, event(U_27, V_28), true)=true))). % 18.06/8.27 tff(c_515, plain, (female(skc8, skc12)=true)). % 18.06/8.27 tff(c_54, plain, (![U_57, V_58]: (ifeq3(entity(U_57, V_58), true, existent(U_57, V_58), true)=true))). % 18.06/8.27 tff(c_480, plain, (human(skc8, skc15)=true)). % 18.06/8.27 tff(c_64, plain, (![U_67, V_68]: (ifeq3(woman(U_67, V_68), true, female(U_67, V_68), true)=true))). % 18.06/8.27 tff(c_459, plain, (animate(skc8, skc15)=true)). % 18.06/8.27 tff(c_444, plain, (ifeq3(vincent_forename(skc8, skc11), true, true, true)=true)). % 18.06/8.27 tff(c_66, plain, (![U_69, V_70]: (ifeq3(vincent_forename(U_69, V_70), true, forename(U_69, V_70), true)=true))). % 18.06/8.28 tff(c_410, plain, (human_person(skc8, skc15)=true)). % 18.06/8.28 tff(c_68, plain, (![U_71, V_72]: (ifeq3(man(U_71, V_72), true, human_person(U_71, V_72), true)=true))). % 18.06/8.28 tff(c_56, plain, (![U_59, V_60]: (ifeq3(organism(U_59, V_60), true, impartial(U_59, V_60), true)=true))). % 18.06/8.28 tff(c_10, plain, (![U_13, V_14]: (ifeq3(dance(U_13, V_14), true, event(U_13, V_14), true)=true))). % 18.06/8.28 tff(c_357, plain, (male(skc8, skc15)=true)). % 18.06/8.28 tff(c_62, plain, (![U_65, V_66]: (ifeq3(human_person(U_65, V_66), true, animate(U_65, V_66), true)=true))). % 18.06/8.28 tff(c_70, plain, (![U_73, V_74]: (ifeq3(man(U_73, V_74), true, male(U_73, V_74), true)=true))). % 18.06/8.28 tff(c_60, plain, (![U_63, V_64]: (ifeq3(human_person(U_63, V_64), true, human(U_63, V_64), true)=true))). % 18.06/8.28 tff(c_58, plain, (![U_61, V_62]: (ifeq3(organism(U_61, V_62), true, living(U_61, V_62), true)=true))). % 18.06/8.28 tff(c_40, plain, (![U_43, V_44]: (ifeq3(relname(U_43, V_44), true, relation(U_43, V_44), true)=true))). % 18.06/8.28 tff(c_48, plain, (![U_51, V_52]: (ifeq3(organism(U_51, V_52), true, entity(U_51, V_52), true)=true))). % 18.06/8.28 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq4(A_1, A_1, B_2, C_3)=B_2))). % 18.06/8.28 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq3(A_4, A_4, B_5, C_6)=B_5))). % 18.06/8.28 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq2(A_7, A_7, B_8, C_9)=B_8))). % 18.06/8.28 tff(c_8, plain, (![A_10, B_11, C_12]: (ifeq(A_10, A_10, B_11, C_12)=B_11))). % 18.06/8.28 tff(c_178, plain, (agent(skc10, skc13, skc12)=true)). % 18.06/8.28 tff(c_176, plain, (agent(skc8, skc9, skc12)=true)). % 18.06/8.28 tff(c_172, plain, (of(skc8, skc14, skc15)=true)). % 18.06/8.28 tff(c_174, plain, (of(skc8, skc11, skc12)=true)). % 18.06/8.28 tff(c_180, plain, (theme(skc8, skc9, skc10)=true)). % 18.06/8.28 tff(c_148, plain, (event(skc10, skc13)=true)). % 18.06/8.28 tff(c_170, plain, (vincent_forename(skc8, skc14)=true)). % 18.06/8.28 tff(c_152, plain, (present(skc10, skc13)=true)). % 18.06/8.28 tff(c_154, plain, (dance(skc10, skc13)=true)). % 18.06/8.28 tff(c_158, plain, (mia_forename(skc8, skc11)=true)). % 18.06/8.28 tff(c_150, plain, (woman(skc8, skc12)=true)). % 18.06/8.28 tff(c_156, plain, (forename(skc8, skc11)=true)). % 18.06/8.28 tff(c_146, plain, (man(skc8, skc15)=true)). % 18.06/8.28 tff(c_168, plain, (forename(skc8, skc14)=true)). % 18.06/8.28 tff(c_160, plain, (proposition(skc8, skc10)=true)). % 18.06/8.28 tff(c_162, plain, (accessible_world(skc8, skc10)=true)). % 18.06/8.28 tff(c_164, plain, (desire_want(skc8, skc9)=true)). % 18.06/8.28 tff(c_166, plain, (present(skc8, skc9)=true)). % 18.06/8.28 tff(c_144, plain, (actual_world(skc8)=true)). % 18.06/8.28 tff(c_196, plain, (b!=a)). % 18.06/8.28 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 18.06/8.28 %------------------------------------------------------------------------------