%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP224-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:39 PM UTC 2025 % Result : Satisfiable 19.58s 10.04s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP224-10 : TPTP v9.0.0. Released v7.5.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 09:29:03 EDT 2025 % 0.13/0.34 % CPUTime : % 19.58/10.03 % 19.58/10.04 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.58/10.04 % 19.58/10.04 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.58/10.04 %$ 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 > skc17 > skc16 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 > b > a % 19.58/10.04 % 19.58/10.04 %Foreground sorts: % 19.58/10.04 % 19.58/10.04 % 19.58/10.04 %Background operators: % 19.58/10.04 % 19.58/10.04 % 19.58/10.04 %Foreground operators: % 19.58/10.04 tff(agent, type, agent: ($i * $i * $i) > $i). % 19.58/10.04 tff(skc16, type, skc16: $i). % 19.58/10.04 tff(proposition, type, proposition: ($i * $i) > $i). % 19.58/10.04 tff(specific, type, specific: ($i * $i) > $i). % 19.58/10.04 tff(organism, type, organism: ($i * $i) > $i). % 19.58/10.04 tff(impartial, type, impartial: ($i * $i) > $i). % 19.58/10.04 tff(skc11, type, skc11: $i). % 19.58/10.04 tff(a, type, a: $i). % 19.58/10.04 tff(smoke, type, smoke: ($i * $i) > $i). % 19.58/10.04 tff(jules_forename, type, jules_forename: ($i * $i) > $i). % 19.58/10.04 tff(skc9, type, skc9: $i). % 19.58/10.04 tff(eventuality, type, eventuality: ($i * $i) > $i). % 19.58/10.04 tff(theme, type, theme: ($i * $i * $i) > $i). % 19.58/10.04 tff(state, type, state: ($i * $i) > $i). % 19.58/10.04 tff(tuple, type, tuple: ($i * $i) > $i). % 19.58/10.04 tff(human_person, type, human_person: ($i * $i) > $i). % 19.58/10.04 tff(skf1, type, skf1: $i > $i). % 19.58/10.04 tff(be, type, be: ($i * $i * $i * $i) > $i). % 19.58/10.04 tff(relname, type, relname: ($i * $i) > $i). % 19.58/10.04 tff(skc14, type, skc14: $i). % 19.58/10.04 tff(skc17, type, skc17: $i). % 19.58/10.04 tff(skc13, type, skc13: $i). % 19.58/10.04 tff(thing, type, thing: ($i * $i) > $i). % 19.58/10.04 tff(unisex, type, unisex: ($i * $i) > $i). % 19.58/10.04 tff(abstraction, type, abstraction: ($i * $i) > $i). % 19.58/10.04 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 19.58/10.04 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 19.58/10.04 tff(relation, type, relation: ($i * $i) > $i). % 19.58/10.04 tff(actual_world, type, actual_world: $i > $i). % 19.58/10.04 tff(of, type, of: ($i * $i * $i) > $i). % 19.58/10.04 tff(present, type, present: ($i * $i) > $i). % 19.58/10.04 tff(b, type, b: $i). % 19.58/10.04 tff(animate, type, animate: ($i * $i) > $i). % 19.58/10.04 tff(human, type, human: ($i * $i) > $i). % 19.58/10.04 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 19.58/10.04 tff(skc15, type, skc15: $i). % 19.58/10.04 tff(existent, type, existent: ($i * $i) > $i). % 19.58/10.04 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 19.58/10.04 tff(forename, type, forename: ($i * $i) > $i). % 19.58/10.04 tff(true, type, true: $i). % 19.58/10.04 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 19.58/10.04 tff(male, type, male: ($i * $i) > $i). % 19.58/10.04 tff(skc12, type, skc12: $i). % 19.58/10.04 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 19.58/10.04 tff(entity, type, entity: ($i * $i) > $i). % 19.58/10.04 tff(skc10, type, skc10: $i). % 19.58/10.04 tff(singleton, type, singleton: ($i * $i) > $i). % 19.58/10.04 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 19.58/10.04 tff(event, type, event: ($i * $i) > $i). % 19.58/10.04 tff(man, type, man: ($i * $i) > $i). % 19.58/10.04 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 19.58/10.04 tff(general, type, general: ($i * $i) > $i). % 19.58/10.04 tff(living, type, living: ($i * $i) > $i). % 19.58/10.04 % 19.58/10.04 %Saturated clause set: % 19.58/10.05 tff(c_7945, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skf1(skc17), V_190), true, ifeq3(agent(skc14, Y_189, skc17), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.05 tff(c_7775, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skf1(skc11), V_190), true, ifeq3(agent(skc14, Y_189, skc11), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.05 tff(c_18391, plain, (![W_1089, V_1091]: (ifeq3(theme(skc14, skf1(skc11), W_1089), true, ifeq3(theme(skc14, skf1(skc11), V_1091), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1089), true, ifeq3(proposition(skc14, V_1091), true, V_1091, W_1089), W_1089), W_1089), W_1089), W_1089), W_1089)=W_1089))). % 19.58/10.05 tff(c_18024, plain, (![W_1070, V_1072]: (ifeq3(theme(skc14, skf1(skc17), W_1070), true, ifeq3(theme(skc14, skf1(skc17), V_1072), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_1070), true, ifeq3(proposition(skc14, V_1072), true, V_1072, W_1070), W_1070), W_1070), W_1070), W_1070), W_1070)=W_1070))). % 19.58/10.05 tff(c_7774, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skf1(skc11), W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.05 tff(c_17672, plain, (![Y_1047, V_1049]: (ifeq3(theme(skc14, Y_1047, skc14), true, ifeq3(theme(skc14, skf1(skc17), V_1049), true, ifeq3(agent(skc14, Y_1047, skc17), true, ifeq3(think_believe_consider(skc14, Y_1047), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, V_1049), true, V_1049, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17810, plain, (![W_1056, X_1057]: (ifeq3(theme(skc14, skf1(skc11), W_1056), true, ifeq3(theme(skc14, X_1057, skc14), true, ifeq3(agent(skc14, X_1057, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, X_1057), true, ifeq3(proposition(skc14, W_1056), true, skc14, W_1056), W_1056), W_1056), W_1056), W_1056), W_1056)=W_1056))). % 19.58/10.05 tff(c_17382, plain, (![W_1028, V_1030]: (ifeq3(theme(skc14, skc15, W_1028), true, ifeq3(theme(skc14, skf1(skc11), V_1030), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1028), true, ifeq3(proposition(skc14, V_1030), true, V_1030, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.58/10.05 tff(c_17673, plain, (![X_1048, V_1049]: (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(theme(skc14, X_1048, V_1049), true, ifeq3(agent(skc14, X_1048, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, X_1048), true, ifeq3(proposition(skc14, V_1049), true, V_1049, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17808, plain, (![W_1056, X_1057]: (ifeq3(theme(skc14, skf1(skc17), W_1056), true, ifeq3(theme(skc14, X_1057, skc14), true, ifeq3(agent(skc14, X_1057, skc17), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, X_1057), true, ifeq3(proposition(skc14, W_1056), true, skc14, W_1056), W_1056), W_1056), W_1056), W_1056), W_1056)=W_1056))). % 19.58/10.05 tff(c_18120, plain, (![V_1077]: (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(theme(skc14, skf1(skc17), V_1077), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, V_1077), true, V_1077, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17671, plain, (![X_1048, V_1049]: (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(theme(skc14, X_1048, V_1049), true, ifeq3(agent(skc14, X_1048, skc17), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, X_1048), true, ifeq3(proposition(skc14, V_1049), true, V_1049, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_18061, plain, (![W_1074]: (ifeq3(theme(skc14, skf1(skc11), W_1074), true, ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1074), true, skc14, W_1074), W_1074), W_1074), W_1074), W_1074)=W_1074))). % 19.58/10.05 tff(c_17811, plain, (![Y_1055, W_1056]: (ifeq3(theme(skc14, Y_1055, W_1056), true, ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(agent(skc14, Y_1055, skc11), true, ifeq3(think_believe_consider(skc14, Y_1055), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1056), true, skc14, W_1056), W_1056), W_1056), W_1056), W_1056), W_1056)=W_1056))). % 19.58/10.05 tff(c_7944, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skf1(skc17), W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc17), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.05 tff(c_17982, plain, (![V_1068]: (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(theme(skc14, skf1(skc11), V_1068), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, V_1068), true, V_1068, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17674, plain, (![Y_1047, V_1049]: (ifeq3(theme(skc14, Y_1047, skc14), true, ifeq3(theme(skc14, skf1(skc11), V_1049), true, ifeq3(agent(skc14, Y_1047, skc11), true, ifeq3(think_believe_consider(skc14, Y_1047), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, V_1049), true, V_1049, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17924, plain, (![W_1063]: (ifeq3(theme(skc14, skf1(skc17), W_1063), true, ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_1063), true, skc14, W_1063), W_1063), W_1063), W_1063), W_1063)=W_1063))). % 19.58/10.05 tff(c_17488, plain, (![W_1036, V_1037]: (ifeq3(theme(skc14, skf1(skc11), W_1036), true, ifeq3(theme(skc14, skc15, V_1037), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1036), true, ifeq3(proposition(skc14, V_1037), true, V_1037, W_1036), W_1036), W_1036), W_1036), W_1036), W_1036)=W_1036))). % 19.58/10.05 tff(c_17809, plain, (![Y_1055, W_1056]: (ifeq3(theme(skc14, Y_1055, W_1056), true, ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(agent(skc14, Y_1055, skc17), true, ifeq3(think_believe_consider(skc14, Y_1055), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_1056), true, skc14, W_1056), W_1056), W_1056), W_1056), W_1056), W_1056)=W_1056))). % 19.58/10.05 tff(c_17722, plain, (![Y_1051]: (ifeq3(theme(skc14, Y_1051, skc14), true, ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(agent(skc14, Y_1051, skc11), true, ifeq3(think_believe_consider(skc14, Y_1051), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17720, plain, (![Y_1051]: (ifeq3(theme(skc14, Y_1051, skc14), true, ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(agent(skc14, Y_1051, skc17), true, ifeq3(think_believe_consider(skc14, Y_1051), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17835, plain, (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 19.58/10.05 tff(c_17721, plain, (![X_1052]: (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(theme(skc14, X_1052, skc14), true, ifeq3(agent(skc14, X_1052, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(think_believe_consider(skc14, X_1052), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_4201, plain, (![Y_189, W_185, X_188, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, X_188, skc14), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, skc14, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.05 tff(c_17748, plain, (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 19.58/10.05 tff(c_17719, plain, (![X_1052]: (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(theme(skc14, X_1052, skc14), true, ifeq3(agent(skc14, X_1052, skc17), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(think_believe_consider(skc14, X_1052), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17679, plain, (![Y_1047, X_1048, Z_1050]: (ifeq3(theme(skc14, Y_1047, skc14), true, ifeq3(theme(skc14, X_1048, skc14), true, ifeq3(agent(skc14, Y_1047, Z_1050), true, ifeq3(agent(skc14, X_1048, Z_1050), true, ifeq3(think_believe_consider(skc14, Y_1047), true, ifeq3(think_believe_consider(skc14, X_1048), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_4200, plain, (![Y_189, X_188, V_190, Z_187]: (ifeq3(theme(skc14, Y_189, skc14), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, V_190), true, V_190, skc14), skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.05 tff(c_17608, plain, (![V_1044]: (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(theme(skc14, skc15, V_1044), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, V_1044), true, V_1044, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_17493, plain, (![Y_1035, V_1037, Z_1038]: (ifeq3(theme(skc14, Y_1035, skc14), true, ifeq3(theme(skc14, skc15, V_1037), true, ifeq3(agent(skc14, Y_1035, Z_1038), true, ifeq3(agent(skc14, skc15, Z_1038), true, ifeq3(think_believe_consider(skc14, Y_1035), true, ifeq3(proposition(skc14, V_1037), true, V_1037, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_17389, plain, (![W_1028, V_1030, Z_1031]: (ifeq3(theme(skc14, skc15, W_1028), true, ifeq3(theme(skc14, skc15, V_1030), true, ifeq3(agent(skc14, skc15, Z_1031), true, ifeq3(agent(skc14, skc15, Z_1031), true, ifeq3(proposition(skc14, W_1028), true, ifeq3(proposition(skc14, V_1030), true, V_1030, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.58/10.06 tff(c_17434, plain, (![W_1032]: (ifeq3(theme(skc14, skc15, W_1032), true, ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_1032), true, skc14, W_1032), W_1032), W_1032), W_1032), W_1032)=W_1032))). % 19.58/10.06 tff(c_3958, plain, (![Y_189, W_185, V_190, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc15, V_190), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.06 tff(c_17388, plain, (![W_1028, X_1029, Z_1031]: (ifeq3(theme(skc14, skc15, W_1028), true, ifeq3(theme(skc14, X_1029, skc14), true, ifeq3(agent(skc14, skc15, Z_1031), true, ifeq3(agent(skc14, X_1029, Z_1031), true, ifeq3(think_believe_consider(skc14, X_1029), true, ifeq3(proposition(skc14, W_1028), true, skc14, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.58/10.06 tff(c_3957, plain, (![W_185, X_188, V_190, Z_187]: (ifeq3(theme(skc14, skc15, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.06 tff(c_13749, plain, (![Y_822, X_823, Z_825]: (ifeq3(theme(skc9, Y_822, skc14), true, ifeq3(theme(skc9, X_823, skc14), true, ifeq3(agent(skc9, Y_822, Z_825), true, ifeq3(agent(skc9, X_823, Z_825), true, ifeq3(think_believe_consider(skc9, Y_822), true, ifeq3(think_believe_consider(skc9, X_823), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_13375, plain, (![W_796, V_798, Z_799]: (ifeq3(theme(skc9, skc15, W_796), true, ifeq3(theme(skc9, skc15, V_798), true, ifeq3(agent(skc9, skc15, Z_799), true, ifeq3(agent(skc9, skc15, Z_799), true, ifeq3(proposition(skc9, W_796), true, ifeq3(proposition(skc9, V_798), true, V_798, W_796), W_796), W_796), W_796), W_796), W_796)=W_796))). % 19.58/10.06 tff(c_17184, plain, (![W_1015, V_1016]: (ifeq3(theme(skc14, skf1(skc17), W_1015), true, ifeq3(theme(skc14, skc15, V_1016), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_1015), true, ifeq3(proposition(skc14, V_1016), true, V_1016, W_1015), W_1015), W_1015), W_1015), W_1015)=W_1015))). % 19.58/10.06 tff(c_17237, plain, (![V_1018]: (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(theme(skc14, skc15, V_1018), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, V_1018), true, V_1018, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_17188, plain, (![Y_1014, V_1016]: (ifeq3(theme(skc14, Y_1014, skc14), true, ifeq3(theme(skc14, skc15, V_1016), true, ifeq3(agent(skc14, Y_1014, skc17), true, ifeq3(think_believe_consider(skc14, Y_1014), true, ifeq3(proposition(skc14, V_1016), true, V_1016, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_6336, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc15, V_190), true, ifeq3(agent(skc14, Y_189, skc17), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.06 tff(c_16933, plain, (![W_999, V_1001]: (ifeq3(theme(skc14, skc15, W_999), true, ifeq3(theme(skc14, skf1(skc17), V_1001), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_999), true, ifeq3(proposition(skc14, V_1001), true, V_1001, W_999), W_999), W_999), W_999), W_999)=W_999))). % 19.58/10.06 tff(c_17037, plain, (![W_1006]: (ifeq3(theme(skc14, skc15, W_1006), true, ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_1006), true, skc14, W_1006), W_1006), W_1006), W_1006)=W_1006))). % 19.58/10.06 tff(c_13377, plain, (![W_796, X_797, Z_799]: (ifeq3(theme(skc9, skc15, W_796), true, ifeq3(theme(skc9, X_797, skc14), true, ifeq3(agent(skc9, skc15, Z_799), true, ifeq3(agent(skc9, X_797, Z_799), true, ifeq3(think_believe_consider(skc9, X_797), true, ifeq3(proposition(skc9, W_796), true, skc14, W_796), W_796), W_796), W_796), W_796), W_796)=W_796))). % 19.58/10.06 tff(c_16938, plain, (![W_999, X_1000]: (ifeq3(theme(skc14, skc15, W_999), true, ifeq3(theme(skc14, X_1000, skc14), true, ifeq3(agent(skc14, X_1000, skc17), true, ifeq3(think_believe_consider(skc14, X_1000), true, ifeq3(proposition(skc14, W_999), true, skc14, W_999), W_999), W_999), W_999), W_999)=W_999))). % 19.58/10.06 tff(c_16675, plain, (![W_985]: (ifeq3(theme(skc14, skf1(skc11), W_985), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, W_985), true, skc14, W_985), W_985), W_985), W_985)=W_985))). % 19.58/10.06 tff(c_16492, plain, (![V_973]: (ifeq3(theme(skc14, skf1(skc11), V_973), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, ifeq3(proposition(skc14, V_973), true, V_973, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16934, plain, (![W_999, V_1001]: (ifeq3(theme(skc14, skc15, W_999), true, ifeq3(theme(skc14, skc15, V_1001), true, ifeq3(proposition(skc14, W_999), true, ifeq3(proposition(skc14, V_1001), true, V_1001, W_999), W_999), W_999), W_999)=W_999))). % 19.58/10.06 tff(c_6335, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skc15, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc17), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.06 tff(c_16680, plain, (![W_985, Z_986]: (ifeq3(theme(skc14, skc15, W_985), true, ifeq3(agent(skc14, skc15, Z_986), true, ifeq3(agent(skc14, skc15, Z_986), true, ifeq3(proposition(skc14, W_985), true, skc14, W_985), W_985), W_985), W_985)=W_985))). % 19.58/10.06 tff(c_16679, plain, (![Y_984, Z_986]: (ifeq3(theme(skc14, Y_984, skc14), true, ifeq3(agent(skc14, Y_984, Z_986), true, ifeq3(agent(skc14, skc15, Z_986), true, ifeq3(think_believe_consider(skc14, Y_984), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16819, plain, (ifeq3(theme(skc14, skf1(skc11), skc14), true, ifeq3(agent(skc14, skc15, skc11), true, ifeq3(think_believe_consider(skc14, skf1(skc11)), true, skc14, skc14), skc14), skc14)=skc14)). % 19.58/10.06 tff(c_16496, plain, (![X_972, Z_974]: (ifeq3(theme(skc14, X_972, skc14), true, ifeq3(agent(skc14, skc15, Z_974), true, ifeq3(agent(skc14, X_972, Z_974), true, ifeq3(think_believe_consider(skc14, X_972), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16497, plain, (![V_973, Z_974]: (ifeq3(theme(skc14, skc15, V_973), true, ifeq3(agent(skc14, skc15, Z_974), true, ifeq3(agent(skc14, skc15, Z_974), true, ifeq3(proposition(skc14, V_973), true, V_973, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16677, plain, (![Y_984, W_985]: (ifeq3(theme(skc14, Y_984, W_985), true, ifeq3(agent(skc14, Y_984, skc17), true, ifeq3(think_believe_consider(skc14, Y_984), true, ifeq3(proposition(skc14, W_985), true, skc14, W_985), W_985), W_985), W_985)=W_985))). % 19.58/10.06 tff(c_16674, plain, (![W_985]: (ifeq3(theme(skc14, skf1(skc17), W_985), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, W_985), true, skc14, W_985), W_985), W_985)=W_985))). % 19.58/10.06 tff(c_16676, plain, (![W_985]: (ifeq3(theme(skc14, skc15, W_985), true, ifeq3(proposition(skc14, W_985), true, skc14, W_985), W_985)=W_985))). % 19.58/10.06 tff(c_6301, plain, (![Y_189, W_185, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, skc14, W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.58/10.06 tff(c_16609, plain, (![X_981]: (ifeq3(theme(skc14, X_981, skc14), true, ifeq3(agent(skc14, X_981, skc17), true, ifeq3(think_believe_consider(skc14, X_981), true, skc14, skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16493, plain, (![X_972, V_973]: (ifeq3(theme(skc14, X_972, V_973), true, ifeq3(agent(skc14, X_972, skc17), true, ifeq3(think_believe_consider(skc14, X_972), true, ifeq3(proposition(skc14, V_973), true, V_973, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16538, plain, (ifeq3(theme(skc14, skf1(skc17), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, skc14, skc14), skc14)=skc14)). % 19.58/10.06 tff(c_13558, plain, (![Y_809, V_811, Z_812]: (ifeq3(theme(skc9, Y_809, skc14), true, ifeq3(theme(skc9, skc15, V_811), true, ifeq3(agent(skc9, Y_809, Z_812), true, ifeq3(agent(skc9, skc15, Z_812), true, ifeq3(think_believe_consider(skc9, Y_809), true, ifeq3(proposition(skc9, V_811), true, V_811, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16491, plain, (![V_973]: (ifeq3(theme(skc14, skf1(skc17), V_973), true, ifeq3(think_believe_consider(skc14, skf1(skc17)), true, ifeq3(proposition(skc14, V_973), true, V_973, skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16495, plain, (![Z_974]: (ifeq3(agent(skc14, skc15, Z_974), true, ifeq3(agent(skc14, skc15, Z_974), true, skc14, skc14), skc14)=skc14))). % 19.58/10.06 tff(c_16494, plain, (![V_973]: (ifeq3(theme(skc14, skc15, V_973), true, ifeq3(proposition(skc14, V_973), true, V_973, skc14), skc14)=skc14))). % 19.58/10.06 tff(c_6300, plain, (![X_188, V_190, Z_187]: (ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, V_190), true, V_190, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_13961, plain, (![W_836, X_837]: (ifeq3(theme(skc9, skc15, W_836), true, ifeq3(theme(skc9, X_837, skc14), true, ifeq3(agent(skc9, X_837, skc17), true, ifeq3(think_believe_consider(skc9, X_837), true, ifeq3(proposition(skc9, W_836), true, skc14, W_836), W_836), W_836), W_836), W_836)=W_836))). % 19.58/10.06 tff(c_13176, plain, (![Y_784, V_786]: (ifeq3(theme(skc9, Y_784, skc14), true, ifeq3(theme(skc9, skc15, V_786), true, ifeq3(agent(skc9, Y_784, skc17), true, ifeq3(think_believe_consider(skc9, Y_784), true, ifeq3(proposition(skc9, V_786), true, V_786, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_12604, plain, (![V_749, Z_750]: (ifeq3(theme(skc9, skc15, V_749), true, ifeq3(agent(skc9, skc15, Z_750), true, ifeq3(agent(skc9, skc15, Z_750), true, ifeq3(proposition(skc9, V_749), true, V_749, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_13746, plain, (![Y_822, Z_825]: (ifeq3(theme(skc9, Y_822, skc14), true, ifeq3(agent(skc9, Y_822, Z_825), true, ifeq3(agent(skc9, skc15, Z_825), true, ifeq3(think_believe_consider(skc9, Y_822), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_13963, plain, (![X_837, Z_838]: (ifeq3(theme(skc9, X_837, skc14), true, ifeq3(agent(skc9, skc15, Z_838), true, ifeq3(agent(skc9, X_837, Z_838), true, ifeq3(think_believe_consider(skc9, X_837), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.06 tff(c_5806, plain, (![W_182, V_184]: (ifeq3(of(skc14, W_182, skc17), true, ifeq3(of(skc14, V_184, skc17), true, ifeq3(forename(skc14, W_182), true, ifeq3(forename(skc14, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 19.58/10.06 tff(c_5479, plain, (![W_182, V_184]: (ifeq3(of(skc14, W_182, skc11), true, ifeq3(of(skc14, V_184, skc11), true, ifeq3(forename(skc14, W_182), true, ifeq3(forename(skc14, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 19.58/10.06 tff(c_3790, plain, (![W_405, V_407]: (ifeq3(of(skc9, W_405, skc11), true, ifeq3(of(skc9, V_407, skc11), true, ifeq3(forename(skc9, W_405), true, ifeq3(forename(skc9, V_407), true, W_405, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.06 tff(c_3789, plain, (![W_405, V_407]: (ifeq3(of(skc9, W_405, skc17), true, ifeq3(of(skc9, V_407, skc17), true, ifeq3(forename(skc9, W_405), true, ifeq3(forename(skc9, V_407), true, W_405, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.06 tff(c_16117, plain, (![V_952]: (ifeq3(of(skc14, skc12, skc17), true, ifeq3(of(skc14, V_952, skc17), true, ifeq3(forename(skc14, V_952), true, skc12, V_952), V_952), V_952)=V_952))). % 19.58/10.06 tff(c_3785, plain, (![X_406, V_407]: (ifeq3(of(skc14, skc12, X_406), true, ifeq3(of(skc14, V_407, X_406), true, ifeq3(forename(skc14, V_407), true, ifeq3(entity(skc14, X_406), true, skc12, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.06 tff(c_15995, plain, (![W_946]: (ifeq3(of(skc14, W_946, skc17), true, ifeq3(of(skc14, skc12, skc17), true, ifeq3(forename(skc14, W_946), true, W_946, skc12), skc12), skc12)=skc12))). % 19.58/10.06 tff(c_15938, plain, (![W_943]: (ifeq3(of(skc14, W_943, skc11), true, ifeq3(of(skc14, skc16, skc11), true, ifeq3(forename(skc14, W_943), true, W_943, skc16), skc16), skc16)=skc16))). % 19.58/10.06 tff(c_16020, plain, (ifeq3(of(skc14, skc12, skc17), true, ifeq3(of(skc14, skc12, skc17), true, skc12, skc12), skc12)=skc12)). % 19.58/10.06 tff(c_15997, plain, (![X_947]: (ifeq3(of(skc14, skc12, X_947), true, ifeq3(of(skc14, skc12, X_947), true, ifeq3(entity(skc14, X_947), true, skc12, skc12), skc12), skc12)=skc12))). % 19.58/10.06 tff(c_3786, plain, (![W_405, X_406]: (ifeq3(of(skc14, W_405, X_406), true, ifeq3(of(skc14, skc12, X_406), true, ifeq3(forename(skc14, W_405), true, ifeq3(entity(skc14, X_406), true, W_405, skc12), skc12), skc12), skc12)=skc12))). % 19.58/10.06 tff(c_15939, plain, (![X_944]: (ifeq3(of(skc14, skc12, X_944), true, ifeq3(of(skc14, skc16, X_944), true, ifeq3(entity(skc14, X_944), true, skc12, skc16), skc16), skc16)=skc16))). % 19.58/10.06 tff(c_3788, plain, (![W_405, X_406]: (ifeq3(of(skc14, W_405, X_406), true, ifeq3(of(skc14, skc16, X_406), true, ifeq3(forename(skc14, W_405), true, ifeq3(entity(skc14, X_406), true, W_405, skc16), skc16), skc16), skc16)=skc16))). % 19.58/10.07 tff(c_15797, plain, (![V_937]: (ifeq3(of(skc14, skc16, skc11), true, ifeq3(of(skc14, V_937, skc11), true, ifeq3(forename(skc14, V_937), true, skc16, V_937), V_937), V_937)=V_937))). % 19.58/10.07 tff(c_13374, plain, (![W_796, Z_799]: (ifeq3(theme(skc9, skc15, W_796), true, ifeq3(agent(skc9, skc15, Z_799), true, ifeq3(agent(skc9, skc15, Z_799), true, ifeq3(proposition(skc9, W_796), true, skc14, W_796), W_796), W_796), W_796)=W_796))). % 19.58/10.07 tff(c_15798, plain, (![X_936]: (ifeq3(of(skc14, skc16, X_936), true, ifeq3(of(skc14, skc12, X_936), true, ifeq3(entity(skc14, X_936), true, skc16, skc12), skc12), skc12)=skc12))). % 19.58/10.07 tff(c_15822, plain, (ifeq3(of(skc14, skc16, skc11), true, ifeq3(of(skc14, skc16, skc11), true, skc16, skc16), skc16)=skc16)). % 19.58/10.07 tff(c_15799, plain, (![X_936]: (ifeq3(of(skc14, skc16, X_936), true, ifeq3(of(skc14, skc16, X_936), true, ifeq3(entity(skc14, X_936), true, skc16, skc16), skc16), skc16)=skc16))). % 19.58/10.07 tff(c_3787, plain, (![X_406, V_407]: (ifeq3(of(skc14, skc16, X_406), true, ifeq3(of(skc14, V_407, X_406), true, ifeq3(forename(skc14, V_407), true, ifeq3(entity(skc14, X_406), true, skc16, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.07 tff(c_12959, plain, (![X_773, V_774]: (ifeq3(theme(skc9, X_773, V_774), true, ifeq3(agent(skc9, X_773, skc17), true, ifeq3(think_believe_consider(skc9, X_773), true, ifeq3(proposition(skc9, V_774), true, V_774, skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.07 tff(c_15699, plain, (![Y_931]: (ifeq3(theme(skc9, Y_931, skc14), true, ifeq3(agent(skc9, Y_931, skc17), true, ifeq3(think_believe_consider(skc9, Y_931), true, skc14, skc14), skc14), skc14)=skc14))). % 19.58/10.07 tff(c_13962, plain, (![Y_835, W_836]: (ifeq3(theme(skc9, Y_835, W_836), true, ifeq3(agent(skc9, Y_835, skc17), true, ifeq3(think_believe_consider(skc9, Y_835), true, ifeq3(proposition(skc9, W_836), true, skc14, W_836), W_836), W_836), W_836)=W_836))). % 19.58/10.07 tff(c_12417, plain, (![W_738]: (ifeq3(of(skc9, W_738, skc11), true, ifeq3(of(skc9, skc16, skc11), true, ifeq3(forename(skc9, W_738), true, W_738, skc16), skc16), skc16)=skc16))). % 19.58/10.07 tff(c_13553, plain, (![W_810, V_811]: (ifeq3(theme(skc9, skc15, W_810), true, ifeq3(theme(skc9, skc15, V_811), true, ifeq3(proposition(skc9, W_810), true, ifeq3(proposition(skc9, V_811), true, V_811, W_810), W_810), W_810), W_810)=W_810))). % 19.58/10.07 tff(c_11922, plain, (![V_711]: (ifeq3(of(skc9, skc16, skc11), true, ifeq3(of(skc9, V_711, skc11), true, ifeq3(forename(skc9, V_711), true, skc16, V_711), V_711), V_711)=V_711))). % 19.58/10.07 tff(c_12243, plain, (![V_729]: (ifeq3(of(skc9, skc12, skc17), true, ifeq3(of(skc9, V_729, skc17), true, ifeq3(forename(skc9, V_729), true, skc12, V_729), V_729), V_729)=V_729))). % 19.58/10.07 tff(c_12072, plain, (![W_718]: (ifeq3(of(skc9, W_718, skc17), true, ifeq3(of(skc9, skc12, skc17), true, ifeq3(forename(skc9, W_718), true, W_718, skc12), skc12), skc12)=skc12))). % 19.58/10.07 tff(c_15052, plain, (ifeq3(of(skc9, skc12, skc17), true, ifeq3(of(skc9, skc12, skc17), true, skc12, skc12), skc12)=skc12)). % 19.58/10.07 tff(c_15519, plain, (ifeq3(of(skc9, skc16, skc11), true, ifeq3(of(skc9, skc16, skc11), true, skc16, skc16), skc16)=skc16)). % 19.58/10.07 tff(c_15487, plain, (![V_922]: (ifeq2(accessible_world(skc14, V_922), true, agent(V_922, skf1(skc17), skc17), true)=true))). % 19.58/10.07 tff(c_11927, plain, (![X_710]: (ifeq3(of(skc9, skc16, X_710), true, ifeq3(of(skc9, skc16, X_710), true, ifeq3(entity(skc9, X_710), true, skc16, skc16), skc16), skc16)=skc16))). % 19.58/10.07 tff(c_7768, plain, (![U_168]: (ifeq2(agent(U_168, skf1(skc11), skc11), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_7938, plain, (![U_168]: (ifeq2(agent(U_168, skf1(skc17), skc17), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_15414, plain, (![V_918]: (ifeq2(accessible_world(skc14, V_918), true, agent(V_918, skf1(skc11), skc11), true)=true))). % 19.58/10.07 tff(c_9350, plain, (![U_177]: (ifeq2(be(U_177, skc10, skc11, skc11), true, ifeq2(accessible_world(U_177, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_15347, plain, (![V_915]: (ifeq2(accessible_world(skc14, V_915), true, be(V_915, skc10, skc11, skc11), true)=true))). % 19.58/10.07 tff(c_3669, plain, (![U_402]: (ifeq2(be(U_402, skc10, skc11, skc11), true, ifeq2(accessible_world(U_402, skc9), true, true, true), true)=true))). % 19.58/10.07 tff(c_15273, plain, (![V_912]: (ifeq2(accessible_world(skc9, V_912), true, be(V_912, skc10, skc11, skc11), true)=true))). % 19.58/10.07 tff(c_6911, plain, (![U_83, V_465]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skf1(V_465)), true, true, true), true)=true))). % 19.58/10.07 tff(c_6752, plain, (![U_86, V_456]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(specific(U_86, skf1(V_456)), true, true, true), true)=true))). % 19.58/10.07 tff(c_6683, plain, (![U_92, V_453]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skf1(V_453)), true, true, true), true)=true))). % 19.58/10.07 tff(c_6841, plain, (![U_89, V_460]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(nonexistent(U_89, skf1(V_460)), true, true, true), true)=true))). % 19.58/10.07 tff(c_15185, plain, (ifeq3(of(skc14, skc12, skc17), true, skc16, skc12)=skc12)). % 19.58/10.07 tff(c_6370, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc17), true, ifeq3(forename(skc14, V_184), true, skc16, V_184), V_184)=V_184))). % 19.58/10.07 tff(c_15151, plain, (ifeq3(of(skc14, skc16, skc11), true, skc12, skc16)=skc16)). % 19.58/10.07 tff(c_6420, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc11), true, ifeq3(forename(skc14, V_184), true, skc12, V_184), V_184)=V_184))). % 19.58/10.07 tff(c_15096, plain, (ifeq3(of(skc14, skc12, skc17), true, skc12, skc16)=skc16)). % 19.58/10.07 tff(c_6795, plain, (![U_80, V_458]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skf1(V_458)), true, true, true), true)=true))). % 19.58/10.07 tff(c_6371, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc17), true, ifeq3(forename(skc14, W_182), true, W_182, skc16), skc16)=skc16))). % 19.58/10.07 tff(c_15074, plain, (ifeq3(of(skc14, skc16, skc11), true, skc16, skc12)=skc12)). % 19.58/10.07 tff(c_6421, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc11), true, ifeq3(forename(skc14, W_182), true, W_182, skc12), skc12)=skc12))). % 19.58/10.07 tff(c_12248, plain, (![X_728]: (ifeq3(of(skc9, skc12, X_728), true, ifeq3(of(skc9, skc12, X_728), true, ifeq3(entity(skc9, X_728), true, skc12, skc12), skc12), skc12)=skc12))). % 19.58/10.07 tff(c_6630, plain, (![U_77, V_451]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(eventuality(U_77, skf1(V_451)), true, true, true), true)=true))). % 19.58/10.07 tff(c_6561, plain, (![U_149, V_446]: (ifeq2(accessible_world(U_149, skc14), true, ifeq2(smoke(U_149, skf1(V_446)), true, true, true), true)=true))). % 19.58/10.07 tff(c_14937, plain, (![V_888, V_889]: (ifeq2(accessible_world(skc14, V_888), true, present(V_888, skf1(V_889)), true)=true))). % 19.58/10.07 tff(c_12078, plain, (![X_719]: (ifeq3(of(skc9, skc16, X_719), true, ifeq3(of(skc9, skc12, X_719), true, ifeq3(entity(skc9, X_719), true, skc16, skc12), skc12), skc12)=skc12))). % 19.58/10.07 tff(c_11924, plain, (![V_711]: (ifeq3(of(skc9, V_711, skc17), true, ifeq3(forename(skc9, V_711), true, skc16, V_711), V_711)=V_711))). % 19.58/10.07 tff(c_6520, plain, (![U_95, V_444]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(event(U_95, skf1(V_444)), true, true, true), true)=true))). % 19.58/10.07 tff(c_12245, plain, (![V_729]: (ifeq3(of(skc9, V_729, skc11), true, ifeq3(forename(skc9, V_729), true, skc12, V_729), V_729)=V_729))). % 19.58/10.07 tff(c_12420, plain, (![W_738]: (ifeq3(of(skc9, W_738, skc17), true, ifeq3(forename(skc9, W_738), true, W_738, skc16), skc16)=skc16))). % 19.58/10.07 tff(c_6451, plain, (![U_152, V_440]: (ifeq2(present(U_152, skf1(V_440)), true, ifeq2(accessible_world(U_152, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_12249, plain, (![X_728]: (ifeq3(of(skc9, skc12, X_728), true, ifeq3(of(skc9, skc16, X_728), true, ifeq3(entity(skc9, X_728), true, skc12, skc16), skc16), skc16)=skc16))). % 19.58/10.07 tff(c_12075, plain, (![W_718]: (ifeq3(of(skc9, W_718, skc11), true, ifeq3(forename(skc9, W_718), true, W_718, skc12), skc12)=skc12))). % 19.58/10.07 tff(c_6416, plain, (![U_164]: (ifeq2(of(U_164, skc12, skc11), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_14707, plain, (![V_876]: (ifeq2(accessible_world(skc14, V_876), true, of(V_876, skc12, skc11), true)=true))). % 19.58/10.07 tff(c_14664, plain, (![V_874]: (ifeq2(accessible_world(skc14, V_874), true, theme(V_874, skc15, skc14), true)=true))). % 19.58/10.07 tff(c_6296, plain, (![U_172]: (ifeq2(theme(U_172, skc15, skc14), true, ifeq2(accessible_world(U_172, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_14597, plain, (![V_871]: (ifeq2(accessible_world(skc14, V_871), true, agent(V_871, skc15, skc17), true)=true))). % 19.58/10.07 tff(c_14554, plain, (![V_869]: (ifeq2(accessible_world(skc14, V_869), true, of(V_869, skc16, skc17), true)=true))). % 19.58/10.07 tff(c_6366, plain, (![U_164]: (ifeq2(of(U_164, skc16, skc17), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_6331, plain, (![U_168]: (ifeq2(agent(U_168, skc15, skc17), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 19.58/10.07 tff(c_3540, plain, (![U_390]: (ifeq2(of(U_390, skc12, skc11), true, ifeq2(accessible_world(U_390, skc9), true, true, true), true)=true))). % 19.58/10.07 tff(c_12781, plain, (![Z_762]: (ifeq3(agent(skc9, skc15, Z_762), true, ifeq3(agent(skc9, skc15, Z_762), true, skc14, skc14), skc14)=skc14))). % 19.58/10.07 tff(c_14419, plain, (![V_863]: (ifeq2(accessible_world(skc9, V_863), true, of(V_863, skc12, skc11), true)=true))). % 19.58/10.07 tff(c_12960, plain, (![W_772]: (ifeq3(theme(skc9, skc15, W_772), true, ifeq3(proposition(skc9, W_772), true, skc14, W_772), W_772)=W_772))). % 19.58/10.07 tff(c_4010, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_3494, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_3903, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(nonhuman(U_140, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_3979, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(general(U_143, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_5683, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc17), true, true, true), true)=true))). % 19.58/10.07 tff(c_5876, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(existent(U_110, skc17), true, true, true), true)=true))). % 19.58/10.07 tff(c_3289, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_6209, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(specific(U_86, skc17), true, true, true), true)=true))). % 19.58/10.07 tff(c_5647, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_5665, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_3463, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(nonhuman(U_140, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_3818, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(abstraction(U_137, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_3350, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_13173, plain, (![V_786]: (ifeq3(theme(skc9, skc15, V_786), true, ifeq3(proposition(skc9, V_786), true, V_786, skc14), skc14)=skc14))). % 19.58/10.07 tff(c_3408, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(general(U_143, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_6010, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(specific(U_86, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_5936, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(existent(U_110, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_5972, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_2706, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc9), true, ifeq2(singleton(U_83, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_2734, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc9), true, ifeq2(singleton(U_83, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_2829, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc9), true, ifeq2(singleton(U_83, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_2881, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc9), true, ifeq2(singleton(U_83, skc17), true, true, true), true)=true))). % 19.58/10.07 tff(c_3719, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(relation(U_134, skc12), true, true, true), true)=true))). % 19.58/10.07 tff(c_3879, plain, (![Y_410, W_409, X_413, Z_412]: (ifeq3(theme(skc9, Y_410, W_409), true, ifeq3(theme(skc9, X_413, skc14), true, ifeq3(agent(skc9, Y_410, Z_412), true, ifeq3(agent(skc9, X_413, Z_412), true, ifeq3(think_believe_consider(skc9, Y_410), true, ifeq3(think_believe_consider(skc9, X_413), true, ifeq3(proposition(skc9, W_409), true, skc14, W_409), W_409), W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.07 tff(c_5464, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(entity(U_107, skc11), true, true, true), true)=true))). % 19.58/10.07 tff(c_5433, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(living(U_116, skc17), true, true, true), true)=true))). % 19.58/10.07 tff(c_3218, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(abstraction(U_137, skc16), true, true, true), true)=true))). % 19.58/10.07 tff(c_5617, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_5362, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(general(U_143, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_6095, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_5760, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(living(U_116, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_6124, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_5503, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_3878, plain, (![Y_410, X_413, V_408, Z_412]: (ifeq3(theme(skc9, Y_410, skc14), true, ifeq3(theme(skc9, X_413, V_408), true, ifeq3(agent(skc9, Y_410, Z_412), true, ifeq3(agent(skc9, X_413, Z_412), true, ifeq3(think_believe_consider(skc9, Y_410), true, ifeq3(think_believe_consider(skc9, X_413), true, ifeq3(proposition(skc9, V_408), true, V_408, skc14), skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.08 tff(c_5310, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(nonhuman(U_140, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_5848, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(impartial(U_113, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_5590, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_5791, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(entity(U_107, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_5731, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(impartial(U_113, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_2783, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc9), true, ifeq2(specific(U_351, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2635, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc9), true, ifeq2(existent(U_342, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_2641, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc9), true, ifeq2(existent(U_342, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2777, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc9), true, ifeq2(specific(U_351, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_3877, plain, (![Y_410, W_409, V_408, Z_412]: (ifeq3(theme(skc9, Y_410, W_409), true, ifeq3(theme(skc9, skc15, V_408), true, ifeq3(agent(skc9, Y_410, Z_412), true, ifeq3(agent(skc9, skc15, Z_412), true, ifeq3(think_believe_consider(skc9, Y_410), true, ifeq3(proposition(skc9, W_409), true, ifeq3(proposition(skc9, V_408), true, V_408, W_409), W_409), W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.08 tff(c_3157, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc9), true, ifeq2(general(U_371, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_2131, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc9), true, ifeq2(thing(U_315, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_2125, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc9), true, ifeq2(thing(U_315, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_2969, plain, (![U_361]: (ifeq2(accessible_world(U_361, skc9), true, ifeq2(unisex(U_361, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_3151, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc9), true, ifeq2(general(U_371, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_2408, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc9), true, ifeq2(thing(U_80, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2463, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc9), true, ifeq2(thing(U_80, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_2975, plain, (![U_361]: (ifeq2(accessible_world(U_361, skc9), true, ifeq2(unisex(U_361, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_2906, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc9), true, ifeq2(nonhuman(U_357, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_3876, plain, (![W_409, X_413, V_408, Z_412]: (ifeq3(theme(skc9, skc15, W_409), true, ifeq3(theme(skc9, X_413, V_408), true, ifeq3(agent(skc9, skc15, Z_412), true, ifeq3(agent(skc9, X_413, Z_412), true, ifeq3(think_believe_consider(skc9, X_413), true, ifeq3(proposition(skc9, W_409), true, ifeq3(proposition(skc9, V_408), true, V_408, W_409), W_409), W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.08 tff(c_2677, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc9), true, ifeq2(singleton(U_345, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_2900, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc9), true, ifeq2(nonhuman(U_357, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_5005, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_5263, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_4696, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc14), true, ifeq2(organism(U_104, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_5087, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc14), true, ifeq2(organism(U_104, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_5570, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(singleton(U_83, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_3684, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc14), true, ifeq2(relname(U_131, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_4733, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(nonexistent(U_89, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_3873, plain, (![Y_410, W_409, V_408]: (ifeq3(theme(skc9, Y_410, W_409), true, ifeq3(theme(skc9, skc15, V_408), true, ifeq3(agent(skc9, Y_410, skc17), true, ifeq3(think_believe_consider(skc9, Y_410), true, ifeq3(proposition(skc9, W_409), true, ifeq3(proposition(skc9, V_408), true, V_408, W_409), W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.08 tff(c_4397, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_4958, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(thing(U_80, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_4349, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(unisex(U_92, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_5241, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc14), true, ifeq2(human(U_119, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_5040, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(specific(U_86, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_5164, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(animate(U_122, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_4930, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(animate(U_122, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_4257, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(nonexistent(U_89, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_4307, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(specific(U_86, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_3872, plain, (![W_409, X_413, V_408]: (ifeq3(theme(skc9, skc15, W_409), true, ifeq3(theme(skc9, X_413, V_408), true, ifeq3(agent(skc9, X_413, skc17), true, ifeq3(think_believe_consider(skc9, X_413), true, ifeq3(proposition(skc9, W_409), true, ifeq3(proposition(skc9, V_408), true, V_408, W_409), W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.08 tff(c_4899, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc14), true, ifeq2(human(U_119, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_3180, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(relation(U_134, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_5124, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(abstraction(U_137, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_2683, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc9), true, ifeq2(singleton(U_345, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_2259, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc9), true, ifeq2(living(U_321, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_3447, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc9), true, ifeq2(impartial(U_383, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_3163, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc9), true, ifeq2(general(U_371, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_2253, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc9), true, ifeq2(living(U_321, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2369, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc9), true, ifeq2(abstraction(U_327, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_3875, plain, (![Y_410, W_409, Z_412]: (ifeq3(theme(skc9, Y_410, W_409), true, ifeq3(agent(skc9, Y_410, Z_412), true, ifeq3(agent(skc9, skc15, Z_412), true, ifeq3(think_believe_consider(skc9, Y_410), true, ifeq3(proposition(skc9, W_409), true, skc14, W_409), W_409), W_409), W_409), W_409)=W_409))). % 19.58/10.08 tff(c_3041, plain, (![U_365]: (ifeq2(accessible_world(U_365, skc9), true, ifeq2(entity(U_365, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2689, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc9), true, ifeq2(singleton(U_345, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_2912, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc9), true, ifeq2(nonhuman(U_357, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_3047, plain, (![U_365]: (ifeq2(accessible_world(U_365, skc9), true, ifeq2(entity(U_365, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_2375, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc9), true, ifeq2(abstraction(U_327, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_2993, plain, (![U_361]: (ifeq2(accessible_world(U_361, skc9), true, ifeq2(unisex(U_361, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_2149, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc9), true, ifeq2(thing(U_315, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_3441, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc9), true, ifeq2(impartial(U_383, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_4600, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(eventuality(U_77, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_3874, plain, (![X_413, V_408, Z_412]: (ifeq3(theme(skc9, X_413, V_408), true, ifeq3(agent(skc9, skc15, Z_412), true, ifeq3(agent(skc9, X_413, Z_412), true, ifeq3(think_believe_consider(skc9, X_413), true, ifeq3(proposition(skc9, V_408), true, V_408, skc14), skc14), skc14), skc14), skc14)=skc14))). % 19.58/10.08 tff(c_4092, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(event(U_95, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_4821, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(male(U_125, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_4528, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(male(U_125, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_4852, plain, (![U_101]: (ifeq2(accessible_world(U_101, skc14), true, ifeq2(human_person(U_101, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_4126, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(eventuality(U_77, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_3633, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(forename(U_128, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_4477, plain, (![U_101]: (ifeq2(accessible_world(U_101, skc14), true, ifeq2(human_person(U_101, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_4223, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(relation(U_134, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_12418, plain, (ifeq3(of(skc9, skc16, skc11), true, skc12, skc16)=skc16)). % 19.58/10.08 tff(c_3798, plain, (![W_405, X_406]: (ifeq3(of(skc9, W_405, X_406), true, ifeq3(of(skc9, skc16, X_406), true, ifeq3(forename(skc9, W_405), true, ifeq3(entity(skc9, X_406), true, W_405, skc16), skc16), skc16), skc16)=skc16))). % 19.58/10.08 tff(c_3249, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc14), true, ifeq2(relname(U_374, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_2502, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc9), true, ifeq2(animate(U_333, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_1997, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc9), true, ifeq2(nonexistent(U_309, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_2795, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc9), true, ifeq2(specific(U_351, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_1948, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc9), true, ifeq2(relation(U_306, skc12), true, true, true), true)=true))). % 19.58/10.08 tff(c_2143, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc9), true, ifeq2(thing(U_315, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_2496, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc9), true, ifeq2(animate(U_333, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2987, plain, (![U_361]: (ifeq2(accessible_world(U_361, skc9), true, ifeq2(unisex(U_361, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_12247, plain, (ifeq3(of(skc9, skc12, skc17), true, skc12, skc16)=skc16)). % 19.58/10.08 tff(c_3795, plain, (![X_406, V_407]: (ifeq3(of(skc9, skc12, X_406), true, ifeq3(of(skc9, V_407, X_406), true, ifeq3(forename(skc9, V_407), true, ifeq3(entity(skc9, X_406), true, skc12, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.08 tff(c_2074, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc9), true, ifeq2(human(U_312, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_3392, plain, (![U_380]: (ifeq2(accessible_world(U_380, skc9), true, ifeq2(organism(U_380, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_2003, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc9), true, ifeq2(nonexistent(U_309, skc10), true, true, true), true)=true))). % 19.58/10.08 tff(c_2789, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc9), true, ifeq2(specific(U_351, skc15), true, true, true), true)=true))). % 19.58/10.08 tff(c_3386, plain, (![U_380]: (ifeq2(accessible_world(U_380, skc9), true, ifeq2(organism(U_380, skc17), true, true, true), true)=true))). % 19.58/10.08 tff(c_2080, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc9), true, ifeq2(human(U_312, skc11), true, true, true), true)=true))). % 19.58/10.08 tff(c_1942, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc9), true, ifeq2(relation(U_306, skc16), true, true, true), true)=true))). % 19.58/10.08 tff(c_2381, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc9), true, ifeq2(abstraction(U_327, skc14), true, true, true), true)=true))). % 19.58/10.08 tff(c_12076, plain, (ifeq3(of(skc9, skc12, skc17), true, skc16, skc12)=skc12)). % 19.58/10.08 tff(c_3796, plain, (![W_405, X_406]: (ifeq3(of(skc9, W_405, X_406), true, ifeq3(of(skc9, skc12, X_406), true, ifeq3(forename(skc9, W_405), true, ifeq3(entity(skc9, X_406), true, W_405, skc12), skc12), skc12), skc12)=skc12))). % 19.58/10.09 tff(c_2137, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc9), true, ifeq2(thing(U_315, skc15), true, true, true), true)=true))). % 19.58/10.09 tff(c_2981, plain, (![U_361]: (ifeq2(accessible_world(U_361, skc9), true, ifeq2(unisex(U_361, skc10), true, true, true), true)=true))). % 19.58/10.09 tff(c_3588, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc14), true, ifeq2(jules_forename(U_146, skc12), true, true, true), true)=true))). % 19.58/10.09 tff(c_11957, plain, (![V_713]: (ifeq2(accessible_world(skc14, V_713), true, think_believe_consider(V_713, skc15), true)=true))). % 19.58/10.09 tff(c_4663, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc14), true, ifeq2(vincent_forename(U_161, skc16), true, true, true), true)=true))). % 19.58/10.09 tff(c_11923, plain, (ifeq3(of(skc9, skc16, skc11), true, skc16, skc12)=skc12)). % 19.58/10.09 tff(c_3797, plain, (![X_406, V_407]: (ifeq3(of(skc9, skc16, X_406), true, ifeq3(of(skc9, V_407, X_406), true, ifeq3(forename(skc9, V_407), true, ifeq3(entity(skc9, X_406), true, skc16, V_407), V_407), V_407), V_407)=V_407))). % 19.58/10.09 tff(c_11854, plain, (![V_708]: (ifeq2(accessible_world(skc14, V_708), true, present(V_708, skc15), true)=true))). % 19.58/10.09 tff(c_4061, plain, (![U_74]: (ifeq2(accessible_world(U_74, skc14), true, ifeq2(state(U_74, skc10), true, true, true), true)=true))). % 19.58/10.09 tff(c_4437, plain, (![U_98]: (ifeq2(accessible_world(U_98, skc14), true, ifeq2(man(U_98, skc17), true, true, true), true)=true))). % 19.58/10.09 tff(c_2953, plain, (![U_152]: (ifeq2(present(U_152, skc15), true, ifeq2(accessible_world(U_152, skc14), true, true, true), true)=true))). % 19.58/10.09 tff(c_3953, plain, (![U_155]: (ifeq2(think_believe_consider(U_155, skc15), true, ifeq2(accessible_world(U_155, skc14), true, true, true), true)=true))). % 19.58/10.09 tff(c_4781, plain, (![U_98]: (ifeq2(accessible_world(U_98, skc14), true, ifeq2(man(U_98, skc11), true, true, true), true)=true))). % 19.58/10.09 tff(c_11690, plain, (![V_701]: (ifeq2(accessible_world(skc9, V_701), true, agent(V_701, skc15, skc17), true)=true))). % 19.58/10.09 tff(c_4193, plain, (![U_158]: (ifeq2(accessible_world(U_158, skc14), true, ifeq2(proposition(U_158, skc14), true, true, true), true)=true))). % 19.58/10.09 tff(c_4562, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(event(U_95, skc15), true, true, true), true)=true))). % 19.58/10.09 tff(c_3066, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(forename(U_128, skc16), true, true, true), true)=true))). % 19.58/10.09 tff(c_1842, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc9), true, ifeq2(event(U_300, skc10), true, true, true), true)=true))). % 19.58/10.09 tff(c_3255, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc9), true, ifeq2(relname(U_374, skc16), true, true, true), true)=true))). % 19.58/10.09 tff(c_2327, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc9), true, ifeq2(male(U_324, skc17), true, true, true), true)=true))). % 19.58/10.09 tff(c_1751, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc9), true, ifeq2(eventuality(U_294, skc10), true, true, true), true)=true))). % 19.58/10.09 tff(c_2321, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc9), true, ifeq2(male(U_324, skc11), true, true, true), true)=true))). % 19.58/10.09 tff(c_2854, plain, (![U_354]: (ifeq2(accessible_world(U_354, skc9), true, ifeq2(human_person(U_354, skc17), true, true, true), true)=true))). % 19.58/10.09 tff(c_3618, plain, (![U_395]: (ifeq2(agent(U_395, skc15, skc17), true, ifeq2(accessible_world(U_395, skc9), true, true, true), true)=true))). % 19.58/10.09 tff(c_1745, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc9), true, ifeq2(eventuality(U_294, skc15), true, true, true), true)=true))). % 19.58/10.09 tff(c_1954, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc9), true, ifeq2(relation(U_306, skc14), true, true, true), true)=true))). % 19.58/10.09 tff(c_2848, plain, (![U_354]: (ifeq2(accessible_world(U_354, skc9), true, ifeq2(human_person(U_354, skc11), true, true, true), true)=true))). % 19.58/10.09 tff(c_3261, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc9), true, ifeq2(relname(U_374, skc12), true, true, true), true)=true))). % 19.58/10.09 tff(c_6844, plain, (![V_460]: (ifeq(tuple(true, existent(skc14, skf1(V_460))), tuple(true, true), a, b)=b))). % 19.58/10.09 tff(c_6686, plain, (![V_453]: (ifeq(tuple(true, male(skc14, skf1(V_453))), tuple(true, true), a, b)=b))). % 19.58/10.09 tff(c_3546, plain, (![U_390]: (ifeq2(of(U_390, skc16, skc17), true, ifeq2(accessible_world(U_390, skc9), true, true, true), true)=true))). % 19.58/10.09 tff(c_6755, plain, (![V_456]: (ifeq(tuple(true, general(skc14, skf1(V_456))), tuple(true, true), a, b)=b))). % 19.58/10.09 tff(c_3982, plain, (ifeq(tuple(specific(skc14, skc12), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3906, plain, (ifeq(tuple(human(skc14, skc12), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_4013, plain, (ifeq(tuple(true, male(skc14, skc12)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3514, plain, (![U_386]: (ifeq2(theme(U_386, skc15, skc14), true, ifeq2(accessible_world(U_386, skc9), true, true, true), true)=true))). % 19.58/10.09 tff(c_6212, plain, (ifeq(tuple(true, general(skc14, skc17)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3353, plain, (ifeq(tuple(true, male(skc14, skc16)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5879, plain, (ifeq(tuple(nonexistent(skc14, skc17), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3466, plain, (ifeq(tuple(human(skc14, skc16), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5939, plain, (ifeq(tuple(nonexistent(skc14, skc11), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3411, plain, (ifeq(tuple(specific(skc14, skc16), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_6013, plain, (ifeq(tuple(true, general(skc14, skc11)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_11294, plain, (![V_680]: (ifeq2(accessible_world(skc9, V_680), true, of(V_680, skc16, skc17), true)=true))). % 19.58/10.09 tff(c_5365, plain, (ifeq(tuple(specific(skc14, skc14), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5313, plain, (ifeq(tuple(human(skc14, skc14), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2104, plain, (ifeq(tuple(true, general(skc9, skc17)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2224, plain, (ifeq(tuple(specific(skc9, skc16), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2580, plain, (ifeq(tuple(true, male(skc9, skc16)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2350, plain, (ifeq(tuple(nonexistent(skc9, skc11), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2546, plain, (ifeq(tuple(specific(skc9, skc12), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_11215, plain, (![V_678]: (ifeq2(accessible_world(skc9, V_678), true, theme(V_678, skc15, skc14), true)=true))). % 19.58/10.09 tff(c_2299, plain, (ifeq(tuple(true, male(skc9, skc12)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_1978, plain, (ifeq(tuple(human(skc9, skc12), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2272, plain, (ifeq(tuple(true, general(skc9, skc11)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2056, plain, (ifeq(tuple(human(skc9, skc16), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2176, plain, (ifeq(tuple(nonexistent(skc9, skc17), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5008, plain, (ifeq(tuple(true, male(skc14, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_11142, plain, (![V_454]: (ifeq2(specific(skc9, skf1(V_454)), true, true, true)=true))). % 19.58/10.09 tff(c_11087, plain, (![W_675]: (ifeq2(specific(skc9, W_675), true, specific(skc14, W_675), true)=true))). % 19.58/10.09 tff(c_4902, plain, (ifeq(tuple(true, nonhuman(skc14, skc11)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_4260, plain, (ifeq(tuple(true, existent(skc14, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5043, plain, (ifeq(tuple(true, general(skc14, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_6918, plain, (![V_84, V_465]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skf1(V_465)), true)=true))). % 19.58/10.09 tff(c_6696, plain, (![V_93, V_453]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skf1(V_453)), true)=true))). % 19.58/10.09 tff(c_5266, plain, (ifeq(tuple(true, male(skc14, skc14)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_6765, plain, (![V_87, V_456]: (ifeq2(accessible_world(skc14, V_87), true, specific(V_87, skf1(V_456)), true)=true))). % 19.58/10.09 tff(c_10979, plain, (![W_667]: (ifeq2(male(skc9, W_667), true, male(skc14, W_667), true)=true))). % 19.58/10.09 tff(c_6851, plain, (![V_90, V_460]: (ifeq2(accessible_world(skc14, V_90), true, nonexistent(V_90, skf1(V_460)), true)=true))). % 19.58/10.09 tff(c_6811, plain, (![V_81, V_458]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skf1(V_458)), true)=true))). % 19.58/10.09 tff(c_6652, plain, (![V_78, V_451]: (ifeq2(accessible_world(skc14, V_78), true, eventuality(V_78, skf1(V_451)), true)=true))). % 19.58/10.09 tff(c_6568, plain, (![V_150, V_446]: (ifeq2(accessible_world(skc14, V_150), true, smoke(V_150, skf1(V_446)), true)=true))). % 19.58/10.09 tff(c_6533, plain, (![V_96, V_444]: (ifeq2(accessible_world(skc14, V_96), true, event(V_96, skf1(V_444)), true)=true))). % 19.58/10.09 tff(c_4352, plain, (ifeq(tuple(true, male(skc14, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_4022, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skc12), true)=true))). % 19.58/10.09 tff(c_10830, plain, (![W_654]: (ifeq2(relation(skc9, W_654), true, relation(skc14, W_654), true)=true))). % 19.58/10.09 tff(c_3988, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, general(V_144, skc12), true)=true))). % 19.58/10.09 tff(c_3500, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc16), true)=true))). % 19.58/10.09 tff(c_3912, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, nonhuman(V_141, skc12), true)=true))). % 19.58/10.09 tff(c_3417, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, general(V_144, skc16), true)=true))). % 19.58/10.09 tff(c_3362, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skc16), true)=true))). % 19.58/10.09 tff(c_4736, plain, (ifeq(tuple(true, existent(skc14, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5987, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc11), true)=true))). % 19.58/10.09 tff(c_3472, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, nonhuman(V_141, skc16), true)=true))). % 19.58/10.09 tff(c_5885, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, existent(V_111, skc17), true)=true))). % 19.58/10.09 tff(c_1848, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc9), true, ifeq2(event(U_300, skc15), true, true, true), true)=true))). % 19.58/10.09 tff(c_6221, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, specific(V_87, skc17), true)=true))). % 19.58/10.09 tff(c_3304, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc16), true)=true))). % 19.58/10.09 tff(c_5672, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc11), true)=true))). % 19.58/10.09 tff(c_6022, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, specific(V_87, skc11), true)=true))). % 19.58/10.09 tff(c_5945, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, existent(V_111, skc11), true)=true))). % 19.58/10.09 tff(c_4310, plain, (ifeq(tuple(true, general(skc14, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_3836, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, abstraction(V_138, skc12), true)=true))). % 19.58/10.09 tff(c_10538, plain, (![W_637]: (ifeq2(relname(skc9, W_637), true, relname(skc14, W_637), true)=true))). % 19.58/10.09 tff(c_5690, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc17), true)=true))). % 19.58/10.09 tff(c_5654, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc12), true)=true))). % 19.58/10.09 tff(c_2835, plain, (![V_84]: (ifeq2(accessible_world(skc9, V_84), true, singleton(V_84, skc11), true)=true))). % 19.58/10.09 tff(c_2887, plain, (![V_84]: (ifeq2(accessible_world(skc9, V_84), true, singleton(V_84, skc17), true)=true))). % 19.58/10.09 tff(c_2712, plain, (![V_84]: (ifeq2(accessible_world(skc9, V_84), true, singleton(V_84, skc12), true)=true))). % 19.58/10.09 tff(c_5244, plain, (ifeq(tuple(true, nonhuman(skc14, skc17)), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_2740, plain, (![V_84]: (ifeq2(accessible_world(skc9, V_84), true, singleton(V_84, skc16), true)=true))). % 19.58/10.09 tff(c_10369, plain, (![W_629]: (ifeq2(human_person(skc9, W_629), true, human_person(skc14, W_629), true)=true))). % 19.58/10.09 tff(c_6140, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc12), true)=true))). % 19.58/10.09 tff(c_5854, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, impartial(V_114, skc17), true)=true))). % 19.58/10.09 tff(c_5632, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc14), true)=true))). % 19.58/10.09 tff(c_3236, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, abstraction(V_138, skc16), true)=true))). % 19.58/10.09 tff(c_5371, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, general(V_144, skc14), true)=true))). % 19.58/10.09 tff(c_1594, plain, (ifeq(tuple(human(skc9, skc14), true), tuple(true, true), a, b)=b)). % 19.58/10.09 tff(c_5509, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc10), true)=true))). % 19.58/10.09 tff(c_10232, plain, (![W_621]: (ifeq2(proposition(skc9, W_621), true, proposition(skc14, W_621), true)=true))). % 19.58/10.09 tff(c_5807, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, entity(V_108, skc17), true)=true))). % 19.58/10.09 tff(c_5439, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, living(V_117, skc17), true)=true))). % 19.58/10.09 tff(c_3731, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, relation(V_135, skc12), true)=true))). % 19.58/10.09 tff(c_6111, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc17), true)=true))). % 19.58/10.09 tff(c_5319, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, nonhuman(V_141, skc14), true)=true))). % 19.58/10.09 tff(c_1672, plain, (ifeq(tuple(true, male(skc9, skc14)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_5480, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, entity(V_108, skc11), true)=true))). % 19.58/10.10 tff(c_10079, plain, (![W_613]: (ifeq2(forename(skc9, W_613), true, forename(skc14, W_613), true)=true))). % 19.58/10.10 tff(c_5766, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, living(V_117, skc11), true)=true))). % 19.58/10.10 tff(c_5737, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, impartial(V_114, skc11), true)=true))). % 19.58/10.10 tff(c_5597, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc14), true)=true))). % 19.58/10.10 tff(c_2919, plain, (![V_358]: (ifeq2(accessible_world(skc9, V_358), true, nonhuman(V_358, skc12), true)=true))). % 19.58/10.10 tff(c_2801, plain, (![V_352]: (ifeq2(accessible_world(skc9, V_352), true, specific(V_352, skc11), true)=true))). % 19.58/10.10 tff(c_1554, plain, (ifeq(tuple(specific(skc9, skc14), true), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_2155, plain, (![V_316]: (ifeq2(accessible_world(skc9, V_316), true, thing(V_316, skc16), true)=true))). % 19.58/10.10 tff(c_9922, plain, (![V_605]: (ifeq2(accessible_world(skc9, V_605), true, present(V_605, skc15), true)=true))). % 19.58/10.10 tff(c_3169, plain, (![V_372]: (ifeq2(accessible_world(skc9, V_372), true, general(V_372, skc12), true)=true))). % 19.58/10.10 tff(c_2918, plain, (![V_358]: (ifeq2(accessible_world(skc9, V_358), true, nonhuman(V_358, skc16), true)=true))). % 19.58/10.10 tff(c_3170, plain, (![V_372]: (ifeq2(accessible_world(skc9, V_372), true, general(V_372, skc16), true)=true))). % 19.58/10.10 tff(c_2478, plain, (![V_81]: (ifeq2(accessible_world(skc9, V_81), true, thing(V_81, skc11), true)=true))). % 19.58/10.10 tff(c_2695, plain, (![V_346]: (ifeq2(accessible_world(skc9, V_346), true, singleton(V_346, skc14), true)=true))). % 19.58/10.10 tff(c_4531, plain, (ifeq(tuple(unisex(skc14, skc17), true), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_2647, plain, (![V_343]: (ifeq2(accessible_world(skc9, V_343), true, existent(V_343, skc11), true)=true))). % 19.58/10.10 tff(c_3000, plain, (![V_362]: (ifeq2(accessible_world(skc9, V_362), true, unisex(V_362, skc12), true)=true))). % 19.58/10.10 tff(c_2999, plain, (![V_362]: (ifeq2(accessible_world(skc9, V_362), true, unisex(V_362, skc16), true)=true))). % 19.58/10.10 tff(c_2205, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc9), true, ifeq2(forename(U_318, skc12), true, true, true), true)=true))). % 19.58/10.10 tff(c_2423, plain, (![V_81]: (ifeq2(accessible_world(skc9, V_81), true, thing(V_81, skc17), true)=true))). % 19.58/10.10 tff(c_2648, plain, (![V_343]: (ifeq2(accessible_world(skc9, V_343), true, existent(V_343, skc17), true)=true))). % 19.58/10.10 tff(c_2156, plain, (![V_316]: (ifeq2(accessible_world(skc9, V_316), true, thing(V_316, skc12), true)=true))). % 19.58/10.10 tff(c_2802, plain, (![V_352]: (ifeq2(accessible_world(skc9, V_352), true, specific(V_352, skc17), true)=true))). % 19.58/10.10 tff(c_3192, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, relation(V_135, skc16), true)=true))). % 19.58/10.10 tff(c_4824, plain, (ifeq(tuple(unisex(skc14, skc11), true), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_4908, plain, (![V_120]: (ifeq2(accessible_world(skc14, V_120), true, human(V_120, skc11), true)=true))). % 19.58/10.10 tff(c_4319, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, specific(V_87, skc10), true)=true))). % 19.58/10.10 tff(c_5170, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, animate(V_123, skc17), true)=true))). % 19.58/10.10 tff(c_3317, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc9), true, ifeq2(man(U_377, skc17), true, true, true), true)=true))). % 19.58/10.10 tff(c_3693, plain, (![V_132]: (ifeq2(accessible_world(skc14, V_132), true, relname(V_132, skc12), true)=true))). % 19.58/10.10 tff(c_4936, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, animate(V_123, skc11), true)=true))). % 19.58/10.10 tff(c_4266, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, nonexistent(V_90, skc10), true)=true))). % 19.58/10.10 tff(c_4742, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, nonexistent(V_90, skc15), true)=true))). % 19.58/10.10 tff(c_5250, plain, (![V_120]: (ifeq2(accessible_world(skc14, V_120), true, human(V_120, skc17), true)=true))). % 19.58/10.10 tff(c_1706, plain, (ifeq(tuple(true, existent(skc9, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_5577, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, singleton(V_84, skc15), true)=true))). % 19.58/10.10 tff(c_4412, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc10), true)=true))). % 19.58/10.10 tff(c_5102, plain, (![V_105]: (ifeq2(accessible_world(skc14, V_105), true, organism(V_105, skc11), true)=true))). % 19.58/10.10 tff(c_2448, plain, (![U_330]: (ifeq2(present(U_330, skc15), true, ifeq2(accessible_world(U_330, skc9), true, true, true), true)=true))). % 19.58/10.10 tff(c_4973, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, thing(V_81, skc15), true)=true))). % 19.58/10.10 tff(c_5052, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, specific(V_87, skc15), true)=true))). % 19.58/10.10 tff(c_5276, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skc14), true)=true))). % 19.58/10.10 tff(c_4361, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skc10), true)=true))). % 19.58/10.10 tff(c_5017, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, unisex(V_93, skc15), true)=true))). % 19.58/10.10 tff(c_1597, plain, (ifeq(tuple(true, nonhuman(skc9, skc17)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_9332, plain, (be(skc14, skc10, skc11, skc11)=true)). % 19.58/10.10 tff(c_3675, plain, (![W_400, X_403, Y_399]: (ifeq2(be(skc9, W_400, X_403, Y_399), true, be(skc14, W_400, X_403, Y_399), true)=true))). % 19.58/10.10 tff(c_4711, plain, (![V_105]: (ifeq2(accessible_world(skc14, V_105), true, organism(V_105, skc17), true)=true))). % 19.58/10.10 tff(c_5142, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, abstraction(V_138, skc14), true)=true))). % 19.58/10.10 tff(c_2388, plain, (![V_328]: (ifeq2(accessible_world(skc9, V_328), true, abstraction(V_328, skc12), true)=true))). % 19.58/10.10 tff(c_3453, plain, (![V_384]: (ifeq2(accessible_world(skc9, V_384), true, impartial(V_384, skc17), true)=true))). % 19.58/10.10 tff(c_2266, plain, (![V_322]: (ifeq2(accessible_world(skc9, V_322), true, living(V_322, skc11), true)=true))). % 19.58/10.10 tff(c_1551, plain, (ifeq(tuple(true, general(skc9, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_2387, plain, (![V_328]: (ifeq2(accessible_world(skc9, V_328), true, abstraction(V_328, skc16), true)=true))). % 19.58/10.10 tff(c_9155, plain, (![W_562]: (ifeq2(human(skc9, W_562), true, human(skc14, W_562), true)=true))). % 19.58/10.10 tff(c_3053, plain, (![V_366]: (ifeq2(accessible_world(skc9, V_366), true, entity(V_366, skc17), true)=true))). % 19.58/10.10 tff(c_2697, plain, (![V_346]: (ifeq2(accessible_world(skc9, V_346), true, singleton(V_346, skc15), true)=true))). % 19.58/10.10 tff(c_3003, plain, (![V_362]: (ifeq2(accessible_world(skc9, V_362), true, unisex(V_362, skc14), true)=true))). % 19.58/10.10 tff(c_2265, plain, (![V_322]: (ifeq2(accessible_world(skc9, V_322), true, living(V_322, skc17), true)=true))). % 19.58/10.10 tff(c_2696, plain, (![V_346]: (ifeq2(accessible_world(skc9, V_346), true, singleton(V_346, skc10), true)=true))). % 19.58/10.10 tff(c_1600, plain, (ifeq(tuple(true, nonhuman(skc9, skc11)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_3054, plain, (![V_366]: (ifeq2(accessible_world(skc9, V_366), true, entity(V_366, skc11), true)=true))). % 19.58/10.10 tff(c_8978, plain, (![W_554]: (ifeq2(existent(skc9, W_554), true, existent(skc14, W_554), true)=true))). % 19.58/10.10 tff(c_2920, plain, (![V_358]: (ifeq2(accessible_world(skc9, V_358), true, nonhuman(V_358, skc14), true)=true))). % 19.58/10.10 tff(c_3454, plain, (![V_384]: (ifeq2(accessible_world(skc9, V_384), true, impartial(V_384, skc11), true)=true))). % 19.58/10.10 tff(c_3171, plain, (![V_372]: (ifeq2(accessible_world(skc9, V_372), true, general(V_372, skc14), true)=true))). % 19.58/10.10 tff(c_2159, plain, (![V_316]: (ifeq2(accessible_world(skc9, V_316), true, thing(V_316, skc14), true)=true))). % 19.58/10.10 tff(c_4867, plain, (![V_102]: (ifeq2(accessible_world(skc14, V_102), true, human_person(V_102, skc11), true)=true))). % 19.58/10.10 tff(c_1660, plain, (ifeq(tuple(true, male(skc9, skc10)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_3267, plain, (![V_375]: (ifeq2(accessible_world(skc14, V_375), true, relname(V_375, skc16), true)=true))). % 19.58/10.10 tff(c_8793, plain, (![W_546]: (ifeq2(general(skc9, W_546), true, general(skc14, W_546), true)=true))). % 19.58/10.10 tff(c_3645, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, forename(V_129, skc12), true)=true))). % 19.58/10.10 tff(c_4830, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, male(V_126, skc11), true)=true))). % 19.58/10.10 tff(c_4621, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, eventuality(V_78, skc15), true)=true))). % 19.58/10.10 tff(c_4147, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, eventuality(V_78, skc10), true)=true))). % 19.58/10.10 tff(c_7756, plain, (ifeq2(agent(skc9, skf1(skc11), skc11), true, true, true)=true)). % 19.58/10.10 tff(c_1703, plain, (ifeq(tuple(true, existent(skc9, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_4537, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, male(V_126, skc17), true)=true))). % 19.58/10.10 tff(c_4235, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, relation(V_135, skc14), true)=true))). % 19.58/10.10 tff(c_4492, plain, (![V_102]: (ifeq2(accessible_world(skc14, V_102), true, human_person(V_102, skc17), true)=true))). % 19.58/10.10 tff(c_1890, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc9), true, ifeq2(proposition(U_303, skc14), true, true, true), true)=true))). % 19.58/10.10 tff(c_7926, plain, (ifeq2(agent(skc9, skf1(skc17), skc17), true, true, true)=true)). % 19.58/10.10 tff(c_4104, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, event(V_96, skc10), true)=true))). % 19.58/10.10 tff(c_2509, plain, (![V_334]: (ifeq2(accessible_world(skc9, V_334), true, animate(V_334, skc11), true)=true))). % 19.58/10.10 tff(c_2157, plain, (![V_316]: (ifeq2(accessible_world(skc9, V_316), true, thing(V_316, skc15), true)=true))). % 19.58/10.10 tff(c_3399, plain, (![V_381]: (ifeq2(accessible_world(skc9, V_381), true, organism(V_381, skc11), true)=true))). % 19.58/10.10 tff(c_1548, plain, (ifeq(tuple(true, general(skc9, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_1960, plain, (![V_307]: (ifeq2(accessible_world(skc9, V_307), true, relation(V_307, skc16), true)=true))). % 19.58/10.10 tff(c_8515, plain, (![V_531]: (ifeq2(accessible_world(skc9, V_531), true, think_believe_consider(V_531, skc15), true)=true))). % 19.58/10.10 tff(c_2009, plain, (![V_310]: (ifeq2(accessible_world(skc9, V_310), true, nonexistent(V_310, skc15), true)=true))). % 19.58/10.10 tff(c_2158, plain, (![V_316]: (ifeq2(accessible_world(skc9, V_316), true, thing(V_316, skc10), true)=true))). % 19.58/10.10 tff(c_2087, plain, (![V_313]: (ifeq2(accessible_world(skc9, V_313), true, human(V_313, skc11), true)=true))). % 19.58/10.10 tff(c_1961, plain, (![V_307]: (ifeq2(accessible_world(skc9, V_307), true, relation(V_307, skc12), true)=true))). % 19.58/10.10 tff(c_2508, plain, (![V_334]: (ifeq2(accessible_world(skc9, V_334), true, animate(V_334, skc17), true)=true))). % 19.58/10.10 tff(c_1663, plain, (ifeq(tuple(true, male(skc9, skc15)), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_2803, plain, (![V_352]: (ifeq2(accessible_world(skc9, V_352), true, specific(V_352, skc15), true)=true))). % 19.58/10.10 tff(c_8338, plain, (![W_523]: (ifeq2(man(skc9, W_523), true, man(skc14, W_523), true)=true))). % 19.58/10.10 tff(c_3398, plain, (![V_381]: (ifeq2(accessible_world(skc9, V_381), true, organism(V_381, skc17), true)=true))). % 19.58/10.10 tff(c_2389, plain, (![V_328]: (ifeq2(accessible_world(skc9, V_328), true, abstraction(V_328, skc14), true)=true))). % 19.58/10.10 tff(c_2804, plain, (![V_352]: (ifeq2(accessible_world(skc9, V_352), true, specific(V_352, skc10), true)=true))). % 19.58/10.10 tff(c_3001, plain, (![V_362]: (ifeq2(accessible_world(skc9, V_362), true, unisex(V_362, skc10), true)=true))). % 19.58/10.10 tff(c_3002, plain, (![V_362]: (ifeq2(accessible_world(skc9, V_362), true, unisex(V_362, skc15), true)=true))). % 19.58/10.10 tff(c_1666, plain, (ifeq(tuple(unisex(skc9, skc11), true), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_2086, plain, (![V_313]: (ifeq2(accessible_world(skc9, V_313), true, human(V_313, skc17), true)=true))). % 19.58/10.10 tff(c_8161, plain, (![W_515]: (ifeq2(impartial(skc9, W_515), true, impartial(skc14, W_515), true)=true))). % 19.58/10.10 tff(c_2010, plain, (![V_310]: (ifeq2(accessible_world(skc9, V_310), true, nonexistent(V_310, skc10), true)=true))). % 19.58/10.10 tff(c_4575, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, event(V_96, skc15), true)=true))). % 19.58/10.10 tff(c_4456, plain, (![V_99]: (ifeq2(accessible_world(skc14, V_99), true, man(V_99, skc17), true)=true))). % 19.58/10.10 tff(c_3079, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, forename(V_129, skc16), true)=true))). % 19.58/10.10 tff(c_3595, plain, (![V_147]: (ifeq2(accessible_world(skc14, V_147), true, jules_forename(V_147, skc12), true)=true))). % 19.58/10.10 tff(c_1669, plain, (ifeq(tuple(unisex(skc9, skc17), true), tuple(true, true), a, b)=b)). % 19.58/10.10 tff(c_4071, plain, (![V_75]: (ifeq2(accessible_world(skc14, V_75), true, state(V_75, skc10), true)=true))). % 19.58/10.10 tff(c_7988, plain, (![W_507]: (ifeq2(nonhuman(skc9, W_507), true, nonhuman(skc14, W_507), true)=true))). % 19.58/10.10 tff(c_4202, plain, (![V_159]: (ifeq2(accessible_world(skc14, V_159), true, proposition(V_159, skc14), true)=true))). % 19.58/10.10 tff(c_4670, plain, (![V_162]: (ifeq2(accessible_world(skc14, V_162), true, vincent_forename(V_162, skc16), true)=true))). % 19.58/10.10 tff(c_7904, plain, (ifeq2(accessible_world(skc14, skc14), true, true, true)=true)). % 19.58/10.10 tff(c_7914, plain, (agent(skc14, skf1(skc17), skc17)=true)). % 19.58/10.10 tff(c_4800, plain, (![V_99]: (ifeq2(accessible_world(skc14, V_99), true, man(V_99, skc11), true)=true))). % 19.58/10.10 tff(c_2333, plain, (![V_325]: (ifeq2(accessible_world(skc9, V_325), true, male(V_325, skc11), true)=true))). % 19.58/10.10 tff(c_1854, plain, (![V_301]: (ifeq2(accessible_world(skc9, V_301), true, event(V_301, skc10), true)=true))). % 19.58/10.10 tff(c_1793, plain, (![U_297]: (ifeq2(think_believe_consider(U_297, skc15), true, ifeq2(accessible_world(U_297, skc9), true, true, true), true)=true))). % 19.58/10.10 tff(c_2861, plain, (![V_355]: (ifeq2(accessible_world(skc9, V_355), true, human_person(V_355, skc17), true)=true))). % 19.58/10.10 tff(c_2860, plain, (![V_355]: (ifeq2(accessible_world(skc9, V_355), true, human_person(V_355, skc11), true)=true))). % 19.58/10.10 tff(c_2334, plain, (![V_325]: (ifeq2(accessible_world(skc9, V_325), true, male(V_325, skc17), true)=true))). % 19.58/10.10 tff(c_7744, plain, (agent(skc14, skf1(skc11), skc11)=true)). % 19.58/10.10 tff(c_1758, plain, (![V_295]: (ifeq2(accessible_world(skc9, V_295), true, eventuality(V_295, skc10), true)=true))). % 19.58/10.10 tff(c_7668, plain, (![W_495]: (ifeq2(organism(skc9, W_495), true, organism(skc14, W_495), true)=true))). % 19.58/10.11 tff(c_3269, plain, (![V_375]: (ifeq2(accessible_world(skc9, V_375), true, relname(V_375, skc12), true)=true))). % 19.58/10.11 tff(c_3268, plain, (![V_375]: (ifeq2(accessible_world(skc9, V_375), true, relname(V_375, skc16), true)=true))). % 19.58/10.11 tff(c_1757, plain, (![V_295]: (ifeq2(accessible_world(skc9, V_295), true, eventuality(V_295, skc15), true)=true))). % 19.58/10.11 tff(c_1962, plain, (![V_307]: (ifeq2(accessible_world(skc9, V_307), true, relation(V_307, skc14), true)=true))). % 19.58/10.11 tff(c_7530, plain, (![W_489]: (ifeq2(living(skc9, W_489), true, living(skc14, W_489), true)=true))). % 19.58/10.11 tff(c_7497, plain, (![V_443]: (ifeq2(event(skc9, skf1(V_443)), true, true, true)=true))). % 19.58/10.11 tff(c_5391, plain, (![W_430]: (ifeq2(event(skc9, W_430), true, event(skc14, W_430), true)=true))). % 19.58/10.11 tff(c_5327, plain, (![W_429]: (ifeq2(vincent_forename(skc9, W_429), true, vincent_forename(skc14, W_429), true)=true))). % 19.58/10.11 tff(c_7414, plain, (![W_484]: (ifeq2(abstraction(skc9, W_484), true, abstraction(skc14, W_484), true)=true))). % 19.58/10.11 tff(c_7335, plain, (![V_452]: (ifeq2(unisex(skc9, skf1(V_452)), true, true, true)=true))). % 19.58/10.11 tff(c_5189, plain, (![W_428]: (ifeq2(unisex(skc9, W_428), true, unisex(skc14, W_428), true)=true))). % 19.58/10.11 tff(c_7256, plain, (![V_457]: (ifeq2(thing(skc9, skf1(V_457)), true, true, true)=true))). % 19.58/10.11 tff(c_6030, plain, (![W_435]: (ifeq2(thing(skc9, W_435), true, thing(skc14, W_435), true)=true))). % 19.58/10.11 tff(c_7232, plain, (![V_445]: (ifeq2(smoke(skc9, skf1(V_445)), true, true, true)=true))). % 19.58/10.11 tff(c_7138, plain, (![W_475]: (ifeq2(smoke(skc9, W_475), true, smoke(skc14, W_475), true)=true))). % 19.58/10.11 tff(c_7153, plain, (![V_464]: (ifeq2(singleton(skc9, skf1(V_464)), true, true, true)=true))). % 19.58/10.11 tff(c_5549, plain, (![W_431]: (ifeq2(singleton(skc9, W_431), true, singleton(skc14, W_431), true)=true))). % 19.58/10.11 tff(c_6484, plain, (![W_442]: (ifeq2(state(skc9, W_442), true, state(skc14, W_442), true)=true))). % 19.58/10.11 tff(c_7073, plain, (![V_459]: (ifeq2(nonexistent(skc9, skf1(V_459)), true, true, true)=true))). % 19.58/10.11 tff(c_5904, plain, (![W_434]: (ifeq2(nonexistent(skc9, W_434), true, nonexistent(skc14, W_434), true)=true))). % 19.58/10.11 tff(c_6261, plain, (![W_437]: (ifeq2(entity(skc9, W_437), true, entity(skc14, W_437), true)=true))). % 19.58/10.11 tff(c_5705, plain, (![W_432]: (ifeq2(jules_forename(skc9, W_432), true, jules_forename(skc14, W_432), true)=true))). % 19.58/10.11 tff(c_3323, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc9), true, ifeq2(man(U_377, skc11), true, true, true), true)=true))). % 19.58/10.11 tff(c_6964, plain, (![V_450]: (ifeq2(eventuality(skc9, skf1(V_450)), true, true, true)=true))). % 19.58/10.11 tff(c_6177, plain, (![W_436]: (ifeq2(eventuality(skc9, W_436), true, eventuality(skc14, W_436), true)=true))). % 19.58/10.11 tff(c_6718, plain, (![W_455]: (ifeq2(animate(skc9, W_455), true, animate(skc14, W_455), true)=true))). % 19.58/10.11 tff(c_6890, plain, (![V_464]: (singleton(skc14, skf1(V_464))=true))). % 19.58/10.11 tff(c_6692, plain, (![V_453]: (ifeq2(abstraction(skc14, skf1(V_453)), true, true, true)=true))). % 19.58/10.11 tff(c_3116, plain, (![U_368]: (ifeq2(accessible_world(U_368, skc9), true, ifeq2(state(U_368, skc10), true, true, true), true)=true))). % 19.58/10.11 tff(c_6761, plain, (![V_456]: (ifeq2(entity(skc14, skf1(V_456)), true, true, true)=true))). % 19.88/10.11 tff(c_6820, plain, (![V_459]: (nonexistent(skc14, skf1(V_459))=true))). % 19.88/10.11 tff(c_6774, plain, (![V_457]: (thing(skc14, skf1(V_457))=true))). % 19.88/10.11 tff(c_6705, plain, (![V_454]: (specific(skc14, skf1(V_454))=true))). % 19.88/10.11 tff(c_6662, plain, (![V_452]: (unisex(skc14, skf1(V_452))=true))). % 19.88/10.11 tff(c_6609, plain, (![V_450]: (eventuality(skc14, skf1(V_450))=true))). % 19.88/10.11 tff(c_6523, plain, (![V_444]: (ifeq2(state(skc14, skf1(V_444)), true, true, true)=true))). % 19.88/10.11 tff(c_6445, plain, (![V_440]: (ifeq2(present(skc9, skf1(V_440)), true, true, true)=true))). % 19.88/10.11 tff(c_2211, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc9), true, ifeq2(forename(U_318, skc16), true, true, true), true)=true))). % 19.88/10.11 tff(c_6541, plain, (![V_445]: (smoke(skc14, skf1(V_445))=true))). % 19.88/10.11 tff(c_6497, plain, (![V_443]: (event(skc14, skf1(V_443))=true))). % 19.88/10.11 tff(c_6438, plain, (![U_193]: (ifeq2(man(skc14, U_193), true, true, true)=true))). % 19.88/10.11 tff(c_6429, plain, (![V_439]: (present(skc14, skf1(V_439))=true))). % 19.88/10.11 tff(c_6392, plain, (of(skc14, skc12, skc11)=true)). % 19.88/10.11 tff(c_2754, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc9), true, ifeq2(jules_forename(U_348, skc12), true, true, true), true)=true))). % 19.88/10.11 tff(c_6342, plain, (of(skc14, skc16, skc17)=true)). % 19.88/10.11 tff(c_6307, plain, (agent(skc14, skc15, skc17)=true)). % 19.88/10.11 tff(c_6272, plain, (theme(skc14, skc15, skc14)=true)). % 19.88/10.11 tff(c_5984, plain, (ifeq2(abstraction(skc14, skc11), true, true, true)=true)). % 19.88/10.11 tff(c_6016, plain, (ifeq2(eventuality(skc14, skc11), true, true, true)=true)). % 19.88/10.11 tff(c_6165, plain, (specific(skc14, skc17)=true)). % 19.88/10.11 tff(c_6104, plain, (ifeq2(eventuality(skc14, skc17), true, true, true)=true)). % 19.88/10.11 tff(c_6107, plain, (ifeq2(abstraction(skc14, skc17), true, true, true)=true)). % 19.88/10.11 tff(c_6127, plain, (ifeq2(entity(skc14, skc12), true, true, true)=true)). % 19.88/10.11 tff(c_6133, plain, (ifeq2(eventuality(skc14, skc12), true, true, true)=true)). % 19.88/10.11 tff(c_6082, plain, (thing(skc14, skc12)=true)). % 19.88/10.11 tff(c_6080, plain, (thing(skc14, skc17)=true)). % 19.88/10.11 tff(c_5995, plain, (specific(skc14, skc11)=true)). % 19.88/10.11 tff(c_5957, plain, (thing(skc14, skc11)=true)). % 19.88/10.11 tff(c_5620, plain, (ifeq2(entity(skc14, skc14), true, true, true)=true)). % 19.88/10.11 tff(c_5892, plain, (existent(skc14, skc11)=true)). % 19.88/10.11 tff(c_5861, plain, (existent(skc14, skc17)=true)). % 19.88/10.11 tff(c_5833, plain, (impartial(skc14, skc17)=true)). % 19.88/10.11 tff(c_5823, plain, (ifeq2(accessible_world(skc14, skc9), true, true, true)=true)). % 19.88/10.11 tff(c_2601, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc9), true, ifeq2(vincent_forename(U_339, skc16), true, true, true), true)=true))). % 19.88/10.11 tff(c_5773, plain, (entity(skc14, skc17)=true)). % 19.88/10.11 tff(c_5745, plain, (living(skc14, skc11)=true)). % 19.88/10.11 tff(c_5716, plain, (impartial(skc14, skc11)=true)). % 19.88/10.11 tff(c_5554, plain, (singleton(skc14, skc17)=true)). % 19.88/10.11 tff(c_5555, plain, (singleton(skc14, skc11)=true)). % 19.88/10.11 tff(c_5557, plain, (singleton(skc14, skc12)=true)). % 19.88/10.11 tff(c_5602, plain, (thing(skc14, skc14)=true)). % 19.88/10.11 tff(c_5558, plain, (singleton(skc14, skc14)=true)). % 19.88/10.11 tff(c_5560, plain, (singleton(skc14, skc15)=true)). % 19.88/10.11 tff(c_5488, plain, (singleton(skc14, skc10)=true)). % 19.88/10.11 tff(c_5446, plain, (entity(skc14, skc11)=true)). % 19.88/10.11 tff(c_5418, plain, (living(skc14, skc17)=true)). % 19.88/10.11 tff(c_5014, plain, (ifeq2(abstraction(skc14, skc15), true, true, true)=true)). % 19.88/10.11 tff(c_5049, plain, (ifeq2(entity(skc14, skc15), true, true, true)=true)). % 19.88/10.11 tff(c_5347, plain, (general(skc14, skc14)=true)). % 19.88/10.11 tff(c_5295, plain, (nonhuman(skc14, skc14)=true)). % 19.88/10.11 tff(c_4409, plain, (ifeq2(abstraction(skc14, skc10), true, true, true)=true)). % 19.88/10.11 tff(c_5269, plain, (ifeq2(eventuality(skc14, skc14), true, true, true)=true)). % 19.88/10.11 tff(c_4316, plain, (ifeq2(entity(skc14, skc10), true, true, true)=true)). % 19.88/10.11 tff(c_5232, plain, (unisex(skc14, skc14)=true)). % 19.88/10.11 tff(c_5177, plain, (human(skc14, skc17)=true)). % 19.88/10.11 tff(c_5149, plain, (animate(skc14, skc17)=true)). % 19.88/10.11 tff(c_5109, plain, (abstraction(skc14, skc14)=true)). % 19.88/10.11 tff(c_5059, plain, (organism(skc14, skc11)=true)). % 19.88/10.11 tff(c_3552, plain, (![W_391, X_392]: (ifeq2(of(skc9, W_391, X_392), true, of(skc14, W_391, X_392), true)=true))). % 19.88/10.11 tff(c_5025, plain, (specific(skc14, skc15)=true)). % 19.88/10.11 tff(c_4990, plain, (unisex(skc14, skc15)=true)). % 19.88/10.11 tff(c_3520, plain, (![W_387, X_388]: (ifeq2(theme(skc9, W_387, X_388), true, theme(skc14, W_387, X_388), true)=true))). % 19.88/10.11 tff(c_4943, plain, (thing(skc14, skc15)=true)). % 19.88/10.11 tff(c_4915, plain, (animate(skc14, skc11)=true)). % 19.88/10.11 tff(c_4884, plain, (human(skc14, skc11)=true)). % 19.88/10.11 tff(c_3624, plain, (![W_396, X_397]: (ifeq2(agent(skc9, W_396, X_397), true, agent(skc14, W_396, X_397), true)=true))). % 19.88/10.11 tff(c_4837, plain, (human_person(skc14, skc11)=true)). % 19.88/10.11 tff(c_4806, plain, (male(skc14, skc11)=true)). % 19.88/10.11 tff(c_4763, plain, (man(skc14, skc11)=true)). % 19.88/10.11 tff(c_3330, plain, (![V_378]: (ifeq2(accessible_world(skc9, V_378), true, man(V_378, skc11), true)=true))). % 19.88/10.11 tff(c_4718, plain, (nonexistent(skc14, skc15)=true)). % 19.88/10.11 tff(c_4681, plain, (organism(skc14, skc17)=true)). % 19.88/10.11 tff(c_4571, plain, (ifeq2(smoke(skc14, skc15), true, true, true)=true)). % 19.88/10.11 tff(c_4643, plain, (vincent_forename(skc14, skc16)=true)). % 19.88/10.11 tff(c_2607, plain, (![V_340]: (ifeq2(accessible_world(skc9, V_340), true, vincent_forename(V_340, skc16), true)=true))). % 19.88/10.11 tff(c_4585, plain, (eventuality(skc14, skc15)=true)). % 19.88/10.11 tff(c_4565, plain, (ifeq2(state(skc14, skc15), true, true, true)=true)). % 19.88/10.11 tff(c_4544, plain, (event(skc14, skc15)=true)). % 19.88/10.11 tff(c_4499, plain, (male(skc14, skc17)=true)). % 19.88/10.11 tff(c_1855, plain, (![V_301]: (ifeq2(accessible_world(skc9, V_301), true, event(V_301, skc15), true)=true))). % 19.88/10.11 tff(c_4462, plain, (human_person(skc14, skc17)=true)). % 19.88/10.11 tff(c_4419, plain, (man(skc14, skc17)=true)). % 19.88/10.11 tff(c_4368, plain, (thing(skc14, skc10)=true)). % 19.88/10.11 tff(c_3329, plain, (![V_378]: (ifeq2(accessible_world(skc9, V_378), true, man(V_378, skc17), true)=true))). % 19.88/10.11 tff(c_4334, plain, (unisex(skc14, skc10)=true)). % 19.88/10.11 tff(c_4101, plain, (ifeq2(smoke(skc14, skc10), true, true, true)=true)). % 19.88/10.11 tff(c_4229, plain, (ifeq2(relname(skc14, skc14), true, true, true)=true)). % 19.88/10.11 tff(c_4292, plain, (specific(skc14, skc10)=true)). % 19.88/10.11 tff(c_2217, plain, (![V_319]: (ifeq2(accessible_world(skc9, V_319), true, forename(V_319, skc12), true)=true))). % 19.88/10.11 tff(c_4242, plain, (nonexistent(skc14, skc10)=true)). % 19.88/10.11 tff(c_4208, plain, (relation(skc14, skc14)=true)). % 19.88/10.11 tff(c_4169, plain, (proposition(skc14, skc14)=true)). % 19.88/10.11 tff(c_1896, plain, (![V_304]: (ifeq2(accessible_world(skc9, V_304), true, proposition(V_304, skc14), true)=true))). % 19.88/10.11 tff(c_4111, plain, (eventuality(skc14, skc10)=true)). % 19.88/10.11 tff(c_4077, plain, (event(skc14, skc10)=true)). % 19.88/10.11 tff(c_4043, plain, (state(skc14, skc10)=true)). % 19.88/10.11 tff(c_3122, plain, (![V_369]: (ifeq2(accessible_world(skc9, V_369), true, state(V_369, skc10), true)=true))). % 19.88/10.11 tff(c_3995, plain, (unisex(skc14, skc12)=true)). % 19.88/10.11 tff(c_3964, plain, (general(skc14, skc12)=true)). % 19.88/10.11 tff(c_3929, plain, (think_believe_consider(skc14, skc15)=true)). % 19.88/10.11 tff(c_1799, plain, (![W_298]: (ifeq2(think_believe_consider(skc9, W_298), true, think_believe_consider(skc14, W_298), true)=true))). % 19.88/10.11 tff(c_3888, plain, (nonhuman(skc14, skc12)=true)). % 19.88/10.11 tff(c_3722, plain, (ifeq2(proposition(skc14, skc12), true, true, true)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3803, plain, (abstraction(skc14, skc12)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3704, plain, (relation(skc14, skc12)=true)). % 19.88/10.11 tff(c_3639, plain, (ifeq2(vincent_forename(skc14, skc12), true, true, true)=true)). % 19.88/10.11 tff(c_3652, plain, (relname(skc14, skc12)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3601, plain, (forename(skc14, skc12)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3570, plain, (jules_forename(skc14, skc12)=true)). % 19.88/10.11 tff(c_2760, plain, (![V_349]: (ifeq2(accessible_world(skc9, V_349), true, jules_forename(V_349, skc12), true)=true))). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3292, plain, (ifeq2(entity(skc14, skc16), true, true, true)=true)). % 19.88/10.11 tff(c_3356, plain, (ifeq2(eventuality(skc14, skc16), true, true, true)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3479, plain, (singleton(skc14, skc16)=true)). % 19.88/10.11 tff(c_3428, plain, (nonhuman(skc14, skc16)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3369, plain, (general(skc14, skc16)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3335, plain, (unisex(skc14, skc16)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3274, plain, (thing(skc14, skc16)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3203, plain, (abstraction(skc14, skc16)=true)). % 19.88/10.11 tff(c_3183, plain, (ifeq2(proposition(skc14, skc16), true, true, true)=true)). % 19.88/10.11 tff(c_3134, plain, (relation(skc14, skc16)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3075, plain, (ifeq2(jules_forename(skc14, skc16), true, true, true)=true)). % 19.88/10.11 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))). % 19.88/10.11 tff(c_3085, plain, (relname(skc14, skc16)=true)). % 19.88/10.11 tff(c_3028, plain, (forename(skc14, skc16)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_3011, plain, (ifeq2(accessible_world(skc9, skc9), true, true, true)=true)). % 19.88/10.12 tff(c_2218, plain, (![V_319]: (ifeq2(accessible_world(skc9, V_319), true, forename(V_319, skc16), true)=true))). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2935, plain, (present(skc14, skc15)=true)). % 19.88/10.12 tff(c_2454, plain, (![W_331]: (ifeq2(present(skc9, W_331), true, present(skc14, W_331), true)=true))). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2866, plain, (singleton(skc9, skc17)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2814, plain, (singleton(skc9, skc11)=true)). % 19.88/10.12 tff(c_2420, plain, (ifeq2(abstraction(skc9, skc17), true, true, true)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2417, plain, (ifeq2(eventuality(skc9, skc17), true, true, true)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2719, plain, (singleton(skc9, skc16)=true)). % 19.88/10.12 tff(c_2664, plain, (singleton(skc9, skc12)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1919, plain, (ifeq2(eventuality(skc9, skc12), true, true, true)=true)). % 19.88/10.12 tff(c_1913, plain, (ifeq2(entity(skc9, skc12), true, true, true)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2475, plain, (ifeq2(abstraction(skc9, skc11), true, true, true)=true)). % 19.88/10.12 tff(c_2472, plain, (ifeq2(eventuality(skc9, skc11), true, true, true)=true)). % 19.88/10.12 tff(c_2583, plain, (ifeq2(eventuality(skc9, skc16), true, true, true)=true)). % 19.88/10.12 tff(c_2026, plain, (ifeq2(entity(skc9, skc16), true, true, true)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2568, plain, (unisex(skc9, skc16)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2534, plain, (general(skc9, skc12)=true)). % 19.88/10.12 tff(c_2513, plain, (singleton(skc9, skc14)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1182, plain, (ifeq2(entity(skc9, skc14), true, true, true)=true)). % 19.88/10.12 tff(c_2431, plain, (thing(skc9, skc11)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2393, plain, (thing(skc9, skc17)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2338, plain, (existent(skc9, skc11)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2287, plain, (unisex(skc9, skc12)=true)). % 19.88/10.12 tff(c_2236, plain, (specific(skc9, skc11)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2188, plain, (general(skc9, skc16)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2164, plain, (existent(skc9, skc17)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2092, plain, (specific(skc9, skc17)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_2044, plain, (nonhuman(skc9, skc16)=true)). % 19.88/10.12 tff(c_2014, plain, (thing(skc9, skc16)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1966, plain, (nonhuman(skc9, skc12)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_975, plain, (ifeq2(eventuality(skc9, skc14), true, true, true)=true)). % 19.88/10.12 tff(c_1901, plain, (thing(skc9, skc12)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1825, plain, (abstraction(skc9, skc16)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1804, plain, (impartial(skc9, skc17)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1766, plain, (living(skc9, skc17)=true)). % 19.88/10.12 tff(c_1490, plain, (ifeq2(abstraction(skc9, skc10), true, true, true)=true)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_1717, plain, (impartial(skc9, skc11)=true)). % 19.88/10.12 tff(c_1093, plain, (ifeq2(entity(skc9, skc10), true, true, true)=true)). % 19.88/10.12 tff(c_194, plain, (![U_204, V_205]: (ifeq(tuple(nonexistent(U_204, V_205), existent(U_204, V_205)), tuple(true, true), a, b)=b))). % 19.88/10.12 tff(c_1679, plain, (living(skc9, skc11)=true)). % 19.88/10.12 tff(c_188, plain, (![U_198, V_199]: (ifeq(tuple(unisex(U_198, V_199), male(U_198, V_199)), tuple(true, true), a, b)=b))). % 19.88/10.12 tff(c_1636, plain, (singleton(skc9, skc10)=true)). % 19.88/10.12 tff(c_1606, plain, (entity(skc9, skc17)=true)). % 19.88/10.12 tff(c_192, plain, (![U_202, V_203]: (ifeq(tuple(human(U_202, V_203), nonhuman(U_202, V_203)), tuple(true, true), a, b)=b))). % 19.88/10.12 tff(c_1560, plain, (entity(skc9, skc11)=true)). % 19.88/10.12 tff(c_190, plain, (![U_200, V_201]: (ifeq(tuple(specific(U_200, V_201), general(U_200, V_201)), tuple(true, true), a, b)=b))). % 19.88/10.12 tff(c_1390, plain, (ifeq2(entity(skc9, skc15), true, true, true)=true)). % 19.88/10.12 tff(c_1399, plain, (ifeq2(abstraction(skc9, skc15), true, true, true)=true)). % 19.88/10.12 tff(c_186, plain, (![U_197]: (ifeq2(man(skc14, U_197), true, agent(skc14, skf1(U_197), U_197), true)=true))). % 19.88/10.12 tff(c_1506, plain, (singleton(skc9, skc15)=true)). % 19.88/10.12 tff(c_1475, plain, (unisex(skc9, skc10)=true)). % 19.88/10.12 tff(c_1451, plain, (unisex(skc9, skc15)=true)). % 19.88/10.12 tff(c_1412, plain, (specific(skc9, skc15)=true)). % 19.88/10.12 tff(c_1352, plain, (ifeq2(smoke(skc9, skc10), true, true, true)=true)). % 19.88/10.12 tff(c_1378, plain, (thing(skc9, skc15)=true)). % 19.88/10.12 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, unisex(U_20, V_21), true)=true))). % 19.88/10.12 tff(c_1334, plain, (event(skc9, skc10)=true)). % 19.88/10.12 tff(c_20, plain, (![U_22, V_23]: (ifeq2(state(U_22, V_23), true, event(U_22, V_23), true)=true))). % 19.88/10.12 tff(c_1299, plain, (nonexistent(skc9, skc15)=true)). % 19.88/10.12 tff(c_1273, plain, (ifeq2(state(skc9, skc15), true, true, true)=true)). % 19.88/10.12 tff(c_28, plain, (![U_30, V_31]: (ifeq2(organism(U_30, V_31), true, entity(U_30, V_31), true)=true))). % 19.88/10.12 tff(c_1249, plain, (eventuality(skc9, skc15)=true)). % 19.88/10.12 tff(c_22, plain, (![U_24, V_25]: (ifeq2(event(U_24, V_25), true, eventuality(U_24, V_25), true)=true))). % 19.88/10.12 tff(c_1215, plain, (nonhuman(skc9, skc14)=true)). % 19.88/10.12 tff(c_1188, plain, (organism(skc9, skc17)=true)). % 19.88/10.12 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, thing(U_32, V_33), true)=true))). % 19.88/10.12 tff(c_1148, plain, (organism(skc9, skc11)=true)). % 19.88/10.12 tff(c_26, plain, (![U_28, V_29]: (ifeq2(human_person(U_28, V_29), true, organism(U_28, V_29), true)=true))). % 19.88/10.12 tff(c_1102, plain, (abstraction(skc9, skc12)=true)). % 19.88/10.12 tff(c_1065, plain, (specific(skc9, skc10)=true)). % 19.88/10.12 tff(c_12, plain, (![U_14, V_15]: (ifeq2(thing(U_14, V_15), true, singleton(U_14, V_15), true)=true))). % 19.88/10.12 tff(c_1034, plain, (general(skc9, skc14)=true)). % 19.88/10.12 tff(c_14, plain, (![U_16, V_17]: (ifeq2(eventuality(U_16, V_17), true, specific(U_16, V_17), true)=true))). % 19.88/10.12 tff(c_777, plain, (ifeq2(proposition(skc9, skc16), true, true, true)=true)). % 19.88/10.12 tff(c_737, plain, (ifeq2(proposition(skc9, skc12), true, true, true)=true)). % 19.88/10.12 tff(c_995, plain, (thing(skc9, skc10)=true)). % 19.88/10.12 tff(c_34, plain, (![U_36, V_37]: (ifeq2(entity(U_36, V_37), true, existent(U_36, V_37), true)=true))). % 19.88/10.12 tff(c_961, plain, (human(skc9, skc17)=true)). % 19.88/10.12 tff(c_10, plain, (![U_12, V_13]: (ifeq2(eventuality(U_12, V_13), true, thing(U_12, V_13), true)=true))). % 19.88/10.12 tff(c_940, plain, (animate(skc9, skc17)=true)). % 19.88/10.12 tff(c_38, plain, (![U_40, V_41]: (ifeq2(organism(U_40, V_41), true, living(U_40, V_41), true)=true))). % 19.88/10.12 tff(c_912, plain, (nonexistent(skc9, skc10)=true)). % 19.88/10.12 tff(c_36, plain, (![U_38, V_39]: (ifeq2(organism(U_38, V_39), true, impartial(U_38, V_39), true)=true))). % 19.88/10.12 tff(c_884, plain, (human(skc9, skc11)=true)). % 19.88/10.12 tff(c_863, plain, (animate(skc9, skc11)=true)). % 19.88/10.12 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, nonexistent(U_18, V_19), true)=true))). % 19.88/10.12 tff(c_826, plain, (human_person(skc9, skc11)=true)). % 19.88/10.12 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, human(U_42, V_43), true)=true))). % 19.88/10.12 tff(c_792, plain, (human_person(skc9, skc17)=true)). % 19.88/10.12 tff(c_756, plain, (relation(skc9, skc16)=true)). % 19.88/10.12 tff(c_24, plain, (![U_26, V_27]: (ifeq2(man(U_26, V_27), true, human_person(U_26, V_27), true)=true))). % 19.88/10.12 tff(c_722, plain, (relation(skc9, skc12)=true)). % 19.88/10.12 tff(c_42, plain, (![U_44, V_45]: (ifeq2(human_person(U_44, V_45), true, animate(U_44, V_45), true)=true))). % 19.88/10.12 tff(c_694, plain, (relname(skc9, skc16)=true)). % 19.88/10.12 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, specific(U_34, V_35), true)=true))). % 19.88/10.12 tff(c_663, plain, (relname(skc9, skc12)=true)). % 19.88/10.12 tff(c_46, plain, (![U_48, V_49]: (ifeq2(forename(U_48, V_49), true, relname(U_48, V_49), true)=true))). % 19.88/10.12 tff(c_629, plain, (male(skc9, skc11)=true)). % 19.88/10.12 tff(c_608, plain, (male(skc9, skc17)=true)). % 19.88/10.12 tff(c_44, plain, (![U_46, V_47]: (ifeq2(man(U_46, V_47), true, male(U_46, V_47), true)=true))). % 19.88/10.12 tff(c_574, plain, (ifeq2(smoke(skc9, skc15), true, true, true)=true)). % 19.88/10.12 tff(c_560, plain, (thing(skc9, skc14)=true)). % 19.88/10.12 tff(c_62, plain, (![U_64, V_65]: (ifeq2(smoke(U_64, V_65), true, event(U_64, V_65), true)=true))). % 19.88/10.12 tff(c_539, plain, (unisex(skc9, skc14)=true)). % 19.88/10.12 tff(c_524, plain, (ifeq2(vincent_forename(skc9, skc12), true, true, true)=true)). % 19.88/10.12 tff(c_66, plain, (![U_68, V_69]: (ifeq2(vincent_forename(U_68, V_69), true, forename(U_68, V_69), true)=true))). % 19.88/10.12 tff(c_479, plain, (ifeq2(jules_forename(skc9, skc16), true, true, true)=true)). % 19.88/10.12 tff(c_462, plain, (abstraction(skc9, skc14)=true)). % 19.88/10.12 tff(c_60, plain, (![U_62, V_63]: (ifeq2(jules_forename(U_62, V_63), true, forename(U_62, V_63), true)=true))). % 19.88/10.12 tff(c_446, plain, (ifeq2(relname(skc9, skc14), true, true, true)=true)). % 19.88/10.12 tff(c_431, plain, (relation(skc9, skc14)=true)). % 19.88/10.12 tff(c_58, plain, (![U_60, V_61]: (ifeq2(abstraction(U_60, V_61), true, unisex(U_60, V_61), true)=true))). % 19.88/10.12 tff(c_64, plain, (![U_66, V_67]: (ifeq2(proposition(U_66, V_67), true, relation(U_66, V_67), true)=true))). % 19.88/10.12 tff(c_56, plain, (![U_58, V_59]: (ifeq2(abstraction(U_58, V_59), true, general(U_58, V_59), true)=true))). % 19.88/10.12 tff(c_375, plain, (be(skc9, skc10, skc11, skc11)=true)). % 19.88/10.12 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, nonhuman(U_56, V_57), true)=true))). % 19.88/10.12 tff(c_376, plain, (of(skc9, skc12, skc11)=true)). % 19.88/10.12 tff(c_367, plain, (skc13=skc11)). % 19.88/10.12 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))). % 19.88/10.12 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, thing(U_54, V_55), true)=true))). % 19.88/10.12 tff(c_327, plain, (eventuality(skc9, skc10)=true)). % 19.88/10.12 tff(c_48, plain, (![U_50, V_51]: (ifeq2(relname(U_50, V_51), true, relation(U_50, V_51), true)=true))). % 19.88/10.12 tff(c_8, plain, (![U_10, V_11]: (ifeq2(state(U_10, V_11), true, eventuality(U_10, V_11), true)=true))). % 19.88/10.12 tff(c_50, plain, (![U_52, V_53]: (ifeq2(relation(U_52, V_53), true, abstraction(U_52, V_53), true)=true))). % 19.88/10.12 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 19.88/10.12 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 19.88/10.12 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 19.88/10.12 tff(c_172, plain, (agent(skc9, skc15, skc17)=true)). % 19.88/10.12 tff(c_174, plain, (theme(skc9, skc15, skc14)=true)). % 19.88/10.12 tff(c_170, plain, (of(skc9, skc16, skc17)=true)). % 19.88/10.12 tff(c_148, plain, (vincent_forename(skc9, skc16)=true)). % 19.88/10.12 tff(c_150, plain, (event(skc9, skc15)=true)). % 19.88/10.12 tff(c_152, plain, (present(skc9, skc15)=true)). % 19.88/10.12 tff(c_154, plain, (think_believe_consider(skc9, skc15)=true)). % 19.88/10.12 tff(c_158, plain, (forename(skc9, skc12)=true)). % 19.88/10.12 tff(c_146, plain, (forename(skc9, skc16)=true)). % 19.88/10.12 tff(c_144, plain, (man(skc9, skc17)=true)). % 19.88/10.12 tff(c_168, plain, (proposition(skc9, skc14)=true)). % 19.88/10.12 tff(c_160, plain, (jules_forename(skc9, skc12)=true)). % 19.88/10.12 tff(c_162, plain, (man(skc9, skc11)=true)). % 19.88/10.12 tff(c_164, plain, (state(skc9, skc10)=true)). % 19.88/10.12 tff(c_166, plain, (accessible_world(skc9, skc14)=true)). % 19.88/10.12 tff(c_142, plain, (actual_world(skc9)=true)). % 19.88/10.12 tff(c_196, plain, (b!=a)). % 19.88/10.12 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.88/10.12 %------------------------------------------------------------------------------