%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP226-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 07:48:40 PM UTC 2025 % Result : Satisfiable 19.81s 9.36s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP226-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 09:32:19 EDT 2025 % 0.13/0.33 % CPUTime : % 19.81/9.36 % 19.81/9.36 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.81/9.36 % 19.81/9.36 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.81/9.37 %$ ifeq3 > ifeq2 > ifeq > be > theme > of > agent > vincent_forename > unisex > tuple > think_believe_consider > thing > state > specific > smoke > singleton > relname > relation > proposition > present > organism > nonhuman > nonexistent > man > male > living > jules_forename > impartial > human_person > human > general > forename > existent > eventuality > event > entity > animate > accessible_world > abstraction > #nlpp > skf1 > actual_world > true > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 > b > a % 19.81/9.37 % 19.81/9.37 %Foreground sorts: % 19.81/9.37 % 19.81/9.37 % 19.81/9.37 %Background operators: % 19.81/9.37 % 19.81/9.37 % 19.81/9.37 %Foreground operators: % 19.81/9.37 tff(agent, type, agent: ($i * $i * $i) > $i). % 19.81/9.37 tff(proposition, type, proposition: ($i * $i) > $i). % 19.81/9.37 tff(specific, type, specific: ($i * $i) > $i). % 19.81/9.37 tff(organism, type, organism: ($i * $i) > $i). % 19.81/9.37 tff(impartial, type, impartial: ($i * $i) > $i). % 19.81/9.37 tff(skc11, type, skc11: $i). % 19.81/9.37 tff(a, type, a: $i). % 19.81/9.37 tff(smoke, type, smoke: ($i * $i) > $i). % 19.81/9.37 tff(jules_forename, type, jules_forename: ($i * $i) > $i). % 19.81/9.37 tff(skc9, type, skc9: $i). % 19.81/9.37 tff(eventuality, type, eventuality: ($i * $i) > $i). % 19.81/9.37 tff(theme, type, theme: ($i * $i * $i) > $i). % 19.81/9.37 tff(state, type, state: ($i * $i) > $i). % 19.81/9.37 tff(tuple, type, tuple: ($i * $i) > $i). % 19.81/9.37 tff(human_person, type, human_person: ($i * $i) > $i). % 19.81/9.37 tff(skf1, type, skf1: $i > $i). % 19.81/9.37 tff(be, type, be: ($i * $i * $i * $i) > $i). % 19.81/9.37 tff(skc8, type, skc8: $i). % 19.81/9.37 tff(relname, type, relname: ($i * $i) > $i). % 19.81/9.37 tff(skc14, type, skc14: $i). % 19.81/9.37 tff(skc13, type, skc13: $i). % 19.81/9.37 tff(thing, type, thing: ($i * $i) > $i). % 19.81/9.37 tff(unisex, type, unisex: ($i * $i) > $i). % 19.81/9.37 tff(abstraction, type, abstraction: ($i * $i) > $i). % 19.81/9.37 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 19.81/9.37 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 19.81/9.37 tff(relation, type, relation: ($i * $i) > $i). % 19.81/9.37 tff(actual_world, type, actual_world: $i > $i). % 19.81/9.37 tff(of, type, of: ($i * $i * $i) > $i). % 19.81/9.37 tff(present, type, present: ($i * $i) > $i). % 19.81/9.37 tff(b, type, b: $i). % 19.81/9.37 tff(animate, type, animate: ($i * $i) > $i). % 19.81/9.37 tff(human, type, human: ($i * $i) > $i). % 19.81/9.37 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 19.81/9.37 tff(skc15, type, skc15: $i). % 19.81/9.37 tff(existent, type, existent: ($i * $i) > $i). % 19.81/9.37 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 19.81/9.37 tff(forename, type, forename: ($i * $i) > $i). % 19.81/9.37 tff(true, type, true: $i). % 19.81/9.37 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 19.81/9.37 tff(male, type, male: ($i * $i) > $i). % 19.81/9.37 tff(skc12, type, skc12: $i). % 19.81/9.37 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 19.81/9.37 tff(entity, type, entity: ($i * $i) > $i). % 19.81/9.37 tff(skc10, type, skc10: $i). % 19.81/9.37 tff(singleton, type, singleton: ($i * $i) > $i). % 19.81/9.37 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 19.81/9.37 tff(event, type, event: ($i * $i) > $i). % 19.81/9.37 tff(man, type, man: ($i * $i) > $i). % 19.81/9.37 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 19.81/9.37 tff(general, type, general: ($i * $i) > $i). % 19.81/9.37 tff(living, type, living: ($i * $i) > $i). % 19.81/9.37 % 19.81/9.37 %Saturated clause set: % 19.81/9.37 tff(c_7969, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc12, skf1(skc10), W_185), true, ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, X_188, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.37 tff(c_7808, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(theme(skc12, skf1(skc15), V_190), true, ifeq3(agent(skc12, Y_189, skc15), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.37 tff(c_18424, plain, (![W_1091, V_1093]: (ifeq3(theme(skc12, skf1(skc15), W_1091), true, ifeq3(theme(skc12, skf1(skc15), V_1093), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1091), true, ifeq3(proposition(skc12, V_1093), true, V_1093, W_1091), W_1091), W_1091), W_1091), W_1091), W_1091)=W_1091))). % 19.81/9.37 tff(c_7807, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc12, skf1(skc15), W_185), true, ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, X_188, skc15), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.37 tff(c_18095, plain, (![W_1073, V_1074]: (ifeq3(theme(skc12, skf1(skc10), W_1073), true, ifeq3(theme(skc12, skf1(skc10), V_1074), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1073), true, ifeq3(proposition(skc12, V_1074), true, V_1074, W_1073), W_1073), W_1073), W_1073), W_1073), W_1073)=W_1073))). % 19.81/9.37 tff(c_17844, plain, (![W_1058, X_1059]: (ifeq3(theme(skc12, skf1(skc15), W_1058), true, ifeq3(theme(skc12, X_1059, skc12), true, ifeq3(agent(skc12, X_1059, skc15), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, X_1059), true, ifeq3(proposition(skc12, W_1058), true, skc12, W_1058), W_1058), W_1058), W_1058), W_1058), W_1058)=W_1058))). % 19.81/9.37 tff(c_18238, plain, (![W_1083]: (ifeq3(theme(skc12, skf1(skc15), W_1083), true, ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1083), true, skc12, W_1083), W_1083), W_1083), W_1083), W_1083)=W_1083))). % 19.81/9.37 tff(c_17842, plain, (![W_1058, X_1059]: (ifeq3(theme(skc12, skf1(skc10), W_1058), true, ifeq3(theme(skc12, X_1059, skc12), true, ifeq3(agent(skc12, X_1059, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, X_1059), true, ifeq3(proposition(skc12, W_1058), true, skc12, W_1058), W_1058), W_1058), W_1058), W_1058), W_1058)=W_1058))). % 19.81/9.37 tff(c_17845, plain, (![Y_1057, W_1058]: (ifeq3(theme(skc12, Y_1057, W_1058), true, ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(agent(skc12, Y_1057, skc15), true, ifeq3(think_believe_consider(skc12, Y_1057), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1058), true, skc12, W_1058), W_1058), W_1058), W_1058), W_1058), W_1058)=W_1058))). % 19.81/9.37 tff(c_17712, plain, (![Y_1049, V_1051]: (ifeq3(theme(skc12, Y_1049, skc12), true, ifeq3(theme(skc12, skf1(skc15), V_1051), true, ifeq3(agent(skc12, Y_1049, skc15), true, ifeq3(think_believe_consider(skc12, Y_1049), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, V_1051), true, V_1051, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_17531, plain, (![W_1037, V_1038]: (ifeq3(theme(skc12, skf1(skc10), W_1037), true, ifeq3(theme(skc12, skc13, V_1038), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1037), true, ifeq3(proposition(skc12, V_1038), true, V_1038, W_1037), W_1037), W_1037), W_1037), W_1037), W_1037)=W_1037))). % 19.81/9.37 tff(c_18122, plain, (![V_1076]: (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(theme(skc12, skf1(skc15), V_1076), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, V_1076), true, V_1076, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_17711, plain, (![X_1050, V_1051]: (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(theme(skc12, X_1050, V_1051), true, ifeq3(agent(skc12, X_1050, skc15), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, X_1050), true, ifeq3(proposition(skc12, V_1051), true, V_1051, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_7970, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(theme(skc12, skf1(skc10), V_190), true, ifeq3(agent(skc12, Y_189, skc10), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.37 tff(c_17710, plain, (![Y_1049, V_1051]: (ifeq3(theme(skc12, Y_1049, skc12), true, ifeq3(theme(skc12, skf1(skc10), V_1051), true, ifeq3(agent(skc12, Y_1049, skc10), true, ifeq3(think_believe_consider(skc12, Y_1049), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, V_1051), true, V_1051, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_17992, plain, (![V_1067]: (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(theme(skc12, skf1(skc10), V_1067), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, V_1067), true, V_1067, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_17959, plain, (![W_1065]: (ifeq3(theme(skc12, skf1(skc10), W_1065), true, ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1065), true, skc12, W_1065), W_1065), W_1065), W_1065), W_1065)=W_1065))). % 19.81/9.37 tff(c_17709, plain, (![X_1050, V_1051]: (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(theme(skc12, X_1050, V_1051), true, ifeq3(agent(skc12, X_1050, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, X_1050), true, ifeq3(proposition(skc12, V_1051), true, V_1051, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.37 tff(c_17843, plain, (![Y_1057, W_1058]: (ifeq3(theme(skc12, Y_1057, W_1058), true, ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(agent(skc12, Y_1057, skc10), true, ifeq3(think_believe_consider(skc12, Y_1057), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1058), true, skc12, W_1058), W_1058), W_1058), W_1058), W_1058), W_1058)=W_1058))). % 19.81/9.37 tff(c_17758, plain, (![Y_1053]: (ifeq3(theme(skc12, Y_1053, skc12), true, ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(agent(skc12, Y_1053, skc10), true, ifeq3(think_believe_consider(skc12, Y_1053), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, skc12, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17759, plain, (![X_1054]: (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(theme(skc12, X_1054, skc12), true, ifeq3(agent(skc12, X_1054, skc15), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, X_1054), true, skc12, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17872, plain, (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, skc12, skc12), skc12), skc12), skc12)=skc12)). % 19.81/9.38 tff(c_17760, plain, (![Y_1053]: (ifeq3(theme(skc12, Y_1053, skc12), true, ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(agent(skc12, Y_1053, skc15), true, ifeq3(think_believe_consider(skc12, Y_1053), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, skc12, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_4629, plain, (![Y_189, W_185, X_188, Z_187]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(theme(skc12, X_188, skc12), true, ifeq3(agent(skc12, Y_189, Z_187), true, ifeq3(agent(skc12, X_188, Z_187), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, W_185), true, skc12, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_17783, plain, (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, skc12, skc12), skc12), skc12), skc12)=skc12)). % 19.81/9.38 tff(c_17757, plain, (![X_1054]: (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(theme(skc12, X_1054, skc12), true, ifeq3(agent(skc12, X_1054, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(think_believe_consider(skc12, X_1054), true, skc12, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17717, plain, (![Y_1049, X_1050, Z_1052]: (ifeq3(theme(skc12, Y_1049, skc12), true, ifeq3(theme(skc12, X_1050, skc12), true, ifeq3(agent(skc12, Y_1049, Z_1052), true, ifeq3(agent(skc12, X_1050, Z_1052), true, ifeq3(think_believe_consider(skc12, Y_1049), true, ifeq3(think_believe_consider(skc12, X_1050), true, skc12, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_4628, plain, (![Y_189, X_188, V_190, Z_187]: (ifeq3(theme(skc12, Y_189, skc12), true, ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, Y_189, Z_187), true, ifeq3(agent(skc12, X_188, Z_187), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, V_190), true, V_190, skc12), skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17398, plain, (![W_1028, V_1030]: (ifeq3(theme(skc12, skc13, W_1028), true, ifeq3(theme(skc12, skf1(skc10), V_1030), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1028), true, ifeq3(proposition(skc12, V_1030), true, V_1030, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.81/9.38 tff(c_17624, plain, (![V_1044]: (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(theme(skc12, skc13, V_1044), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, V_1044), true, V_1044, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17537, plain, (![Y_1036, V_1038, Z_1039]: (ifeq3(theme(skc12, Y_1036, skc12), true, ifeq3(theme(skc12, skc13, V_1038), true, ifeq3(agent(skc12, Y_1036, Z_1039), true, ifeq3(agent(skc12, skc13, Z_1039), true, ifeq3(think_believe_consider(skc12, Y_1036), true, ifeq3(proposition(skc12, V_1038), true, V_1038, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17406, plain, (![W_1028, V_1030, Z_1031]: (ifeq3(theme(skc12, skc13, W_1028), true, ifeq3(theme(skc12, skc13, V_1030), true, ifeq3(agent(skc12, skc13, Z_1031), true, ifeq3(agent(skc12, skc13, Z_1031), true, ifeq3(proposition(skc12, W_1028), true, ifeq3(proposition(skc12, V_1030), true, V_1030, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.81/9.38 tff(c_3934, plain, (![Y_189, W_185, V_190, Z_187]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(theme(skc12, skc13, V_190), true, ifeq3(agent(skc12, Y_189, Z_187), true, ifeq3(agent(skc12, skc13, Z_187), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_17450, plain, (![W_1032]: (ifeq3(theme(skc12, skc13, W_1032), true, ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_1032), true, skc12, W_1032), W_1032), W_1032), W_1032), W_1032)=W_1032))). % 19.81/9.38 tff(c_17405, plain, (![W_1028, X_1029, Z_1031]: (ifeq3(theme(skc12, skc13, W_1028), true, ifeq3(theme(skc12, X_1029, skc12), true, ifeq3(agent(skc12, skc13, Z_1031), true, ifeq3(agent(skc12, X_1029, Z_1031), true, ifeq3(think_believe_consider(skc12, X_1029), true, ifeq3(proposition(skc12, W_1028), true, skc12, W_1028), W_1028), W_1028), W_1028), W_1028), W_1028)=W_1028))). % 19.81/9.38 tff(c_3933, plain, (![W_185, X_188, V_190, Z_187]: (ifeq3(theme(skc12, skc13, W_185), true, ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, skc13, Z_187), true, ifeq3(agent(skc12, X_188, Z_187), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_13977, plain, (![Y_830, V_832, Z_833]: (ifeq3(theme(skc8, Y_830, skc12), true, ifeq3(theme(skc8, skc13, V_832), true, ifeq3(agent(skc8, Y_830, Z_833), true, ifeq3(agent(skc8, skc13, Z_833), true, ifeq3(think_believe_consider(skc8, Y_830), true, ifeq3(proposition(skc8, V_832), true, V_832, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17181, plain, (![W_1015, V_1016]: (ifeq3(theme(skc12, skf1(skc15), W_1015), true, ifeq3(theme(skc12, skc13, V_1016), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1015), true, ifeq3(proposition(skc12, V_1016), true, V_1016, W_1015), W_1015), W_1015), W_1015), W_1015)=W_1015))). % 19.81/9.38 tff(c_17233, plain, (![V_1018]: (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(theme(skc12, skc13, V_1018), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, V_1018), true, V_1018, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_13979, plain, (![W_831, V_832, Z_833]: (ifeq3(theme(skc8, skc13, W_831), true, ifeq3(theme(skc8, skc13, V_832), true, ifeq3(agent(skc8, skc13, Z_833), true, ifeq3(agent(skc8, skc13, Z_833), true, ifeq3(proposition(skc8, W_831), true, ifeq3(proposition(skc8, V_832), true, V_832, W_831), W_831), W_831), W_831), W_831), W_831)=W_831))). % 19.81/9.38 tff(c_17185, plain, (![Y_1014, V_1016]: (ifeq3(theme(skc12, Y_1014, skc12), true, ifeq3(theme(skc12, skc13, V_1016), true, ifeq3(agent(skc12, Y_1014, skc15), true, ifeq3(think_believe_consider(skc12, Y_1014), true, ifeq3(proposition(skc12, V_1016), true, V_1016, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_6352, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(theme(skc12, skc13, V_190), true, ifeq3(agent(skc12, Y_189, skc15), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_16963, plain, (![W_1000, V_1002]: (ifeq3(theme(skc12, skc13, W_1000), true, ifeq3(theme(skc12, skf1(skc15), V_1002), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1000), true, ifeq3(proposition(skc12, V_1002), true, V_1002, W_1000), W_1000), W_1000), W_1000), W_1000)=W_1000))). % 19.81/9.38 tff(c_14397, plain, (![Y_856, X_858, Z_859]: (ifeq3(theme(skc8, Y_856, skc12), true, ifeq3(theme(skc8, X_858, skc12), true, ifeq3(agent(skc8, Y_856, Z_859), true, ifeq3(agent(skc8, X_858, Z_859), true, ifeq3(think_believe_consider(skc8, Y_856), true, ifeq3(think_believe_consider(skc8, X_858), true, skc12, skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_17056, plain, (![W_1006]: (ifeq3(theme(skc12, skc13, W_1006), true, ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_1006), true, skc12, W_1006), W_1006), W_1006), W_1006)=W_1006))). % 19.81/9.38 tff(c_16968, plain, (![W_1000, X_1001]: (ifeq3(theme(skc12, skc13, W_1000), true, ifeq3(theme(skc12, X_1001, skc12), true, ifeq3(agent(skc12, X_1001, skc15), true, ifeq3(think_believe_consider(skc12, X_1001), true, ifeq3(proposition(skc12, W_1000), true, skc12, W_1000), W_1000), W_1000), W_1000), W_1000)=W_1000))). % 19.81/9.38 tff(c_16716, plain, (![W_987]: (ifeq3(theme(skc12, skf1(skc10), W_987), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, W_987), true, skc12, W_987), W_987), W_987), W_987)=W_987))). % 19.81/9.38 tff(c_16966, plain, (![W_1000, V_1002]: (ifeq3(theme(skc12, skc13, W_1000), true, ifeq3(theme(skc12, skc13, V_1002), true, ifeq3(proposition(skc12, W_1000), true, ifeq3(proposition(skc12, V_1002), true, V_1002, W_1000), W_1000), W_1000), W_1000)=W_1000))). % 19.81/9.38 tff(c_6351, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc12, skc13, W_185), true, ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, X_188, skc15), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, W_185), true, ifeq3(proposition(skc12, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_16508, plain, (![V_973]: (ifeq3(theme(skc12, skf1(skc10), V_973), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, ifeq3(proposition(skc12, V_973), true, V_973, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16722, plain, (![W_987, Z_988]: (ifeq3(theme(skc12, skc13, W_987), true, ifeq3(agent(skc12, skc13, Z_988), true, ifeq3(agent(skc12, skc13, Z_988), true, ifeq3(proposition(skc12, W_987), true, skc12, W_987), W_987), W_987), W_987)=W_987))). % 19.81/9.38 tff(c_16721, plain, (![Y_986, Z_988]: (ifeq3(theme(skc12, Y_986, skc12), true, ifeq3(agent(skc12, Y_986, Z_988), true, ifeq3(agent(skc12, skc13, Z_988), true, ifeq3(think_believe_consider(skc12, Y_986), true, skc12, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16837, plain, (ifeq3(theme(skc12, skf1(skc10), skc12), true, ifeq3(agent(skc12, skc13, skc10), true, ifeq3(think_believe_consider(skc12, skf1(skc10)), true, skc12, skc12), skc12), skc12)=skc12)). % 19.81/9.38 tff(c_16513, plain, (![X_972, Z_974]: (ifeq3(theme(skc12, X_972, skc12), true, ifeq3(agent(skc12, skc13, Z_974), true, ifeq3(agent(skc12, X_972, Z_974), true, ifeq3(think_believe_consider(skc12, X_972), true, skc12, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16720, plain, (![Y_986, W_987]: (ifeq3(theme(skc12, Y_986, W_987), true, ifeq3(agent(skc12, Y_986, skc15), true, ifeq3(think_believe_consider(skc12, Y_986), true, ifeq3(proposition(skc12, W_987), true, skc12, W_987), W_987), W_987), W_987)=W_987))). % 19.81/9.38 tff(c_16717, plain, (![W_987]: (ifeq3(theme(skc12, skf1(skc15), W_987), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, W_987), true, skc12, W_987), W_987), W_987)=W_987))). % 19.81/9.38 tff(c_16719, plain, (![W_987]: (ifeq3(theme(skc12, skc13, W_987), true, ifeq3(proposition(skc12, W_987), true, skc12, W_987), W_987)=W_987))). % 19.81/9.38 tff(c_6416, plain, (![Y_189, W_185, Z_187]: (ifeq3(theme(skc12, Y_189, W_185), true, ifeq3(agent(skc12, Y_189, Z_187), true, ifeq3(agent(skc12, skc13, Z_187), true, ifeq3(think_believe_consider(skc12, Y_189), true, ifeq3(proposition(skc12, W_185), true, skc12, W_185), W_185), W_185), W_185), W_185)=W_185))). % 19.81/9.38 tff(c_16514, plain, (![V_973, Z_974]: (ifeq3(theme(skc12, skc13, V_973), true, ifeq3(agent(skc12, skc13, Z_974), true, ifeq3(agent(skc12, skc13, Z_974), true, ifeq3(proposition(skc12, V_973), true, V_973, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16628, plain, (![X_981]: (ifeq3(theme(skc12, X_981, skc12), true, ifeq3(agent(skc12, X_981, skc15), true, ifeq3(think_believe_consider(skc12, X_981), true, skc12, skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16511, plain, (![X_972, V_973]: (ifeq3(theme(skc12, X_972, V_973), true, ifeq3(agent(skc12, X_972, skc15), true, ifeq3(think_believe_consider(skc12, X_972), true, ifeq3(proposition(skc12, V_973), true, V_973, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_14192, plain, (![W_843, X_844, Z_846]: (ifeq3(theme(skc8, skc13, W_843), true, ifeq3(theme(skc8, X_844, skc12), true, ifeq3(agent(skc8, skc13, Z_846), true, ifeq3(agent(skc8, X_844, Z_846), true, ifeq3(think_believe_consider(skc8, X_844), true, ifeq3(proposition(skc8, W_843), true, skc12, W_843), W_843), W_843), W_843), W_843), W_843)=W_843))). % 19.81/9.38 tff(c_16555, plain, (ifeq3(theme(skc12, skf1(skc15), skc12), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, skc12, skc12), skc12)=skc12)). % 19.81/9.38 tff(c_16509, plain, (![V_973]: (ifeq3(theme(skc12, skf1(skc15), V_973), true, ifeq3(think_believe_consider(skc12, skf1(skc15)), true, ifeq3(proposition(skc12, V_973), true, V_973, skc12), skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16510, plain, (![Z_974]: (ifeq3(agent(skc12, skc13, Z_974), true, ifeq3(agent(skc12, skc13, Z_974), true, skc12, skc12), skc12)=skc12))). % 19.81/9.38 tff(c_16512, plain, (![V_973]: (ifeq3(theme(skc12, skc13, V_973), true, ifeq3(proposition(skc12, V_973), true, V_973, skc12), skc12)=skc12))). % 19.81/9.38 tff(c_6415, plain, (![X_188, V_190, Z_187]: (ifeq3(theme(skc12, X_188, V_190), true, ifeq3(agent(skc12, skc13, Z_187), true, ifeq3(agent(skc12, X_188, Z_187), true, ifeq3(think_believe_consider(skc12, X_188), true, ifeq3(proposition(skc12, V_190), true, V_190, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_14395, plain, (![W_857, X_858]: (ifeq3(theme(skc8, skc13, W_857), true, ifeq3(theme(skc8, X_858, skc12), true, ifeq3(agent(skc8, X_858, skc15), true, ifeq3(think_believe_consider(skc8, X_858), true, ifeq3(proposition(skc8, W_857), true, skc12, W_857), W_857), W_857), W_857), W_857)=W_857))). % 19.81/9.39 tff(c_13768, plain, (![Y_817, V_819]: (ifeq3(theme(skc8, Y_817, skc12), true, ifeq3(theme(skc8, skc13, V_819), true, ifeq3(agent(skc8, Y_817, skc15), true, ifeq3(think_believe_consider(skc8, Y_817), true, ifeq3(proposition(skc8, V_819), true, V_819, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_13206, plain, (![Y_781, Z_783]: (ifeq3(theme(skc8, Y_781, skc12), true, ifeq3(agent(skc8, Y_781, Z_783), true, ifeq3(agent(skc8, skc13, Z_783), true, ifeq3(think_believe_consider(skc8, Y_781), true, skc12, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_13001, plain, (![V_770, Z_771]: (ifeq3(theme(skc8, skc13, V_770), true, ifeq3(agent(skc8, skc13, Z_771), true, ifeq3(agent(skc8, skc13, Z_771), true, ifeq3(proposition(skc8, V_770), true, V_770, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_5142, plain, (![W_182, V_184]: (ifeq3(of(skc12, W_182, skc15), true, ifeq3(of(skc12, V_184, skc15), true, ifeq3(forename(skc12, W_182), true, ifeq3(forename(skc12, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 19.81/9.39 tff(c_5715, plain, (![W_182, V_184]: (ifeq3(of(skc12, W_182, skc10), true, ifeq3(of(skc12, V_184, skc10), true, ifeq3(forename(skc12, W_182), true, ifeq3(forename(skc12, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 19.81/9.39 tff(c_3664, plain, (![W_406, V_408]: (ifeq3(of(skc8, W_406, skc10), true, ifeq3(of(skc8, V_408, skc10), true, ifeq3(forename(skc8, W_406), true, ifeq3(forename(skc8, V_408), true, W_406, V_408), V_408), V_408), V_408)=V_408))). % 19.81/9.39 tff(c_3663, plain, (![W_406, V_408]: (ifeq3(of(skc8, W_406, skc15), true, ifeq3(of(skc8, V_408, skc15), true, ifeq3(forename(skc8, W_406), true, ifeq3(forename(skc8, V_408), true, W_406, V_408), V_408), V_408), V_408)=V_408))). % 19.81/9.39 tff(c_13207, plain, (![W_782, Z_783]: (ifeq3(theme(skc8, skc13, W_782), true, ifeq3(agent(skc8, skc13, Z_783), true, ifeq3(agent(skc8, skc13, Z_783), true, ifeq3(proposition(skc8, W_782), true, skc12, W_782), W_782), W_782), W_782)=W_782))). % 19.81/9.39 tff(c_16086, plain, (![V_950]: (ifeq3(of(skc12, skc11, skc15), true, ifeq3(of(skc12, V_950, skc15), true, ifeq3(forename(skc12, V_950), true, skc11, V_950), V_950), V_950)=V_950))). % 19.81/9.39 tff(c_16039, plain, (![W_947]: (ifeq3(of(skc12, W_947, skc15), true, ifeq3(of(skc12, skc11, skc15), true, ifeq3(forename(skc12, W_947), true, W_947, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_16111, plain, (ifeq3(of(skc12, skc11, skc15), true, ifeq3(of(skc12, skc11, skc15), true, skc11, skc11), skc11)=skc11)). % 19.81/9.39 tff(c_16040, plain, (![X_948]: (ifeq3(of(skc12, skc11, X_948), true, ifeq3(of(skc12, skc11, X_948), true, ifeq3(entity(skc12, X_948), true, skc11, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_4449, plain, (![X_183, V_184]: (ifeq3(of(skc12, skc11, X_183), true, ifeq3(of(skc12, V_184, X_183), true, ifeq3(forename(skc12, V_184), true, ifeq3(entity(skc12, X_183), true, skc11, V_184), V_184), V_184), V_184)=V_184))). % 19.81/9.39 tff(c_4450, plain, (![W_182, X_183]: (ifeq3(of(skc12, W_182, X_183), true, ifeq3(of(skc12, skc11, X_183), true, ifeq3(forename(skc12, W_182), true, ifeq3(entity(skc12, X_183), true, W_182, skc11), skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_15856, plain, (![V_939]: (ifeq3(of(skc12, skc14, skc10), true, ifeq3(of(skc12, V_939, skc10), true, ifeq3(forename(skc12, V_939), true, skc14, V_939), V_939), V_939)=V_939))). % 19.81/9.39 tff(c_15809, plain, (![W_936]: (ifeq3(of(skc12, W_936, skc10), true, ifeq3(of(skc12, skc14, skc10), true, ifeq3(forename(skc12, W_936), true, W_936, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_13000, plain, (![X_769, Z_771]: (ifeq3(theme(skc8, X_769, skc12), true, ifeq3(agent(skc8, skc13, Z_771), true, ifeq3(agent(skc8, X_769, Z_771), true, ifeq3(think_believe_consider(skc8, X_769), true, skc12, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_15858, plain, (![X_938]: (ifeq3(of(skc12, skc14, X_938), true, ifeq3(of(skc12, skc11, X_938), true, ifeq3(entity(skc12, X_938), true, skc14, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_15811, plain, (![X_937]: (ifeq3(of(skc12, skc11, X_937), true, ifeq3(of(skc12, skc14, X_937), true, ifeq3(entity(skc12, X_937), true, skc11, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_15881, plain, (ifeq3(of(skc12, skc14, skc10), true, ifeq3(of(skc12, skc14, skc10), true, skc14, skc14), skc14)=skc14)). % 19.81/9.39 tff(c_15812, plain, (![X_937]: (ifeq3(of(skc12, skc14, X_937), true, ifeq3(of(skc12, skc14, X_937), true, ifeq3(entity(skc12, X_937), true, skc14, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_3661, plain, (![X_407, V_408]: (ifeq3(of(skc12, skc14, X_407), true, ifeq3(of(skc12, V_408, X_407), true, ifeq3(forename(skc12, V_408), true, ifeq3(entity(skc12, X_407), true, skc14, V_408), V_408), V_408), V_408)=V_408))). % 19.81/9.39 tff(c_3662, plain, (![W_406, X_407]: (ifeq3(of(skc12, W_406, X_407), true, ifeq3(of(skc12, skc14, X_407), true, ifeq3(forename(skc12, W_406), true, ifeq3(entity(skc12, X_407), true, W_406, skc14), skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_13409, plain, (![X_794, V_795]: (ifeq3(theme(skc8, X_794, V_795), true, ifeq3(agent(skc8, X_794, skc15), true, ifeq3(think_believe_consider(skc8, X_794), true, ifeq3(proposition(skc8, V_795), true, V_795, skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_15715, plain, (![Y_931]: (ifeq3(theme(skc8, Y_931, skc12), true, ifeq3(agent(skc8, Y_931, skc15), true, ifeq3(think_believe_consider(skc8, Y_931), true, skc12, skc12), skc12), skc12)=skc12))). % 19.81/9.39 tff(c_13205, plain, (![Y_781, W_782]: (ifeq3(theme(skc8, Y_781, W_782), true, ifeq3(agent(skc8, Y_781, skc15), true, ifeq3(think_believe_consider(skc8, Y_781), true, ifeq3(proposition(skc8, W_782), true, skc12, W_782), W_782), W_782), W_782)=W_782))). % 19.81/9.39 tff(c_12663, plain, (![V_750]: (ifeq3(of(skc8, skc11, skc15), true, ifeq3(of(skc8, V_750, skc15), true, ifeq3(forename(skc8, V_750), true, skc11, V_750), V_750), V_750)=V_750))). % 19.81/9.39 tff(c_12302, plain, (![V_730]: (ifeq3(of(skc8, skc14, skc10), true, ifeq3(of(skc8, V_730, skc10), true, ifeq3(forename(skc8, V_730), true, skc14, V_730), V_730), V_730)=V_730))). % 19.81/9.39 tff(c_12845, plain, (![W_759]: (ifeq3(of(skc8, W_759, skc10), true, ifeq3(of(skc8, skc14, skc10), true, ifeq3(forename(skc8, W_759), true, W_759, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_12460, plain, (![W_739]: (ifeq3(of(skc8, W_739, skc15), true, ifeq3(of(skc8, skc11, skc15), true, ifeq3(forename(skc8, W_739), true, W_739, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_13408, plain, (![W_793, V_795]: (ifeq3(theme(skc8, skc13, W_793), true, ifeq3(theme(skc8, skc13, V_795), true, ifeq3(proposition(skc8, W_793), true, ifeq3(proposition(skc8, V_795), true, V_795, W_793), W_793), W_793), W_793)=W_793))). % 19.81/9.39 tff(c_15555, plain, (ifeq3(of(skc8, skc14, skc10), true, ifeq3(of(skc8, skc14, skc10), true, skc14, skc14), skc14)=skc14)). % 19.81/9.39 tff(c_12849, plain, (![X_760]: (ifeq3(of(skc8, skc14, X_760), true, ifeq3(of(skc8, skc14, X_760), true, ifeq3(entity(skc8, X_760), true, skc14, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_15118, plain, (ifeq3(of(skc8, skc11, skc15), true, ifeq3(of(skc8, skc11, skc15), true, skc11, skc11), skc11)=skc11)). % 19.81/9.39 tff(c_7801, plain, (![U_168]: (ifeq2(agent(U_168, skf1(skc15), skc15), true, ifeq2(accessible_world(U_168, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_7963, plain, (![U_168]: (ifeq2(agent(U_168, skf1(skc10), skc10), true, ifeq2(accessible_world(U_168, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_15463, plain, (![V_920]: (ifeq2(accessible_world(skc12, V_920), true, agent(V_920, skf1(skc10), skc10), true)=true))). % 19.81/9.39 tff(c_15405, plain, (![V_917]: (ifeq2(accessible_world(skc12, V_917), true, agent(V_917, skf1(skc15), skc15), true)=true))). % 19.81/9.39 tff(c_12307, plain, (![X_729]: (ifeq3(of(skc8, skc14, X_729), true, ifeq3(of(skc8, skc11, X_729), true, ifeq3(entity(skc8, X_729), true, skc14, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_15362, plain, (![V_915]: (ifeq2(accessible_world(skc12, V_915), true, be(V_915, skc9, skc10, skc10), true)=true))). % 19.81/9.39 tff(c_8534, plain, (![U_177]: (ifeq2(be(U_177, skc9, skc10, skc10), true, ifeq2(accessible_world(U_177, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_6909, plain, (![U_83, V_467]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skf1(V_467)), true, true, true), true)=true))). % 19.81/9.39 tff(c_6680, plain, (![U_89, V_455]: (ifeq2(accessible_world(U_89, skc12), true, ifeq2(nonexistent(U_89, skf1(V_455)), true, true, true), true)=true))). % 19.81/9.39 tff(c_6781, plain, (![U_92, V_460]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skf1(V_460)), true, true, true), true)=true))). % 19.81/9.39 tff(c_6720, plain, (![U_86, V_457]: (ifeq2(accessible_world(U_86, skc12), true, ifeq2(specific(U_86, skf1(V_457)), true, true, true), true)=true))). % 19.81/9.39 tff(c_15252, plain, (ifeq3(of(skc12, skc14, skc10), true, skc11, skc14)=skc14)). % 19.81/9.39 tff(c_6316, plain, (![V_184]: (ifeq3(of(skc12, V_184, skc10), true, ifeq3(forename(skc12, V_184), true, skc11, V_184), V_184)=V_184))). % 19.81/9.39 tff(c_15216, plain, (ifeq3(of(skc12, skc11, skc15), true, skc14, skc11)=skc11)). % 19.81/9.39 tff(c_6281, plain, (![V_184]: (ifeq3(of(skc12, V_184, skc15), true, ifeq3(forename(skc12, V_184), true, skc14, V_184), V_184)=V_184))). % 19.81/9.39 tff(c_15163, plain, (ifeq3(of(skc12, skc14, skc10), true, skc14, skc11)=skc11)). % 19.81/9.39 tff(c_6821, plain, (![U_80, V_462]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skf1(V_462)), true, true, true), true)=true))). % 19.81/9.39 tff(c_6317, plain, (![W_182]: (ifeq3(of(skc12, W_182, skc10), true, ifeq3(forename(skc12, W_182), true, W_182, skc11), skc11)=skc11))). % 19.81/9.39 tff(c_15139, plain, (ifeq3(of(skc12, skc11, skc15), true, skc11, skc14)=skc14)). % 19.81/9.39 tff(c_6282, plain, (![W_182]: (ifeq3(of(skc12, W_182, skc15), true, ifeq3(forename(skc12, W_182), true, W_182, skc14), skc14)=skc14))). % 19.81/9.39 tff(c_12669, plain, (![X_749]: (ifeq3(of(skc8, skc11, X_749), true, ifeq3(of(skc8, skc11, X_749), true, ifeq3(entity(skc8, X_749), true, skc11, skc11), skc11), skc11)=skc11))). % 19.81/9.39 tff(c_6630, plain, (![U_77, V_453]: (ifeq2(accessible_world(U_77, skc12), true, ifeq2(eventuality(U_77, skf1(V_453)), true, true, true), true)=true))). % 19.81/9.39 tff(c_3668, plain, (![W_406]: (ifeq3(of(skc8, W_406, skc10), true, ifeq3(forename(skc8, W_406), true, W_406, skc11), skc11)=skc11))). % 19.81/9.39 tff(c_12850, plain, (![X_760]: (ifeq3(of(skc8, skc11, X_760), true, ifeq3(of(skc8, skc14, X_760), true, ifeq3(entity(skc8, X_760), true, skc11, skc14), skc14), skc14)=skc14))). % 19.81/9.39 tff(c_6541, plain, (![U_95, V_448]: (ifeq2(accessible_world(U_95, skc12), true, ifeq2(event(U_95, skf1(V_448)), true, true, true), true)=true))). % 19.81/9.39 tff(c_14971, plain, (![V_889, V_890]: (ifeq2(accessible_world(skc12, V_889), true, present(V_889, skf1(V_890)), true)=true))). % 19.81/9.39 tff(c_6443, plain, (![U_149, V_442]: (ifeq2(accessible_world(U_149, skc12), true, ifeq2(smoke(U_149, skf1(V_442)), true, true, true), true)=true))). % 19.81/9.39 tff(c_3665, plain, (![V_408]: (ifeq3(of(skc8, V_408, skc15), true, ifeq3(forename(skc8, V_408), true, skc14, V_408), V_408)=V_408))). % 19.81/9.39 tff(c_3667, plain, (![V_408]: (ifeq3(of(skc8, V_408, skc10), true, ifeq3(forename(skc8, V_408), true, skc11, V_408), V_408)=V_408))). % 19.81/9.39 tff(c_12847, plain, (![W_759]: (ifeq3(of(skc8, W_759, skc15), true, ifeq3(forename(skc8, W_759), true, W_759, skc14), skc14)=skc14))). % 19.81/9.39 tff(c_6510, plain, (![U_152, V_446]: (ifeq2(present(U_152, skf1(V_446)), true, ifeq2(accessible_world(U_152, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_6277, plain, (![U_164]: (ifeq2(of(U_164, skc14, skc15), true, ifeq2(accessible_world(U_164, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_14795, plain, (![V_879]: (ifeq2(accessible_world(skc12, V_879), true, of(V_879, skc11, skc10), true)=true))). % 19.81/9.39 tff(c_6312, plain, (![U_164]: (ifeq2(of(U_164, skc11, skc10), true, ifeq2(accessible_world(U_164, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_14729, plain, (![V_876]: (ifeq2(accessible_world(skc12, V_876), true, agent(V_876, skc13, skc15), true)=true))). % 19.81/9.39 tff(c_12997, plain, (![Z_771]: (ifeq3(agent(skc8, skc13, Z_771), true, ifeq3(agent(skc8, skc13, Z_771), true, skc12, skc12), skc12)=skc12))). % 19.81/9.39 tff(c_6347, plain, (![U_168]: (ifeq2(agent(U_168, skc13, skc15), true, ifeq2(accessible_world(U_168, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_14648, plain, (![V_872]: (ifeq2(accessible_world(skc12, V_872), true, theme(V_872, skc13, skc12), true)=true))). % 19.81/9.39 tff(c_6411, plain, (![U_172]: (ifeq2(theme(U_172, skc13, skc12), true, ifeq2(accessible_world(U_172, skc12), true, true, true), true)=true))). % 19.81/9.39 tff(c_14582, plain, (![V_869]: (ifeq2(accessible_world(skc12, V_869), true, of(V_869, skc14, skc15), true)=true))). % 19.81/9.39 tff(c_13204, plain, (![W_782]: (ifeq3(theme(skc8, skc13, W_782), true, ifeq3(proposition(skc8, W_782), true, skc12, W_782), W_782)=W_782))). % 19.81/9.39 tff(c_13588, plain, (![V_807]: (ifeq3(theme(skc8, skc13, V_807), true, ifeq3(proposition(skc8, V_807), true, V_807, skc12), skc12)=skc12))). % 19.81/9.39 tff(c_6225, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc15), true, true, true), true)=true))). % 19.81/9.39 tff(c_3501, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc14), true, true, true), true)=true))). % 19.81/9.39 tff(c_6196, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc10), true, true, true), true)=true))). % 19.81/9.39 tff(c_3447, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc12), true, ifeq2(general(U_143, skc14), true, true, true), true)=true))). % 19.81/9.39 tff(c_3413, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skc14), true, true, true), true)=true))). % 19.81/9.39 tff(c_6086, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_5948, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3778, plain, (![Y_411, W_410, X_414, Z_413]: (ifeq3(theme(skc8, Y_411, W_410), true, ifeq3(theme(skc8, X_414, skc12), true, ifeq3(agent(skc8, Y_411, Z_413), true, ifeq3(agent(skc8, X_414, Z_413), true, ifeq3(think_believe_consider(skc8, Y_411), true, ifeq3(think_believe_consider(skc8, X_414), true, ifeq3(proposition(skc8, W_410), true, skc12, W_410), W_410), W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_6023, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5917, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc12), true, ifeq2(existent(U_110, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5889, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_3365, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc12), true, ifeq2(nonhuman(U_140, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_6116, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc12), true, ifeq2(existent(U_110, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3304, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_3169, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_3175, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_3187, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_3779, plain, (![W_410, X_414, V_409, Z_413]: (ifeq3(theme(skc8, skc13, W_410), true, ifeq3(theme(skc8, X_414, V_409), true, ifeq3(agent(skc8, skc13, Z_413), true, ifeq3(agent(skc8, X_414, Z_413), true, ifeq3(think_believe_consider(skc8, X_414), true, ifeq3(proposition(skc8, W_410), true, ifeq3(proposition(skc8, V_409), true, V_409, W_410), W_410), W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_3181, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_5260, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc12), true, ifeq2(nonhuman(U_140, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_5016, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc12), true, ifeq2(living(U_116, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_5767, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc12), true, ifeq2(specific(U_86, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_5621, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc12), true, ifeq2(impartial(U_113, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_5792, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc12), true, ifeq2(specific(U_86, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5827, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc12), true, ifeq2(impartial(U_113, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5555, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc12), true, ifeq2(living(U_116, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5127, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc12), true, ifeq2(entity(U_107, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3780, plain, (![Y_411, W_410, V_409, Z_413]: (ifeq3(theme(skc8, Y_411, W_410), true, ifeq3(theme(skc8, skc13, V_409), true, ifeq3(agent(skc8, Y_411, Z_413), true, ifeq3(agent(skc8, skc13, Z_413), true, ifeq3(think_believe_consider(skc8, Y_411), true, ifeq3(proposition(skc8, W_410), true, ifeq3(proposition(skc8, V_409), true, V_409, W_410), W_410), W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_5700, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc12), true, ifeq2(entity(U_107, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_5219, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_3236, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc12), true, ifeq2(abstraction(U_137, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_5583, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_5450, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_5189, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc12), true, ifeq2(general(U_143, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_5493, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_5669, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_5394, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc12), true, ifeq2(nonhuman(U_140, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_3777, plain, (![Y_411, X_414, V_409, Z_413]: (ifeq3(theme(skc8, Y_411, skc12), true, ifeq3(theme(skc8, X_414, V_409), true, ifeq3(agent(skc8, Y_411, Z_413), true, ifeq3(agent(skc8, X_414, Z_413), true, ifeq3(think_believe_consider(skc8, Y_411), true, ifeq3(think_believe_consider(skc8, X_414), true, ifeq3(proposition(skc8, V_409), true, V_409, skc12), skc12), skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.40 tff(c_5093, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc12), true, ifeq2(general(U_143, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_5065, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc12), true, ifeq2(singleton(U_83, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_2457, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc8), true, ifeq2(unisex(U_92, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_2970, plain, (![U_367]: (ifeq2(accessible_world(U_367, skc8), true, ifeq2(general(U_367, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_2207, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(nonhuman(U_324, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_2976, plain, (![U_367]: (ifeq2(accessible_world(U_367, skc8), true, ifeq2(general(U_367, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_2761, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc8), true, ifeq2(specific(U_351, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_2767, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc8), true, ifeq2(specific(U_351, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_2112, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc8), true, ifeq2(unisex(U_92, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_3776, plain, (![Y_411, W_410, V_409]: (ifeq3(theme(skc8, Y_411, W_410), true, ifeq3(theme(skc8, skc13, V_409), true, ifeq3(agent(skc8, Y_411, skc15), true, ifeq3(think_believe_consider(skc8, Y_411), true, ifeq3(proposition(skc8, W_410), true, ifeq3(proposition(skc8, V_409), true, V_409, W_410), W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_2632, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc8), true, ifeq2(existent(U_110, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_2516, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_2528, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_2510, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_2522, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3205, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_2442, plain, (![U_336]: (ifeq2(accessible_world(U_336, skc8), true, ifeq2(existent(U_336, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_2577, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc8), true, ifeq2(nonhuman(U_140, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_4907, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc12), true, ifeq2(human(U_119, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3775, plain, (![W_410, X_414, V_409]: (ifeq3(theme(skc8, skc13, W_410), true, ifeq3(theme(skc8, X_414, V_409), true, ifeq3(agent(skc8, X_414, skc15), true, ifeq3(think_believe_consider(skc8, X_414), true, ifeq3(proposition(skc8, W_410), true, ifeq3(proposition(skc8, V_409), true, V_409, W_410), W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_4736, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc12), true, ifeq2(abstraction(U_137, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_4492, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_3955, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc12), true, ifeq2(thing(U_80, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_4776, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc12), true, ifeq2(animate(U_122, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_4533, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_5349, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc12), true, ifeq2(abstraction(U_137, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_4804, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc12), true, ifeq2(specific(U_86, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_4685, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc12), true, ifeq2(unisex(U_92, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_4879, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc12), true, ifeq2(animate(U_122, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_3774, plain, (![Y_411, W_410, Z_413]: (ifeq3(theme(skc8, Y_411, W_410), true, ifeq3(agent(skc8, Y_411, Z_413), true, ifeq3(agent(skc8, skc13, Z_413), true, ifeq3(think_believe_consider(skc8, Y_411), true, ifeq3(proposition(skc8, W_410), true, skc12, W_410), W_410), W_410), W_410), W_410)=W_410))). % 19.81/9.40 tff(c_4985, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc12), true, ifeq2(human(U_119, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_3845, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc12), true, ifeq2(nonexistent(U_89, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_3143, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc12), true, ifeq2(relation(U_134, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_4567, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc12), true, ifeq2(nonexistent(U_89, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_3886, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc12), true, ifeq2(specific(U_86, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_4848, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc12), true, ifeq2(relname(U_131, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_4948, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc12), true, ifeq2(organism(U_104, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_4238, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc12), true, ifeq2(organism(U_104, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_3199, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_3773, plain, (![X_414, V_409, Z_413]: (ifeq3(theme(skc8, X_414, V_409), true, ifeq3(agent(skc8, skc13, Z_413), true, ifeq3(agent(skc8, X_414, Z_413), true, ifeq3(think_believe_consider(skc8, X_414), true, ifeq3(proposition(skc8, V_409), true, V_409, skc12), skc12), skc12), skc12), skc12)=skc12))). % 19.81/9.40 tff(c_2663, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc8), true, ifeq2(living(U_345, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_2546, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_2158, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc8), true, ifeq2(abstraction(U_321, skc11), true, true, true), true)=true))). % 19.81/9.40 tff(c_3090, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc8), true, ifeq2(impartial(U_374, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_2394, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc8), true, ifeq2(entity(U_333, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_1753, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc8), true, ifeq2(unisex(U_300, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_3096, plain, (![U_374]: (ifeq2(accessible_world(U_374, skc8), true, ifeq2(impartial(U_374, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_2152, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc8), true, ifeq2(abstraction(U_321, skc14), true, true, true), true)=true))). % 19.81/9.40 tff(c_12848, plain, (ifeq3(of(skc8, skc14, skc10), true, skc11, skc14)=skc14)). % 19.81/9.40 tff(c_3670, plain, (![W_406, X_407]: (ifeq3(of(skc8, W_406, X_407), true, ifeq3(of(skc8, skc14, X_407), true, ifeq3(forename(skc8, W_406), true, ifeq3(entity(skc8, X_407), true, W_406, skc14), skc14), skc14), skc14)=skc14))). % 19.81/9.40 tff(c_2669, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc8), true, ifeq2(living(U_345, skc15), true, true, true), true)=true))). % 19.81/9.40 tff(c_2213, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc8), true, ifeq2(nonhuman(U_324, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_2982, plain, (![U_367]: (ifeq2(accessible_world(U_367, skc8), true, ifeq2(general(U_367, skc12), true, true, true), true)=true))). % 19.81/9.40 tff(c_3193, plain, (![U_377]: (ifeq2(accessible_world(U_377, skc8), true, ifeq2(singleton(U_377, skc13), true, true, true), true)=true))). % 19.81/9.40 tff(c_2400, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc8), true, ifeq2(entity(U_333, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_4090, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc12), true, ifeq2(male(U_125, skc10), true, true, true), true)=true))). % 19.81/9.40 tff(c_3725, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc12), true, ifeq2(event(U_95, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_3800, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc12), true, ifeq2(eventuality(U_77, skc9), true, true, true), true)=true))). % 19.81/9.40 tff(c_12665, plain, (ifeq3(of(skc8, skc11, skc15), true, skc11, skc14)=skc14)). % 19.81/9.40 tff(c_3671, plain, (![X_407, V_408]: (ifeq3(of(skc8, skc11, X_407), true, ifeq3(of(skc8, V_408, X_407), true, ifeq3(forename(skc8, V_408), true, ifeq3(entity(skc8, X_407), true, skc11, V_408), V_408), V_408), V_408)=V_408))). % 19.81/9.40 tff(c_5315, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc12), true, ifeq2(relation(U_134, skc11), true, true, true), true)=true))). % 19.81/9.41 tff(c_4318, plain, (![U_101]: (ifeq2(accessible_world(U_101, skc12), true, ifeq2(human_person(U_101, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_4053, plain, (![U_101]: (ifeq2(accessible_world(U_101, skc12), true, ifeq2(human_person(U_101, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_4437, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc12), true, ifeq2(forename(U_128, skc11), true, true, true), true)=true))). % 19.81/9.41 tff(c_4651, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc12), true, ifeq2(relation(U_134, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_4180, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc12), true, ifeq2(eventuality(U_77, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_3112, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc12), true, ifeq2(relname(U_131, skc14), true, true, true), true)=true))). % 19.81/9.41 tff(c_4369, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc12), true, ifeq2(male(U_125, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_12462, plain, (ifeq3(of(skc8, skc11, skc15), true, skc14, skc11)=skc11)). % 19.81/9.41 tff(c_3672, plain, (![W_406, X_407]: (ifeq3(of(skc8, W_406, X_407), true, ifeq3(of(skc8, skc11, X_407), true, ifeq3(forename(skc8, W_406), true, ifeq3(entity(skc8, X_407), true, W_406, skc11), skc11), skc11), skc11)=skc11))). % 19.81/9.41 tff(c_2281, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc8), true, ifeq2(nonexistent(U_327, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_2534, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_2708, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc8), true, ifeq2(organism(U_348, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_2714, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc8), true, ifeq2(organism(U_348, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_1904, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc8), true, ifeq2(relation(U_309, skc14), true, true, true), true)=true))). % 19.81/9.41 tff(c_1741, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc8), true, ifeq2(unisex(U_300, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_2779, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc8), true, ifeq2(specific(U_351, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_1910, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc8), true, ifeq2(relation(U_309, skc11), true, true, true), true)=true))). % 19.81/9.41 tff(c_12305, plain, (ifeq3(of(skc8, skc14, skc10), true, skc14, skc11)=skc11)). % 19.81/9.41 tff(c_3669, plain, (![X_407, V_408]: (ifeq3(of(skc8, skc14, X_407), true, ifeq3(of(skc8, V_408, X_407), true, ifeq3(forename(skc8, V_408), true, ifeq3(entity(skc8, X_407), true, skc14, V_408), V_408), V_408), V_408)=V_408))). % 19.81/9.41 tff(c_3268, plain, (![U_380]: (ifeq2(accessible_world(U_380, skc8), true, ifeq2(animate(U_380, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_2164, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc8), true, ifeq2(abstraction(U_321, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_1747, plain, (![U_300]: (ifeq2(accessible_world(U_300, skc8), true, ifeq2(unisex(U_300, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_3274, plain, (![U_380]: (ifeq2(accessible_world(U_380, skc8), true, ifeq2(animate(U_380, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_2335, plain, (![U_330]: (ifeq2(accessible_world(U_330, skc8), true, ifeq2(human(U_330, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_2275, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc8), true, ifeq2(nonexistent(U_327, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_2329, plain, (![U_330]: (ifeq2(accessible_world(U_330, skc8), true, ifeq2(human(U_330, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_2773, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc8), true, ifeq2(specific(U_351, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_2540, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc8), true, ifeq2(thing(U_339, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_3571, plain, (![U_402]: (ifeq2(be(U_402, skc9, skc10, skc10), true, ifeq2(accessible_world(U_402, skc8), true, true, true), true)=true))). % 19.81/9.41 tff(c_3029, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc12), true, ifeq2(forename(U_128, skc14), true, true, true), true)=true))). % 19.81/9.41 tff(c_2954, plain, (![U_152]: (ifeq2(present(U_152, skc13), true, ifeq2(accessible_world(U_152, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_3929, plain, (![U_155]: (ifeq2(think_believe_consider(U_155, skc13), true, ifeq2(accessible_world(U_155, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_3591, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc12), true, ifeq2(vincent_forename(U_161, skc14), true, true, true), true)=true))). % 19.81/9.41 tff(c_4403, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc12), true, ifeq2(jules_forename(U_146, skc11), true, true, true), true)=true))). % 19.81/9.41 tff(c_4278, plain, (![U_98]: (ifeq2(accessible_world(U_98, skc12), true, ifeq2(man(U_98, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_4138, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc12), true, ifeq2(event(U_95, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_11921, plain, (![V_710]: (ifeq2(accessible_world(skc8, V_710), true, be(V_710, skc9, skc10, skc10), true)=true))). % 19.81/9.41 tff(c_3694, plain, (![U_74]: (ifeq2(accessible_world(U_74, skc12), true, ifeq2(state(U_74, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_11859, plain, (![V_707]: (ifeq2(accessible_world(skc12, V_707), true, think_believe_consider(V_707, skc13), true)=true))). % 19.81/9.41 tff(c_4013, plain, (![U_98]: (ifeq2(accessible_world(U_98, skc12), true, ifeq2(man(U_98, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_4621, plain, (![U_158]: (ifeq2(accessible_world(U_158, skc12), true, ifeq2(proposition(U_158, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_11773, plain, (![V_703]: (ifeq2(accessible_world(skc12, V_703), true, present(V_703, skc13), true)=true))). % 19.81/9.41 tff(c_3521, plain, (![U_394]: (ifeq2(agent(U_394, skc13, skc15), true, ifeq2(accessible_world(U_394, skc8), true, true, true), true)=true))). % 19.81/9.41 tff(c_2885, plain, (![U_360]: (ifeq2(accessible_world(U_360, skc8), true, ifeq2(male(U_360, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_2891, plain, (![U_360]: (ifeq2(accessible_world(U_360, skc8), true, ifeq2(male(U_360, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_2029, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc8), true, ifeq2(event(U_315, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_1916, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc8), true, ifeq2(relation(U_309, skc12), true, true, true), true)=true))). % 19.81/9.41 tff(c_1647, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc8), true, ifeq2(relname(U_294, skc14), true, true, true), true)=true))). % 19.81/9.41 tff(c_1641, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc8), true, ifeq2(relname(U_294, skc11), true, true, true), true)=true))). % 19.81/9.41 tff(c_1795, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc8), true, ifeq2(eventuality(U_303, skc13), true, true, true), true)=true))). % 19.81/9.41 tff(c_3349, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc8), true, ifeq2(human_person(U_383, skc15), true, true, true), true)=true))). % 19.81/9.41 tff(c_1801, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc8), true, ifeq2(eventuality(U_303, skc9), true, true, true), true)=true))). % 19.81/9.41 tff(c_3476, plain, (![U_390]: (ifeq2(of(U_390, skc11, skc10), true, ifeq2(accessible_world(U_390, skc8), true, true, true), true)=true))). % 19.81/9.41 tff(c_3343, plain, (![U_383]: (ifeq2(accessible_world(U_383, skc8), true, ifeq2(human_person(U_383, skc10), true, true, true), true)=true))). % 19.81/9.41 tff(c_6683, plain, (![V_455]: (ifeq(tuple(true, existent(skc12, skf1(V_455))), tuple(true, true), a, b)=b))). % 19.81/9.41 tff(c_11514, plain, (![V_688]: (ifeq2(accessible_world(skc8, V_688), true, of(V_688, skc14, skc15), true)=true))). % 19.81/9.41 tff(c_6784, plain, (![V_460]: (ifeq(tuple(true, male(skc12, skf1(V_460))), tuple(true, true), a, b)=b))). % 19.81/9.41 tff(c_6723, plain, (![V_457]: (ifeq(tuple(true, general(skc12, skf1(V_457))), tuple(true, true), a, b)=b))). % 19.81/9.41 tff(c_3450, plain, (ifeq(tuple(specific(skc12, skc14), true), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_6119, plain, (ifeq(tuple(nonexistent(skc12, skc15), true), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_11438, plain, (![V_684]: (ifeq2(accessible_world(skc8, V_684), true, of(V_684, skc11, skc10), true)=true))). % 19.81/9.41 tff(c_5920, plain, (ifeq(tuple(nonexistent(skc12, skc10), true), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_3368, plain, (ifeq(tuple(human(skc12, skc14), true), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_3416, plain, (ifeq(tuple(true, male(skc12, skc14)), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_5192, plain, (ifeq(tuple(specific(skc12, skc11), true), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_5586, plain, (ifeq(tuple(true, male(skc12, skc12)), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_5770, plain, (ifeq(tuple(true, general(skc12, skc15)), tuple(true, true), a, b)=b)). % 19.81/9.41 tff(c_5096, plain, (ifeq(tuple(specific(skc12, skc12), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_5795, plain, (ifeq(tuple(true, general(skc12, skc10)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_5263, plain, (ifeq(tuple(human(skc12, skc12), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_3398, plain, (![U_386]: (ifeq2(theme(U_386, skc13, skc12), true, ifeq2(accessible_world(U_386, skc8), true, true, true), true)=true))). % 20.08/9.41 tff(c_5397, plain, (ifeq(tuple(human(skc12, skc11), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_5453, plain, (ifeq(tuple(true, male(skc12, skc11)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2178, plain, (ifeq(tuple(human(skc8, skc11), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2460, plain, (ifeq(tuple(true, male(skc8, skc11)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2488, plain, (ifeq(tuple(true, general(skc8, skc15)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2257, plain, (ifeq(tuple(specific(skc8, skc11), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2580, plain, (ifeq(tuple(human(skc8, skc14), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_11300, plain, (![V_681]: (ifeq2(accessible_world(skc8, V_681), true, theme(V_681, skc13, skc12), true)=true))). % 20.08/9.41 tff(c_2413, plain, (ifeq(tuple(nonexistent(skc8, skc15), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2115, plain, (ifeq(tuple(true, male(skc8, skc14)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2058, plain, (ifeq(tuple(true, general(skc8, skc10)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2635, plain, (ifeq(tuple(nonexistent(skc8, skc10), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_2010, plain, (ifeq(tuple(specific(skc8, skc14), true), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_3889, plain, (ifeq(tuple(true, general(skc12, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_4988, plain, (ifeq(tuple(true, nonhuman(skc12, skc10)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_3848, plain, (ifeq(tuple(true, existent(skc12, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_6916, plain, (![V_84, V_467]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skf1(V_467)), true)=true))). % 20.08/9.41 tff(c_3470, plain, (![U_390]: (ifeq2(of(U_390, skc14, skc15), true, ifeq2(accessible_world(U_390, skc8), true, true, true), true)=true))). % 20.08/9.41 tff(c_6690, plain, (![V_90, V_455]: (ifeq2(accessible_world(skc12, V_90), true, nonexistent(V_90, skf1(V_455)), true)=true))). % 20.08/9.41 tff(c_6733, plain, (![V_87, V_457]: (ifeq2(accessible_world(skc12, V_87), true, specific(V_87, skf1(V_457)), true)=true))). % 20.08/9.41 tff(c_6794, plain, (![V_93, V_460]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skf1(V_460)), true)=true))). % 20.08/9.41 tff(c_6837, plain, (![V_81, V_462]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skf1(V_462)), true)=true))). % 20.08/9.41 tff(c_6652, plain, (![V_78, V_453]: (ifeq2(accessible_world(skc12, V_78), true, eventuality(V_78, skf1(V_453)), true)=true))). % 20.08/9.41 tff(c_4910, plain, (ifeq(tuple(true, nonhuman(skc12, skc15)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_6554, plain, (![V_96, V_448]: (ifeq2(accessible_world(skc12, V_96), true, event(V_96, skf1(V_448)), true)=true))). % 20.08/9.41 tff(c_11113, plain, (![V_664]: (ifeq2(accessible_world(skc8, V_664), true, agent(V_664, skc13, skc15), true)=true))). % 20.08/9.41 tff(c_6450, plain, (![V_150, V_442]: (ifeq2(accessible_world(skc12, V_150), true, smoke(V_150, skf1(V_442)), true)=true))). % 20.08/9.41 tff(c_6202, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc10), true)=true))). % 20.08/9.41 tff(c_3507, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc14), true)=true))). % 20.08/9.41 tff(c_6231, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc15), true)=true))). % 20.08/9.41 tff(c_3425, plain, (![V_93]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skc14), true)=true))). % 20.08/9.41 tff(c_4688, plain, (ifeq(tuple(true, male(skc12, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.41 tff(c_3456, plain, (![V_144]: (ifeq2(accessible_world(skc12, V_144), true, general(V_144, skc14), true)=true))). % 20.08/9.42 tff(c_10964, plain, (![W_655]: (ifeq2(existent(skc8, W_655), true, existent(skc12, W_655), true)=true))). % 20.08/9.42 tff(c_3319, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc14), true)=true))). % 20.08/9.42 tff(c_3374, plain, (![V_141]: (ifeq2(accessible_world(skc12, V_141), true, nonhuman(V_141, skc14), true)=true))). % 20.08/9.42 tff(c_5963, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc15), true)=true))). % 20.08/9.42 tff(c_6038, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc10), true)=true))). % 20.08/9.42 tff(c_5895, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc11), true)=true))). % 20.08/9.42 tff(c_4570, plain, (ifeq(tuple(true, existent(skc12, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_6092, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc12), true)=true))). % 20.08/9.42 tff(c_6125, plain, (![V_111]: (ifeq2(accessible_world(skc12, V_111), true, existent(V_111, skc15), true)=true))). % 20.08/9.42 tff(c_5926, plain, (![V_111]: (ifeq2(accessible_world(skc12, V_111), true, existent(V_111, skc10), true)=true))). % 20.08/9.42 tff(c_2600, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc8), true, ifeq2(man(U_342, skc15), true, true, true), true)=true))). % 20.08/9.42 tff(c_3211, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc11), true)=true))). % 20.08/9.42 tff(c_3212, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc10), true)=true))). % 20.08/9.42 tff(c_3213, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc15), true)=true))). % 20.08/9.42 tff(c_3214, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc14), true)=true))). % 20.08/9.42 tff(c_5627, plain, (![V_114]: (ifeq2(accessible_world(skc12, V_114), true, impartial(V_114, skc15), true)=true))). % 20.08/9.42 tff(c_4536, plain, (ifeq(tuple(true, male(skc12, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_5022, plain, (![V_117]: (ifeq2(accessible_world(skc12, V_117), true, living(V_117, skc15), true)=true))). % 20.08/9.42 tff(c_10651, plain, (![W_638]: (ifeq2(impartial(skc8, W_638), true, impartial(skc12, W_638), true)=true))). % 20.08/9.42 tff(c_5561, plain, (![V_117]: (ifeq2(accessible_world(skc12, V_117), true, living(V_117, skc10), true)=true))). % 20.08/9.42 tff(c_5102, plain, (![V_144]: (ifeq2(accessible_world(skc12, V_144), true, general(V_144, skc12), true)=true))). % 20.08/9.42 tff(c_5199, plain, (![V_144]: (ifeq2(accessible_world(skc12, V_144), true, general(V_144, skc11), true)=true))). % 20.08/9.42 tff(c_5780, plain, (![V_87]: (ifeq2(accessible_world(skc12, V_87), true, specific(V_87, skc15), true)=true))). % 20.08/9.42 tff(c_5462, plain, (![V_93]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skc11), true)=true))). % 20.08/9.42 tff(c_4807, plain, (ifeq(tuple(true, general(skc12, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_5269, plain, (![V_141]: (ifeq2(accessible_world(skc12, V_141), true, nonhuman(V_141, skc12), true)=true))). % 20.08/9.42 tff(c_10498, plain, (![W_630]: (ifeq2(man(skc8, W_630), true, man(skc12, W_630), true)=true))). % 20.08/9.42 tff(c_3254, plain, (![V_138]: (ifeq2(accessible_world(skc12, V_138), true, abstraction(V_138, skc14), true)=true))). % 20.08/9.42 tff(c_5403, plain, (![V_141]: (ifeq2(accessible_world(skc12, V_141), true, nonhuman(V_141, skc11), true)=true))). % 20.08/9.42 tff(c_5595, plain, (![V_93]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skc12), true)=true))). % 20.08/9.42 tff(c_5234, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc12), true)=true))). % 20.08/9.42 tff(c_5508, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc11), true)=true))). % 20.08/9.42 tff(c_1562, plain, (ifeq(tuple(true, male(skc8, skc12)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_5805, plain, (![V_87]: (ifeq2(accessible_world(skc12, V_87), true, specific(V_87, skc10), true)=true))). % 20.08/9.42 tff(c_5675, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc13), true)=true))). % 20.08/9.42 tff(c_5071, plain, (![V_84]: (ifeq2(accessible_world(skc12, V_84), true, singleton(V_84, skc9), true)=true))). % 20.08/9.42 tff(c_2606, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc8), true, ifeq2(man(U_342, skc10), true, true, true), true)=true))). % 20.08/9.42 tff(c_5716, plain, (![V_108]: (ifeq2(accessible_world(skc12, V_108), true, entity(V_108, skc10), true)=true))). % 20.08/9.42 tff(c_5143, plain, (![V_108]: (ifeq2(accessible_world(skc12, V_108), true, entity(V_108, skc15), true)=true))). % 20.08/9.42 tff(c_5833, plain, (![V_114]: (ifeq2(accessible_world(skc12, V_114), true, impartial(V_114, skc10), true)=true))). % 20.08/9.42 tff(c_2554, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc15), true)=true))). % 20.08/9.42 tff(c_2785, plain, (![V_352]: (ifeq2(accessible_world(skc8, V_352), true, specific(V_352, skc15), true)=true))). % 20.08/9.42 tff(c_1459, plain, (ifeq(tuple(human(skc8, skc12), true), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_10234, plain, (![V_454]: (ifeq2(nonexistent(skc8, skf1(V_454)), true, true, true)=true))). % 20.08/9.42 tff(c_10195, plain, (![W_613]: (ifeq2(nonexistent(skc8, W_613), true, nonexistent(skc12, W_613), true)=true))). % 20.08/9.42 tff(c_2555, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc14), true)=true))). % 20.08/9.42 tff(c_2552, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc11), true)=true))). % 20.08/9.42 tff(c_2553, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc10), true)=true))). % 20.08/9.42 tff(c_2586, plain, (![V_141]: (ifeq2(accessible_world(skc8, V_141), true, nonhuman(V_141, skc14), true)=true))). % 20.08/9.42 tff(c_2469, plain, (![V_93]: (ifeq2(accessible_world(skc8, V_93), true, unisex(V_93, skc11), true)=true))). % 20.08/9.42 tff(c_1516, plain, (ifeq(tuple(specific(skc8, skc12), true), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_2786, plain, (![V_352]: (ifeq2(accessible_world(skc8, V_352), true, specific(V_352, skc10), true)=true))). % 20.08/9.42 tff(c_10018, plain, (![W_605]: (ifeq2(male(skc8, W_605), true, male(skc12, W_605), true)=true))). % 20.08/9.42 tff(c_2219, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, nonhuman(V_325, skc11), true)=true))). % 20.08/9.42 tff(c_2641, plain, (![V_111]: (ifeq2(accessible_world(skc8, V_111), true, existent(V_111, skc10), true)=true))). % 20.08/9.42 tff(c_2124, plain, (![V_93]: (ifeq2(accessible_world(skc8, V_93), true, unisex(V_93, skc14), true)=true))). % 20.08/9.42 tff(c_2989, plain, (![V_368]: (ifeq2(accessible_world(skc8, V_368), true, general(V_368, skc14), true)=true))). % 20.08/9.42 tff(c_3217, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc12), true)=true))). % 20.08/9.42 tff(c_4372, plain, (ifeq(tuple(unisex(skc12, skc15), true), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_9862, plain, (![V_459]: (ifeq2(unisex(skc8, skf1(V_459)), true, true, true)=true))). % 20.08/9.42 tff(c_9799, plain, (![W_597]: (ifeq2(unisex(skc8, W_597), true, unisex(skc12, W_597), true)=true))). % 20.08/9.42 tff(c_2988, plain, (![V_368]: (ifeq2(accessible_world(skc8, V_368), true, general(V_368, skc11), true)=true))). % 20.08/9.42 tff(c_2448, plain, (![V_337]: (ifeq2(accessible_world(skc8, V_337), true, existent(V_337, skc15), true)=true))). % 20.08/9.42 tff(c_4545, plain, (![V_93]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skc13), true)=true))). % 20.08/9.42 tff(c_4697, plain, (![V_93]: (ifeq2(accessible_world(skc12, V_93), true, unisex(V_93, skc9), true)=true))). % 20.08/9.42 tff(c_4754, plain, (![V_138]: (ifeq2(accessible_world(skc12, V_138), true, abstraction(V_138, skc12), true)=true))). % 20.08/9.42 tff(c_4093, plain, (ifeq(tuple(unisex(skc12, skc10), true), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_3155, plain, (![V_135]: (ifeq2(accessible_world(skc12, V_135), true, relation(V_135, skc14), true)=true))). % 20.08/9.42 tff(c_4816, plain, (![V_87]: (ifeq2(accessible_world(skc12, V_87), true, specific(V_87, skc13), true)=true))). % 20.08/9.42 tff(c_4857, plain, (![V_132]: (ifeq2(accessible_world(skc12, V_132), true, relname(V_132, skc11), true)=true))). % 20.08/9.42 tff(c_2080, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc8), true, ifeq2(forename(U_318, skc14), true, true, true), true)=true))). % 20.08/9.42 tff(c_3898, plain, (![V_87]: (ifeq2(accessible_world(skc12, V_87), true, specific(V_87, skc9), true)=true))). % 20.08/9.42 tff(c_4916, plain, (![V_120]: (ifeq2(accessible_world(skc12, V_120), true, human(V_120, skc15), true)=true))). % 20.08/9.42 tff(c_4994, plain, (![V_120]: (ifeq2(accessible_world(skc12, V_120), true, human(V_120, skc10), true)=true))). % 20.08/9.42 tff(c_4507, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc13), true)=true))). % 20.08/9.42 tff(c_4963, plain, (![V_105]: (ifeq2(accessible_world(skc12, V_105), true, organism(V_105, skc15), true)=true))). % 20.08/9.42 tff(c_1513, plain, (ifeq(tuple(true, general(skc8, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_4782, plain, (![V_123]: (ifeq2(accessible_world(skc12, V_123), true, animate(V_123, skc10), true)=true))). % 20.08/9.42 tff(c_4576, plain, (![V_90]: (ifeq2(accessible_world(skc12, V_90), true, nonexistent(V_90, skc13), true)=true))). % 20.08/9.42 tff(c_3854, plain, (![V_90]: (ifeq2(accessible_world(skc12, V_90), true, nonexistent(V_90, skc9), true)=true))). % 20.08/9.42 tff(c_2086, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc8), true, ifeq2(forename(U_318, skc11), true, true, true), true)=true))). % 20.08/9.42 tff(c_3970, plain, (![V_81]: (ifeq2(accessible_world(skc12, V_81), true, thing(V_81, skc9), true)=true))). % 20.08/9.42 tff(c_4885, plain, (![V_123]: (ifeq2(accessible_world(skc12, V_123), true, animate(V_123, skc15), true)=true))). % 20.08/9.42 tff(c_4253, plain, (![V_105]: (ifeq2(accessible_world(skc12, V_105), true, organism(V_105, skc10), true)=true))). % 20.08/9.42 tff(c_5367, plain, (![V_138]: (ifeq2(accessible_world(skc12, V_138), true, abstraction(V_138, skc11), true)=true))). % 20.08/9.42 tff(c_2676, plain, (![V_346]: (ifeq2(accessible_world(skc8, V_346), true, living(V_346, skc15), true)=true))). % 20.08/9.42 tff(c_1453, plain, (ifeq(tuple(true, nonhuman(skc8, skc10)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_9357, plain, (![V_461]: (ifeq2(thing(skc8, skf1(V_461)), true, true, true)=true))). % 20.08/9.42 tff(c_9278, plain, (![W_571]: (ifeq2(thing(skc8, W_571), true, thing(skc12, W_571), true)=true))). % 20.08/9.42 tff(c_2220, plain, (![V_325]: (ifeq2(accessible_world(skc8, V_325), true, nonhuman(V_325, skc12), true)=true))). % 20.08/9.42 tff(c_2675, plain, (![V_346]: (ifeq2(accessible_world(skc8, V_346), true, living(V_346, skc10), true)=true))). % 20.08/9.42 tff(c_2990, plain, (![V_368]: (ifeq2(accessible_world(skc8, V_368), true, general(V_368, skc12), true)=true))). % 20.08/9.42 tff(c_1761, plain, (![V_301]: (ifeq2(accessible_world(skc8, V_301), true, unisex(V_301, skc12), true)=true))). % 20.08/9.42 tff(c_3102, plain, (![V_375]: (ifeq2(accessible_world(skc8, V_375), true, impartial(V_375, skc10), true)=true))). % 20.08/9.42 tff(c_1456, plain, (ifeq(tuple(true, nonhuman(skc8, skc15)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_9146, plain, (![V_447]: (ifeq2(event(skc8, skf1(V_447)), true, true, true)=true))). % 20.08/9.42 tff(c_9107, plain, (![W_563]: (ifeq2(event(skc8, W_563), true, event(skc12, W_563), true)=true))). % 20.08/9.42 tff(c_2171, plain, (![V_322]: (ifeq2(accessible_world(skc8, V_322), true, abstraction(V_322, skc11), true)=true))). % 20.08/9.42 tff(c_2407, plain, (![V_334]: (ifeq2(accessible_world(skc8, V_334), true, entity(V_334, skc10), true)=true))). % 20.08/9.42 tff(c_2170, plain, (![V_322]: (ifeq2(accessible_world(skc8, V_322), true, abstraction(V_322, skc14), true)=true))). % 20.08/9.42 tff(c_3103, plain, (![V_375]: (ifeq2(accessible_world(skc8, V_375), true, impartial(V_375, skc15), true)=true))). % 20.08/9.42 tff(c_2406, plain, (![V_334]: (ifeq2(accessible_world(skc8, V_334), true, entity(V_334, skc15), true)=true))). % 20.08/9.42 tff(c_1559, plain, (ifeq(tuple(true, male(skc8, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_2558, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc12), true)=true))). % 20.08/9.42 tff(c_8930, plain, (![W_555]: (ifeq2(entity(skc8, W_555), true, entity(skc12, W_555), true)=true))). % 20.08/9.42 tff(c_3215, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc13), true)=true))). % 20.08/9.42 tff(c_3216, plain, (![V_378]: (ifeq2(accessible_world(skc8, V_378), true, singleton(V_378, skc9), true)=true))). % 20.08/9.42 tff(c_5328, plain, (![V_135]: (ifeq2(accessible_world(skc12, V_135), true, relation(V_135, skc11), true)=true))). % 20.08/9.42 tff(c_3737, plain, (![V_96]: (ifeq2(accessible_world(skc12, V_96), true, event(V_96, skc9), true)=true))). % 20.08/9.42 tff(c_3821, plain, (![V_78]: (ifeq2(accessible_world(skc12, V_78), true, eventuality(V_78, skc9), true)=true))). % 20.08/9.42 tff(c_1556, plain, (ifeq(tuple(true, male(skc8, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_4099, plain, (![V_126]: (ifeq2(accessible_world(skc12, V_126), true, male(V_126, skc10), true)=true))). % 20.08/9.42 tff(c_8769, plain, (![W_547]: (ifeq2(animate(skc8, W_547), true, animate(skc12, W_547), true)=true))). % 20.08/9.42 tff(c_4333, plain, (![V_102]: (ifeq2(accessible_world(skc12, V_102), true, human_person(V_102, skc15), true)=true))). % 20.08/9.42 tff(c_7951, plain, (ifeq2(agent(skc8, skf1(skc10), skc10), true, true, true)=true)). % 20.08/9.42 tff(c_4068, plain, (![V_102]: (ifeq2(accessible_world(skc12, V_102), true, human_person(V_102, skc10), true)=true))). % 20.08/9.42 tff(c_4378, plain, (![V_126]: (ifeq2(accessible_world(skc12, V_126), true, male(V_126, skc15), true)=true))). % 20.08/9.42 tff(c_4663, plain, (![V_135]: (ifeq2(accessible_world(skc12, V_135), true, relation(V_135, skc12), true)=true))). % 20.08/9.42 tff(c_1604, plain, (ifeq(tuple(true, existent(skc8, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.42 tff(c_7789, plain, (ifeq2(agent(skc8, skf1(skc15), skc15), true, true, true)=true)). % 20.08/9.42 tff(c_4201, plain, (![V_78]: (ifeq2(accessible_world(skc12, V_78), true, eventuality(V_78, skc13), true)=true))). % 20.08/9.42 tff(c_4451, plain, (![V_129]: (ifeq2(accessible_world(skc12, V_129), true, forename(V_129, skc11), true)=true))). % 20.08/9.42 tff(c_1855, plain, (![U_306]: (ifeq2(think_believe_consider(U_306, skc13), true, ifeq2(accessible_world(U_306, skc8), true, true, true), true)=true))). % 20.08/9.43 tff(c_3121, plain, (![V_132]: (ifeq2(accessible_world(skc12, V_132), true, relname(V_132, skc14), true)=true))). % 20.08/9.43 tff(c_2288, plain, (![V_328]: (ifeq2(accessible_world(skc8, V_328), true, nonexistent(V_328, skc9), true)=true))). % 20.08/9.43 tff(c_2787, plain, (![V_352]: (ifeq2(accessible_world(skc8, V_352), true, specific(V_352, skc13), true)=true))). % 20.08/9.43 tff(c_1760, plain, (![V_301]: (ifeq2(accessible_world(skc8, V_301), true, unisex(V_301, skc13), true)=true))). % 20.08/9.43 tff(c_1922, plain, (![V_310]: (ifeq2(accessible_world(skc8, V_310), true, relation(V_310, skc14), true)=true))). % 20.08/9.43 tff(c_1510, plain, (ifeq(tuple(true, general(skc8, skc13)), tuple(true, true), a, b)=b)). % 20.08/9.43 tff(c_8516, plain, (be(skc12, skc9, skc10, skc10)=true)). % 20.08/9.43 tff(c_3577, plain, (![W_400, X_403, Y_399]: (ifeq2(be(skc8, W_400, X_403, Y_399), true, be(skc12, W_400, X_403, Y_399), true)=true))). % 20.08/9.43 tff(c_1923, plain, (![V_310]: (ifeq2(accessible_world(skc8, V_310), true, relation(V_310, skc11), true)=true))). % 20.08/9.43 tff(c_2788, plain, (![V_352]: (ifeq2(accessible_world(skc8, V_352), true, specific(V_352, skc9), true)=true))). % 20.08/9.43 tff(c_2557, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc13), true)=true))). % 20.08/9.43 tff(c_2172, plain, (![V_322]: (ifeq2(accessible_world(skc8, V_322), true, abstraction(V_322, skc12), true)=true))). % 20.08/9.43 tff(c_2721, plain, (![V_349]: (ifeq2(accessible_world(skc8, V_349), true, organism(V_349, skc15), true)=true))). % 20.08/9.43 tff(c_1607, plain, (ifeq(tuple(true, existent(skc8, skc9)), tuple(true, true), a, b)=b)). % 20.08/9.43 tff(c_2556, plain, (![V_340]: (ifeq2(accessible_world(skc8, V_340), true, thing(V_340, skc9), true)=true))). % 20.08/9.43 tff(c_8347, plain, (![W_524]: (ifeq2(state(skc8, W_524), true, state(skc12, W_524), true)=true))). % 20.08/9.43 tff(c_2720, plain, (![V_349]: (ifeq2(accessible_world(skc8, V_349), true, organism(V_349, skc10), true)=true))). % 20.08/9.43 tff(c_2342, plain, (![V_331]: (ifeq2(accessible_world(skc8, V_331), true, human(V_331, skc15), true)=true))). % 20.08/9.43 tff(c_2341, plain, (![V_331]: (ifeq2(accessible_world(skc8, V_331), true, human(V_331, skc10), true)=true))). % 20.08/9.43 tff(c_2287, plain, (![V_328]: (ifeq2(accessible_world(skc8, V_328), true, nonexistent(V_328, skc13), true)=true))). % 20.08/9.43 tff(c_3280, plain, (![V_381]: (ifeq2(accessible_world(skc8, V_381), true, animate(V_381, skc15), true)=true))). % 20.08/9.43 tff(c_1565, plain, (ifeq(tuple(unisex(skc8, skc15), true), tuple(true, true), a, b)=b)). % 20.08/9.43 tff(c_3281, plain, (![V_381]: (ifeq2(accessible_world(skc8, V_381), true, animate(V_381, skc10), true)=true))). % 20.08/9.43 tff(c_8186, plain, (![W_516]: (ifeq2(vincent_forename(skc8, W_516), true, vincent_forename(skc12, W_516), true)=true))). % 20.08/9.43 tff(c_1759, plain, (![V_301]: (ifeq2(accessible_world(skc8, V_301), true, unisex(V_301, skc9), true)=true))). % 20.08/9.43 tff(c_4151, plain, (![V_96]: (ifeq2(accessible_world(skc12, V_96), true, event(V_96, skc13), true)=true))). % 20.08/9.43 tff(c_3704, plain, (![V_75]: (ifeq2(accessible_world(skc12, V_75), true, state(V_75, skc9), true)=true))). % 20.08/9.43 tff(c_3042, plain, (![V_129]: (ifeq2(accessible_world(skc12, V_129), true, forename(V_129, skc14), true)=true))). % 20.08/9.43 tff(c_4630, plain, (![V_159]: (ifeq2(accessible_world(skc12, V_159), true, proposition(V_159, skc12), true)=true))). % 20.08/9.43 tff(c_1568, plain, (ifeq(tuple(unisex(skc8, skc10), true), tuple(true, true), a, b)=b)). % 20.08/9.43 tff(c_4032, plain, (![V_99]: (ifeq2(accessible_world(skc12, V_99), true, man(V_99, skc10), true)=true))). % 20.08/9.43 tff(c_8013, plain, (![W_508]: (ifeq2(abstraction(skc8, W_508), true, abstraction(skc12, W_508), true)=true))). % 20.08/9.43 tff(c_4297, plain, (![V_99]: (ifeq2(accessible_world(skc12, V_99), true, man(V_99, skc15), true)=true))). % 20.08/9.43 tff(c_3598, plain, (![V_162]: (ifeq2(accessible_world(skc12, V_162), true, vincent_forename(V_162, skc14), true)=true))). % 20.08/9.43 tff(c_7929, plain, (ifeq2(accessible_world(skc12, skc12), true, true, true)=true)). % 20.08/9.43 tff(c_7939, plain, (agent(skc12, skf1(skc10), skc10)=true)). % 20.08/9.43 tff(c_4410, plain, (![V_147]: (ifeq2(accessible_world(skc12, V_147), true, jules_forename(V_147, skc11), true)=true))). % 20.08/9.43 tff(c_1807, plain, (![V_304]: (ifeq2(accessible_world(skc8, V_304), true, eventuality(V_304, skc13), true)=true))). % 20.08/9.43 tff(c_1654, plain, (![V_295]: (ifeq2(accessible_world(skc8, V_295), true, relname(V_295, skc14), true)=true))). % 20.08/9.43 tff(c_2823, plain, (![U_354]: (ifeq2(accessible_world(U_354, skc8), true, ifeq2(jules_forename(U_354, skc11), true, true, true), true)=true))). % 20.08/9.43 tff(c_1653, plain, (![V_295]: (ifeq2(accessible_world(skc8, V_295), true, relname(V_295, skc11), true)=true))). % 20.08/9.43 tff(c_1924, plain, (![V_310]: (ifeq2(accessible_world(skc8, V_310), true, relation(V_310, skc12), true)=true))). % 20.08/9.43 tff(c_1808, plain, (![V_304]: (ifeq2(accessible_world(skc8, V_304), true, eventuality(V_304, skc9), true)=true))). % 20.08/9.43 tff(c_7777, plain, (agent(skc12, skf1(skc15), skc15)=true)). % 20.08/9.43 tff(c_3356, plain, (![V_384]: (ifeq2(accessible_world(skc8, V_384), true, human_person(V_384, skc15), true)=true))). % 20.08/9.43 tff(c_7701, plain, (![W_496]: (ifeq2(human(skc8, W_496), true, human(skc12, W_496), true)=true))). % 20.08/9.43 tff(c_2897, plain, (![V_361]: (ifeq2(accessible_world(skc8, V_361), true, male(V_361, skc15), true)=true))). % 20.08/9.43 tff(c_3355, plain, (![V_384]: (ifeq2(accessible_world(skc8, V_384), true, human_person(V_384, skc10), true)=true))). % 20.08/9.43 tff(c_2041, plain, (![V_316]: (ifeq2(accessible_world(skc8, V_316), true, event(V_316, skc9), true)=true))). % 20.08/9.43 tff(c_2898, plain, (![V_361]: (ifeq2(accessible_world(skc8, V_361), true, male(V_361, skc10), true)=true))). % 20.08/9.43 tff(c_7608, plain, (![V_441]: (ifeq2(smoke(skc8, skf1(V_441)), true, true, true)=true))). % 20.08/9.43 tff(c_7583, plain, (![W_489]: (ifeq2(smoke(skc8, W_489), true, smoke(skc12, W_489), true)=true))). % 20.08/9.43 tff(c_7510, plain, (![V_456]: (ifeq2(specific(skc8, skf1(V_456)), true, true, true)=true))). % 20.08/9.43 tff(c_5038, plain, (![W_428]: (ifeq2(proposition(skc8, W_428), true, proposition(skc12, W_428), true)=true))). % 20.08/9.43 tff(c_5749, plain, (![W_434]: (ifeq2(specific(skc8, W_434), true, specific(skc12, W_434), true)=true))). % 20.08/9.43 tff(c_1968, plain, (![U_312]: (ifeq2(present(U_312, skc13), true, ifeq2(accessible_world(U_312, skc8), true, true, true), true)=true))). % 20.08/9.43 tff(c_7350, plain, (![W_480]: (ifeq2(forename(skc8, W_480), true, forename(skc12, W_480), true)=true))). % 20.08/9.43 tff(c_7413, plain, (![V_452]: (ifeq2(eventuality(skc8, skf1(V_452)), true, true, true)=true))). % 20.08/9.43 tff(c_5874, plain, (![W_435]: (ifeq2(eventuality(skc8, W_435), true, eventuality(skc12, W_435), true)=true))). % 20.08/9.43 tff(c_6138, plain, (![W_438]: (ifeq2(nonhuman(skc8, W_438), true, nonhuman(skc12, W_438), true)=true))). % 20.08/9.43 tff(c_5993, plain, (![W_436]: (ifeq2(relname(skc8, W_436), true, relname(skc12, W_436), true)=true))). % 20.08/9.43 tff(c_5430, plain, (![V_431]: (ifeq2(accessible_world(skc8, V_431), true, think_believe_consider(V_431, skc13), true)=true))). % 20.08/9.43 tff(c_7213, plain, (![V_466]: (ifeq2(singleton(skc8, skf1(V_466)), true, true, true)=true))). % 20.08/9.43 tff(c_7091, plain, (![W_472]: (ifeq2(singleton(skc8, W_472), true, singleton(skc12, W_472), true)=true))). % 20.08/9.43 tff(c_5278, plain, (![W_430]: (ifeq2(relation(skc8, W_430), true, relation(skc12, W_430), true)=true))). % 20.08/9.43 tff(c_5535, plain, (![V_432]: (ifeq2(accessible_world(skc8, V_432), true, present(V_432, skc13), true)=true))). % 20.08/9.43 tff(c_6573, plain, (![W_450]: (ifeq2(human_person(skc8, W_450), true, human_person(skc12, W_450), true)=true))). % 20.08/9.43 tff(c_6377, plain, (![W_440]: (ifeq2(living(skc8, W_440), true, living(skc12, W_440), true)=true))). % 20.08/9.43 tff(c_6860, plain, (![W_465]: (ifeq2(organism(skc8, W_465), true, organism(skc12, W_465), true)=true))). % 20.08/9.43 tff(c_5171, plain, (![W_429]: (ifeq2(general(skc8, W_429), true, general(skc12, W_429), true)=true))). % 20.08/9.43 tff(c_6741, plain, (![W_458]: (ifeq2(jules_forename(skc8, W_458), true, jules_forename(skc12, W_458), true)=true))). % 20.08/9.43 tff(c_6891, plain, (![V_466]: (singleton(skc12, skf1(V_466))=true))). % 20.08/9.43 tff(c_6729, plain, (![V_457]: (ifeq2(entity(skc12, skf1(V_457)), true, true, true)=true))). % 20.08/9.43 tff(c_6790, plain, (![V_460]: (ifeq2(abstraction(skc12, skf1(V_460)), true, true, true)=true))). % 20.08/9.43 tff(c_6803, plain, (![V_461]: (thing(skc12, skf1(V_461))=true))). % 20.08/9.43 tff(c_6763, plain, (![V_459]: (unisex(skc12, skf1(V_459))=true))). % 20.08/9.43 tff(c_6699, plain, (![V_456]: (specific(skc12, skf1(V_456))=true))). % 20.08/9.43 tff(c_6662, plain, (![V_454]: (nonexistent(skc12, skf1(V_454))=true))). % 20.08/9.43 tff(c_6609, plain, (![V_452]: (eventuality(skc12, skf1(V_452))=true))). % 20.08/9.43 tff(c_6544, plain, (![V_448]: (ifeq2(state(skc12, skf1(V_448)), true, true, true)=true))). % 20.08/9.43 tff(c_6504, plain, (![V_446]: (ifeq2(present(skc8, skf1(V_446)), true, true, true)=true))). % 20.08/9.43 tff(c_6521, plain, (![V_447]: (event(skc12, skf1(V_447))=true))). % 20.08/9.43 tff(c_6472, plain, (![V_444]: (present(skc12, skf1(V_444))=true))). % 20.08/9.43 tff(c_2035, plain, (![U_315]: (ifeq2(accessible_world(U_315, skc8), true, ifeq2(event(U_315, skc13), true, true, true), true)=true))). % 20.08/9.43 tff(c_6433, plain, (![U_191]: (ifeq2(man(skc12, U_191), true, true, true)=true))). % 20.08/9.43 tff(c_6424, plain, (![V_441]: (smoke(skc12, skf1(V_441))=true))). % 20.08/9.43 tff(c_6387, plain, (theme(skc12, skc13, skc12)=true)). % 20.08/9.43 tff(c_6323, plain, (agent(skc12, skc13, skc15)=true)). % 20.08/9.43 tff(c_6288, plain, (of(skc12, skc11, skc10)=true)). % 20.08/9.43 tff(c_6253, plain, (of(skc12, skc14, skc15)=true)). % 20.08/9.43 tff(c_1703, plain, (![U_297]: (ifeq2(accessible_world(U_297, skc8), true, ifeq2(proposition(U_297, skc12), true, true, true), true)=true))). % 20.08/9.43 tff(c_6210, plain, (singleton(skc12, skc15)=true)). % 20.08/9.43 tff(c_6181, plain, (singleton(skc12, skc10)=true)). % 20.08/9.43 tff(c_6035, plain, (ifeq2(abstraction(skc12, skc10), true, true, true)=true)). % 20.08/9.43 tff(c_5960, plain, (ifeq2(abstraction(skc12, skc15), true, true, true)=true)). % 20.08/9.43 tff(c_5773, plain, (ifeq2(eventuality(skc12, skc15), true, true, true)=true)). % 20.08/9.43 tff(c_6101, plain, (existent(skc12, skc15)=true)). % 20.08/9.43 tff(c_6071, plain, (singleton(skc12, skc12)=true)). % 20.08/9.43 tff(c_3055, plain, (![U_371]: (ifeq2(accessible_world(U_371, skc8), true, ifeq2(vincent_forename(U_371, skc14), true, true, true), true)=true))). % 20.08/9.43 tff(c_5225, plain, (ifeq2(eventuality(skc12, skc12), true, true, true)=true)). % 20.08/9.43 tff(c_5222, plain, (ifeq2(entity(skc12, skc12), true, true, true)=true)). % 20.08/9.43 tff(c_6008, plain, (thing(skc12, skc10)=true)). % 20.08/9.43 tff(c_5456, plain, (ifeq2(eventuality(skc12, skc11), true, true, true)=true)). % 20.08/9.43 tff(c_5496, plain, (ifeq2(entity(skc12, skc11), true, true, true)=true)). % 20.08/9.43 tff(c_5933, plain, (thing(skc12, skc15)=true)). % 20.08/9.43 tff(c_5902, plain, (existent(skc12, skc10)=true)). % 20.08/9.43 tff(c_5845, plain, (singleton(skc12, skc11)=true)). % 20.08/9.43 tff(c_5798, plain, (ifeq2(eventuality(skc12, skc10), true, true, true)=true)). % 20.08/9.43 tff(c_5812, plain, (impartial(skc12, skc10)=true)). % 20.08/9.43 tff(c_5755, plain, (specific(skc12, skc10)=true)). % 20.08/9.43 tff(c_5754, plain, (specific(skc12, skc15)=true)). % 20.08/9.43 tff(c_5682, plain, (entity(skc12, skc10)=true)). % 20.08/9.43 tff(c_5654, plain, (singleton(skc12, skc13)=true)). % 20.08/9.43 tff(c_5644, plain, (ifeq2(accessible_world(skc12, skc8), true, true, true)=true)). % 20.08/9.43 tff(c_2926, plain, (![U_364]: (ifeq2(accessible_world(U_364, skc8), true, ifeq2(state(U_364, skc9), true, true, true), true)=true))). % 20.08/9.43 tff(c_5606, plain, (impartial(skc12, skc15)=true)). % 20.08/9.43 tff(c_3958, plain, (ifeq2(entity(skc12, skc9), true, true, true)=true)). % 20.08/9.43 tff(c_5568, plain, (unisex(skc12, skc12)=true)). % 20.08/9.43 tff(c_5515, plain, (living(skc12, skc10)=true)). % 20.08/9.43 tff(c_5478, plain, (thing(skc12, skc11)=true)). % 20.08/9.43 tff(c_4504, plain, (ifeq2(abstraction(skc12, skc13), true, true, true)=true)). % 20.08/9.43 tff(c_4694, plain, (ifeq2(abstraction(skc12, skc9), true, true, true)=true)). % 20.08/9.43 tff(c_5410, plain, (unisex(skc12, skc11)=true)). % 20.08/9.43 tff(c_5379, plain, (nonhuman(skc12, skc11)=true)). % 20.08/9.43 tff(c_5324, plain, (ifeq2(proposition(skc12, skc11), true, true, true)=true)). % 20.08/9.43 tff(c_5334, plain, (abstraction(skc12, skc11)=true)). % 20.08/9.43 tff(c_5304, plain, (relation(skc12, skc11)=true)). % 20.08/9.43 tff(c_5245, plain, (nonhuman(skc12, skc12)=true)). % 20.08/9.43 tff(c_4813, plain, (ifeq2(entity(skc12, skc13), true, true, true)=true)). % 20.08/9.43 tff(c_5204, plain, (thing(skc12, skc12)=true)). % 20.08/9.43 tff(c_5176, plain, (general(skc12, skc11)=true)). % 20.08/9.43 tff(c_5109, plain, (entity(skc12, skc15)=true)). % 20.08/9.43 tff(c_5078, plain, (general(skc12, skc12)=true)). % 20.08/9.43 tff(c_5050, plain, (singleton(skc12, skc9)=true)). % 20.08/9.43 tff(c_5001, plain, (living(skc12, skc15)=true)). % 20.08/9.43 tff(c_4970, plain, (human(skc12, skc10)=true)). % 20.08/9.43 tff(c_4933, plain, (organism(skc12, skc15)=true)). % 20.08/9.43 tff(c_3527, plain, (![W_395, X_396]: (ifeq2(agent(skc8, W_395, X_396), true, agent(skc12, W_395, X_396), true)=true))). % 20.08/9.43 tff(c_4892, plain, (human(skc12, skc15)=true)). % 20.08/9.43 tff(c_4864, plain, (animate(skc12, skc15)=true)). % 20.08/9.43 tff(c_4833, plain, (relname(skc12, skc11)=true)). % 20.08/9.43 tff(c_3404, plain, (![W_387, X_388]: (ifeq2(theme(skc8, W_387, X_388), true, theme(skc12, W_387, X_388), true)=true))). % 20.08/9.43 tff(c_4789, plain, (specific(skc12, skc13)=true)). % 20.08/9.43 tff(c_4761, plain, (animate(skc12, skc10)=true)). % 20.08/9.43 tff(c_4721, plain, (abstraction(skc12, skc12)=true)). % 20.08/9.43 tff(c_4654, plain, (ifeq2(relname(skc12, skc12), true, true, true)=true)). % 20.08/9.43 tff(c_3482, plain, (![W_391, X_392]: (ifeq2(of(skc8, W_391, X_392), true, of(skc12, W_391, X_392), true)=true))). % 20.08/9.43 tff(c_4670, plain, (unisex(skc12, skc9)=true)). % 20.08/9.43 tff(c_4636, plain, (relation(skc12, skc12)=true)). % 20.08/9.43 tff(c_4597, plain, (proposition(skc12, skc12)=true)). % 20.08/9.43 tff(c_1709, plain, (![V_298]: (ifeq2(accessible_world(skc8, V_298), true, proposition(V_298, skc12), true)=true))). % 20.08/9.43 tff(c_4552, plain, (nonexistent(skc12, skc13)=true)). % 20.08/9.43 tff(c_4518, plain, (unisex(skc12, skc13)=true)). % 20.08/9.44 tff(c_4446, plain, (ifeq2(vincent_forename(skc12, skc11), true, true, true)=true)). % 20.08/9.44 tff(c_4458, plain, (thing(skc12, skc13)=true)). % 20.08/9.44 tff(c_2093, plain, (![V_319]: (ifeq2(accessible_world(skc8, V_319), true, forename(V_319, skc11), true)=true))). % 20.08/9.44 tff(c_4416, plain, (forename(skc12, skc11)=true)). % 20.08/9.44 tff(c_4385, plain, (jules_forename(skc12, skc11)=true)). % 20.08/9.44 tff(c_4340, plain, (male(skc12, skc15)=true)). % 20.08/9.44 tff(c_2829, plain, (![V_355]: (ifeq2(accessible_world(skc8, V_355), true, jules_forename(V_355, skc11), true)=true))). % 20.08/9.44 tff(c_4303, plain, (human_person(skc12, skc15)=true)). % 20.08/9.44 tff(c_4260, plain, (man(skc12, skc15)=true)). % 20.08/9.44 tff(c_4209, plain, (organism(skc12, skc10)=true)). % 20.08/9.44 tff(c_2612, plain, (![V_343]: (ifeq2(accessible_world(skc8, V_343), true, man(V_343, skc15), true)=true))). % 20.08/9.44 tff(c_4165, plain, (eventuality(skc12, skc13)=true)). % 20.08/9.44 tff(c_4147, plain, (ifeq2(smoke(skc12, skc13), true, true, true)=true)). % 20.08/9.44 tff(c_4141, plain, (ifeq2(state(skc12, skc13), true, true, true)=true)). % 20.08/9.44 tff(c_4120, plain, (event(skc12, skc13)=true)). % 20.08/9.44 tff(c_2042, plain, (![V_316]: (ifeq2(accessible_world(skc8, V_316), true, event(V_316, skc13), true)=true))). % 20.08/9.44 tff(c_4075, plain, (male(skc12, skc10)=true)). % 20.08/9.44 tff(c_4038, plain, (human_person(skc12, skc10)=true)). % 20.08/9.44 tff(c_3995, plain, (man(skc12, skc10)=true)). % 20.08/9.44 tff(c_2613, plain, (![V_343]: (ifeq2(accessible_world(skc8, V_343), true, man(V_343, skc10), true)=true))). % 20.08/9.44 tff(c_3734, plain, (ifeq2(smoke(skc12, skc9), true, true, true)=true)). % 20.08/9.44 tff(c_3940, plain, (thing(skc12, skc9)=true)). % 20.08/9.44 tff(c_3905, plain, (think_believe_consider(skc12, skc13)=true)). % 20.08/9.44 tff(c_3861, plain, (specific(skc12, skc9)=true)). % 20.08/9.44 tff(c_1861, plain, (![W_307]: (ifeq2(think_believe_consider(skc8, W_307), true, think_believe_consider(skc12, W_307), true)=true))). % 20.08/9.44 tff(c_3830, plain, (nonexistent(skc12, skc9)=true)). % 20.08/9.44 tff(c_3785, plain, (eventuality(skc12, skc9)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3710, plain, (event(skc12, skc9)=true)). % 20.08/9.44 tff(c_3676, plain, (state(skc12, skc9)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2932, plain, (![V_365]: (ifeq2(accessible_world(skc8, V_365), true, state(V_365, skc9), true)=true))). % 20.08/9.44 tff(c_3554, plain, (vincent_forename(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3061, plain, (![V_372]: (ifeq2(accessible_world(skc8, V_372), true, vincent_forename(V_372, skc14), true)=true))). % 20.08/9.44 tff(c_3307, plain, (ifeq2(entity(skc12, skc14), true, true, true)=true)). % 20.08/9.44 tff(c_3419, plain, (ifeq2(eventuality(skc12, skc14), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3486, plain, (singleton(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3432, plain, (general(skc12, skc14)=true)). % 20.08/9.44 tff(c_3381, plain, (unisex(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3326, plain, (nonhuman(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3289, plain, (thing(skc12, skc14)=true)). % 20.08/9.44 tff(c_3152, plain, (ifeq2(proposition(skc12, skc14), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3221, plain, (abstraction(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3128, plain, (relation(skc12, skc14)=true)). % 20.08/9.44 tff(c_3073, plain, (relname(skc12, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3032, plain, (ifeq2(jules_forename(skc12, skc14), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_3011, plain, (forename(skc12, skc14)=true)). % 20.08/9.44 tff(c_2998, plain, (ifeq2(accessible_world(skc8, skc8), true, true, true)=true)). % 20.08/9.44 tff(c_2092, plain, (![V_319]: (ifeq2(accessible_world(skc8, V_319), true, forename(V_319, skc14), true)=true))). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2936, plain, (present(skc12, skc13)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1974, plain, (![W_313]: (ifeq2(present(skc8, W_313), true, present(skc12, W_313), true)=true))). % 20.08/9.44 tff(c_2463, plain, (ifeq2(eventuality(skc8, skc11), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2858, plain, (singleton(skc8, skc11)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2308, plain, (ifeq2(eventuality(skc8, skc10), true, true, true)=true)). % 20.08/9.44 tff(c_2314, plain, (ifeq2(abstraction(skc8, skc10), true, true, true)=true)). % 20.08/9.44 tff(c_1983, plain, (ifeq2(eventuality(skc8, skc14), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2796, plain, (singleton(skc8, skc10)=true)). % 20.08/9.44 tff(c_2229, plain, (ifeq2(eventuality(skc8, skc15), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2235, plain, (ifeq2(abstraction(skc8, skc15), true, true, true)=true)). % 20.08/9.44 tff(c_2729, plain, (singleton(skc8, skc15)=true)). % 20.08/9.44 tff(c_2359, plain, (ifeq2(entity(skc8, skc11), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2680, plain, (singleton(skc8, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1980, plain, (ifeq2(entity(skc8, skc14), true, true, true)=true)). % 20.08/9.44 tff(c_1187, plain, (ifeq2(entity(skc8, skc12), true, true, true)=true)). % 20.08/9.44 tff(c_2617, plain, (existent(skc8, skc10)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2562, plain, (nonhuman(skc8, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2476, plain, (specific(skc8, skc15)=true)). % 20.08/9.44 tff(c_2429, plain, (unisex(skc8, skc11)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2381, plain, (existent(skc8, skc15)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2347, plain, (thing(skc8, skc11)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2293, plain, (thing(skc8, skc10)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2245, plain, (general(skc8, skc11)=true)). % 20.08/9.44 tff(c_2190, plain, (thing(skc8, skc15)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2135, plain, (nonhuman(skc8, skc11)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1144, plain, (ifeq2(eventuality(skc8, skc12), true, true, true)=true)). % 20.08/9.44 tff(c_2097, plain, (unisex(skc8, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_2046, plain, (specific(skc8, skc10)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1998, plain, (general(skc8, skc14)=true)). % 20.08/9.44 tff(c_1955, plain, (thing(skc8, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1887, plain, (abstraction(skc8, skc14)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1866, plain, (living(skc8, skc10)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1816, plain, (abstraction(skc8, skc11)=true)). % 20.08/9.44 tff(c_912, plain, (ifeq2(proposition(skc8, skc11), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1767, plain, (impartial(skc8, skc10)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1714, plain, (singleton(skc8, skc13)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1666, plain, (entity(skc8, skc15)=true)). % 20.08/9.44 tff(c_1171, plain, (ifeq2(abstraction(skc8, skc13), true, true, true)=true)). % 20.08/9.44 tff(c_1206, plain, (ifeq2(entity(skc8, skc9), true, true, true)=true)). % 20.08/9.44 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))). % 20.08/9.44 tff(c_1613, plain, (living(skc8, skc15)=true)). % 20.08/9.44 tff(c_192, plain, (![U_204, V_205]: (ifeq(tuple(nonexistent(U_204, V_205), existent(U_204, V_205)), tuple(true, true), a, b)=b))). % 20.08/9.44 tff(c_946, plain, (ifeq2(proposition(skc8, skc14), true, true, true)=true)). % 20.08/9.44 tff(c_1575, plain, (impartial(skc8, skc15)=true)). % 20.08/9.44 tff(c_186, plain, (![U_198, V_199]: (ifeq(tuple(unisex(U_198, V_199), male(U_198, V_199)), tuple(true, true), a, b)=b))). % 20.08/9.44 tff(c_1523, plain, (entity(skc8, skc10)=true)). % 20.08/9.44 tff(c_188, plain, (![U_200, V_201]: (ifeq(tuple(specific(U_200, V_201), general(U_200, V_201)), tuple(true, true), a, b)=b))). % 20.08/9.44 tff(c_1486, plain, (animate(skc8, skc15)=true)). % 20.08/9.44 tff(c_1465, plain, (animate(skc8, skc10)=true)). % 20.08/9.44 tff(c_190, plain, (![U_202, V_203]: (ifeq(tuple(human(U_202, V_203), nonhuman(U_202, V_203)), tuple(true, true), a, b)=b))). % 20.08/9.44 tff(c_1428, plain, (human(skc8, skc10)=true)). % 20.08/9.44 tff(c_184, plain, (![U_197]: (ifeq2(man(skc12, U_197), true, agent(skc12, skf1(U_197), U_197), true)=true))). % 20.08/9.44 tff(c_1400, plain, (human(skc8, skc15)=true)). % 20.08/9.44 tff(c_1363, plain, (organism(skc8, skc10)=true)). % 20.08/9.44 tff(c_1326, plain, (organism(skc8, skc15)=true)). % 20.08/9.44 tff(c_1296, plain, (human_person(skc8, skc10)=true)). % 20.08/9.44 tff(c_1259, plain, (human_person(skc8, skc15)=true)). % 20.08/9.44 tff(c_24, plain, (![U_26, V_27]: (ifeq2(man(U_26, V_27), true, human_person(U_26, V_27), true)=true))). % 20.08/9.44 tff(c_1225, plain, (singleton(skc8, skc9)=true)). % 20.08/9.44 tff(c_1194, plain, (thing(skc8, skc9)=true)). % 20.08/9.44 tff(c_30, plain, (![U_32, V_33]: (ifeq2(entity(U_32, V_33), true, thing(U_32, V_33), true)=true))). % 20.08/9.44 tff(c_1153, plain, (thing(skc8, skc13)=true)). % 20.08/9.44 tff(c_10, plain, (![U_12, V_13]: (ifeq2(eventuality(U_12, V_13), true, thing(U_12, V_13), true)=true))). % 20.08/9.44 tff(c_1049, plain, (ifeq2(entity(skc8, skc13), true, true, true)=true)). % 20.08/9.44 tff(c_1120, plain, (ifeq2(abstraction(skc8, skc9), true, true, true)=true)). % 20.08/9.44 tff(c_1105, plain, (unisex(skc8, skc9)=true)). % 20.08/9.44 tff(c_34, plain, (![U_36, V_37]: (ifeq2(entity(U_36, V_37), true, existent(U_36, V_37), true)=true))). % 20.08/9.44 tff(c_1074, plain, (unisex(skc8, skc13)=true)). % 20.08/9.44 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, unisex(U_20, V_21), true)=true))). % 20.08/9.44 tff(c_1034, plain, (specific(skc8, skc13)=true)). % 20.08/9.44 tff(c_1013, plain, (ifeq2(smoke(skc8, skc9), true, true, true)=true)). % 20.08/9.44 tff(c_28, plain, (![U_30, V_31]: (ifeq2(organism(U_30, V_31), true, entity(U_30, V_31), true)=true))). % 20.08/9.44 tff(c_993, plain, (event(skc8, skc9)=true)). % 20.08/9.44 tff(c_20, plain, (![U_22, V_23]: (ifeq2(state(U_22, V_23), true, event(U_22, V_23), true)=true))). % 20.08/9.44 tff(c_955, plain, (specific(skc8, skc9)=true)). % 20.08/9.44 tff(c_928, plain, (relation(skc8, skc14)=true)). % 20.08/9.44 tff(c_42, plain, (![U_44, V_45]: (ifeq2(human_person(U_44, V_45), true, animate(U_44, V_45), true)=true))). % 20.08/9.44 tff(c_894, plain, (relation(skc8, skc11)=true)). % 20.08/9.44 tff(c_14, plain, (![U_16, V_17]: (ifeq2(eventuality(U_16, V_17), true, specific(U_16, V_17), true)=true))). % 20.08/9.44 tff(c_865, plain, (ifeq2(relname(skc8, skc12), true, true, true)=true)). % 20.08/9.44 tff(c_48, plain, (![U_50, V_51]: (ifeq2(relname(U_50, V_51), true, relation(U_50, V_51), true)=true))). % 20.08/9.44 tff(c_840, plain, (singleton(skc8, skc12)=true)). % 20.08/9.44 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, human(U_42, V_43), true)=true))). % 20.08/9.44 tff(c_785, plain, (ifeq2(state(skc8, skc13), true, true, true)=true)). % 20.08/9.44 tff(c_798, plain, (nonexistent(skc8, skc13)=true)). % 20.08/9.44 tff(c_12, plain, (![U_14, V_15]: (ifeq2(thing(U_14, V_15), true, singleton(U_14, V_15), true)=true))). % 20.08/9.44 tff(c_767, plain, (eventuality(skc8, skc13)=true)). % 20.08/9.44 tff(c_22, plain, (![U_24, V_25]: (ifeq2(event(U_24, V_25), true, eventuality(U_24, V_25), true)=true))). % 20.08/9.44 tff(c_733, plain, (unisex(skc8, skc12)=true)). % 20.08/9.44 tff(c_32, plain, (![U_34, V_35]: (ifeq2(entity(U_34, V_35), true, specific(U_34, V_35), true)=true))). % 20.08/9.44 tff(c_705, plain, (male(skc8, skc15)=true)). % 20.08/9.44 tff(c_677, plain, (male(skc8, skc10)=true)). % 20.08/9.44 tff(c_36, plain, (![U_38, V_39]: (ifeq2(organism(U_38, V_39), true, impartial(U_38, V_39), true)=true))). % 20.08/9.44 tff(c_643, plain, (thing(skc8, skc12)=true)). % 20.08/9.44 tff(c_44, plain, (![U_46, V_47]: (ifeq2(man(U_46, V_47), true, male(U_46, V_47), true)=true))). % 20.08/9.44 tff(c_622, plain, (nonexistent(skc8, skc9)=true)). % 20.08/9.44 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, nonexistent(U_18, V_19), true)=true))). % 20.08/9.44 tff(c_591, plain, (nonhuman(skc8, skc12)=true)). % 20.08/9.44 tff(c_26, plain, (![U_28, V_29]: (ifeq2(human_person(U_28, V_29), true, organism(U_28, V_29), true)=true))). % 20.08/9.45 tff(c_563, plain, (general(skc8, skc12)=true)). % 20.08/9.45 tff(c_530, plain, (abstraction(skc8, skc12)=true)). % 20.08/9.45 tff(c_50, plain, (![U_52, V_53]: (ifeq2(relation(U_52, V_53), true, abstraction(U_52, V_53), true)=true))). % 20.08/9.45 tff(c_499, plain, (relation(skc8, skc12)=true)). % 20.08/9.45 tff(c_64, plain, (![U_66, V_67]: (ifeq2(proposition(U_66, V_67), true, relation(U_66, V_67), true)=true))). % 20.08/9.45 tff(c_56, plain, (![U_58, V_59]: (ifeq2(abstraction(U_58, V_59), true, general(U_58, V_59), true)=true))). % 20.08/9.45 tff(c_461, plain, (eventuality(skc8, skc9)=true)). % 20.08/9.45 tff(c_8, plain, (![U_10, V_11]: (ifeq2(state(U_10, V_11), true, eventuality(U_10, V_11), true)=true))). % 20.08/9.45 tff(c_58, plain, (![U_60, V_61]: (ifeq2(abstraction(U_60, V_61), true, unisex(U_60, V_61), true)=true))). % 20.08/9.45 tff(c_434, plain, (ifeq2(smoke(skc8, skc13), true, true, true)=true)). % 20.08/9.45 tff(c_62, plain, (![U_64, V_65]: (ifeq2(smoke(U_64, V_65), true, event(U_64, V_65), true)=true))). % 20.08/9.45 tff(c_412, plain, (ifeq2(jules_forename(skc8, skc14), true, true, true)=true)). % 20.08/9.45 tff(c_60, plain, (![U_62, V_63]: (ifeq2(jules_forename(U_62, V_63), true, forename(U_62, V_63), true)=true))). % 20.08/9.45 tff(c_387, plain, (relname(skc8, skc11)=true)). % 20.08/9.45 tff(c_359, plain, (relname(skc8, skc14)=true)). % 20.08/9.45 tff(c_54, plain, (![U_56, V_57]: (ifeq2(abstraction(U_56, V_57), true, nonhuman(U_56, V_57), true)=true))). % 20.08/9.45 tff(c_46, plain, (![U_48, V_49]: (ifeq2(forename(U_48, V_49), true, relname(U_48, V_49), true)=true))). % 20.08/9.45 tff(c_334, plain, (ifeq2(vincent_forename(skc8, skc11), true, true, true)=true)). % 20.08/9.45 tff(c_66, plain, (![U_68, V_69]: (ifeq2(vincent_forename(U_68, V_69), true, forename(U_68, V_69), true)=true))). % 20.08/9.45 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))). % 20.08/9.45 tff(c_38, plain, (![U_40, V_41]: (ifeq2(organism(U_40, V_41), true, living(U_40, V_41), true)=true))). % 20.08/9.45 tff(c_52, plain, (![U_54, V_55]: (ifeq2(abstraction(U_54, V_55), true, thing(U_54, V_55), true)=true))). % 20.08/9.45 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 20.08/9.45 tff(c_176, plain, (be(skc8, skc9, skc10, skc10)=true)). % 20.08/9.45 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 20.08/9.45 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 20.08/9.45 tff(c_172, plain, (theme(skc8, skc13, skc12)=true)). % 20.08/9.45 tff(c_168, plain, (of(skc8, skc14, skc15)=true)). % 20.08/9.45 tff(c_170, plain, (agent(skc8, skc13, skc15)=true)). % 20.08/9.45 tff(c_174, plain, (of(skc8, skc11, skc10)=true)). % 20.08/9.45 tff(c_166, plain, (proposition(skc8, skc12)=true)). % 20.08/9.45 tff(c_150, plain, (event(skc8, skc13)=true)). % 20.08/9.45 tff(c_152, plain, (present(skc8, skc13)=true)). % 20.08/9.45 tff(c_154, plain, (think_believe_consider(skc8, skc13)=true)). % 20.08/9.45 tff(c_146, plain, (forename(skc8, skc14)=true)). % 20.08/9.45 tff(c_148, plain, (vincent_forename(skc8, skc14)=true)). % 20.08/9.45 tff(c_156, plain, (jules_forename(skc8, skc11)=true)). % 20.08/9.45 tff(c_144, plain, (man(skc8, skc15)=true)). % 20.08/9.45 tff(c_158, plain, (forename(skc8, skc11)=true)). % 20.08/9.45 tff(c_160, plain, (man(skc8, skc10)=true)). % 20.08/9.45 tff(c_162, plain, (state(skc8, skc9)=true)). % 20.08/9.45 tff(c_164, plain, (accessible_world(skc8, skc12)=true)). % 20.08/9.45 tff(c_142, plain, (actual_world(skc8)=true)). % 20.08/9.45 tff(c_194, plain, (b!=a)). % 20.08/9.45 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.08/9.45 %------------------------------------------------------------------------------