%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP023-10 : TPTP v9.0.0. Released v7.3.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 : n016.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:56 PM UTC 2025 % Result : Satisfiable 12.70s 5.00s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : NLP023-10 : TPTP v9.0.0. Released v7.3.0. % 0.00/0.07 % 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.07/0.26 % Computer : n016.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.26 % CPULimit : 300 % 0.07/0.26 % WCLimit : 300 % 0.07/0.26 % DateTime : Tue Apr 8 08:09:38 EDT 2025 % 0.07/0.26 % CPUTime : % 12.70/4.99 % 12.70/5.00 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.70/5.00 % 12.70/5.00 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.70/5.00 %$ ifeq3 > ifeq2 > ifeq > theme > of > agent > woman > unisex > tuple > thing > specific > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > mia_forename > living > impartial > human_person > human > general > forename > female > existent > eventuality > event > entity > desire_want > dance > animate > accessible_world > abstraction > #nlpp > actual_world > true > skc9 > skc8 > skc7 > skc6 > skc11 > skc10 > b > a % 12.70/5.00 % 12.70/5.00 %Foreground sorts: % 12.70/5.00 % 12.70/5.00 % 12.70/5.00 %Background operators: % 12.70/5.00 % 12.70/5.00 % 12.70/5.00 %Foreground operators: % 12.70/5.00 tff(agent, type, agent: ($i * $i * $i) > $i). % 12.70/5.00 tff(proposition, type, proposition: ($i * $i) > $i). % 12.70/5.00 tff(specific, type, specific: ($i * $i) > $i). % 12.70/5.00 tff(organism, type, organism: ($i * $i) > $i). % 12.70/5.00 tff(woman, type, woman: ($i * $i) > $i). % 12.70/5.00 tff(impartial, type, impartial: ($i * $i) > $i). % 12.70/5.00 tff(skc7, type, skc7: $i). % 12.70/5.00 tff(skc11, type, skc11: $i). % 12.70/5.00 tff(a, type, a: $i). % 12.70/5.00 tff(skc9, type, skc9: $i). % 12.70/5.00 tff(eventuality, type, eventuality: ($i * $i) > $i). % 12.70/5.00 tff(theme, type, theme: ($i * $i * $i) > $i). % 12.70/5.00 tff(tuple, type, tuple: ($i * $i) > $i). % 12.70/5.00 tff(human_person, type, human_person: ($i * $i) > $i). % 12.70/5.00 tff(skc8, type, skc8: $i). % 12.70/5.00 tff(relname, type, relname: ($i * $i) > $i). % 12.70/5.00 tff(thing, type, thing: ($i * $i) > $i). % 12.70/5.00 tff(unisex, type, unisex: ($i * $i) > $i). % 12.70/5.00 tff(abstraction, type, abstraction: ($i * $i) > $i). % 12.70/5.00 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 12.70/5.00 tff(relation, type, relation: ($i * $i) > $i). % 12.70/5.00 tff(actual_world, type, actual_world: $i > $i). % 12.70/5.00 tff(of, type, of: ($i * $i * $i) > $i). % 12.70/5.00 tff(present, type, present: ($i * $i) > $i). % 12.70/5.00 tff(b, type, b: $i). % 12.70/5.00 tff(desire_want, type, desire_want: ($i * $i) > $i). % 12.70/5.00 tff(animate, type, animate: ($i * $i) > $i). % 12.70/5.00 tff(human, type, human: ($i * $i) > $i). % 12.70/5.00 tff(dance, type, dance: ($i * $i) > $i). % 12.70/5.00 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 12.70/5.00 tff(mia_forename, type, mia_forename: ($i * $i) > $i). % 12.70/5.00 tff(existent, type, existent: ($i * $i) > $i). % 12.70/5.00 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 12.70/5.00 tff(forename, type, forename: ($i * $i) > $i). % 12.70/5.00 tff(female, type, female: ($i * $i) > $i). % 12.70/5.00 tff(true, type, true: $i). % 12.70/5.00 tff(skc6, type, skc6: $i). % 12.70/5.00 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 12.70/5.00 tff(entity, type, entity: ($i * $i) > $i). % 12.70/5.00 tff(skc10, type, skc10: $i). % 12.70/5.00 tff(singleton, type, singleton: ($i * $i) > $i). % 12.70/5.00 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 12.70/5.00 tff(event, type, event: ($i * $i) > $i). % 12.70/5.00 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 12.70/5.00 tff(general, type, general: ($i * $i) > $i). % 12.70/5.00 tff(living, type, living: ($i * $i) > $i). % 12.70/5.00 % 12.70/5.00 %Saturated clause set: % 12.70/5.01 tff(c_3336, plain, (![Y_169, X_168, W_166]: (ifeq3(theme(skc8, Y_169, X_168), true, ifeq3(theme(skc8, skc7, W_166), true, ifeq3(proposition(skc8, X_168), true, ifeq3(proposition(skc8, W_166), true, ifeq3(desire_want(skc8, Y_169), true, X_168, W_166), W_166), W_166), W_166), W_166)=W_166))). % 12.70/5.01 tff(c_3220, plain, (![Y_359, X_361, V_360]: (ifeq3(theme(skc8, Y_359, X_361), true, ifeq3(theme(skc8, V_360, skc8), true, ifeq3(proposition(skc8, X_361), true, ifeq3(desire_want(skc8, Y_359), true, ifeq3(desire_want(skc8, V_360), true, X_361, skc8), skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9938, plain, (![X_679, V_680]: (ifeq3(theme(skc8, skc7, X_679), true, ifeq3(theme(skc8, V_680, skc8), true, ifeq3(proposition(skc8, X_679), true, ifeq3(desire_want(skc8, V_680), true, X_679, skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9936, plain, (![X_679, W_681]: (ifeq3(theme(skc8, skc7, X_679), true, ifeq3(theme(skc8, skc7, W_681), true, ifeq3(proposition(skc8, X_679), true, ifeq3(proposition(skc8, W_681), true, X_679, W_681), W_681), W_681), W_681)=W_681))). % 12.70/5.01 tff(c_3335, plain, (![X_168, V_170, W_166]: (ifeq3(theme(skc8, skc7, X_168), true, ifeq3(theme(skc8, V_170, W_166), true, ifeq3(proposition(skc8, X_168), true, ifeq3(proposition(skc8, W_166), true, ifeq3(desire_want(skc8, V_170), true, X_168, W_166), W_166), W_166), W_166), W_166)=W_166))). % 12.70/5.01 tff(c_9851, plain, (![Y_672, V_673]: (ifeq3(theme(skc8, Y_672, skc8), true, ifeq3(theme(skc8, V_673, skc8), true, ifeq3(desire_want(skc8, Y_672), true, ifeq3(desire_want(skc8, V_673), true, skc8, skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9850, plain, (![Y_672, W_674]: (ifeq3(theme(skc8, Y_672, skc8), true, ifeq3(theme(skc8, skc7, W_674), true, ifeq3(proposition(skc8, W_674), true, ifeq3(desire_want(skc8, Y_672), true, skc8, W_674), W_674), W_674), W_674)=W_674))). % 12.70/5.01 tff(c_3219, plain, (![Y_359, V_360, W_358]: (ifeq3(theme(skc8, Y_359, skc8), true, ifeq3(theme(skc8, V_360, W_358), true, ifeq3(proposition(skc8, W_358), true, ifeq3(desire_want(skc8, Y_359), true, ifeq3(desire_want(skc8, V_360), true, skc8, W_358), W_358), W_358), W_358), W_358)=W_358))). % 12.70/5.01 tff(c_3225, plain, (![Y_359, V_360, W_358]: (ifeq3(theme(skc6, Y_359, skc8), true, ifeq3(theme(skc6, V_360, W_358), true, ifeq3(proposition(skc6, W_358), true, ifeq3(desire_want(skc6, Y_359), true, ifeq3(desire_want(skc6, V_360), true, skc8, W_358), W_358), W_358), W_358), W_358)=W_358))). % 12.70/5.01 tff(c_3797, plain, (![W_163, V_165]: (ifeq3(of(skc8, W_163, skc10), true, ifeq3(of(skc8, V_165, skc10), true, ifeq3(forename(skc8, W_163), true, ifeq3(forename(skc8, V_165), true, W_163, V_165), V_165), V_165), V_165)=V_165))). % 12.70/5.01 tff(c_9735, plain, (![Y_662, V_664]: (ifeq3(theme(skc6, Y_662, skc8), true, ifeq3(theme(skc6, V_664, skc8), true, ifeq3(desire_want(skc6, Y_662), true, ifeq3(desire_want(skc6, V_664), true, skc8, skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_3226, plain, (![Y_359, X_361, V_360]: (ifeq3(theme(skc6, Y_359, X_361), true, ifeq3(theme(skc6, V_360, skc8), true, ifeq3(proposition(skc6, X_361), true, ifeq3(desire_want(skc6, Y_359), true, ifeq3(desire_want(skc6, V_360), true, X_361, skc8), skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_3150, plain, (![W_355, V_357]: (ifeq3(of(skc6, W_355, skc10), true, ifeq3(of(skc6, V_357, skc10), true, ifeq3(forename(skc6, W_355), true, ifeq3(forename(skc6, V_357), true, W_355, V_357), V_357), V_357), V_357)=V_357))). % 12.70/5.01 tff(c_3149, plain, (![W_355, X_356]: (ifeq3(of(skc8, W_355, X_356), true, ifeq3(of(skc8, skc9, X_356), true, ifeq3(entity(skc8, X_356), true, ifeq3(forename(skc8, W_355), true, W_355, skc9), skc9), skc9), skc9)=skc9))). % 12.70/5.01 tff(c_9631, plain, (![X_655]: (ifeq3(of(skc8, skc9, X_655), true, ifeq3(of(skc8, skc9, X_655), true, ifeq3(entity(skc8, X_655), true, skc9, skc9), skc9), skc9)=skc9))). % 12.70/5.01 tff(c_3148, plain, (![X_356, V_357]: (ifeq3(of(skc8, skc9, X_356), true, ifeq3(of(skc8, V_357, X_356), true, ifeq3(entity(skc8, X_356), true, ifeq3(forename(skc8, V_357), true, skc9, V_357), V_357), V_357), V_357)=V_357))). % 12.70/5.01 tff(c_9291, plain, (![X_633, W_635]: (ifeq3(theme(skc6, skc7, X_633), true, ifeq3(theme(skc6, skc7, W_635), true, ifeq3(proposition(skc6, X_633), true, ifeq3(proposition(skc6, W_635), true, X_633, W_635), W_635), W_635), W_635)=W_635))). % 12.70/5.01 tff(c_9293, plain, (![X_633, V_634]: (ifeq3(theme(skc6, skc7, X_633), true, ifeq3(theme(skc6, V_634, skc8), true, ifeq3(proposition(skc6, X_633), true, ifeq3(desire_want(skc6, V_634), true, X_633, skc8), skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9500, plain, (![Y_646, W_648]: (ifeq3(theme(skc6, Y_646, skc8), true, ifeq3(theme(skc6, skc7, W_648), true, ifeq3(proposition(skc6, W_648), true, ifeq3(desire_want(skc6, Y_646), true, skc8, W_648), W_648), W_648), W_648)=W_648))). % 12.70/5.01 tff(c_3224, plain, (![Y_359, X_361, W_358]: (ifeq3(theme(skc6, Y_359, X_361), true, ifeq3(theme(skc6, skc7, W_358), true, ifeq3(proposition(skc6, X_361), true, ifeq3(proposition(skc6, W_358), true, ifeq3(desire_want(skc6, Y_359), true, X_361, W_358), W_358), W_358), W_358), W_358)=W_358))). % 12.70/5.01 tff(c_8987, plain, (![X_618]: (ifeq3(of(skc6, skc9, X_618), true, ifeq3(of(skc6, skc9, X_618), true, ifeq3(entity(skc6, X_618), true, skc9, skc9), skc9), skc9)=skc9))). % 12.70/5.01 tff(c_9384, plain, (![X_641]: (ifeq3(theme(skc8, skc7, X_641), true, ifeq3(proposition(skc8, X_641), true, X_641, skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9356, plain, (![V_638]: (ifeq3(theme(skc8, V_638, skc8), true, ifeq3(desire_want(skc8, V_638), true, skc8, skc8), skc8)=skc8))). % 12.70/5.01 tff(c_9355, plain, (![W_639]: (ifeq3(theme(skc8, skc7, W_639), true, ifeq3(proposition(skc8, W_639), true, skc8, W_639), W_639)=W_639))). % 12.70/5.01 tff(c_4006, plain, (![Y_169, X_168]: (ifeq3(theme(skc8, Y_169, X_168), true, ifeq3(proposition(skc8, X_168), true, ifeq3(desire_want(skc8, Y_169), true, X_168, skc8), skc8), skc8)=skc8))). % 12.70/5.01 tff(c_4005, plain, (![V_170, W_166]: (ifeq3(theme(skc8, V_170, W_166), true, ifeq3(proposition(skc8, W_166), true, ifeq3(desire_want(skc8, V_170), true, skc8, W_166), W_166), W_166)=W_166))). % 12.70/5.01 tff(c_4062, plain, (![W_163]: (ifeq3(of(skc8, W_163, skc10), true, ifeq3(forename(skc8, W_163), true, W_163, skc9), skc9)=skc9))). % 12.70/5.01 tff(c_4061, plain, (![V_165]: (ifeq3(of(skc8, V_165, skc10), true, ifeq3(forename(skc8, V_165), true, skc9, V_165), V_165)=V_165))). % 12.70/5.01 tff(c_3223, plain, (![X_361, V_360, W_358]: (ifeq3(theme(skc6, skc7, X_361), true, ifeq3(theme(skc6, V_360, W_358), true, ifeq3(proposition(skc6, X_361), true, ifeq3(proposition(skc6, W_358), true, ifeq3(desire_want(skc6, V_360), true, X_361, W_358), W_358), W_358), W_358), W_358)=W_358))). % 12.70/5.01 tff(c_9172, plain, (![W_627]: (ifeq3(of(skc6, W_627, skc10), true, ifeq3(forename(skc6, W_627), true, W_627, skc9), skc9)=skc9))). % 12.70/5.01 tff(c_3151, plain, (![V_357]: (ifeq3(of(skc6, V_357, skc10), true, ifeq3(forename(skc6, V_357), true, skc9, V_357), V_357)=V_357))). % 12.70/5.01 tff(c_4001, plain, (![U_154]: (ifeq2(theme(U_154, skc7, skc8), true, ifeq2(accessible_world(U_154, skc8), true, true, true), true)=true))). % 12.70/5.01 tff(c_9125, plain, (![V_626]: (ifeq2(accessible_world(skc8, V_626), true, theme(V_626, skc7, skc8), true)=true))). % 12.70/5.02 tff(c_3154, plain, (![W_355, X_356]: (ifeq3(of(skc6, W_355, X_356), true, ifeq3(of(skc6, skc9, X_356), true, ifeq3(entity(skc6, X_356), true, ifeq3(forename(skc6, W_355), true, W_355, skc9), skc9), skc9), skc9)=skc9))). % 12.70/5.02 tff(c_9082, plain, (![V_624]: (ifeq2(accessible_world(skc8, V_624), true, agent(V_624, skc7, skc10), true)=true))). % 12.70/5.02 tff(c_4086, plain, (![U_150]: (ifeq2(agent(U_150, skc7, skc10), true, ifeq2(accessible_world(U_150, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_4057, plain, (![U_158]: (ifeq2(of(U_158, skc9, skc10), true, ifeq2(accessible_world(U_158, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_8993, plain, (![V_620]: (ifeq2(accessible_world(skc8, V_620), true, of(V_620, skc9, skc10), true)=true))). % 12.70/5.02 tff(c_3153, plain, (![X_356, V_357]: (ifeq3(of(skc6, skc9, X_356), true, ifeq3(of(skc6, V_357, X_356), true, ifeq3(entity(skc6, X_356), true, ifeq3(forename(skc6, V_357), true, skc9, V_357), V_357), V_357), V_357)=V_357))). % 12.70/5.02 tff(c_8808, plain, (![X_609]: (ifeq3(theme(skc6, skc7, X_609), true, ifeq3(proposition(skc6, X_609), true, X_609, skc8), skc8)=skc8))). % 12.70/5.02 tff(c_8809, plain, (![Y_608]: (ifeq3(theme(skc6, Y_608, skc8), true, ifeq3(desire_want(skc6, Y_608), true, skc8, skc8), skc8)=skc8))). % 12.70/5.02 tff(c_8616, plain, (![W_598]: (ifeq3(theme(skc6, skc7, W_598), true, ifeq3(proposition(skc6, W_598), true, skc8, W_598), W_598)=W_598))). % 12.70/5.02 tff(c_2867, plain, (![U_78]: (ifeq2(accessible_world(U_78, skc8), true, ifeq2(singleton(U_78, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_3959, plain, (![U_78]: (ifeq2(accessible_world(U_78, skc8), true, ifeq2(singleton(U_78, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2887, plain, (![U_337]: (ifeq2(accessible_world(U_337, skc8), true, ifeq2(nonhuman(U_337, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_2782, plain, (![U_75]: (ifeq2(accessible_world(U_75, skc8), true, ifeq2(thing(U_75, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_2680, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc8), true, ifeq2(unisex(U_328, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_3222, plain, (![Y_359, X_361]: (ifeq3(theme(skc6, Y_359, X_361), true, ifeq3(proposition(skc6, X_361), true, ifeq3(desire_want(skc6, Y_359), true, X_361, skc8), skc8), skc8)=skc8))). % 12.70/5.02 tff(c_3907, plain, (![U_81]: (ifeq2(accessible_world(U_81, skc8), true, ifeq2(specific(U_81, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2836, plain, (![U_108]: (ifeq2(accessible_world(U_108, skc8), true, ifeq2(general(U_108, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_3820, plain, (![U_75]: (ifeq2(accessible_world(U_75, skc8), true, ifeq2(thing(U_75, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2352, plain, (![U_78]: (ifeq2(accessible_world(U_78, skc8), true, ifeq2(singleton(U_78, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_3876, plain, (![U_132]: (ifeq2(accessible_world(U_132, skc8), true, ifeq2(existent(U_132, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_3397, plain, (![U_78]: (ifeq2(accessible_world(U_78, skc8), true, ifeq2(singleton(U_78, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_2252, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc6), true, ifeq2(singleton(U_306, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_2246, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc6), true, ifeq2(singleton(U_306, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_3235, plain, (![U_75]: (ifeq2(accessible_world(U_75, skc8), true, ifeq2(thing(U_75, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_3221, plain, (![V_360, W_358]: (ifeq3(theme(skc6, V_360, W_358), true, ifeq3(proposition(skc6, W_358), true, ifeq3(desire_want(skc6, V_360), true, skc8, W_358), W_358), W_358)=W_358))). % 12.70/5.02 tff(c_3272, plain, (![U_108]: (ifeq2(accessible_world(U_108, skc8), true, ifeq2(general(U_108, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_2404, plain, (![U_316]: (ifeq2(accessible_world(U_316, skc8), true, ifeq2(specific(U_316, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_2622, plain, (![U_325]: (ifeq2(accessible_world(U_325, skc8), true, ifeq2(abstraction(U_325, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_3163, plain, (![U_105]: (ifeq2(accessible_world(U_105, skc8), true, ifeq2(nonhuman(U_105, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_3782, plain, (![U_129]: (ifeq2(accessible_world(U_129, skc8), true, ifeq2(entity(U_129, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_3751, plain, (![U_138]: (ifeq2(accessible_world(U_138, skc8), true, ifeq2(living(U_138, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_3359, plain, (![U_87]: (ifeq2(accessible_world(U_87, skc8), true, ifeq2(unisex(U_87, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_2186, plain, (![U_84]: (ifeq2(accessible_world(U_84, skc8), true, ifeq2(nonexistent(U_84, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_2217, plain, (![U_75]: (ifeq2(accessible_world(U_75, skc8), true, ifeq2(thing(U_75, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_2927, plain, (![U_340]: (ifeq2(theme(U_340, skc7, skc8), true, ifeq2(accessible_world(U_340, skc6), true, true, true), true)=true))). % 12.70/5.02 tff(c_2686, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc8), true, ifeq2(unisex(U_328, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_3710, plain, (![U_135]: (ifeq2(accessible_world(U_135, skc8), true, ifeq2(impartial(U_135, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_1510, plain, (![U_261]: (ifeq2(accessible_world(U_261, skc6), true, ifeq2(thing(U_261, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_1640, plain, (![U_75]: (ifeq2(accessible_world(U_75, skc6), true, ifeq2(thing(U_75, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2410, plain, (![U_316]: (ifeq2(accessible_world(U_316, skc6), true, ifeq2(specific(U_316, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2506, plain, (![U_319]: (ifeq2(accessible_world(U_319, skc6), true, ifeq2(general(U_319, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_1572, plain, (![U_264]: (ifeq2(accessible_world(U_264, skc6), true, ifeq2(existent(U_264, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2692, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc6), true, ifeq2(unisex(U_328, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_2893, plain, (![U_337]: (ifeq2(accessible_world(U_337, skc6), true, ifeq2(nonhuman(U_337, skc9), true, true, true), true)=true))). % 12.70/5.02 tff(c_3051, plain, (![U_350]: (ifeq2(agent(U_350, skc11, skc10), true, ifeq2(accessible_world(U_350, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_2270, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc6), true, ifeq2(singleton(U_306, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_2258, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc6), true, ifeq2(singleton(U_306, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_3086, plain, (![U_102]: (ifeq2(accessible_world(U_102, skc8), true, ifeq2(abstraction(U_102, skc8), true, true, true), true)=true))). % 12.70/5.02 tff(c_3682, plain, (![U_144]: (ifeq2(accessible_world(U_144, skc8), true, ifeq2(animate(U_144, skc10), true, true, true), true)=true))). % 12.70/5.02 tff(c_2077, plain, (![U_72]: (ifeq2(accessible_world(U_72, skc8), true, ifeq2(eventuality(U_72, skc7), true, true, true), true)=true))). % 12.70/5.02 tff(c_3651, plain, (![U_141]: (ifeq2(accessible_world(U_141, skc8), true, ifeq2(human(U_141, skc10), true, true, true), true)=true))). % 12.96/5.02 tff(c_3604, plain, (![U_126]: (ifeq2(accessible_world(U_126, skc8), true, ifeq2(organism(U_126, skc10), true, true, true), true)=true))). % 12.96/5.02 tff(c_8070, plain, (![V_568]: (ifeq2(accessible_world(skc6, V_568), true, agent(V_568, skc7, skc10), true)=true))). % 12.96/5.02 tff(c_2560, plain, (![U_99]: (ifeq2(accessible_world(U_99, skc8), true, ifeq2(relation(U_99, skc9), true, true, true), true)=true))). % 12.96/5.02 tff(c_1516, plain, (![U_261]: (ifeq2(accessible_world(U_261, skc6), true, ifeq2(thing(U_261, skc7), true, true, true), true)=true))). % 12.96/5.02 tff(c_2698, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc6), true, ifeq2(unisex(U_328, skc7), true, true, true), true)=true))). % 12.96/5.02 tff(c_1439, plain, (![U_258]: (ifeq2(accessible_world(U_258, skc6), true, ifeq2(nonexistent(U_258, skc7), true, true, true), true)=true))). % 12.96/5.02 tff(c_1762, plain, (![U_276]: (ifeq2(accessible_world(U_276, skc6), true, ifeq2(entity(U_276, skc10), true, true, true), true)=true))). % 12.96/5.02 tff(c_1528, plain, (![U_261]: (ifeq2(accessible_world(U_261, skc6), true, ifeq2(thing(U_261, skc8), true, true, true), true)=true))). % 12.96/5.02 tff(c_2899, plain, (![U_337]: (ifeq2(accessible_world(U_337, skc6), true, ifeq2(nonhuman(U_337, skc8), true, true, true), true)=true))). % 12.96/5.02 tff(c_2512, plain, (![U_319]: (ifeq2(accessible_world(U_319, skc6), true, ifeq2(general(U_319, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_2062, plain, (![U_297]: (ifeq2(accessible_world(U_297, skc6), true, ifeq2(living(U_297, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_3000, plain, (![U_346]: (ifeq2(of(U_346, skc9, skc10), true, ifeq2(accessible_world(U_346, skc6), true, true, true), true)=true))). % 12.96/5.03 tff(c_2710, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc6), true, ifeq2(unisex(U_328, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_2416, plain, (![U_316]: (ifeq2(accessible_world(U_316, skc6), true, ifeq2(specific(U_316, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_1615, plain, (![U_267]: (ifeq2(accessible_world(U_267, skc6), true, ifeq2(impartial(U_267, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_2634, plain, (![U_325]: (ifeq2(accessible_world(U_325, skc6), true, ifeq2(abstraction(U_325, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_2264, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc8), true, ifeq2(singleton(U_306, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_2484, plain, (![U_114]: (ifeq2(accessible_world(U_114, skc8), true, ifeq2(relname(U_114, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_2026, plain, (![U_69]: (ifeq2(accessible_world(U_69, skc8), true, ifeq2(event(U_69, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_7740, plain, (![V_549]: (ifeq2(accessible_world(skc6, V_549), true, of(V_549, skc9, skc10), true)=true))). % 12.96/5.03 tff(c_3573, plain, (![U_147]: (ifeq2(accessible_world(U_147, skc8), true, ifeq2(female(U_147, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_3536, plain, (![U_123]: (ifeq2(accessible_world(U_123, skc8), true, ifeq2(human_person(U_123, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_3025, plain, (![U_99]: (ifeq2(accessible_world(U_99, skc8), true, ifeq2(relation(U_99, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_2422, plain, (![U_316]: (ifeq2(accessible_world(U_316, skc8), true, ifeq2(specific(U_316, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_1724, plain, (![U_273]: (ifeq2(accessible_world(U_273, skc6), true, ifeq2(animate(U_273, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_1394, plain, (![U_255]: (ifeq2(accessible_world(U_255, skc6), true, ifeq2(eventuality(U_255, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_1445, plain, (![U_258]: (ifeq2(accessible_world(U_258, skc8), true, ifeq2(nonexistent(U_258, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_7564, plain, (![V_540]: (ifeq2(accessible_world(skc6, V_540), true, theme(V_540, skc7, skc8), true)=true))). % 12.96/5.03 tff(c_2545, plain, (![U_322]: (ifeq2(accessible_world(U_322, skc6), true, ifeq2(organism(U_322, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_2704, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc8), true, ifeq2(unisex(U_328, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_1522, plain, (![U_261]: (ifeq2(accessible_world(U_261, skc8), true, ifeq2(thing(U_261, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_1354, plain, (![U_252]: (ifeq2(accessible_world(U_252, skc6), true, ifeq2(human(U_252, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_1958, plain, (![U_290]: (ifeq2(accessible_world(U_290, skc6), true, ifeq2(relation(U_290, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_2628, plain, (![U_325]: (ifeq2(accessible_world(U_325, skc6), true, ifeq2(abstraction(U_325, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_7423, plain, (![V_532]: (ifeq2(accessible_world(skc8, V_532), true, present(V_532, skc7), true)=true))). % 12.96/5.03 tff(c_3057, plain, (![U_350]: (ifeq2(agent(U_350, skc7, skc10), true, ifeq2(accessible_world(U_350, skc6), true, true, true), true)=true))). % 12.96/5.03 tff(c_2453, plain, (![U_111]: (ifeq2(accessible_world(U_111, skc8), true, ifeq2(forename(U_111, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_1937, plain, (![U_90]: (ifeq2(present(U_90, skc7), true, ifeq2(accessible_world(U_90, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_3444, plain, (![U_117]: (ifeq2(accessible_world(U_117, skc8), true, ifeq2(mia_forename(U_117, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_3328, plain, (![U_93]: (ifeq2(accessible_world(U_93, skc8), true, ifeq2(desire_want(U_93, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_3495, plain, (![U_120]: (ifeq2(accessible_world(U_120, skc8), true, ifeq2(woman(U_120, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_2980, plain, (![U_96]: (ifeq2(accessible_world(U_96, skc8), true, ifeq2(proposition(U_96, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_1896, plain, (![U_286]: (ifeq2(accessible_world(U_286, skc6), true, ifeq2(relname(U_286, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_7232, plain, (![V_522]: (ifeq2(accessible_world(skc8, V_522), true, agent(V_522, skc11, skc10), true)=true))). % 12.96/5.03 tff(c_1400, plain, (![U_255]: (ifeq2(accessible_world(U_255, skc8), true, ifeq2(eventuality(U_255, skc11), true, true, true), true)=true))). % 12.96/5.03 tff(c_2318, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc6), true, ifeq2(human_person(U_309, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_1808, plain, (![U_279]: (ifeq2(accessible_world(U_279, skc6), true, ifeq2(event(U_279, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_1952, plain, (![U_290]: (ifeq2(accessible_world(U_290, skc6), true, ifeq2(relation(U_290, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_1669, plain, (![U_270]: (ifeq2(accessible_world(U_270, skc6), true, ifeq2(female(U_270, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_7127, plain, (ifeq2(singleton(skc6, skc11), true, true, true)=true)). % 12.96/5.03 tff(c_7051, plain, (![W_515]: (ifeq2(singleton(skc6, W_515), true, singleton(skc8, W_515), true)=true))). % 12.96/5.03 tff(c_7008, plain, (![W_513]: (ifeq2(forename(skc6, W_513), true, forename(skc8, W_513), true)=true))). % 12.96/5.03 tff(c_6949, plain, (![W_511]: (ifeq2(relation(skc6, W_511), true, relation(skc8, W_511), true)=true))). % 12.96/5.03 tff(c_6906, plain, (![W_509]: (ifeq2(entity(skc6, W_509), true, entity(skc8, W_509), true)=true))). % 12.96/5.03 tff(c_2824, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc6), true, ifeq2(woman(U_334, skc10), true, true, true), true)=true))). % 12.96/5.03 tff(c_2374, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc6), true, ifeq2(forename(U_312, skc9), true, true, true), true)=true))). % 12.96/5.03 tff(c_6833, plain, (![W_505]: (ifeq2(female(skc6, W_505), true, female(skc8, W_505), true)=true))). % 12.96/5.03 tff(c_2171, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc6), true, ifeq2(desire_want(U_303, skc7), true, true, true), true)=true))). % 12.96/5.03 tff(c_6773, plain, (![W_502]: (ifeq2(organism(skc6, W_502), true, organism(skc8, W_502), true)=true))). % 12.96/5.03 tff(c_6749, plain, (ifeq2(thing(skc6, skc11), true, true, true)=true)). % 12.96/5.03 tff(c_6673, plain, (![W_500]: (ifeq2(thing(skc6, W_500), true, thing(skc8, W_500), true)=true))). % 12.96/5.03 tff(c_6630, plain, (![W_498]: (ifeq2(animate(skc6, W_498), true, animate(skc8, W_498), true)=true))). % 12.96/5.03 tff(c_6570, plain, (![W_496]: (ifeq2(general(skc6, W_496), true, general(skc8, W_496), true)=true))). % 12.96/5.03 tff(c_6528, plain, (![W_494]: (ifeq2(mia_forename(skc6, W_494), true, mia_forename(skc8, W_494), true)=true))). % 12.96/5.03 tff(c_1847, plain, (![U_282]: (ifeq2(present(U_282, skc11), true, ifeq2(accessible_world(U_282, skc8), true, true, true), true)=true))). % 12.96/5.03 tff(c_6474, plain, (![V_491]: (ifeq2(accessible_world(skc8, V_491), true, present(V_491, skc11), true)=true))). % 12.96/5.03 tff(c_6430, plain, (![W_489]: (ifeq2(impartial(skc6, W_489), true, impartial(skc8, W_489), true)=true))). % 12.96/5.03 tff(c_6412, plain, (ifeq2(specific(skc6, skc11), true, true, true)=true)). % 12.96/5.03 tff(c_6361, plain, (![W_487]: (ifeq2(specific(skc6, W_487), true, specific(skc8, W_487), true)=true))). % 12.96/5.03 tff(c_6318, plain, (![W_485]: (ifeq2(woman(skc6, W_485), true, woman(skc8, W_485), true)=true))). % 12.96/5.03 tff(c_6259, plain, (![W_483]: (ifeq2(abstraction(skc6, W_483), true, abstraction(skc8, W_483), true)=true))). % 12.96/5.03 tff(c_2839, plain, (ifeq(tuple(specific(skc8, skc9), true), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_2659, plain, (ifeq(tuple(true, female(skc8, skc9)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_3910, plain, (ifeq(tuple(true, general(skc8, skc10)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_2738, plain, (ifeq(tuple(true, human(skc8, skc9)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_3879, plain, (ifeq(tuple(nonexistent(skc8, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_2189, plain, (ifeq(tuple(true, existent(skc8, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_3275, plain, (ifeq(tuple(specific(skc8, skc8), true), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_6188, plain, (![W_481]: (ifeq2(desire_want(skc6, W_481), true, desire_want(skc8, W_481), true)=true))). % 12.96/5.03 tff(c_2139, plain, (ifeq(tuple(true, female(skc8, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_2296, plain, (ifeq(tuple(true, general(skc8, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_3166, plain, (ifeq(tuple(true, human(skc8, skc8)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_3362, plain, (ifeq(tuple(true, female(skc8, skc8)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_1488, plain, (ifeq(tuple(true, general(skc6, skc10)), tuple(true, true), a, b)=b)). % 12.96/5.03 tff(c_6151, plain, (ifeq2(nonexistent(skc6, skc11), true, true, true)=true)). % 12.96/5.03 tff(c_6114, plain, (![W_479]: (ifeq2(nonexistent(skc6, W_479), true, nonexistent(skc8, W_479), true)=true))). % 12.96/5.03 tff(c_1553, plain, (ifeq(tuple(nonexistent(skc6, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1691, plain, (ifeq(tuple(true, human(skc6, skc9)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1595, plain, (ifeq(tuple(specific(skc6, skc9), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1736, plain, (ifeq(tuple(true, female(skc6, skc9)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_3654, plain, (ifeq(tuple(nonhuman(skc8, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1235, plain, (ifeq(tuple(true, female(skc6, skc8)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_6054, plain, (![W_477]: (ifeq2(dance(skc6, W_477), true, dance(skc8, W_477), true)=true))). % 12.96/5.04 tff(c_3965, plain, (![V_79]: (ifeq2(accessible_world(skc8, V_79), true, singleton(V_79, skc10), true)=true))). % 12.96/5.04 tff(c_2873, plain, (![V_79]: (ifeq2(accessible_world(skc8, V_79), true, singleton(V_79, skc9), true)=true))). % 12.96/5.04 tff(c_2716, plain, (![V_329]: (ifeq2(accessible_world(skc8, V_329), true, unisex(V_329, skc9), true)=true))). % 12.96/5.04 tff(c_3835, plain, (![V_76]: (ifeq2(accessible_world(skc8, V_76), true, thing(V_76, skc10), true)=true))). % 12.96/5.04 tff(c_1181, plain, (ifeq(tuple(true, human(skc6, skc8)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2845, plain, (![V_109]: (ifeq2(accessible_world(skc8, V_109), true, general(V_109, skc9), true)=true))). % 12.96/5.04 tff(c_5931, plain, (![W_470]: (ifeq2(living(skc6, W_470), true, living(skc8, W_470), true)=true))). % 12.96/5.04 tff(c_3403, plain, (![V_79]: (ifeq2(accessible_world(skc8, V_79), true, singleton(V_79, skc8), true)=true))). % 12.96/5.04 tff(c_3885, plain, (![V_133]: (ifeq2(accessible_world(skc8, V_133), true, existent(V_133, skc10), true)=true))). % 12.96/5.04 tff(c_2358, plain, (![V_79]: (ifeq2(accessible_world(skc8, V_79), true, singleton(V_79, skc7), true)=true))). % 12.96/5.04 tff(c_2797, plain, (![V_76]: (ifeq2(accessible_world(skc8, V_76), true, thing(V_76, skc9), true)=true))). % 12.96/5.04 tff(c_3919, plain, (![V_82]: (ifeq2(accessible_world(skc8, V_82), true, specific(V_82, skc10), true)=true))). % 12.96/5.04 tff(c_1266, plain, (ifeq(tuple(true, existent(skc6, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2905, plain, (![V_338]: (ifeq2(accessible_world(skc8, V_338), true, nonhuman(V_338, skc9), true)=true))). % 12.96/5.04 tff(c_5786, plain, (![V_462]: (ifeq2(accessible_world(skc6, V_462), true, present(V_462, skc7), true)=true))). % 12.96/5.04 tff(c_2277, plain, (![V_307]: (ifeq2(accessible_world(skc6, V_307), true, singleton(V_307, skc9), true)=true))). % 12.96/5.04 tff(c_2276, plain, (![V_307]: (ifeq2(accessible_world(skc6, V_307), true, singleton(V_307, skc10), true)=true))). % 12.96/5.04 tff(c_2428, plain, (![V_317]: (ifeq2(accessible_world(skc8, V_317), true, specific(V_317, skc7), true)=true))). % 12.96/5.04 tff(c_3798, plain, (![V_130]: (ifeq2(accessible_world(skc8, V_130), true, entity(V_130, skc10), true)=true))). % 12.96/5.04 tff(c_3250, plain, (![V_76]: (ifeq2(accessible_world(skc8, V_76), true, thing(V_76, skc8), true)=true))). % 12.96/5.04 tff(c_1308, plain, (ifeq(tuple(true, general(skc6, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2640, plain, (![V_326]: (ifeq2(accessible_world(skc8, V_326), true, abstraction(V_326, skc9), true)=true))). % 12.96/5.04 tff(c_5641, plain, (![W_454]: (ifeq2(human(skc6, W_454), true, human(skc8, W_454), true)=true))). % 12.96/5.04 tff(c_2232, plain, (![V_76]: (ifeq2(accessible_world(skc8, V_76), true, thing(V_76, skc7), true)=true))). % 12.96/5.04 tff(c_3371, plain, (![V_88]: (ifeq2(accessible_world(skc8, V_88), true, unisex(V_88, skc8), true)=true))). % 12.96/5.04 tff(c_3281, plain, (![V_109]: (ifeq2(accessible_world(skc8, V_109), true, general(V_109, skc8), true)=true))). % 12.96/5.04 tff(c_5573, plain, (ifeq2(dance(skc6, skc11), true, true, true)=true)). % 12.96/5.04 tff(c_3172, plain, (![V_106]: (ifeq2(accessible_world(skc8, V_106), true, nonhuman(V_106, skc8), true)=true))). % 12.96/5.04 tff(c_2717, plain, (![V_329]: (ifeq2(accessible_world(skc8, V_329), true, unisex(V_329, skc7), true)=true))). % 12.96/5.04 tff(c_3716, plain, (![V_136]: (ifeq2(accessible_world(skc8, V_136), true, impartial(V_136, skc10), true)=true))). % 12.96/5.04 tff(c_2770, plain, (![U_331]: (ifeq2(accessible_world(U_331, skc8), true, ifeq2(dance(U_331, skc11), true, true, true), true)=true))). % 12.96/5.04 tff(c_3757, plain, (![V_139]: (ifeq2(accessible_world(skc8, V_139), true, living(V_139, skc10), true)=true))). % 12.96/5.04 tff(c_2195, plain, (![V_85]: (ifeq2(accessible_world(skc8, V_85), true, nonexistent(V_85, skc7), true)=true))). % 12.96/5.04 tff(c_2906, plain, (![V_338]: (ifeq2(accessible_world(skc6, V_338), true, nonhuman(V_338, skc9), true)=true))). % 12.96/5.04 tff(c_2278, plain, (![V_307]: (ifeq2(accessible_world(skc6, V_307), true, singleton(V_307, skc7), true)=true))). % 12.96/5.04 tff(c_2280, plain, (![V_307]: (ifeq2(accessible_world(skc6, V_307), true, singleton(V_307, skc8), true)=true))). % 12.96/5.04 tff(c_1332, plain, (ifeq(tuple(true, female(skc6, skc7)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_5409, plain, (ifeq2(eventuality(skc6, skc11), true, true, true)=true)). % 12.96/5.04 tff(c_5372, plain, (![W_440]: (ifeq2(eventuality(skc6, W_440), true, eventuality(skc8, W_440), true)=true))). % 12.96/5.04 tff(c_2429, plain, (![V_317]: (ifeq2(accessible_world(skc6, V_317), true, specific(V_317, skc10), true)=true))). % 12.96/5.04 tff(c_2718, plain, (![V_329]: (ifeq2(accessible_world(skc6, V_329), true, unisex(V_329, skc9), true)=true))). % 12.96/5.04 tff(c_1655, plain, (![V_76]: (ifeq2(accessible_world(skc6, V_76), true, thing(V_76, skc10), true)=true))). % 12.96/5.04 tff(c_2518, plain, (![V_320]: (ifeq2(accessible_world(skc6, V_320), true, general(V_320, skc9), true)=true))). % 12.96/5.04 tff(c_1534, plain, (![V_262]: (ifeq2(accessible_world(skc6, V_262), true, thing(V_262, skc9), true)=true))). % 12.96/5.04 tff(c_1314, plain, (ifeq(tuple(specific(skc6, skc8), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1578, plain, (![V_265]: (ifeq2(accessible_world(skc6, V_265), true, existent(V_265, skc10), true)=true))). % 12.96/5.04 tff(c_3619, plain, (![V_127]: (ifeq2(accessible_world(skc8, V_127), true, organism(V_127, skc10), true)=true))). % 12.96/5.04 tff(c_3688, plain, (![V_145]: (ifeq2(accessible_world(skc8, V_145), true, animate(V_145, skc10), true)=true))). % 12.96/5.04 tff(c_1838, plain, (![U_282]: (ifeq2(present(U_282, skc7), true, ifeq2(accessible_world(U_282, skc6), true, true, true), true)=true))). % 12.96/5.04 tff(c_2572, plain, (![V_100]: (ifeq2(accessible_world(skc8, V_100), true, relation(V_100, skc9), true)=true))). % 12.96/5.04 tff(c_3660, plain, (![V_142]: (ifeq2(accessible_world(skc8, V_142), true, human(V_142, skc10), true)=true))). % 12.96/5.04 tff(c_3104, plain, (![V_103]: (ifeq2(accessible_world(skc8, V_103), true, abstraction(V_103, skc8), true)=true))). % 12.96/5.04 tff(c_2095, plain, (![V_73]: (ifeq2(accessible_world(skc8, V_73), true, eventuality(V_73, skc7), true)=true))). % 12.96/5.04 tff(c_2430, plain, (![V_317]: (ifeq2(accessible_world(skc6, V_317), true, specific(V_317, skc7), true)=true))). % 12.96/5.04 tff(c_3576, plain, (ifeq(tuple(unisex(skc8, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2721, plain, (![V_329]: (ifeq2(accessible_world(skc6, V_329), true, unisex(V_329, skc8), true)=true))). % 12.96/5.04 tff(c_5040, plain, (![W_423]: (ifeq2(nonhuman(skc6, W_423), true, nonhuman(skc8, W_423), true)=true))). % 12.96/5.04 tff(c_1451, plain, (![V_259]: (ifeq2(accessible_world(skc6, V_259), true, nonexistent(V_259, skc7), true)=true))). % 12.96/5.04 tff(c_1537, plain, (![V_262]: (ifeq2(accessible_world(skc6, V_262), true, thing(V_262, skc8), true)=true))). % 12.96/5.04 tff(c_1535, plain, (![V_262]: (ifeq2(accessible_world(skc6, V_262), true, thing(V_262, skc7), true)=true))). % 12.96/5.04 tff(c_1621, plain, (![V_268]: (ifeq2(accessible_world(skc6, V_268), true, impartial(V_268, skc10), true)=true))). % 12.96/5.04 tff(c_2642, plain, (![V_326]: (ifeq2(accessible_world(skc6, V_326), true, abstraction(V_326, skc9), true)=true))). % 12.96/5.04 tff(c_1229, plain, (ifeq(tuple(true, female(skc8, skc11)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2719, plain, (![V_329]: (ifeq2(accessible_world(skc6, V_329), true, unisex(V_329, skc7), true)=true))). % 12.96/5.04 tff(c_4879, plain, (![W_415]: (ifeq2(existent(skc6, W_415), true, existent(skc8, W_415), true)=true))). % 12.96/5.04 tff(c_2519, plain, (![V_320]: (ifeq2(accessible_world(skc6, V_320), true, general(V_320, skc8), true)=true))). % 12.96/5.04 tff(c_2279, plain, (![V_307]: (ifeq2(accessible_world(skc8, V_307), true, singleton(V_307, skc11), true)=true))). % 12.96/5.04 tff(c_2068, plain, (![V_298]: (ifeq2(accessible_world(skc6, V_298), true, living(V_298, skc10), true)=true))). % 12.96/5.04 tff(c_2907, plain, (![V_338]: (ifeq2(accessible_world(skc6, V_338), true, nonhuman(V_338, skc8), true)=true))). % 12.96/5.04 tff(c_1768, plain, (![V_277]: (ifeq2(accessible_world(skc6, V_277), true, entity(V_277, skc10), true)=true))). % 12.96/5.04 tff(c_1184, plain, (ifeq(tuple(nonhuman(skc6, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_3582, plain, (![V_148]: (ifeq2(accessible_world(skc8, V_148), true, female(V_148, skc10), true)=true))). % 12.96/5.04 tff(c_4730, plain, (![W_407]: (ifeq2(human_person(skc6, W_407), true, human_person(skc8, W_407), true)=true))). % 12.96/5.04 tff(c_2039, plain, (![V_70]: (ifeq2(accessible_world(skc8, V_70), true, event(V_70, skc7), true)=true))). % 12.96/5.04 tff(c_2493, plain, (![V_115]: (ifeq2(accessible_world(skc8, V_115), true, relname(V_115, skc9), true)=true))). % 12.96/5.04 tff(c_3037, plain, (![V_100]: (ifeq2(accessible_world(skc8, V_100), true, relation(V_100, skc8), true)=true))). % 12.96/5.04 tff(c_3551, plain, (![V_124]: (ifeq2(accessible_world(skc8, V_124), true, human_person(V_124, skc10), true)=true))). % 12.96/5.04 tff(c_2431, plain, (![V_317]: (ifeq2(accessible_world(skc8, V_317), true, specific(V_317, skc11), true)=true))). % 12.96/5.04 tff(c_1269, plain, (ifeq(tuple(true, existent(skc8, skc11)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_1730, plain, (![V_274]: (ifeq2(accessible_world(skc6, V_274), true, animate(V_274, skc10), true)=true))). % 12.96/5.04 tff(c_1536, plain, (![V_262]: (ifeq2(accessible_world(skc8, V_262), true, thing(V_262, skc11), true)=true))). % 12.96/5.04 tff(c_1965, plain, (![V_291]: (ifeq2(accessible_world(skc6, V_291), true, relation(V_291, skc9), true)=true))). % 12.96/5.04 tff(c_2011, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc6), true, ifeq2(mia_forename(U_294, skc9), true, true, true), true)=true))). % 12.96/5.04 tff(c_2641, plain, (![V_326]: (ifeq2(accessible_world(skc6, V_326), true, abstraction(V_326, skc8), true)=true))). % 12.96/5.04 tff(c_1360, plain, (![V_253]: (ifeq2(accessible_world(skc6, V_253), true, human(V_253, skc10), true)=true))). % 12.96/5.04 tff(c_1452, plain, (![V_259]: (ifeq2(accessible_world(skc8, V_259), true, nonexistent(V_259, skc11), true)=true))). % 12.96/5.04 tff(c_2720, plain, (![V_329]: (ifeq2(accessible_world(skc8, V_329), true, unisex(V_329, skc11), true)=true))). % 12.96/5.04 tff(c_1406, plain, (![V_256]: (ifeq2(accessible_world(skc6, V_256), true, eventuality(V_256, skc7), true)=true))). % 12.96/5.04 tff(c_1311, plain, (ifeq(tuple(true, general(skc8, skc11)), tuple(true, true), a, b)=b)). % 12.96/5.04 tff(c_2551, plain, (![V_323]: (ifeq2(accessible_world(skc6, V_323), true, organism(V_323, skc10), true)=true))). % 12.96/5.04 tff(c_4438, plain, (![W_390]: (ifeq2(event(skc6, W_390), true, event(skc8, W_390), true)=true))). % 12.96/5.04 tff(c_3505, plain, (![V_121]: (ifeq2(accessible_world(skc8, V_121), true, woman(V_121, skc10), true)=true))). % 12.96/5.04 tff(c_2987, plain, (![V_97]: (ifeq2(accessible_world(skc8, V_97), true, proposition(V_97, skc8), true)=true))). % 12.96/5.04 tff(c_2463, plain, (![V_112]: (ifeq2(accessible_world(skc8, V_112), true, forename(V_112, skc9), true)=true))). % 12.96/5.04 tff(c_3337, plain, (![V_94]: (ifeq2(accessible_world(skc8, V_94), true, desire_want(V_94, skc7), true)=true))). % 12.96/5.04 tff(c_3451, plain, (![V_118]: (ifeq2(accessible_world(skc8, V_118), true, mia_forename(V_118, skc9), true)=true))). % 12.96/5.05 tff(c_1232, plain, (ifeq(tuple(unisex(skc6, skc10), true), tuple(true, true), a, b)=b)). % 12.96/5.05 tff(c_4336, plain, (ifeq2(unisex(skc6, skc11), true, true, true)=true)). % 12.96/5.05 tff(c_4274, plain, (![W_383]: (ifeq2(unisex(skc6, W_383), true, unisex(skc8, W_383), true)=true))). % 12.96/5.05 tff(c_1902, plain, (![V_287]: (ifeq2(accessible_world(skc6, V_287), true, relname(V_287, skc9), true)=true))). % 12.96/5.05 tff(c_1964, plain, (![V_291]: (ifeq2(accessible_world(skc6, V_291), true, relation(V_291, skc8), true)=true))). % 12.96/5.05 tff(c_1675, plain, (![V_271]: (ifeq2(accessible_world(skc6, V_271), true, female(V_271, skc10), true)=true))). % 12.96/5.05 tff(c_4194, plain, (ifeq2(event(skc6, skc11), true, true, true)=true)). % 12.96/5.05 tff(c_1407, plain, (![V_256]: (ifeq2(accessible_world(skc8, V_256), true, eventuality(V_256, skc11), true)=true))). % 12.96/5.05 tff(c_4142, plain, (![W_377]: (ifeq2(proposition(skc6, W_377), true, proposition(skc8, W_377), true)=true))). % 12.96/5.05 tff(c_2324, plain, (![V_310]: (ifeq2(accessible_world(skc6, V_310), true, human_person(V_310, skc10), true)=true))). % 12.96/5.05 tff(c_4035, plain, (![W_374]: (ifeq2(relname(skc6, W_374), true, relname(skc8, W_374), true)=true))). % 12.96/5.05 tff(c_3726, plain, (ifeq2(agent(skc6, skc11, skc10), true, true, true)=true)). % 12.96/5.05 tff(c_4068, plain, (agent(skc8, skc7, skc10)=true)). % 12.96/5.05 tff(c_4012, plain, (of(skc8, skc9, skc10)=true)). % 12.96/5.05 tff(c_3977, plain, (theme(skc8, skc7, skc8)=true)). % 12.96/5.05 tff(c_3832, plain, (ifeq2(abstraction(skc8, skc10), true, true, true)=true)). % 12.96/5.05 tff(c_3944, plain, (singleton(skc8, skc10)=true)). % 12.96/5.05 tff(c_1817, plain, (![U_279]: (ifeq2(accessible_world(U_279, skc8), true, ifeq2(event(U_279, skc11), true, true, true), true)=true))). % 12.96/5.05 tff(c_3913, plain, (ifeq2(eventuality(skc8, skc10), true, true, true)=true)). % 12.96/5.05 tff(c_3892, plain, (specific(skc8, skc10)=true)). % 12.96/5.05 tff(c_3861, plain, (existent(skc8, skc10)=true)). % 12.96/5.05 tff(c_3851, plain, (ifeq2(accessible_world(skc8, skc6), true, true, true)=true)). % 12.96/5.05 tff(c_2130, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc6), true, ifeq2(proposition(U_300, skc8), true, true, true), true)=true))). % 12.96/5.05 tff(c_3805, plain, (thing(skc8, skc10)=true)). % 12.96/5.05 tff(c_3764, plain, (entity(skc8, skc10)=true)). % 12.96/5.05 tff(c_3736, plain, (living(skc8, skc10)=true)). % 12.96/5.05 tff(c_3063, plain, (![W_351, X_352]: (ifeq2(agent(skc6, W_351, X_352), true, agent(skc8, W_351, X_352), true)=true))). % 12.96/5.05 tff(c_3695, plain, (impartial(skc8, skc10)=true)). % 12.96/5.05 tff(c_3667, plain, (animate(skc8, skc10)=true)). % 12.96/5.05 tff(c_3636, plain, (human(skc8, skc10)=true)). % 12.96/5.05 tff(c_3006, plain, (![W_347, X_348]: (ifeq2(of(skc6, W_347, X_348), true, of(skc8, W_347, X_348), true)=true))). % 12.96/5.05 tff(c_3589, plain, (organism(skc8, skc10)=true)). % 12.96/5.05 tff(c_3558, plain, (female(skc8, skc10)=true)). % 12.96/5.05 tff(c_3521, plain, (human_person(skc8, skc10)=true)). % 12.96/5.05 tff(c_2933, plain, (![W_341, X_342]: (ifeq2(theme(skc6, W_341, X_342), true, theme(skc8, W_341, X_342), true)=true))). % 12.96/5.05 tff(c_3477, plain, (woman(skc8, skc10)=true)). % 12.96/5.05 tff(c_2827, plain, (![V_335]: (ifeq2(accessible_world(skc6, V_335), true, woman(V_335, skc10), true)=true))). % 12.96/5.05 tff(c_3238, plain, (ifeq2(entity(skc8, skc8), true, true, true)=true)). % 12.96/5.05 tff(c_3424, plain, (mia_forename(skc8, skc9)=true)). % 12.96/5.05 tff(c_2014, plain, (![V_295]: (ifeq2(accessible_world(skc6, V_295), true, mia_forename(V_295, skc9), true)=true))). % 12.96/5.05 tff(c_3382, plain, (singleton(skc8, skc8)=true)). % 12.96/5.05 tff(c_3241, plain, (ifeq2(eventuality(skc8, skc8), true, true, true)=true)). % 12.96/5.05 tff(c_3344, plain, (unisex(skc8, skc8)=true)). % 12.96/5.05 tff(c_3302, plain, (desire_want(skc8, skc7)=true)). % 12.96/5.05 tff(c_2177, plain, (![V_304]: (ifeq2(accessible_world(skc6, V_304), true, desire_want(V_304, skc7), true)=true))). % 12.96/5.05 tff(c_3257, plain, (general(skc8, skc8)=true)). % 12.96/5.05 tff(c_3179, plain, (thing(skc8, skc8)=true)). % 12.96/5.05 tff(c_128, plain, (![V_170, U_167, Y_169, W_166, X_168]: (ifeq3(theme(U_167, Y_169, X_168), true, ifeq3(theme(U_167, V_170, W_166), true, ifeq3(proposition(U_167, X_168), true, ifeq3(proposition(U_167, W_166), true, ifeq3(desire_want(U_167, Y_169), true, ifeq3(desire_want(U_167, V_170), true, X_168, W_166), W_166), W_166), W_166), W_166), W_166)=W_166))). % 12.96/5.05 tff(c_3111, plain, (nonhuman(skc8, skc8)=true)). % 12.96/5.05 tff(c_126, plain, (![U_162, W_163, X_164, V_165]: (ifeq3(of(U_162, W_163, X_164), true, ifeq3(of(U_162, V_165, X_164), true, ifeq3(entity(U_162, X_164), true, ifeq3(forename(U_162, W_163), true, ifeq3(forename(U_162, V_165), true, W_163, V_165), V_165), V_165), V_165), V_165)=V_165))). % 12.96/5.05 tff(c_3071, plain, (abstraction(skc8, skc8)=true)). % 12.96/5.05 tff(c_3034, plain, (ifeq2(relname(skc8, skc8), true, true, true)=true)). % 12.96/5.05 tff(c_120, plain, (![U_150, W_151, X_152, V_153]: (ifeq2(agent(U_150, W_151, X_152), true, ifeq2(accessible_world(U_150, V_153), true, agent(V_153, W_151, X_152), true), true)=true))). % 12.96/5.05 tff(c_3010, plain, (relation(skc8, skc8)=true)). % 12.96/5.05 tff(c_124, plain, (![U_158, W_159, X_160, V_161]: (ifeq2(of(U_158, W_159, X_160), true, ifeq2(accessible_world(U_158, V_161), true, of(V_161, W_159, X_160), true), true)=true))). % 12.96/5.05 tff(c_2962, plain, (proposition(skc8, skc8)=true)). % 12.96/5.05 tff(c_2133, plain, (![V_301]: (ifeq2(accessible_world(skc6, V_301), true, proposition(V_301, skc8), true)=true))). % 12.96/5.05 tff(c_2773, plain, (![V_332]: (ifeq2(accessible_world(skc8, V_332), true, dance(V_332, skc11), true)=true))). % 12.96/5.05 tff(c_122, plain, (![U_154, W_155, X_156, V_157]: (ifeq2(theme(U_154, W_155, X_156), true, ifeq2(accessible_world(U_154, V_157), true, theme(V_157, W_155, X_156), true), true)=true))). % 12.96/5.05 tff(c_2662, plain, (ifeq2(eventuality(skc8, skc9), true, true, true)=true)). % 12.96/5.05 tff(c_2785, plain, (ifeq2(entity(skc8, skc9), true, true, true)=true)). % 12.96/5.05 tff(c_90, plain, (![U_105, V_106, W_107]: (ifeq2(accessible_world(U_105, V_106), true, ifeq2(nonhuman(U_105, W_107), true, nonhuman(V_106, W_107), true), true)=true))). % 12.96/5.05 tff(c_2852, plain, (singleton(skc8, skc9)=true)). % 12.96/5.05 tff(c_2808, plain, (general(skc8, skc9)=true)). % 12.96/5.05 tff(c_100, plain, (![U_120, V_121, W_122]: (ifeq2(accessible_world(U_120, V_121), true, ifeq2(woman(U_120, W_122), true, woman(V_121, W_122), true), true)=true))). % 12.96/5.05 tff(c_2750, plain, (thing(skc8, skc9)=true)). % 12.96/5.05 tff(c_64, plain, (![U_66, V_67, W_68]: (ifeq2(accessible_world(U_66, V_67), true, ifeq2(dance(U_66, W_68), true, dance(V_67, W_68), true), true)=true))). % 12.96/5.05 tff(c_2726, plain, (nonhuman(skc8, skc9)=true)). % 12.96/5.05 tff(c_78, plain, (![U_87, V_88, W_89]: (ifeq2(accessible_world(U_87, V_88), true, ifeq2(unisex(U_87, W_89), true, unisex(V_88, W_89), true), true)=true))). % 12.96/5.05 tff(c_2647, plain, (unisex(skc8, skc9)=true)). % 12.96/5.05 tff(c_88, plain, (![U_102, V_103, W_104]: (ifeq2(accessible_world(U_102, V_103), true, ifeq2(abstraction(U_102, W_104), true, abstraction(V_103, W_104), true), true)=true))). % 12.96/5.05 tff(c_2583, plain, (abstraction(skc8, skc9)=true)). % 12.96/5.05 tff(c_2563, plain, (ifeq2(proposition(skc8, skc9), true, true, true)=true)). % 12.96/5.05 tff(c_2532, plain, (relation(skc8, skc9)=true)). % 12.96/5.05 tff(c_104, plain, (![U_126, V_127, W_128]: (ifeq2(accessible_world(U_126, V_127), true, ifeq2(organism(U_126, W_128), true, organism(V_127, W_128), true), true)=true))). % 12.96/5.05 tff(c_92, plain, (![U_108, V_109, W_110]: (ifeq2(accessible_world(U_108, V_109), true, ifeq2(general(U_108, W_110), true, general(V_109, W_110), true), true)=true))). % 12.96/5.05 tff(c_2469, plain, (relname(skc8, skc9)=true)). % 12.96/5.05 tff(c_2435, plain, (forename(skc8, skc9)=true)). % 12.96/5.05 tff(c_74, plain, (![U_81, V_82, W_83]: (ifeq2(accessible_world(U_81, V_82), true, ifeq2(specific(U_81, W_83), true, specific(V_82, W_83), true), true)=true))). % 12.96/5.05 tff(c_2377, plain, (![V_313]: (ifeq2(accessible_world(skc6, V_313), true, forename(V_313, skc9), true)=true))). % 12.96/5.05 tff(c_94, plain, (![U_111, V_112, W_113]: (ifeq2(accessible_world(U_111, V_112), true, ifeq2(forename(U_111, W_113), true, forename(V_112, W_113), true), true)=true))). % 12.96/5.05 tff(c_2337, plain, (singleton(skc8, skc7)=true)). % 12.96/5.05 tff(c_2302, plain, (ifeq2(entity(skc8, skc7), true, true, true)=true)). % 12.96/5.05 tff(c_2229, plain, (ifeq2(abstraction(skc8, skc7), true, true, true)=true)). % 12.96/5.05 tff(c_102, plain, (![U_123, V_124, W_125]: (ifeq2(accessible_world(U_123, V_124), true, ifeq2(human_person(U_123, W_125), true, human_person(V_124, W_125), true), true)=true))). % 12.96/5.05 tff(c_2284, plain, (specific(skc8, skc7)=true)). % 12.96/5.05 tff(c_72, plain, (![U_78, V_79, W_80]: (ifeq2(accessible_world(U_78, V_79), true, ifeq2(singleton(U_78, W_80), true, singleton(V_79, W_80), true), true)=true))). % 12.96/5.05 tff(c_2202, plain, (thing(skc8, skc7)=true)). % 12.96/5.05 tff(c_2154, plain, (nonexistent(skc8, skc7)=true)). % 12.96/5.05 tff(c_82, plain, (![U_93, V_94, W_95]: (ifeq2(accessible_world(U_93, V_94), true, ifeq2(desire_want(U_93, W_95), true, desire_want(V_94, W_95), true), true)=true))). % 12.96/5.05 tff(c_2110, plain, (unisex(skc8, skc7)=true)). % 12.96/5.05 tff(c_84, plain, (![U_96, V_97, W_98]: (ifeq2(accessible_world(U_96, V_97), true, ifeq2(proposition(U_96, W_98), true, proposition(V_97, W_98), true), true)=true))). % 12.96/5.05 tff(c_2032, plain, (ifeq2(dance(skc8, skc7), true, true, true)=true)). % 12.96/5.05 tff(c_2045, plain, (eventuality(skc8, skc7)=true)). % 12.96/5.05 tff(c_112, plain, (![U_138, V_139, W_140]: (ifeq2(accessible_world(U_138, V_139), true, ifeq2(living(U_138, W_140), true, living(V_139, W_140), true), true)=true))). % 12.96/5.05 tff(c_1991, plain, (event(skc8, skc7)=true)). % 12.96/5.05 tff(c_98, plain, (![U_117, V_118, W_119]: (ifeq2(accessible_world(U_117, V_118), true, ifeq2(mia_forename(U_117, W_119), true, mia_forename(V_118, W_119), true), true)=true))). % 12.96/5.05 tff(c_1978, plain, (ifeq2(accessible_world(skc6, skc6), true, true, true)=true)). % 12.96/5.05 tff(c_1820, plain, (![V_280]: (ifeq2(accessible_world(skc6, V_280), true, event(V_280, skc7), true)=true))). % 12.96/5.05 tff(c_1913, plain, (ifeq2(present(skc6, skc11), true, true, true)=true)). % 12.96/5.05 tff(c_86, plain, (![U_99, V_100, W_101]: (ifeq2(accessible_world(U_99, V_100), true, ifeq2(relation(U_99, W_101), true, relation(V_100, W_101), true), true)=true))). % 12.96/5.05 tff(c_1919, plain, (present(skc8, skc7)=true)). % 12.96/5.05 tff(c_1850, plain, (![W_283]: (ifeq2(present(skc6, W_283), true, present(skc8, W_283), true)=true))). % 12.96/5.05 tff(c_96, plain, (![U_114, V_115, W_116]: (ifeq2(accessible_world(U_114, V_115), true, ifeq2(relname(U_114, W_116), true, relname(V_115, W_116), true), true)=true))). % 12.96/5.05 tff(c_1879, plain, (ifeq2(accessible_world(skc8, skc8), true, true, true)=true)). % 12.96/5.05 tff(c_1821, plain, (![V_280]: (ifeq2(accessible_world(skc8, V_280), true, event(V_280, skc11), true)=true))). % 12.96/5.05 tff(c_1854, plain, (singleton(skc6, skc10)=true)). % 12.96/5.05 tff(c_80, plain, (![U_90, W_91, V_92]: (ifeq2(present(U_90, W_91), true, ifeq2(accessible_world(U_90, V_92), true, present(V_92, W_91), true), true)=true))). % 12.96/5.05 tff(c_1491, plain, (ifeq2(eventuality(skc6, skc10), true, true, true)=true)). % 12.96/5.05 tff(c_66, plain, (![U_69, V_70, W_71]: (ifeq2(accessible_world(U_69, V_70), true, ifeq2(event(U_69, W_71), true, event(V_70, W_71), true), true)=true))). % 12.96/5.05 tff(c_1781, plain, (singleton(skc6, skc9)=true)). % 12.96/5.05 tff(c_1458, plain, (ifeq2(entity(skc6, skc9), true, true, true)=true)). % 12.96/5.05 tff(c_1739, plain, (ifeq2(eventuality(skc6, skc9), true, true, true)=true)). % 12.96/5.05 tff(c_106, plain, (![U_129, V_130, W_131]: (ifeq2(accessible_world(U_129, V_130), true, ifeq2(entity(U_129, W_131), true, entity(V_130, W_131), true), true)=true))). % 12.96/5.05 tff(c_1652, plain, (ifeq2(abstraction(skc6, skc10), true, true, true)=true)). % 12.96/5.05 tff(c_1707, plain, (unisex(skc6, skc9)=true)). % 12.96/5.05 tff(c_116, plain, (![U_144, V_145, W_146]: (ifeq2(accessible_world(U_144, V_145), true, ifeq2(animate(U_144, W_146), true, animate(V_145, W_146), true), true)=true))). % 12.96/5.05 tff(c_1147, plain, (ifeq2(entity(skc6, skc8), true, true, true)=true)). % 12.96/5.06 tff(c_1679, plain, (nonhuman(skc6, skc9)=true)). % 12.96/5.06 tff(c_118, plain, (![U_147, V_148, W_149]: (ifeq2(accessible_world(U_147, V_148), true, ifeq2(female(U_147, W_149), true, female(V_148, W_149), true), true)=true))). % 12.96/5.06 tff(c_1625, plain, (thing(skc6, skc10)=true)). % 12.96/5.06 tff(c_110, plain, (![U_135, V_136, W_137]: (ifeq2(accessible_world(U_135, V_136), true, ifeq2(impartial(U_135, W_137), true, impartial(V_136, W_137), true), true)=true))). % 12.96/5.06 tff(c_1583, plain, (general(skc6, skc9)=true)). % 12.96/5.06 tff(c_108, plain, (![U_132, V_133, W_134]: (ifeq2(accessible_world(U_132, V_133), true, ifeq2(existent(U_132, W_134), true, existent(V_133, W_134), true), true)=true))). % 12.96/5.06 tff(c_1541, plain, (existent(skc6, skc10)=true)). % 12.96/5.06 tff(c_70, plain, (![U_75, V_76, W_77]: (ifeq2(accessible_world(U_75, V_76), true, ifeq2(thing(U_75, W_77), true, thing(V_76, W_77), true), true)=true))). % 12.96/5.06 tff(c_1476, plain, (specific(skc6, skc10)=true)). % 12.96/5.06 tff(c_1426, plain, (thing(skc6, skc9)=true)). % 12.96/5.06 tff(c_76, plain, (![U_84, V_85, W_86]: (ifeq2(accessible_world(U_84, V_85), true, ifeq2(nonexistent(U_84, W_86), true, nonexistent(V_85, W_86), true), true)=true))). % 12.96/5.06 tff(c_1377, plain, (singleton(skc6, skc7)=true)). % 12.96/5.06 tff(c_68, plain, (![U_72, V_73, W_74]: (ifeq2(accessible_world(U_72, V_73), true, ifeq2(eventuality(U_72, W_74), true, eventuality(V_73, W_74), true), true)=true))). % 12.96/5.06 tff(c_1294, plain, (ifeq2(entity(skc6, skc7), true, true, true)=true)). % 12.96/5.06 tff(c_1338, plain, (ifeq2(abstraction(skc6, skc7), true, true, true)=true)). % 12.96/5.06 tff(c_983, plain, (ifeq2(eventuality(skc6, skc8), true, true, true)=true)). % 12.96/5.06 tff(c_114, plain, (![U_141, V_142, W_143]: (ifeq2(accessible_world(U_141, V_142), true, ifeq2(human(U_141, W_143), true, human(V_142, W_143), true), true)=true))). % 12.96/5.06 tff(c_1320, plain, (unisex(skc6, skc7)=true)). % 12.96/5.06 tff(c_162, plain, (![U_173, V_174]: (ifeq(tuple(specific(U_173, V_174), general(U_173, V_174)), tuple(true, true), a, b)=b))). % 12.96/5.06 tff(c_1279, plain, (specific(skc6, skc7)=true)). % 12.96/5.06 tff(c_1110, plain, (ifeq2(abstraction(skc8, skc11), true, true, true)=true)). % 12.96/5.06 tff(c_166, plain, (![U_177, V_178]: (ifeq(tuple(nonexistent(U_177, V_178), existent(U_177, V_178)), tuple(true, true), a, b)=b))). % 12.96/5.06 tff(c_1215, plain, (thing(skc6, skc7)=true)). % 12.96/5.06 tff(c_160, plain, (![U_171, V_172]: (ifeq(tuple(unisex(U_171, V_172), female(U_171, V_172)), tuple(true, true), a, b)=b))). % 12.96/5.06 tff(c_1144, plain, (ifeq2(entity(skc8, skc11), true, true, true)=true)). % 12.96/5.06 tff(c_1190, plain, (singleton(skc8, skc11)=true)). % 12.96/5.06 tff(c_164, plain, (![U_175, V_176]: (ifeq(tuple(nonhuman(U_175, V_176), human(U_175, V_176)), tuple(true, true), a, b)=b))). % 12.96/5.06 tff(c_1156, plain, (nonexistent(skc6, skc7)=true)). % 12.96/5.06 tff(c_48, plain, (![U_50, V_51]: (ifeq2(entity(U_50, V_51), true, thing(U_50, V_51), true)=true))). % 12.96/5.06 tff(c_1119, plain, (nonexistent(skc8, skc11)=true)). % 12.96/5.06 tff(c_1082, plain, (unisex(skc8, skc11)=true)). % 12.96/5.06 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 12.96/5.06 tff(c_1045, plain, (thing(skc8, skc11)=true)). % 12.96/5.06 tff(c_52, plain, (![U_54, V_55]: (ifeq2(entity(U_54, V_55), true, existent(U_54, V_55), true)=true))). % 12.96/5.06 tff(c_1024, plain, (female(skc6, skc10)=true)). % 12.96/5.06 tff(c_62, plain, (![U_64, V_65]: (ifeq2(woman(U_64, V_65), true, female(U_64, V_65), true)=true))). % 12.96/5.06 tff(c_990, plain, (specific(skc8, skc11)=true)). % 12.96/5.06 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 12.96/5.06 tff(c_947, plain, (eventuality(skc6, skc7)=true)). % 12.96/5.06 tff(c_920, plain, (eventuality(skc8, skc11)=true)). % 12.96/5.06 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 12.96/5.06 tff(c_886, plain, (singleton(skc6, skc8)=true)). % 12.96/5.06 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 12.96/5.06 tff(c_855, plain, (thing(skc6, skc8)=true)). % 12.96/5.06 tff(c_836, plain, (ifeq2(dance(skc6, skc7), true, true, true)=true)). % 12.96/5.06 tff(c_8, plain, (![U_10, V_11]: (ifeq2(dance(U_10, V_11), true, event(U_10, V_11), true)=true))). % 12.96/5.06 tff(c_812, plain, (nonhuman(skc6, skc8)=true)). % 12.96/5.06 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 12.96/5.06 tff(c_784, plain, (general(skc6, skc8)=true)). % 12.96/5.06 tff(c_666, plain, (ifeq2(proposition(skc6, skc9), true, true, true)=true)). % 12.96/5.06 tff(c_743, plain, (unisex(skc6, skc8)=true)). % 12.96/5.06 tff(c_30, plain, (![U_32, V_33]: (ifeq2(abstraction(U_32, V_33), true, nonhuman(U_32, V_33), true)=true))). % 12.96/5.06 tff(c_693, plain, (ifeq2(relname(skc6, skc8), true, true, true)=true)). % 12.96/5.06 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 12.96/5.06 tff(c_702, plain, (abstraction(skc6, skc8)=true)). % 12.96/5.06 tff(c_675, plain, (relation(skc6, skc8)=true)). % 12.96/5.06 tff(c_24, plain, (![U_26, V_27]: (ifeq2(proposition(U_26, V_27), true, relation(U_26, V_27), true)=true))). % 12.96/5.06 tff(c_632, plain, (abstraction(skc6, skc9)=true)). % 12.96/5.06 tff(c_50, plain, (![U_52, V_53]: (ifeq2(entity(U_52, V_53), true, specific(U_52, V_53), true)=true))). % 12.96/5.06 tff(c_26, plain, (![U_28, V_29]: (ifeq2(relation(U_28, V_29), true, abstraction(U_28, V_29), true)=true))). % 12.96/5.06 tff(c_581, plain, (ifeq2(desire_want(skc8, skc11), true, true, true)=true)). % 12.96/5.06 tff(c_587, plain, (event(skc6, skc7)=true)). % 12.96/5.06 tff(c_22, plain, (![U_24, V_25]: (ifeq2(desire_want(U_24, V_25), true, event(U_24, V_25), true)=true))). % 12.96/5.06 tff(c_28, plain, (![U_30, V_31]: (ifeq2(abstraction(U_30, V_31), true, thing(U_30, V_31), true)=true))). % 12.96/5.06 tff(c_539, plain, (animate(skc6, skc10)=true)). % 12.96/5.06 tff(c_32, plain, (![U_34, V_35]: (ifeq2(abstraction(U_34, V_35), true, general(U_34, V_35), true)=true))). % 12.96/5.06 tff(c_518, plain, (relation(skc6, skc9)=true)). % 12.96/5.06 tff(c_60, plain, (![U_62, V_63]: (ifeq2(human_person(U_62, V_63), true, animate(U_62, V_63), true)=true))). % 12.96/5.06 tff(c_484, plain, (relname(skc6, skc9)=true)). % 12.96/5.06 tff(c_36, plain, (![U_38, V_39]: (ifeq2(forename(U_38, V_39), true, relname(U_38, V_39), true)=true))). % 12.96/5.06 tff(c_453, plain, (impartial(skc6, skc10)=true)). % 12.96/5.06 tff(c_432, plain, (human(skc6, skc10)=true)). % 12.96/5.06 tff(c_58, plain, (![U_60, V_61]: (ifeq2(human_person(U_60, V_61), true, human(U_60, V_61), true)=true))). % 12.96/5.06 tff(c_401, plain, (living(skc6, skc10)=true)). % 12.96/5.06 tff(c_54, plain, (![U_56, V_57]: (ifeq2(organism(U_56, V_57), true, impartial(U_56, V_57), true)=true))). % 12.96/5.06 tff(c_56, plain, (![U_58, V_59]: (ifeq2(organism(U_58, V_59), true, living(U_58, V_59), true)=true))). % 12.96/5.06 tff(c_360, plain, (entity(skc6, skc10)=true)). % 12.96/5.06 tff(c_34, plain, (![U_36, V_37]: (ifeq2(abstraction(U_36, V_37), true, unisex(U_36, V_37), true)=true))). % 12.96/5.06 tff(c_329, plain, (organism(skc6, skc10)=true)). % 12.96/5.06 tff(c_44, plain, (![U_46, V_47]: (ifeq2(human_person(U_46, V_47), true, organism(U_46, V_47), true)=true))). % 12.96/5.06 tff(c_38, plain, (![U_40, V_41]: (ifeq2(relname(U_40, V_41), true, relation(U_40, V_41), true)=true))). % 12.96/5.06 tff(c_46, plain, (![U_48, V_49]: (ifeq2(organism(U_48, V_49), true, entity(U_48, V_49), true)=true))). % 12.96/5.06 tff(c_284, plain, (human_person(skc6, skc10)=true)). % 12.96/5.06 tff(c_42, plain, (![U_44, V_45]: (ifeq2(woman(U_44, V_45), true, human_person(U_44, V_45), true)=true))). % 12.96/5.06 tff(c_40, plain, (![U_42, V_43]: (ifeq2(mia_forename(U_42, V_43), true, forename(U_42, V_43), true)=true))). % 12.96/5.06 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 12.96/5.06 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 12.96/5.06 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 12.96/5.06 tff(c_156, plain, (agent(skc8, skc11, skc10)=true)). % 12.96/5.06 tff(c_158, plain, (theme(skc6, skc7, skc8)=true)). % 12.96/5.06 tff(c_154, plain, (agent(skc6, skc7, skc10)=true)). % 12.96/5.06 tff(c_152, plain, (of(skc6, skc9, skc10)=true)). % 12.96/5.06 tff(c_148, plain, (desire_want(skc6, skc7)=true)). % 12.96/5.06 tff(c_150, plain, (present(skc6, skc7)=true)). % 12.96/5.06 tff(c_146, plain, (accessible_world(skc6, skc8)=true)). % 12.96/5.06 tff(c_144, plain, (proposition(skc6, skc8)=true)). % 12.96/5.06 tff(c_142, plain, (mia_forename(skc6, skc9)=true)). % 12.96/5.06 tff(c_140, plain, (forename(skc6, skc9)=true)). % 12.96/5.06 tff(c_132, plain, (event(skc8, skc11)=true)). % 12.96/5.06 tff(c_134, plain, (woman(skc6, skc10)=true)). % 12.96/5.06 tff(c_136, plain, (present(skc8, skc11)=true)). % 12.96/5.06 tff(c_138, plain, (dance(skc8, skc11)=true)). % 12.96/5.06 tff(c_130, plain, (actual_world(skc6)=true)). % 12.96/5.06 tff(c_168, plain, (b!=a)). % 12.96/5.06 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.96/5.06 %------------------------------------------------------------------------------