%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP220-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 : n020.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:48:38 PM UTC 2025 % Result : Satisfiable 14.36s 6.06s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP220-10 : TPTP v9.0.0. Released v7.3.0. % 0.06/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.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 09:26:34 EDT 2025 % 0.13/0.33 % CPUTime : % 14.36/6.06 % 14.36/6.06 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.36/6.07 % 14.36/6.07 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.36/6.07 %$ ifeq3 > ifeq2 > ifeq > theme > of > agent > vincent_forename > unisex > tuple > think_believe_consider > thing > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > #nlpp > skf1 > actual_world > true > skc9 > skc8 > skc7 > skc6 > skc5 > b > a % 14.36/6.07 % 14.36/6.07 %Foreground sorts: % 14.36/6.07 % 14.36/6.07 % 14.36/6.07 %Background operators: % 14.36/6.07 % 14.36/6.07 % 14.36/6.07 %Foreground operators: % 14.36/6.07 tff(agent, type, agent: ($i * $i * $i) > $i). % 14.36/6.07 tff(proposition, type, proposition: ($i * $i) > $i). % 14.36/6.07 tff(specific, type, specific: ($i * $i) > $i). % 14.36/6.07 tff(organism, type, organism: ($i * $i) > $i). % 14.36/6.07 tff(impartial, type, impartial: ($i * $i) > $i). % 14.36/6.07 tff(skc7, type, skc7: $i). % 14.36/6.07 tff(a, type, a: $i). % 14.36/6.07 tff(smoke, type, smoke: ($i * $i) > $i). % 14.36/6.07 tff(skc9, type, skc9: $i). % 14.36/6.07 tff(eventuality, type, eventuality: ($i * $i) > $i). % 14.36/6.07 tff(theme, type, theme: ($i * $i * $i) > $i). % 14.36/6.07 tff(tuple, type, tuple: ($i * $i) > $i). % 14.36/6.07 tff(human_person, type, human_person: ($i * $i) > $i). % 14.36/6.07 tff(skf1, type, skf1: $i > $i). % 14.36/6.07 tff(skc8, type, skc8: $i). % 14.36/6.07 tff(relname, type, relname: ($i * $i) > $i). % 14.36/6.07 tff(thing, type, thing: ($i * $i) > $i). % 14.36/6.07 tff(unisex, type, unisex: ($i * $i) > $i). % 14.36/6.07 tff(abstraction, type, abstraction: ($i * $i) > $i). % 14.36/6.07 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 14.36/6.07 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 14.36/6.07 tff(relation, type, relation: ($i * $i) > $i). % 14.36/6.07 tff(actual_world, type, actual_world: $i > $i). % 14.36/6.07 tff(of, type, of: ($i * $i * $i) > $i). % 14.36/6.07 tff(present, type, present: ($i * $i) > $i). % 14.36/6.07 tff(b, type, b: $i). % 14.36/6.07 tff(animate, type, animate: ($i * $i) > $i). % 14.36/6.07 tff(human, type, human: ($i * $i) > $i). % 14.36/6.07 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 14.36/6.07 tff(existent, type, existent: ($i * $i) > $i). % 14.36/6.07 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 14.36/6.07 tff(skc5, type, skc5: $i). % 14.36/6.07 tff(forename, type, forename: ($i * $i) > $i). % 14.36/6.07 tff(true, type, true: $i). % 14.36/6.07 tff(skc6, type, skc6: $i). % 14.36/6.07 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 14.36/6.07 tff(male, type, male: ($i * $i) > $i). % 14.36/6.07 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 14.36/6.07 tff(entity, type, entity: ($i * $i) > $i). % 14.36/6.07 tff(singleton, type, singleton: ($i * $i) > $i). % 14.36/6.07 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 14.36/6.07 tff(event, type, event: ($i * $i) > $i). % 14.36/6.07 tff(man, type, man: ($i * $i) > $i). % 14.36/6.07 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 14.36/6.07 tff(general, type, general: ($i * $i) > $i). % 14.36/6.07 tff(living, type, living: ($i * $i) > $i). % 14.36/6.07 % 14.36/6.07 %Saturated clause set: % 14.36/6.08 tff(c_11553, plain, (![W_841, V_842]: (ifeq3(theme(skc6, skf1(skc9), W_841), true, ifeq3(theme(skc6, skf1(skc9), V_842), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_841), true, ifeq3(proposition(skc6, V_842), true, V_842, W_841), W_841), W_841), W_841), W_841), W_841)=W_841))). % 14.36/6.08 tff(c_3415, plain, (![W_164, X_167, V_169]: (ifeq3(theme(skc6, skf1(skc9), W_164), true, ifeq3(theme(skc6, X_167, V_169), true, ifeq3(agent(skc6, X_167, skc9), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.08 tff(c_11324, plain, (![X_825, V_826]: (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(theme(skc6, X_825, V_826), true, ifeq3(agent(skc6, X_825, skc9), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, X_825), true, ifeq3(proposition(skc6, V_826), true, V_826, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_11639, plain, (![V_846]: (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(theme(skc6, skf1(skc9), V_846), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, V_846), true, V_846, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_11325, plain, (![Y_824, V_826]: (ifeq3(theme(skc6, Y_824, skc6), true, ifeq3(theme(skc6, skf1(skc9), V_826), true, ifeq3(agent(skc6, Y_824, skc9), true, ifeq3(think_believe_consider(skc6, Y_824), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, V_826), true, V_826, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_11445, plain, (![W_833, X_834]: (ifeq3(theme(skc6, skf1(skc9), W_833), true, ifeq3(theme(skc6, X_834, skc6), true, ifeq3(agent(skc6, X_834, skc9), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, X_834), true, ifeq3(proposition(skc6, W_833), true, skc6, W_833), W_833), W_833), W_833), W_833), W_833)=W_833))). % 14.36/6.08 tff(c_3416, plain, (![Y_168, W_164, V_169]: (ifeq3(theme(skc6, Y_168, W_164), true, ifeq3(theme(skc6, skf1(skc9), V_169), true, ifeq3(agent(skc6, Y_168, skc9), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.08 tff(c_11507, plain, (![W_838]: (ifeq3(theme(skc6, skf1(skc9), W_838), true, ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_838), true, skc6, W_838), W_838), W_838), W_838), W_838)=W_838))). % 14.36/6.08 tff(c_11446, plain, (![Y_832, W_833]: (ifeq3(theme(skc6, Y_832, W_833), true, ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(agent(skc6, Y_832, skc9), true, ifeq3(think_believe_consider(skc6, Y_832), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_833), true, skc6, W_833), W_833), W_833), W_833), W_833), W_833)=W_833))). % 14.36/6.08 tff(c_11364, plain, (![Y_828]: (ifeq3(theme(skc6, Y_828, skc6), true, ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(agent(skc6, Y_828, skc9), true, ifeq3(think_believe_consider(skc6, Y_828), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, skc6, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_3490, plain, (![Y_168, W_164, X_167, Z_166]: (ifeq3(theme(skc6, Y_168, W_164), true, ifeq3(theme(skc6, X_167, skc6), true, ifeq3(agent(skc6, Y_168, Z_166), true, ifeq3(agent(skc6, X_167, Z_166), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, W_164), true, skc6, W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.08 tff(c_11388, plain, (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, skc6, skc6), skc6), skc6), skc6)=skc6)). % 14.36/6.08 tff(c_11363, plain, (![X_829]: (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(theme(skc6, X_829, skc6), true, ifeq3(agent(skc6, X_829, skc9), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(think_believe_consider(skc6, X_829), true, skc6, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_11323, plain, (![Y_824, X_825, Z_827]: (ifeq3(theme(skc6, Y_824, skc6), true, ifeq3(theme(skc6, X_825, skc6), true, ifeq3(agent(skc6, Y_824, Z_827), true, ifeq3(agent(skc6, X_825, Z_827), true, ifeq3(think_believe_consider(skc6, Y_824), true, ifeq3(think_believe_consider(skc6, X_825), true, skc6, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_3489, plain, (![Y_168, X_167, V_169, Z_166]: (ifeq3(theme(skc6, Y_168, skc6), true, ifeq3(theme(skc6, X_167, V_169), true, ifeq3(agent(skc6, Y_168, Z_166), true, ifeq3(agent(skc6, X_167, Z_166), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, V_169), true, V_169, skc6), skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_11226, plain, (![Y_817, V_819, Z_820]: (ifeq3(theme(skc6, Y_817, skc6), true, ifeq3(theme(skc6, skc7, V_819), true, ifeq3(agent(skc6, Y_817, Z_820), true, ifeq3(agent(skc6, skc7, Z_820), true, ifeq3(think_believe_consider(skc6, Y_817), true, ifeq3(proposition(skc6, V_819), true, V_819, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_3382, plain, (![Y_168, W_164, V_169, Z_166]: (ifeq3(theme(skc6, Y_168, W_164), true, ifeq3(theme(skc6, skc7, V_169), true, ifeq3(agent(skc6, Y_168, Z_166), true, ifeq3(agent(skc6, skc7, Z_166), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.08 tff(c_11098, plain, (![W_807, V_809, Z_810]: (ifeq3(theme(skc6, skc7, W_807), true, ifeq3(theme(skc6, skc7, V_809), true, ifeq3(agent(skc6, skc7, Z_810), true, ifeq3(agent(skc6, skc7, Z_810), true, ifeq3(proposition(skc6, W_807), true, ifeq3(proposition(skc6, V_809), true, V_809, W_807), W_807), W_807), W_807), W_807), W_807)=W_807))). % 14.36/6.08 tff(c_11096, plain, (![W_807, X_808, Z_810]: (ifeq3(theme(skc6, skc7, W_807), true, ifeq3(theme(skc6, X_808, skc6), true, ifeq3(agent(skc6, skc7, Z_810), true, ifeq3(agent(skc6, X_808, Z_810), true, ifeq3(think_believe_consider(skc6, X_808), true, ifeq3(proposition(skc6, W_807), true, skc6, W_807), W_807), W_807), W_807), W_807), W_807)=W_807))). % 14.36/6.08 tff(c_3381, plain, (![W_164, X_167, V_169, Z_166]: (ifeq3(theme(skc6, skc7, W_164), true, ifeq3(theme(skc6, X_167, V_169), true, ifeq3(agent(skc6, skc7, Z_166), true, ifeq3(agent(skc6, X_167, Z_166), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.08 tff(c_9896, plain, (![Y_728, X_729, Z_731]: (ifeq3(theme(skc5, Y_728, skc6), true, ifeq3(theme(skc5, X_729, skc6), true, ifeq3(agent(skc5, Y_728, Z_731), true, ifeq3(agent(skc5, X_729, Z_731), true, ifeq3(think_believe_consider(skc5, Y_728), true, ifeq3(think_believe_consider(skc5, X_729), true, skc6, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.08 tff(c_10868, plain, (![W_793, V_795]: (ifeq3(theme(skc6, skc7, W_793), true, ifeq3(theme(skc6, skf1(skc9), V_795), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_793), true, ifeq3(proposition(skc6, V_795), true, V_795, W_793), W_793), W_793), W_793), W_793)=W_793))). % 14.36/6.08 tff(c_10921, plain, (![W_796]: (ifeq3(theme(skc6, skc7, W_796), true, ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_796), true, skc6, W_796), W_796), W_796), W_796)=W_796))). % 14.36/6.08 tff(c_9447, plain, (![W_694, X_695, Z_696]: (ifeq3(theme(skc5, skc7, W_694), true, ifeq3(theme(skc5, X_695, skc6), true, ifeq3(agent(skc5, skc7, Z_696), true, ifeq3(agent(skc5, X_695, Z_696), true, ifeq3(think_believe_consider(skc5, X_695), true, ifeq3(proposition(skc5, W_694), true, skc6, W_694), W_694), W_694), W_694), W_694), W_694)=W_694))). % 14.36/6.09 tff(c_10867, plain, (![W_793, X_794]: (ifeq3(theme(skc6, skc7, W_793), true, ifeq3(theme(skc6, X_794, skc6), true, ifeq3(agent(skc6, X_794, skc9), true, ifeq3(think_believe_consider(skc6, X_794), true, ifeq3(proposition(skc6, W_793), true, skc6, W_793), W_793), W_793), W_793), W_793)=W_793))). % 14.36/6.09 tff(c_4125, plain, (![W_164, X_167, V_169]: (ifeq3(theme(skc6, skc7, W_164), true, ifeq3(theme(skc6, X_167, V_169), true, ifeq3(agent(skc6, X_167, skc9), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.09 tff(c_10682, plain, (![W_782, V_783]: (ifeq3(theme(skc6, skf1(skc9), W_782), true, ifeq3(theme(skc6, skc7, V_783), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_782), true, ifeq3(proposition(skc6, V_783), true, V_783, W_782), W_782), W_782), W_782), W_782)=W_782))). % 14.36/6.09 tff(c_10784, plain, (![V_789]: (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(theme(skc6, skc7, V_789), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, V_789), true, V_789, skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.09 tff(c_10680, plain, (![Y_781, V_783]: (ifeq3(theme(skc6, Y_781, skc6), true, ifeq3(theme(skc6, skc7, V_783), true, ifeq3(agent(skc6, Y_781, skc9), true, ifeq3(think_believe_consider(skc6, Y_781), true, ifeq3(proposition(skc6, V_783), true, V_783, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.09 tff(c_10258, plain, (![X_753, Z_755]: (ifeq3(theme(skc6, X_753, skc6), true, ifeq3(agent(skc6, skc7, Z_755), true, ifeq3(agent(skc6, X_753, Z_755), true, ifeq3(think_believe_consider(skc6, X_753), true, skc6, skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.09 tff(c_10679, plain, (![W_782, V_783]: (ifeq3(theme(skc6, skc7, W_782), true, ifeq3(theme(skc6, skc7, V_783), true, ifeq3(proposition(skc6, W_782), true, ifeq3(proposition(skc6, V_783), true, V_783, W_782), W_782), W_782), W_782)=W_782))). % 14.36/6.09 tff(c_4126, plain, (![Y_168, W_164, V_169]: (ifeq3(theme(skc6, Y_168, W_164), true, ifeq3(theme(skc6, skc7, V_169), true, ifeq3(agent(skc6, Y_168, skc9), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(proposition(skc6, W_164), true, ifeq3(proposition(skc6, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.36/6.09 tff(c_10260, plain, (![V_754, Z_755]: (ifeq3(theme(skc6, skc7, V_754), true, ifeq3(agent(skc6, skc7, Z_755), true, ifeq3(agent(skc6, skc7, Z_755), true, ifeq3(proposition(skc6, V_754), true, V_754, skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.09 tff(c_10379, plain, (![Y_762, Z_764]: (ifeq3(theme(skc6, Y_762, skc6), true, ifeq3(agent(skc6, Y_762, Z_764), true, ifeq3(agent(skc6, skc7, Z_764), true, ifeq3(think_believe_consider(skc6, Y_762), true, skc6, skc6), skc6), skc6), skc6)=skc6))). % 14.36/6.09 tff(c_10381, plain, (![W_763, Z_764]: (ifeq3(theme(skc6, skc7, W_763), true, ifeq3(agent(skc6, skc7, Z_764), true, ifeq3(agent(skc6, skc7, Z_764), true, ifeq3(proposition(skc6, W_763), true, skc6, W_763), W_763), W_763), W_763)=W_763))). % 14.54/6.09 tff(c_9898, plain, (![Y_728, V_730, Z_731]: (ifeq3(theme(skc5, Y_728, skc6), true, ifeq3(theme(skc5, skc7, V_730), true, ifeq3(agent(skc5, Y_728, Z_731), true, ifeq3(agent(skc5, skc7, Z_731), true, ifeq3(think_believe_consider(skc5, Y_728), true, ifeq3(proposition(skc5, V_730), true, V_730, skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_10378, plain, (![Y_762, W_763]: (ifeq3(theme(skc6, Y_762, W_763), true, ifeq3(agent(skc6, Y_762, skc9), true, ifeq3(think_believe_consider(skc6, Y_762), true, ifeq3(proposition(skc6, W_763), true, skc6, W_763), W_763), W_763), W_763)=W_763))). % 14.54/6.09 tff(c_10456, plain, (![X_767]: (ifeq3(theme(skc6, X_767, skc6), true, ifeq3(agent(skc6, X_767, skc9), true, ifeq3(think_believe_consider(skc6, X_767), true, skc6, skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_10256, plain, (![X_753, V_754]: (ifeq3(theme(skc6, X_753, V_754), true, ifeq3(agent(skc6, X_753, skc9), true, ifeq3(think_believe_consider(skc6, X_753), true, ifeq3(proposition(skc6, V_754), true, V_754, skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_10380, plain, (![W_763]: (ifeq3(theme(skc6, skf1(skc9), W_763), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, W_763), true, skc6, W_763), W_763), W_763)=W_763))). % 14.54/6.09 tff(c_10377, plain, (![W_763]: (ifeq3(theme(skc6, skc7, W_763), true, ifeq3(proposition(skc6, W_763), true, skc6, W_763), W_763)=W_763))). % 14.54/6.09 tff(c_4161, plain, (![Y_168, W_164, Z_166]: (ifeq3(theme(skc6, Y_168, W_164), true, ifeq3(agent(skc6, Y_168, Z_166), true, ifeq3(agent(skc6, skc7, Z_166), true, ifeq3(think_believe_consider(skc6, Y_168), true, ifeq3(proposition(skc6, W_164), true, skc6, W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.54/6.09 tff(c_10334, plain, (ifeq3(theme(skc6, skf1(skc9), skc6), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, skc6, skc6), skc6)=skc6)). % 14.54/6.09 tff(c_10259, plain, (![V_754]: (ifeq3(theme(skc6, skf1(skc9), V_754), true, ifeq3(think_believe_consider(skc6, skf1(skc9)), true, ifeq3(proposition(skc6, V_754), true, V_754, skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_10255, plain, (![Z_755]: (ifeq3(agent(skc6, skc7, Z_755), true, ifeq3(agent(skc6, skc7, Z_755), true, skc6, skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9792, plain, (![W_721, V_723, Z_724]: (ifeq3(theme(skc5, skc7, W_721), true, ifeq3(theme(skc5, skc7, V_723), true, ifeq3(agent(skc5, skc7, Z_724), true, ifeq3(agent(skc5, skc7, Z_724), true, ifeq3(proposition(skc5, W_721), true, ifeq3(proposition(skc5, V_723), true, V_723, W_721), W_721), W_721), W_721), W_721), W_721)=W_721))). % 14.54/6.09 tff(c_10257, plain, (![V_754]: (ifeq3(theme(skc6, skc7, V_754), true, ifeq3(proposition(skc6, V_754), true, V_754, skc6), skc6)=skc6))). % 14.54/6.09 tff(c_4160, plain, (![X_167, V_169, Z_166]: (ifeq3(theme(skc6, X_167, V_169), true, ifeq3(agent(skc6, skc7, Z_166), true, ifeq3(agent(skc6, X_167, Z_166), true, ifeq3(think_believe_consider(skc6, X_167), true, ifeq3(proposition(skc6, V_169), true, V_169, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9442, plain, (![W_694, X_695]: (ifeq3(theme(skc5, skc7, W_694), true, ifeq3(theme(skc5, X_695, skc6), true, ifeq3(agent(skc5, X_695, skc9), true, ifeq3(think_believe_consider(skc5, X_695), true, ifeq3(proposition(skc5, W_694), true, skc6, W_694), W_694), W_694), W_694), W_694)=W_694))). % 14.54/6.09 tff(c_9308, plain, (![Y_683, V_685]: (ifeq3(theme(skc5, Y_683, skc6), true, ifeq3(theme(skc5, skc7, V_685), true, ifeq3(agent(skc5, Y_683, skc9), true, ifeq3(think_believe_consider(skc5, Y_683), true, ifeq3(proposition(skc5, V_685), true, V_685, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_8731, plain, (![Y_647, Z_649]: (ifeq3(theme(skc5, Y_647, skc6), true, ifeq3(agent(skc5, Y_647, Z_649), true, ifeq3(agent(skc5, skc7, Z_649), true, ifeq3(think_believe_consider(skc5, Y_647), true, skc6, skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9636, plain, (![V_712, Z_713]: (ifeq3(theme(skc5, skc7, V_712), true, ifeq3(agent(skc5, skc7, Z_713), true, ifeq3(agent(skc5, skc7, Z_713), true, ifeq3(proposition(skc5, V_712), true, V_712, skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9789, plain, (![W_721, Z_724]: (ifeq3(theme(skc5, skc7, W_721), true, ifeq3(agent(skc5, skc7, Z_724), true, ifeq3(agent(skc5, skc7, Z_724), true, ifeq3(proposition(skc5, W_721), true, skc6, W_721), W_721), W_721), W_721)=W_721))). % 14.54/6.09 tff(c_9444, plain, (![X_695, Z_696]: (ifeq3(theme(skc5, X_695, skc6), true, ifeq3(agent(skc5, skc7, Z_696), true, ifeq3(agent(skc5, X_695, Z_696), true, ifeq3(think_believe_consider(skc5, X_695), true, skc6, skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_3164, plain, (![W_377, V_379]: (ifeq3(of(skc6, W_377, skc9), true, ifeq3(of(skc6, V_379, skc9), true, ifeq3(forename(skc6, W_377), true, ifeq3(forename(skc6, V_379), true, W_377, V_379), V_379), V_379), V_379)=V_379))). % 14.54/6.09 tff(c_3167, plain, (![W_377, V_379]: (ifeq3(of(skc5, W_377, skc9), true, ifeq3(of(skc5, V_379, skc9), true, ifeq3(forename(skc5, W_377), true, ifeq3(forename(skc5, V_379), true, W_377, V_379), V_379), V_379), V_379)=V_379))). % 14.54/6.09 tff(c_3166, plain, (![W_377, X_378]: (ifeq3(of(skc6, W_377, X_378), true, ifeq3(of(skc6, skc8, X_378), true, ifeq3(forename(skc6, W_377), true, ifeq3(entity(skc6, X_378), true, W_377, skc8), skc8), skc8), skc8)=skc8))). % 14.54/6.09 tff(c_9923, plain, (![X_732]: (ifeq3(of(skc6, skc8, X_732), true, ifeq3(of(skc6, skc8, X_732), true, ifeq3(entity(skc6, X_732), true, skc8, skc8), skc8), skc8)=skc8))). % 14.54/6.09 tff(c_3165, plain, (![X_378, V_379]: (ifeq3(of(skc6, skc8, X_378), true, ifeq3(of(skc6, V_379, X_378), true, ifeq3(forename(skc6, V_379), true, ifeq3(entity(skc6, X_378), true, skc8, V_379), V_379), V_379), V_379)=V_379))). % 14.54/6.09 tff(c_3260, plain, (![Y_389, X_388, V_386, Z_387]: (ifeq3(theme(skc5, Y_389, skc6), true, ifeq3(theme(skc5, X_388, V_386), true, ifeq3(agent(skc5, Y_389, Z_387), true, ifeq3(agent(skc5, X_388, Z_387), true, ifeq3(think_believe_consider(skc5, Y_389), true, ifeq3(think_believe_consider(skc5, X_388), true, ifeq3(proposition(skc5, V_386), true, V_386, skc6), skc6), skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9309, plain, (![Y_683, W_684]: (ifeq3(theme(skc5, Y_683, W_684), true, ifeq3(agent(skc5, Y_683, skc9), true, ifeq3(think_believe_consider(skc5, Y_683), true, ifeq3(proposition(skc5, W_684), true, skc6, W_684), W_684), W_684), W_684)=W_684))). % 14.54/6.09 tff(c_9744, plain, (![X_719]: (ifeq3(theme(skc5, X_719, skc6), true, ifeq3(agent(skc5, X_719, skc9), true, ifeq3(think_believe_consider(skc5, X_719), true, skc6, skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_3262, plain, (![W_384, X_388, V_386, Z_387]: (ifeq3(theme(skc5, skc7, W_384), true, ifeq3(theme(skc5, X_388, V_386), true, ifeq3(agent(skc5, skc7, Z_387), true, ifeq3(agent(skc5, X_388, Z_387), true, ifeq3(think_believe_consider(skc5, X_388), true, ifeq3(proposition(skc5, W_384), true, ifeq3(proposition(skc5, V_386), true, V_386, W_384), W_384), W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.09 tff(c_8934, plain, (![X_659, V_660]: (ifeq3(theme(skc5, X_659, V_660), true, ifeq3(agent(skc5, X_659, skc9), true, ifeq3(think_believe_consider(skc5, X_659), true, ifeq3(proposition(skc5, V_660), true, V_660, skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.09 tff(c_9126, plain, (![W_669, V_671]: (ifeq3(theme(skc5, skc7, W_669), true, ifeq3(theme(skc5, skc7, V_671), true, ifeq3(proposition(skc5, W_669), true, ifeq3(proposition(skc5, V_671), true, V_671, W_669), W_669), W_669), W_669)=W_669))). % 14.54/6.09 tff(c_8352, plain, (![X_625]: (ifeq3(of(skc5, skc8, X_625), true, ifeq3(of(skc5, skc8, X_625), true, ifeq3(entity(skc5, X_625), true, skc8, skc8), skc8), skc8)=skc8))). % 14.54/6.09 tff(c_9646, plain, (![V_714]: (ifeq2(accessible_world(skc6, V_714), true, agent(V_714, skf1(skc9), skc9), true)=true))). % 14.54/6.10 tff(c_3263, plain, (![Y_389, W_384, V_386, Z_387]: (ifeq3(theme(skc5, Y_389, W_384), true, ifeq3(theme(skc5, skc7, V_386), true, ifeq3(agent(skc5, Y_389, Z_387), true, ifeq3(agent(skc5, skc7, Z_387), true, ifeq3(think_believe_consider(skc5, Y_389), true, ifeq3(proposition(skc5, W_384), true, ifeq3(proposition(skc5, V_386), true, V_386, W_384), W_384), W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.10 tff(c_3409, plain, (![U_148]: (ifeq2(agent(U_148, skf1(skc9), skc9), true, ifeq2(accessible_world(U_148, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_8936, plain, (![Z_661]: (ifeq3(agent(skc5, skc7, Z_661), true, ifeq3(agent(skc5, skc7, Z_661), true, skc6, skc6), skc6)=skc6))). % 14.54/6.10 tff(c_3287, plain, (![U_76, V_391]: (ifeq2(accessible_world(U_76, skc6), true, ifeq2(singleton(U_76, skf1(V_391)), true, true, true), true)=true))). % 14.54/6.10 tff(c_3114, plain, (![U_85, V_375]: (ifeq2(accessible_world(U_85, skc6), true, ifeq2(unisex(U_85, skf1(V_375)), true, true, true), true)=true))). % 14.54/6.10 tff(c_3054, plain, (![U_73, V_369]: (ifeq2(accessible_world(U_73, skc6), true, ifeq2(thing(U_73, skf1(V_369)), true, true, true), true)=true))). % 14.54/6.10 tff(c_3014, plain, (![U_79, V_367]: (ifeq2(accessible_world(U_79, skc6), true, ifeq2(specific(U_79, skf1(V_367)), true, true, true), true)=true))). % 14.54/6.10 tff(c_3195, plain, (![U_82, V_381]: (ifeq2(accessible_world(U_82, skc6), true, ifeq2(nonexistent(U_82, skf1(V_381)), true, true, true), true)=true))). % 14.54/6.10 tff(c_4196, plain, (![W_161]: (ifeq3(of(skc6, W_161, skc9), true, ifeq3(forename(skc6, W_161), true, W_161, skc8), skc8)=skc8))). % 14.54/6.10 tff(c_3261, plain, (![Y_389, W_384, X_388, Z_387]: (ifeq3(theme(skc5, Y_389, W_384), true, ifeq3(theme(skc5, X_388, skc6), true, ifeq3(agent(skc5, Y_389, Z_387), true, ifeq3(agent(skc5, X_388, Z_387), true, ifeq3(think_believe_consider(skc5, Y_389), true, ifeq3(think_believe_consider(skc5, X_388), true, ifeq3(proposition(skc5, W_384), true, skc6, W_384), W_384), W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.10 tff(c_4195, plain, (![V_163]: (ifeq3(of(skc6, V_163, skc9), true, ifeq3(forename(skc6, V_163), true, skc8, V_163), V_163)=V_163))). % 14.54/6.10 tff(c_2951, plain, (![U_70, V_361]: (ifeq2(accessible_world(U_70, skc6), true, ifeq2(eventuality(U_70, skf1(V_361)), true, true, true), true)=true))). % 14.54/6.10 tff(c_2896, plain, (![U_67, V_355]: (ifeq2(accessible_world(U_67, skc6), true, ifeq2(event(U_67, skf1(V_355)), true, true, true), true)=true))). % 14.54/6.10 tff(c_3169, plain, (![W_377]: (ifeq3(of(skc5, W_377, skc9), true, ifeq3(forename(skc5, W_377), true, W_377, skc8), skc8)=skc8))). % 14.54/6.10 tff(c_8350, plain, (![V_626]: (ifeq3(of(skc5, V_626, skc9), true, ifeq3(forename(skc5, V_626), true, skc8, V_626), V_626)=V_626))). % 14.54/6.10 tff(c_3257, plain, (![Y_389, W_384, V_386]: (ifeq3(theme(skc5, Y_389, W_384), true, ifeq3(theme(skc5, skc7, V_386), true, ifeq3(agent(skc5, Y_389, skc9), true, ifeq3(think_believe_consider(skc5, Y_389), true, ifeq3(proposition(skc5, W_384), true, ifeq3(proposition(skc5, V_386), true, V_386, W_384), W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.10 tff(c_2786, plain, (![U_64, V_344]: (ifeq2(accessible_world(U_64, skc6), true, ifeq2(smoke(U_64, skf1(V_344)), true, true, true), true)=true))). % 14.54/6.10 tff(c_9219, plain, (![V_677, V_678]: (ifeq2(accessible_world(skc6, V_677), true, present(V_677, skf1(V_678)), true)=true))). % 14.54/6.10 tff(c_2848, plain, (![U_88, V_350]: (ifeq2(present(U_88, skf1(V_350)), true, ifeq2(accessible_world(U_88, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_4191, plain, (![U_156]: (ifeq2(of(U_156, skc8, skc9), true, ifeq2(accessible_world(U_156, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_4156, plain, (![U_152]: (ifeq2(theme(U_152, skc7, skc6), true, ifeq2(accessible_world(U_152, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_9078, plain, (![V_668]: (ifeq2(accessible_world(skc6, V_668), true, agent(V_668, skc7, skc9), true)=true))). % 14.54/6.10 tff(c_3256, plain, (![W_384, X_388, V_386]: (ifeq3(theme(skc5, skc7, W_384), true, ifeq3(theme(skc5, X_388, V_386), true, ifeq3(agent(skc5, X_388, skc9), true, ifeq3(think_believe_consider(skc5, X_388), true, ifeq3(proposition(skc5, W_384), true, ifeq3(proposition(skc5, V_386), true, V_386, W_384), W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.10 tff(c_4121, plain, (![U_148]: (ifeq2(agent(U_148, skc7, skc9), true, ifeq2(accessible_world(U_148, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_9012, plain, (![V_665]: (ifeq2(accessible_world(skc6, V_665), true, theme(V_665, skc7, skc6), true)=true))). % 14.54/6.10 tff(c_8969, plain, (![V_663]: (ifeq2(accessible_world(skc6, V_663), true, of(V_663, skc8, skc9), true)=true))). % 14.54/6.10 tff(c_8935, plain, (![V_660]: (ifeq3(theme(skc5, skc7, V_660), true, ifeq3(proposition(skc5, V_660), true, V_660, skc6), skc6)=skc6))). % 14.54/6.10 tff(c_3258, plain, (![X_388, V_386, Z_387]: (ifeq3(theme(skc5, X_388, V_386), true, ifeq3(agent(skc5, skc7, Z_387), true, ifeq3(agent(skc5, X_388, Z_387), true, ifeq3(think_believe_consider(skc5, X_388), true, ifeq3(proposition(skc5, V_386), true, V_386, skc6), skc6), skc6), skc6), skc6)=skc6))). % 14.54/6.10 tff(c_8728, plain, (![W_648]: (ifeq3(theme(skc5, skc7, W_648), true, ifeq3(proposition(skc5, W_648), true, skc6, W_648), W_648)=W_648))). % 14.54/6.10 tff(c_2615, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc6), true, ifeq2(singleton(U_334, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_1839, plain, (![U_73]: (ifeq2(accessible_world(U_73, skc6), true, ifeq2(thing(U_73, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_1982, plain, (![U_133]: (ifeq2(accessible_world(U_133, skc6), true, ifeq2(nonhuman(U_133, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_1900, plain, (![U_136]: (ifeq2(accessible_world(U_136, skc6), true, ifeq2(general(U_136, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_2093, plain, (![U_310]: (ifeq2(accessible_world(U_310, skc6), true, ifeq2(unisex(U_310, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_2727, plain, (![U_76]: (ifeq2(accessible_world(U_76, skc6), true, ifeq2(singleton(U_76, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_4055, plain, (![U_76]: (ifeq2(accessible_world(U_76, skc6), true, ifeq2(singleton(U_76, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_2668, plain, (![U_79]: (ifeq2(accessible_world(U_79, skc6), true, ifeq2(specific(U_79, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_3259, plain, (![Y_389, W_384, Z_387]: (ifeq3(theme(skc5, Y_389, W_384), true, ifeq3(agent(skc5, Y_389, Z_387), true, ifeq3(agent(skc5, skc7, Z_387), true, ifeq3(think_believe_consider(skc5, Y_389), true, ifeq3(proposition(skc5, W_384), true, skc6, W_384), W_384), W_384), W_384), W_384)=W_384))). % 14.54/6.10 tff(c_2592, plain, (![U_103]: (ifeq2(accessible_world(U_103, skc6), true, ifeq2(existent(U_103, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_1778, plain, (![U_130]: (ifeq2(accessible_world(U_130, skc6), true, ifeq2(abstraction(U_130, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_2538, plain, (![U_73]: (ifeq2(accessible_world(U_73, skc6), true, ifeq2(thing(U_73, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2621, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc5), true, ifeq2(singleton(U_334, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2627, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc5), true, ifeq2(singleton(U_334, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_3855, plain, (![U_136]: (ifeq2(accessible_world(U_136, skc6), true, ifeq2(general(U_136, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_2397, plain, (![U_100]: (ifeq2(accessible_world(U_100, skc6), true, ifeq2(entity(U_100, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_3927, plain, (![U_76]: (ifeq2(accessible_world(U_76, skc6), true, ifeq2(singleton(U_76, skc7), true, true, true), true)=true))). % 14.54/6.10 tff(c_3886, plain, (![U_133]: (ifeq2(accessible_world(U_133, skc6), true, ifeq2(nonhuman(U_133, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_3171, plain, (![W_377, X_378]: (ifeq3(of(skc5, W_377, X_378), true, ifeq3(of(skc5, skc8, X_378), true, ifeq3(forename(skc5, W_377), true, ifeq3(entity(skc5, X_378), true, W_377, skc8), skc8), skc8), skc8)=skc8))). % 14.54/6.10 tff(c_2510, plain, (![U_109]: (ifeq2(accessible_world(U_109, skc6), true, ifeq2(living(U_109, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2481, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc6), true, ifeq2(relation(U_328, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_3955, plain, (![U_73]: (ifeq2(accessible_world(U_73, skc6), true, ifeq2(thing(U_73, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_4008, plain, (![U_85]: (ifeq2(accessible_world(U_85, skc6), true, ifeq2(unisex(U_85, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_2451, plain, (![U_106]: (ifeq2(accessible_world(U_106, skc6), true, ifeq2(impartial(U_106, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2633, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc5), true, ifeq2(singleton(U_334, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_1441, plain, (![U_272]: (ifeq2(accessible_world(U_272, skc5), true, ifeq2(general(U_272, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_1878, plain, (![U_297]: (ifeq2(accessible_world(U_297, skc5), true, ifeq2(specific(U_297, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2105, plain, (![U_310]: (ifeq2(accessible_world(U_310, skc5), true, ifeq2(unisex(U_310, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_3170, plain, (![X_378, V_379]: (ifeq3(of(skc5, skc8, X_378), true, ifeq3(of(skc5, V_379, X_378), true, ifeq3(forename(skc5, V_379), true, ifeq3(entity(skc5, X_378), true, skc8, V_379), V_379), V_379), V_379)=V_379))). % 14.54/6.10 tff(c_1639, plain, (![U_285]: (ifeq2(accessible_world(U_285, skc5), true, ifeq2(thing(U_285, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_1362, plain, (![U_266]: (ifeq2(accessible_world(U_266, skc5), true, ifeq2(nonhuman(U_266, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_2051, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc5), true, ifeq2(existent(U_306, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_1633, plain, (![U_285]: (ifeq2(accessible_world(U_285, skc5), true, ifeq2(thing(U_285, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2345, plain, (![U_115]: (ifeq2(accessible_world(U_115, skc6), true, ifeq2(animate(U_115, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_2298, plain, (![U_97]: (ifeq2(accessible_world(U_97, skc6), true, ifeq2(organism(U_97, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_3643, plain, (![U_130]: (ifeq2(accessible_world(U_130, skc6), true, ifeq2(abstraction(U_130, skc6), true, true, true), true)=true))). % 14.54/6.10 tff(c_3798, plain, (![U_79]: (ifeq2(accessible_world(U_79, skc6), true, ifeq2(specific(U_79, skc7), true, true, true), true)=true))). % 14.54/6.10 tff(c_3683, plain, (![U_73]: (ifeq2(accessible_world(U_73, skc6), true, ifeq2(thing(U_73, skc7), true, true, true), true)=true))). % 14.54/6.10 tff(c_2934, plain, (![U_357]: (ifeq2(agent(U_357, skc7, skc9), true, ifeq2(accessible_world(U_357, skc5), true, true, true), true)=true))). % 14.54/6.10 tff(c_2267, plain, (![U_112]: (ifeq2(accessible_world(U_112, skc6), true, ifeq2(human(U_112, skc9), true, true, true), true)=true))). % 14.54/6.10 tff(c_1950, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc6), true, ifeq2(relname(U_300, skc8), true, true, true), true)=true))). % 14.54/6.10 tff(c_3733, plain, (![U_85]: (ifeq2(accessible_world(U_85, skc6), true, ifeq2(unisex(U_85, skc7), true, true, true), true)=true))). % 14.54/6.10 tff(c_3767, plain, (![U_82]: (ifeq2(accessible_world(U_82, skc6), true, ifeq2(nonexistent(U_82, skc7), true, true, true), true)=true))). % 14.54/6.10 tff(c_2111, plain, (![U_310]: (ifeq2(accessible_world(U_310, skc5), true, ifeq2(unisex(U_310, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_1594, plain, (![U_282]: (ifeq2(accessible_world(U_282, skc5), true, ifeq2(abstraction(U_282, skc8), true, true, true), true)=true))). % 14.54/6.11 tff(c_1368, plain, (![U_266]: (ifeq2(accessible_world(U_266, skc5), true, ifeq2(nonhuman(U_266, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_7983, plain, (![V_606]: (ifeq2(accessible_world(skc5, V_606), true, agent(V_606, skc7, skc9), true)=true))). % 14.54/6.11 tff(c_2005, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc5), true, ifeq2(entity(U_303, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_1645, plain, (![U_285]: (ifeq2(accessible_world(U_285, skc5), true, ifeq2(thing(U_285, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_1447, plain, (![U_272]: (ifeq2(accessible_world(U_272, skc5), true, ifeq2(general(U_272, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_2639, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc5), true, ifeq2(singleton(U_334, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_1491, plain, (![U_275]: (ifeq2(accessible_world(U_275, skc5), true, ifeq2(impartial(U_275, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2242, plain, (![U_316]: (ifeq2(accessible_world(U_316, skc5), true, ifeq2(living(U_316, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2172, plain, (![U_94]: (ifeq2(accessible_world(U_94, skc6), true, ifeq2(human_person(U_94, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_7823, plain, (![V_597]: (ifeq2(accessible_world(skc5, V_597), true, of(V_597, skc8, skc9), true)=true))). % 14.54/6.11 tff(c_3599, plain, (![U_70]: (ifeq2(accessible_world(U_70, skc6), true, ifeq2(eventuality(U_70, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_3546, plain, (![U_127]: (ifeq2(accessible_world(U_127, skc6), true, ifeq2(relation(U_127, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_2364, plain, (![U_322]: (ifeq2(accessible_world(U_322, skc6), true, ifeq2(male(U_322, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2747, plain, (![U_340]: (ifeq2(accessible_world(U_340, skc6), true, ifeq2(forename(U_340, skc8), true, true, true), true)=true))). % 14.54/6.11 tff(c_1884, plain, (![U_297]: (ifeq2(accessible_world(U_297, skc5), true, ifeq2(specific(U_297, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_1651, plain, (![U_285]: (ifeq2(accessible_world(U_285, skc5), true, ifeq2(thing(U_285, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_1824, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc5), true, ifeq2(animate(U_294, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2487, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc5), true, ifeq2(relation(U_328, skc8), true, true, true), true)=true))). % 14.54/6.11 tff(c_1753, plain, (![U_291]: (ifeq2(accessible_world(U_291, skc5), true, ifeq2(human(U_291, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_3084, plain, (![U_370]: (ifeq2(theme(U_370, skc7, skc6), true, ifeq2(accessible_world(U_370, skc5), true, true, true), true)=true))). % 14.54/6.11 tff(c_2099, plain, (![U_310]: (ifeq2(accessible_world(U_310, skc5), true, ifeq2(unisex(U_310, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_1600, plain, (![U_282]: (ifeq2(accessible_world(U_282, skc5), true, ifeq2(abstraction(U_282, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_2816, plain, (![U_346]: (ifeq2(accessible_world(U_346, skc5), true, ifeq2(nonexistent(U_346, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_2201, plain, (![U_313]: (ifeq2(accessible_world(U_313, skc5), true, ifeq2(organism(U_313, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2132, plain, (![U_91]: (ifeq2(accessible_world(U_91, skc6), true, ifeq2(man(U_91, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_1575, plain, (![U_145]: (ifeq2(accessible_world(U_145, skc6), true, ifeq2(vincent_forename(U_145, skc8), true, true, true), true)=true))). % 14.54/6.11 tff(c_7494, plain, (![V_579]: (ifeq2(accessible_world(skc5, V_579), true, theme(V_579, skc7, skc6), true)=true))). % 14.54/6.11 tff(c_7452, plain, (![V_577]: (ifeq2(accessible_world(skc6, V_577), true, present(V_577, skc7), true)=true))). % 14.54/6.11 tff(c_7409, plain, (![V_575]: (ifeq2(accessible_world(skc6, V_575), true, think_believe_consider(V_575, skc7), true)=true))). % 14.54/6.11 tff(c_3334, plain, (![U_88]: (ifeq2(present(U_88, skc7), true, ifeq2(accessible_world(U_88, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_3482, plain, (![U_124]: (ifeq2(accessible_world(U_124, skc6), true, ifeq2(proposition(U_124, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_3377, plain, (![U_121]: (ifeq2(think_believe_consider(U_121, skc7), true, ifeq2(accessible_world(U_121, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_3515, plain, (![U_67]: (ifeq2(accessible_world(U_67, skc6), true, ifeq2(event(U_67, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_2997, plain, (![U_363]: (ifeq2(of(U_363, skc8, skc9), true, ifeq2(accessible_world(U_363, skc5), true, true, true), true)=true))). % 14.54/6.11 tff(c_1412, plain, (![U_269]: (ifeq2(accessible_world(U_269, skc5), true, ifeq2(eventuality(U_269, skc7), true, true, true), true)=true))). % 14.54/6.11 tff(c_1523, plain, (![U_278]: (ifeq2(accessible_world(U_278, skc5), true, ifeq2(human_person(U_278, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_1956, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc5), true, ifeq2(relname(U_300, skc8), true, true, true), true)=true))). % 14.54/6.11 tff(c_2370, plain, (![U_322]: (ifeq2(accessible_world(U_322, skc5), true, ifeq2(male(U_322, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_2493, plain, (![U_328]: (ifeq2(accessible_world(U_328, skc5), true, ifeq2(relation(U_328, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_7162, plain, (![W_562]: (ifeq2(impartial(skc5, W_562), true, impartial(skc6, W_562), true)=true))). % 14.54/6.11 tff(c_7141, plain, (![W_561]: (ifeq2(human_person(skc5, W_561), true, human_person(skc6, W_561), true)=true))). % 14.54/6.11 tff(c_1709, plain, (![U_288]: (ifeq2(accessible_world(U_288, skc5), true, ifeq2(man(U_288, skc9), true, true, true), true)=true))). % 14.54/6.11 tff(c_7098, plain, (![V_356]: (ifeq2(eventuality(skc5, skf1(V_356)), true, true, true)=true))). % 14.54/6.11 tff(c_7064, plain, (![W_557]: (ifeq2(eventuality(skc5, W_557), true, eventuality(skc6, W_557), true)=true))). % 14.54/6.11 tff(c_7021, plain, (![W_555]: (ifeq2(human(skc5, W_555), true, human(skc6, W_555), true)=true))). % 14.54/6.11 tff(c_2702, plain, (![U_337]: (ifeq2(accessible_world(U_337, skc5), true, ifeq2(proposition(U_337, skc6), true, true, true), true)=true))). % 14.54/6.11 tff(c_6947, plain, (![W_552]: (ifeq2(relation(skc5, W_552), true, relation(skc6, W_552), true)=true))). % 14.54/6.11 tff(c_6904, plain, (![W_550]: (ifeq2(man(skc5, W_550), true, man(skc6, W_550), true)=true))). % 14.54/6.11 tff(c_6861, plain, (![W_548]: (ifeq2(relname(skc5, W_548), true, relname(skc6, W_548), true)=true))). % 14.54/6.11 tff(c_6818, plain, (![W_546]: (ifeq2(organism(skc5, W_546), true, organism(skc6, W_546), true)=true))). % 14.54/6.11 tff(c_6726, plain, (![W_542]: (ifeq2(forename(skc5, W_542), true, forename(skc6, W_542), true)=true))). % 14.54/6.11 tff(c_6760, plain, (![V_374]: (ifeq2(unisex(skc5, skf1(V_374)), true, true, true)=true))). % 14.54/6.11 tff(c_6686, plain, (![W_541]: (ifeq2(unisex(skc5, W_541), true, unisex(skc6, W_541), true)=true))). % 14.54/6.11 tff(c_6641, plain, (![W_539]: (ifeq2(entity(skc5, W_539), true, entity(skc6, W_539), true)=true))). % 14.54/6.11 tff(c_6619, plain, (![V_380]: (ifeq2(nonexistent(skc5, skf1(V_380)), true, true, true)=true))). % 14.54/6.11 tff(c_6585, plain, (![W_536]: (ifeq2(nonexistent(skc5, W_536), true, nonexistent(skc6, W_536), true)=true))). % 14.54/6.11 tff(c_6542, plain, (![V_368]: (ifeq2(thing(skc5, skf1(V_368)), true, true, true)=true))). % 14.54/6.11 tff(c_6481, plain, (![W_533]: (ifeq2(thing(skc5, W_533), true, thing(skc6, W_533), true)=true))). % 14.54/6.11 tff(c_6438, plain, (![W_531]: (ifeq2(existent(skc5, W_531), true, existent(skc6, W_531), true)=true))). % 14.54/6.11 tff(c_6395, plain, (![W_529]: (ifeq2(vincent_forename(skc5, W_529), true, vincent_forename(skc6, W_529), true)=true))). % 14.54/6.11 tff(c_3198, plain, (![V_381]: (ifeq(tuple(true, existent(skc6, skf1(V_381))), tuple(true, true), a, b)=b))). % 14.54/6.11 tff(c_3017, plain, (![V_367]: (ifeq(tuple(true, general(skc6, skf1(V_367))), tuple(true, true), a, b)=b))). % 14.54/6.11 tff(c_3117, plain, (![V_375]: (ifeq(tuple(true, male(skc6, skf1(V_375))), tuple(true, true), a, b)=b))). % 14.54/6.11 tff(c_6311, plain, (![W_524]: (ifeq2(abstraction(skc5, W_524), true, abstraction(skc6, W_524), true)=true))). % 14.54/6.11 tff(c_1903, plain, (ifeq(tuple(specific(skc6, skc8), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1928, plain, (ifeq(tuple(true, male(skc6, skc8)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1985, plain, (ifeq(tuple(human(skc6, skc8), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_2595, plain, (ifeq(tuple(nonexistent(skc6, skc9), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_2671, plain, (ifeq(tuple(true, general(skc6, skc9)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_4011, plain, (ifeq(tuple(true, male(skc6, skc6)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_3889, plain, (ifeq(tuple(human(skc6, skc6), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_6232, plain, (![V_522]: (ifeq2(accessible_world(skc5, V_522), true, present(V_522, skc7), true)=true))). % 14.54/6.11 tff(c_3858, plain, (ifeq(tuple(specific(skc6, skc6), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1276, plain, (ifeq(tuple(specific(skc5, skc8), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1255, plain, (ifeq(tuple(human(skc5, skc8), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1212, plain, (ifeq(tuple(true, male(skc5, skc8)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1393, plain, (ifeq(tuple(nonexistent(skc5, skc9), true), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_1180, plain, (ifeq(tuple(true, general(skc5, skc9)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_3801, plain, (ifeq(tuple(true, general(skc6, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_6161, plain, (![W_520]: (ifeq2(male(skc5, W_520), true, male(skc6, W_520), true)=true))). % 14.54/6.11 tff(c_3294, plain, (![V_77, V_391]: (ifeq2(accessible_world(skc6, V_77), true, singleton(V_77, skf1(V_391)), true)=true))). % 14.54/6.11 tff(c_3127, plain, (![V_86, V_375]: (ifeq2(accessible_world(skc6, V_86), true, unisex(V_86, skf1(V_375)), true)=true))). % 14.54/6.11 tff(c_3205, plain, (![V_83, V_381]: (ifeq2(accessible_world(skc6, V_83), true, nonexistent(V_83, skf1(V_381)), true)=true))). % 14.54/6.11 tff(c_3070, plain, (![V_74, V_369]: (ifeq2(accessible_world(skc6, V_74), true, thing(V_74, skf1(V_369)), true)=true))). % 14.54/6.11 tff(c_3027, plain, (![V_80, V_367]: (ifeq2(accessible_world(skc6, V_80), true, specific(V_80, skf1(V_367)), true)=true))). % 14.54/6.11 tff(c_3736, plain, (ifeq(tuple(true, male(skc6, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.11 tff(c_2970, plain, (![V_71, V_361]: (ifeq2(accessible_world(skc6, V_71), true, eventuality(V_71, skf1(V_361)), true)=true))). % 14.54/6.11 tff(c_6040, plain, (![V_506]: (ifeq2(accessible_world(skc5, V_506), true, think_believe_consider(V_506, skc7), true)=true))). % 14.54/6.11 tff(c_2793, plain, (![V_65, V_344]: (ifeq2(accessible_world(skc6, V_65), true, smoke(V_65, skf1(V_344)), true)=true))). % 14.54/6.11 tff(c_2906, plain, (![V_68, V_355]: (ifeq2(accessible_world(skc6, V_68), true, event(V_68, skf1(V_355)), true)=true))). % 14.54/6.11 tff(c_2645, plain, (![V_335]: (ifeq2(accessible_world(skc6, V_335), true, singleton(V_335, skc8), true)=true))). % 14.54/6.11 tff(c_2117, plain, (![V_311]: (ifeq2(accessible_world(skc6, V_311), true, unisex(V_311, skc8), true)=true))). % 14.54/6.12 tff(c_1909, plain, (![V_137]: (ifeq2(accessible_world(skc6, V_137), true, general(V_137, skc8), true)=true))). % 14.54/6.12 tff(c_2270, plain, (ifeq(tuple(true, nonhuman(skc6, skc9)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_5926, plain, (![V_390]: (ifeq2(singleton(skc5, skf1(V_390)), true, true, true)=true))). % 14.54/6.12 tff(c_5865, plain, (![W_496]: (ifeq2(singleton(skc5, W_496), true, singleton(skc6, W_496), true)=true))). % 14.54/6.12 tff(c_1854, plain, (![V_74]: (ifeq2(accessible_world(skc6, V_74), true, thing(V_74, skc8), true)=true))). % 14.54/6.12 tff(c_1991, plain, (![V_134]: (ifeq2(accessible_world(skc6, V_134), true, nonhuman(V_134, skc8), true)=true))). % 14.54/6.12 tff(c_2733, plain, (![V_77]: (ifeq2(accessible_world(skc6, V_77), true, singleton(V_77, skc9), true)=true))). % 14.54/6.12 tff(c_2680, plain, (![V_80]: (ifeq2(accessible_world(skc6, V_80), true, specific(V_80, skc9), true)=true))). % 14.54/6.12 tff(c_2553, plain, (![V_74]: (ifeq2(accessible_world(skc6, V_74), true, thing(V_74, skc9), true)=true))). % 14.54/6.12 tff(c_3770, plain, (ifeq(tuple(true, existent(skc6, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_1796, plain, (![V_131]: (ifeq2(accessible_world(skc6, V_131), true, abstraction(V_131, skc8), true)=true))). % 14.54/6.12 tff(c_5712, plain, (![W_488]: (ifeq2(nonhuman(skc5, W_488), true, nonhuman(skc6, W_488), true)=true))). % 14.54/6.12 tff(c_4061, plain, (![V_77]: (ifeq2(accessible_world(skc6, V_77), true, singleton(V_77, skc6), true)=true))). % 14.54/6.12 tff(c_2601, plain, (![V_104]: (ifeq2(accessible_world(skc6, V_104), true, existent(V_104, skc9), true)=true))). % 14.54/6.12 tff(c_2647, plain, (![V_335]: (ifeq2(accessible_world(skc5, V_335), true, singleton(V_335, skc8), true)=true))). % 14.54/6.12 tff(c_2646, plain, (![V_335]: (ifeq2(accessible_world(skc5, V_335), true, singleton(V_335, skc9), true)=true))). % 14.54/6.12 tff(c_2457, plain, (![V_107]: (ifeq2(accessible_world(skc6, V_107), true, impartial(V_107, skc9), true)=true))). % 14.54/6.12 tff(c_1215, plain, (ifeq(tuple(true, male(skc5, skc6)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_3933, plain, (![V_77]: (ifeq2(accessible_world(skc6, V_77), true, singleton(V_77, skc7), true)=true))). % 14.54/6.12 tff(c_5567, plain, (![W_480]: (ifeq2(proposition(skc5, W_480), true, proposition(skc6, W_480), true)=true))). % 14.54/6.12 tff(c_2516, plain, (![V_110]: (ifeq2(accessible_world(skc6, V_110), true, living(V_110, skc9), true)=true))). % 14.54/6.12 tff(c_3864, plain, (![V_137]: (ifeq2(accessible_world(skc6, V_137), true, general(V_137, skc6), true)=true))). % 14.54/6.12 tff(c_3895, plain, (![V_134]: (ifeq2(accessible_world(skc6, V_134), true, nonhuman(V_134, skc6), true)=true))). % 14.54/6.12 tff(c_2412, plain, (![V_101]: (ifeq2(accessible_world(skc6, V_101), true, entity(V_101, skc9), true)=true))). % 14.54/6.12 tff(c_4020, plain, (![V_86]: (ifeq2(accessible_world(skc6, V_86), true, unisex(V_86, skc6), true)=true))). % 14.54/6.12 tff(c_1121, plain, (ifeq(tuple(specific(skc5, skc6), true), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_2499, plain, (![V_329]: (ifeq2(accessible_world(skc6, V_329), true, relation(V_329, skc8), true)=true))). % 14.54/6.12 tff(c_5430, plain, (![W_472]: (ifeq2(living(skc5, W_472), true, living(skc6, W_472), true)=true))). % 14.54/6.12 tff(c_3970, plain, (![V_74]: (ifeq2(accessible_world(skc6, V_74), true, thing(V_74, skc6), true)=true))). % 14.54/6.12 tff(c_1453, plain, (![V_273]: (ifeq2(accessible_world(skc5, V_273), true, general(V_273, skc8), true)=true))). % 14.54/6.12 tff(c_2057, plain, (![V_307]: (ifeq2(accessible_world(skc5, V_307), true, existent(V_307, skc9), true)=true))). % 14.54/6.12 tff(c_2648, plain, (![V_335]: (ifeq2(accessible_world(skc5, V_335), true, singleton(V_335, skc6), true)=true))). % 14.54/6.12 tff(c_1657, plain, (![V_286]: (ifeq2(accessible_world(skc5, V_286), true, thing(V_286, skc9), true)=true))). % 14.54/6.12 tff(c_1258, plain, (ifeq(tuple(human(skc5, skc6), true), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_1658, plain, (![V_286]: (ifeq2(accessible_world(skc5, V_286), true, thing(V_286, skc8), true)=true))). % 14.54/6.12 tff(c_1374, plain, (![V_267]: (ifeq2(accessible_world(skc5, V_267), true, nonhuman(V_267, skc8), true)=true))). % 14.54/6.12 tff(c_2119, plain, (![V_311]: (ifeq2(accessible_world(skc5, V_311), true, unisex(V_311, skc8), true)=true))). % 14.54/6.12 tff(c_2570, plain, (![U_331]: (ifeq2(present(U_331, skc7), true, ifeq2(accessible_world(U_331, skc5), true, true, true), true)=true))). % 14.54/6.12 tff(c_1890, plain, (![V_298]: (ifeq2(accessible_world(skc5, V_298), true, specific(V_298, skc9), true)=true))). % 14.54/6.12 tff(c_2351, plain, (![V_116]: (ifeq2(accessible_world(skc6, V_116), true, animate(V_116, skc9), true)=true))). % 14.54/6.12 tff(c_1962, plain, (![V_301]: (ifeq2(accessible_world(skc6, V_301), true, relname(V_301, skc8), true)=true))). % 14.54/6.12 tff(c_3810, plain, (![V_80]: (ifeq2(accessible_world(skc6, V_80), true, specific(V_80, skc7), true)=true))). % 14.54/6.12 tff(c_3661, plain, (![V_131]: (ifeq2(accessible_world(skc6, V_131), true, abstraction(V_131, skc6), true)=true))). % 14.54/6.12 tff(c_2223, plain, (ifeq(tuple(unisex(skc6, skc9), true), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_3698, plain, (![V_74]: (ifeq2(accessible_world(skc6, V_74), true, thing(V_74, skc7), true)=true))). % 14.54/6.12 tff(c_5114, plain, (![W_455]: (ifeq2(animate(skc5, W_455), true, animate(skc6, W_455), true)=true))). % 14.54/6.12 tff(c_2313, plain, (![V_98]: (ifeq2(accessible_world(skc6, V_98), true, organism(V_98, skc9), true)=true))). % 14.54/6.12 tff(c_3745, plain, (![V_86]: (ifeq2(accessible_world(skc6, V_86), true, unisex(V_86, skc7), true)=true))). % 14.54/6.12 tff(c_3776, plain, (![V_83]: (ifeq2(accessible_world(skc6, V_83), true, nonexistent(V_83, skc7), true)=true))). % 14.54/6.12 tff(c_2276, plain, (![V_113]: (ifeq2(accessible_world(skc6, V_113), true, human(V_113, skc9), true)=true))). % 14.54/6.12 tff(c_2120, plain, (![V_311]: (ifeq2(accessible_world(skc5, V_311), true, unisex(V_311, skc6), true)=true))). % 14.54/6.12 tff(c_1118, plain, (ifeq(tuple(true, general(skc5, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_2248, plain, (![V_317]: (ifeq2(accessible_world(skc5, V_317), true, living(V_317, skc9), true)=true))). % 14.54/6.12 tff(c_1659, plain, (![V_286]: (ifeq2(accessible_world(skc5, V_286), true, thing(V_286, skc6), true)=true))). % 14.54/6.12 tff(c_2011, plain, (![V_304]: (ifeq2(accessible_world(skc5, V_304), true, entity(V_304, skc9), true)=true))). % 14.54/6.12 tff(c_1327, plain, (![U_263]: (ifeq2(accessible_world(U_263, skc5), true, ifeq2(vincent_forename(U_263, skc8), true, true, true), true)=true))). % 14.54/6.12 tff(c_2649, plain, (![V_335]: (ifeq2(accessible_world(skc5, V_335), true, singleton(V_335, skc7), true)=true))). % 14.54/6.12 tff(c_1375, plain, (![V_267]: (ifeq2(accessible_world(skc5, V_267), true, nonhuman(V_267, skc6), true)=true))). % 14.54/6.12 tff(c_1454, plain, (![V_273]: (ifeq2(accessible_world(skc5, V_273), true, general(V_273, skc6), true)=true))). % 14.54/6.12 tff(c_1497, plain, (![V_276]: (ifeq2(accessible_world(skc5, V_276), true, impartial(V_276, skc9), true)=true))). % 14.54/6.12 tff(c_1606, plain, (![V_283]: (ifeq2(accessible_world(skc5, V_283), true, abstraction(V_283, skc8), true)=true))). % 14.54/6.12 tff(c_1161, plain, (ifeq(tuple(true, existent(skc5, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_4838, plain, (![V_354]: (ifeq2(event(skc5, skf1(V_354)), true, true, true)=true))). % 14.54/6.12 tff(c_4804, plain, (![W_438]: (ifeq2(event(skc5, W_438), true, event(skc6, W_438), true)=true))). % 14.54/6.12 tff(c_2187, plain, (![V_95]: (ifeq2(accessible_world(skc6, V_95), true, human_person(V_95, skc9), true)=true))). % 14.54/6.12 tff(c_2376, plain, (![V_323]: (ifeq2(accessible_world(skc6, V_323), true, male(V_323, skc9), true)=true))). % 14.54/6.12 tff(c_3617, plain, (![V_71]: (ifeq2(accessible_world(skc6, V_71), true, eventuality(V_71, skc7), true)=true))). % 14.54/6.12 tff(c_3709, plain, (ifeq2(agent(skc5, skf1(skc9), skc9), true, true, true)=true)). % 14.54/6.12 tff(c_2759, plain, (![V_341]: (ifeq2(accessible_world(skc6, V_341), true, forename(V_341, skc8), true)=true))). % 14.54/6.12 tff(c_1252, plain, (ifeq(tuple(true, nonhuman(skc5, skc9)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_3558, plain, (![V_128]: (ifeq2(accessible_world(skc6, V_128), true, relation(V_128, skc6), true)=true))). % 14.54/6.12 tff(c_2822, plain, (![V_347]: (ifeq2(accessible_world(skc5, V_347), true, nonexistent(V_347, skc7), true)=true))). % 14.54/6.12 tff(c_1660, plain, (![V_286]: (ifeq2(accessible_world(skc5, V_286), true, thing(V_286, skc7), true)=true))). % 14.54/6.12 tff(c_2756, plain, (![U_340]: (ifeq2(accessible_world(U_340, skc5), true, ifeq2(forename(U_340, skc8), true, true, true), true)=true))). % 14.54/6.12 tff(c_1607, plain, (![V_283]: (ifeq2(accessible_world(skc5, V_283), true, abstraction(V_283, skc6), true)=true))). % 14.54/6.12 tff(c_1830, plain, (![V_295]: (ifeq2(accessible_world(skc5, V_295), true, animate(V_295, skc9), true)=true))). % 14.54/6.12 tff(c_2207, plain, (![V_314]: (ifeq2(accessible_world(skc5, V_314), true, organism(V_314, skc9), true)=true))). % 14.54/6.12 tff(c_2118, plain, (![V_311]: (ifeq2(accessible_world(skc5, V_311), true, unisex(V_311, skc7), true)=true))). % 14.54/6.12 tff(c_1891, plain, (![V_298]: (ifeq2(accessible_world(skc5, V_298), true, specific(V_298, skc7), true)=true))). % 14.54/6.12 tff(c_1209, plain, (ifeq(tuple(true, male(skc5, skc7)), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_4539, plain, (![V_362]: (ifeq2(specific(skc5, skf1(V_362)), true, true, true)=true))). % 14.54/6.12 tff(c_4497, plain, (![W_422]: (ifeq2(specific(skc5, W_422), true, specific(skc6, W_422), true)=true))). % 14.54/6.12 tff(c_1759, plain, (![V_292]: (ifeq2(accessible_world(skc5, V_292), true, human(V_292, skc9), true)=true))). % 14.54/6.12 tff(c_2500, plain, (![V_329]: (ifeq2(accessible_world(skc5, V_329), true, relation(V_329, skc8), true)=true))). % 14.54/6.12 tff(c_2151, plain, (![V_92]: (ifeq2(accessible_world(skc6, V_92), true, man(V_92, skc9), true)=true))). % 14.54/6.12 tff(c_1582, plain, (![V_146]: (ifeq2(accessible_world(skc6, V_146), true, vincent_forename(V_146, skc8), true)=true))). % 14.54/6.12 tff(c_3491, plain, (![V_125]: (ifeq2(accessible_world(skc6, V_125), true, proposition(V_125, skc6), true)=true))). % 14.54/6.12 tff(c_4397, plain, (![V_343]: (ifeq2(smoke(skc5, skf1(V_343)), true, true, true)=true))). % 14.54/6.12 tff(c_4370, plain, (![W_414]: (ifeq2(smoke(skc5, W_414), true, smoke(skc6, W_414), true)=true))). % 14.54/6.12 tff(c_4358, plain, (ifeq2(accessible_world(skc6, skc6), true, true, true)=true)). % 14.54/6.12 tff(c_3525, plain, (![V_68]: (ifeq2(accessible_world(skc6, V_68), true, event(V_68, skc7), true)=true))). % 14.54/6.12 tff(c_1529, plain, (![V_279]: (ifeq2(accessible_world(skc5, V_279), true, human_person(V_279, skc9), true)=true))). % 14.54/6.12 tff(c_2377, plain, (![V_323]: (ifeq2(accessible_world(skc5, V_323), true, male(V_323, skc9), true)=true))). % 14.54/6.12 tff(c_2501, plain, (![V_329]: (ifeq2(accessible_world(skc5, V_329), true, relation(V_329, skc6), true)=true))). % 14.54/6.12 tff(c_1418, plain, (![V_270]: (ifeq2(accessible_world(skc5, V_270), true, eventuality(V_270, skc7), true)=true))). % 14.54/6.12 tff(c_1218, plain, (ifeq(tuple(unisex(skc5, skc9), true), tuple(true, true), a, b)=b)). % 14.54/6.12 tff(c_1963, plain, (![V_301]: (ifeq2(accessible_world(skc5, V_301), true, relname(V_301, skc8), true)=true))). % 14.54/6.12 tff(c_4070, plain, (![W_405]: (ifeq2(general(skc5, W_405), true, general(skc6, W_405), true)=true))). % 14.54/6.12 tff(c_2439, plain, (![U_325]: (ifeq2(think_believe_consider(U_325, skc7), true, ifeq2(accessible_world(U_325, skc5), true, true, true), true)=true))). % 14.54/6.12 tff(c_4167, plain, (of(skc6, skc8, skc9)=true)). % 14.54/6.12 tff(c_4132, plain, (theme(skc6, skc7, skc6)=true)). % 14.54/6.12 tff(c_4097, plain, (agent(skc6, skc7, skc9)=true)). % 14.54/6.12 tff(c_4040, plain, (singleton(skc6, skc6)=true)). % 14.54/6.12 tff(c_3961, plain, (ifeq2(entity(skc6, skc6), true, true, true)=true)). % 14.54/6.12 tff(c_3967, plain, (ifeq2(eventuality(skc6, skc6), true, true, true)=true)). % 14.54/6.12 tff(c_3998, plain, (ifeq2(accessible_world(skc6, skc5), true, true, true)=true)). % 14.54/6.12 tff(c_3978, plain, (unisex(skc6, skc6)=true)). % 14.54/6.12 tff(c_2867, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc5), true, ifeq2(event(U_351, skc7), true, true, true), true)=true))). % 14.54/6.12 tff(c_3940, plain, (thing(skc6, skc6)=true)). % 14.54/6.12 tff(c_3912, plain, (singleton(skc6, skc7)=true)). % 14.54/6.13 tff(c_3003, plain, (![W_364, X_365]: (ifeq2(of(skc5, W_364, X_365), true, of(skc6, W_364, X_365), true)=true))). % 14.54/6.13 tff(c_3871, plain, (nonhuman(skc6, skc6)=true)). % 14.54/6.13 tff(c_3840, plain, (general(skc6, skc6)=true)). % 14.54/6.13 tff(c_3742, plain, (ifeq2(abstraction(skc6, skc7), true, true, true)=true)). % 14.54/6.13 tff(c_3807, plain, (ifeq2(entity(skc6, skc7), true, true, true)=true)). % 14.54/6.13 tff(c_3549, plain, (ifeq2(relname(skc6, skc6), true, true, true)=true)). % 14.54/6.13 tff(c_3090, plain, (![W_371, X_372]: (ifeq2(theme(skc5, W_371, X_372), true, theme(skc6, W_371, X_372), true)=true))). % 14.54/6.13 tff(c_3783, plain, (specific(skc6, skc7)=true)). % 14.54/6.13 tff(c_3752, plain, (nonexistent(skc6, skc7)=true)). % 14.54/6.13 tff(c_3718, plain, (unisex(skc6, skc7)=true)). % 14.54/6.13 tff(c_2940, plain, (![W_358, X_359]: (ifeq2(agent(skc5, W_358, X_359), true, agent(skc6, W_358, X_359), true)=true))). % 14.54/6.13 tff(c_3668, plain, (thing(skc6, skc7)=true)). % 14.54/6.13 tff(c_3628, plain, (abstraction(skc6, skc6)=true)). % 14.54/6.13 tff(c_3521, plain, (ifeq2(smoke(skc6, skc7), true, true, true)=true)). % 14.54/6.13 tff(c_3565, plain, (eventuality(skc6, skc7)=true)). % 14.54/6.13 tff(c_2760, plain, (![V_341]: (ifeq2(accessible_world(skc5, V_341), true, forename(V_341, skc8), true)=true))). % 14.54/6.13 tff(c_3531, plain, (relation(skc6, skc6)=true)). % 14.54/6.13 tff(c_3497, plain, (event(skc6, skc7)=true)). % 14.54/6.13 tff(c_3444, plain, (proposition(skc6, skc6)=true)). % 14.54/6.13 tff(c_2870, plain, (![V_352]: (ifeq2(accessible_world(skc5, V_352), true, event(V_352, skc7), true)=true))). % 14.54/6.13 tff(c_2708, plain, (![V_338]: (ifeq2(accessible_world(skc5, V_338), true, proposition(V_338, skc6), true)=true))). % 14.54/6.13 tff(c_3307, plain, (![V_349]: (ifeq2(present(skc5, skf1(V_349)), true, true, true)=true))). % 14.54/6.13 tff(c_3388, plain, (agent(skc6, skf1(skc9), skc9)=true)). % 14.54/6.13 tff(c_3353, plain, (think_believe_consider(skc6, skc7)=true)). % 14.54/6.13 tff(c_2442, plain, (![W_326]: (ifeq2(think_believe_consider(skc5, W_326), true, think_believe_consider(skc6, W_326), true)=true))). % 14.54/6.13 tff(c_3316, plain, (present(skc6, skc7)=true)). % 14.54/6.13 tff(c_2573, plain, (![W_332]: (ifeq2(present(skc5, W_332), true, present(skc6, W_332), true)=true))). % 14.54/6.13 tff(c_3269, plain, (![V_390]: (singleton(skc6, skf1(V_390))=true))). % 14.54/6.13 tff(c_126, plain, (![X_167, V_169, Y_168, W_164, Z_166, U_165]: (ifeq3(theme(U_165, Y_168, W_164), true, ifeq3(theme(U_165, X_167, V_169), true, ifeq3(agent(U_165, Y_168, Z_166), true, ifeq3(agent(U_165, X_167, Z_166), true, ifeq3(think_believe_consider(U_165, Y_168), true, ifeq3(think_believe_consider(U_165, X_167), true, ifeq3(proposition(U_165, W_164), true, ifeq3(proposition(U_165, V_169), true, V_169, W_164), W_164), W_164), W_164), W_164), W_164), W_164), W_164)=W_164))). % 14.54/6.13 tff(c_3023, plain, (![V_367]: (ifeq2(entity(skc6, skf1(V_367)), true, true, true)=true))). % 14.54/6.13 tff(c_3123, plain, (![V_375]: (ifeq2(abstraction(skc6, skf1(V_375)), true, true, true)=true))). % 14.54/6.13 tff(c_3177, plain, (![V_380]: (nonexistent(skc6, skf1(V_380))=true))). % 14.54/6.13 tff(c_124, plain, (![U_160, W_161, X_162, V_163]: (ifeq3(of(U_160, W_161, X_162), true, ifeq3(of(U_160, V_163, X_162), true, ifeq3(forename(U_160, W_161), true, ifeq3(forename(U_160, V_163), true, ifeq3(entity(U_160, X_162), true, W_161, V_163), V_163), V_163), V_163), V_163)=V_163))). % 14.54/6.13 tff(c_3096, plain, (![V_374]: (unisex(skc6, skf1(V_374))=true))). % 14.54/6.13 tff(c_120, plain, (![U_152, W_153, X_154, V_155]: (ifeq2(theme(U_152, W_153, X_154), true, ifeq2(accessible_world(U_152, V_155), true, theme(V_155, W_153, X_154), true), true)=true))). % 14.54/6.13 tff(c_3036, plain, (![V_368]: (thing(skc6, skf1(V_368))=true))). % 14.54/6.13 tff(c_2979, plain, (![V_362]: (specific(skc6, skf1(V_362))=true))). % 14.54/6.13 tff(c_122, plain, (![U_156, W_157, X_158, V_159]: (ifeq2(of(U_156, W_157, X_158), true, ifeq2(accessible_world(U_156, V_159), true, of(V_159, W_157, X_158), true), true)=true))). % 14.54/6.13 tff(c_2916, plain, (![V_356]: (eventuality(skc6, skf1(V_356))=true))). % 14.54/6.13 tff(c_118, plain, (![U_148, W_149, X_150, V_151]: (ifeq2(agent(U_148, W_149, X_150), true, ifeq2(accessible_world(U_148, V_151), true, agent(V_151, W_149, X_150), true), true)=true))). % 14.54/6.13 tff(c_2876, plain, (![V_354]: (event(skc6, skf1(V_354))=true))). % 14.54/6.13 tff(c_64, plain, (![U_67, V_68, W_69]: (ifeq2(accessible_world(U_67, V_68), true, ifeq2(event(U_67, W_69), true, event(V_68, W_69), true), true)=true))). % 14.54/6.13 tff(c_2828, plain, (![V_349]: (present(skc6, skf1(V_349))=true))). % 14.54/6.13 tff(c_74, plain, (![U_82, V_83, W_84]: (ifeq2(accessible_world(U_82, V_83), true, ifeq2(nonexistent(U_82, W_84), true, nonexistent(V_83, W_84), true), true)=true))). % 14.54/6.13 tff(c_2776, plain, (![U_170]: (ifeq2(man(skc6, U_170), true, true, true)=true))). % 14.54/6.13 tff(c_2767, plain, (![V_343]: (smoke(skc6, skf1(V_343))=true))). % 14.54/6.13 tff(c_112, plain, (![U_139, V_140, W_141]: (ifeq2(accessible_world(U_139, V_140), true, ifeq2(forename(U_139, W_141), true, forename(V_140, W_141), true), true)=true))). % 14.54/6.13 tff(c_2712, plain, (singleton(skc6, skc9)=true)). % 14.54/6.13 tff(c_102, plain, (![U_124, V_125, W_126]: (ifeq2(accessible_world(U_124, V_125), true, ifeq2(proposition(U_124, W_126), true, proposition(V_125, W_126), true), true)=true))). % 14.54/6.13 tff(c_2541, plain, (ifeq2(abstraction(skc6, skc9), true, true, true)=true)). % 14.54/6.13 tff(c_2550, plain, (ifeq2(eventuality(skc6, skc9), true, true, true)=true)). % 14.54/6.13 tff(c_2653, plain, (specific(skc6, skc9)=true)). % 14.54/6.13 tff(c_70, plain, (![U_76, V_77, W_78]: (ifeq2(accessible_world(U_76, V_77), true, ifeq2(singleton(U_76, W_78), true, singleton(V_77, W_78), true), true)=true))). % 14.54/6.13 tff(c_2577, plain, (existent(skc6, skc9)=true)). % 14.54/6.13 tff(c_78, plain, (![U_88, W_89, V_90]: (ifeq2(present(U_88, W_89), true, ifeq2(accessible_world(U_88, V_90), true, present(V_90, W_89), true), true)=true))). % 14.54/6.13 tff(c_2523, plain, (thing(skc6, skc9)=true)). % 14.54/6.13 tff(c_2468, plain, (living(skc6, skc9)=true)). % 14.54/6.13 tff(c_104, plain, (![U_127, V_128, W_129]: (ifeq2(accessible_world(U_127, V_128), true, ifeq2(relation(U_127, W_129), true, relation(V_128, W_129), true), true)=true))). % 14.54/6.13 tff(c_2419, plain, (impartial(skc6, skc9)=true)). % 14.54/6.13 tff(c_100, plain, (![U_121, W_122, V_123]: (ifeq2(think_believe_consider(U_121, W_122), true, ifeq2(accessible_world(U_121, V_123), true, think_believe_consider(V_123, W_122), true), true)=true))). % 14.54/6.13 tff(c_2382, plain, (entity(skc6, skc9)=true)). % 14.54/6.13 tff(c_98, plain, (![U_118, V_119, W_120]: (ifeq2(accessible_world(U_118, V_119), true, ifeq2(male(U_118, W_120), true, male(V_119, W_120), true), true)=true))). % 14.54/6.13 tff(c_2330, plain, (animate(skc6, skc9)=true)). % 14.54/6.13 tff(c_62, plain, (![U_64, V_65, W_66]: (ifeq2(accessible_world(U_64, V_65), true, ifeq2(smoke(U_64, W_66), true, smoke(V_65, W_66), true), true)=true))). % 14.54/6.13 tff(c_2283, plain, (organism(skc6, skc9)=true)). % 14.54/6.13 tff(c_2252, plain, (human(skc6, skc9)=true)). % 14.54/6.13 tff(c_92, plain, (![U_109, V_110, W_111]: (ifeq2(accessible_world(U_109, V_110), true, ifeq2(living(U_109, W_111), true, living(V_110, W_111), true), true)=true))). % 14.54/6.13 tff(c_2211, plain, (male(skc6, skc9)=true)). % 14.54/6.13 tff(c_84, plain, (![U_97, V_98, W_99]: (ifeq2(accessible_world(U_97, V_98), true, ifeq2(organism(U_97, W_99), true, organism(V_98, W_99), true), true)=true))). % 14.54/6.13 tff(c_2157, plain, (human_person(skc6, skc9)=true)). % 14.54/6.13 tff(c_2076, plain, (man(skc6, skc9)=true)). % 14.54/6.13 tff(c_76, plain, (![U_85, V_86, W_87]: (ifeq2(accessible_world(U_85, V_86), true, ifeq2(unisex(U_85, W_87), true, unisex(V_86, W_87), true), true)=true))). % 14.54/6.13 tff(c_1715, plain, (![V_289]: (ifeq2(accessible_world(skc5, V_289), true, man(V_289, skc9), true)=true))). % 14.54/6.13 tff(c_88, plain, (![U_103, V_104, W_105]: (ifeq2(accessible_world(U_103, V_104), true, ifeq2(existent(U_103, W_105), true, existent(V_104, W_105), true), true)=true))). % 14.54/6.13 tff(c_1845, plain, (ifeq2(entity(skc6, skc8), true, true, true)=true)). % 14.54/6.13 tff(c_1851, plain, (ifeq2(eventuality(skc6, skc8), true, true, true)=true)). % 14.54/6.13 tff(c_2015, plain, (singleton(skc6, skc8)=true)). % 14.54/6.13 tff(c_86, plain, (![U_100, V_101, W_102]: (ifeq2(accessible_world(U_100, V_101), true, ifeq2(entity(U_100, W_102), true, entity(V_101, W_102), true), true)=true))). % 14.54/6.13 tff(c_1967, plain, (nonhuman(skc6, skc8)=true)). % 14.54/6.13 tff(c_114, plain, (![U_142, V_143, W_144]: (ifeq2(accessible_world(U_142, V_143), true, ifeq2(relname(U_142, W_144), true, relname(V_143, W_144), true), true)=true))). % 14.54/6.13 tff(c_1916, plain, (unisex(skc6, skc8)=true)). % 14.54/6.13 tff(c_1861, plain, (general(skc6, skc8)=true)). % 14.54/6.13 tff(c_72, plain, (![U_79, V_80, W_81]: (ifeq2(accessible_world(U_79, V_80), true, ifeq2(specific(U_79, W_81), true, specific(V_80, W_81), true), true)=true))). % 14.54/6.13 tff(c_1807, plain, (thing(skc6, skc8)=true)). % 14.54/6.13 tff(c_96, plain, (![U_115, V_116, W_117]: (ifeq2(accessible_world(U_115, V_116), true, ifeq2(animate(U_115, W_117), true, animate(V_116, W_117), true), true)=true))). % 14.54/6.13 tff(c_1734, plain, (ifeq2(proposition(skc6, skc8), true, true, true)=true)). % 14.54/6.13 tff(c_1763, plain, (abstraction(skc6, skc8)=true)). % 14.54/6.13 tff(c_94, plain, (![U_112, V_113, W_114]: (ifeq2(accessible_world(U_112, V_113), true, ifeq2(human(U_112, W_114), true, human(V_113, W_114), true), true)=true))). % 14.54/6.13 tff(c_1719, plain, (relation(skc6, skc8)=true)). % 14.54/6.13 tff(c_80, plain, (![U_91, V_92, W_93]: (ifeq2(accessible_world(U_91, V_92), true, ifeq2(man(U_91, W_93), true, man(V_92, W_93), true), true)=true))). % 14.54/6.13 tff(c_1678, plain, (relname(skc6, skc8)=true)). % 14.54/6.13 tff(c_1620, plain, (forename(skc6, skc8)=true)). % 14.54/6.13 tff(c_68, plain, (![U_73, V_74, W_75]: (ifeq2(accessible_world(U_73, V_74), true, ifeq2(thing(U_73, W_75), true, thing(V_74, W_75), true), true)=true))). % 14.54/6.13 tff(c_1551, plain, (ifeq2(accessible_world(skc5, skc5), true, true, true)=true)). % 14.54/6.13 tff(c_106, plain, (![U_130, V_131, W_132]: (ifeq2(accessible_world(U_130, V_131), true, ifeq2(abstraction(U_130, W_132), true, abstraction(V_131, W_132), true), true)=true))). % 14.54/6.13 tff(c_1557, plain, (vincent_forename(skc6, skc8)=true)). % 14.54/6.13 tff(c_1330, plain, (![V_264]: (ifeq2(accessible_world(skc5, V_264), true, vincent_forename(V_264, skc8), true)=true))). % 14.54/6.13 tff(c_1506, plain, (singleton(skc5, skc9)=true)). % 14.54/6.13 tff(c_82, plain, (![U_94, V_95, W_96]: (ifeq2(accessible_world(U_94, V_95), true, ifeq2(human_person(U_94, W_96), true, human_person(V_95, W_96), true), true)=true))). % 14.54/6.13 tff(c_1300, plain, (ifeq2(abstraction(skc5, skc9), true, true, true)=true)). % 14.54/6.13 tff(c_90, plain, (![U_106, V_107, W_108]: (ifeq2(accessible_world(U_106, V_107), true, ifeq2(impartial(U_106, W_108), true, impartial(V_107, W_108), true), true)=true))). % 14.54/6.13 tff(c_1229, plain, (ifeq2(entity(skc5, skc8), true, true, true)=true)). % 14.54/6.13 tff(c_1458, plain, (singleton(skc5, skc8)=true)). % 14.54/6.13 tff(c_110, plain, (![U_136, V_137, W_138]: (ifeq2(accessible_world(U_136, V_137), true, ifeq2(general(U_136, W_138), true, general(V_137, W_138), true), true)=true))). % 14.54/6.13 tff(c_1309, plain, (ifeq2(eventuality(skc5, skc9), true, true, true)=true)). % 14.54/6.13 tff(c_1235, plain, (ifeq2(eventuality(skc5, skc8), true, true, true)=true)). % 14.54/6.13 tff(c_1038, plain, (ifeq2(entity(skc5, skc6), true, true, true)=true)). % 14.54/6.13 tff(c_66, plain, (![U_70, V_71, W_72]: (ifeq2(accessible_world(U_70, V_71), true, ifeq2(eventuality(U_70, W_72), true, eventuality(V_71, W_72), true), true)=true))). % 14.54/6.13 tff(c_1381, plain, (existent(skc5, skc9)=true)). % 14.54/6.13 tff(c_108, plain, (![U_133, V_134, W_135]: (ifeq2(accessible_world(U_133, V_134), true, ifeq2(nonhuman(U_133, W_135), true, nonhuman(V_134, W_135), true), true)=true))). % 14.54/6.13 tff(c_1335, plain, (singleton(skc5, skc6)=true)). % 14.54/6.13 tff(c_116, plain, (![U_145, V_146, W_147]: (ifeq2(accessible_world(U_145, V_146), true, ifeq2(vincent_forename(U_145, W_147), true, vincent_forename(V_146, W_147), true), true)=true))). % 14.54/6.13 tff(c_1288, plain, (thing(skc5, skc9)=true)). % 14.54/6.13 tff(c_1264, plain, (general(skc5, skc8)=true)). % 14.54/6.13 tff(c_164, plain, (![U_181, V_182]: (ifeq(tuple(human(U_181, V_182), nonhuman(U_181, V_182)), tuple(true, true), a, b)=b))). % 14.54/6.13 tff(c_559, plain, (ifeq2(eventuality(skc5, skc6), true, true, true)=true)). % 14.54/6.13 tff(c_1195, plain, (thing(skc5, skc8)=true)). % 14.54/6.13 tff(c_160, plain, (![U_177, V_178]: (ifeq(tuple(unisex(U_177, V_178), male(U_177, V_178)), tuple(true, true), a, b)=b))). % 14.54/6.13 tff(c_1168, plain, (specific(skc5, skc9)=true)). % 14.54/6.13 tff(c_166, plain, (![U_183, V_184]: (ifeq(tuple(nonexistent(U_183, V_184), existent(U_183, V_184)), tuple(true, true), a, b)=b))). % 14.54/6.13 tff(c_1128, plain, (entity(skc5, skc9)=true)). % 14.54/6.13 tff(c_162, plain, (![U_179, V_180]: (ifeq(tuple(specific(U_179, V_180), general(U_179, V_180)), tuple(true, true), a, b)=b))). % 14.54/6.13 tff(c_1093, plain, (living(skc5, skc9)=true)). % 14.54/6.13 tff(c_986, plain, (ifeq2(entity(skc5, skc7), true, true, true)=true)). % 14.54/6.13 tff(c_158, plain, (![U_176]: (ifeq2(man(skc6, U_176), true, agent(skc6, skf1(U_176), U_176), true)=true))). % 14.54/6.13 tff(c_1060, plain, (singleton(skc5, skc7)=true)). % 14.54/6.13 tff(c_1023, plain, (thing(skc5, skc6)=true)). % 14.54/6.13 tff(c_995, plain, (impartial(skc5, skc9)=true)). % 14.54/6.13 tff(c_964, plain, (specific(skc5, skc7)=true)). % 14.54/6.14 tff(c_943, plain, (human(skc5, skc9)=true)). % 14.54/6.14 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 14.54/6.14 tff(c_912, plain, (animate(skc5, skc9)=true)). % 14.54/6.14 tff(c_26, plain, (![U_28, V_29]: (ifeq2(organism(U_28, V_29), true, entity(U_28, V_29), true)=true))). % 14.54/6.14 tff(c_875, plain, (organism(skc5, skc9)=true)). % 14.54/6.14 tff(c_845, plain, (human_person(skc5, skc9)=true)). % 14.54/6.14 tff(c_22, plain, (![U_24, V_25]: (ifeq2(man(U_24, V_25), true, human_person(U_24, V_25), true)=true))). % 14.54/6.14 tff(c_717, plain, (ifeq2(abstraction(skc5, skc7), true, true, true)=true)). % 14.54/6.14 tff(c_794, plain, (general(skc5, skc6)=true)). % 14.54/6.14 tff(c_48, plain, (![U_50, V_51]: (ifeq2(abstraction(U_50, V_51), true, thing(U_50, V_51), true)=true))). % 14.54/6.14 tff(c_767, plain, (thing(skc5, skc7)=true)). % 14.54/6.14 tff(c_28, plain, (![U_30, V_31]: (ifeq2(entity(U_30, V_31), true, thing(U_30, V_31), true)=true))). % 14.54/6.14 tff(c_739, plain, (nonexistent(skc5, skc7)=true)). % 14.54/6.14 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, general(U_54, V_55), true)=true))). % 14.54/6.14 tff(c_702, plain, (unisex(skc5, skc7)=true)). % 14.54/6.14 tff(c_672, plain, (eventuality(skc5, skc7)=true)). % 14.54/6.14 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 14.54/6.14 tff(c_638, plain, (ifeq2(smoke(skc5, skc7), true, true, true)=true)). % 14.54/6.14 tff(c_624, plain, (unisex(skc5, skc8)=true)). % 14.54/6.14 tff(c_8, plain, (![U_10, V_11]: (ifeq2(smoke(U_10, V_11), true, event(U_10, V_11), true)=true))). % 14.54/6.14 tff(c_603, plain, (nonhuman(skc5, skc8)=true)). % 14.54/6.14 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 14.54/6.14 tff(c_569, plain, (abstraction(skc5, skc8)=true)). % 14.54/6.14 tff(c_539, plain, (ifeq2(proposition(skc5, skc8), true, true, true)=true)). % 14.54/6.14 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 14.54/6.14 tff(c_517, plain, (ifeq2(relname(skc5, skc6), true, true, true)=true)). % 14.54/6.14 tff(c_524, plain, (relation(skc5, skc8)=true)). % 14.54/6.14 tff(c_58, plain, (![U_60, V_61]: (ifeq2(relname(U_60, V_61), true, relation(U_60, V_61), true)=true))). % 14.54/6.14 tff(c_490, plain, (unisex(skc5, skc6)=true)). % 14.54/6.14 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, unisex(U_56, V_57), true)=true))). % 14.54/6.14 tff(c_60, plain, (![U_62, V_63]: (ifeq2(vincent_forename(U_62, V_63), true, forename(U_62, V_63), true)=true))). % 14.54/6.14 tff(c_444, plain, (relname(skc5, skc8)=true)). % 14.54/6.14 tff(c_56, plain, (![U_58, V_59]: (ifeq2(forename(U_58, V_59), true, relname(U_58, V_59), true)=true))). % 14.54/6.14 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 14.54/6.14 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, existent(U_34, V_35), true)=true))). % 14.54/6.14 tff(c_399, plain, (nonhuman(skc5, skc6)=true)). % 14.54/6.14 tff(c_50, plain, (![U_52, V_53]: (ifeq2(abstraction(U_52, V_53), true, nonhuman(U_52, V_53), true)=true))). % 14.54/6.14 tff(c_24, plain, (![U_26, V_27]: (ifeq2(human_person(U_26, V_27), true, organism(U_26, V_27), true)=true))). % 14.54/6.14 tff(c_361, plain, (abstraction(skc5, skc6)=true)). % 14.54/6.14 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, specific(U_32, V_33), true)=true))). % 14.54/6.14 tff(c_330, plain, (relation(skc5, skc6)=true)). % 14.54/6.14 tff(c_44, plain, (![U_46, V_47]: (ifeq2(proposition(U_46, V_47), true, relation(U_46, V_47), true)=true))). % 14.54/6.14 tff(c_34, plain, (![U_36, V_37]: (ifeq2(organism(U_36, V_37), true, impartial(U_36, V_37), true)=true))). % 14.54/6.14 tff(c_46, plain, (![U_48, V_49]: (ifeq2(relation(U_48, V_49), true, abstraction(U_48, V_49), true)=true))). % 14.54/6.14 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 14.54/6.14 tff(c_278, plain, (male(skc5, skc9)=true)). % 14.54/6.14 tff(c_42, plain, (![U_44, V_45]: (ifeq2(man(U_44, V_45), true, male(U_44, V_45), true)=true))). % 14.54/6.14 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, animate(U_42, V_43), true)=true))). % 14.54/6.14 tff(c_38, plain, (![U_40, V_41]: (ifeq2(human_person(U_40, V_41), true, human(U_40, V_41), true)=true))). % 14.54/6.14 tff(c_36, plain, (![U_38, V_39]: (ifeq2(organism(U_38, V_39), true, living(U_38, V_39), true)=true))). % 14.54/6.14 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 14.54/6.14 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 14.54/6.14 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 14.54/6.14 tff(c_146, plain, (of(skc5, skc8, skc9)=true)). % 14.54/6.14 tff(c_148, plain, (agent(skc5, skc7, skc9)=true)). % 14.54/6.14 tff(c_150, plain, (theme(skc5, skc7, skc6)=true)). % 14.54/6.14 tff(c_130, plain, (man(skc5, skc9)=true)). % 14.54/6.14 tff(c_144, plain, (proposition(skc5, skc6)=true)). % 14.54/6.14 tff(c_142, plain, (accessible_world(skc5, skc6)=true)). % 14.54/6.14 tff(c_140, plain, (think_believe_consider(skc5, skc7)=true)). % 14.54/6.14 tff(c_138, plain, (present(skc5, skc7)=true)). % 14.54/6.14 tff(c_132, plain, (forename(skc5, skc8)=true)). % 14.54/6.14 tff(c_134, plain, (vincent_forename(skc5, skc8)=true)). % 14.54/6.14 tff(c_136, plain, (event(skc5, skc7)=true)). % 14.54/6.14 tff(c_128, plain, (actual_world(skc5)=true)). % 14.54/6.14 tff(c_168, plain, (b!=a)). % 14.54/6.14 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.54/6.14 %------------------------------------------------------------------------------