%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP248-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n017.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:46 PM UTC 2025 % Result : Satisfiable 42.42s 27.48s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : NLP248-10 : TPTP v9.0.0. Released v7.5.0. % 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.09/0.29 % Computer : n017.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Tue Apr 8 09:47:25 EDT 2025 % 0.09/0.29 % CPUTime : % 42.42/27.47 % 42.42/27.48 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/27.48 % 42.42/27.48 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/27.48 %$ 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 > skc26 > skc25 > skc24 > skc23 > skc22 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 > skc14 > skc13 > b > a % 42.42/27.48 % 42.42/27.48 %Foreground sorts: % 42.42/27.48 % 42.42/27.48 % 42.42/27.48 %Background operators: % 42.42/27.48 % 42.42/27.48 % 42.42/27.48 %Foreground operators: % 42.42/27.48 tff(agent, type, agent: ($i * $i * $i) > $i). % 42.42/27.48 tff(skc16, type, skc16: $i). % 42.42/27.48 tff(proposition, type, proposition: ($i * $i) > $i). % 42.42/27.48 tff(specific, type, specific: ($i * $i) > $i). % 42.42/27.48 tff(organism, type, organism: ($i * $i) > $i). % 42.42/27.48 tff(impartial, type, impartial: ($i * $i) > $i). % 42.42/27.48 tff(a, type, a: $i). % 42.42/27.48 tff(smoke, type, smoke: ($i * $i) > $i). % 42.42/27.48 tff(jules_forename, type, jules_forename: ($i * $i) > $i). % 42.42/27.48 tff(eventuality, type, eventuality: ($i * $i) > $i). % 42.42/27.48 tff(theme, type, theme: ($i * $i * $i) > $i). % 42.42/27.48 tff(skc18, type, skc18: $i). % 42.42/27.48 tff(state, type, state: ($i * $i) > $i). % 42.42/27.48 tff(tuple, type, tuple: ($i * $i) > $i). % 42.42/27.48 tff(skc25, type, skc25: $i). % 42.42/27.48 tff(human_person, type, human_person: ($i * $i) > $i). % 42.42/27.48 tff(skf1, type, skf1: $i > $i). % 42.42/27.48 tff(be, type, be: ($i * $i * $i * $i) > $i). % 42.42/27.48 tff(relname, type, relname: ($i * $i) > $i). % 42.42/27.48 tff(skc14, type, skc14: $i). % 42.42/27.48 tff(skc17, type, skc17: $i). % 42.42/27.48 tff(skc13, type, skc13: $i). % 42.42/27.48 tff(thing, type, thing: ($i * $i) > $i). % 42.42/27.48 tff(unisex, type, unisex: ($i * $i) > $i). % 42.42/27.48 tff(abstraction, type, abstraction: ($i * $i) > $i). % 42.42/27.48 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 42.42/27.48 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 42.42/27.48 tff(skc26, type, skc26: $i). % 42.42/27.48 tff(relation, type, relation: ($i * $i) > $i). % 42.42/27.48 tff(skc24, type, skc24: $i). % 42.42/27.48 tff(actual_world, type, actual_world: $i > $i). % 42.42/27.48 tff(of, type, of: ($i * $i * $i) > $i). % 42.42/27.48 tff(present, type, present: ($i * $i) > $i). % 42.42/27.48 tff(b, type, b: $i). % 42.42/27.48 tff(skc20, type, skc20: $i). % 42.42/27.48 tff(animate, type, animate: ($i * $i) > $i). % 42.42/27.48 tff(human, type, human: ($i * $i) > $i). % 42.42/27.48 tff(skc23, type, skc23: $i). % 42.42/27.48 tff(skc22, type, skc22: $i). % 42.42/27.48 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 42.42/27.48 tff(skc15, type, skc15: $i). % 42.42/27.48 tff(existent, type, existent: ($i * $i) > $i). % 42.42/27.48 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 42.42/27.48 tff(forename, type, forename: ($i * $i) > $i). % 42.42/27.48 tff(true, type, true: $i). % 42.42/27.48 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 42.42/27.48 tff(male, type, male: ($i * $i) > $i). % 42.42/27.48 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 42.42/27.48 tff(entity, type, entity: ($i * $i) > $i). % 42.42/27.48 tff(skc19, type, skc19: $i). % 42.42/27.48 tff(singleton, type, singleton: ($i * $i) > $i). % 42.42/27.48 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 42.42/27.48 tff(event, type, event: ($i * $i) > $i). % 42.42/27.48 tff(man, type, man: ($i * $i) > $i). % 42.42/27.48 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 42.42/27.48 tff(general, type, general: ($i * $i) > $i). % 42.42/27.48 tff(living, type, living: ($i * $i) > $i). % 42.42/27.48 % 42.42/27.48 %Saturated clause set: % 42.42/27.49 tff(c_28974, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skf1(skc19), V_190), true, ifeq3(agent(skc14, Y_189, skc19), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_40073, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skf1(skc23), V_190), true, ifeq3(agent(skc14, Y_189, skc23), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_40030, plain, (![W_1596, V_1598]: (ifeq3(theme(skc14, skf1(skc23), W_1596), true, ifeq3(theme(skc14, skf1(skc23), V_1598), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1596), true, ifeq3(proposition(skc14, V_1598), true, V_1598, W_1596), W_1596), W_1596), W_1596), W_1596), W_1596)=W_1596))). % 42.42/27.49 tff(c_39987, plain, (![W_1593, V_1595]: (ifeq3(theme(skc14, skf1(skc19), W_1593), true, ifeq3(theme(skc14, skf1(skc19), V_1595), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1593), true, ifeq3(proposition(skc14, V_1595), true, V_1595, W_1593), W_1593), W_1593), W_1593), W_1593), W_1593)=W_1593))). % 42.42/27.49 tff(c_39996, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skf1(skc23), W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_28973, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skf1(skc19), W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_39912, plain, (![W_1588, V_1589]: (ifeq3(theme(skc14, skf1(skc23), W_1588), true, ifeq3(theme(skc14, skc15, V_1589), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1588), true, ifeq3(proposition(skc14, V_1589), true, V_1589, W_1588), W_1588), W_1588), W_1588), W_1588), W_1588)=W_1588))). % 42.42/27.49 tff(c_5656, plain, (![Y_189, W_185, V_190, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc15, V_190), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_38238, plain, (![Y_1504, V_1506]: (ifeq3(theme(skc14, Y_1504, skc14), true, ifeq3(theme(skc14, skf1(skc19), V_1506), true, ifeq3(agent(skc14, Y_1504, skc19), true, ifeq3(think_believe_consider(skc14, Y_1504), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_39757, plain, (![V_1583]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skf1(skc19), V_1583), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1583), true, V_1583, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_38237, plain, (![X_1505, V_1506]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, X_1505, V_1506), true, ifeq3(agent(skc14, X_1505, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1505), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_38445, plain, (![W_1513, X_1514]: (ifeq3(theme(skc14, skf1(skc23), W_1513), true, ifeq3(theme(skc14, X_1514, skc14), true, ifeq3(agent(skc14, X_1514, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, X_1514), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.49 tff(c_39608, plain, (![W_1578]: (ifeq3(theme(skc14, skf1(skc23), W_1578), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1578), true, skc14, W_1578), W_1578), W_1578), W_1578), W_1578)=W_1578))). % 42.42/27.49 tff(c_38446, plain, (![Y_1512, W_1513]: (ifeq3(theme(skc14, Y_1512, W_1513), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, Y_1512, skc23), true, ifeq3(think_believe_consider(skc14, Y_1512), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.49 tff(c_38448, plain, (![Y_1512, W_1513]: (ifeq3(theme(skc14, Y_1512, W_1513), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(agent(skc14, Y_1512, skc19), true, ifeq3(think_believe_consider(skc14, Y_1512), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.49 tff(c_39430, plain, (![W_1568, V_1569]: (ifeq3(theme(skc14, skf1(skc23), W_1568), true, ifeq3(theme(skc14, skc17, V_1569), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1568), true, ifeq3(proposition(skc14, V_1569), true, V_1569, W_1568), W_1568), W_1568), W_1568), W_1568), W_1568)=W_1568))). % 42.42/27.49 tff(c_38236, plain, (![Y_1504, V_1506]: (ifeq3(theme(skc14, Y_1504, skc14), true, ifeq3(theme(skc14, skf1(skc23), V_1506), true, ifeq3(agent(skc14, Y_1504, skc23), true, ifeq3(think_believe_consider(skc14, Y_1504), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_39371, plain, (![Y_189, W_185, V_190, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc17, V_190), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc17, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.49 tff(c_38699, plain, (![W_1522, V_1524]: (ifeq3(theme(skc14, skc15, W_1522), true, ifeq3(theme(skc14, skf1(skc23), V_1524), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1522), true, ifeq3(proposition(skc14, V_1524), true, V_1524, W_1522), W_1522), W_1522), W_1522), W_1522), W_1522)=W_1522))). % 42.42/27.49 tff(c_39332, plain, (![V_1563]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skf1(skc23), V_1563), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1563), true, V_1563, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_38235, plain, (![X_1505, V_1506]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, X_1505, V_1506), true, ifeq3(agent(skc14, X_1505, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, X_1505), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.49 tff(c_39149, plain, (![W_1547, V_1549]: (ifeq3(theme(skc14, skc17, W_1547), true, ifeq3(theme(skc14, skf1(skc23), V_1549), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1547), true, ifeq3(proposition(skc14, V_1549), true, V_1549, W_1547), W_1547), W_1547), W_1547), W_1547), W_1547)=W_1547))). % 42.42/27.49 tff(c_39261, plain, (![W_1557]: (ifeq3(theme(skc14, skf1(skc19), W_1557), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1557), true, skc14, W_1557), W_1557), W_1557), W_1557), W_1557)=W_1557))). % 42.42/27.49 tff(c_38447, plain, (![W_1513, X_1514]: (ifeq3(theme(skc14, skf1(skc19), W_1513), true, ifeq3(theme(skc14, X_1514, skc14), true, ifeq3(agent(skc14, X_1514, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1514), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.49 tff(c_39160, plain, (![W_1547, V_1549, Z_1550]: (ifeq3(theme(skc14, skc17, W_1547), true, ifeq3(theme(skc14, skc17, V_1549), true, ifeq3(agent(skc14, skc17, Z_1550), true, ifeq3(agent(skc14, skc17, Z_1550), true, ifeq3(proposition(skc14, W_1547), true, ifeq3(proposition(skc14, V_1549), true, V_1549, W_1547), W_1547), W_1547), W_1547), W_1547), W_1547)=W_1547))). % 42.42/27.49 tff(c_39159, plain, (![W_1547, V_1549, Z_1550]: (ifeq3(theme(skc14, skc17, W_1547), true, ifeq3(theme(skc14, skc15, V_1549), true, ifeq3(agent(skc14, skc17, Z_1550), true, ifeq3(agent(skc14, skc15, Z_1550), true, ifeq3(proposition(skc14, W_1547), true, ifeq3(proposition(skc14, V_1549), true, V_1549, W_1547), W_1547), W_1547), W_1547), W_1547), W_1547)=W_1547))). % 42.42/27.49 tff(c_5620, plain, (![W_185, X_188, V_190, Z_187]: (ifeq3(theme(skc14, skc17, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc17, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_29001, plain, (![W_406, V_405]: (ifeq3(theme(skc14, skf1(skc23), W_406), true, ifeq3(theme(skc14, skc26, V_405), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_406), true, ifeq3(proposition(skc14, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.42/27.50 tff(c_39045, plain, (![W_1541]: (ifeq3(theme(skc14, skc17, W_1541), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1541), true, skc14, W_1541), W_1541), W_1541), W_1541), W_1541)=W_1541))). % 42.42/27.50 tff(c_38460, plain, (![W_1513, X_1514, Z_1515]: (ifeq3(theme(skc14, skc17, W_1513), true, ifeq3(theme(skc14, X_1514, skc14), true, ifeq3(agent(skc14, skc17, Z_1515), true, ifeq3(agent(skc14, X_1514, Z_1515), true, ifeq3(think_believe_consider(skc14, X_1514), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.50 tff(c_38709, plain, (![W_1522, V_1524, Z_1525]: (ifeq3(theme(skc14, skc15, W_1522), true, ifeq3(theme(skc14, skc15, V_1524), true, ifeq3(agent(skc14, skc15, Z_1525), true, ifeq3(agent(skc14, skc15, Z_1525), true, ifeq3(proposition(skc14, W_1522), true, ifeq3(proposition(skc14, V_1524), true, V_1524, W_1522), W_1522), W_1522), W_1522), W_1522), W_1522)=W_1522))). % 42.42/27.50 tff(c_38710, plain, (![W_1522, V_1524, Z_1525]: (ifeq3(theme(skc14, skc15, W_1522), true, ifeq3(theme(skc14, skc17, V_1524), true, ifeq3(agent(skc14, skc15, Z_1525), true, ifeq3(agent(skc14, skc17, Z_1525), true, ifeq3(proposition(skc14, W_1522), true, ifeq3(proposition(skc14, V_1524), true, V_1524, W_1522), W_1522), W_1522), W_1522), W_1522), W_1522)=W_1522))). % 42.42/27.50 tff(c_38873, plain, (![W_1531]: (ifeq3(theme(skc14, skc15, W_1531), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1531), true, skc14, W_1531), W_1531), W_1531), W_1531), W_1531)=W_1531))). % 42.42/27.50 tff(c_38458, plain, (![W_1513, X_1514, Z_1515]: (ifeq3(theme(skc14, skc15, W_1513), true, ifeq3(theme(skc14, X_1514, skc14), true, ifeq3(agent(skc14, skc15, Z_1515), true, ifeq3(agent(skc14, X_1514, Z_1515), true, ifeq3(think_believe_consider(skc14, X_1514), true, ifeq3(proposition(skc14, W_1513), true, skc14, W_1513), W_1513), W_1513), W_1513), W_1513), W_1513)=W_1513))). % 42.42/27.50 tff(c_38780, plain, (![V_1528]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skc17, V_1528), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1528), true, V_1528, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38251, plain, (![Y_1504, V_1506, Z_1507]: (ifeq3(theme(skc14, Y_1504, skc14), true, ifeq3(theme(skc14, skc17, V_1506), true, ifeq3(agent(skc14, Y_1504, Z_1507), true, ifeq3(agent(skc14, skc17, Z_1507), true, ifeq3(think_believe_consider(skc14, Y_1504), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38638, plain, (![V_1520]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skc15, V_1520), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1520), true, V_1520, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38650, plain, (![W_185, X_188, V_190, Z_187]: (ifeq3(theme(skc14, skc15, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_38249, plain, (![Y_1504, V_1506, Z_1507]: (ifeq3(theme(skc14, Y_1504, skc14), true, ifeq3(theme(skc14, skc15, V_1506), true, ifeq3(agent(skc14, Y_1504, Z_1507), true, ifeq3(agent(skc14, skc15, Z_1507), true, ifeq3(think_believe_consider(skc14, Y_1504), true, ifeq3(proposition(skc14, V_1506), true, V_1506, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38318, plain, (![Y_1508]: (ifeq3(theme(skc14, Y_1508, skc14), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(agent(skc14, Y_1508, skc19), true, ifeq3(think_believe_consider(skc14, Y_1508), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38316, plain, (![Y_1508]: (ifeq3(theme(skc14, Y_1508, skc14), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, Y_1508, skc23), true, ifeq3(think_believe_consider(skc14, Y_1508), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38492, plain, (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 42.42/27.50 tff(c_38317, plain, (![X_1509]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, X_1509, skc14), true, ifeq3(agent(skc14, X_1509, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1509), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38368, plain, (![Y_189, W_185, X_188, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, X_188, skc14), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, skc14, W_185), W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_38358, plain, (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 42.42/27.50 tff(c_38315, plain, (![X_1509]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, X_1509, skc14), true, ifeq3(agent(skc14, X_1509, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, X_1509), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38247, plain, (![Y_1504, X_1505, Z_1507]: (ifeq3(theme(skc14, Y_1504, skc14), true, ifeq3(theme(skc14, X_1505, skc14), true, ifeq3(agent(skc14, Y_1504, Z_1507), true, ifeq3(agent(skc14, X_1505, Z_1507), true, ifeq3(think_believe_consider(skc14, Y_1504), true, ifeq3(think_believe_consider(skc14, X_1505), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_38170, plain, (![Y_189, X_188, V_190, Z_187]: (ifeq3(theme(skc14, Y_189, skc14), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, V_190), true, V_190, skc14), skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_29000, plain, (![W_406, V_405]: (ifeq3(theme(skc14, skc26, W_406), true, ifeq3(theme(skc14, skf1(skc23), V_405), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_406), true, ifeq3(proposition(skc14, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.42/27.50 tff(c_27117, plain, (![W_956, V_958, Z_959]: (ifeq3(theme(skc13, skc17, W_956), true, ifeq3(theme(skc13, skc17, V_958), true, ifeq3(agent(skc13, skc17, Z_959), true, ifeq3(agent(skc13, skc17, Z_959), true, ifeq3(proposition(skc13, W_956), true, ifeq3(proposition(skc13, V_958), true, V_958, W_956), W_956), W_956), W_956), W_956), W_956)=W_956))). % 42.42/27.50 tff(c_26939, plain, (![W_947, V_948, Z_949]: (ifeq3(theme(skc13, skc15, W_947), true, ifeq3(theme(skc13, skc15, V_948), true, ifeq3(agent(skc13, skc15, Z_949), true, ifeq3(agent(skc13, skc15, Z_949), true, ifeq3(proposition(skc13, W_947), true, ifeq3(proposition(skc13, V_948), true, V_948, W_947), W_947), W_947), W_947), W_947), W_947)=W_947))). % 42.42/27.50 tff(c_37999, plain, (![Y_1000, V_1002, Z_1003]: (ifeq3(theme(skc13, Y_1000, skc14), true, ifeq3(theme(skc13, skc15, V_1002), true, ifeq3(agent(skc13, Y_1000, Z_1003), true, ifeq3(agent(skc13, skc15, Z_1003), true, ifeq3(think_believe_consider(skc13, Y_1000), true, ifeq3(proposition(skc13, V_1002), true, V_1002, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_26938, plain, (![W_947, V_948, Z_949]: (ifeq3(theme(skc13, skc17, W_947), true, ifeq3(theme(skc13, skc15, V_948), true, ifeq3(agent(skc13, skc17, Z_949), true, ifeq3(agent(skc13, skc15, Z_949), true, ifeq3(proposition(skc13, W_947), true, ifeq3(proposition(skc13, V_948), true, V_948, W_947), W_947), W_947), W_947), W_947), W_947)=W_947))). % 42.42/27.50 tff(c_37934, plain, (![V_1488]: (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skc26, V_1488), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_1488), true, V_1488, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_37877, plain, (![Y_929, V_931]: (ifeq3(theme(skc14, Y_929, skc14), true, ifeq3(theme(skc14, skc26, V_931), true, ifeq3(agent(skc14, Y_929, skc23), true, ifeq3(think_believe_consider(skc14, Y_929), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_931), true, V_931, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_26570, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc17, W_930), true, ifeq3(theme(skc14, skc26, V_931), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_930), true, ifeq3(proposition(skc14, V_931), true, V_931, W_930), W_930), W_930), W_930), W_930), W_930)=W_930))). % 42.42/27.50 tff(c_37822, plain, (![W_1482]: (ifeq3(theme(skc14, skc26, W_1482), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1482), true, skc14, W_1482), W_1482), W_1482), W_1482), W_1482)=W_1482))). % 42.42/27.50 tff(c_26725, plain, (![W_937, X_938]: (ifeq3(theme(skc14, skc26, W_937), true, ifeq3(theme(skc14, X_938, skc14), true, ifeq3(agent(skc14, X_938, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, X_938), true, ifeq3(proposition(skc14, W_937), true, skc14, W_937), W_937), W_937), W_937), W_937), W_937)=W_937))). % 42.42/27.50 tff(c_26726, plain, (![W_937, V_939]: (ifeq3(theme(skc14, skc26, W_937), true, ifeq3(theme(skc14, skc15, V_939), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_937), true, ifeq3(proposition(skc14, V_939), true, V_939, W_937), W_937), W_937), W_937), W_937), W_937)=W_937))). % 42.42/27.50 tff(c_37640, plain, (![W_1473, V_1474]: (ifeq3(theme(skc14, skf1(skc19), W_1473), true, ifeq3(theme(skc14, skc17, V_1474), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1473), true, ifeq3(proposition(skc14, V_1474), true, V_1474, W_1473), W_1473), W_1473), W_1473), W_1473)=W_1473))). % 42.42/27.50 tff(c_37704, plain, (![V_1476]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc17, V_1476), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1476), true, V_1476, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_37646, plain, (![Y_1472, V_1474]: (ifeq3(theme(skc14, Y_1472, skc14), true, ifeq3(theme(skc14, skc17, V_1474), true, ifeq3(agent(skc14, Y_1472, skc19), true, ifeq3(think_believe_consider(skc14, Y_1472), true, ifeq3(proposition(skc14, V_1474), true, V_1474, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_15046, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc17, V_190), true, ifeq3(agent(skc14, Y_189, skc19), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_27568, plain, (![W_992, V_994, Z_995]: (ifeq3(theme(skc13, skc15, W_992), true, ifeq3(theme(skc13, skc17, V_994), true, ifeq3(agent(skc13, skc15, Z_995), true, ifeq3(agent(skc13, skc17, Z_995), true, ifeq3(proposition(skc13, W_992), true, ifeq3(proposition(skc13, V_994), true, V_994, W_992), W_992), W_992), W_992), W_992), W_992)=W_992))). % 42.42/27.50 tff(c_26727, plain, (![W_937, V_939]: (ifeq3(theme(skc14, skc26, W_937), true, ifeq3(theme(skc14, skc17, V_939), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_937), true, ifeq3(proposition(skc14, V_939), true, V_939, W_937), W_937), W_937), W_937), W_937), W_937)=W_937))). % 42.42/27.50 tff(c_26569, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc15, W_930), true, ifeq3(theme(skc14, skc26, V_931), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_930), true, ifeq3(proposition(skc14, V_931), true, V_931, W_930), W_930), W_930), W_930), W_930), W_930)=W_930))). % 42.42/27.50 tff(c_37407, plain, (![W_1458, V_1459]: (ifeq3(theme(skc14, skf1(skc19), W_1458), true, ifeq3(theme(skc14, skc15, V_1459), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1458), true, ifeq3(proposition(skc14, V_1459), true, V_1459, W_1458), W_1458), W_1458), W_1458), W_1458)=W_1458))). % 42.42/27.50 tff(c_37471, plain, (![V_1461]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc15, V_1461), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1461), true, V_1461, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_37413, plain, (![Y_1457, V_1459]: (ifeq3(theme(skc14, Y_1457, skc14), true, ifeq3(theme(skc14, skc15, V_1459), true, ifeq3(agent(skc14, Y_1457, skc19), true, ifeq3(think_believe_consider(skc14, Y_1457), true, ifeq3(proposition(skc14, V_1459), true, V_1459, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_37357, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skc15, V_190), true, ifeq3(agent(skc14, Y_189, skc19), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_37135, plain, (![W_1442, V_1444]: (ifeq3(theme(skc14, skc17, W_1442), true, ifeq3(theme(skc14, skf1(skc19), V_1444), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1442), true, ifeq3(proposition(skc14, V_1444), true, V_1444, W_1442), W_1442), W_1442), W_1442), W_1442)=W_1442))). % 42.42/27.50 tff(c_37243, plain, (![W_1449]: (ifeq3(theme(skc14, skc17, W_1449), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1449), true, skc14, W_1449), W_1449), W_1449), W_1449)=W_1449))). % 42.42/27.50 tff(c_37252, plain, (![Y_965, X_966, Z_968]: (ifeq3(theme(skc13, Y_965, skc14), true, ifeq3(theme(skc13, X_966, skc14), true, ifeq3(agent(skc13, Y_965, Z_968), true, ifeq3(agent(skc13, X_966, Z_968), true, ifeq3(think_believe_consider(skc13, Y_965), true, ifeq3(think_believe_consider(skc13, X_966), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_37142, plain, (![W_1442, X_1443]: (ifeq3(theme(skc14, skc17, W_1442), true, ifeq3(theme(skc14, X_1443, skc14), true, ifeq3(agent(skc14, X_1443, skc19), true, ifeq3(think_believe_consider(skc14, X_1443), true, ifeq3(proposition(skc14, W_1442), true, skc14, W_1442), W_1442), W_1442), W_1442), W_1442)=W_1442))). % 42.42/27.50 tff(c_37140, plain, (![W_1442, V_1444]: (ifeq3(theme(skc14, skc17, W_1442), true, ifeq3(theme(skc14, skc15, V_1444), true, ifeq3(proposition(skc14, W_1442), true, ifeq3(proposition(skc14, V_1444), true, V_1444, W_1442), W_1442), W_1442), W_1442)=W_1442))). % 42.42/27.50 tff(c_37138, plain, (![W_1442, V_1444]: (ifeq3(theme(skc14, skc17, W_1442), true, ifeq3(theme(skc14, skc17, V_1444), true, ifeq3(proposition(skc14, W_1442), true, ifeq3(proposition(skc14, V_1444), true, V_1444, W_1442), W_1442), W_1442), W_1442)=W_1442))). % 42.42/27.50 tff(c_15045, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skc17, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc19), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.50 tff(c_36950, plain, (![V_1434]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skf1(skc23), V_1434), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1434), true, V_1434, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.50 tff(c_36955, plain, (![V_1434]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skc17, V_1434), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_1434), true, V_1434, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36954, plain, (![V_1434]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skc15, V_1434), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_1434), true, V_1434, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_27567, plain, (![W_992, X_993, Z_995]: (ifeq3(theme(skc13, skc15, W_992), true, ifeq3(theme(skc13, X_993, skc14), true, ifeq3(agent(skc13, skc15, Z_995), true, ifeq3(agent(skc13, X_993, Z_995), true, ifeq3(think_believe_consider(skc13, X_993), true, ifeq3(proposition(skc13, W_992), true, skc14, W_992), W_992), W_992), W_992), W_992), W_992)=W_992))). % 42.42/27.51 tff(c_36990, plain, (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 42.42/27.51 tff(c_36953, plain, (![X_1433]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, X_1433, skc14), true, ifeq3(agent(skc14, X_1433, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, X_1433), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_26724, plain, (![X_938, V_939]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, X_938, V_939), true, ifeq3(agent(skc14, X_938, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, X_938), true, ifeq3(proposition(skc14, V_939), true, V_939, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36597, plain, (![W_1416]: (ifeq3(theme(skc14, skf1(skc23), W_1416), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_1416), true, skc14, W_1416), W_1416), W_1416), W_1416), W_1416)=W_1416))). % 42.42/27.51 tff(c_36678, plain, (![W_1418, V_1420]: (ifeq3(theme(skc14, skc15, W_1418), true, ifeq3(theme(skc14, skf1(skc19), V_1420), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1418), true, ifeq3(proposition(skc14, V_1420), true, V_1420, W_1418), W_1418), W_1418), W_1418), W_1418)=W_1418))). % 42.42/27.51 tff(c_36601, plain, (![W_1416]: (ifeq3(theme(skc14, skc15, W_1416), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_1416), true, skc14, W_1416), W_1416), W_1416), W_1416), W_1416)=W_1416))). % 42.42/27.51 tff(c_36814, plain, (![W_1426]: (ifeq3(theme(skc14, skc15, W_1426), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1426), true, skc14, W_1426), W_1426), W_1426), W_1426)=W_1426))). % 42.42/27.51 tff(c_36685, plain, (![W_1418, X_1419]: (ifeq3(theme(skc14, skc15, W_1418), true, ifeq3(theme(skc14, X_1419, skc14), true, ifeq3(agent(skc14, X_1419, skc19), true, ifeq3(think_believe_consider(skc14, X_1419), true, ifeq3(proposition(skc14, W_1418), true, skc14, W_1418), W_1418), W_1418), W_1418), W_1418)=W_1418))). % 42.42/27.51 tff(c_36602, plain, (![W_1416]: (ifeq3(theme(skc14, skc17, W_1416), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_1416), true, skc14, W_1416), W_1416), W_1416), W_1416), W_1416)=W_1416))). % 42.42/27.51 tff(c_36683, plain, (![W_1418, V_1420]: (ifeq3(theme(skc14, skc15, W_1418), true, ifeq3(theme(skc14, skc15, V_1420), true, ifeq3(proposition(skc14, W_1418), true, ifeq3(proposition(skc14, V_1420), true, V_1420, W_1418), W_1418), W_1418), W_1418)=W_1418))). % 42.42/27.51 tff(c_36680, plain, (![W_1418, V_1420]: (ifeq3(theme(skc14, skc15, W_1418), true, ifeq3(theme(skc14, skc17, V_1420), true, ifeq3(proposition(skc14, W_1418), true, ifeq3(proposition(skc14, V_1420), true, V_1420, W_1418), W_1418), W_1418), W_1418)=W_1418))). % 42.42/27.51 tff(c_14722, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skc15, W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc19), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, W_185), true, ifeq3(proposition(skc14, V_190), true, V_190, W_185), W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.42/27.51 tff(c_36629, plain, (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(think_believe_consider(skc14, skc26), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 42.42/27.51 tff(c_36600, plain, (![Y_1415]: (ifeq3(theme(skc14, Y_1415, skc14), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, Y_1415, skc23), true, ifeq3(think_believe_consider(skc14, Y_1415), true, ifeq3(think_believe_consider(skc14, skc26), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_26568, plain, (![Y_929, W_930]: (ifeq3(theme(skc14, Y_929, W_930), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, Y_929, skc23), true, ifeq3(think_believe_consider(skc14, Y_929), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_930), true, skc14, W_930), W_930), W_930), W_930), W_930), W_930)=W_930))). % 42.42/27.51 tff(c_36353, plain, (![V_1403]: (ifeq3(theme(skc14, skf1(skc23), V_1403), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1403), true, V_1403, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36361, plain, (![V_1403, Z_1404]: (ifeq3(theme(skc14, skc15, V_1403), true, ifeq3(agent(skc14, skc15, Z_1404), true, ifeq3(agent(skc14, skc15, Z_1404), true, ifeq3(proposition(skc14, V_1403), true, V_1403, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36362, plain, (![V_1403, Z_1404]: (ifeq3(theme(skc14, skc17, V_1403), true, ifeq3(agent(skc14, skc15, Z_1404), true, ifeq3(agent(skc14, skc17, Z_1404), true, ifeq3(proposition(skc14, V_1403), true, V_1403, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36360, plain, (![X_1402, Z_1404]: (ifeq3(theme(skc14, X_1402, skc14), true, ifeq3(agent(skc14, skc15, Z_1404), true, ifeq3(agent(skc14, X_1402, Z_1404), true, ifeq3(think_believe_consider(skc14, X_1402), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_27116, plain, (![W_956, X_957, Z_959]: (ifeq3(theme(skc13, skc17, W_956), true, ifeq3(theme(skc13, X_957, skc14), true, ifeq3(agent(skc13, skc17, Z_959), true, ifeq3(agent(skc13, X_957, Z_959), true, ifeq3(think_believe_consider(skc13, X_957), true, ifeq3(proposition(skc13, W_956), true, skc14, W_956), W_956), W_956), W_956), W_956), W_956)=W_956))). % 42.42/27.51 tff(c_14975, plain, (![X_188, V_190, Z_187]: (ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, V_190), true, V_190, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_36055, plain, (![W_1387]: (ifeq3(theme(skc14, skf1(skc23), W_1387), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1387), true, skc14, W_1387), W_1387), W_1387), W_1387)=W_1387))). % 42.42/27.51 tff(c_35770, plain, (![W_1373]: (ifeq3(theme(skc14, skf1(skc23), W_1373), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373), W_1373), W_1373)=W_1373))). % 42.42/27.51 tff(c_36064, plain, (![W_1387, Z_1388]: (ifeq3(theme(skc14, skc17, W_1387), true, ifeq3(agent(skc14, skc17, Z_1388), true, ifeq3(agent(skc14, skc15, Z_1388), true, ifeq3(proposition(skc14, W_1387), true, skc14, W_1387), W_1387), W_1387), W_1387)=W_1387))). % 42.42/27.51 tff(c_36063, plain, (![W_1387, Z_1388]: (ifeq3(theme(skc14, skc15, W_1387), true, ifeq3(agent(skc14, skc15, Z_1388), true, ifeq3(agent(skc14, skc15, Z_1388), true, ifeq3(proposition(skc14, W_1387), true, skc14, W_1387), W_1387), W_1387), W_1387)=W_1387))). % 42.42/27.51 tff(c_36198, plain, (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, skc14, skc14), skc14), skc14)=skc14)). % 42.42/27.51 tff(c_36062, plain, (![Y_1386, Z_1388]: (ifeq3(theme(skc14, Y_1386, skc14), true, ifeq3(agent(skc14, Y_1386, Z_1388), true, ifeq3(agent(skc14, skc15, Z_1388), true, ifeq3(think_believe_consider(skc14, Y_1386), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_35777, plain, (![Y_1372, Z_1374]: (ifeq3(theme(skc14, Y_1372, skc14), true, ifeq3(agent(skc14, Y_1372, Z_1374), true, ifeq3(agent(skc14, skc17, Z_1374), true, ifeq3(think_believe_consider(skc14, Y_1372), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.42/27.51 tff(c_35778, plain, (![W_1373, Z_1374]: (ifeq3(theme(skc14, skc15, W_1373), true, ifeq3(agent(skc14, skc15, Z_1374), true, ifeq3(agent(skc14, skc17, Z_1374), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373), W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_36059, plain, (![Z_1388]: (ifeq3(agent(skc14, skc15, Z_1388), true, ifeq3(agent(skc14, skc15, Z_1388), true, skc14, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_36012, plain, (![Y_189, W_185, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc15, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, skc14, W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.63/27.51 tff(c_35779, plain, (![W_1373, Z_1374]: (ifeq3(theme(skc14, skc17, W_1373), true, ifeq3(agent(skc14, skc17, Z_1374), true, ifeq3(agent(skc14, skc17, Z_1374), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373), W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_35774, plain, (![Y_1372, W_1373]: (ifeq3(theme(skc14, Y_1372, W_1373), true, ifeq3(agent(skc14, Y_1372, skc19), true, ifeq3(think_believe_consider(skc14, Y_1372), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373), W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_35771, plain, (![W_1373]: (ifeq3(theme(skc14, skf1(skc19), W_1373), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_27872, plain, (![Y_1004, V_1006, Z_1007]: (ifeq3(theme(skc13, Y_1004, skc14), true, ifeq3(theme(skc13, skc17, V_1006), true, ifeq3(agent(skc13, Y_1004, Z_1007), true, ifeq3(agent(skc13, skc17, Z_1007), true, ifeq3(think_believe_consider(skc13, Y_1004), true, ifeq3(proposition(skc13, V_1006), true, V_1006, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35775, plain, (![Z_1374]: (ifeq3(agent(skc14, skc15, Z_1374), true, ifeq3(agent(skc14, skc17, Z_1374), true, skc14, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35776, plain, (![W_1373]: (ifeq3(theme(skc14, skc15, W_1373), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_35773, plain, (![W_1373]: (ifeq3(theme(skc14, skc17, W_1373), true, ifeq3(proposition(skc14, W_1373), true, skc14, W_1373), W_1373)=W_1373))). % 42.63/27.51 tff(c_35717, plain, (![Y_189, W_185, Z_187]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(agent(skc14, Y_189, Z_187), true, ifeq3(agent(skc14, skc17, Z_187), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(proposition(skc14, W_185), true, skc14, W_185), W_185), W_185), W_185), W_185)=W_185))). % 42.63/27.51 tff(c_35487, plain, (![V_1359]: (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skc26, V_1359), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_1359), true, V_1359, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35689, plain, (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skc26), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 42.63/27.51 tff(c_35488, plain, (![W_1358]: (ifeq3(theme(skc14, skc26, W_1358), true, ifeq3(theme(skc14, skc26, skc14), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_1358), true, skc14, W_1358), W_1358), W_1358), W_1358), W_1358)=W_1358))). % 42.63/27.51 tff(c_35390, plain, (![V_1351]: (ifeq3(theme(skc14, skf1(skc23), V_1351), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35398, plain, (![V_1351, Z_1352]: (ifeq3(theme(skc14, skc15, V_1351), true, ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(agent(skc14, skc15, Z_1352), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35628, plain, (ifeq3(theme(skc14, skf1(skc23), skc14), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skf1(skc23)), true, skc14, skc14), skc14), skc14)=skc14)). % 42.63/27.51 tff(c_35397, plain, (![X_1350, Z_1352]: (ifeq3(theme(skc14, X_1350, skc14), true, ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(agent(skc14, X_1350, Z_1352), true, ifeq3(think_believe_consider(skc14, X_1350), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35399, plain, (![V_1351, Z_1352]: (ifeq3(theme(skc14, skc17, V_1351), true, ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35529, plain, (![X_1360]: (ifeq3(theme(skc14, X_1360, skc14), true, ifeq3(agent(skc14, X_1360, skc19), true, ifeq3(think_believe_consider(skc14, X_1360), true, skc14, skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35393, plain, (![X_1350, V_1351]: (ifeq3(theme(skc14, X_1350, V_1351), true, ifeq3(agent(skc14, X_1350, skc19), true, ifeq3(think_believe_consider(skc14, X_1350), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35471, plain, (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14)=skc14)). % 42.63/27.51 tff(c_26571, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc26, W_930), true, ifeq3(theme(skc14, skc26, V_931), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_930), true, ifeq3(proposition(skc14, V_931), true, V_931, W_930), W_930), W_930), W_930), W_930), W_930)=W_930))). % 42.63/27.51 tff(c_35391, plain, (![V_1351]: (ifeq3(theme(skc14, skf1(skc19), V_1351), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35395, plain, (![Z_1352]: (ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(agent(skc14, skc15, Z_1352), true, skc14, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35392, plain, (![Z_1352]: (ifeq3(agent(skc14, skc17, Z_1352), true, ifeq3(agent(skc14, skc17, Z_1352), true, skc14, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35396, plain, (![V_1351]: (ifeq3(theme(skc14, skc15, V_1351), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35394, plain, (![V_1351]: (ifeq3(theme(skc14, skc17, V_1351), true, ifeq3(proposition(skc14, V_1351), true, V_1351, skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35349, plain, (![X_188, V_190, Z_187]: (ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, skc17, Z_187), true, ifeq3(agent(skc14, X_188, Z_187), true, ifeq3(think_believe_consider(skc14, X_188), true, ifeq3(proposition(skc14, V_190), true, V_190, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_27984, plain, (![X_410, V_405, Z_409]: (ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, skc17, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, V_405), true, V_405, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_27979, plain, (![Y_407, W_406, Z_409]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, skc17, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, skc14, W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.51 tff(c_35183, plain, (![W_922, X_923]: (ifeq3(theme(skc13, skc17, W_922), true, ifeq3(theme(skc13, X_923, skc14), true, ifeq3(agent(skc13, X_923, skc19), true, ifeq3(think_believe_consider(skc13, X_923), true, ifeq3(proposition(skc13, W_922), true, skc14, W_922), W_922), W_922), W_922), W_922)=W_922))). % 42.63/27.51 tff(c_35130, plain, (![Y_907, V_909]: (ifeq3(theme(skc13, Y_907, skc14), true, ifeq3(theme(skc13, skc17, V_909), true, ifeq3(agent(skc13, Y_907, skc19), true, ifeq3(think_believe_consider(skc13, Y_907), true, ifeq3(proposition(skc13, V_909), true, V_909, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_35069, plain, (![Y_1000, V_1002]: (ifeq3(theme(skc13, Y_1000, skc14), true, ifeq3(theme(skc13, skc15, V_1002), true, ifeq3(agent(skc13, Y_1000, skc19), true, ifeq3(think_believe_consider(skc13, Y_1000), true, ifeq3(proposition(skc13, V_1002), true, V_1002, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_25988, plain, (![W_900, X_901]: (ifeq3(theme(skc13, skc15, W_900), true, ifeq3(theme(skc13, X_901, skc14), true, ifeq3(agent(skc13, X_901, skc19), true, ifeq3(think_believe_consider(skc13, X_901), true, ifeq3(proposition(skc13, W_900), true, skc14, W_900), W_900), W_900), W_900), W_900)=W_900))). % 42.63/27.51 tff(c_25403, plain, (![V_870, Z_871]: (ifeq3(theme(skc13, skc15, V_870), true, ifeq3(agent(skc13, skc15, Z_871), true, ifeq3(agent(skc13, skc15, Z_871), true, ifeq3(proposition(skc13, V_870), true, V_870, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_27866, plain, (![V_1006, Z_1007]: (ifeq3(theme(skc13, skc17, V_1006), true, ifeq3(agent(skc13, skc15, Z_1007), true, ifeq3(agent(skc13, skc17, Z_1007), true, ifeq3(proposition(skc13, V_1006), true, V_1006, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_34918, plain, (![V_880, Z_881]: (ifeq3(theme(skc13, skc15, V_880), true, ifeq3(agent(skc13, skc17, Z_881), true, ifeq3(agent(skc13, skc15, Z_881), true, ifeq3(proposition(skc13, V_880), true, V_880, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_34880, plain, (![V_880, Z_881]: (ifeq3(theme(skc13, skc17, V_880), true, ifeq3(agent(skc13, skc17, Z_881), true, ifeq3(agent(skc13, skc17, Z_881), true, ifeq3(proposition(skc13, V_880), true, V_880, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_25200, plain, (![W_860, Z_861]: (ifeq3(theme(skc13, skc17, W_860), true, ifeq3(agent(skc13, skc17, Z_861), true, ifeq3(agent(skc13, skc15, Z_861), true, ifeq3(proposition(skc13, W_860), true, skc14, W_860), W_860), W_860), W_860)=W_860))). % 42.63/27.51 tff(c_25199, plain, (![Y_859, Z_861]: (ifeq3(theme(skc13, Y_859, skc14), true, ifeq3(agent(skc13, Y_859, Z_861), true, ifeq3(agent(skc13, skc15, Z_861), true, ifeq3(think_believe_consider(skc13, Y_859), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_34766, plain, (![X_998, Z_999]: (ifeq3(theme(skc13, X_998, skc14), true, ifeq3(agent(skc13, skc17, Z_999), true, ifeq3(agent(skc13, X_998, Z_999), true, ifeq3(think_believe_consider(skc13, X_998), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_25401, plain, (![X_869, Z_871]: (ifeq3(theme(skc13, X_869, skc14), true, ifeq3(agent(skc13, skc15, Z_871), true, ifeq3(agent(skc13, X_869, Z_871), true, ifeq3(think_believe_consider(skc13, X_869), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.51 tff(c_34705, plain, (![W_890, Z_891]: (ifeq3(theme(skc13, skc15, W_890), true, ifeq3(agent(skc13, skc15, Z_891), true, ifeq3(agent(skc13, skc17, Z_891), true, ifeq3(proposition(skc13, W_890), true, skc14, W_890), W_890), W_890), W_890)=W_890))). % 42.63/27.52 tff(c_34669, plain, (![W_182, V_184]: (ifeq3(of(skc14, W_182, skc23), true, ifeq3(of(skc14, V_184, skc23), true, ifeq3(forename(skc14, W_182), true, ifeq3(forename(skc14, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 42.63/27.52 tff(c_34635, plain, (![W_182, V_184]: (ifeq3(of(skc14, W_182, skc19), true, ifeq3(of(skc14, V_184, skc19), true, ifeq3(forename(skc14, W_182), true, ifeq3(forename(skc14, V_184), true, W_182, V_184), V_184), V_184), V_184)=V_184))). % 42.63/27.52 tff(c_27560, plain, (![W_992, Z_995]: (ifeq3(theme(skc13, skc15, W_992), true, ifeq3(agent(skc13, skc15, Z_995), true, ifeq3(agent(skc13, skc15, Z_995), true, ifeq3(proposition(skc13, W_992), true, skc14, W_992), W_992), W_992), W_992)=W_992))). % 42.63/27.52 tff(c_4203, plain, (![W_402, V_404]: (ifeq3(of(skc13, W_402, skc23), true, ifeq3(of(skc13, V_404, skc23), true, ifeq3(forename(skc13, W_402), true, ifeq3(forename(skc13, V_404), true, W_402, V_404), V_404), V_404), V_404)=V_404))). % 42.63/27.52 tff(c_4204, plain, (![W_402, V_404]: (ifeq3(of(skc13, W_402, skc19), true, ifeq3(of(skc13, V_404, skc19), true, ifeq3(forename(skc13, W_402), true, ifeq3(forename(skc13, V_404), true, W_402, V_404), V_404), V_404), V_404)=V_404))). % 42.63/27.52 tff(c_34500, plain, (![V_1306]: (ifeq3(of(skc14, skc24, skc19), true, ifeq3(of(skc14, V_1306, skc19), true, ifeq3(forename(skc14, V_1306), true, skc24, V_1306), V_1306), V_1306)=V_1306))). % 42.63/27.52 tff(c_34455, plain, (![X_183, V_184]: (ifeq3(of(skc14, skc24, X_183), true, ifeq3(of(skc14, V_184, X_183), true, ifeq3(forename(skc14, V_184), true, ifeq3(entity(skc14, X_183), true, skc24, V_184), V_184), V_184), V_184)=V_184))). % 42.63/27.52 tff(c_34345, plain, (![V_1300]: (ifeq3(of(skc14, skc18, skc23), true, ifeq3(of(skc14, V_1300, skc23), true, ifeq3(forename(skc14, V_1300), true, skc18, V_1300), V_1300), V_1300)=V_1300))). % 42.63/27.52 tff(c_34298, plain, (![W_1297]: (ifeq3(of(skc14, W_1297, skc19), true, ifeq3(of(skc14, skc24, skc19), true, ifeq3(forename(skc14, W_1297), true, W_1297, skc24), skc24), skc24)=skc24))). % 42.63/27.52 tff(c_34300, plain, (![X_1298]: (ifeq3(of(skc14, skc18, X_1298), true, ifeq3(of(skc14, skc24, X_1298), true, ifeq3(entity(skc14, X_1298), true, skc18, skc24), skc24), skc24)=skc24))). % 42.63/27.52 tff(c_34371, plain, (ifeq3(of(skc14, skc24, skc19), true, ifeq3(of(skc14, skc24, skc19), true, skc24, skc24), skc24)=skc24)). % 42.63/27.52 tff(c_34299, plain, (![X_1298]: (ifeq3(of(skc14, skc24, X_1298), true, ifeq3(of(skc14, skc24, X_1298), true, ifeq3(entity(skc14, X_1298), true, skc24, skc24), skc24), skc24)=skc24))). % 42.63/27.52 tff(c_34301, plain, (![X_183, V_184]: (ifeq3(of(skc14, skc18, X_183), true, ifeq3(of(skc14, V_184, X_183), true, ifeq3(forename(skc14, V_184), true, ifeq3(entity(skc14, X_183), true, skc18, V_184), V_184), V_184), V_184)=V_184))). % 42.63/27.52 tff(c_34265, plain, (![W_182, X_183]: (ifeq3(of(skc14, W_182, X_183), true, ifeq3(of(skc14, skc24, X_183), true, ifeq3(forename(skc14, W_182), true, ifeq3(entity(skc14, X_183), true, W_182, skc24), skc24), skc24), skc24)=skc24))). % 42.63/27.52 tff(c_34227, plain, (![Y_889, Z_891]: (ifeq3(theme(skc13, Y_889, skc14), true, ifeq3(agent(skc13, Y_889, Z_891), true, ifeq3(agent(skc13, skc17, Z_891), true, ifeq3(think_believe_consider(skc13, Y_889), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.52 tff(c_28601, plain, (![W_406]: (ifeq3(theme(skc14, skc26, W_406), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_406), true, skc14, W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.52 tff(c_34131, plain, (![W_1289]: (ifeq3(of(skc14, W_1289, skc23), true, ifeq3(of(skc14, skc18, skc23), true, ifeq3(forename(skc14, W_1289), true, W_1289, skc18), skc18), skc18)=skc18))). % 42.63/27.52 tff(c_34179, plain, (ifeq3(of(skc14, skc18, skc23), true, ifeq3(of(skc14, skc18, skc23), true, skc18, skc18), skc18)=skc18)). % 42.63/27.52 tff(c_34134, plain, (![X_1290]: (ifeq3(of(skc14, skc18, X_1290), true, ifeq3(of(skc14, skc18, X_1290), true, ifeq3(entity(skc14, X_1290), true, skc18, skc18), skc18), skc18)=skc18))). % 42.63/27.52 tff(c_34133, plain, (![X_1290]: (ifeq3(of(skc14, skc24, X_1290), true, ifeq3(of(skc14, skc18, X_1290), true, ifeq3(entity(skc14, X_1290), true, skc24, skc18), skc18), skc18)=skc18))). % 42.63/27.52 tff(c_34099, plain, (![W_182, X_183]: (ifeq3(of(skc14, W_182, X_183), true, ifeq3(of(skc14, skc18, X_183), true, ifeq3(forename(skc14, W_182), true, ifeq3(entity(skc14, X_183), true, W_182, skc18), skc18), skc18), skc18)=skc18))). % 42.63/27.52 tff(c_26563, plain, (![V_931]: (ifeq3(theme(skc14, skc26, V_931), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_931), true, V_931, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.52 tff(c_34046, plain, (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, skc14, skc14), skc14), skc14)=skc14)). % 42.63/27.52 tff(c_34047, plain, (![W_890, Z_891]: (ifeq3(theme(skc13, skc17, W_890), true, ifeq3(agent(skc13, skc17, Z_891), true, ifeq3(agent(skc13, skc17, Z_891), true, ifeq3(proposition(skc13, W_890), true, skc14, W_890), W_890), W_890), W_890)=W_890))). % 42.63/27.52 tff(c_26720, plain, (![W_937]: (ifeq3(theme(skc14, skc26, W_937), true, ifeq3(agent(skc14, skc15, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_937), true, skc14, W_937), W_937), W_937), W_937)=W_937))). % 42.63/27.52 tff(c_34029, plain, (ifeq3(theme(skc14, skc26, skc14), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, skc14, skc14), skc14), skc14)=skc14)). % 42.63/27.52 tff(c_34018, plain, (![V_931]: (ifeq3(theme(skc14, skc26, V_931), true, ifeq3(agent(skc14, skc17, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, V_931), true, V_931, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.52 tff(c_24473, plain, (![W_830]: (ifeq3(of(skc13, W_830, skc19), true, ifeq3(of(skc13, skc24, skc19), true, ifeq3(forename(skc13, W_830), true, W_830, skc24), skc24), skc24)=skc24))). % 42.63/27.52 tff(c_24288, plain, (![W_821]: (ifeq3(of(skc13, W_821, skc23), true, ifeq3(of(skc13, skc18, skc23), true, ifeq3(forename(skc13, W_821), true, W_821, skc18), skc18), skc18)=skc18))). % 42.63/27.52 tff(c_33925, plain, (![V_814]: (ifeq3(of(skc13, skc18, skc23), true, ifeq3(of(skc13, V_814, skc23), true, ifeq3(forename(skc13, V_814), true, skc18, V_814), V_814), V_814)=V_814))). % 42.63/27.52 tff(c_23611, plain, (![V_801]: (ifeq3(of(skc13, skc24, skc19), true, ifeq3(of(skc13, V_801, skc19), true, ifeq3(forename(skc13, V_801), true, skc24, V_801), V_801), V_801)=V_801))). % 42.63/27.52 tff(c_32235, plain, (![X_1195]: (ifeq3(theme(skc13, X_1195, skc14), true, ifeq3(agent(skc13, X_1195, skc19), true, ifeq3(think_believe_consider(skc13, X_1195), true, skc14, skc14), skc14), skc14)=skc14))). % 42.63/27.52 tff(c_30548, plain, (ifeq3(of(skc13, skc18, skc23), true, ifeq3(of(skc13, skc18, skc23), true, skc18, skc18), skc18)=skc18)). % 42.63/27.52 tff(c_30695, plain, (ifeq3(of(skc13, skc24, skc19), true, ifeq3(of(skc13, skc24, skc19), true, skc24, skc24), skc24)=skc24)). % 42.63/27.52 tff(c_33838, plain, (![U_164]: (ifeq2(agent(U_164, skf1(skc23), skc23), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33818, plain, (![U_164]: (ifeq2(agent(U_164, skf1(skc19), skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33802, plain, (![V_167]: (ifeq2(accessible_world(skc14, V_167), true, agent(V_167, skf1(skc19), skc19), true)=true))). % 42.63/27.52 tff(c_33772, plain, (![V_1274]: (ifeq2(accessible_world(skc14, V_1274), true, agent(V_1274, skf1(skc23), skc23), true)=true))). % 42.63/27.52 tff(c_33742, plain, (![V_180]: (ifeq2(accessible_world(skc14, V_180), true, be(V_180, skc22, skc23, skc23), true)=true))). % 42.63/27.52 tff(c_33718, plain, (![U_177]: (ifeq2(be(U_177, skc22, skc23, skc23), true, ifeq2(accessible_world(U_177, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33697, plain, (![U_86, V_538]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skf1(V_538)), true, true, true), true)=true))). % 42.63/27.52 tff(c_28830, plain, (![U_95, V_1014]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skf1(V_1014)), true, true, true), true)=true))). % 42.63/27.52 tff(c_28858, plain, (![U_92, V_1015]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skf1(V_1015)), true, true, true), true)=true))). % 42.63/27.52 tff(c_33617, plain, (ifeq3(of(skc14, skc24, skc19), true, skc24, skc18)=skc18)). % 42.63/27.52 tff(c_28883, plain, (![U_83, V_1016]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skf1(V_1016)), true, true, true), true)=true))). % 42.63/27.52 tff(c_33589, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc19), true, ifeq3(forename(skc14, W_182), true, W_182, skc18), skc18)=skc18))). % 42.63/27.52 tff(c_33582, plain, (ifeq3(of(skc14, skc18, skc23), true, skc24, skc18)=skc18)). % 42.63/27.52 tff(c_33551, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc23), true, ifeq3(forename(skc14, V_184), true, skc24, V_184), V_184)=V_184))). % 42.63/27.52 tff(c_33545, plain, (ifeq3(of(skc14, skc24, skc19), true, skc18, skc24)=skc24)). % 42.63/27.52 tff(c_33525, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc19), true, ifeq3(forename(skc14, V_184), true, skc18, V_184), V_184)=V_184))). % 42.63/27.52 tff(c_33520, plain, (ifeq3(of(skc14, skc18, skc23), true, skc18, skc24)=skc24)). % 42.63/27.52 tff(c_33501, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc23), true, ifeq3(forename(skc14, W_182), true, W_182, skc24), skc24)=skc24))). % 42.63/27.52 tff(c_33481, plain, (![U_89, V_530]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skf1(V_530)), true, true, true), true)=true))). % 42.63/27.52 tff(c_33452, plain, (![U_80, V_526]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skf1(V_526)), true, true, true), true)=true))). % 42.63/27.52 tff(c_28739, plain, (![U_74, V_1010]: (ifeq2(accessible_world(U_74, skc14), true, ifeq2(smoke(U_74, skf1(V_1010)), true, true, true), true)=true))). % 42.63/27.52 tff(c_23614, plain, (![V_801]: (ifeq3(of(skc13, V_801, skc23), true, ifeq3(forename(skc13, V_801), true, skc24, V_801), V_801)=V_801))). % 42.63/27.52 tff(c_33370, plain, (![U_98, V_521]: (ifeq2(present(U_98, skf1(V_521)), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_24895, plain, (![V_849]: (ifeq3(of(skc13, V_849, skc19), true, ifeq3(forename(skc13, V_849), true, skc18, V_849), V_849)=V_849))). % 42.63/27.52 tff(c_4210, plain, (![W_402]: (ifeq3(of(skc13, W_402, skc23), true, ifeq3(forename(skc13, W_402), true, W_402, skc24), skc24)=skc24))). % 42.63/27.52 tff(c_4212, plain, (![W_402]: (ifeq3(of(skc13, W_402, skc19), true, ifeq3(forename(skc13, W_402), true, W_402, skc18), skc18)=skc18))). % 42.63/27.52 tff(c_33270, plain, (![V_1244, V_1245]: (ifeq2(accessible_world(skc14, V_1244), true, present(V_1244, skf1(V_1245)), true)=true))). % 42.63/27.52 tff(c_28712, plain, (![U_77, V_1009]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skf1(V_1009)), true, true, true), true)=true))). % 42.63/27.52 tff(c_33209, plain, (![U_168]: (ifeq2(theme(U_168, skc15, skc14), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_28598, plain, (![U_168]: (ifeq2(theme(U_168, skc17, skc14), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33149, plain, (![U_172]: (ifeq2(of(U_172, skc18, skc19), true, ifeq2(accessible_world(U_172, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33109, plain, (![V_1237]: (ifeq2(accessible_world(skc14, V_1237), true, theme(V_1237, skc15, skc14), true)=true))). % 42.63/27.52 tff(c_33063, plain, (![V_1235]: (ifeq2(accessible_world(skc14, V_1235), true, agent(V_1235, skc15, skc19), true)=true))). % 42.63/27.52 tff(c_33032, plain, (![U_164]: (ifeq2(agent(U_164, skc17, skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_33008, plain, (![U_164]: (ifeq2(agent(U_164, skc15, skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_32970, plain, (![V_1231]: (ifeq2(accessible_world(skc14, V_1231), true, of(V_1231, skc24, skc23), true)=true))). % 42.63/27.52 tff(c_32945, plain, (![V_167]: (ifeq2(accessible_world(skc14, V_167), true, agent(V_167, skc17, skc19), true)=true))). % 42.63/27.52 tff(c_32925, plain, (![V_175]: (ifeq2(accessible_world(skc14, V_175), true, of(V_175, skc18, skc19), true)=true))). % 42.63/27.52 tff(c_32886, plain, (![V_1227]: (ifeq2(accessible_world(skc14, V_1227), true, theme(V_1227, skc17, skc14), true)=true))). % 42.63/27.52 tff(c_32857, plain, (![U_172]: (ifeq2(of(U_172, skc24, skc23), true, ifeq2(accessible_world(U_172, skc14), true, true, true), true)=true))). % 42.63/27.52 tff(c_28049, plain, (![U_392]: (ifeq2(theme(U_392, skc17, skc14), true, ifeq2(accessible_world(U_392, skc13), true, true, true), true)=true))). % 42.63/27.52 tff(c_14573, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc19), true, true, true), true)=true))). % 42.63/27.52 tff(c_14448, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc23), true, true, true), true)=true))). % 42.63/27.52 tff(c_32756, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc24), true, true, true), true)=true))). % 42.63/27.52 tff(c_32735, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc18), true, true, true), true)=true))). % 42.63/27.52 tff(c_13190, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc23), true, true, true), true)=true))). % 42.63/27.52 tff(c_12961, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc18), true, true, true), true)=true))). % 42.63/27.52 tff(c_12702, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc24), true, true, true), true)=true))). % 42.63/27.52 tff(c_13101, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc19), true, true, true), true)=true))). % 42.63/27.52 tff(c_12447, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(existent(U_134, skc19), true, true, true), true)=true))). % 42.63/27.52 tff(c_12469, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(existent(U_134, skc23), true, true, true), true)=true))). % 42.63/27.52 tff(c_32589, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(impartial(U_137, skc19), true, true, true), true)=true))). % 42.63/27.52 tff(c_32562, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc24), true, true, true), true)=true))). % 42.63/27.52 tff(c_11308, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc14), true, ifeq2(entity(U_131, skc23), true, true, true), true)=true))). % 42.63/27.52 tff(c_32522, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc19), true, true, true), true)=true))). % 42.63/27.52 tff(c_26435, plain, (![W_922, V_924]: (ifeq3(theme(skc13, skc17, W_922), true, ifeq3(theme(skc13, skc17, V_924), true, ifeq3(proposition(skc13, W_922), true, ifeq3(proposition(skc13, V_924), true, V_924, W_922), W_922), W_922), W_922)=W_922))). % 42.63/27.52 tff(c_32472, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_10048, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_32432, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_32411, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_32387, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_32367, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(impartial(U_137, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_32346, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_11753, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_32305, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc14), true, ifeq2(entity(U_131, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_32280, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_32260, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_32240, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_25981, plain, (![X_901, V_902]: (ifeq3(theme(skc13, X_901, V_902), true, ifeq3(agent(skc13, X_901, skc19), true, ifeq3(think_believe_consider(skc13, X_901), true, ifeq3(proposition(skc13, V_902), true, V_902, skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.53 tff(c_32172, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_32152, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_32132, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3647, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_26269, plain, (![W_915, V_916]: (ifeq3(theme(skc13, skc17, W_915), true, ifeq3(theme(skc13, skc15, V_916), true, ifeq3(proposition(skc13, W_915), true, ifeq3(proposition(skc13, V_916), true, V_916, W_915), W_915), W_915), W_915)=W_915))). % 42.63/27.53 tff(c_9958, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc13), true, ifeq2(existent(U_134, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_32055, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3828, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_32022, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc13), true, ifeq2(general(U_116, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_3971, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_25990, plain, (![W_900, V_902]: (ifeq3(theme(skc13, skc15, W_900), true, ifeq3(theme(skc13, skc15, V_902), true, ifeq3(proposition(skc13, W_900), true, ifeq3(proposition(skc13, V_902), true, V_902, W_900), W_900), W_900), W_900)=W_900))). % 42.63/27.53 tff(c_31966, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_31949, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc13), true, ifeq2(general(U_116, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3791, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_10126, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc13), true, ifeq2(specific(U_89, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_4388, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_31888, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3544, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc13), true, ifeq2(existent(U_134, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_9897, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc13), true, ifeq2(specific(U_89, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_31841, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_25984, plain, (![W_900, V_902]: (ifeq3(theme(skc13, skc15, W_900), true, ifeq3(theme(skc13, skc17, V_902), true, ifeq3(proposition(skc13, W_900), true, ifeq3(proposition(skc13, V_902), true, V_902, W_900), W_900), W_900), W_900)=W_900))). % 42.63/27.53 tff(c_7420, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_8455, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc14), true, ifeq2(animate(U_146, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_31748, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(living(U_140, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_31706, plain, (![Y_889, W_890]: (ifeq3(theme(skc13, Y_889, W_890), true, ifeq3(agent(skc13, Y_889, skc19), true, ifeq3(think_believe_consider(skc13, Y_889), true, ifeq3(proposition(skc13, W_890), true, skc14, W_890), W_890), W_890), W_890)=W_890))). % 42.63/27.53 tff(c_31686, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_9182, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(human(U_143, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_31643, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(human(U_143, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_31620, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_31600, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc14), true, ifeq2(animate(U_146, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_31580, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_7582, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_31535, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_31514, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_31494, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(organism(U_128, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_31473, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_31452, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_9244, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_31412, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_31391, plain, (![U_155]: (ifeq2(accessible_world(U_155, skc14), true, ifeq2(relname(U_155, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_8803, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_31351, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_31331, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_31308, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(living(U_140, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_7667, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_8172, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_31249, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_31228, plain, (![U_155]: (ifeq2(accessible_world(U_155, skc14), true, ifeq2(relname(U_155, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_31208, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_8213, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_31168, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_31148, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(organism(U_128, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_7860, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3577, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_3372, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc13), true, ifeq2(living(U_140, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_3519, plain, (![U_372]: (ifeq2(accessible_world(U_372, skc13), true, ifeq2(entity(U_372, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_31057, plain, (![X_813]: (ifeq3(of(skc13, skc18, X_813), true, ifeq3(of(skc13, skc24, X_813), true, ifeq3(entity(skc13, X_813), true, skc18, skc24), skc24), skc24)=skc24))). % 42.63/27.53 tff(c_3212, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_3595, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_2671, plain, (![U_330]: (ifeq2(accessible_world(U_330, skc13), true, ifeq2(general(U_330, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_3138, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_2379, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_3289, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc13), true, ifeq2(impartial(U_137, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_3525, plain, (![U_372]: (ifeq2(accessible_world(U_372, skc13), true, ifeq2(entity(U_372, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_30932, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_3192, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc13), true, ifeq2(living(U_140, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_2967, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc13), true, ifeq2(impartial(U_137, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_3583, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_3670, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_3589, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc14), true, ifeq2(singleton(U_375, skc26), true, true, true), true)=true))). % 42.63/27.53 tff(c_30825, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_23620, plain, (![X_800]: (ifeq3(of(skc13, skc24, X_800), true, ifeq3(of(skc13, skc18, X_800), true, ifeq3(entity(skc13, X_800), true, skc24, skc18), skc18), skc18)=skc18))). % 42.63/27.53 tff(c_30778, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_5261, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(human_person(U_125, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_5377, plain, (![U_149]: (ifeq2(accessible_world(U_149, skc14), true, ifeq2(male(U_149, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_5826, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_30698, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc22), true, true, true), true)=true))). % 42.63/27.53 tff(c_30674, plain, (![X_800]: (ifeq3(of(skc13, skc24, X_800), true, ifeq3(of(skc13, skc24, X_800), true, ifeq3(entity(skc13, X_800), true, skc24, skc24), skc24), skc24)=skc24))). % 42.63/27.53 tff(c_30652, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_30632, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(human_person(U_125, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_30611, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc14), true, true, true), true)=true))). % 42.63/27.53 tff(c_6235, plain, (![U_149]: (ifeq2(accessible_world(U_149, skc14), true, ifeq2(male(U_149, skc19), true, true, true), true)=true))). % 42.63/27.53 tff(c_30572, plain, (![U_152]: (ifeq2(accessible_world(U_152, skc14), true, ifeq2(forename(U_152, skc18), true, true, true), true)=true))). % 42.63/27.53 tff(c_30552, plain, (![U_152]: (ifeq2(accessible_world(U_152, skc14), true, ifeq2(forename(U_152, skc24), true, true, true), true)=true))). % 42.63/27.53 tff(c_30528, plain, (![X_813]: (ifeq3(of(skc13, skc18, X_813), true, ifeq3(of(skc13, skc18, X_813), true, ifeq3(entity(skc13, X_813), true, skc18, skc18), skc18), skc18)=skc18))). % 42.63/27.53 tff(c_2562, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc17), true, true, true), true)=true))). % 42.63/27.53 tff(c_2901, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc15), true, true, true), true)=true))). % 42.63/27.53 tff(c_2314, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc13), true, ifeq2(animate(U_312, skc23), true, true, true), true)=true))). % 42.63/27.53 tff(c_2182, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc14), true, ifeq2(unisex(U_306, skc26), true, true, true), true)=true))). % 42.63/27.54 tff(c_3224, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc14), true, ifeq2(thing(U_357, skc26), true, true, true), true)=true))). % 42.63/27.54 tff(c_2568, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_2842, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc13), true, ifeq2(organism(U_339, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_2550, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc14), true, ifeq2(nonexistent(U_324, skc26), true, true, true), true)=true))). % 42.63/27.54 tff(c_2188, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_3218, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc15), true, true, true), true)=true))). % 42.63/27.54 tff(c_2194, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc15), true, true, true), true)=true))). % 42.63/27.54 tff(c_2907, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_2889, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc17), true, true, true), true)=true))). % 42.63/27.54 tff(c_2556, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc15), true, true, true), true)=true))). % 42.63/27.54 tff(c_2734, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc13), true, ifeq2(human(U_333, skc23), true, true, true), true)=true))). % 42.63/27.54 tff(c_2308, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc13), true, ifeq2(animate(U_312, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_2176, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc17), true, true, true), true)=true))). % 42.63/27.54 tff(c_2895, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc14), true, ifeq2(specific(U_342, skc26), true, true, true), true)=true))). % 42.63/27.54 tff(c_30221, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_30205, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc24), true, true, true), true)=true))). % 42.63/27.54 tff(c_30189, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc18), true, true, true), true)=true))). % 42.63/27.54 tff(c_2836, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc13), true, ifeq2(organism(U_339, skc23), true, true, true), true)=true))). % 42.63/27.54 tff(c_2728, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc13), true, ifeq2(human(U_333, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_3230, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc17), true, true, true), true)=true))). % 42.63/27.54 tff(c_3236, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_5216, plain, (![U_98]: (ifeq2(present(U_98, skc17), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_30075, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc17), true, true, true), true)=true))). % 42.63/27.54 tff(c_30052, plain, (![V_103]: (ifeq2(accessible_world(skc14, V_103), true, think_believe_consider(V_103, skc17), true)=true))). % 42.63/27.54 tff(c_30031, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc14), true, ifeq2(proposition(U_104, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_30015, plain, (![Z_881]: (ifeq3(agent(skc13, skc17, Z_881), true, ifeq3(agent(skc13, skc15, Z_881), true, skc14, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_29983, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(man(U_122, skc23), true, true, true), true)=true))). % 42.63/27.54 tff(c_29958, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(man(U_122, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_29942, plain, (![Z_881]: (ifeq3(agent(skc13, skc17, Z_881), true, ifeq3(agent(skc13, skc17, Z_881), true, skc14, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_6617, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc14), true, ifeq2(state(U_119, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_29884, plain, (![V_1070]: (ifeq2(accessible_world(skc14, V_1070), true, present(V_1070, skc17), true)=true))). % 42.63/27.54 tff(c_29854, plain, (![U_101]: (ifeq2(think_believe_consider(U_101, skc15), true, ifeq2(accessible_world(U_101, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_5616, plain, (![U_101]: (ifeq2(think_believe_consider(U_101, skc17), true, ifeq2(accessible_world(U_101, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_4485, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc15), true, true, true), true)=true))). % 42.63/27.54 tff(c_25194, plain, (![Z_861]: (ifeq3(agent(skc13, skc15, Z_861), true, ifeq3(agent(skc13, skc15, Z_861), true, skc14, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_29777, plain, (![V_100]: (ifeq2(accessible_world(skc14, V_100), true, present(V_100, skc15), true)=true))). % 42.63/27.54 tff(c_5189, plain, (![U_98]: (ifeq2(present(U_98, skc15), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_29734, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc14), true, ifeq2(jules_forename(U_161, skc24), true, true, true), true)=true))). % 42.63/27.54 tff(c_29714, plain, (![U_158]: (ifeq2(accessible_world(U_158, skc14), true, ifeq2(vincent_forename(U_158, skc18), true, true, true), true)=true))). % 42.63/27.54 tff(c_29676, plain, (![V_1060]: (ifeq2(accessible_world(skc14, V_1060), true, think_believe_consider(V_1060, skc15), true)=true))). % 42.63/27.54 tff(c_3079, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc13), true, ifeq2(human_person(U_351, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_2250, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_29625, plain, (![Z_891]: (ifeq3(agent(skc13, skc15, Z_891), true, ifeq3(agent(skc13, skc17, Z_891), true, skc14, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_3762, plain, (![U_381]: (ifeq2(accessible_world(U_381, skc13), true, ifeq2(male(U_381, skc23), true, true, true), true)=true))). % 42.63/27.54 tff(c_2244, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc14), true, ifeq2(eventuality(U_309, skc26), true, true, true), true)=true))). % 42.63/27.54 tff(c_2232, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc15), true, true, true), true)=true))). % 42.63/27.54 tff(c_2106, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc13), true, ifeq2(relname(U_303, skc24), true, true, true), true)=true))). % 42.63/27.54 tff(c_2238, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc17), true, true, true), true)=true))). % 42.63/27.54 tff(c_3020, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc22), true, true, true), true)=true))). % 42.63/27.54 tff(c_3085, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc13), true, ifeq2(human_person(U_351, skc23), true, true, true), true)=true))). % 42.63/27.54 tff(c_3756, plain, (![U_381]: (ifeq2(accessible_world(U_381, skc13), true, ifeq2(male(U_381, skc19), true, true, true), true)=true))). % 42.63/27.54 tff(c_29481, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc13), true, ifeq2(relname(U_303, skc18), true, true, true), true)=true))). % 42.63/27.54 tff(c_29465, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc14), true, true, true), true)=true))). % 42.63/27.54 tff(c_29451, plain, (![V_530]: (ifeq(tuple(true, general(skc14, skf1(V_530))), tuple(true, true), a, b)=b))). % 42.63/27.54 tff(c_28861, plain, (![V_1015]: (ifeq(tuple(true, existent(skc14, skf1(V_1015))), tuple(true, true), a, b)=b))). % 42.63/27.54 tff(c_28833, plain, (![V_1014]: (ifeq(tuple(true, male(skc14, skf1(V_1014))), tuple(true, true), a, b)=b))). % 42.63/27.54 tff(c_29419, plain, (ifeq(tuple(true, general(skc14, skc23)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_12472, plain, (ifeq(tuple(nonexistent(skc14, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29401, plain, (ifeq(tuple(true, human(skc14, skc24)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29390, plain, (ifeq(tuple(true, general(skc14, skc19)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_26433, plain, (![W_922]: (ifeq3(theme(skc13, skc17, W_922), true, ifeq3(proposition(skc13, W_922), true, skc14, W_922), W_922)=W_922))). % 42.63/27.54 tff(c_10699, plain, (ifeq(tuple(specific(skc14, skc24), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_11756, plain, (ifeq(tuple(specific(skc14, skc18), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_12450, plain, (ifeq(tuple(nonexistent(skc14, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29337, plain, (ifeq(tuple(true, male(skc14, skc24)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29331, plain, (ifeq(tuple(true, male(skc14, skc18)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29326, plain, (ifeq(tuple(true, human(skc14, skc18)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9900, plain, (ifeq(tuple(true, general(skc13, skc19)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_3547, plain, (ifeq(tuple(nonexistent(skc13, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_10129, plain, (ifeq(tuple(true, general(skc13, skc23)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_4357, plain, (ifeq(tuple(true, male(skc13, skc18)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29299, plain, (ifeq(tuple(specific(skc13, skc18), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9961, plain, (ifeq(tuple(nonexistent(skc13, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_4242, plain, (ifeq(tuple(true, male(skc13, skc24)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29285, plain, (ifeq(tuple(true, human(skc13, skc18)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_3736, plain, (ifeq(tuple(specific(skc13, skc24), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29276, plain, (ifeq(tuple(true, human(skc13, skc24)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_27934, plain, (ifeq(tuple(true, male(skc14, skc14)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_29261, plain, (ifeq(tuple(specific(skc14, skc14), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_8216, plain, (ifeq(tuple(true, general(skc14, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9216, plain, (ifeq(tuple(true, existent(skc14, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_28951, plain, (![V_87, V_1018]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skf1(V_1018)), true)=true))). % 42.63/27.54 tff(c_28929, plain, (![V_90, V_1017]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skf1(V_1017)), true)=true))). % 42.63/27.54 tff(c_28869, plain, (![V_93, V_1015]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skf1(V_1015)), true)=true))). % 42.63/27.54 tff(c_28900, plain, (![V_84, V_1016]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skf1(V_1016)), true)=true))). % 42.63/27.54 tff(c_28844, plain, (![V_96, V_1014]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skf1(V_1014)), true)=true))). % 42.63/27.54 tff(c_28801, plain, (![V_81, V_1012]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skf1(V_1012)), true)=true))). % 42.63/27.54 tff(c_28263, plain, (![U_197]: (ifeq2(man(skc14, U_197), true, agent(skc14, skf1(U_197), U_197), true)=true))). % 42.63/27.54 tff(c_28747, plain, (![V_75, V_1010]: (ifeq2(accessible_world(skc14, V_75), true, smoke(V_75, skf1(V_1010)), true)=true))). % 42.63/27.54 tff(c_27959, plain, (![V_78, V_515]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skf1(V_515)), true)=true))). % 42.63/27.54 tff(c_29105, plain, (![V_880]: (ifeq3(theme(skc13, skc15, V_880), true, ifeq3(proposition(skc13, V_880), true, V_880, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_28043, plain, (![V_714]: (ifeq2(accessible_world(skc13, V_714), true, theme(V_714, skc17, skc14), true)=true))). % 42.63/27.54 tff(c_28099, plain, (![V_533]: (ifeq2(abstraction(skc14, skf1(V_533)), true, true, true)=true))). % 42.63/27.54 tff(c_28921, plain, (![V_1017]: (ifeq2(entity(skc14, skf1(V_1017)), true, true, true)=true))). % 42.63/27.54 tff(c_28715, plain, (![V_1009]: (ifeq2(state(skc14, skf1(V_1009)), true, true, true)=true))). % 42.63/27.54 tff(c_25195, plain, (![W_860]: (ifeq3(theme(skc13, skc15, W_860), true, ifeq3(proposition(skc13, W_860), true, skc14, W_860), W_860)=W_860))). % 42.63/27.54 tff(c_28110, plain, (![U_195]: (ifeq2(man(skc14, U_195), true, true, true)=true))). % 42.63/27.54 tff(c_28068, plain, (agent(skc14, skf1(skc23), skc23)=true)). % 42.63/27.54 tff(c_28069, plain, (agent(skc14, skf1(skc19), skc19)=true)). % 42.63/27.54 tff(c_28100, plain, (![V_537]: (singleton(skc14, skf1(V_537))=true))). % 42.63/27.54 tff(c_28104, plain, (![V_529]: (specific(skc14, skf1(V_529))=true))). % 42.63/27.54 tff(c_28103, plain, (![V_532]: (thing(skc14, skf1(V_532))=true))). % 42.63/27.54 tff(c_28105, plain, (![V_527]: (nonexistent(skc14, skf1(V_527))=true))). % 42.63/27.54 tff(c_28102, plain, (![V_534]: (unisex(skc14, skf1(V_534))=true))). % 42.63/27.54 tff(c_25399, plain, (![V_870]: (ifeq3(theme(skc13, skc17, V_870), true, ifeq3(proposition(skc13, V_870), true, V_870, skc14), skc14)=skc14))). % 42.63/27.54 tff(c_28106, plain, (![V_524]: (eventuality(skc14, skf1(V_524))=true))). % 42.63/27.54 tff(c_28108, plain, (![V_520]: (present(skc14, skf1(V_520))=true))). % 42.63/27.54 tff(c_28109, plain, (![V_517]: (smoke(skc14, skf1(V_517))=true))). % 42.63/27.54 tff(c_28111, plain, (![V_514]: (event(skc14, skf1(V_514))=true))). % 42.63/27.54 tff(c_28267, plain, (theme(skc13, skc17, skc14)=true)). % 42.63/27.54 tff(c_28115, plain, (theme(skc14, skc17, skc14)=true)). % 42.63/27.54 tff(c_27928, plain, (skc16=skc14)). % 42.63/27.54 tff(c_7460, plain, (ifeq(tuple(true, general(skc14, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_7670, plain, (ifeq(tuple(true, human(skc14, skc14)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_8413, plain, (ifeq(tuple(true, existent(skc14, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_4333, plain, (![Y_407, W_406, V_405, Z_409]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(theme(skc13, skc17, V_405), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, skc17, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.54 tff(c_8324, plain, (ifeq(tuple(true, male(skc14, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9247, plain, (ifeq(tuple(true, existent(skc14, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_8806, plain, (ifeq(tuple(true, male(skc14, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_6406, plain, (ifeq(tuple(nonhuman(skc14, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_7585, plain, (ifeq(tuple(true, general(skc14, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9297, plain, (ifeq(tuple(true, male(skc14, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_9185, plain, (ifeq(tuple(nonhuman(skc14, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_2382, plain, (ifeq(tuple(true, human(skc13, skc14)), tuple(true, true), a, b)=b)). % 42.63/27.54 tff(c_3141, plain, (ifeq(tuple(true, male(skc13, skc14)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4331, plain, (![Y_407, W_406, X_410, Z_409]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(theme(skc13, X_410, skc14), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, W_406), true, skc14, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_2652, plain, (ifeq(tuple(specific(skc13, skc14), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_6238, plain, (ifeq(tuple(unisex(skc14, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_5380, plain, (ifeq(tuple(unisex(skc14, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4334, plain, (![W_406, X_410, V_405, Z_409]: (ifeq3(theme(skc13, skc15, W_406), true, ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, skc15, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_1832, plain, (ifeq(tuple(true, general(skc13, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_2019, plain, (ifeq(tuple(nonhuman(skc13, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_14580, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc19), true)=true))). % 42.63/27.55 tff(c_1732, plain, (ifeq(tuple(true, existent(skc13, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_14454, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc23), true)=true))). % 42.63/27.55 tff(c_14383, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc14), true)=true))). % 42.63/27.55 tff(c_4330, plain, (![Y_407, X_410, V_405, Z_409]: (ifeq3(theme(skc13, Y_407, skc14), true, ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, V_405), true, V_405, skc14), skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.55 tff(c_13658, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc19), true)=true))). % 42.63/27.55 tff(c_1959, plain, (ifeq(tuple(true, general(skc13, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_13843, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc19), true)=true))). % 42.63/27.55 tff(c_4332, plain, (![W_406, X_410, V_405, Z_409]: (ifeq3(theme(skc13, skc17, W_406), true, ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, skc17, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_27042, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc24), true)=true))). % 42.63/27.55 tff(c_13901, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc23), true)=true))). % 42.63/27.55 tff(c_1877, plain, (ifeq(tuple(true, male(skc13, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4335, plain, (![Y_407, W_406, V_405, Z_409]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(theme(skc13, skc15, V_405), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, skc15, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_26844, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc18), true)=true))). % 42.63/27.55 tff(c_13108, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc19), true)=true))). % 42.63/27.55 tff(c_1835, plain, (ifeq(tuple(true, general(skc13, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_13197, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc23), true)=true))). % 42.63/27.55 tff(c_26756, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc18), true)=true))). % 42.63/27.55 tff(c_12709, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc24), true)=true))). % 42.63/27.55 tff(c_4322, plain, (![W_406, X_410, V_405]: (ifeq3(theme(skc14, skc26, W_406), true, ifeq3(theme(skc14, X_410, V_405), true, ifeq3(agent(skc14, X_410, skc23), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(think_believe_consider(skc14, X_410), true, ifeq3(proposition(skc14, W_406), true, ifeq3(proposition(skc14, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_11324, plain, (![V_132]: (ifeq2(accessible_world(skc14, V_132), true, entity(V_132, skc23), true)=true))). % 42.63/27.55 tff(c_11011, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc14), true)=true))). % 42.63/27.55 tff(c_10388, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, living(V_141, skc23), true)=true))). % 42.63/27.55 tff(c_1729, plain, (ifeq(tuple(true, existent(skc13, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4323, plain, (![Y_407, W_406, V_405]: (ifeq3(theme(skc14, Y_407, W_406), true, ifeq3(theme(skc14, skc26, V_405), true, ifeq3(agent(skc14, Y_407, skc23), true, ifeq3(think_believe_consider(skc14, Y_407), true, ifeq3(think_believe_consider(skc14, skc26), true, ifeq3(proposition(skc14, W_406), true, ifeq3(proposition(skc14, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_10804, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, living(V_141, skc19), true)=true))). % 42.63/27.55 tff(c_1829, plain, (ifeq(tuple(true, general(skc14, skc26)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4326, plain, (![W_406, X_410, V_405]: (ifeq3(theme(skc13, skc17, W_406), true, ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, X_410, skc19), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_10058, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc18), true)=true))). % 42.63/27.55 tff(c_11762, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc18), true)=true))). % 42.63/27.55 tff(c_11193, plain, (![V_132]: (ifeq2(accessible_world(skc14, V_132), true, entity(V_132, skc19), true)=true))). % 42.63/27.55 tff(c_1707, plain, (ifeq(tuple(nonhuman(skc13, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4325, plain, (![Y_407, W_406, V_405]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(theme(skc13, skc15, V_405), true, ifeq3(agent(skc13, Y_407, skc19), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_11513, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, impartial(V_138, skc23), true)=true))). % 42.63/27.55 tff(c_11283, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc17), true)=true))). % 42.63/27.55 tff(c_11542, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc15), true)=true))). % 42.63/27.55 tff(c_2124, plain, (ifeq(tuple(true, male(skc13, skc17)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_10521, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc22), true)=true))). % 42.63/27.55 tff(c_4327, plain, (![Y_407, W_406, V_405]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(theme(skc13, skc17, V_405), true, ifeq3(agent(skc13, Y_407, skc19), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_12035, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc24), true)=true))). % 42.63/27.55 tff(c_12066, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc14), true)=true))). % 42.63/27.55 tff(c_1735, plain, (ifeq(tuple(true, existent(skc13, skc22)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_25991, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc24), true)=true))). % 42.63/27.55 tff(c_4324, plain, (![W_406, X_410, V_405]: (ifeq3(theme(skc13, skc15, W_406), true, ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, X_410, skc19), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, W_406), true, ifeq3(proposition(skc13, V_405), true, V_405, W_406), W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_12000, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, impartial(V_138, skc19), true)=true))). % 42.63/27.55 tff(c_7751, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc24), true)=true))). % 42.63/27.55 tff(c_1853, plain, (ifeq(tuple(true, existent(skc14, skc26)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_12457, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, existent(V_135, skc19), true)=true))). % 42.63/27.55 tff(c_25800, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc24), true)=true))). % 42.63/27.55 tff(c_25780, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc24), true)=true))). % 42.63/27.55 tff(c_10327, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc14), true)=true))). % 42.63/27.55 tff(c_2056, plain, (ifeq(tuple(true, male(skc14, skc26)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_12513, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc18), true)=true))). % 42.63/27.55 tff(c_11667, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc18), true)=true))). % 42.63/27.55 tff(c_25523, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc18), true)=true))). % 42.63/27.55 tff(c_1789, plain, (ifeq(tuple(true, male(skc13, skc15)), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_4320, plain, (![X_410, V_405, Z_409]: (ifeq3(theme(skc13, X_410, V_405), true, ifeq3(agent(skc13, skc15, Z_409), true, ifeq3(agent(skc13, X_410, Z_409), true, ifeq3(think_believe_consider(skc13, X_410), true, ifeq3(proposition(skc13, V_405), true, V_405, skc14), skc14), skc14), skc14), skc14)=skc14))). % 42.63/27.55 tff(c_14214, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc23), true)=true))). % 42.63/27.55 tff(c_12479, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, existent(V_135, skc23), true)=true))). % 42.63/27.55 tff(c_1792, plain, (ifeq(tuple(unisex(skc13, skc19), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_9967, plain, (![V_135]: (ifeq2(accessible_world(skc13, V_135), true, existent(V_135, skc19), true)=true))). % 42.63/27.55 tff(c_4321, plain, (![Y_407, W_406, Z_409]: (ifeq3(theme(skc13, Y_407, W_406), true, ifeq3(agent(skc13, Y_407, Z_409), true, ifeq3(agent(skc13, skc15, Z_409), true, ifeq3(think_believe_consider(skc13, Y_407), true, ifeq3(proposition(skc13, W_406), true, skc14, W_406), W_406), W_406), W_406), W_406)=W_406))). % 42.63/27.55 tff(c_3806, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc19), true)=true))). % 42.63/27.55 tff(c_1795, plain, (ifeq(tuple(unisex(skc13, skc23), true), tuple(true, true), a, b)=b)). % 42.63/27.55 tff(c_9909, plain, (![V_90]: (ifeq2(accessible_world(skc13, V_90), true, specific(V_90, skc19), true)=true))). % 42.63/27.55 tff(c_10035, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc18), true)=true))). % 42.63/27.55 tff(c_25012, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc18), true)=true))). % 42.63/27.55 tff(c_3986, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc23), true)=true))). % 42.63/27.55 tff(c_10138, plain, (![V_90]: (ifeq2(accessible_world(skc13, V_90), true, specific(V_90, skc23), true)=true))). % 42.63/27.55 tff(c_24927, plain, (![V_117]: (ifeq2(accessible_world(skc13, V_117), true, general(V_117, skc24), true)=true))). % 42.63/27.55 tff(c_3553, plain, (![V_135]: (ifeq2(accessible_world(skc13, V_135), true, existent(V_135, skc23), true)=true))). % 42.63/27.55 tff(c_4219, plain, (![X_403, V_404]: (ifeq3(of(skc13, skc18, X_403), true, ifeq3(of(skc13, V_404, X_403), true, ifeq3(forename(skc13, V_404), true, ifeq3(entity(skc13, X_403), true, skc18, V_404), V_404), V_404), V_404)=V_404))). % 42.63/27.55 tff(c_4366, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc18), true)=true))). % 42.63/27.55 tff(c_3843, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc24), true)=true))). % 42.63/27.55 tff(c_24770, plain, (![V_117]: (ifeq2(accessible_world(skc13, V_117), true, general(V_117, skc18), true)=true))). % 42.63/27.55 tff(c_3656, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc24), true)=true))). % 42.63/27.55 tff(c_9740, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc14), true)=true))). % 42.63/27.55 tff(c_23366, plain, (![V_790]: (ifeq2(accessible_world(skc13, V_790), true, be(V_790, skc22, skc23, skc23), true)=true))). % 42.63/27.55 tff(c_4251, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc24), true)=true))). % 42.63/27.55 tff(c_8225, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc17), true)=true))). % 42.63/27.55 tff(c_7594, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc22), true)=true))). % 42.63/27.55 tff(c_9253, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc17), true)=true))). % 42.63/27.55 tff(c_7116, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc14), true)=true))). % 42.63/27.55 tff(c_7677, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc14), true)=true))). % 42.63/27.55 tff(c_8632, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, organism(V_129, skc19), true)=true))). % 42.63/27.55 tff(c_24476, plain, (ifeq3(of(skc13, skc24, skc19), true, skc18, skc24)=skc24)). % 42.63/27.55 tff(c_24433, plain, (![W_402, X_403]: (ifeq3(of(skc13, W_402, X_403), true, ifeq3(of(skc13, skc24, X_403), true, ifeq3(forename(skc13, W_402), true, ifeq3(entity(skc13, X_403), true, W_402, skc24), skc24), skc24), skc24)=skc24))). % 42.63/27.55 tff(c_8333, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc17), true)=true))). % 42.63/27.55 tff(c_8419, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc15), true)=true))). % 42.63/27.55 tff(c_8493, plain, (![V_147]: (ifeq2(accessible_world(skc14, V_147), true, animate(V_147, skc23), true)=true))). % 42.63/27.55 tff(c_8461, plain, (![V_147]: (ifeq2(accessible_world(skc14, V_147), true, animate(V_147, skc19), true)=true))). % 42.63/27.55 tff(c_9191, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, human(V_144, skc23), true)=true))). % 42.63/27.55 tff(c_24290, plain, (ifeq3(of(skc13, skc18, skc23), true, skc24, skc18)=skc18)). % 42.63/27.55 tff(c_4220, plain, (![W_402, X_403]: (ifeq3(of(skc13, W_402, X_403), true, ifeq3(of(skc13, skc18, X_403), true, ifeq3(forename(skc13, W_402), true, ifeq3(entity(skc13, X_403), true, W_402, skc18), skc18), skc18), skc18)=skc18))). % 42.63/27.55 tff(c_7469, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc15), true)=true))). % 42.63/27.55 tff(c_9222, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc22), true)=true))). % 42.63/27.55 tff(c_8954, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, organism(V_129, skc23), true)=true))). % 42.63/27.55 tff(c_24140, plain, (ifeq3(of(skc13, skc18, skc23), true, skc18, skc24)=skc24)). % 42.63/27.55 tff(c_24007, plain, (skc20=skc18)). % 42.63/27.55 tff(c_23925, plain, (![V_156]: (ifeq2(accessible_world(skc14, V_156), true, relname(V_156, skc24), true)=true))). % 42.63/27.55 tff(c_7435, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc15), true)=true))). % 42.63/27.55 tff(c_6412, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, human(V_144, skc19), true)=true))). % 42.63/27.55 tff(c_23616, plain, (ifeq3(of(skc13, skc24, skc19), true, skc24, skc18)=skc18)). % 42.63/27.55 tff(c_23612, plain, (skc25=skc24)). % 42.63/27.55 tff(c_4213, plain, (![X_403, V_404]: (ifeq3(of(skc13, skc24, X_403), true, ifeq3(of(skc13, V_404, X_403), true, ifeq3(forename(skc13, V_404), true, ifeq3(entity(skc13, X_403), true, skc24, V_404), V_404), V_404), V_404)=V_404))). % 42.63/27.55 tff(c_9377, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc17), true)=true))). % 42.63/27.55 tff(c_9306, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc15), true)=true))). % 42.63/27.55 tff(c_22769, plain, (![V_762]: (ifeq2(accessible_world(skc13, V_762), true, of(V_762, skc18, skc19), true)=true))). % 42.63/27.55 tff(c_8187, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc22), true)=true))). % 42.63/27.55 tff(c_7909, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc24), true)=true))). % 42.63/27.55 tff(c_4068, plain, (![U_399]: (ifeq2(be(U_399, skc22, skc23, skc23), true, ifeq2(accessible_world(U_399, skc13), true, true, true), true)=true))). % 42.63/27.55 tff(c_8815, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc22), true)=true))). % 42.63/27.55 tff(c_22239, plain, (![V_743]: (ifeq2(accessible_world(skc13, V_743), true, theme(V_743, skc15, skc14), true)=true))). % 42.63/27.55 tff(c_8697, plain, (![V_156]: (ifeq2(accessible_world(skc14, V_156), true, relname(V_156, skc18), true)=true))). % 42.63/27.55 tff(c_7879, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc18), true)=true))). % 42.63/27.55 tff(c_3606, plain, (![V_376]: (ifeq2(accessible_world(skc14, V_376), true, singleton(V_376, skc26), true)=true))). % 42.63/27.55 tff(c_3535, plain, (![V_373]: (ifeq2(accessible_world(skc13, V_373), true, entity(V_373, skc19), true)=true))). % 42.63/27.55 tff(c_3607, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc15), true)=true))). % 42.63/27.55 tff(c_2973, plain, (![V_138]: (ifeq2(accessible_world(skc13, V_138), true, impartial(V_138, skc19), true)=true))). % 42.63/27.55 tff(c_3150, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc14), true)=true))). % 42.63/27.55 tff(c_3605, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc17), true)=true))). % 42.63/27.55 tff(c_3709, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc18), true)=true))). % 42.63/27.55 tff(c_22005, plain, (![V_733]: (ifeq2(accessible_world(skc13, V_733), true, of(V_733, skc24, skc23), true)=true))). % 42.63/27.55 tff(c_2388, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc14), true)=true))). % 42.63/27.55 tff(c_3245, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc14), true)=true))). % 42.63/27.55 tff(c_4016, plain, (![U_392]: (ifeq2(theme(U_392, skc15, skc14), true, ifeq2(accessible_world(U_392, skc13), true, true, true), true)=true))). % 42.63/27.55 tff(c_3295, plain, (![V_138]: (ifeq2(accessible_world(skc13, V_138), true, impartial(V_138, skc23), true)=true))). % 42.63/27.55 tff(c_3378, plain, (![V_141]: (ifeq2(accessible_world(skc13, V_141), true, living(V_141, skc19), true)=true))). % 42.63/27.55 tff(c_3604, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc22), true)=true))). % 42.63/27.55 tff(c_3710, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc24), true)=true))). % 42.63/27.56 tff(c_3534, plain, (![V_373]: (ifeq2(accessible_world(skc13, V_373), true, entity(V_373, skc23), true)=true))). % 42.63/27.56 tff(c_2686, plain, (![V_331]: (ifeq2(accessible_world(skc13, V_331), true, general(V_331, skc14), true)=true))). % 42.63/27.56 tff(c_3198, plain, (![V_141]: (ifeq2(accessible_world(skc13, V_141), true, living(V_141, skc23), true)=true))). % 42.63/27.56 tff(c_5017, plain, (![V_153]: (ifeq2(accessible_world(skc14, V_153), true, forename(V_153, skc18), true)=true))). % 42.63/27.56 tff(c_21835, plain, (![V_724]: (ifeq2(accessible_world(skc14, V_724), true, agent(V_724, skc26, skc23), true)=true))). % 42.63/27.56 tff(c_6291, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc17), true)=true))). % 42.63/27.56 tff(c_5697, plain, (![V_153]: (ifeq2(accessible_world(skc14, V_153), true, forename(V_153, skc24), true)=true))). % 42.63/27.56 tff(c_6244, plain, (![V_150]: (ifeq2(accessible_world(skc14, V_150), true, male(V_150, skc19), true)=true))). % 42.63/27.56 tff(c_5276, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, human_person(V_126, skc19), true)=true))). % 42.63/27.56 tff(c_5386, plain, (![V_150]: (ifeq2(accessible_world(skc14, V_150), true, male(V_150, skc23), true)=true))). % 42.63/27.56 tff(c_5148, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, human_person(V_126, skc23), true)=true))). % 42.63/27.56 tff(c_5847, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc15), true)=true))). % 42.63/27.56 tff(c_6739, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc22), true)=true))). % 42.63/27.56 tff(c_19872, plain, (ifeq2(agent(skc13, skf1(skc23), skc23), true, true, true)=true)). % 42.63/27.56 tff(c_19639, plain, (ifeq2(agent(skc13, skf1(skc19), skc19), true, true, true)=true)). % 42.63/27.56 tff(c_6773, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc22), true)=true))). % 42.63/27.56 tff(c_7019, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc14), true)=true))). % 42.63/27.56 tff(c_2324, plain, (![V_313]: (ifeq2(accessible_world(skc13, V_313), true, animate(V_313, skc23), true)=true))). % 42.63/27.56 tff(c_1937, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc18), true)=true))). % 42.63/27.56 tff(c_20773, plain, (![V_679]: (ifeq2(accessible_world(skc13, V_679), true, agent(V_679, skc17, skc19), true)=true))). % 42.63/27.56 tff(c_2578, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc15), true)=true))). % 42.63/27.56 tff(c_1939, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc24), true)=true))). % 42.63/27.56 tff(c_3929, plain, (![U_388]: (ifeq2(agent(U_388, skc26, skc23), true, ifeq2(accessible_world(U_388, skc14), true, true, true), true)=true))). % 42.63/27.56 tff(c_2851, plain, (![V_340]: (ifeq2(accessible_world(skc13, V_340), true, organism(V_340, skc23), true)=true))). % 42.63/27.56 tff(c_2577, plain, (![V_325]: (ifeq2(accessible_world(skc14, V_325), true, nonexistent(V_325, skc26), true)=true))). % 42.63/27.56 tff(c_3714, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc14), true)=true))). % 42.63/27.56 tff(c_2743, plain, (![V_334]: (ifeq2(accessible_world(skc13, V_334), true, human(V_334, skc19), true)=true))). % 42.63/27.56 tff(c_2580, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc22), true)=true))). % 42.63/27.56 tff(c_2744, plain, (![V_334]: (ifeq2(accessible_world(skc13, V_334), true, human(V_334, skc23), true)=true))). % 42.63/27.56 tff(c_3247, plain, (![V_358]: (ifeq2(accessible_world(skc14, V_358), true, thing(V_358, skc26), true)=true))). % 42.63/27.56 tff(c_2323, plain, (![V_313]: (ifeq2(accessible_world(skc13, V_313), true, animate(V_313, skc19), true)=true))). % 42.63/27.56 tff(c_3868, plain, (![U_384]: (ifeq2(of(U_384, skc24, skc23), true, ifeq2(accessible_world(U_384, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_2204, plain, (![V_307]: (ifeq2(accessible_world(skc14, V_307), true, unisex(V_307, skc26), true)=true))). % 42.63/27.56 tff(c_2203, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc17), true)=true))). % 42.63/27.56 tff(c_2206, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc15), true)=true))). % 42.63/27.56 tff(c_2916, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc17), true)=true))). % 42.63/27.56 tff(c_2579, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc17), true)=true))). % 42.63/27.56 tff(c_2917, plain, (![V_343]: (ifeq2(accessible_world(skc14, V_343), true, specific(V_343, skc26), true)=true))). % 42.63/27.56 tff(c_2852, plain, (![V_340]: (ifeq2(accessible_world(skc13, V_340), true, organism(V_340, skc19), true)=true))). % 42.63/27.56 tff(c_2205, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc22), true)=true))). % 42.63/27.56 tff(c_3246, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc15), true)=true))). % 42.63/27.56 tff(c_3249, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc22), true)=true))). % 42.63/27.56 tff(c_2918, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc15), true)=true))). % 42.63/27.56 tff(c_3248, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc17), true)=true))). % 42.63/27.56 tff(c_2919, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc22), true)=true))). % 42.63/27.56 tff(c_3941, plain, (![U_388]: (ifeq2(agent(U_388, skc17, skc19), true, ifeq2(accessible_world(U_388, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_5449, plain, (![V_162]: (ifeq2(accessible_world(skc14, V_162), true, jules_forename(V_162, skc24), true)=true))). % 42.63/27.56 tff(c_4976, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, man(V_123, skc23), true)=true))). % 42.63/27.56 tff(c_19960, plain, (![V_644]: (ifeq2(accessible_world(skc13, V_644), true, agent(V_644, skc15, skc19), true)=true))). % 42.63/27.56 tff(c_4593, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc17), true)=true))). % 42.63/27.56 tff(c_4498, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc15), true)=true))). % 42.63/27.56 tff(c_4840, plain, (![V_159]: (ifeq2(accessible_world(skc14, V_159), true, vincent_forename(V_159, skc18), true)=true))). % 42.63/27.56 tff(c_5112, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, man(V_123, skc19), true)=true))). % 42.63/27.56 tff(c_3874, plain, (![U_384]: (ifeq2(of(U_384, skc18, skc19), true, ifeq2(accessible_world(U_384, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_6508, plain, (![V_105]: (ifeq2(accessible_world(skc14, V_105), true, proposition(V_105, skc14), true)=true))). % 42.63/27.56 tff(c_6627, plain, (![V_120]: (ifeq2(accessible_world(skc14, V_120), true, state(V_120, skc22), true)=true))). % 42.63/27.56 tff(c_3772, plain, (![V_382]: (ifeq2(accessible_world(skc13, V_382), true, male(V_382, skc23), true)=true))). % 42.63/27.56 tff(c_2118, plain, (![V_304]: (ifeq2(accessible_world(skc13, V_304), true, relname(V_304, skc24), true)=true))). % 42.63/27.56 tff(c_3771, plain, (![V_382]: (ifeq2(accessible_world(skc13, V_382), true, male(V_382, skc19), true)=true))). % 42.63/27.56 tff(c_2115, plain, (![V_304]: (ifeq2(accessible_world(skc13, V_304), true, relname(V_304, skc18), true)=true))). % 42.63/27.56 tff(c_3095, plain, (![V_352]: (ifeq2(accessible_world(skc13, V_352), true, human_person(V_352, skc23), true)=true))). % 42.63/27.56 tff(c_2262, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc22), true)=true))). % 42.63/27.56 tff(c_3094, plain, (![V_352]: (ifeq2(accessible_world(skc13, V_352), true, human_person(V_352, skc19), true)=true))). % 42.63/27.56 tff(c_2260, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc17), true)=true))). % 42.63/27.56 tff(c_2261, plain, (![V_310]: (ifeq2(accessible_world(skc14, V_310), true, eventuality(V_310, skc26), true)=true))). % 42.63/27.56 tff(c_1941, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc14), true)=true))). % 42.63/27.56 tff(c_3047, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc22), true)=true))). % 42.63/27.56 tff(c_2259, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc15), true)=true))). % 42.63/27.56 tff(c_3935, plain, (![U_388]: (ifeq2(agent(U_388, skc15, skc19), true, ifeq2(accessible_world(U_388, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_19317, plain, (![V_514]: (ifeq2(event(skc13, skf1(V_514)), true, true, true)=true))). % 42.63/27.56 tff(c_2489, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc13), true, ifeq2(state(U_321, skc22), true, true, true), true)=true))). % 42.63/27.56 tff(c_19249, plain, (ifeq2(unisex(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_19120, plain, (![W_618]: (ifeq2(unisex(skc13, W_618), true, unisex(skc14, W_618), true)=true))). % 42.63/27.56 tff(c_19154, plain, (![V_524]: (ifeq2(eventuality(skc13, skf1(V_524)), true, true, true)=true))). % 42.63/27.56 tff(c_8541, plain, (![W_453]: (ifeq2(state(skc13, W_453), true, state(skc14, W_453), true)=true))). % 42.63/27.56 tff(c_8645, plain, (![W_454]: (ifeq2(man(skc13, W_454), true, man(skc14, W_454), true)=true))). % 42.63/27.56 tff(c_18795, plain, (ifeq2(nonexistent(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_18567, plain, (![W_607]: (ifeq2(nonexistent(skc13, W_607), true, nonexistent(skc14, W_607), true)=true))). % 42.63/27.56 tff(c_11245, plain, (![W_474]: (ifeq2(vincent_forename(skc13, W_474), true, vincent_forename(skc14, W_474), true)=true))). % 42.63/27.56 tff(c_18668, plain, (be(skc14, skc22, skc23, skc23)=true)). % 42.63/27.56 tff(c_18450, plain, (![V_529]: (ifeq2(specific(skc13, skf1(V_529)), true, true, true)=true))). % 42.63/27.56 tff(c_11952, plain, (![W_481]: (ifeq2(entity(skc13, W_481), true, entity(skc14, W_481), true)=true))). % 42.63/27.56 tff(c_7650, plain, (![W_444]: (ifeq2(nonhuman(skc13, W_444), true, nonhuman(skc14, W_444), true)=true))). % 42.63/27.56 tff(c_18235, plain, (![V_534]: (ifeq2(unisex(skc13, skf1(V_534)), true, true, true)=true))). % 42.63/27.56 tff(c_18134, plain, (![V_594]: (ifeq2(accessible_world(skc13, V_594), true, think_believe_consider(V_594, skc17), true)=true))). % 42.63/27.56 tff(c_13570, plain, (![W_497]: (ifeq2(animate(skc13, W_497), true, animate(skc14, W_497), true)=true))). % 42.63/27.56 tff(c_18090, plain, (![V_527]: (ifeq2(nonexistent(skc13, skf1(V_527)), true, true, true)=true))). % 42.63/27.56 tff(c_14278, plain, (![W_504]: (ifeq2(living(skc13, W_504), true, living(skc14, W_504), true)=true))). % 42.63/27.56 tff(c_13045, plain, (![W_491]: (ifeq2(human(skc13, W_491), true, human(skc14, W_491), true)=true))). % 42.63/27.56 tff(c_12269, plain, (![W_486]: (ifeq2(forename(skc13, W_486), true, forename(skc14, W_486), true)=true))). % 42.63/27.56 tff(c_12432, plain, (![W_487]: (ifeq2(existent(skc13, W_487), true, existent(skc14, W_487), true)=true))). % 42.63/27.56 tff(c_11782, plain, (![V_479]: (ifeq2(accessible_world(skc13, V_479), true, present(V_479, skc15), true)=true))). % 42.63/27.56 tff(c_15555, plain, (![V_519]: (ifeq2(accessible_world(skc13, V_519), true, think_believe_consider(V_519, skc15), true)=true))). % 42.63/27.56 tff(c_8341, plain, (![V_449]: (ifeq2(accessible_world(skc14, V_449), true, present(V_449, skc26), true)=true))). % 42.63/27.56 tff(c_10340, plain, (![W_466]: (ifeq2(proposition(skc13, W_466), true, proposition(skc14, W_466), true)=true))). % 42.63/27.56 tff(c_17590, plain, (ifeq2(eventuality(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_13391, plain, (![W_495]: (ifeq2(eventuality(skc13, W_495), true, eventuality(skc14, W_495), true)=true))). % 42.63/27.56 tff(c_17433, plain, (![V_532]: (ifeq2(thing(skc13, skf1(V_532)), true, true, true)=true))). % 42.63/27.56 tff(c_13455, plain, (![W_496]: (ifeq2(organism(skc13, W_496), true, organism(skc14, W_496), true)=true))). % 42.63/27.56 tff(c_10667, plain, (![W_469]: (ifeq2(male(skc13, W_469), true, male(skc14, W_469), true)=true))). % 42.63/27.56 tff(c_14809, plain, (![W_509]: (ifeq2(relname(skc13, W_509), true, relname(skc14, W_509), true)=true))). % 42.63/27.56 tff(c_17189, plain, (![V_537]: (ifeq2(singleton(skc13, skf1(V_537)), true, true, true)=true))). % 42.63/27.56 tff(c_7809, plain, (![W_445]: (ifeq2(abstraction(skc13, W_445), true, abstraction(skc14, W_445), true)=true))). % 42.63/27.56 tff(c_14675, plain, (![W_508]: (ifeq2(general(skc13, W_508), true, general(skc14, W_508), true)=true))). % 42.63/27.56 tff(c_16880, plain, (ifeq2(thing(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_16936, plain, (ifeq2(event(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_16756, plain, (![W_558]: (ifeq2(event(skc13, W_558), true, event(skc14, W_558), true)=true))). % 42.63/27.56 tff(c_14094, plain, (![W_503]: (ifeq2(thing(skc13, W_503), true, thing(skc14, W_503), true)=true))). % 42.63/27.56 tff(c_14341, plain, (![V_505]: (ifeq2(accessible_world(skc13, V_505), true, present(V_505, skc17), true)=true))). % 42.63/27.56 tff(c_14930, plain, (![W_510]: (ifeq2(impartial(skc13, W_510), true, impartial(skc14, W_510), true)=true))). % 42.63/27.56 tff(c_16694, plain, (![V_517]: (ifeq2(smoke(skc13, skf1(V_517)), true, true, true)=true))). % 42.63/27.56 tff(c_15064, plain, (![W_511]: (ifeq2(relation(skc13, W_511), true, relation(skc14, W_511), true)=true))). % 42.63/27.56 tff(c_10437, plain, (![W_467]: (ifeq2(jules_forename(skc13, W_467), true, jules_forename(skc14, W_467), true)=true))). % 42.63/27.56 tff(c_13157, plain, (![W_492]: (ifeq2(human_person(skc13, W_492), true, human_person(skc14, W_492), true)=true))). % 42.63/27.56 tff(c_3490, plain, (![U_369]: (ifeq2(think_believe_consider(U_369, skc15), true, ifeq2(accessible_world(U_369, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_16395, plain, (ifeq2(smoke(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_16228, plain, (![W_543]: (ifeq2(smoke(skc13, W_543), true, smoke(skc14, W_543), true)=true))). % 42.63/27.56 tff(c_16194, plain, (ifeq2(specific(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_16026, plain, (![W_539]: (ifeq2(specific(skc13, W_539), true, specific(skc14, W_539), true)=true))). % 42.63/27.56 tff(c_16124, plain, (ifeq2(singleton(skc13, skc26), true, true, true)=true)). % 42.63/27.56 tff(c_14540, plain, (![W_507]: (ifeq2(singleton(skc13, W_507), true, singleton(skc14, W_507), true)=true))). % 42.63/27.56 tff(c_2436, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc13), true, ifeq2(forename(U_318, skc18), true, true, true), true)=true))). % 42.63/27.56 tff(c_15606, plain, (![V_521]: (ifeq2(present(skc13, skf1(V_521)), true, true, true)=true))). % 42.63/27.56 tff(c_15017, plain, (agent(skc14, skc17, skc19)=true)). % 42.63/27.56 tff(c_14918, plain, (theme(skc14, skc15, skc14)=true)). % 42.63/27.56 tff(c_14733, plain, (of(skc14, skc18, skc19)=true)). % 42.63/27.56 tff(c_7287, plain, (ifeq2(agent(skc13, skc26, skc23), true, true, true)=true)). % 42.63/27.56 tff(c_14694, plain, (agent(skc14, skc15, skc19)=true)). % 42.63/27.56 tff(c_14598, plain, (of(skc14, skc24, skc23)=true)). % 42.63/27.56 tff(c_13646, plain, (ifeq2(abstraction(skc14, skc19), true, true, true)=true)). % 42.63/27.56 tff(c_13655, plain, (ifeq2(eventuality(skc14, skc19), true, true, true)=true)). % 42.63/27.56 tff(c_14551, plain, (singleton(skc14, skc19)=true)). % 42.63/27.56 tff(c_14433, plain, (singleton(skc14, skc23)=true)). % 42.63/27.56 tff(c_11836, plain, (ifeq2(entity(skc14, skc24), true, true, true)=true)). % 42.63/27.56 tff(c_14201, plain, (ifeq2(abstraction(skc14, skc23), true, true, true)=true)). % 42.63/27.56 tff(c_14362, plain, (singleton(skc14, skc14)=true)). % 42.63/27.56 tff(c_14296, plain, (singleton(skc14, skc18)=true)). % 42.63/27.56 tff(c_14210, plain, (ifeq2(eventuality(skc14, skc23), true, true, true)=true)). % 42.63/27.56 tff(c_14181, plain, (thing(skc14, skc23)=true)). % 42.63/27.56 tff(c_11005, plain, (ifeq2(entity(skc14, skc14), true, true, true)=true)). % 42.63/27.56 tff(c_1986, plain, (![U_297]: (ifeq2(present(U_297, skc15), true, ifeq2(accessible_world(U_297, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_13874, plain, (specific(skc14, skc23)=true)). % 42.63/27.56 tff(c_13816, plain, (specific(skc14, skc19)=true)). % 42.63/27.56 tff(c_13788, plain, (singleton(skc14, skc24)=true)). % 42.63/27.56 tff(c_2418, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc13), true, ifeq2(forename(U_318, skc24), true, true, true), true)=true))). % 42.63/27.56 tff(c_11008, plain, (ifeq2(eventuality(skc14, skc14), true, true, true)=true)). % 42.63/27.56 tff(c_13628, plain, (thing(skc14, skc19)=true)). % 42.63/27.56 tff(c_11661, plain, (ifeq2(entity(skc14, skc18), true, true, true)=true)). % 42.63/27.56 tff(c_12250, plain, (ifeq2(proposition(skc14, skc18), true, true, true)=true)). % 42.63/27.56 tff(c_12507, plain, (ifeq2(eventuality(skc14, skc18), true, true, true)=true)). % 42.63/27.56 tff(c_11567, plain, (ifeq2(proposition(skc14, skc24), true, true, true)=true)). % 42.63/27.56 tff(c_12029, plain, (ifeq2(eventuality(skc14, skc24), true, true, true)=true)). % 42.63/27.56 tff(c_3170, plain, (![U_354]: (ifeq2(accessible_world(U_354, skc14), true, ifeq2(smoke(U_354, skc26), true, true, true), true)=true))). % 42.63/27.56 tff(c_3837, plain, (ifeq2(entity(skc13, skc24), true, true, true)=true)). % 42.63/27.56 tff(c_3794, plain, (ifeq2(abstraction(skc13, skc19), true, true, true)=true)). % 42.63/27.56 tff(c_3484, plain, (![U_369]: (ifeq2(think_believe_consider(U_369, skc17), true, ifeq2(accessible_world(U_369, skc13), true, true, true), true)=true))). % 42.63/27.56 tff(c_13172, plain, (singleton(skc13, skc23)=true)). % 42.63/27.56 tff(c_10135, plain, (ifeq2(eventuality(skc13, skc23), true, true, true)=true)). % 42.63/27.56 tff(c_13083, plain, (singleton(skc13, skc19)=true)). % 42.63/27.56 tff(c_3974, plain, (ifeq2(abstraction(skc13, skc23), true, true, true)=true)). % 42.63/27.56 tff(c_12943, plain, (singleton(skc13, skc18)=true)). % 42.63/27.56 tff(c_4397, plain, (ifeq2(entity(skc13, skc18), true, true, true)=true)). % 42.63/27.56 tff(c_4245, plain, (ifeq2(eventuality(skc13, skc24), true, true, true)=true)). % 42.63/27.56 tff(c_9906, plain, (ifeq2(eventuality(skc13, skc19), true, true, true)=true)). % 42.63/27.56 tff(c_4400, plain, (ifeq2(eventuality(skc13, skc18), true, true, true)=true)). % 42.63/27.57 tff(c_12621, plain, (singleton(skc13, skc24)=true)). % 42.63/27.57 tff(c_12486, plain, (unisex(skc14, skc18)=true)). % 42.63/27.57 tff(c_12436, plain, (existent(skc14, skc23)=true)). % 42.63/27.57 tff(c_12435, plain, (existent(skc14, skc19)=true)). % 42.63/27.57 tff(c_12230, plain, (relation(skc14, skc18)=true)). % 42.63/27.57 tff(c_8219, plain, (ifeq2(entity(skc14, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_4078, plain, (![W_397, X_400, Y_396]: (ifeq2(be(skc13, W_397, X_400, Y_396), true, be(skc14, W_397, X_400, Y_396), true)=true))). % 42.63/27.57 tff(c_12042, plain, (general(skc14, skc14)=true)). % 42.63/27.57 tff(c_12008, plain, (unisex(skc14, skc24)=true)). % 42.63/27.57 tff(c_11979, plain, (impartial(skc14, skc19)=true)). % 42.63/27.57 tff(c_3314, plain, (![U_360]: (ifeq2(accessible_world(U_360, skc13), true, ifeq2(jules_forename(U_360, skc24), true, true, true), true)=true))). % 42.63/27.57 tff(c_11812, plain, (thing(skc14, skc24)=true)). % 42.63/27.57 tff(c_8812, plain, (ifeq2(abstraction(skc14, skc22), true, true, true)=true)). % 42.63/27.57 tff(c_11738, plain, (general(skc14, skc18)=true)). % 42.63/27.57 tff(c_3038, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc15), true, true, true), true)=true))). % 42.63/27.57 tff(c_11637, plain, (thing(skc14, skc18)=true)). % 42.63/27.57 tff(c_2621, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc13), true, ifeq2(vincent_forename(U_327, skc18), true, true, true), true)=true))). % 42.63/27.57 tff(c_11549, plain, (relation(skc14, skc24)=true)). % 42.63/27.57 tff(c_11521, plain, (singleton(skc14, skc15)=true)). % 42.63/27.57 tff(c_11492, plain, (impartial(skc14, skc23)=true)). % 42.63/27.57 tff(c_3356, plain, (![U_363]: (ifeq2(accessible_world(U_363, skc13), true, ifeq2(proposition(U_363, skc14), true, true, true), true)=true))). % 42.63/27.57 tff(c_9303, plain, (ifeq2(abstraction(skc14, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_3044, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc17), true, true, true), true)=true))). % 42.63/27.57 tff(c_11290, plain, (entity(skc14, skc23)=true)). % 42.63/27.57 tff(c_11262, plain, (singleton(skc14, skc17)=true)). % 42.63/27.57 tff(c_11159, plain, (entity(skc14, skc19)=true)). % 42.63/27.57 tff(c_1998, plain, (![U_297]: (ifeq2(present(U_297, skc17), true, ifeq2(accessible_world(U_297, skc13), true, true, true), true)=true))). % 42.63/27.57 tff(c_10981, plain, (thing(skc14, skc14)=true)). % 42.63/27.57 tff(c_8181, plain, (ifeq2(entity(skc14, skc22), true, true, true)=true)). % 42.63/27.57 tff(c_10783, plain, (living(skc14, skc19)=true)). % 42.63/27.57 tff(c_9365, plain, (ifeq2(abstraction(skc14, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_10681, plain, (general(skc14, skc24)=true)). % 42.63/27.57 tff(c_10500, plain, (singleton(skc14, skc22)=true)). % 42.63/27.57 tff(c_7463, plain, (ifeq2(entity(skc14, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_10367, plain, (living(skc14, skc23)=true)). % 42.63/27.57 tff(c_10300, plain, (unisex(skc14, skc14)=true)). % 42.63/27.57 tff(c_2817, plain, (ifeq2(entity(skc13, skc14), true, true, true)=true)). % 42.63/27.57 tff(c_10111, plain, (specific(skc13, skc23)=true)). % 42.63/27.57 tff(c_10034, plain, (nonhuman(skc14, skc18)=true)). % 42.63/27.57 tff(c_10007, plain, (nonhuman(skc13, skc18)=true)). % 42.63/27.57 tff(c_9943, plain, (existent(skc13, skc19)=true)). % 42.63/27.57 tff(c_9882, plain, (specific(skc13, skc19)=true)). % 42.63/27.57 tff(c_9719, plain, (singleton(skc13, skc14)=true)). % 42.63/27.57 tff(c_3144, plain, (ifeq2(eventuality(skc13, skc14), true, true, true)=true)). % 42.63/27.57 tff(c_9347, plain, (thing(skc14, skc17)=true)). % 42.63/27.57 tff(c_9260, plain, (unisex(skc14, skc15)=true)). % 42.63/27.57 tff(c_2954, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc13), true, ifeq2(man(U_345, skc19), true, true, true), true)=true))). % 42.63/27.57 tff(c_9229, plain, (nonexistent(skc14, skc17)=true)). % 42.63/27.57 tff(c_9198, plain, (nonexistent(skc14, skc22)=true)). % 42.63/27.57 tff(c_9138, plain, (human(skc14, skc23)=true)). % 42.63/27.57 tff(c_8924, plain, (organism(skc14, skc23)=true)). % 42.63/27.57 tff(c_8788, plain, (unisex(skc14, skc22)=true)). % 42.63/27.57 tff(c_3032, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc14), true, ifeq2(event(U_348, skc26), true, true, true), true)=true))). % 42.63/27.57 tff(c_8673, plain, (relname(skc14, skc18)=true)). % 42.63/27.57 tff(c_8602, plain, (organism(skc14, skc19)=true)). % 42.63/27.57 tff(c_5686, plain, (ifeq2(vincent_forename(skc14, skc24), true, true, true)=true)). % 42.63/27.57 tff(c_8472, plain, (animate(skc14, skc23)=true)). % 42.63/27.57 tff(c_6770, plain, (ifeq2(smoke(skc14, skc22), true, true, true)=true)). % 42.63/27.57 tff(c_8440, plain, (animate(skc14, skc19)=true)). % 42.63/27.57 tff(c_8395, plain, (nonexistent(skc14, skc15)=true)). % 42.63/27.57 tff(c_8306, plain, (unisex(skc14, skc17)=true)). % 42.63/27.57 tff(c_5012, plain, (ifeq2(jules_forename(skc14, skc18), true, true, true)=true)). % 42.63/27.57 tff(c_2948, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc13), true, ifeq2(man(U_345, skc23), true, true, true), true)=true))). % 42.63/27.57 tff(c_8151, plain, (ifeq2(accessible_world(skc14, skc13), true, true, true)=true)). % 42.63/27.57 tff(c_8198, plain, (specific(skc14, skc17)=true)). % 42.63/27.57 tff(c_8157, plain, (thing(skc14, skc22)=true)). % 42.63/27.57 tff(c_1992, plain, (![U_297]: (ifeq2(present(U_297, skc26), true, ifeq2(accessible_world(U_297, skc14), true, true, true), true)=true))). % 42.63/27.57 tff(c_7814, plain, (abstraction(skc14, skc24)=true)). % 42.63/27.57 tff(c_7813, plain, (abstraction(skc14, skc18)=true)). % 42.63/27.57 tff(c_7653, plain, (nonhuman(skc14, skc24)=true)). % 42.63/27.57 tff(c_7655, plain, (nonhuman(skc14, skc14)=true)). % 42.63/27.57 tff(c_7567, plain, (specific(skc14, skc22)=true)). % 42.63/27.57 tff(c_7442, plain, (specific(skc14, skc15)=true)). % 42.63/27.57 tff(c_7405, plain, (thing(skc14, skc15)=true)). % 42.63/27.57 tff(c_3884, plain, (![W_385, X_386]: (ifeq2(of(skc13, W_385, X_386), true, of(skc14, W_385, X_386), true)=true))). % 42.63/27.57 tff(c_7273, plain, (relname(skc14, skc24)=true)). % 42.63/27.57 tff(c_3951, plain, (![W_389, X_390]: (ifeq2(agent(skc13, W_389, X_390), true, agent(skc14, W_389, X_390), true)=true))). % 42.63/27.57 tff(c_7016, plain, (ifeq2(relname(skc14, skc14), true, true, true)=true)). % 42.63/27.57 tff(c_7083, plain, (abstraction(skc14, skc14)=true)). % 42.63/27.57 tff(c_4026, plain, (![W_393, X_394]: (ifeq2(theme(skc13, W_393, X_394), true, theme(skc14, W_393, X_394), true)=true))). % 42.63/27.57 tff(c_6992, plain, (relation(skc14, skc14)=true)). % 42.63/27.57 tff(c_6746, plain, (event(skc14, skc22)=true)). % 42.63/27.57 tff(c_6703, plain, (eventuality(skc14, skc22)=true)). % 42.63/27.57 tff(c_6599, plain, (state(skc14, skc22)=true)). % 42.63/27.57 tff(c_2492, plain, (![V_322]: (ifeq2(accessible_world(skc13, V_322), true, state(V_322, skc22), true)=true))). % 42.63/27.57 tff(c_6475, plain, (proposition(skc14, skc14)=true)). % 42.63/27.57 tff(c_3363, plain, (![V_364]: (ifeq2(accessible_world(skc13, V_364), true, proposition(V_364, skc14), true)=true))). % 42.63/27.57 tff(c_6388, plain, (human(skc14, skc19)=true)). % 42.63/27.57 tff(c_6255, plain, (eventuality(skc14, skc17)=true)). % 42.63/27.57 tff(c_4589, plain, (ifeq2(smoke(skc14, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_6220, plain, (male(skc14, skc19)=true)). % 42.63/27.57 tff(c_2439, plain, (![V_319]: (ifeq2(accessible_world(skc13, V_319), true, forename(V_319, skc24), true)=true))). % 42.63/27.57 tff(c_4494, plain, (ifeq2(smoke(skc14, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_2442, plain, (![V_319]: (ifeq2(accessible_world(skc13, V_319), true, forename(V_319, skc18), true)=true))). % 42.63/27.57 tff(c_5811, plain, (eventuality(skc14, skc15)=true)). % 42.63/27.57 tff(c_3048, plain, (![V_349]: (ifeq2(accessible_world(skc14, V_349), true, event(V_349, skc26), true)=true))). % 42.63/27.57 tff(c_4583, plain, (ifeq2(state(skc14, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_5708, plain, (ifeq2(accessible_world(skc14, skc14), true, true, true)=true)). % 42.63/27.57 tff(c_3173, plain, (![V_355]: (ifeq2(accessible_world(skc14, V_355), true, smoke(V_355, skc26), true)=true))). % 42.63/27.57 tff(c_5662, plain, (forename(skc14, skc24)=true)). % 42.63/27.57 tff(c_5627, plain, (think_believe_consider(skc14, skc15)=true)). % 42.63/27.57 tff(c_5592, plain, (think_believe_consider(skc14, skc17)=true)). % 42.63/27.57 tff(c_3494, plain, (![W_370]: (ifeq2(think_believe_consider(skc13, W_370), true, think_believe_consider(skc14, W_370), true)=true))). % 42.63/27.57 tff(c_4488, plain, (ifeq2(state(skc14, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_5424, plain, (jules_forename(skc14, skc24)=true)). % 42.63/27.57 tff(c_5345, plain, (male(skc14, skc23)=true)). % 42.63/27.57 tff(c_3323, plain, (![V_361]: (ifeq2(accessible_world(skc13, V_361), true, jules_forename(V_361, skc24), true)=true))). % 42.63/27.57 tff(c_5229, plain, (human_person(skc14, skc19)=true)). % 42.63/27.57 tff(c_5161, plain, (ifeq2(present(skc13, skc26), true, true, true)=true)). % 42.63/27.57 tff(c_5198, plain, (present(skc14, skc17)=true)). % 42.63/27.57 tff(c_5171, plain, (present(skc14, skc15)=true)). % 42.63/27.57 tff(c_2002, plain, (![W_298]: (ifeq2(present(skc13, W_298), true, present(skc14, W_298), true)=true))). % 42.63/27.57 tff(c_5118, plain, (human_person(skc14, skc23)=true)). % 42.63/27.57 tff(c_5084, plain, (man(skc14, skc19)=true)). % 42.63/27.57 tff(c_2958, plain, (![V_346]: (ifeq2(accessible_world(skc13, V_346), true, man(V_346, skc19), true)=true))). % 42.63/27.57 tff(c_4982, plain, (forename(skc14, skc18)=true)). % 42.63/27.57 tff(c_4948, plain, (man(skc14, skc23)=true)). % 42.63/27.57 tff(c_2957, plain, (![V_346]: (ifeq2(accessible_world(skc13, V_346), true, man(V_346, skc23), true)=true))). % 42.63/27.57 tff(c_4815, plain, (vincent_forename(skc14, skc18)=true)). % 42.63/27.57 tff(c_2630, plain, (![V_328]: (ifeq2(accessible_world(skc13, V_328), true, vincent_forename(V_328, skc18), true)=true))). % 42.63/27.57 tff(c_4562, plain, (event(skc14, skc17)=true)). % 42.63/27.57 tff(c_3050, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc17), true)=true))). % 42.63/27.57 tff(c_4467, plain, (event(skc14, skc15)=true)). % 42.63/27.57 tff(c_4419, plain, (ifeq2(accessible_world(skc13, skc13), true, true, true)=true)). % 42.63/27.57 tff(c_3049, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc15), true)=true))). % 42.63/27.57 tff(c_4373, plain, (thing(skc13, skc18)=true)). % 42.63/27.57 tff(c_4339, plain, (unisex(skc13, skc18)=true)). % 42.63/27.57 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))). % 42.63/27.57 tff(c_4224, plain, (unisex(skc13, skc24)=true)). % 42.63/27.57 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))). % 42.63/27.57 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))). % 42.63/27.57 tff(c_3993, plain, (general(skc13, skc18)=true)). % 42.63/27.57 tff(c_132, plain, (![U_168, W_169, X_170, V_171]: (ifeq2(theme(U_168, W_169, X_170), true, ifeq2(accessible_world(U_168, V_171), true, theme(V_171, W_169, X_170), true), true)=true))). % 42.63/27.57 tff(c_3956, plain, (thing(skc13, skc23)=true)). % 42.63/27.57 tff(c_130, plain, (![U_164, W_165, X_166, V_167]: (ifeq2(agent(U_164, W_165, X_166), true, ifeq2(accessible_world(U_164, V_167), true, agent(V_167, W_165, X_166), true), true)=true))). % 42.63/27.57 tff(c_134, plain, (![U_172, W_173, X_174, V_175]: (ifeq2(of(U_172, W_173, X_174), true, ifeq2(accessible_world(U_172, V_175), true, of(V_175, W_173, X_174), true), true)=true))). % 42.63/27.57 tff(c_3813, plain, (thing(skc13, skc24)=true)). % 42.63/27.57 tff(c_3776, plain, (thing(skc13, skc19)=true)). % 42.63/27.57 tff(c_120, plain, (![U_149, V_150, W_151]: (ifeq2(accessible_world(U_149, V_150), true, ifeq2(male(U_149, W_151), true, male(V_150, W_151), true), true)=true))). % 42.63/27.57 tff(c_3718, plain, (general(skc13, skc24)=true)). % 42.63/27.57 tff(c_94, plain, (![U_110, V_111, W_112]: (ifeq2(accessible_world(U_110, V_111), true, ifeq2(abstraction(U_110, W_112), true, abstraction(V_111, W_112), true), true)=true))). % 42.63/27.57 tff(c_3632, plain, (nonhuman(skc13, skc24)=true)). % 42.63/27.57 tff(c_78, plain, (![U_86, V_87, W_88]: (ifeq2(accessible_world(U_86, V_87), true, ifeq2(singleton(U_86, W_88), true, singleton(V_87, W_88), true), true)=true))). % 42.63/27.57 tff(c_3502, plain, (existent(skc13, skc23)=true)). % 42.63/27.57 tff(c_108, plain, (![U_131, V_132, W_133]: (ifeq2(accessible_world(U_131, V_132), true, ifeq2(entity(U_131, W_133), true, entity(V_132, W_133), true), true)=true))). % 42.63/27.57 tff(c_88, plain, (![U_101, W_102, V_103]: (ifeq2(think_believe_consider(U_101, W_102), true, ifeq2(accessible_world(U_101, V_103), true, think_believe_consider(V_103, W_102), true), true)=true))). % 42.63/27.57 tff(c_3439, plain, (abstraction(skc13, skc18)=true)). % 42.63/27.57 tff(c_110, plain, (![U_134, V_135, W_136]: (ifeq2(accessible_world(U_134, V_135), true, ifeq2(existent(U_134, W_136), true, existent(V_135, W_136), true), true)=true))). % 42.63/27.57 tff(c_977, plain, (ifeq2(proposition(skc13, skc24), true, true, true)=true)). % 42.63/27.57 tff(c_3330, plain, (living(skc13, skc19)=true)). % 42.63/27.57 tff(c_90, plain, (![U_104, V_105, W_106]: (ifeq2(accessible_world(U_104, V_105), true, ifeq2(proposition(U_104, W_106), true, proposition(V_105, W_106), true), true)=true))). % 42.63/27.57 tff(c_128, plain, (![U_161, V_162, W_163]: (ifeq2(accessible_world(U_161, V_162), true, ifeq2(jules_forename(U_161, W_163), true, jules_forename(V_162, W_163), true), true)=true))). % 42.63/27.57 tff(c_3274, plain, (impartial(skc13, skc23)=true)). % 42.63/27.57 tff(c_3253, plain, (singleton(skc13, skc22)=true)). % 42.63/27.57 tff(c_76, plain, (![U_83, V_84, W_85]: (ifeq2(accessible_world(U_83, V_84), true, ifeq2(thing(U_83, W_85), true, thing(V_84, W_85), true), true)=true))). % 42.63/27.57 tff(c_3177, plain, (living(skc13, skc23)=true)). % 42.63/27.57 tff(c_70, plain, (![U_74, V_75, W_76]: (ifeq2(accessible_world(U_74, V_75), true, ifeq2(smoke(U_74, W_76), true, smoke(V_75, W_76), true), true)=true))). % 42.63/27.57 tff(c_3123, plain, (unisex(skc13, skc14)=true)). % 42.63/27.57 tff(c_104, plain, (![U_125, V_126, W_127]: (ifeq2(accessible_world(U_125, V_126), true, ifeq2(human_person(U_125, W_127), true, human_person(V_126, W_127), true), true)=true))). % 42.63/27.57 tff(c_2062, plain, (ifeq2(abstraction(skc14, skc26), true, true, true)=true)). % 42.63/27.57 tff(c_1418, plain, (ifeq2(entity(skc13, skc22), true, true, true)=true)). % 42.63/27.57 tff(c_72, plain, (![U_77, V_78, W_79]: (ifeq2(accessible_world(U_77, V_78), true, ifeq2(event(U_77, W_79), true, event(V_78, W_79), true), true)=true))). % 42.63/27.57 tff(c_2980, plain, (abstraction(skc13, skc24)=true)). % 42.63/27.57 tff(c_2925, plain, (impartial(skc13, skc19)=true)). % 42.63/27.57 tff(c_102, plain, (![U_122, V_123, W_124]: (ifeq2(accessible_world(U_122, V_123), true, ifeq2(man(U_122, W_124), true, man(V_123, W_124), true), true)=true))). % 42.63/27.57 tff(c_80, plain, (![U_89, V_90, W_91]: (ifeq2(accessible_world(U_89, V_90), true, ifeq2(specific(U_89, W_91), true, specific(V_90, W_91), true), true)=true))). % 42.63/27.57 tff(c_1374, plain, (ifeq2(abstraction(skc13, skc22), true, true, true)=true)). % 42.63/27.57 tff(c_2856, plain, (singleton(skc13, skc17)=true)). % 42.63/27.57 tff(c_106, plain, (![U_128, V_129, W_130]: (ifeq2(accessible_world(U_128, V_129), true, ifeq2(organism(U_128, W_130), true, organism(V_129, W_130), true), true)=true))). % 42.63/27.57 tff(c_2799, plain, (thing(skc13, skc14)=true)). % 42.63/27.57 tff(c_114, plain, (![U_140, V_141, W_142]: (ifeq2(accessible_world(U_140, V_141), true, ifeq2(living(U_140, W_142), true, living(V_141, W_142), true), true)=true))). % 42.63/27.57 tff(c_116, plain, (![U_143, V_144, W_145]: (ifeq2(accessible_world(U_143, V_144), true, ifeq2(human(U_143, W_145), true, human(V_144, W_145), true), true)=true))). % 42.63/27.57 tff(c_2691, plain, (entity(skc13, skc23)=true)). % 42.63/27.57 tff(c_98, plain, (![U_116, V_117, W_118]: (ifeq2(accessible_world(U_116, V_117), true, ifeq2(general(U_116, W_118), true, general(V_117, W_118), true), true)=true))). % 42.63/27.57 tff(c_2640, plain, (general(skc13, skc14)=true)). % 42.63/27.57 tff(c_1773, plain, (ifeq2(entity(skc14, skc26), true, true, true)=true)). % 42.63/27.57 tff(c_126, plain, (![U_158, V_159, W_160]: (ifeq2(accessible_world(U_158, V_159), true, ifeq2(vincent_forename(U_158, W_160), true, vincent_forename(V_159, W_160), true), true)=true))). % 42.63/27.57 tff(c_2588, plain, (singleton(skc14, skc26)=true)). % 42.63/27.57 tff(c_1962, plain, (ifeq2(entity(skc13, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_82, plain, (![U_92, V_93, W_94]: (ifeq2(accessible_world(U_92, V_93), true, ifeq2(nonexistent(U_92, W_94), true, nonexistent(V_93, W_94), true), true)=true))). % 42.63/27.57 tff(c_100, plain, (![U_119, V_120, W_121]: (ifeq2(accessible_world(U_119, V_120), true, ifeq2(state(U_119, W_121), true, state(V_120, W_121), true), true)=true))). % 42.63/27.57 tff(c_2395, plain, (entity(skc13, skc19)=true)). % 42.63/27.57 tff(c_122, plain, (![U_152, V_153, W_154]: (ifeq2(accessible_world(U_152, V_153), true, ifeq2(forename(U_152, W_154), true, forename(V_153, W_154), true), true)=true))). % 42.63/27.57 tff(c_2364, plain, (nonhuman(skc13, skc14)=true)). % 42.63/27.57 tff(c_1093, plain, (ifeq2(proposition(skc13, skc18), true, true, true)=true)). % 42.63/27.57 tff(c_96, plain, (![U_113, V_114, W_115]: (ifeq2(accessible_world(U_113, V_114), true, ifeq2(nonhuman(U_113, W_115), true, nonhuman(V_114, W_115), true), true)=true))). % 42.63/27.57 tff(c_1478, plain, (ifeq2(abstraction(skc13, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_1579, plain, (ifeq2(abstraction(skc13, skc17), true, true, true)=true)). % 42.63/27.57 tff(c_118, plain, (![U_146, V_147, W_148]: (ifeq2(accessible_world(U_146, V_147), true, ifeq2(animate(U_146, W_148), true, animate(V_147, W_148), true), true)=true))). % 42.63/27.57 tff(c_2219, plain, (singleton(skc13, skc15)=true)). % 42.63/27.57 tff(c_74, plain, (![U_80, V_81, W_82]: (ifeq2(accessible_world(U_80, V_81), true, ifeq2(eventuality(U_80, W_82), true, eventuality(V_81, W_82), true), true)=true))). % 42.63/27.57 tff(c_2157, plain, (ifeq2(entity(skc13, skc15), true, true, true)=true)). % 42.63/27.57 tff(c_84, plain, (![U_95, V_96, W_97]: (ifeq2(accessible_world(U_95, V_96), true, ifeq2(unisex(U_95, W_97), true, unisex(V_96, W_97), true), true)=true))). % 42.63/27.57 tff(c_2139, plain, (thing(skc13, skc15)=true)). % 42.63/27.57 tff(c_2071, plain, (unisex(skc13, skc17)=true)). % 42.63/27.57 tff(c_124, plain, (![U_155, V_156, W_157]: (ifeq2(accessible_world(U_155, V_156), true, ifeq2(relname(U_155, W_157), true, relname(V_156, W_157), true), true)=true))). % 42.63/27.57 tff(c_2031, plain, (unisex(skc14, skc26)=true)). % 42.63/27.57 tff(c_112, plain, (![U_137, V_138, W_139]: (ifeq2(accessible_world(U_137, V_138), true, ifeq2(impartial(U_137, W_139), true, impartial(V_138, W_139), true), true)=true))). % 42.63/27.57 tff(c_2007, plain, (human(skc13, skc19)=true)). % 42.63/27.57 tff(c_86, plain, (![U_98, W_99, V_100]: (ifeq2(present(U_98, W_99), true, ifeq2(accessible_world(U_98, V_100), true, present(V_100, W_99), true), true)=true))). % 42.63/27.57 tff(c_1947, plain, (specific(skc13, skc17)=true)). % 42.63/27.57 tff(c_92, plain, (![U_107, V_108, W_109]: (ifeq2(accessible_world(U_107, V_108), true, ifeq2(relation(U_107, W_109), true, relation(V_108, W_109), true), true)=true))). % 42.63/27.57 tff(c_1865, plain, (unisex(skc13, skc22)=true)). % 42.63/27.57 tff(c_1841, plain, (nonexistent(skc14, skc26)=true)). % 42.63/27.57 tff(c_222, plain, (![U_200, V_201]: (ifeq(tuple(specific(U_200, V_201), general(U_200, V_201)), tuple(true, true), a, b)=b))). % 42.63/27.57 tff(c_1801, plain, (specific(skc14, skc26)=true)). % 42.63/27.57 tff(c_220, plain, (![U_198, V_199]: (ifeq(tuple(unisex(U_198, V_199), male(U_198, V_199)), tuple(true, true), a, b)=b))). % 42.63/27.57 tff(c_1755, plain, (thing(skc14, skc26)=true)). % 42.63/27.58 tff(c_1715, plain, (specific(skc13, skc15)=true)). % 42.63/27.58 tff(c_226, plain, (![U_204, V_205]: (ifeq(tuple(nonexistent(U_204, V_205), existent(U_204, V_205)), tuple(true, true), a, b)=b))). % 42.63/27.58 tff(c_224, plain, (![U_202, V_203]: (ifeq(tuple(nonhuman(U_202, V_203), human(U_202, V_203)), tuple(true, true), a, b)=b))). % 42.63/27.58 tff(c_1683, plain, (human(skc13, skc23)=true)). % 42.63/27.58 tff(c_1653, plain, (organism(skc13, skc23)=true)). % 42.63/27.58 tff(c_1625, plain, (nonexistent(skc13, skc15)=true)). % 42.63/27.58 tff(c_1597, plain, (nonexistent(skc13, skc17)=true)). % 42.63/27.58 tff(c_1564, plain, (thing(skc13, skc17)=true)). % 42.63/27.58 tff(c_1531, plain, (nonexistent(skc13, skc22)=true)). % 42.63/27.58 tff(c_1510, plain, (animate(skc13, skc19)=true)). % 42.63/27.58 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 42.63/27.58 tff(c_1446, plain, (ifeq2(smoke(skc13, skc22), true, true, true)=true)). % 42.63/27.58 tff(c_1456, plain, (unisex(skc13, skc15)=true)). % 42.63/27.58 tff(c_48, plain, (![U_50, V_51]: (ifeq2(entity(U_50, V_51), true, existent(U_50, V_51), true)=true))). % 42.63/27.58 tff(c_1428, plain, (event(skc13, skc22)=true)). % 42.63/27.58 tff(c_1317, plain, (ifeq2(state(skc13, skc17), true, true, true)=true)). % 42.63/27.58 tff(c_46, plain, (![U_48, V_49]: (ifeq2(entity(U_48, V_49), true, specific(U_48, V_49), true)=true))). % 42.63/27.58 tff(c_1380, plain, (eventuality(skc13, skc15)=true)). % 42.63/27.58 tff(c_26, plain, (![U_28, V_29]: (ifeq2(abstraction(U_28, V_29), true, thing(U_28, V_29), true)=true))). % 42.63/27.58 tff(c_1311, plain, (ifeq2(state(skc13, skc15), true, true, true)=true)). % 42.63/27.58 tff(c_1308, plain, (ifeq2(state(skc14, skc26), true, true, true)=true)). % 42.63/27.58 tff(c_1323, plain, (eventuality(skc13, skc17)=true)). % 42.63/27.58 tff(c_36, plain, (![U_38, V_39]: (ifeq2(state(U_38, V_39), true, event(U_38, V_39), true)=true))). % 42.63/27.58 tff(c_1271, plain, (eventuality(skc14, skc26)=true)). % 42.63/27.58 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 42.63/27.58 tff(c_1222, plain, (organism(skc13, skc19)=true)). % 42.63/27.58 tff(c_1195, plain, (animate(skc13, skc23)=true)). % 42.63/27.58 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 42.63/27.58 tff(c_1155, plain, (human_person(skc13, skc19)=true)). % 42.63/27.58 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 42.63/27.58 tff(c_1121, plain, (human_person(skc13, skc23)=true)). % 42.63/27.58 tff(c_38, plain, (![U_40, V_41]: (ifeq2(man(U_40, V_41), true, human_person(U_40, V_41), true)=true))). % 42.63/27.58 tff(c_1081, plain, (relation(skc13, skc18)=true)). % 42.63/27.58 tff(c_799, plain, (ifeq2(relname(skc13, skc14), true, true, true)=true)). % 42.63/27.58 tff(c_42, plain, (![U_44, V_45]: (ifeq2(organism(U_44, V_45), true, entity(U_44, V_45), true)=true))). % 42.63/27.58 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, organism(U_42, V_43), true)=true))). % 42.63/27.58 tff(c_30, plain, (![U_32, V_33]: (ifeq2(abstraction(U_32, V_33), true, general(U_32, V_33), true)=true))). % 42.63/27.58 tff(c_965, plain, (relation(skc13, skc24)=true)). % 42.63/27.58 tff(c_28, plain, (![U_30, V_31]: (ifeq2(abstraction(U_30, V_31), true, nonhuman(U_30, V_31), true)=true))). % 42.63/27.58 tff(c_894, plain, (ifeq2(vincent_forename(skc13, skc24), true, true, true)=true)). % 42.63/27.58 tff(c_64, plain, (![U_66, V_67]: (ifeq2(vincent_forename(U_66, V_67), true, forename(U_66, V_67), true)=true))). % 42.63/27.58 tff(c_867, plain, (abstraction(skc13, skc14)=true)). % 42.63/27.58 tff(c_846, plain, (specific(skc13, skc22)=true)). % 42.63/27.58 tff(c_44, plain, (![U_46, V_47]: (ifeq2(entity(U_46, V_47), true, thing(U_46, V_47), true)=true))). % 42.63/27.58 tff(c_815, plain, (thing(skc13, skc22)=true)). % 42.63/27.58 tff(c_50, plain, (![U_52, V_53]: (ifeq2(organism(U_52, V_53), true, impartial(U_52, V_53), true)=true))). % 42.63/27.58 tff(c_781, plain, (relation(skc13, skc14)=true)). % 42.63/27.58 tff(c_745, plain, (eventuality(skc13, skc22)=true)). % 42.63/27.58 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))). % 42.63/27.58 tff(c_34, plain, (![U_36, V_37]: (ifeq2(state(U_36, V_37), true, eventuality(U_36, V_37), true)=true))). % 42.63/27.58 tff(c_680, plain, (relname(skc13, skc18)=true)). % 42.63/27.58 tff(c_22, plain, (![U_24, V_25]: (ifeq2(proposition(U_24, V_25), true, relation(U_24, V_25), true)=true))). % 42.63/27.58 tff(c_52, plain, (![U_54, V_55]: (ifeq2(organism(U_54, V_55), true, living(U_54, V_55), true)=true))). % 42.63/27.58 tff(c_588, plain, (relname(skc13, skc24)=true)). % 42.63/27.58 tff(c_60, plain, (![U_62, V_63]: (ifeq2(forename(U_62, V_63), true, relname(U_62, V_63), true)=true))). % 42.63/27.58 tff(c_24, plain, (![U_26, V_27]: (ifeq2(relation(U_26, V_27), true, abstraction(U_26, V_27), true)=true))). % 42.63/27.58 tff(c_505, plain, (ifeq2(jules_forename(skc13, skc18), true, true, true)=true)). % 42.63/27.58 tff(c_32, plain, (![U_34, V_35]: (ifeq2(abstraction(U_34, V_35), true, unisex(U_34, V_35), true)=true))). % 42.63/27.58 tff(c_526, plain, (male(skc13, skc19)=true)). % 42.63/27.58 tff(c_476, plain, (male(skc13, skc23)=true)). % 42.63/27.58 tff(c_66, plain, (![U_68, V_69]: (ifeq2(jules_forename(U_68, V_69), true, forename(U_68, V_69), true)=true))). % 42.63/27.58 tff(c_58, plain, (![U_60, V_61]: (ifeq2(man(U_60, V_61), true, male(U_60, V_61), true)=true))). % 42.63/27.58 tff(c_62, plain, (![U_64, V_65]: (ifeq2(relname(U_64, V_65), true, relation(U_64, V_65), true)=true))). % 42.63/27.58 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 42.63/27.58 tff(c_56, plain, (![U_58, V_59]: (ifeq2(human_person(U_58, V_59), true, animate(U_58, V_59), true)=true))). % 42.63/27.58 tff(c_426, plain, (ifeq2(smoke(skc13, skc17), true, true, true)=true)). % 42.63/27.58 tff(c_420, plain, (ifeq2(smoke(skc13, skc15), true, true, true)=true)). % 42.63/27.58 tff(c_8, plain, (![U_10, V_11]: (ifeq2(smoke(U_10, V_11), true, event(U_10, V_11), true)=true))). % 42.63/27.58 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 42.63/27.58 tff(c_54, plain, (![U_56, V_57]: (ifeq2(human_person(U_56, V_57), true, human(U_56, V_57), true)=true))). % 42.63/27.58 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 42.63/27.58 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 42.63/27.58 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 42.63/27.58 tff(c_210, plain, (be(skc13, skc22, skc23, skc23)=true)). % 42.63/27.58 tff(c_208, plain, (theme(skc13, skc15, skc14)=true)). % 42.63/27.58 tff(c_196, plain, (agent(skc14, skc26, skc23)=true)). % 42.63/27.58 tff(c_204, plain, (agent(skc13, skc15, skc19)=true)). % 42.63/27.58 tff(c_202, plain, (agent(skc13, skc17, skc19)=true)). % 42.63/27.58 tff(c_194, plain, (of(skc13, skc24, skc23)=true)). % 42.63/27.58 tff(c_200, plain, (of(skc13, skc18, skc19)=true)). % 42.63/27.58 tff(c_186, plain, (proposition(skc13, skc14)=true)). % 42.63/27.58 tff(c_188, plain, (accessible_world(skc13, skc14)=true)). % 42.63/27.58 tff(c_144, plain, (event(skc14, skc26)=true)). % 42.63/27.58 tff(c_146, plain, (jules_forename(skc13, skc24)=true)). % 42.63/27.58 tff(c_180, plain, (event(skc13, skc15)=true)). % 42.63/27.58 tff(c_178, plain, (present(skc13, skc15)=true)). % 42.63/27.58 tff(c_174, plain, (think_believe_consider(skc13, skc17)=true)). % 42.63/27.58 tff(c_148, plain, (forename(skc13, skc24)=true)). % 42.63/27.58 tff(c_190, plain, (state(skc13, skc22)=true)). % 42.63/27.58 tff(c_176, plain, (think_believe_consider(skc13, skc15)=true)). % 42.63/27.58 tff(c_154, plain, (present(skc14, skc26)=true)). % 42.63/27.58 tff(c_158, plain, (man(skc13, skc23)=true)). % 42.63/27.58 tff(c_172, plain, (present(skc13, skc17)=true)). % 42.63/27.58 tff(c_156, plain, (smoke(skc14, skc26)=true)). % 42.63/27.58 tff(c_170, plain, (event(skc13, skc17)=true)). % 42.63/27.58 tff(c_168, plain, (vincent_forename(skc13, skc18)=true)). % 42.63/27.58 tff(c_164, plain, (man(skc13, skc19)=true)). % 42.63/27.58 tff(c_166, plain, (forename(skc13, skc18)=true)). % 42.63/27.58 tff(c_142, plain, (actual_world(skc13)=true)). % 42.63/27.58 tff(c_228, plain, (b!=a)). % 42.63/27.58 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.63/27.58 %------------------------------------------------------------------------------