%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP225-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 : n014.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:40 PM UTC 2025 % Result : Satisfiable 16.35s 7.45s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP225-10 : TPTP v9.0.0. Released v7.3.0. % 0.11/0.12 % 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.12/0.33 % Computer : n014.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 09:30:49 EDT 2025 % 0.12/0.33 % CPUTime : % 16.35/7.45 % 16.35/7.45 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.35/7.45 % 16.35/7.45 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.35/7.46 %$ ifeq3 > ifeq2 > ifeq > be > theme > of > agent > vincent_forename > unisex > tuple > think_believe_consider > thing > state > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > jules_forename > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > #nlpp > skf1 > actual_world > true > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 > b > a % 16.35/7.46 % 16.35/7.46 %Foreground sorts: % 16.35/7.46 % 16.35/7.46 % 16.35/7.46 %Background operators: % 16.35/7.46 % 16.35/7.46 % 16.35/7.46 %Foreground operators: % 16.35/7.46 tff(agent, type, agent: ($i * $i * $i) > $i). % 16.35/7.46 tff(proposition, type, proposition: ($i * $i) > $i). % 16.35/7.46 tff(specific, type, specific: ($i * $i) > $i). % 16.35/7.46 tff(organism, type, organism: ($i * $i) > $i). % 16.35/7.46 tff(impartial, type, impartial: ($i * $i) > $i). % 16.35/7.46 tff(skc11, type, skc11: $i). % 16.35/7.46 tff(a, type, a: $i). % 16.35/7.46 tff(smoke, type, smoke: ($i * $i) > $i). % 16.35/7.46 tff(jules_forename, type, jules_forename: ($i * $i) > $i). % 16.35/7.46 tff(skc9, type, skc9: $i). % 16.35/7.46 tff(eventuality, type, eventuality: ($i * $i) > $i). % 16.35/7.46 tff(theme, type, theme: ($i * $i * $i) > $i). % 16.35/7.46 tff(state, type, state: ($i * $i) > $i). % 16.35/7.46 tff(tuple, type, tuple: ($i * $i) > $i). % 16.35/7.46 tff(human_person, type, human_person: ($i * $i) > $i). % 16.35/7.46 tff(skf1, type, skf1: $i > $i). % 16.35/7.46 tff(be, type, be: ($i * $i * $i * $i) > $i). % 16.35/7.46 tff(skc8, type, skc8: $i). % 16.35/7.46 tff(relname, type, relname: ($i * $i) > $i). % 16.35/7.46 tff(skc14, type, skc14: $i). % 16.35/7.46 tff(skc13, type, skc13: $i). % 16.35/7.46 tff(thing, type, thing: ($i * $i) > $i). % 16.35/7.46 tff(unisex, type, unisex: ($i * $i) > $i). % 16.35/7.46 tff(abstraction, type, abstraction: ($i * $i) > $i). % 16.35/7.46 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 16.35/7.46 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 16.35/7.46 tff(relation, type, relation: ($i * $i) > $i). % 16.35/7.46 tff(actual_world, type, actual_world: $i > $i). % 16.35/7.46 tff(of, type, of: ($i * $i * $i) > $i). % 16.35/7.46 tff(present, type, present: ($i * $i) > $i). % 16.35/7.46 tff(b, type, b: $i). % 16.35/7.46 tff(animate, type, animate: ($i * $i) > $i). % 16.35/7.46 tff(human, type, human: ($i * $i) > $i). % 16.35/7.46 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 16.35/7.46 tff(skc15, type, skc15: $i). % 16.35/7.46 tff(existent, type, existent: ($i * $i) > $i). % 16.35/7.46 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 16.35/7.46 tff(forename, type, forename: ($i * $i) > $i). % 16.35/7.46 tff(true, type, true: $i). % 16.35/7.46 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 16.35/7.46 tff(male, type, male: ($i * $i) > $i). % 16.35/7.46 tff(skc12, type, skc12: $i). % 16.35/7.46 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 16.35/7.46 tff(entity, type, entity: ($i * $i) > $i). % 16.35/7.46 tff(skc10, type, skc10: $i). % 16.35/7.46 tff(singleton, type, singleton: ($i * $i) > $i). % 16.35/7.46 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 16.35/7.46 tff(event, type, event: ($i * $i) > $i). % 16.35/7.46 tff(man, type, man: ($i * $i) > $i). % 16.35/7.46 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 16.35/7.46 tff(general, type, general: ($i * $i) > $i). % 16.35/7.46 tff(living, type, living: ($i * $i) > $i). % 16.35/7.46 % 16.35/7.46 %Saturated clause set: % 16.35/7.46 tff(c_15034, plain, (![W_964, V_966]: (ifeq3(theme(skc11, skf1(skc10), W_964), true, ifeq3(theme(skc11, skf1(skc10), V_966), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_964), true, ifeq3(proposition(skc11, V_966), true, V_966, W_964), W_964), W_964), W_964), W_964), W_964)=W_964))). % 16.35/7.46 tff(c_6042, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc11, Y_189, W_185), true, ifeq3(theme(skc11, skf1(skc10), V_190), true, ifeq3(agent(skc11, Y_189, skc10), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.35/7.47 tff(c_6041, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc11, skf1(skc10), W_185), true, ifeq3(theme(skc11, X_188, V_190), true, ifeq3(agent(skc11, X_188, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.35/7.47 tff(c_14688, plain, (![X_944, V_945]: (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, X_944, V_945), true, ifeq3(agent(skc11, X_944, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, X_944), true, ifeq3(proposition(skc11, V_945), true, V_945, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_14418, plain, (![Y_924, W_925]: (ifeq3(theme(skc11, Y_924, W_925), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(agent(skc11, Y_924, skc10), true, ifeq3(think_believe_consider(skc11, Y_924), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_925), true, skc11, W_925), W_925), W_925), W_925), W_925), W_925)=W_925))). % 16.35/7.47 tff(c_14877, plain, (![V_958]: (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skf1(skc10), V_958), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, V_958), true, V_958, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_14689, plain, (![Y_943, V_945]: (ifeq3(theme(skc11, Y_943, skc11), true, ifeq3(theme(skc11, skf1(skc10), V_945), true, ifeq3(agent(skc11, Y_943, skc10), true, ifeq3(think_believe_consider(skc11, Y_943), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, V_945), true, V_945, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_4597, plain, (![Y_189, W_185, V_190, Z_187]: (ifeq3(theme(skc11, Y_189, W_185), true, ifeq3(theme(skc11, skc12, V_190), true, ifeq3(agent(skc11, Y_189, Z_187), true, ifeq3(agent(skc11, skc12, Z_187), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.35/7.47 tff(c_14776, plain, (![W_950]: (ifeq3(theme(skc11, skf1(skc10), W_950), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_950), true, skc11, W_950), W_950), W_950), W_950), W_950)=W_950))). % 16.35/7.47 tff(c_14417, plain, (![W_925, X_926]: (ifeq3(theme(skc11, skf1(skc10), W_925), true, ifeq3(theme(skc11, X_926, skc11), true, ifeq3(agent(skc11, X_926, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, X_926), true, ifeq3(proposition(skc11, W_925), true, skc11, W_925), W_925), W_925), W_925), W_925), W_925)=W_925))). % 16.35/7.47 tff(c_14695, plain, (![Y_943, V_945, Z_946]: (ifeq3(theme(skc11, Y_943, skc11), true, ifeq3(theme(skc11, skc12, V_945), true, ifeq3(agent(skc11, Y_943, Z_946), true, ifeq3(agent(skc11, skc12, Z_946), true, ifeq3(think_believe_consider(skc11, Y_943), true, ifeq3(proposition(skc11, V_945), true, V_945, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_4383, plain, (![Y_189, X_188, V_190, Z_187]: (ifeq3(theme(skc11, Y_189, skc11), true, ifeq3(theme(skc11, X_188, V_190), true, ifeq3(agent(skc11, Y_189, Z_187), true, ifeq3(agent(skc11, X_188, Z_187), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, V_190), true, V_190, skc11), skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_14511, plain, (![W_931, V_933, Z_934]: (ifeq3(theme(skc11, skc12, W_931), true, ifeq3(theme(skc11, skc12, V_933), true, ifeq3(agent(skc11, skc12, Z_934), true, ifeq3(agent(skc11, skc12, Z_934), true, ifeq3(proposition(skc11, W_931), true, ifeq3(proposition(skc11, V_933), true, V_933, W_931), W_931), W_931), W_931), W_931), W_931)=W_931))). % 16.35/7.47 tff(c_14546, plain, (![Y_935]: (ifeq3(theme(skc11, Y_935, skc11), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(agent(skc11, Y_935, skc10), true, ifeq3(think_believe_consider(skc11, Y_935), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_14572, plain, (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11), skc11), skc11)=skc11)). % 16.35/7.47 tff(c_14545, plain, (![X_936]: (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, X_936, skc11), true, ifeq3(agent(skc11, X_936, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, X_936), true, skc11, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_14425, plain, (![Y_924, X_926, Z_927]: (ifeq3(theme(skc11, Y_924, skc11), true, ifeq3(theme(skc11, X_926, skc11), true, ifeq3(agent(skc11, Y_924, Z_927), true, ifeq3(agent(skc11, X_926, Z_927), true, ifeq3(think_believe_consider(skc11, Y_924), true, ifeq3(think_believe_consider(skc11, X_926), true, skc11, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.35/7.47 tff(c_4596, plain, (![W_185, X_188, V_190, Z_187]: (ifeq3(theme(skc11, skc12, W_185), true, ifeq3(theme(skc11, X_188, V_190), true, ifeq3(agent(skc11, skc12, Z_187), true, ifeq3(agent(skc11, X_188, Z_187), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.35/7.47 tff(c_14423, plain, (![W_925, X_926, Z_927]: (ifeq3(theme(skc11, skc12, W_925), true, ifeq3(theme(skc11, X_926, skc11), true, ifeq3(agent(skc11, skc12, Z_927), true, ifeq3(agent(skc11, X_926, Z_927), true, ifeq3(think_believe_consider(skc11, X_926), true, ifeq3(proposition(skc11, W_925), true, skc11, W_925), W_925), W_925), W_925), W_925), W_925)=W_925))). % 16.35/7.47 tff(c_4384, plain, (![Y_189, W_185, X_188, Z_187]: (ifeq3(theme(skc11, Y_189, W_185), true, ifeq3(theme(skc11, X_188, skc11), true, ifeq3(agent(skc11, Y_189, Z_187), true, ifeq3(agent(skc11, X_188, Z_187), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, W_185), true, skc11, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.35/7.47 tff(c_11295, plain, (![W_730, V_731, Z_732]: (ifeq3(theme(skc8, skc12, W_730), true, ifeq3(theme(skc8, skc12, V_731), true, ifeq3(agent(skc8, skc12, Z_732), true, ifeq3(agent(skc8, skc12, Z_732), true, ifeq3(proposition(skc8, W_730), true, ifeq3(proposition(skc8, V_731), true, V_731, W_730), W_730), W_730), W_730), W_730), W_730)=W_730))). % 16.35/7.47 tff(c_14220, plain, (![W_911, V_912]: (ifeq3(theme(skc11, skf1(skc10), W_911), true, ifeq3(theme(skc11, skc12, V_912), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_911), true, ifeq3(proposition(skc11, V_912), true, V_912, W_911), W_911), W_911), W_911), W_911)=W_911))). % 16.47/7.47 tff(c_14303, plain, (![V_917]: (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skc12, V_917), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, V_917), true, V_917, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.47 tff(c_14225, plain, (![Y_910, V_912]: (ifeq3(theme(skc11, Y_910, skc11), true, ifeq3(theme(skc11, skc12, V_912), true, ifeq3(agent(skc11, Y_910, skc10), true, ifeq3(think_believe_consider(skc11, Y_910), true, ifeq3(proposition(skc11, V_912), true, V_912, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.47 tff(c_11839, plain, (![Y_764, X_765, Z_767]: (ifeq3(theme(skc8, Y_764, skc11), true, ifeq3(theme(skc8, X_765, skc11), true, ifeq3(agent(skc8, Y_764, Z_767), true, ifeq3(agent(skc8, X_765, Z_767), true, ifeq3(think_believe_consider(skc8, Y_764), true, ifeq3(think_believe_consider(skc8, X_765), true, skc11, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.47 tff(c_5638, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc11, Y_189, W_185), true, ifeq3(theme(skc11, skc12, V_190), true, ifeq3(agent(skc11, Y_189, skc10), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.47/7.47 tff(c_14005, plain, (![W_897, V_899]: (ifeq3(theme(skc11, skc12, W_897), true, ifeq3(theme(skc11, skf1(skc10), V_899), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_897), true, ifeq3(proposition(skc11, V_899), true, V_899, W_897), W_897), W_897), W_897), W_897)=W_897))). % 16.47/7.47 tff(c_14075, plain, (![W_902]: (ifeq3(theme(skc11, skc12, W_902), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_902), true, skc11, W_902), W_902), W_902), W_902)=W_902))). % 16.47/7.47 tff(c_11296, plain, (![Y_729, V_731, Z_732]: (ifeq3(theme(skc8, Y_729, skc11), true, ifeq3(theme(skc8, skc12, V_731), true, ifeq3(agent(skc8, Y_729, Z_732), true, ifeq3(agent(skc8, skc12, Z_732), true, ifeq3(think_believe_consider(skc8, Y_729), true, ifeq3(proposition(skc8, V_731), true, V_731, skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.47 tff(c_14011, plain, (![W_897, X_898]: (ifeq3(theme(skc11, skc12, W_897), true, ifeq3(theme(skc11, X_898, skc11), true, ifeq3(agent(skc11, X_898, skc10), true, ifeq3(think_believe_consider(skc11, X_898), true, ifeq3(proposition(skc11, W_897), true, skc11, W_897), W_897), W_897), W_897), W_897)=W_897))). % 16.47/7.47 tff(c_14006, plain, (![W_897, V_899]: (ifeq3(theme(skc11, skc12, W_897), true, ifeq3(theme(skc11, skc12, V_899), true, ifeq3(proposition(skc11, W_897), true, ifeq3(proposition(skc11, V_899), true, V_899, W_897), W_897), W_897), W_897)=W_897))). % 16.47/7.48 tff(c_5637, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc11, skc12, W_185), true, ifeq3(theme(skc11, X_188, V_190), true, ifeq3(agent(skc11, X_188, skc10), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, W_185), true, ifeq3(proposition(skc11, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.47/7.48 tff(c_3860, plain, (![Y_418, W_417, V_416]: (ifeq3(theme(skc8, Y_418, W_417), true, ifeq3(theme(skc8, skc12, V_416), true, ifeq3(agent(skc8, Y_418, skc10), true, ifeq3(think_believe_consider(skc8, Y_418), true, ifeq3(proposition(skc8, W_417), true, ifeq3(proposition(skc8, V_416), true, V_416, W_417), W_417), W_417), W_417), W_417), W_417)=W_417))). % 16.47/7.48 tff(c_11635, plain, (![W_752, X_753, V_754]: (ifeq3(theme(skc8, skc12, W_752), true, ifeq3(theme(skc8, X_753, V_754), true, ifeq3(agent(skc8, X_753, skc10), true, ifeq3(think_believe_consider(skc8, X_753), true, ifeq3(proposition(skc8, W_752), true, ifeq3(proposition(skc8, V_754), true, V_754, W_752), W_752), W_752), W_752), W_752), W_752)=W_752))). % 16.47/7.48 tff(c_11834, plain, (![Y_764, V_766]: (ifeq3(theme(skc8, Y_764, skc11), true, ifeq3(theme(skc8, skc12, V_766), true, ifeq3(agent(skc8, Y_764, skc10), true, ifeq3(think_believe_consider(skc8, Y_764), true, ifeq3(proposition(skc8, V_766), true, V_766, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13689, plain, (![Y_878, Z_880]: (ifeq3(theme(skc11, Y_878, skc11), true, ifeq3(agent(skc11, Y_878, Z_880), true, ifeq3(agent(skc11, skc12, Z_880), true, ifeq3(think_believe_consider(skc11, Y_878), true, skc11, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13688, plain, (![W_879, Z_880]: (ifeq3(theme(skc11, skc12, W_879), true, ifeq3(agent(skc11, skc12, Z_880), true, ifeq3(agent(skc11, skc12, Z_880), true, ifeq3(proposition(skc11, W_879), true, skc11, W_879), W_879), W_879), W_879)=W_879))). % 16.47/7.48 tff(c_13686, plain, (![Y_878, W_879]: (ifeq3(theme(skc11, Y_878, W_879), true, ifeq3(agent(skc11, Y_878, skc10), true, ifeq3(think_believe_consider(skc11, Y_878), true, ifeq3(proposition(skc11, W_879), true, skc11, W_879), W_879), W_879), W_879)=W_879))). % 16.47/7.48 tff(c_13684, plain, (![W_879]: (ifeq3(theme(skc11, skf1(skc10), W_879), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, W_879), true, skc11, W_879), W_879), W_879)=W_879))). % 16.47/7.48 tff(c_13685, plain, (![W_879]: (ifeq3(theme(skc11, skc12, W_879), true, ifeq3(proposition(skc11, W_879), true, skc11, W_879), W_879)=W_879))). % 16.47/7.48 tff(c_5544, plain, (![Y_189, W_185, Z_187]: (ifeq3(theme(skc11, Y_189, W_185), true, ifeq3(agent(skc11, Y_189, Z_187), true, ifeq3(agent(skc11, skc12, Z_187), true, ifeq3(think_believe_consider(skc11, Y_189), true, ifeq3(proposition(skc11, W_185), true, skc11, W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.47/7.48 tff(c_13458, plain, (![X_862, Z_864]: (ifeq3(theme(skc11, X_862, skc11), true, ifeq3(agent(skc11, skc12, Z_864), true, ifeq3(agent(skc11, X_862, Z_864), true, ifeq3(think_believe_consider(skc11, X_862), true, skc11, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13457, plain, (![V_863, Z_864]: (ifeq3(theme(skc11, skc12, V_863), true, ifeq3(agent(skc11, skc12, Z_864), true, ifeq3(agent(skc11, skc12, Z_864), true, ifeq3(proposition(skc11, V_863), true, V_863, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13530, plain, (![X_868]: (ifeq3(theme(skc11, X_868, skc11), true, ifeq3(agent(skc11, X_868, skc10), true, ifeq3(think_believe_consider(skc11, X_868), true, skc11, skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_11641, plain, (![W_752, X_753, Z_755]: (ifeq3(theme(skc8, skc12, W_752), true, ifeq3(theme(skc8, X_753, skc11), true, ifeq3(agent(skc8, skc12, Z_755), true, ifeq3(agent(skc8, X_753, Z_755), true, ifeq3(think_believe_consider(skc8, X_753), true, ifeq3(proposition(skc8, W_752), true, skc11, W_752), W_752), W_752), W_752), W_752), W_752)=W_752))). % 16.47/7.48 tff(c_13454, plain, (![X_862, V_863]: (ifeq3(theme(skc11, X_862, V_863), true, ifeq3(agent(skc11, X_862, skc10), true, ifeq3(think_believe_consider(skc11, X_862), true, ifeq3(proposition(skc11, V_863), true, V_863, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13499, plain, (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11)=skc11)). % 16.47/7.48 tff(c_13453, plain, (![V_863]: (ifeq3(theme(skc11, skf1(skc10), V_863), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, V_863), true, V_863, skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13456, plain, (![Z_864]: (ifeq3(agent(skc11, skc12, Z_864), true, ifeq3(agent(skc11, skc12, Z_864), true, skc11, skc11), skc11)=skc11))). % 16.47/7.48 tff(c_13455, plain, (![V_863]: (ifeq3(theme(skc11, skc12, V_863), true, ifeq3(proposition(skc11, V_863), true, V_863, skc11), skc11)=skc11))). % 16.47/7.48 tff(c_5543, plain, (![X_188, V_190, Z_187]: (ifeq3(theme(skc11, X_188, V_190), true, ifeq3(agent(skc11, skc12, Z_187), true, ifeq3(agent(skc11, X_188, Z_187), true, ifeq3(think_believe_consider(skc11, X_188), true, ifeq3(proposition(skc11, V_190), true, V_190, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_11493, plain, (![W_743, X_744]: (ifeq3(theme(skc8, skc12, W_743), true, ifeq3(theme(skc8, X_744, skc11), true, ifeq3(agent(skc8, X_744, skc10), true, ifeq3(think_believe_consider(skc8, X_744), true, ifeq3(proposition(skc8, W_743), true, skc11, W_743), W_743), W_743), W_743), W_743)=W_743))). % 16.47/7.48 tff(c_3747, plain, (![W_410, V_412]: (ifeq3(of(skc11, W_410, skc10), true, ifeq3(of(skc11, V_412, skc10), true, ifeq3(forename(skc11, W_410), true, ifeq3(forename(skc11, V_412), true, W_410, V_412), V_412), V_412), V_412)=V_412))). % 16.47/7.48 tff(c_3750, plain, (![W_410, V_412]: (ifeq3(of(skc8, W_410, skc10), true, ifeq3(of(skc8, V_412, skc10), true, ifeq3(forename(skc8, W_410), true, ifeq3(forename(skc8, V_412), true, W_410, V_412), V_412), V_412), V_412)=V_412))). % 16.47/7.48 tff(c_13299, plain, (![X_411, V_412]: (ifeq3(of(skc11, skc13, X_411), true, ifeq3(of(skc11, V_412, X_411), true, ifeq3(forename(skc11, V_412), true, ifeq3(entity(skc11, X_411), true, skc13, V_412), V_412), V_412), V_412)=V_412))). % 16.47/7.48 tff(c_13278, plain, (![X_852]: (ifeq3(of(skc11, skc13, X_852), true, ifeq3(of(skc11, skc13, X_852), true, ifeq3(entity(skc11, X_852), true, skc13, skc13), skc13), skc13)=skc13))). % 16.47/7.48 tff(c_13256, plain, (![W_410, X_411]: (ifeq3(of(skc11, W_410, X_411), true, ifeq3(of(skc11, skc13, X_411), true, ifeq3(forename(skc11, W_410), true, ifeq3(entity(skc11, X_411), true, W_410, skc13), skc13), skc13), skc13)=skc13))). % 16.47/7.48 tff(c_11833, plain, (![X_765, V_766]: (ifeq3(theme(skc8, X_765, V_766), true, ifeq3(agent(skc8, X_765, skc10), true, ifeq3(think_believe_consider(skc8, X_765), true, ifeq3(proposition(skc8, V_766), true, V_766, skc11), skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_11636, plain, (![W_752, V_754]: (ifeq3(theme(skc8, skc12, W_752), true, ifeq3(theme(skc8, skc12, V_754), true, ifeq3(proposition(skc8, W_752), true, ifeq3(proposition(skc8, V_754), true, V_754, W_752), W_752), W_752), W_752)=W_752))). % 16.47/7.48 tff(c_11112, plain, (![Y_718, W_719]: (ifeq3(theme(skc8, Y_718, W_719), true, ifeq3(agent(skc8, Y_718, skc10), true, ifeq3(think_believe_consider(skc8, Y_718), true, ifeq3(proposition(skc8, W_719), true, skc11, W_719), W_719), W_719), W_719)=W_719))). % 16.47/7.48 tff(c_12778, plain, (![X_819]: (ifeq3(theme(skc8, X_819, skc11), true, ifeq3(agent(skc8, X_819, skc10), true, ifeq3(think_believe_consider(skc8, X_819), true, skc11, skc11), skc11), skc11)=skc11))). % 16.47/7.48 tff(c_6035, plain, (![U_168]: (ifeq2(agent(U_168, skf1(skc10), skc10), true, ifeq2(accessible_world(U_168, skc11), true, true, true), true)=true))). % 16.47/7.48 tff(c_13098, plain, (![V_841]: (ifeq2(accessible_world(skc11, V_841), true, agent(V_841, skf1(skc10), skc10), true)=true))). % 16.47/7.48 tff(c_7226, plain, (![U_177]: (ifeq2(be(U_177, skc9, skc10, skc10), true, ifeq2(accessible_world(U_177, skc11), true, true, true), true)=true))). % 16.47/7.48 tff(c_13032, plain, (![V_838]: (ifeq2(accessible_world(skc11, V_838), true, be(V_838, skc9, skc10, skc10), true)=true))). % 16.47/7.48 tff(c_3659, plain, (![U_405]: (ifeq2(be(U_405, skc9, skc10, skc10), true, ifeq2(accessible_world(U_405, skc8), true, true, true), true)=true))). % 16.51/7.48 tff(c_12958, plain, (![V_835]: (ifeq2(accessible_world(skc8, V_835), true, be(V_835, skc9, skc10, skc10), true)=true))). % 16.51/7.48 tff(c_11836, plain, (![Y_764, Z_767]: (ifeq3(theme(skc8, Y_764, skc11), true, ifeq3(agent(skc8, Y_764, Z_767), true, ifeq3(agent(skc8, skc12, Z_767), true, ifeq3(think_believe_consider(skc8, Y_764), true, skc11, skc11), skc11), skc11), skc11)=skc11))). % 16.51/7.48 tff(c_5843, plain, (![U_83, V_456]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skf1(V_456)), true, true, true), true)=true))). % 16.51/7.48 tff(c_3898, plain, (![U_92, V_424]: (ifeq2(accessible_world(U_92, skc11), true, ifeq2(unisex(U_92, skf1(V_424)), true, true, true), true)=true))). % 16.51/7.48 tff(c_3938, plain, (![U_89, V_426]: (ifeq2(accessible_world(U_89, skc11), true, ifeq2(nonexistent(U_89, skf1(V_426)), true, true, true), true)=true))). % 16.51/7.48 tff(c_5767, plain, (![U_80, V_451]: (ifeq2(accessible_world(U_80, skc11), true, ifeq2(thing(U_80, skf1(V_451)), true, true, true), true)=true))). % 16.51/7.48 tff(c_3989, plain, (![U_86, V_429]: (ifeq2(accessible_world(U_86, skc11), true, ifeq2(specific(U_86, skf1(V_429)), true, true, true), true)=true))). % 16.51/7.48 tff(c_12800, plain, (![W_182]: (ifeq3(of(skc11, W_182, skc10), true, ifeq3(forename(skc11, W_182), true, W_182, skc13), skc13)=skc13))). % 16.51/7.48 tff(c_5672, plain, (![V_184]: (ifeq3(of(skc11, V_184, skc10), true, ifeq3(forename(skc11, V_184), true, skc13, V_184), V_184)=V_184))). % 16.51/7.48 tff(c_11495, plain, (![X_744, Z_745]: (ifeq3(theme(skc8, X_744, skc11), true, ifeq3(agent(skc8, skc12, Z_745), true, ifeq3(agent(skc8, X_744, Z_745), true, ifeq3(think_believe_consider(skc8, X_744), true, skc11, skc11), skc11), skc11), skc11)=skc11))). % 16.51/7.48 tff(c_3800, plain, (![U_77, V_415]: (ifeq2(accessible_world(U_77, skc11), true, ifeq2(eventuality(U_77, skf1(V_415)), true, true, true), true)=true))). % 16.51/7.48 tff(c_12709, plain, (![W_410]: (ifeq3(of(skc8, W_410, skc10), true, ifeq3(forename(skc8, W_410), true, W_410, skc13), skc13)=skc13))). % 16.51/7.48 tff(c_10262, plain, (![V_677]: (ifeq3(of(skc8, V_677, skc10), true, ifeq3(forename(skc8, V_677), true, skc13, V_677), V_677)=V_677))). % 16.51/7.48 tff(c_11638, plain, (![W_752, Z_755]: (ifeq3(theme(skc8, skc12, W_752), true, ifeq3(agent(skc8, skc12, Z_755), true, ifeq3(agent(skc8, skc12, Z_755), true, ifeq3(proposition(skc8, W_752), true, skc11, W_752), W_752), W_752), W_752)=W_752))). % 16.51/7.49 tff(c_3771, plain, (![U_152, V_413]: (ifeq2(present(U_152, skf1(V_413)), true, ifeq2(accessible_world(U_152, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_12607, plain, (![V_807, V_808]: (ifeq2(accessible_world(skc11, V_807), true, present(V_807, skf1(V_808)), true)=true))). % 16.51/7.49 tff(c_3610, plain, (![U_95, V_399]: (ifeq2(accessible_world(U_95, skc11), true, ifeq2(event(U_95, skf1(V_399)), true, true, true), true)=true))). % 16.51/7.49 tff(c_3678, plain, (![U_149, V_407]: (ifeq2(accessible_world(U_149, skc11), true, ifeq2(smoke(U_149, skf1(V_407)), true, true, true), true)=true))). % 16.51/7.49 tff(c_12502, plain, (![V_799]: (ifeq2(accessible_world(skc11, V_799), true, agent(V_799, skc12, skc10), true)=true))). % 16.51/7.49 tff(c_10982, plain, (![V_710, Z_711]: (ifeq3(theme(skc8, skc12, V_710), true, ifeq3(agent(skc8, skc12, Z_711), true, ifeq3(agent(skc8, skc12, Z_711), true, ifeq3(proposition(skc8, V_710), true, V_710, skc11), skc11), skc11), skc11)=skc11))). % 16.51/7.49 tff(c_5668, plain, (![U_164]: (ifeq2(of(U_164, skc13, skc10), true, ifeq2(accessible_world(U_164, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_5633, plain, (![U_168]: (ifeq2(agent(U_168, skc12, skc10), true, ifeq2(accessible_world(U_168, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_12412, plain, (![V_795]: (ifeq2(accessible_world(skc11, V_795), true, of(V_795, skc13, skc10), true)=true))). % 16.51/7.49 tff(c_12376, plain, (![V_793]: (ifeq2(accessible_world(skc11, V_793), true, theme(V_793, skc12, skc11), true)=true))). % 16.51/7.49 tff(c_5539, plain, (![U_172]: (ifeq2(theme(U_172, skc12, skc11), true, ifeq2(accessible_world(U_172, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_11111, plain, (![W_719]: (ifeq3(theme(skc8, skc12, W_719), true, ifeq3(proposition(skc8, W_719), true, skc11, W_719), W_719)=W_719))). % 16.51/7.49 tff(c_3543, plain, (![U_390]: (ifeq2(of(U_390, skc13, skc10), true, ifeq2(accessible_world(U_390, skc8), true, true, true), true)=true))). % 16.51/7.49 tff(c_12242, plain, (![V_788]: (ifeq2(accessible_world(skc8, V_788), true, of(V_788, skc13, skc10), true)=true))). % 16.51/7.49 tff(c_12217, plain, (![X_676]: (ifeq3(of(skc8, skc13, X_676), true, ifeq3(of(skc8, skc13, X_676), true, ifeq3(entity(skc8, X_676), true, skc13, skc13), skc13), skc13)=skc13))). % 16.51/7.49 tff(c_10980, plain, (![V_710]: (ifeq3(theme(skc8, skc12, V_710), true, ifeq3(proposition(skc8, V_710), true, V_710, skc11), skc11)=skc11))). % 16.51/7.49 tff(c_12156, plain, (![V_784]: (ifeq2(accessible_world(skc8, V_784), true, agent(V_784, skc12, skc10), true)=true))). % 16.51/7.49 tff(c_3478, plain, (![U_386]: (ifeq2(agent(U_386, skc12, skc10), true, ifeq2(accessible_world(U_386, skc8), true, true, true), true)=true))). % 16.51/7.49 tff(c_3558, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_12087, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_12063, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc11), true, ifeq2(thing(U_368, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3493, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc11), true, ifeq2(specific(U_86, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_5285, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_3384, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc11), true, ifeq2(existent(U_110, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_11985, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc11), true, ifeq2(nonhuman(U_140, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_10981, plain, (![Z_711]: (ifeq3(agent(skc8, skc12, Z_711), true, ifeq3(agent(skc8, skc12, Z_711), true, skc11, skc11), skc11)=skc11))). % 16.51/7.49 tff(c_11950, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc11), true, ifeq2(general(U_143, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_11930, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc11), true, ifeq2(unisex(U_92, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3439, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc11), true, ifeq2(thing(U_80, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2191, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc8), true, ifeq2(singleton(U_83, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2298, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc8), true, ifeq2(singleton(U_83, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_5023, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc11), true, ifeq2(nonhuman(U_140, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_11840, plain, (![U_358]: (ifeq2(accessible_world(U_358, skc11), true, ifeq2(abstraction(U_358, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3865, plain, (![Y_418, X_421, V_416, Z_420]: (ifeq3(theme(skc8, Y_418, skc11), true, ifeq3(theme(skc8, X_421, V_416), true, ifeq3(agent(skc8, Y_418, Z_420), true, ifeq3(agent(skc8, X_421, Z_420), true, ifeq3(think_believe_consider(skc8, Y_418), true, ifeq3(think_believe_consider(skc8, X_421), true, ifeq3(proposition(skc8, V_416), true, V_416, skc11), skc11), skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.51/7.49 tff(c_4938, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc11), true, ifeq2(unisex(U_92, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_5134, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_5059, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc11), true, ifeq2(general(U_143, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_3287, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc11), true, ifeq2(living(U_116, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_4976, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc11), true, ifeq2(thing(U_80, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_5163, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc11), true, ifeq2(singleton(U_83, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_3339, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc11), true, ifeq2(impartial(U_113, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_3250, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc11), true, ifeq2(entity(U_107, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_3863, plain, (![W_417, X_421, V_416, Z_420]: (ifeq3(theme(skc8, skc12, W_417), true, ifeq3(theme(skc8, X_421, V_416), true, ifeq3(agent(skc8, skc12, Z_420), true, ifeq3(agent(skc8, X_421, Z_420), true, ifeq3(think_believe_consider(skc8, X_421), true, ifeq3(proposition(skc8, W_417), true, ifeq3(proposition(skc8, V_416), true, V_416, W_417), W_417), W_417), W_417), W_417), W_417), W_417)=W_417))). % 16.51/7.49 tff(c_3081, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc8), true, ifeq2(thing(U_368, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_3075, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc8), true, ifeq2(thing(U_368, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_11548, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc8), true, ifeq2(nonhuman(U_315, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3016, plain, (![U_365]: (ifeq2(accessible_world(U_365, skc8), true, ifeq2(existent(U_365, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2689, plain, (![U_349]: (ifeq2(accessible_world(U_349, skc8), true, ifeq2(specific(U_349, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_11500, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(unisex(U_324, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3866, plain, (![Y_418, W_417, X_421, Z_420]: (ifeq3(theme(skc8, Y_418, W_417), true, ifeq3(theme(skc8, X_421, skc11), true, ifeq3(agent(skc8, Y_418, Z_420), true, ifeq3(agent(skc8, X_421, Z_420), true, ifeq3(think_believe_consider(skc8, Y_418), true, ifeq3(think_believe_consider(skc8, X_421), true, ifeq3(proposition(skc8, W_417), true, skc11, W_417), W_417), W_417), W_417), W_417), W_417), W_417)=W_417))). % 16.51/7.49 tff(c_11447, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc8), true, ifeq2(general(U_334, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_2111, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc8), true, ifeq2(singleton(U_318, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_4622, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc11), true, ifeq2(nonexistent(U_89, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_4242, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc11), true, ifeq2(specific(U_86, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_3306, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc11), true, ifeq2(human(U_377, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_4844, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc11), true, ifeq2(thing(U_80, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_11336, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc11), true, ifeq2(relation(U_134, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_4330, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc11), true, ifeq2(thing(U_80, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_4454, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc11), true, ifeq2(unisex(U_92, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_3864, plain, (![Y_418, W_417, V_416, Z_420]: (ifeq3(theme(skc8, Y_418, W_417), true, ifeq3(theme(skc8, skc12, V_416), true, ifeq3(agent(skc8, Y_418, Z_420), true, ifeq3(agent(skc8, skc12, Z_420), true, ifeq3(think_believe_consider(skc8, Y_418), true, ifeq3(proposition(skc8, W_417), true, ifeq3(proposition(skc8, V_416), true, V_416, W_417), W_417), W_417), W_417), W_417), W_417), W_417)=W_417))). % 16.51/7.49 tff(c_4276, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc11), true, ifeq2(nonexistent(U_89, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_4894, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc11), true, ifeq2(abstraction(U_137, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_3144, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc11), true, ifeq2(animate(U_122, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_4783, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc11), true, ifeq2(specific(U_86, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_4736, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc11), true, ifeq2(unisex(U_92, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_3196, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc11), true, ifeq2(organism(U_104, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2099, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc8), true, ifeq2(singleton(U_318, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_3099, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc8), true, ifeq2(thing(U_368, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_3862, plain, (![Y_418, W_417, Z_420]: (ifeq3(theme(skc8, Y_418, W_417), true, ifeq3(agent(skc8, Y_418, Z_420), true, ifeq3(agent(skc8, skc12, Z_420), true, ifeq3(think_believe_consider(skc8, Y_418), true, ifeq3(proposition(skc8, W_417), true, skc11, W_417), W_417), W_417), W_417), W_417)=W_417))). % 16.51/7.49 tff(c_2641, plain, (![U_346]: (ifeq2(accessible_world(U_346, skc8), true, ifeq2(impartial(U_346, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2105, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc8), true, ifeq2(singleton(U_318, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_1683, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc8), true, ifeq2(entity(U_294, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_2383, plain, (![U_334]: (ifeq2(accessible_world(U_334, skc8), true, ifeq2(general(U_334, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_2050, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc8), true, ifeq2(nonhuman(U_315, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_2235, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(unisex(U_324, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_3861, plain, (![X_421, V_416, Z_420]: (ifeq3(theme(skc8, X_421, V_416), true, ifeq3(agent(skc8, skc12, Z_420), true, ifeq3(agent(skc8, X_421, Z_420), true, ifeq3(think_believe_consider(skc8, X_421), true, ifeq3(proposition(skc8, V_416), true, V_416, skc11), skc11), skc11), skc11), skc11)=skc11))). % 16.51/7.49 tff(c_10941, plain, (![U_358]: (ifeq2(accessible_world(U_358, skc8), true, ifeq2(abstraction(U_358, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_1744, plain, (![U_297]: (ifeq2(accessible_world(U_297, skc8), true, ifeq2(living(U_297, skc10), true, true, true), true)=true))). % 16.51/7.49 tff(c_4529, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc11), true, ifeq2(eventuality(U_77, skc12), true, true, true), true)=true))). % 16.51/7.49 tff(c_4106, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc11), true, ifeq2(eventuality(U_77, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_4058, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc11), true, ifeq2(event(U_95, skc9), true, true, true), true)=true))). % 16.51/7.49 tff(c_4406, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc11), true, ifeq2(relation(U_134, skc11), true, true, true), true)=true))). % 16.51/7.49 tff(c_10830, plain, (![U_343]: (ifeq2(accessible_world(U_343, skc11), true, ifeq2(relname(U_343, skc13), true, true, true), true)=true))). % 16.51/7.49 tff(c_3164, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc11), true, ifeq2(male(U_371, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_4187, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc11), true, ifeq2(forename(U_128, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_10293, plain, (![U_337]: (ifeq2(accessible_world(U_337, skc8), true, ifeq2(jules_forename(U_337, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_10267, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc11), true, ifeq2(jules_forename(U_146, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_3417, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc11), true, ifeq2(human_person(U_383, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_3093, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc8), true, ifeq2(thing(U_368, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2223, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(unisex(U_324, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2322, plain, (![U_330]: (ifeq2(accessible_world(U_330, skc8), true, ifeq2(animate(U_330, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_3312, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(human(U_377, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_2963, plain, (![U_362]: (ifeq2(accessible_world(U_362, skc8), true, ifeq2(nonexistent(U_362, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_2701, plain, (![U_349]: (ifeq2(accessible_world(U_349, skc8), true, ifeq2(specific(U_349, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_2695, plain, (![U_349]: (ifeq2(accessible_world(U_349, skc8), true, ifeq2(specific(U_349, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2229, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(unisex(U_324, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_10599, plain, (![U_340]: (ifeq2(accessible_world(U_340, skc8), true, ifeq2(relation(U_340, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_2166, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc8), true, ifeq2(organism(U_321, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_3087, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc8), true, ifeq2(thing(U_368, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_2957, plain, (![U_362]: (ifeq2(accessible_world(U_362, skc8), true, ifeq2(nonexistent(U_362, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2881, plain, (![U_358]: (ifeq2(accessible_world(U_358, skc8), true, ifeq2(abstraction(U_358, skc11), true, true, true), true)=true))). % 16.51/7.50 tff(c_10505, plain, (![W_410, X_411]: (ifeq3(of(skc8, W_410, X_411), true, ifeq3(of(skc8, skc13, X_411), true, ifeq3(forename(skc8, W_410), true, ifeq3(entity(skc8, X_411), true, W_410, skc13), skc13), skc13), skc13)=skc13))). % 16.51/7.50 tff(c_4820, plain, (![U_152]: (ifeq2(present(U_152, skc12), true, ifeq2(accessible_world(U_152, skc11), true, true, true), true)=true))). % 16.51/7.50 tff(c_10297, plain, (![V_338]: (ifeq2(accessible_world(skc8, V_338), true, jules_forename(V_338, skc13), true)=true))). % 16.51/7.50 tff(c_10290, plain, (![V_147]: (ifeq2(accessible_world(skc11, V_147), true, jules_forename(V_147, skc13), true)=true))). % 16.51/7.50 tff(c_4376, plain, (![U_158]: (ifeq2(accessible_world(U_158, skc11), true, ifeq2(proposition(U_158, skc11), true, true, true), true)=true))). % 16.51/7.50 tff(c_10326, plain, (jules_forename(skc8, skc13)=true)). % 16.51/7.50 tff(c_10296, plain, (jules_forename(skc11, skc13)=true)). % 16.51/7.50 tff(c_10261, plain, (skc15=skc13)). % 16.51/7.50 tff(c_3755, plain, (![X_411, V_412]: (ifeq3(of(skc8, skc13, X_411), true, ifeq3(of(skc8, V_412, X_411), true, ifeq3(forename(skc8, V_412), true, ifeq3(entity(skc8, X_411), true, skc13, V_412), V_412), V_412), V_412)=V_412))). % 16.51/7.50 tff(c_4491, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc11), true, ifeq2(event(U_95, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_10157, plain, (![V_672]: (ifeq2(accessible_world(skc11, V_672), true, think_believe_consider(V_672, skc12), true)=true))). % 16.51/7.50 tff(c_10114, plain, (![V_670]: (ifeq2(accessible_world(skc11, V_670), true, present(V_670, skc12), true)=true))). % 16.51/7.50 tff(c_2926, plain, (![U_98]: (ifeq2(accessible_world(U_98, skc11), true, ifeq2(man(U_98, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_3579, plain, (![U_394]: (ifeq2(theme(U_394, skc12, skc11), true, ifeq2(accessible_world(U_394, skc8), true, true, true), true)=true))). % 16.51/7.50 tff(c_4592, plain, (![U_155]: (ifeq2(think_believe_consider(U_155, skc12), true, ifeq2(accessible_world(U_155, skc11), true, true, true), true)=true))). % 16.51/7.50 tff(c_4153, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc11), true, ifeq2(vincent_forename(U_161, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_4027, plain, (![U_74]: (ifeq2(accessible_world(U_74, skc11), true, ifeq2(state(U_74, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2276, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc8), true, ifeq2(eventuality(U_327, skc12), true, true, true), true)=true))). % 16.51/7.50 tff(c_2765, plain, (![U_352]: (ifeq2(accessible_world(U_352, skc8), true, ifeq2(event(U_352, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_9891, plain, (![V_659]: (ifeq2(accessible_world(skc8, V_659), true, theme(V_659, skc12, skc11), true)=true))). % 16.51/7.50 tff(c_2282, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc8), true, ifeq2(eventuality(U_327, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_2500, plain, (![U_340]: (ifeq2(accessible_world(U_340, skc8), true, ifeq2(relation(U_340, skc11), true, true, true), true)=true))). % 16.51/7.50 tff(c_3170, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc8), true, ifeq2(male(U_371, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_2565, plain, (![U_343]: (ifeq2(accessible_world(U_343, skc8), true, ifeq2(relname(U_343, skc13), true, true, true), true)=true))). % 16.51/7.50 tff(c_3423, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc8), true, ifeq2(human_person(U_383, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_9739, plain, (![W_652]: (ifeq2(general(skc8, W_652), true, general(skc11, W_652), true)=true))). % 16.51/7.50 tff(c_9695, plain, (![V_423]: (ifeq2(unisex(skc8, skf1(V_423)), true, true, true)=true))). % 16.51/7.50 tff(c_9620, plain, (![W_649]: (ifeq2(unisex(skc8, W_649), true, unisex(skc11, W_649), true)=true))). % 16.51/7.50 tff(c_9577, plain, (![W_647]: (ifeq2(proposition(skc8, W_647), true, proposition(skc11, W_647), true)=true))). % 16.51/7.50 tff(c_9525, plain, (![V_645]: (ifeq2(accessible_world(skc8, V_645), true, present(V_645, skc12), true)=true))). % 16.51/7.50 tff(c_9483, plain, (![W_643]: (ifeq2(entity(skc8, W_643), true, entity(skc11, W_643), true)=true))). % 16.51/7.50 tff(c_2816, plain, (![U_355]: (ifeq2(accessible_world(U_355, skc8), true, ifeq2(man(U_355, skc10), true, true, true), true)=true))). % 16.51/7.50 tff(c_9420, plain, (![W_640]: (ifeq2(existent(skc8, W_640), true, existent(skc11, W_640), true)=true))). % 16.51/7.50 tff(c_9361, plain, (![V_427]: (ifeq2(specific(skc8, skf1(V_427)), true, true, true)=true))). % 16.51/7.50 tff(c_3358, plain, (![U_380]: (ifeq2(present(U_380, skc12), true, ifeq2(accessible_world(U_380, skc8), true, true, true), true)=true))). % 16.51/7.50 tff(c_9308, plain, (![W_636]: (ifeq2(specific(skc8, W_636), true, specific(skc11, W_636), true)=true))). % 16.51/7.50 tff(c_9232, plain, (![W_634]: (ifeq2(nonhuman(skc8, W_634), true, nonhuman(skc11, W_634), true)=true))). % 16.51/7.50 tff(c_3992, plain, (![V_429]: (ifeq(tuple(true, general(skc11, skf1(V_429))), tuple(true, true), a, b)=b))). % 16.51/7.50 tff(c_3901, plain, (![V_424]: (ifeq(tuple(true, male(skc11, skf1(V_424))), tuple(true, true), a, b)=b))). % 16.51/7.50 tff(c_1951, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc8), true, ifeq2(state(U_309, skc9), true, true, true), true)=true))). % 16.51/7.50 tff(c_3941, plain, (![V_426]: (ifeq(tuple(true, existent(skc11, skf1(V_426))), tuple(true, true), a, b)=b))). % 16.51/7.50 tff(c_5373, plain, (ifeq(tuple(true, male(skc11, skc13)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_5444, plain, (ifeq(tuple(human(skc11, skc13), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_9140, plain, (![W_628]: (ifeq2(human_person(skc8, W_628), true, human_person(skc11, W_628), true)=true))). % 16.51/7.50 tff(c_5321, plain, (ifeq(tuple(specific(skc11, skc13), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_3387, plain, (ifeq(tuple(nonexistent(skc11, skc10), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_3496, plain, (ifeq(tuple(true, general(skc11, skc10)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_5026, plain, (ifeq(tuple(human(skc11, skc11), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_9069, plain, (![W_626]: (ifeq2(jules_forename(skc8, W_626), true, jules_forename(skc11, W_626), true)=true))). % 16.51/7.50 tff(c_4941, plain, (ifeq(tuple(true, male(skc11, skc11)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_5062, plain, (ifeq(tuple(specific(skc11, skc11), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_1695, plain, (ifeq(tuple(true, general(skc8, skc10)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_1646, plain, (ifeq(tuple(specific(skc8, skc13), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_1726, plain, (ifeq(tuple(nonexistent(skc8, skc10), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_2079, plain, (ifeq(tuple(human(skc8, skc13), true), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_8998, plain, (![W_624]: (ifeq2(living(skc8, W_624), true, living(skc11, W_624), true)=true))). % 16.51/7.50 tff(c_1930, plain, (ifeq(tuple(true, male(skc8, skc13)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_5850, plain, (![V_84, V_456]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skf1(V_456)), true)=true))). % 16.51/7.50 tff(c_3911, plain, (![V_93, V_424]: (ifeq2(accessible_world(skc11, V_93), true, unisex(V_93, skf1(V_424)), true)=true))). % 16.51/7.50 tff(c_4279, plain, (ifeq(tuple(true, existent(skc11, skc9)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_4002, plain, (![V_87, V_429]: (ifeq2(accessible_world(skc11, V_87), true, specific(V_87, skf1(V_429)), true)=true))). % 16.51/7.50 tff(c_8890, plain, (![W_616]: (ifeq2(forename(skc8, W_616), true, forename(skc11, W_616), true)=true))). % 16.51/7.50 tff(c_5783, plain, (![V_81, V_451]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skf1(V_451)), true)=true))). % 16.51/7.50 tff(c_3948, plain, (![V_90, V_426]: (ifeq2(accessible_world(skc11, V_90), true, nonexistent(V_90, skf1(V_426)), true)=true))). % 16.51/7.50 tff(c_3822, plain, (![V_78, V_415]: (ifeq2(accessible_world(skc11, V_78), true, eventuality(V_78, skf1(V_415)), true)=true))). % 16.51/7.50 tff(c_3623, plain, (![V_96, V_399]: (ifeq2(accessible_world(skc11, V_96), true, event(V_96, skf1(V_399)), true)=true))). % 16.51/7.50 tff(c_3685, plain, (![V_150, V_407]: (ifeq2(accessible_world(skc11, V_150), true, smoke(V_150, skf1(V_407)), true)=true))). % 16.51/7.50 tff(c_3117, plain, (ifeq(tuple(true, nonhuman(skc11, skc10)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_8766, plain, (![V_450]: (ifeq2(thing(skc8, skf1(V_450)), true, true, true)=true))). % 16.51/7.50 tff(c_8695, plain, (![W_603]: (ifeq2(thing(skc8, W_603), true, thing(skc11, W_603), true)=true))). % 16.51/7.50 tff(c_5503, plain, (![V_84]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skc13), true)=true))). % 16.51/7.50 tff(c_5327, plain, (![V_144]: (ifeq2(accessible_world(skc11, V_144), true, general(V_144, skc13), true)=true))). % 16.51/7.50 tff(c_5450, plain, (![V_141]: (ifeq2(accessible_world(skc11, V_141), true, nonhuman(V_141, skc13), true)=true))). % 16.51/7.50 tff(c_5419, plain, (![V_81]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skc13), true)=true))). % 16.51/7.50 tff(c_5382, plain, (![V_93]: (ifeq2(accessible_world(skc11, V_93), true, unisex(V_93, skc13), true)=true))). % 16.51/7.50 tff(c_4245, plain, (ifeq(tuple(true, general(skc11, skc9)), tuple(true, true), a, b)=b)). % 16.51/7.50 tff(c_8589, plain, (![V_414]: (ifeq2(eventuality(skc8, skf1(V_414)), true, true, true)=true))). % 16.51/7.50 tff(c_8544, plain, (![W_595]: (ifeq2(eventuality(skc8, W_595), true, eventuality(skc11, W_595), true)=true))). % 16.51/7.51 tff(c_3564, plain, (![V_84]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skc10), true)=true))). % 16.51/7.51 tff(c_3393, plain, (![V_111]: (ifeq2(accessible_world(skc11, V_111), true, existent(V_111, skc10), true)=true))). % 16.51/7.51 tff(c_4457, plain, (ifeq(tuple(true, male(skc11, skc9)), tuple(true, true), a, b)=b)). % 16.51/7.51 tff(c_8375, plain, (![W_587]: (ifeq2(abstraction(skc8, W_587), true, abstraction(skc11, W_587), true)=true))). % 16.51/7.51 tff(c_3505, plain, (![V_87]: (ifeq2(accessible_world(skc11, V_87), true, specific(V_87, skc10), true)=true))). % 16.51/7.51 tff(c_5291, plain, (![V_84]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skc11), true)=true))). % 16.51/7.51 tff(c_5236, plain, (![V_138]: (ifeq2(accessible_world(skc11, V_138), true, abstraction(V_138, skc13), true)=true))). % 16.51/7.51 tff(c_3454, plain, (![V_81]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skc10), true)=true))). % 16.51/7.51 tff(c_4786, plain, (ifeq(tuple(true, general(skc11, skc12)), tuple(true, true), a, b)=b)). % 16.51/7.51 tff(c_2304, plain, (![V_84]: (ifeq2(accessible_world(skc8, V_84), true, singleton(V_84, skc13), true)=true))). % 16.51/7.51 tff(c_8234, plain, (![W_579]: (ifeq2(animate(skc8, W_579), true, animate(skc11, W_579), true)=true))). % 16.51/7.51 tff(c_2197, plain, (![V_84]: (ifeq2(accessible_world(skc8, V_84), true, singleton(V_84, skc10), true)=true))). % 16.51/7.51 tff(c_5140, plain, (![V_84]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skc9), true)=true))). % 16.51/7.51 tff(c_3345, plain, (![V_114]: (ifeq2(accessible_world(skc11, V_114), true, impartial(V_114, skc10), true)=true))). % 16.51/7.51 tff(c_5112, plain, (![V_135]: (ifeq2(accessible_world(skc11, V_135), true, relation(V_135, skc13), true)=true))). % 16.51/7.51 tff(c_4625, plain, (ifeq(tuple(true, existent(skc11, skc12)), tuple(true, true), a, b)=b)). % 16.51/7.51 tff(c_8089, plain, (![W_571]: (ifeq2(state(skc8, W_571), true, state(skc11, W_571), true)=true))). % 16.51/7.51 tff(c_4991, plain, (![V_81]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skc11), true)=true))). % 16.51/7.51 tff(c_5169, plain, (![V_84]: (ifeq2(accessible_world(skc11, V_84), true, singleton(V_84, skc12), true)=true))). % 16.51/7.51 tff(c_5032, plain, (![V_141]: (ifeq2(accessible_world(skc11, V_141), true, nonhuman(V_141, skc11), true)=true))). % 16.51/7.51 tff(c_4950, plain, (![V_93]: (ifeq2(accessible_world(skc11, V_93), true, unisex(V_93, skc11), true)=true))). % 16.51/7.51 tff(c_5068, plain, (![V_144]: (ifeq2(accessible_world(skc11, V_144), true, general(V_144, skc11), true)=true))). % 16.51/7.51 tff(c_4739, plain, (ifeq(tuple(true, male(skc11, skc12)), tuple(true, true), a, b)=b)). % 16.51/7.51 tff(c_3293, plain, (![V_117]: (ifeq2(accessible_world(skc11, V_117), true, living(V_117, skc10), true)=true))). % 16.51/7.51 tff(c_7944, plain, (![V_563]: (ifeq2(accessible_world(skc8, V_563), true, think_believe_consider(V_563, skc12), true)=true))). % 16.62/7.51 tff(c_3265, plain, (![V_108]: (ifeq2(accessible_world(skc11, V_108), true, entity(V_108, skc10), true)=true))). % 16.62/7.51 tff(c_3108, plain, (![V_369]: (ifeq2(accessible_world(skc8, V_369), true, thing(V_369, skc10), true)=true))). % 16.62/7.51 tff(c_2707, plain, (![V_350]: (ifeq2(accessible_world(skc8, V_350), true, specific(V_350, skc10), true)=true))). % 16.62/7.51 tff(c_1649, plain, (ifeq(tuple(specific(skc8, skc11), true), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_7755, plain, (![W_555]: (ifeq2(relation(skc8, W_555), true, relation(skc11, W_555), true)=true))). % 16.62/7.51 tff(c_2241, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, unisex(V_325, skc13), true)=true))). % 16.62/7.51 tff(c_2085, plain, (![V_141]: (ifeq2(accessible_world(skc8, V_141), true, nonhuman(V_141, skc13), true)=true))). % 16.62/7.51 tff(c_2119, plain, (![V_319]: (ifeq2(accessible_world(skc8, V_319), true, singleton(V_319, skc11), true)=true))). % 16.62/7.51 tff(c_2390, plain, (![V_335]: (ifeq2(accessible_world(skc8, V_335), true, general(V_335, skc13), true)=true))). % 16.62/7.51 tff(c_1555, plain, (ifeq(tuple(human(skc8, skc11), true), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_7639, plain, (![V_401]: (ifeq2(smoke(skc8, skf1(V_401)), true, true, true)=true))). % 16.62/7.51 tff(c_7616, plain, (![W_547]: (ifeq2(smoke(skc8, W_547), true, smoke(skc11, W_547), true)=true))). % 16.62/7.51 tff(c_3107, plain, (![V_369]: (ifeq2(accessible_world(skc8, V_369), true, thing(V_369, skc13), true)=true))). % 16.62/7.51 tff(c_3022, plain, (![V_366]: (ifeq2(accessible_world(skc8, V_366), true, existent(V_366, skc10), true)=true))). % 16.62/7.51 tff(c_3318, plain, (![V_378]: (ifeq2(accessible_world(skc11, V_378), true, human(V_378, skc10), true)=true))). % 16.62/7.51 tff(c_4254, plain, (![V_87]: (ifeq2(accessible_world(skc11, V_87), true, specific(V_87, skc9), true)=true))). % 16.62/7.51 tff(c_4680, plain, (![V_132]: (ifeq2(accessible_world(skc11, V_132), true, relname(V_132, skc13), true)=true))). % 16.62/7.51 tff(c_1513, plain, (ifeq(tuple(true, male(skc8, skc11)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_3211, plain, (![V_105]: (ifeq2(accessible_world(skc11, V_105), true, organism(V_105, skc10), true)=true))). % 16.62/7.51 tff(c_7471, plain, (![W_539]: (ifeq2(human(skc8, W_539), true, human(skc11, W_539), true)=true))). % 16.62/7.51 tff(c_4859, plain, (![V_81]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skc12), true)=true))). % 16.62/7.51 tff(c_4912, plain, (![V_138]: (ifeq2(accessible_world(skc11, V_138), true, abstraction(V_138, skc11), true)=true))). % 16.62/7.51 tff(c_4748, plain, (![V_93]: (ifeq2(accessible_world(skc11, V_93), true, unisex(V_93, skc12), true)=true))). % 16.62/7.51 tff(c_4466, plain, (![V_93]: (ifeq2(accessible_world(skc11, V_93), true, unisex(V_93, skc9), true)=true))). % 16.62/7.51 tff(c_2987, plain, (ifeq(tuple(unisex(skc11, skc10), true), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_3150, plain, (![V_123]: (ifeq2(accessible_world(skc11, V_123), true, animate(V_123, skc10), true)=true))). % 16.62/7.51 tff(c_4345, plain, (![V_81]: (ifeq2(accessible_world(skc11, V_81), true, thing(V_81, skc9), true)=true))). % 16.62/7.51 tff(c_4795, plain, (![V_87]: (ifeq2(accessible_world(skc11, V_87), true, specific(V_87, skc12), true)=true))). % 16.62/7.51 tff(c_1791, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc8), true, ifeq2(forename(U_300, skc13), true, true, true), true)=true))). % 16.62/7.51 tff(c_4285, plain, (![V_90]: (ifeq2(accessible_world(skc11, V_90), true, nonexistent(V_90, skc9), true)=true))). % 16.62/7.51 tff(c_4631, plain, (![V_90]: (ifeq2(accessible_world(skc11, V_90), true, nonexistent(V_90, skc12), true)=true))). % 16.62/7.51 tff(c_1689, plain, (![V_295]: (ifeq2(accessible_world(skc8, V_295), true, entity(V_295, skc10), true)=true))). % 16.62/7.51 tff(c_2391, plain, (![V_335]: (ifeq2(accessible_world(skc8, V_335), true, general(V_335, skc11), true)=true))). % 16.62/7.51 tff(c_1507, plain, (ifeq(tuple(true, male(skc8, skc9)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_7208, plain, (be(skc11, skc9, skc10, skc10)=true)). % 16.62/7.51 tff(c_3665, plain, (![W_403, X_406, Y_402]: (ifeq2(be(skc8, W_403, X_406, Y_402), true, be(skc11, W_403, X_406, Y_402), true)=true))). % 16.62/7.51 tff(c_2057, plain, (![V_316]: (ifeq2(accessible_world(skc8, V_316), true, nonhuman(V_316, skc11), true)=true))). % 16.62/7.51 tff(c_2647, plain, (![V_347]: (ifeq2(accessible_world(skc8, V_347), true, impartial(V_347, skc10), true)=true))). % 16.62/7.51 tff(c_2118, plain, (![V_319]: (ifeq2(accessible_world(skc8, V_319), true, singleton(V_319, skc9), true)=true))). % 16.62/7.51 tff(c_2245, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, unisex(V_325, skc11), true)=true))). % 16.62/7.51 tff(c_1750, plain, (![V_298]: (ifeq2(accessible_world(skc8, V_298), true, living(V_298, skc10), true)=true))). % 16.62/7.51 tff(c_1510, plain, (ifeq(tuple(true, male(skc8, skc12)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_7074, plain, (![V_398]: (ifeq2(event(skc8, skf1(V_398)), true, true, true)=true))). % 16.62/7.51 tff(c_7029, plain, (![W_514]: (ifeq2(event(skc8, W_514), true, event(skc11, W_514), true)=true))). % 16.62/7.51 tff(c_2888, plain, (![V_359]: (ifeq2(accessible_world(skc8, V_359), true, abstraction(V_359, skc13), true)=true))). % 16.62/7.51 tff(c_2117, plain, (![V_319]: (ifeq2(accessible_world(skc8, V_319), true, singleton(V_319, skc12), true)=true))). % 16.62/7.51 tff(c_3111, plain, (![V_369]: (ifeq2(accessible_world(skc8, V_369), true, thing(V_369, skc11), true)=true))). % 16.62/7.51 tff(c_4550, plain, (![V_78]: (ifeq2(accessible_world(skc11, V_78), true, eventuality(V_78, skc12), true)=true))). % 16.62/7.51 tff(c_4418, plain, (![V_135]: (ifeq2(accessible_world(skc11, V_135), true, relation(V_135, skc11), true)=true))). % 16.62/7.51 tff(c_1552, plain, (ifeq(tuple(true, nonhuman(skc8, skc10)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_4201, plain, (![V_129]: (ifeq2(accessible_world(skc11, V_129), true, forename(V_129, skc13), true)=true))). % 16.62/7.51 tff(c_6864, plain, (![W_506]: (ifeq2(relname(skc8, W_506), true, relname(skc11, W_506), true)=true))). % 16.62/7.51 tff(c_4127, plain, (![V_78]: (ifeq2(accessible_world(skc11, V_78), true, eventuality(V_78, skc9), true)=true))). % 16.62/7.51 tff(c_6023, plain, (ifeq2(agent(skc8, skf1(skc10), skc10), true, true, true)=true)). % 16.62/7.51 tff(c_3176, plain, (![V_372]: (ifeq2(accessible_world(skc11, V_372), true, male(V_372, skc10), true)=true))). % 16.62/7.51 tff(c_4070, plain, (![V_96]: (ifeq2(accessible_world(skc11, V_96), true, event(V_96, skc9), true)=true))). % 16.62/7.51 tff(c_1589, plain, (ifeq(tuple(true, existent(skc8, skc12)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_3429, plain, (![V_384]: (ifeq2(accessible_world(skc11, V_384), true, human_person(V_384, skc10), true)=true))). % 16.62/7.51 tff(c_6738, plain, (![W_499]: (ifeq2(organism(skc8, W_499), true, organism(skc11, W_499), true)=true))). % 16.62/7.51 tff(c_3319, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, human(V_378, skc10), true)=true))). % 16.62/7.51 tff(c_2708, plain, (![V_350]: (ifeq2(accessible_world(skc8, V_350), true, specific(V_350, skc9), true)=true))). % 16.62/7.51 tff(c_2244, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, unisex(V_325, skc12), true)=true))). % 16.62/7.51 tff(c_2890, plain, (![V_359]: (ifeq2(accessible_world(skc8, V_359), true, abstraction(V_359, skc11), true)=true))). % 16.62/7.51 tff(c_2970, plain, (![V_363]: (ifeq2(accessible_world(skc8, V_363), true, nonexistent(V_363, skc12), true)=true))). % 16.62/7.51 tff(c_1586, plain, (ifeq(tuple(true, existent(skc8, skc9)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_2709, plain, (![V_350]: (ifeq2(accessible_world(skc8, V_350), true, specific(V_350, skc12), true)=true))). % 16.62/7.51 tff(c_2243, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, unisex(V_325, skc9), true)=true))). % 16.62/7.51 tff(c_2969, plain, (![V_363]: (ifeq2(accessible_world(skc8, V_363), true, nonexistent(V_363, skc9), true)=true))). % 16.62/7.51 tff(c_2771, plain, (![U_352]: (ifeq2(accessible_world(U_352, skc8), true, ifeq2(event(U_352, skc12), true, true, true), true)=true))). % 16.62/7.51 tff(c_2506, plain, (![V_341]: (ifeq2(accessible_world(skc8, V_341), true, relation(V_341, skc13), true)=true))). % 16.62/7.51 tff(c_2328, plain, (![V_331]: (ifeq2(accessible_world(skc8, V_331), true, animate(V_331, skc10), true)=true))). % 16.62/7.51 tff(c_3109, plain, (![V_369]: (ifeq2(accessible_world(skc8, V_369), true, thing(V_369, skc12), true)=true))). % 16.62/7.51 tff(c_3110, plain, (![V_369]: (ifeq2(accessible_world(skc8, V_369), true, thing(V_369, skc9), true)=true))). % 16.62/7.51 tff(c_2172, plain, (![V_322]: (ifeq2(accessible_world(skc8, V_322), true, organism(V_322, skc10), true)=true))). % 16.62/7.51 tff(c_1640, plain, (ifeq(tuple(true, general(skc8, skc9)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_6406, plain, (![W_482]: (ifeq2(man(skc8, W_482), true, man(skc11, W_482), true)=true))). % 16.62/7.51 tff(c_4504, plain, (![V_96]: (ifeq2(accessible_world(skc11, V_96), true, event(V_96, skc12), true)=true))). % 16.62/7.51 tff(c_2945, plain, (![V_99]: (ifeq2(accessible_world(skc11, V_99), true, man(V_99, skc10), true)=true))). % 16.62/7.51 tff(c_4385, plain, (![V_159]: (ifeq2(accessible_world(skc11, V_159), true, proposition(V_159, skc11), true)=true))). % 16.62/7.51 tff(c_4160, plain, (![V_162]: (ifeq2(accessible_world(skc11, V_162), true, vincent_forename(V_162, skc13), true)=true))). % 16.62/7.51 tff(c_4037, plain, (![V_75]: (ifeq2(accessible_world(skc11, V_75), true, state(V_75, skc9), true)=true))). % 16.62/7.51 tff(c_1643, plain, (ifeq(tuple(true, general(skc8, skc12)), tuple(true, true), a, b)=b)). % 16.62/7.51 tff(c_6296, plain, (ifeq2(accessible_world(skc11, skc11), true, true, true)=true)). % 16.62/7.51 tff(c_1881, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc8), true, ifeq2(proposition(U_306, skc11), true, true, true), true)=true))). % 16.62/7.51 tff(c_3177, plain, (![V_372]: (ifeq2(accessible_world(skc8, V_372), true, male(V_372, skc10), true)=true))). % 16.62/7.51 tff(c_2508, plain, (![V_341]: (ifeq2(accessible_world(skc8, V_341), true, relation(V_341, skc11), true)=true))). % 16.62/7.52 tff(c_3430, plain, (![V_384]: (ifeq2(accessible_world(skc8, V_384), true, human_person(V_384, skc10), true)=true))). % 16.62/7.52 tff(c_2573, plain, (![V_344]: (ifeq2(accessible_world(skc8, V_344), true, relname(V_344, skc13), true)=true))). % 16.62/7.52 tff(c_1516, plain, (ifeq(tuple(unisex(skc8, skc10), true), tuple(true, true), a, b)=b)). % 16.62/7.52 tff(c_6153, plain, (![V_425]: (ifeq2(nonexistent(skc8, skf1(V_425)), true, true, true)=true))). % 16.62/7.52 tff(c_6108, plain, (![W_466]: (ifeq2(nonexistent(skc8, W_466), true, nonexistent(skc11, W_466), true)=true))). % 16.62/7.52 tff(c_2288, plain, (![V_328]: (ifeq2(accessible_world(skc8, V_328), true, eventuality(V_328, skc12), true)=true))). % 16.62/7.52 tff(c_2289, plain, (![V_328]: (ifeq2(accessible_world(skc8, V_328), true, eventuality(V_328, skc9), true)=true))). % 16.62/7.52 tff(c_2777, plain, (![V_353]: (ifeq2(accessible_world(skc8, V_353), true, event(V_353, skc9), true)=true))). % 16.62/7.52 tff(c_6011, plain, (agent(skc11, skf1(skc10), skc10)=true)). % 16.62/7.52 tff(c_3225, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc8), true, ifeq2(vincent_forename(U_374, skc13), true, true, true), true)=true))). % 16.62/7.52 tff(c_5347, plain, (![W_445]: (ifeq2(impartial(skc8, W_445), true, impartial(skc11, W_445), true)=true))). % 16.62/7.52 tff(c_5188, plain, (![W_443]: (ifeq2(male(skc8, W_443), true, male(skc11, W_443), true)=true))). % 16.62/7.52 tff(c_5888, plain, (![V_454]: (ifeq2(singleton(skc8, skf1(V_454)), true, true, true)=true))). % 16.62/7.52 tff(c_5721, plain, (![W_448]: (ifeq2(singleton(skc8, W_448), true, singleton(skc11, W_448), true)=true))). % 16.62/7.52 tff(c_5467, plain, (![W_446]: (ifeq2(vincent_forename(skc8, W_446), true, vincent_forename(skc11, W_446), true)=true))). % 16.62/7.52 tff(c_5807, plain, (![V_454]: (singleton(skc11, skf1(V_454))=true))). % 16.62/7.52 tff(c_3907, plain, (![V_424]: (ifeq2(abstraction(skc11, skf1(V_424)), true, true, true)=true))). % 16.62/7.52 tff(c_3998, plain, (![V_429]: (ifeq2(entity(skc11, skf1(V_429)), true, true, true)=true))). % 16.62/7.52 tff(c_5749, plain, (![V_450]: (thing(skc11, skf1(V_450))=true))). % 16.62/7.52 tff(c_4769, plain, (![V_408]: (ifeq2(present(skc8, skf1(V_408)), true, true, true)=true))). % 16.62/7.52 tff(c_5644, plain, (of(skc11, skc13, skc10)=true)). % 16.62/7.52 tff(c_5609, plain, (agent(skc11, skc12, skc10)=true)). % 16.62/7.52 tff(c_1992, plain, (![U_312]: (ifeq2(think_believe_consider(U_312, skc12), true, ifeq2(accessible_world(U_312, skc8), true, true, true), true)=true))). % 16.62/7.52 tff(c_5515, plain, (theme(skc11, skc12, skc11)=true)). % 16.62/7.52 tff(c_5410, plain, (ifeq2(entity(skc11, skc13), true, true, true)=true)). % 16.62/7.52 tff(c_5482, plain, (singleton(skc11, skc13)=true)). % 16.62/7.52 tff(c_5376, plain, (ifeq2(eventuality(skc11, skc13), true, true, true)=true)). % 16.62/7.52 tff(c_5426, plain, (nonhuman(skc11, skc13)=true)). % 16.62/7.52 tff(c_5389, plain, (thing(skc11, skc13)=true)). % 16.62/7.52 tff(c_5355, plain, (unisex(skc11, skc13)=true)). % 16.62/7.52 tff(c_5303, plain, (general(skc11, skc13)=true)). % 16.62/7.52 tff(c_5109, plain, (ifeq2(proposition(skc11, skc13), true, true, true)=true)). % 16.62/7.52 tff(c_5270, plain, (singleton(skc11, skc11)=true)). % 16.62/7.52 tff(c_5261, plain, (ifeq2(accessible_world(skc11, skc8), true, true, true)=true)). % 16.62/7.52 tff(c_4982, plain, (ifeq2(entity(skc11, skc11), true, true, true)=true)). % 16.62/7.52 tff(c_4979, plain, (ifeq2(eventuality(skc11, skc11), true, true, true)=true)). % 16.62/7.52 tff(c_5203, plain, (abstraction(skc11, skc13)=true)). % 16.62/7.52 tff(c_4463, plain, (ifeq2(abstraction(skc11, skc9), true, true, true)=true)). % 16.62/7.52 tff(c_5148, plain, (singleton(skc11, skc12)=true)). % 16.62/7.52 tff(c_5119, plain, (singleton(skc11, skc9)=true)). % 16.62/7.52 tff(c_5085, plain, (relation(skc11, skc13)=true)). % 16.62/7.52 tff(c_3585, plain, (![W_395, X_396]: (ifeq2(theme(skc8, W_395, X_396), true, theme(skc11, W_395, X_396), true)=true))). % 16.62/7.52 tff(c_5044, plain, (general(skc11, skc11)=true)). % 16.62/7.52 tff(c_4251, plain, (ifeq2(entity(skc11, skc9), true, true, true)=true)). % 16.62/7.52 tff(c_5008, plain, (nonhuman(skc11, skc11)=true)). % 16.62/7.52 tff(c_3484, plain, (![W_387, X_388]: (ifeq2(agent(skc8, W_387, X_388), true, agent(skc11, W_387, X_388), true)=true))). % 16.62/7.52 tff(c_4961, plain, (thing(skc11, skc11)=true)). % 16.62/7.52 tff(c_4745, plain, (ifeq2(abstraction(skc11, skc12), true, true, true)=true)). % 16.62/7.52 tff(c_4923, plain, (unisex(skc11, skc11)=true)). % 16.62/7.52 tff(c_4850, plain, (ifeq2(entity(skc11, skc12), true, true, true)=true)). % 16.62/7.52 tff(c_4866, plain, (abstraction(skc11, skc11)=true)). % 16.62/7.52 tff(c_3549, plain, (![W_391, X_392]: (ifeq2(of(skc8, W_391, X_392), true, of(skc11, W_391, X_392), true)=true))). % 16.62/7.52 tff(c_4829, plain, (thing(skc11, skc12)=true)). % 16.62/7.52 tff(c_4802, plain, (present(skc11, skc12)=true)). % 16.62/7.52 tff(c_4755, plain, (specific(skc11, skc12)=true)). % 16.62/7.52 tff(c_3364, plain, (![W_381]: (ifeq2(present(skc8, W_381), true, present(skc11, W_381), true)=true))). % 16.62/7.52 tff(c_4721, plain, (unisex(skc11, skc12)=true)). % 16.62/7.52 tff(c_4642, plain, (relname(skc11, skc13)=true)). % 16.62/7.52 tff(c_4412, plain, (ifeq2(relname(skc11, skc11), true, true, true)=true)). % 16.62/7.52 tff(c_4607, plain, (nonexistent(skc11, skc12)=true)). % 16.62/7.52 tff(c_4500, plain, (ifeq2(smoke(skc11, skc12), true, true, true)=true)). % 16.62/7.52 tff(c_4568, plain, (think_believe_consider(skc11, skc12)=true)). % 16.62/7.52 tff(c_1998, plain, (![W_313]: (ifeq2(think_believe_consider(skc8, W_313), true, think_believe_consider(skc11, W_313), true)=true))). % 16.62/7.52 tff(c_4514, plain, (eventuality(skc11, skc12)=true)). % 16.62/7.52 tff(c_4494, plain, (ifeq2(state(skc11, skc12), true, true, true)=true)). % 16.62/7.52 tff(c_4473, plain, (event(skc11, skc12)=true)). % 16.62/7.52 tff(c_4425, plain, (unisex(skc11, skc9)=true)). % 16.62/7.52 tff(c_2778, plain, (![V_353]: (ifeq2(accessible_world(skc8, V_353), true, event(V_353, skc12), true)=true))). % 16.62/7.52 tff(c_4391, plain, (relation(skc11, skc11)=true)). % 16.62/7.52 tff(c_4352, plain, (proposition(skc11, skc11)=true)). % 16.62/7.52 tff(c_4301, plain, (thing(skc11, skc9)=true)). % 16.62/7.52 tff(c_1887, plain, (![V_307]: (ifeq2(accessible_world(skc8, V_307), true, proposition(V_307, skc11), true)=true))). % 16.62/7.52 tff(c_4067, plain, (ifeq2(smoke(skc11, skc9), true, true, true)=true)). % 16.62/7.52 tff(c_4261, plain, (nonexistent(skc11, skc9)=true)). % 16.62/7.52 tff(c_4208, plain, (specific(skc11, skc9)=true)). % 16.69/7.52 tff(c_1803, plain, (![V_301]: (ifeq2(accessible_world(skc8, V_301), true, forename(V_301, skc13), true)=true))). % 16.69/7.52 tff(c_4166, plain, (forename(skc11, skc13)=true)). % 16.69/7.52 tff(c_4135, plain, (vincent_forename(skc11, skc13)=true)). % 16.69/7.52 tff(c_4077, plain, (eventuality(skc11, skc9)=true)). % 16.69/7.52 tff(c_3231, plain, (![V_375]: (ifeq2(accessible_world(skc8, V_375), true, vincent_forename(V_375, skc13), true)=true))). % 16.69/7.52 tff(c_4043, plain, (event(skc11, skc9)=true)). % 16.69/7.52 tff(c_4009, plain, (state(skc11, skc9)=true)). % 16.69/7.52 tff(c_3957, plain, (![V_427]: (specific(skc11, skf1(V_427))=true))). % 16.69/7.52 tff(c_1957, plain, (![V_310]: (ifeq2(accessible_world(skc8, V_310), true, state(V_310, skc9), true)=true))). % 16.69/7.52 tff(c_3920, plain, (![V_425]: (nonexistent(skc11, skf1(V_425))=true))). % 16.69/7.52 tff(c_3880, plain, (![V_423]: (unisex(skc11, skf1(V_423))=true))). % 16.69/7.52 tff(c_3613, plain, (![V_399]: (ifeq2(state(skc11, skf1(V_399)), true, true, true)=true))). % 16.69/7.52 tff(c_140, plain, (![Y_189, W_185, V_190, X_188, Z_187, U_186]: (ifeq3(theme(U_186, Y_189, W_185), true, ifeq3(theme(U_186, X_188, V_190), true, ifeq3(agent(U_186, Y_189, Z_187), true, ifeq3(agent(U_186, X_188, Z_187), true, ifeq3(think_believe_consider(U_186, Y_189), true, ifeq3(think_believe_consider(U_186, X_188), true, ifeq3(proposition(U_186, W_185), true, ifeq3(proposition(U_186, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 16.69/7.52 tff(c_3782, plain, (![V_414]: (eventuality(skc11, skf1(V_414))=true))). % 16.69/7.52 tff(c_3694, plain, (![V_408]: (present(skc11, skf1(V_408))=true))). % 16.69/7.52 tff(c_138, plain, (![U_181, W_182, X_183, V_184]: (ifeq3(of(U_181, W_182, X_183), true, ifeq3(of(U_181, V_184, X_183), true, ifeq3(forename(U_181, W_182), true, ifeq3(forename(U_181, V_184), true, ifeq3(entity(U_181, X_183), true, W_182, V_184), V_184), V_184), V_184), V_184)=V_184))). % 16.69/7.52 tff(c_3641, plain, (![V_401]: (smoke(skc11, skf1(V_401))=true))). % 16.69/7.52 tff(c_136, plain, (![X_178, V_180, W_176, Y_179, U_177]: (ifeq2(be(U_177, W_176, X_178, Y_179), true, ifeq2(accessible_world(U_177, V_180), true, be(V_180, W_176, X_178, Y_179), true), true)=true))). % 16.69/7.52 tff(c_3600, plain, (![U_195]: (ifeq2(man(skc11, U_195), true, true, true)=true))). % 16.69/7.52 tff(c_3591, plain, (![V_398]: (event(skc11, skf1(V_398))=true))). % 16.69/7.52 tff(c_134, plain, (![U_172, W_173, X_174, V_175]: (ifeq2(theme(U_172, W_173, X_174), true, ifeq2(accessible_world(U_172, V_175), true, theme(V_175, W_173, X_174), true), true)=true))). % 16.69/7.52 tff(c_3520, plain, (singleton(skc11, skc10)=true)). % 16.69/7.52 tff(c_130, plain, (![U_164, W_165, X_166, V_167]: (ifeq2(of(U_164, W_165, X_166), true, ifeq2(accessible_world(U_164, V_167), true, of(V_167, W_165, X_166), true), true)=true))). % 16.69/7.52 tff(c_3442, plain, (ifeq2(eventuality(skc11, skc10), true, true, true)=true)). % 16.69/7.52 tff(c_3451, plain, (ifeq2(abstraction(skc11, skc10), true, true, true)=true)). % 16.69/7.52 tff(c_3461, plain, (specific(skc11, skc10)=true)). % 16.69/7.52 tff(c_132, plain, (![U_168, W_169, X_170, V_171]: (ifeq2(agent(U_168, W_169, X_170), true, ifeq2(accessible_world(U_168, V_171), true, agent(V_171, W_169, X_170), true), true)=true))). % 16.69/7.52 tff(c_3400, plain, (thing(skc11, skc10)=true)). % 16.69/7.52 tff(c_88, plain, (![U_101, V_102, W_103]: (ifeq2(accessible_world(U_101, V_102), true, ifeq2(human_person(U_101, W_103), true, human_person(V_102, W_103), true), true)=true))). % 16.69/7.52 tff(c_3369, plain, (existent(skc11, skc10)=true)). % 16.69/7.52 tff(c_122, plain, (![U_152, W_153, V_154]: (ifeq2(present(U_152, W_153), true, ifeq2(accessible_world(U_152, V_154), true, present(V_154, W_153), true), true)=true))). % 16.69/7.52 tff(c_3324, plain, (impartial(skc11, skc10)=true)). % 16.69/7.52 tff(c_100, plain, (![U_119, V_120, W_121]: (ifeq2(accessible_world(U_119, V_120), true, ifeq2(human(U_119, W_121), true, human(V_120, W_121), true), true)=true))). % 16.69/7.52 tff(c_3272, plain, (living(skc11, skc10)=true)). % 16.69/7.52 tff(c_3235, plain, (entity(skc11, skc10)=true)). % 16.69/7.52 tff(c_128, plain, (![U_161, V_162, W_163]: (ifeq2(accessible_world(U_161, V_162), true, ifeq2(vincent_forename(U_161, W_163), true, vincent_forename(V_162, W_163), true), true)=true))). % 16.69/7.52 tff(c_3181, plain, (organism(skc11, skc10)=true)). % 16.69/7.52 tff(c_104, plain, (![U_125, V_126, W_127]: (ifeq2(accessible_world(U_125, V_126), true, ifeq2(male(U_125, W_127), true, male(V_126, W_127), true), true)=true))). % 16.69/7.52 tff(c_3129, plain, (animate(skc11, skc10)=true)). % 16.69/7.52 tff(c_3050, plain, (human(skc11, skc10)=true)). % 16.69/7.52 tff(c_74, plain, (![U_80, V_81, W_82]: (ifeq2(accessible_world(U_80, V_81), true, ifeq2(thing(U_80, W_82), true, thing(V_81, W_82), true), true)=true))). % 16.69/7.52 tff(c_2999, plain, (human_person(skc11, skc10)=true)). % 16.69/7.52 tff(c_94, plain, (![U_110, V_111, W_112]: (ifeq2(accessible_world(U_110, V_111), true, ifeq2(existent(U_110, W_112), true, existent(V_111, W_112), true), true)=true))). % 16.69/7.52 tff(c_2975, plain, (male(skc11, skc10)=true)). % 16.69/7.52 tff(c_80, plain, (![U_89, V_90, W_91]: (ifeq2(accessible_world(U_89, V_90), true, ifeq2(nonexistent(U_89, W_91), true, nonexistent(V_90, W_91), true), true)=true))). % 16.69/7.52 tff(c_2908, plain, (man(skc11, skc10)=true)). % 16.69/7.52 tff(c_2819, plain, (![V_356]: (ifeq2(accessible_world(skc8, V_356), true, man(V_356, skc10), true)=true))). % 16.69/7.52 tff(c_112, plain, (![U_137, V_138, W_139]: (ifeq2(accessible_world(U_137, V_138), true, ifeq2(abstraction(U_137, W_139), true, abstraction(V_138, W_139), true), true)=true))). % 16.69/7.52 tff(c_86, plain, (![U_98, V_99, W_100]: (ifeq2(accessible_world(U_98, V_99), true, ifeq2(man(U_98, W_100), true, man(V_99, W_100), true), true)=true))). % 16.69/7.53 tff(c_84, plain, (![U_95, V_96, W_97]: (ifeq2(accessible_world(U_95, V_96), true, ifeq2(event(U_95, W_97), true, event(V_96, W_97), true), true)=true))). % 16.69/7.53 tff(c_78, plain, (![U_86, V_87, W_88]: (ifeq2(accessible_world(U_86, V_87), true, ifeq2(specific(U_86, W_88), true, specific(V_87, W_88), true), true)=true))). % 16.69/7.53 tff(c_96, plain, (![U_113, V_114, W_115]: (ifeq2(accessible_world(U_113, V_114), true, ifeq2(impartial(U_113, W_115), true, impartial(V_114, W_115), true), true)=true))). % 16.69/7.53 tff(c_108, plain, (![U_131, V_132, W_133]: (ifeq2(accessible_world(U_131, V_132), true, ifeq2(relname(U_131, W_133), true, relname(V_132, W_133), true), true)=true))). % 16.69/7.53 tff(c_110, plain, (![U_134, V_135, W_136]: (ifeq2(accessible_world(U_134, V_135), true, ifeq2(relation(U_134, W_136), true, relation(V_135, W_136), true), true)=true))). % 16.69/7.53 tff(c_118, plain, (![U_146, V_147, W_148]: (ifeq2(accessible_world(U_146, V_147), true, ifeq2(jules_forename(U_146, W_148), true, jules_forename(V_147, W_148), true), true)=true))). % 16.69/7.53 tff(c_116, plain, (![U_143, V_144, W_145]: (ifeq2(accessible_world(U_143, V_144), true, ifeq2(general(U_143, W_145), true, general(V_144, W_145), true), true)=true))). % 16.69/7.53 tff(c_2341, plain, (ifeq2(accessible_world(skc8, skc8), true, true, true)=true)). % 16.69/7.53 tff(c_1824, plain, (ifeq2(entity(skc8, skc13), true, true, true)=true)). % 16.69/7.53 tff(c_102, plain, (![U_122, V_123, W_124]: (ifeq2(accessible_world(U_122, V_123), true, ifeq2(animate(U_122, W_124), true, animate(V_123, W_124), true), true)=true))). % 16.69/7.53 tff(c_1776, plain, (ifeq2(abstraction(skc8, skc10), true, true, true)=true)). % 16.69/7.53 tff(c_2259, plain, (singleton(skc8, skc13)=true)). % 16.69/7.53 tff(c_72, plain, (![U_77, V_78, W_79]: (ifeq2(accessible_world(U_77, V_78), true, ifeq2(eventuality(U_77, W_79), true, eventuality(V_78, W_79), true), true)=true))). % 16.69/7.53 tff(c_1821, plain, (ifeq2(eventuality(skc8, skc13), true, true, true)=true)). % 16.69/7.53 tff(c_82, plain, (![U_92, V_93, W_94]: (ifeq2(accessible_world(U_92, V_93), true, ifeq2(unisex(U_92, W_94), true, unisex(V_93, W_94), true), true)=true))). % 16.69/7.53 tff(c_2176, plain, (singleton(skc8, skc10)=true)). % 16.69/7.53 tff(c_90, plain, (![U_104, V_105, W_106]: (ifeq2(accessible_world(U_104, V_105), true, ifeq2(organism(U_104, W_106), true, organism(V_105, W_106), true), true)=true))). % 16.69/7.53 tff(c_1767, plain, (ifeq2(eventuality(skc8, skc10), true, true, true)=true)). % 16.69/7.53 tff(c_76, plain, (![U_83, V_84, W_85]: (ifeq2(accessible_world(U_83, V_84), true, ifeq2(singleton(U_83, W_85), true, singleton(V_84, W_85), true), true)=true))). % 16.69/7.53 tff(c_2061, plain, (nonhuman(skc8, skc13)=true)). % 16.69/7.53 tff(c_114, plain, (![U_140, V_141, W_142]: (ifeq2(accessible_world(U_140, V_141), true, ifeq2(nonhuman(U_140, W_142), true, nonhuman(V_141, W_142), true), true)=true))). % 16.69/7.53 tff(c_890, plain, (ifeq2(entity(skc8, skc11), true, true, true)=true)). % 16.69/7.53 tff(c_124, plain, (![U_155, W_156, V_157]: (ifeq2(think_believe_consider(U_155, W_156), true, ifeq2(accessible_world(U_155, V_157), true, think_believe_consider(V_157, W_156), true), true)=true))). % 16.69/7.53 tff(c_70, plain, (![U_74, V_75, W_76]: (ifeq2(accessible_world(U_74, V_75), true, ifeq2(state(U_74, W_76), true, state(V_75, W_76), true), true)=true))). % 16.69/7.53 tff(c_1918, plain, (unisex(skc8, skc13)=true)). % 16.69/7.53 tff(c_126, plain, (![U_158, V_159, W_160]: (ifeq2(accessible_world(U_158, V_159), true, ifeq2(proposition(U_158, W_160), true, proposition(V_159, W_160), true), true)=true))). % 16.69/7.53 tff(c_120, plain, (![U_149, V_150, W_151]: (ifeq2(accessible_world(U_149, V_150), true, ifeq2(smoke(U_149, W_151), true, smoke(V_150, W_151), true), true)=true))). % 16.69/7.53 tff(c_1809, plain, (thing(skc8, skc13)=true)). % 16.69/7.53 tff(c_106, plain, (![U_128, V_129, W_130]: (ifeq2(accessible_world(U_128, V_129), true, ifeq2(forename(U_128, W_130), true, forename(V_129, W_130), true), true)=true))). % 16.69/7.53 tff(c_1755, plain, (thing(skc8, skc10)=true)). % 16.69/7.53 tff(c_98, plain, (![U_116, V_117, W_118]: (ifeq2(accessible_world(U_116, V_117), true, ifeq2(living(U_116, W_118), true, living(V_117, W_118), true), true)=true))). % 16.69/7.53 tff(c_1714, plain, (existent(skc8, skc10)=true)). % 16.69/7.53 tff(c_1222, plain, (ifeq2(eventuality(skc8, skc11), true, true, true)=true)). % 16.69/7.53 tff(c_1666, plain, (specific(skc8, skc10)=true)). % 16.69/7.53 tff(c_92, plain, (![U_107, V_108, W_109]: (ifeq2(accessible_world(U_107, V_108), true, ifeq2(entity(U_107, W_109), true, entity(V_108, W_109), true), true)=true))). % 16.69/7.53 tff(c_1626, plain, (singleton(skc8, skc12)=true)). % 16.69/7.53 tff(c_188, plain, (![U_200, V_201]: (ifeq(tuple(specific(U_200, V_201), general(U_200, V_201)), tuple(true, true), a, b)=b))). % 16.69/7.53 tff(c_1596, plain, (entity(skc8, skc10)=true)). % 16.69/7.53 tff(c_192, plain, (![U_204, V_205]: (ifeq(tuple(nonexistent(U_204, V_205), existent(U_204, V_205)), tuple(true, true), a, b)=b))). % 16.69/7.53 tff(c_1561, plain, (singleton(skc8, skc9)=true)). % 16.69/7.53 tff(c_190, plain, (![U_202, V_203]: (ifeq(tuple(human(U_202, V_203), nonhuman(U_202, V_203)), tuple(true, true), a, b)=b))). % 16.69/7.53 tff(c_1393, plain, (ifeq2(abstraction(skc8, skc12), true, true, true)=true)). % 16.69/7.53 tff(c_1523, plain, (living(skc8, skc10)=true)). % 16.69/7.53 tff(c_186, plain, (![U_198, V_199]: (ifeq(tuple(unisex(U_198, V_199), male(U_198, V_199)), tuple(true, true), a, b)=b))). % 16.69/7.53 tff(c_1482, plain, (impartial(skc8, skc10)=true)). % 16.69/7.53 tff(c_184, plain, (![U_197]: (ifeq2(man(skc11, U_197), true, agent(skc11, skf1(U_197), U_197), true)=true))). % 16.69/7.53 tff(c_1462, plain, (ifeq2(abstraction(skc8, skc9), true, true, true)=true)). % 16.69/7.53 tff(c_1447, plain, (unisex(skc8, skc9)=true)). % 16.69/7.53 tff(c_1410, plain, (organism(skc8, skc10)=true)). % 16.69/7.53 tff(c_1372, plain, (thing(skc8, skc12)=true)). % 16.69/7.53 tff(c_1341, plain, (thing(skc8, skc9)=true)). % 16.69/7.53 tff(c_1313, plain, (animate(skc8, skc10)=true)). % 16.69/7.53 tff(c_10, plain, (![U_12, V_13]: (ifeq2(eventuality(U_12, V_13), true, thing(U_12, V_13), true)=true))). % 16.69/7.53 tff(c_1273, plain, (unisex(skc8, skc12)=true)). % 16.69/7.53 tff(c_1245, plain, (human(skc8, skc10)=true)). % 16.69/7.53 tff(c_28, plain, (![U_30, V_31]: (ifeq2(organism(U_30, V_31), true, entity(U_30, V_31), true)=true))). % 16.69/7.53 tff(c_1208, plain, (nonexistent(skc8, skc9)=true)). % 16.69/7.53 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, unisex(U_20, V_21), true)=true))). % 16.69/7.53 tff(c_1178, plain, (human_person(skc8, skc10)=true)). % 16.69/7.53 tff(c_24, plain, (![U_26, V_27]: (ifeq2(man(U_26, V_27), true, human_person(U_26, V_27), true)=true))). % 16.69/7.53 tff(c_1147, plain, (nonexistent(skc8, skc12)=true)). % 16.69/7.53 tff(c_1120, plain, (ifeq2(smoke(skc8, skc9), true, true, true)=true)). % 16.69/7.53 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, nonexistent(U_18, V_19), true)=true))). % 16.69/7.53 tff(c_1100, plain, (event(skc8, skc9)=true)). % 16.69/7.53 tff(c_1065, plain, (singleton(skc8, skc11)=true)). % 16.69/7.53 tff(c_20, plain, (![U_22, V_23]: (ifeq2(state(U_22, V_23), true, event(U_22, V_23), true)=true))). % 16.69/7.53 tff(c_1041, plain, (ifeq2(entity(skc8, skc9), true, true, true)=true)). % 16.69/7.53 tff(c_1017, plain, (ifeq2(entity(skc8, skc12), true, true, true)=true)). % 16.69/7.53 tff(c_36, plain, (![U_38, V_39]: (ifeq2(organism(U_38, V_39), true, impartial(U_38, V_39), true)=true))). % 16.69/7.53 tff(c_1026, plain, (specific(skc8, skc9)=true)). % 16.69/7.53 tff(c_995, plain, (specific(skc8, skc12)=true)). % 16.69/7.53 tff(c_34, plain, (![U_36, V_37]: (ifeq2(entity(U_36, V_37), true, existent(U_36, V_37), true)=true))). % 16.69/7.53 tff(c_961, plain, (general(skc8, skc13)=true)). % 16.69/7.53 tff(c_14, plain, (![U_16, V_17]: (ifeq2(eventuality(U_16, V_17), true, specific(U_16, V_17), true)=true))). % 16.69/7.53 tff(c_677, plain, (ifeq2(proposition(skc8, skc13), true, true, true)=true)). % 16.69/7.53 tff(c_936, plain, (general(skc8, skc11)=true)). % 16.69/7.53 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, human(U_42, V_43), true)=true))). % 16.69/7.53 tff(c_896, plain, (abstraction(skc8, skc13)=true)). % 16.69/7.53 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, thing(U_32, V_33), true)=true))). % 16.69/7.53 tff(c_865, plain, (unisex(skc8, skc11)=true)). % 16.69/7.53 tff(c_838, plain, (thing(skc8, skc11)=true)). % 16.69/7.53 tff(c_12, plain, (![U_14, V_15]: (ifeq2(thing(U_14, V_15), true, singleton(U_14, V_15), true)=true))). % 16.69/7.53 tff(c_806, plain, (nonhuman(skc8, skc11)=true)). % 16.69/7.53 tff(c_26, plain, (![U_28, V_29]: (ifeq2(human_person(U_28, V_29), true, organism(U_28, V_29), true)=true))). % 16.69/7.53 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, specific(U_34, V_35), true)=true))). % 16.69/7.53 tff(c_741, plain, (male(skc8, skc10)=true)). % 16.69/7.53 tff(c_44, plain, (![U_46, V_47]: (ifeq2(man(U_46, V_47), true, male(U_46, V_47), true)=true))). % 16.69/7.53 tff(c_714, plain, (ifeq2(state(skc8, skc12), true, true, true)=true)). % 16.69/7.53 tff(c_699, plain, (eventuality(skc8, skc12)=true)). % 16.69/7.53 tff(c_22, plain, (![U_24, V_25]: (ifeq2(event(U_24, V_25), true, eventuality(U_24, V_25), true)=true))). % 16.69/7.53 tff(c_659, plain, (relation(skc8, skc13)=true)). % 16.69/7.53 tff(c_42, plain, (![U_44, V_45]: (ifeq2(human_person(U_44, V_45), true, animate(U_44, V_45), true)=true))). % 16.69/7.53 tff(c_619, plain, (abstraction(skc8, skc11)=true)). % 16.69/7.53 tff(c_50, plain, (![U_52, V_53]: (ifeq2(relation(U_52, V_53), true, abstraction(U_52, V_53), true)=true))). % 16.69/7.53 tff(c_566, plain, (ifeq2(relname(skc8, skc11), true, true, true)=true)). % 16.69/7.53 tff(c_48, plain, (![U_50, V_51]: (ifeq2(relname(U_50, V_51), true, relation(U_50, V_51), true)=true))). % 16.69/7.53 tff(c_56, plain, (![U_58, V_59]: (ifeq2(abstraction(U_58, V_59), true, general(U_58, V_59), true)=true))). % 16.69/7.53 tff(c_60, plain, (![U_62, V_63]: (ifeq2(jules_forename(U_62, V_63), true, forename(U_62, V_63), true)=true))). % 16.69/7.53 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, nonhuman(U_56, V_57), true)=true))). % 16.69/7.53 tff(c_515, plain, (ifeq2(smoke(skc8, skc12), true, true, true)=true)). % 16.69/7.53 tff(c_62, plain, (![U_64, V_65]: (ifeq2(smoke(U_64, V_65), true, event(U_64, V_65), true)=true))). % 16.69/7.53 tff(c_491, plain, (relation(skc8, skc11)=true)). % 16.69/7.53 tff(c_58, plain, (![U_60, V_61]: (ifeq2(abstraction(U_60, V_61), true, unisex(U_60, V_61), true)=true))). % 16.69/7.53 tff(c_442, plain, (relname(skc8, skc13)=true)). % 16.69/7.53 tff(c_64, plain, (![U_66, V_67]: (ifeq2(proposition(U_66, V_67), true, relation(U_66, V_67), true)=true))). % 16.69/7.53 tff(c_411, plain, (eventuality(skc8, skc9)=true)). % 16.69/7.53 tff(c_46, plain, (![U_48, V_49]: (ifeq2(forename(U_48, V_49), true, relname(U_48, V_49), true)=true))). % 16.69/7.53 tff(c_349, plain, (be(skc8, skc9, skc10, skc10)=true)). % 16.69/7.53 tff(c_352, plain, (agent(skc8, skc12, skc10)=true)). % 16.69/7.53 tff(c_350, plain, (of(skc8, skc13, skc10)=true)). % 16.69/7.53 tff(c_8, plain, (![U_10, V_11]: (ifeq2(state(U_10, V_11), true, eventuality(U_10, V_11), true)=true))). % 16.69/7.53 tff(c_341, plain, (skc14=skc10)). % 16.69/7.53 tff(c_66, plain, (![U_68, V_69]: (ifeq2(vincent_forename(U_68, V_69), true, forename(U_68, V_69), true)=true))). % 16.69/7.53 tff(c_68, plain, (![U_70, V_71, W_72, X_73]: (ifeq3(be(U_70, V_71, W_72, X_73), true, W_72, X_73)=X_73))). % 16.69/7.53 tff(c_38, plain, (![U_40, V_41]: (ifeq2(organism(U_40, V_41), true, living(U_40, V_41), true)=true))). % 16.69/7.53 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, thing(U_54, V_55), true)=true))). % 16.69/7.53 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 16.69/7.53 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 16.69/7.53 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 16.69/7.53 tff(c_174, plain, (theme(skc8, skc12, skc11)=true)). % 16.69/7.53 tff(c_166, plain, (state(skc8, skc9)=true)). % 16.69/7.53 tff(c_150, plain, (vincent_forename(skc8, skc13)=true)). % 16.69/7.53 tff(c_152, plain, (forename(skc8, skc13)=true)). % 16.69/7.53 tff(c_154, plain, (think_believe_consider(skc8, skc12)=true)). % 16.69/7.53 tff(c_156, plain, (present(skc8, skc12)=true)). % 16.69/7.53 tff(c_158, plain, (event(skc8, skc12)=true)). % 16.69/7.53 tff(c_160, plain, (proposition(skc8, skc11)=true)). % 16.69/7.53 tff(c_162, plain, (accessible_world(skc8, skc11)=true)). % 16.69/7.53 tff(c_164, plain, (man(skc8, skc10)=true)). % 16.69/7.53 tff(c_142, plain, (actual_world(skc8)=true)). % 16.69/7.53 tff(c_194, plain, (b!=a)). % 16.69/7.53 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.69/7.53 %------------------------------------------------------------------------------