%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP249-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/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 : n021.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 40.08s 25.72s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : NLP249-10 : TPTP v9.0.0. Released v7.3.0. % 0.07/0.12 % 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.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 09:48:43 EDT 2025 % 0.12/0.33 % CPUTime : % 40.08/25.71 % 40.08/25.72 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.08/25.72 % 40.08/25.72 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.08/25.73 %$ 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 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 > skc15 > skc14 > skc13 > b > a % 40.08/25.73 % 40.08/25.73 %Foreground sorts: % 40.08/25.73 % 40.08/25.73 % 40.08/25.73 %Background operators: % 40.08/25.73 % 40.08/25.73 % 40.08/25.73 %Foreground operators: % 40.08/25.73 tff(agent, type, agent: ($i * $i * $i) > $i). % 40.08/25.73 tff(skc16, type, skc16: $i). % 40.08/25.73 tff(proposition, type, proposition: ($i * $i) > $i). % 40.08/25.73 tff(specific, type, specific: ($i * $i) > $i). % 40.08/25.73 tff(organism, type, organism: ($i * $i) > $i). % 40.08/25.73 tff(impartial, type, impartial: ($i * $i) > $i). % 40.08/25.73 tff(a, type, a: $i). % 40.08/25.73 tff(smoke, type, smoke: ($i * $i) > $i). % 40.08/25.73 tff(jules_forename, type, jules_forename: ($i * $i) > $i). % 40.08/25.73 tff(eventuality, type, eventuality: ($i * $i) > $i). % 40.08/25.73 tff(theme, type, theme: ($i * $i * $i) > $i). % 40.08/25.73 tff(skc18, type, skc18: $i). % 40.08/25.73 tff(state, type, state: ($i * $i) > $i). % 40.08/25.73 tff(tuple, type, tuple: ($i * $i) > $i). % 40.08/25.73 tff(skc25, type, skc25: $i). % 40.08/25.73 tff(human_person, type, human_person: ($i * $i) > $i). % 40.08/25.73 tff(skf1, type, skf1: $i > $i). % 40.08/25.73 tff(be, type, be: ($i * $i * $i * $i) > $i). % 40.08/25.73 tff(relname, type, relname: ($i * $i) > $i). % 40.08/25.73 tff(skc14, type, skc14: $i). % 40.08/25.73 tff(skc17, type, skc17: $i). % 40.08/25.73 tff(skc13, type, skc13: $i). % 40.08/25.73 tff(thing, type, thing: ($i * $i) > $i). % 40.08/25.73 tff(unisex, type, unisex: ($i * $i) > $i). % 40.08/25.73 tff(abstraction, type, abstraction: ($i * $i) > $i). % 40.08/25.73 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 40.08/25.73 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $i). % 40.08/25.73 tff(skc26, type, skc26: $i). % 40.08/25.73 tff(relation, type, relation: ($i * $i) > $i). % 40.08/25.73 tff(skc24, type, skc24: $i). % 40.08/25.73 tff(actual_world, type, actual_world: $i > $i). % 40.08/25.73 tff(of, type, of: ($i * $i * $i) > $i). % 40.08/25.73 tff(present, type, present: ($i * $i) > $i). % 40.08/25.73 tff(b, type, b: $i). % 40.08/25.73 tff(skc20, type, skc20: $i). % 40.08/25.73 tff(animate, type, animate: ($i * $i) > $i). % 40.08/25.73 tff(human, type, human: ($i * $i) > $i). % 40.08/25.73 tff(skc21, type, skc21: $i). % 40.08/25.73 tff(skc22, type, skc22: $i). % 40.08/25.73 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 40.08/25.73 tff(skc15, type, skc15: $i). % 40.08/25.73 tff(existent, type, existent: ($i * $i) > $i). % 40.08/25.73 tff(accessible_world, type, accessible_world: ($i * $i) > $i). % 40.08/25.73 tff(forename, type, forename: ($i * $i) > $i). % 40.08/25.73 tff(true, type, true: $i). % 40.08/25.73 tff(vincent_forename, type, vincent_forename: ($i * $i) > $i). % 40.08/25.73 tff(male, type, male: ($i * $i) > $i). % 40.08/25.73 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 40.08/25.73 tff(entity, type, entity: ($i * $i) > $i). % 40.08/25.73 tff(skc19, type, skc19: $i). % 40.08/25.73 tff(singleton, type, singleton: ($i * $i) > $i). % 40.08/25.73 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 40.08/25.73 tff(event, type, event: ($i * $i) > $i). % 40.08/25.73 tff(man, type, man: ($i * $i) > $i). % 40.08/25.73 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 40.08/25.73 tff(general, type, general: ($i * $i) > $i). % 40.08/25.73 tff(living, type, living: ($i * $i) > $i). % 40.08/25.73 % 40.08/25.73 %Saturated clause set: % 40.08/25.73 tff(c_40449, 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))). % 40.08/25.73 tff(c_40401, plain, (![Y_189, W_185, V_190]: (ifeq3(theme(skc14, Y_189, W_185), true, ifeq3(theme(skc14, skf1(skc25), V_190), true, ifeq3(agent(skc14, Y_189, skc25), true, ifeq3(think_believe_consider(skc14, Y_189), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), 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))). % 40.08/25.73 tff(c_40377, plain, (![W_1600, V_1602]: (ifeq3(theme(skc14, skf1(skc25), W_1600), true, ifeq3(theme(skc14, skf1(skc25), V_1602), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1600), true, ifeq3(proposition(skc14, V_1602), true, V_1602, W_1600), W_1600), W_1600), W_1600), W_1600), W_1600)=W_1600))). % 40.08/25.73 tff(c_40346, plain, (![W_185, X_188, V_190]: (ifeq3(theme(skc14, skf1(skc25), W_185), true, ifeq3(theme(skc14, X_188, V_190), true, ifeq3(agent(skc14, X_188, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), 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))). % 40.08/25.73 tff(c_40319, plain, (![W_1595, V_1597]: (ifeq3(theme(skc14, skf1(skc19), W_1595), true, ifeq3(theme(skc14, skf1(skc19), V_1597), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1595), true, ifeq3(proposition(skc14, V_1597), true, V_1597, W_1595), W_1595), W_1595), W_1595), W_1595), W_1595)=W_1595))). % 40.08/25.73 tff(c_29316, 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))). % 40.08/25.73 tff(c_39111, plain, (![X_1541, V_1542]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, X_1541, V_1542), true, ifeq3(agent(skc14, X_1541, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1541), true, ifeq3(proposition(skc14, V_1542), true, V_1542, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.73 tff(c_39767, plain, (![W_1568, V_1570]: (ifeq3(theme(skc14, skc15, W_1568), true, ifeq3(theme(skc14, skf1(skc25), V_1570), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1568), true, ifeq3(proposition(skc14, V_1570), true, V_1570, W_1568), W_1568), W_1568), W_1568), W_1568), W_1568)=W_1568))). % 40.08/25.73 tff(c_39114, plain, (![Y_1540, V_1542]: (ifeq3(theme(skc14, Y_1540, skc14), true, ifeq3(theme(skc14, skf1(skc25), V_1542), true, ifeq3(agent(skc14, Y_1540, skc25), true, ifeq3(think_believe_consider(skc14, Y_1540), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1542), true, V_1542, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.73 tff(c_39314, plain, (![W_1549, X_1550]: (ifeq3(theme(skc14, skf1(skc19), W_1549), true, ifeq3(theme(skc14, X_1550, skc14), true, ifeq3(agent(skc14, X_1550, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1550), true, ifeq3(proposition(skc14, W_1549), true, skc14, W_1549), W_1549), W_1549), W_1549), W_1549), W_1549)=W_1549))). % 40.08/25.73 tff(c_39317, plain, (![Y_1548, W_1549]: (ifeq3(theme(skc14, Y_1548, W_1549), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, Y_1548, skc25), true, ifeq3(think_believe_consider(skc14, Y_1548), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1549), true, skc14, W_1549), W_1549), W_1549), W_1549), W_1549), W_1549)=W_1549))). % 40.08/25.73 tff(c_39975, plain, (![W_1582]: (ifeq3(theme(skc14, skf1(skc25), W_1582), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1582), true, skc14, W_1582), W_1582), W_1582), W_1582), W_1582)=W_1582))). % 40.08/25.73 tff(c_39316, plain, (![W_1549, X_1550]: (ifeq3(theme(skc14, skf1(skc25), W_1549), true, ifeq3(theme(skc14, X_1550, skc14), true, ifeq3(agent(skc14, X_1550, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, X_1550), true, ifeq3(proposition(skc14, W_1549), true, skc14, W_1549), W_1549), W_1549), W_1549), W_1549), W_1549)=W_1549))). % 40.08/25.73 tff(c_39921, plain, (![V_1580]: (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, skf1(skc25), V_1580), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1580), true, V_1580, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39113, plain, (![X_1541, V_1542]: (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, X_1541, V_1542), true, ifeq3(agent(skc14, X_1541, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, X_1541), true, ifeq3(proposition(skc14, V_1542), true, V_1542, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39865, plain, (![V_1577]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skf1(skc19), V_1577), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1577), true, V_1577, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39112, plain, (![Y_1540, V_1542]: (ifeq3(theme(skc14, Y_1540, skc14), true, ifeq3(theme(skc14, skf1(skc19), V_1542), true, ifeq3(agent(skc14, Y_1540, skc19), true, ifeq3(think_believe_consider(skc14, Y_1540), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1542), true, V_1542, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38565, plain, (![W_1509, V_1510]: (ifeq3(theme(skc14, skf1(skc25), W_1509), true, ifeq3(theme(skc14, skc17, V_1510), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1509), true, ifeq3(proposition(skc14, V_1510), true, V_1510, W_1509), W_1509), W_1509), W_1509), W_1509), W_1509)=W_1509))). % 40.08/25.74 tff(c_38636, plain, (![W_1512, V_1514]: (ifeq3(theme(skc14, skc17, W_1512), true, ifeq3(theme(skc14, skf1(skc25), V_1514), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1512), true, ifeq3(proposition(skc14, V_1514), true, V_1514, W_1512), W_1512), W_1512), W_1512), W_1512), W_1512)=W_1512))). % 40.08/25.74 tff(c_6334, 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))). % 40.08/25.74 tff(c_38811, plain, (![W_1524, V_1525]: (ifeq3(theme(skc14, skf1(skc25), W_1524), true, ifeq3(theme(skc14, skc15, V_1525), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1524), true, ifeq3(proposition(skc14, V_1525), true, V_1525, W_1524), W_1524), W_1524), W_1524), W_1524), W_1524)=W_1524))). % 40.08/25.74 tff(c_39665, plain, (![W_1564]: (ifeq3(theme(skc14, skf1(skc19), W_1564), 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_1564), true, skc14, W_1564), W_1564), W_1564), W_1564), W_1564)=W_1564))). % 40.08/25.74 tff(c_39315, plain, (![Y_1548, W_1549]: (ifeq3(theme(skc14, Y_1548, W_1549), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(agent(skc14, Y_1548, skc19), true, ifeq3(think_believe_consider(skc14, Y_1548), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1549), true, skc14, W_1549), W_1549), W_1549), W_1549), W_1549), W_1549)=W_1549))). % 40.08/25.74 tff(c_38818, plain, (![W_1524, V_1525, Z_1526]: (ifeq3(theme(skc14, skc15, W_1524), true, ifeq3(theme(skc14, skc15, V_1525), true, ifeq3(agent(skc14, skc15, Z_1526), true, ifeq3(agent(skc14, skc15, Z_1526), true, ifeq3(proposition(skc14, W_1524), true, ifeq3(proposition(skc14, V_1525), true, V_1525, W_1524), W_1524), W_1524), W_1524), W_1524), W_1524)=W_1524))). % 40.08/25.74 tff(c_39556, plain, (![W_1556]: (ifeq3(theme(skc14, skc15, W_1556), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1556), true, skc14, W_1556), W_1556), W_1556), W_1556), W_1556)=W_1556))). % 40.08/25.74 tff(c_39326, plain, (![W_1549, X_1550, Z_1551]: (ifeq3(theme(skc14, skc15, W_1549), true, ifeq3(theme(skc14, X_1550, skc14), true, ifeq3(agent(skc14, skc15, Z_1551), true, ifeq3(agent(skc14, X_1550, Z_1551), true, ifeq3(think_believe_consider(skc14, X_1550), true, ifeq3(proposition(skc14, W_1549), true, skc14, W_1549), W_1549), W_1549), W_1549), W_1549), W_1549)=W_1549))). % 40.08/25.74 tff(c_39222, plain, (![Y_1545]: (ifeq3(theme(skc14, Y_1545, skc14), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, Y_1545, skc25), true, ifeq3(think_believe_consider(skc14, Y_1545), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39220, plain, (![Y_1545]: (ifeq3(theme(skc14, Y_1545, skc14), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(agent(skc14, Y_1545, skc19), true, ifeq3(think_believe_consider(skc14, Y_1545), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39395, 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)). % 40.08/25.74 tff(c_39219, plain, (![X_1546]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, X_1546, skc14), true, ifeq3(agent(skc14, X_1546, skc19), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, X_1546), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39355, plain, (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 40.08/25.74 tff(c_39221, plain, (![X_1546]: (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, X_1546, skc14), true, ifeq3(agent(skc14, X_1546, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(think_believe_consider(skc14, X_1546), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39237, 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))). % 40.08/25.74 tff(c_39127, plain, (![Y_1540, X_1541, Z_1543]: (ifeq3(theme(skc14, Y_1540, skc14), true, ifeq3(theme(skc14, X_1541, skc14), true, ifeq3(agent(skc14, Y_1540, Z_1543), true, ifeq3(agent(skc14, X_1541, Z_1543), true, ifeq3(think_believe_consider(skc14, Y_1540), true, ifeq3(think_believe_consider(skc14, X_1541), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_39035, plain, (![W_1537]: (ifeq3(theme(skc14, skc17, W_1537), true, ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1537), true, skc14, W_1537), W_1537), W_1537), W_1537), W_1537)=W_1537))). % 40.08/25.74 tff(c_39046, 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))). % 40.08/25.74 tff(c_38646, plain, (![W_1512, X_1513, Z_1515]: (ifeq3(theme(skc14, skc17, W_1512), true, ifeq3(theme(skc14, X_1513, skc14), true, ifeq3(agent(skc14, skc17, Z_1515), true, ifeq3(agent(skc14, X_1513, Z_1515), true, ifeq3(think_believe_consider(skc14, X_1513), true, ifeq3(proposition(skc14, W_1512), true, skc14, W_1512), W_1512), W_1512), W_1512), W_1512), W_1512)=W_1512))). % 40.08/25.74 tff(c_38819, plain, (![W_1524, V_1525, Z_1526]: (ifeq3(theme(skc14, skc17, W_1524), true, ifeq3(theme(skc14, skc15, V_1525), true, ifeq3(agent(skc14, skc17, Z_1526), true, ifeq3(agent(skc14, skc15, Z_1526), true, ifeq3(proposition(skc14, W_1524), true, ifeq3(proposition(skc14, V_1525), true, V_1525, W_1524), W_1524), W_1524), W_1524), W_1524), W_1524)=W_1524))). % 40.08/25.74 tff(c_38910, plain, (![V_1531]: (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, skc15, V_1531), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1531), true, V_1531, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38820, plain, (![Y_1523, V_1525, Z_1526]: (ifeq3(theme(skc14, Y_1523, skc14), true, ifeq3(theme(skc14, skc15, V_1525), true, ifeq3(agent(skc14, Y_1523, Z_1526), true, ifeq3(agent(skc14, skc15, Z_1526), true, ifeq3(think_believe_consider(skc14, Y_1523), true, ifeq3(proposition(skc14, V_1525), true, V_1525, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38573, plain, (![W_1509, V_1510, Z_1511]: (ifeq3(theme(skc14, skc17, W_1509), true, ifeq3(theme(skc14, skc17, V_1510), true, ifeq3(agent(skc14, skc17, Z_1511), true, ifeq3(agent(skc14, skc17, Z_1511), true, ifeq3(proposition(skc14, W_1509), true, ifeq3(proposition(skc14, V_1510), true, V_1510, W_1509), W_1509), W_1509), W_1509), W_1509), W_1509)=W_1509))). % 40.08/25.74 tff(c_38761, 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))). % 40.08/25.74 tff(c_38735, plain, (![V_1520]: (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(theme(skc14, skc17, V_1520), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1520), true, V_1520, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38574, plain, (![Y_1508, V_1510, Z_1511]: (ifeq3(theme(skc14, Y_1508, skc14), true, ifeq3(theme(skc14, skc17, V_1510), true, ifeq3(agent(skc14, Y_1508, Z_1511), true, ifeq3(agent(skc14, skc17, Z_1511), true, ifeq3(think_believe_consider(skc14, Y_1508), true, ifeq3(proposition(skc14, V_1510), true, V_1510, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38572, plain, (![W_1509, V_1510, Z_1511]: (ifeq3(theme(skc14, skc15, W_1509), true, ifeq3(theme(skc14, skc17, V_1510), true, ifeq3(agent(skc14, skc15, Z_1511), true, ifeq3(agent(skc14, skc17, Z_1511), true, ifeq3(proposition(skc14, W_1509), true, ifeq3(proposition(skc14, V_1510), true, V_1510, W_1509), W_1509), W_1509), W_1509), W_1509), W_1509)=W_1509))). % 40.08/25.74 tff(c_6299, 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))). % 40.08/25.74 tff(c_6300, 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))). % 40.08/25.74 tff(c_29314, plain, (![W_406, V_405]: (ifeq3(theme(skc14, skc21, W_406), true, ifeq3(theme(skc14, skf1(skc19), V_405), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), 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))). % 40.08/25.74 tff(c_29313, plain, (![W_406, V_405]: (ifeq3(theme(skc14, skf1(skc19), W_406), true, ifeq3(theme(skc14, skc21, V_405), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.08/25.74 tff(c_27959, plain, (![W_1002, V_1004, Z_1005]: (ifeq3(theme(skc13, skc17, W_1002), true, ifeq3(theme(skc13, skc17, V_1004), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(proposition(skc13, W_1002), true, ifeq3(proposition(skc13, V_1004), true, V_1004, W_1002), W_1002), W_1002), W_1002), W_1002), W_1002)=W_1002))). % 40.08/25.74 tff(c_38366, plain, (![Y_1010, V_1012, Z_1013]: (ifeq3(theme(skc13, Y_1010, skc14), true, ifeq3(theme(skc13, skc15, V_1012), true, ifeq3(agent(skc13, Y_1010, Z_1013), true, ifeq3(agent(skc13, skc15, Z_1013), true, ifeq3(think_believe_consider(skc13, Y_1010), true, ifeq3(proposition(skc13, V_1012), true, V_1012, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_27803, plain, (![W_985, V_987, Z_988]: (ifeq3(theme(skc13, skc15, W_985), true, ifeq3(theme(skc13, skc15, V_987), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(proposition(skc13, W_985), true, ifeq3(proposition(skc13, V_987), true, V_987, W_985), W_985), W_985), W_985), W_985), W_985)=W_985))). % 40.08/25.74 tff(c_27960, plain, (![W_1002, V_1004, Z_1005]: (ifeq3(theme(skc13, skc17, W_1002), true, ifeq3(theme(skc13, skc15, V_1004), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(agent(skc13, skc15, Z_1005), true, ifeq3(proposition(skc13, W_1002), true, ifeq3(proposition(skc13, V_1004), true, V_1004, W_1002), W_1002), W_1002), W_1002), W_1002), W_1002)=W_1002))). % 40.08/25.74 tff(c_38105, plain, (![W_1481, V_1483]: (ifeq3(theme(skc14, skc15, W_1481), true, ifeq3(theme(skc14, skf1(skc19), V_1483), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1481), true, ifeq3(proposition(skc14, V_1483), true, V_1483, W_1481), W_1481), W_1481), W_1481), W_1481)=W_1481))). % 40.08/25.74 tff(c_38175, plain, (![W_1484]: (ifeq3(theme(skc14, skc15, W_1484), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1484), true, skc14, W_1484), W_1484), W_1484), W_1484)=W_1484))). % 40.08/25.74 tff(c_38185, plain, (![Y_938, X_939, Z_941]: (ifeq3(theme(skc13, Y_938, skc14), true, ifeq3(theme(skc13, X_939, skc14), true, ifeq3(agent(skc13, Y_938, Z_941), true, ifeq3(agent(skc13, X_939, Z_941), true, ifeq3(think_believe_consider(skc13, Y_938), true, ifeq3(think_believe_consider(skc13, X_939), true, skc14, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.74 tff(c_38114, plain, (![W_1481, X_1482]: (ifeq3(theme(skc14, skc15, W_1481), true, ifeq3(theme(skc14, X_1482, skc14), true, ifeq3(agent(skc14, X_1482, skc19), true, ifeq3(think_believe_consider(skc14, X_1482), true, ifeq3(proposition(skc14, W_1481), true, skc14, W_1481), W_1481), W_1481), W_1481), W_1481)=W_1481))). % 40.08/25.74 tff(c_15044, 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))). % 40.08/25.74 tff(c_38018, plain, (![W_1478]: (ifeq3(theme(skc14, skc21, W_1478), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1478), true, skc14, W_1478), W_1478), W_1478), W_1478), W_1478)=W_1478))). % 40.08/25.74 tff(c_26579, plain, (![W_922, X_923]: (ifeq3(theme(skc14, skc21, W_922), true, ifeq3(theme(skc14, X_923, skc14), true, ifeq3(agent(skc14, X_923, skc19), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, X_923), true, ifeq3(proposition(skc14, W_922), true, skc14, W_922), W_922), W_922), W_922), W_922), W_922)=W_922))). % 40.08/25.75 tff(c_37918, plain, (![W_1476]: (ifeq3(theme(skc14, skf1(skc19), W_1476), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_1476), true, skc14, W_1476), W_1476), W_1476), W_1476), W_1476)=W_1476))). % 40.08/25.75 tff(c_26726, plain, (![Y_929, W_930]: (ifeq3(theme(skc14, Y_929, W_930), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(agent(skc14, Y_929, skc19), true, ifeq3(think_believe_consider(skc14, Y_929), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_930), true, skc14, W_930), W_930), W_930), W_930), W_930), W_930)=W_930))). % 40.08/25.75 tff(c_37791, plain, (![V_1472]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc21, V_1472), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_1472), true, V_1472, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37839, plain, (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(think_believe_consider(skc14, skc21), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 40.08/25.75 tff(c_37798, plain, (![Y_1471]: (ifeq3(theme(skc14, Y_1471, skc14), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(agent(skc14, Y_1471, skc19), true, ifeq3(think_believe_consider(skc14, Y_1471), true, ifeq3(think_believe_consider(skc14, skc21), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37748, plain, (![Y_929, V_931]: (ifeq3(theme(skc14, Y_929, skc14), true, ifeq3(theme(skc14, skc21, V_931), true, ifeq3(agent(skc14, Y_929, skc19), true, ifeq3(think_believe_consider(skc14, Y_929), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_931), true, V_931, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37288, plain, (![W_1445, V_1446]: (ifeq3(theme(skc14, skf1(skc19), W_1445), true, ifeq3(theme(skc14, skc17, V_1446), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1445), true, ifeq3(proposition(skc14, V_1446), true, V_1446, W_1445), W_1445), W_1445), W_1445), W_1445)=W_1445))). % 40.08/25.75 tff(c_37489, plain, (![W_1455, V_1457]: (ifeq3(theme(skc14, skc17, W_1455), true, ifeq3(theme(skc14, skf1(skc19), V_1457), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1455), true, ifeq3(proposition(skc14, V_1457), true, V_1457, W_1455), W_1455), W_1455), W_1455), W_1455)=W_1455))). % 40.08/25.75 tff(c_37209, plain, (![W_1440, V_1441]: (ifeq3(theme(skc14, skf1(skc19), W_1440), true, ifeq3(theme(skc14, skc15, V_1441), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1440), true, ifeq3(proposition(skc14, V_1441), true, V_1441, W_1440), W_1440), W_1440), W_1440), W_1440)=W_1440))). % 40.08/25.75 tff(c_37646, plain, (![W_1462]: (ifeq3(theme(skc14, skc17, W_1462), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1462), true, skc14, W_1462), W_1462), W_1462), W_1462)=W_1462))). % 40.08/25.75 tff(c_37498, plain, (![W_1455, X_1456]: (ifeq3(theme(skc14, skc17, W_1455), true, ifeq3(theme(skc14, X_1456, skc14), true, ifeq3(agent(skc14, X_1456, skc19), true, ifeq3(think_believe_consider(skc14, X_1456), true, ifeq3(proposition(skc14, W_1455), true, skc14, W_1455), W_1455), W_1455), W_1455), W_1455)=W_1455))). % 40.08/25.75 tff(c_37562, plain, (![V_1460]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc15, V_1460), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1460), true, V_1460, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37217, plain, (![Y_1439, V_1441]: (ifeq3(theme(skc14, Y_1439, skc14), true, ifeq3(theme(skc14, skc15, V_1441), true, ifeq3(agent(skc14, Y_1439, skc19), true, ifeq3(think_believe_consider(skc14, Y_1439), true, ifeq3(proposition(skc14, V_1441), true, V_1441, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37426, plain, (![V_1454]: (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(theme(skc14, skc17, V_1454), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1454), true, V_1454, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37436, 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))). % 40.08/25.75 tff(c_37296, plain, (![Y_1444, V_1446]: (ifeq3(theme(skc14, Y_1444, skc14), true, ifeq3(theme(skc14, skc17, V_1446), true, ifeq3(agent(skc14, Y_1444, skc19), true, ifeq3(think_believe_consider(skc14, Y_1444), true, ifeq3(proposition(skc14, V_1446), true, V_1446, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37292, plain, (![W_1445, V_1446]: (ifeq3(theme(skc14, skc15, W_1445), true, ifeq3(theme(skc14, skc17, V_1446), true, ifeq3(proposition(skc14, W_1445), true, ifeq3(proposition(skc14, V_1446), true, V_1446, W_1445), W_1445), W_1445), W_1445)=W_1445))). % 40.08/25.75 tff(c_37291, plain, (![W_1445, V_1446]: (ifeq3(theme(skc14, skc17, W_1445), true, ifeq3(theme(skc14, skc17, V_1446), true, ifeq3(proposition(skc14, W_1445), true, ifeq3(proposition(skc14, V_1446), true, V_1446, W_1445), W_1445), W_1445), W_1445)=W_1445))). % 40.08/25.75 tff(c_37212, plain, (![W_1440, V_1441]: (ifeq3(theme(skc14, skc15, W_1440), true, ifeq3(theme(skc14, skc15, V_1441), true, ifeq3(proposition(skc14, W_1440), true, ifeq3(proposition(skc14, V_1441), true, V_1441, W_1440), W_1440), W_1440), W_1440)=W_1440))). % 40.08/25.75 tff(c_37245, 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))). % 40.08/25.75 tff(c_37211, plain, (![W_1440, V_1441]: (ifeq3(theme(skc14, skc17, W_1440), true, ifeq3(theme(skc14, skc15, V_1441), true, ifeq3(proposition(skc14, W_1440), true, ifeq3(proposition(skc14, V_1441), true, V_1441, W_1440), W_1440), W_1440), W_1440)=W_1440))). % 40.08/25.75 tff(c_37166, 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))). % 40.08/25.75 tff(c_37038, plain, (![V_1433]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skf1(skc19), V_1433), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1433), true, V_1433, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_27958, plain, (![W_1002, X_1003, Z_1005]: (ifeq3(theme(skc13, skc17, W_1002), true, ifeq3(theme(skc13, X_1003, skc14), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(agent(skc13, X_1003, Z_1005), true, ifeq3(think_believe_consider(skc13, X_1003), true, ifeq3(proposition(skc13, W_1002), true, skc14, W_1002), W_1002), W_1002), W_1002), W_1002), W_1002)=W_1002))). % 40.08/25.75 tff(c_37078, plain, (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 40.08/25.75 tff(c_37045, plain, (![X_1432]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, X_1432, skc14), true, ifeq3(agent(skc14, X_1432, skc19), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, X_1432), true, skc14, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_37003, plain, (![X_923, V_924]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, X_923, V_924), true, ifeq3(agent(skc14, X_923, skc19), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, X_923), true, ifeq3(proposition(skc14, V_924), true, V_924, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36854, plain, (![V_1423]: (ifeq3(theme(skc14, skf1(skc25), V_1423), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1423), true, V_1423, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36862, plain, (![X_1422, Z_1424]: (ifeq3(theme(skc14, X_1422, skc14), true, ifeq3(agent(skc14, skc15, Z_1424), true, ifeq3(agent(skc14, X_1422, Z_1424), true, ifeq3(think_believe_consider(skc14, X_1422), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36861, plain, (![V_1423, Z_1424]: (ifeq3(theme(skc14, skc17, V_1423), true, ifeq3(agent(skc14, skc15, Z_1424), true, ifeq3(agent(skc14, skc17, Z_1424), true, ifeq3(proposition(skc14, V_1423), true, V_1423, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36860, plain, (![V_1423, Z_1424]: (ifeq3(theme(skc14, skc15, V_1423), true, ifeq3(agent(skc14, skc15, Z_1424), true, ifeq3(agent(skc14, skc15, Z_1424), true, ifeq3(proposition(skc14, V_1423), true, V_1423, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36802, 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))). % 40.08/25.75 tff(c_36271, plain, (![V_1392]: (ifeq3(theme(skc14, skf1(skc25), V_1392), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35985, plain, (![W_1377]: (ifeq3(theme(skc14, skf1(skc25), W_1377), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1377), true, skc14, W_1377), W_1377), W_1377), W_1377)=W_1377))). % 40.08/25.75 tff(c_36712, plain, (![Y_938, V_940, Z_941]: (ifeq3(theme(skc13, Y_938, skc14), true, ifeq3(theme(skc13, skc17, V_940), true, ifeq3(agent(skc13, Y_938, Z_941), true, ifeq3(agent(skc13, skc17, Z_941), true, ifeq3(think_believe_consider(skc13, Y_938), true, ifeq3(proposition(skc13, V_940), true, V_940, skc14), skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35850, plain, (![W_1369]: (ifeq3(theme(skc14, skf1(skc25), W_1369), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369), W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_36277, plain, (![V_1392, Z_1393]: (ifeq3(theme(skc14, skc15, V_1392), true, ifeq3(agent(skc14, skc17, Z_1393), true, ifeq3(agent(skc14, skc15, Z_1393), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35857, plain, (![W_1369, Z_1370]: (ifeq3(theme(skc14, skc17, W_1369), true, ifeq3(agent(skc14, skc17, Z_1370), true, ifeq3(agent(skc14, skc17, Z_1370), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369), W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_35991, plain, (![W_1377, Z_1378]: (ifeq3(theme(skc14, skc15, W_1377), true, ifeq3(agent(skc14, skc15, Z_1378), true, ifeq3(agent(skc14, skc15, Z_1378), true, ifeq3(proposition(skc14, W_1377), true, skc14, W_1377), W_1377), W_1377), W_1377)=W_1377))). % 40.08/25.75 tff(c_36278, plain, (![V_1392, Z_1393]: (ifeq3(theme(skc14, skc17, V_1392), true, ifeq3(agent(skc14, skc17, Z_1393), true, ifeq3(agent(skc14, skc17, Z_1393), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36279, plain, (![X_1391, Z_1393]: (ifeq3(theme(skc14, X_1391, skc14), true, ifeq3(agent(skc14, skc17, Z_1393), true, ifeq3(agent(skc14, X_1391, Z_1393), true, ifeq3(think_believe_consider(skc14, X_1391), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35992, plain, (![W_1377, Z_1378]: (ifeq3(theme(skc14, skc17, W_1377), true, ifeq3(agent(skc14, skc17, Z_1378), true, ifeq3(agent(skc14, skc15, Z_1378), true, ifeq3(proposition(skc14, W_1377), true, skc14, W_1377), W_1377), W_1377), W_1377)=W_1377))). % 40.08/25.75 tff(c_36443, plain, (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, skc17, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, skc14, skc14), skc14), skc14)=skc14)). % 40.08/25.75 tff(c_36452, plain, (![W_978, X_979, Z_980]: (ifeq3(theme(skc13, skc15, W_978), true, ifeq3(theme(skc13, X_979, skc14), true, ifeq3(agent(skc13, skc15, Z_980), true, ifeq3(agent(skc13, X_979, Z_980), true, ifeq3(think_believe_consider(skc13, X_979), true, ifeq3(proposition(skc13, W_978), true, skc14, W_978), W_978), W_978), W_978), W_978), W_978)=W_978))). % 40.08/25.75 tff(c_35858, plain, (![Y_1368, Z_1370]: (ifeq3(theme(skc14, Y_1368, skc14), true, ifeq3(agent(skc14, Y_1368, Z_1370), true, ifeq3(agent(skc14, skc17, Z_1370), true, ifeq3(think_believe_consider(skc14, Y_1368), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36273, plain, (![X_1391, V_1392]: (ifeq3(theme(skc14, X_1391, V_1392), true, ifeq3(agent(skc14, X_1391, skc19), true, ifeq3(think_believe_consider(skc14, X_1391), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36270, plain, (![V_1392]: (ifeq3(theme(skc14, skf1(skc19), V_1392), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36275, plain, (![V_1392]: (ifeq3(theme(skc14, skc15, V_1392), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36274, plain, (![V_1392]: (ifeq3(theme(skc14, skc17, V_1392), true, ifeq3(proposition(skc14, V_1392), true, V_1392, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_36219, 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))). % 40.08/25.75 tff(c_36206, plain, (ifeq3(theme(skc14, skf1(skc25), skc14), true, ifeq3(agent(skc14, skc15, skc25), true, ifeq3(think_believe_consider(skc14, skf1(skc25)), true, skc14, skc14), skc14), skc14)=skc14)). % 40.08/25.75 tff(c_35993, plain, (![Y_1376, Z_1378]: (ifeq3(theme(skc14, Y_1376, skc14), true, ifeq3(agent(skc14, Y_1376, Z_1378), true, ifeq3(agent(skc14, skc15, Z_1378), true, ifeq3(think_believe_consider(skc14, Y_1376), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35856, plain, (![W_1369, Z_1370]: (ifeq3(theme(skc14, skc15, W_1369), true, ifeq3(agent(skc14, skc15, Z_1370), true, ifeq3(agent(skc14, skc17, Z_1370), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369), W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_27802, plain, (![W_985, V_987, Z_988]: (ifeq3(theme(skc13, skc15, W_985), true, ifeq3(theme(skc13, skc17, V_987), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(agent(skc13, skc17, Z_988), true, ifeq3(proposition(skc13, W_985), true, ifeq3(proposition(skc13, V_987), true, V_987, W_985), W_985), W_985), W_985), W_985), W_985)=W_985))). % 40.08/25.75 tff(c_36068, plain, (![Y_1381]: (ifeq3(theme(skc14, Y_1381, skc14), true, ifeq3(agent(skc14, Y_1381, skc19), true, ifeq3(think_believe_consider(skc14, Y_1381), true, skc14, skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35853, plain, (![Y_1368, W_1369]: (ifeq3(theme(skc14, Y_1368, W_1369), true, ifeq3(agent(skc14, Y_1368, skc19), true, ifeq3(think_believe_consider(skc14, Y_1368), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369), W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_35990, plain, (![Z_1378]: (ifeq3(agent(skc14, skc15, Z_1378), true, ifeq3(agent(skc14, skc15, Z_1378), true, skc14, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35986, plain, (![Z_1378]: (ifeq3(agent(skc14, skc17, Z_1378), true, ifeq3(agent(skc14, skc15, Z_1378), true, skc14, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_14809, 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))). % 40.08/25.75 tff(c_35937, plain, (ifeq3(theme(skc14, skf1(skc19), skc14), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, skc14, skc14), skc14)=skc14)). % 40.08/25.75 tff(c_35849, plain, (![W_1369]: (ifeq3(theme(skc14, skf1(skc19), W_1369), true, ifeq3(think_believe_consider(skc14, skf1(skc19)), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_35855, plain, (![Z_1370]: (ifeq3(agent(skc14, skc15, Z_1370), true, ifeq3(agent(skc14, skc17, Z_1370), true, skc14, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35851, plain, (![Z_1370]: (ifeq3(agent(skc14, skc17, Z_1370), true, ifeq3(agent(skc14, skc17, Z_1370), true, skc14, skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35854, plain, (![W_1369]: (ifeq3(theme(skc14, skc15, W_1369), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_35852, plain, (![W_1369]: (ifeq3(theme(skc14, skc17, W_1369), true, ifeq3(proposition(skc14, W_1369), true, skc14, W_1369), W_1369)=W_1369))). % 40.08/25.75 tff(c_35806, 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))). % 40.08/25.75 tff(c_35765, plain, (![W_1364]: (ifeq3(theme(skc14, skc21, W_1364), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_1364), true, skc14, W_1364), W_1364), W_1364), W_1364), W_1364)=W_1364))). % 40.08/25.75 tff(c_35776, plain, (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skc21), true, skc14, skc14), skc14), skc14), skc14)=skc14)). % 40.08/25.75 tff(c_35764, plain, (![V_1365]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skc21, V_1365), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_1365), true, V_1365, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_26727, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc21, W_930), true, ifeq3(theme(skc14, skc21, V_931), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.08/25.75 tff(c_28288, 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))). % 40.08/25.75 tff(c_28289, 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))). % 40.08/25.75 tff(c_35584, plain, (![Y_911, V_913]: (ifeq3(theme(skc13, Y_911, skc14), true, ifeq3(theme(skc13, skc17, V_913), true, ifeq3(agent(skc13, Y_911, skc19), true, ifeq3(think_believe_consider(skc13, Y_911), true, ifeq3(proposition(skc13, V_913), true, V_913, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.75 tff(c_35529, plain, (![W_978, X_979]: (ifeq3(theme(skc13, skc17, W_978), true, ifeq3(theme(skc13, X_979, skc14), true, ifeq3(agent(skc13, X_979, skc19), true, ifeq3(think_believe_consider(skc13, X_979), true, ifeq3(proposition(skc13, W_978), true, skc14, W_978), W_978), W_978), W_978), W_978)=W_978))). % 40.08/25.75 tff(c_35496, plain, (![W_1351]: (ifeq3(theme(skc14, skc17, W_1351), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_1351), true, skc14, W_1351), W_1351), W_1351), W_1351)=W_1351))). % 40.08/25.75 tff(c_26717, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc17, W_930), true, ifeq3(theme(skc14, skc21, V_931), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.08/25.76 tff(c_35414, plain, (![W_978, X_979]: (ifeq3(theme(skc13, skc15, W_978), true, ifeq3(theme(skc13, X_979, skc14), true, ifeq3(agent(skc13, X_979, skc19), true, ifeq3(think_believe_consider(skc13, X_979), true, ifeq3(proposition(skc13, W_978), true, skc14, W_978), W_978), W_978), W_978), W_978)=W_978))). % 40.08/25.76 tff(c_35386, plain, (![W_1346]: (ifeq3(theme(skc14, skc15, W_1346), true, ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_1346), true, skc14, W_1346), W_1346), W_1346), W_1346)=W_1346))). % 40.08/25.76 tff(c_26723, plain, (![W_930, V_931]: (ifeq3(theme(skc14, skc15, W_930), true, ifeq3(theme(skc14, skc21, V_931), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.08/25.76 tff(c_35349, plain, (![V_1344]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skc17, V_1344), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_1344), true, V_1344, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_26570, plain, (![W_922, V_924]: (ifeq3(theme(skc14, skc21, W_922), true, ifeq3(theme(skc14, skc17, V_924), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_922), true, ifeq3(proposition(skc14, V_924), true, V_924, W_922), W_922), W_922), W_922), W_922)=W_922))). % 40.08/25.76 tff(c_35279, plain, (![Y_903, V_905]: (ifeq3(theme(skc13, Y_903, skc14), true, ifeq3(theme(skc13, skc15, V_905), true, ifeq3(agent(skc13, Y_903, skc19), true, ifeq3(think_believe_consider(skc13, Y_903), true, ifeq3(proposition(skc13, V_905), true, V_905, skc14), skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_35262, plain, (![V_1339]: (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(theme(skc14, skc15, V_1339), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_1339), true, V_1339, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_26576, plain, (![W_922, V_924]: (ifeq3(theme(skc14, skc21, W_922), true, ifeq3(theme(skc14, skc15, V_924), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_922), true, ifeq3(proposition(skc14, V_924), true, V_924, W_922), W_922), W_922), W_922), W_922)=W_922))). % 40.08/25.76 tff(c_25000, plain, (![W_848, Z_849]: (ifeq3(theme(skc13, skc17, W_848), true, ifeq3(agent(skc13, skc17, Z_849), true, ifeq3(agent(skc13, skc15, Z_849), true, ifeq3(proposition(skc13, W_848), true, skc14, W_848), W_848), W_848), W_848)=W_848))). % 40.08/25.76 tff(c_35174, plain, (![W_985, Z_988]: (ifeq3(theme(skc13, skc15, W_985), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(agent(skc13, skc17, Z_988), true, ifeq3(proposition(skc13, W_985), true, skc14, W_985), W_985), W_985), W_985)=W_985))). % 40.08/25.76 tff(c_35129, plain, (![X_858, Z_860]: (ifeq3(theme(skc13, X_858, skc14), true, ifeq3(agent(skc13, skc15, Z_860), true, ifeq3(agent(skc13, X_858, Z_860), true, ifeq3(think_believe_consider(skc13, X_858), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_28052, plain, (![V_1012, Z_1013]: (ifeq3(theme(skc13, skc15, V_1012), true, ifeq3(agent(skc13, skc15, Z_1013), true, ifeq3(agent(skc13, skc15, Z_1013), true, ifeq3(proposition(skc13, V_1012), true, V_1012, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_35067, plain, (![V_868, Z_869]: (ifeq3(theme(skc13, skc15, V_868), true, ifeq3(agent(skc13, skc17, Z_869), true, ifeq3(agent(skc13, skc15, Z_869), true, ifeq3(proposition(skc13, V_868), true, V_868, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_27794, plain, (![W_985, Z_988]: (ifeq3(theme(skc13, skc15, W_985), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(agent(skc13, skc15, Z_988), true, ifeq3(proposition(skc13, W_985), true, skc14, W_985), W_985), W_985), W_985)=W_985))). % 40.08/25.76 tff(c_35007, plain, (![V_868, Z_869]: (ifeq3(theme(skc13, skc17, V_868), true, ifeq3(agent(skc13, skc17, Z_869), true, ifeq3(agent(skc13, skc17, Z_869), true, ifeq3(proposition(skc13, V_868), true, V_868, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_34962, plain, (![X_949, Z_950]: (ifeq3(theme(skc13, X_949, skc14), true, ifeq3(agent(skc13, skc17, Z_950), true, ifeq3(agent(skc13, X_949, Z_950), true, ifeq3(think_believe_consider(skc13, X_949), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_25222, plain, (![V_859, Z_860]: (ifeq3(theme(skc13, skc17, V_859), true, ifeq3(agent(skc13, skc15, Z_860), true, ifeq3(agent(skc13, skc17, Z_860), true, ifeq3(proposition(skc13, V_859), true, V_859, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_11398, plain, (![W_182, V_184]: (ifeq3(of(skc14, W_182, skc25), true, ifeq3(of(skc14, V_184, skc25), 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))). % 40.08/25.76 tff(c_34870, 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))). % 40.08/25.76 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))). % 40.08/25.76 tff(c_4203, plain, (![W_402, V_404]: (ifeq3(of(skc13, W_402, skc25), true, ifeq3(of(skc13, V_404, skc25), 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))). % 40.08/25.76 tff(c_34766, plain, (![W_1309]: (ifeq3(of(skc14, W_1309, skc19), true, ifeq3(of(skc14, skc26, skc19), true, ifeq3(forename(skc14, W_1309), true, W_1309, skc26), skc26), skc26)=skc26))). % 40.08/25.76 tff(c_5364, plain, (![W_182, X_183]: (ifeq3(of(skc14, W_182, X_183), true, ifeq3(of(skc14, skc26, X_183), true, ifeq3(forename(skc14, W_182), true, ifeq3(entity(skc14, X_183), true, W_182, skc26), skc26), skc26), skc26)=skc26))). % 40.08/25.76 tff(c_34686, plain, (![Y_938, Z_941]: (ifeq3(theme(skc13, Y_938, skc14), true, ifeq3(agent(skc13, Y_938, Z_941), true, ifeq3(agent(skc13, skc17, Z_941), true, ifeq3(think_believe_consider(skc13, Y_938), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_34590, plain, (![V_1302]: (ifeq3(of(skc14, skc26, skc19), true, ifeq3(of(skc14, V_1302, skc19), true, ifeq3(forename(skc14, V_1302), true, skc26, V_1302), V_1302), V_1302)=V_1302))). % 40.08/25.76 tff(c_34621, plain, (![Y_847, Z_849]: (ifeq3(theme(skc13, Y_847, skc14), true, ifeq3(agent(skc13, Y_847, Z_849), true, ifeq3(agent(skc13, skc15, Z_849), true, ifeq3(think_believe_consider(skc13, Y_847), true, skc14, skc14), skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_34615, plain, (ifeq3(of(skc14, skc26, skc19), true, ifeq3(of(skc14, skc26, skc19), true, skc26, skc26), skc26)=skc26)). % 40.08/25.76 tff(c_34592, plain, (![X_1301]: (ifeq3(of(skc14, skc26, X_1301), true, ifeq3(of(skc14, skc26, X_1301), true, ifeq3(entity(skc14, X_1301), true, skc26, skc26), skc26), skc26)=skc26))). % 40.08/25.76 tff(c_34556, plain, (![X_183, V_184]: (ifeq3(of(skc14, skc26, X_183), true, ifeq3(of(skc14, V_184, X_183), true, ifeq3(forename(skc14, V_184), true, ifeq3(entity(skc14, X_183), true, skc26, V_184), V_184), V_184), V_184)=V_184))). % 40.08/25.76 tff(c_34501, plain, (![W_1297]: (ifeq3(of(skc14, W_1297, skc25), true, ifeq3(of(skc14, skc18, skc25), true, ifeq3(forename(skc14, W_1297), true, W_1297, skc18), skc18), skc18)=skc18))). % 40.08/25.76 tff(c_34502, plain, (![X_1298]: (ifeq3(of(skc14, skc26, X_1298), true, ifeq3(of(skc14, skc18, X_1298), true, ifeq3(entity(skc14, X_1298), true, skc26, skc18), skc18), skc18)=skc18))). % 40.08/25.76 tff(c_34458, 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))). % 40.08/25.76 tff(c_34358, plain, (![V_1291]: (ifeq3(of(skc14, skc18, skc25), true, ifeq3(of(skc14, V_1291, skc25), true, ifeq3(forename(skc14, V_1291), true, skc18, V_1291), V_1291), V_1291)=V_1291))). % 40.08/25.76 tff(c_34432, plain, (ifeq3(of(skc14, skc18, skc25), true, ifeq3(of(skc14, skc18, skc25), true, skc18, skc18), skc18)=skc18)). % 40.08/25.76 tff(c_34360, 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))). % 40.08/25.76 tff(c_34384, plain, (![W_1002, Z_1005]: (ifeq3(theme(skc13, skc17, W_1002), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(agent(skc13, skc17, Z_1005), true, ifeq3(proposition(skc13, W_1002), true, skc14, W_1002), W_1002), W_1002), W_1002)=W_1002))). % 40.08/25.76 tff(c_34359, plain, (![X_1290]: (ifeq3(of(skc14, skc18, X_1290), true, ifeq3(of(skc14, skc26, X_1290), true, ifeq3(entity(skc14, X_1290), true, skc18, skc26), skc26), skc26)=skc26))). % 40.08/25.76 tff(c_34323, 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))). % 40.08/25.76 tff(c_23472, plain, (![V_792]: (ifeq3(of(skc13, skc26, skc19), true, ifeq3(of(skc13, V_792, skc19), true, ifeq3(forename(skc13, V_792), true, skc26, V_792), V_792), V_792)=V_792))). % 40.08/25.76 tff(c_24238, plain, (![V_811]: (ifeq3(of(skc13, skc18, skc25), true, ifeq3(of(skc13, V_811, skc25), true, ifeq3(forename(skc13, V_811), true, skc18, V_811), V_811), V_811)=V_811))). % 40.08/25.76 tff(c_24629, plain, (![W_829]: (ifeq3(of(skc13, W_829, skc25), true, ifeq3(of(skc13, skc18, skc25), true, ifeq3(forename(skc13, W_829), true, W_829, skc18), skc18), skc18)=skc18))). % 40.08/25.76 tff(c_23673, plain, (![W_799]: (ifeq3(of(skc13, W_799, skc19), true, ifeq3(of(skc13, skc26, skc19), true, ifeq3(forename(skc13, W_799), true, W_799, skc26), skc26), skc26)=skc26))). % 40.08/25.76 tff(c_34184, plain, (![V_931]: (ifeq3(theme(skc14, skc21, V_931), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, V_931), true, V_931, skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_32836, plain, (![X_1217]: (ifeq3(theme(skc13, X_1217, skc14), true, ifeq3(agent(skc13, X_1217, skc19), true, ifeq3(think_believe_consider(skc13, X_1217), true, skc14, skc14), skc14), skc14)=skc14))). % 40.08/25.76 tff(c_34147, plain, (ifeq3(theme(skc14, skc21, skc14), true, ifeq3(think_believe_consider(skc14, skc21), true, skc14, skc14), skc14)=skc14)). % 40.08/25.76 tff(c_26573, plain, (![W_922]: (ifeq3(theme(skc14, skc21, W_922), true, ifeq3(think_believe_consider(skc14, skc21), true, ifeq3(proposition(skc14, W_922), true, skc14, W_922), W_922), W_922)=W_922))). % 40.08/25.76 tff(c_31620, plain, (ifeq3(of(skc13, skc26, skc19), true, ifeq3(of(skc13, skc26, skc19), true, skc26, skc26), skc26)=skc26)). % 40.08/25.76 tff(c_30495, plain, (ifeq3(of(skc13, skc18, skc25), true, ifeq3(of(skc13, skc18, skc25), true, skc18, skc18), skc18)=skc18)). % 40.08/25.76 tff(c_34093, plain, (![V_1281]: (ifeq2(accessible_world(skc14, V_1281), true, agent(V_1281, skf1(skc25), skc25), true)=true))). % 40.08/25.76 tff(c_34068, plain, (![U_164]: (ifeq2(agent(U_164, skf1(skc19), skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_34052, plain, (![V_167]: (ifeq2(accessible_world(skc14, V_167), true, agent(V_167, skf1(skc19), skc19), true)=true))). % 40.08/25.76 tff(c_34030, plain, (![U_164]: (ifeq2(agent(U_164, skf1(skc25), skc25), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_34007, plain, (![V_180]: (ifeq2(accessible_world(skc14, V_180), true, be(V_180, skc24, skc25, skc25), true)=true))). % 40.08/25.76 tff(c_33983, plain, (![U_177]: (ifeq2(be(U_177, skc24, skc25, skc25), true, ifeq2(accessible_world(U_177, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33960, plain, (![U_86, V_537]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skf1(V_537)), true, true, true), true)=true))). % 40.08/25.76 tff(c_33938, plain, (![U_83, V_532]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skf1(V_532)), true, true, true), true)=true))). % 40.08/25.76 tff(c_33917, plain, (![U_89, V_527]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skf1(V_527)), true, true, true), true)=true))). % 40.08/25.76 tff(c_33896, plain, (![U_95, V_529]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skf1(V_529)), true, true, true), true)=true))). % 40.08/25.76 tff(c_29143, plain, (![U_92, V_1022]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skf1(V_1022)), true, true, true), true)=true))). % 40.08/25.76 tff(c_33865, plain, (ifeq3(of(skc14, skc18, skc25), true, skc18, skc26)=skc26)). % 40.08/25.76 tff(c_14844, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc25), true, ifeq3(forename(skc14, W_182), true, W_182, skc26), skc26)=skc26))). % 40.08/25.76 tff(c_33830, plain, (ifeq3(of(skc14, skc18, skc25), true, skc26, skc18)=skc18)). % 40.08/25.76 tff(c_33809, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc25), true, ifeq3(forename(skc14, V_184), true, skc26, V_184), V_184)=V_184))). % 40.08/25.76 tff(c_33792, plain, (ifeq3(of(skc14, skc26, skc19), true, skc26, skc18)=skc18)). % 40.08/25.76 tff(c_33764, plain, (![W_182]: (ifeq3(of(skc14, W_182, skc19), true, ifeq3(forename(skc14, W_182), true, W_182, skc18), skc18)=skc18))). % 40.08/25.76 tff(c_29078, plain, (![U_80, V_1020]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skf1(V_1020)), true, true, true), true)=true))). % 40.08/25.76 tff(c_33739, plain, (ifeq3(of(skc14, skc26, skc19), true, skc18, skc26)=skc26)). % 40.08/25.76 tff(c_33719, plain, (![V_184]: (ifeq3(of(skc14, V_184, skc19), true, ifeq3(forename(skc14, V_184), true, skc18, V_184), V_184)=V_184))). % 40.08/25.76 tff(c_23675, plain, (![W_799]: (ifeq3(of(skc13, W_799, skc25), true, ifeq3(forename(skc13, W_799), true, W_799, skc26), skc26)=skc26))). % 40.08/25.76 tff(c_29012, plain, (![U_74, V_1017]: (ifeq2(accessible_world(U_74, skc14), true, ifeq2(smoke(U_74, skf1(V_1017)), true, true, true), true)=true))). % 40.08/25.76 tff(c_29061, plain, (![U_98, V_1019]: (ifeq2(present(U_98, skf1(V_1019)), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33605, plain, (![V_404]: (ifeq3(of(skc13, V_404, skc19), true, ifeq3(forename(skc13, V_404), true, skc18, V_404), V_404)=V_404))). % 40.08/25.76 tff(c_33588, plain, (![V_100, V_520]: (ifeq2(accessible_world(skc14, V_100), true, present(V_100, skf1(V_520)), true)=true))). % 40.08/25.76 tff(c_33567, plain, (![U_77, V_517]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skf1(V_517)), true, true, true), true)=true))). % 40.08/25.76 tff(c_23473, plain, (![V_792]: (ifeq3(of(skc13, V_792, skc25), true, ifeq3(forename(skc13, V_792), true, skc26, V_792), V_792)=V_792))). % 40.08/25.76 tff(c_33526, plain, (![W_806]: (ifeq3(of(skc13, W_806, skc19), true, ifeq3(forename(skc13, W_806), true, W_806, skc18), skc18)=skc18))). % 40.08/25.76 tff(c_33467, plain, (![V_1246]: (ifeq2(accessible_world(skc14, V_1246), true, theme(V_1246, skc15, skc14), true)=true))). % 40.08/25.76 tff(c_15040, plain, (![U_164]: (ifeq2(agent(U_164, skc15, skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33399, plain, (![V_1243]: (ifeq2(accessible_world(skc14, V_1243), true, of(V_1243, skc26, skc25), true)=true))). % 40.08/25.76 tff(c_33373, plain, (![V_167]: (ifeq2(accessible_world(skc14, V_167), true, agent(V_167, skc15, skc19), true)=true))). % 40.08/25.76 tff(c_33352, plain, (![V_167]: (ifeq2(accessible_world(skc14, V_167), true, agent(V_167, skc17, skc19), true)=true))). % 40.08/25.76 tff(c_33331, plain, (![V_171]: (ifeq2(accessible_world(skc14, V_171), true, theme(V_171, skc17, skc14), true)=true))). % 40.08/25.76 tff(c_33305, plain, (![U_164]: (ifeq2(agent(U_164, skc17, skc19), true, ifeq2(accessible_world(U_164, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33280, plain, (![U_168]: (ifeq2(theme(U_168, skc17, skc14), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33256, plain, (![U_168]: (ifeq2(theme(U_168, skc15, skc14), true, ifeq2(accessible_world(U_168, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33231, plain, (![U_172]: (ifeq2(of(U_172, skc18, skc19), true, ifeq2(accessible_world(U_172, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33207, plain, (![U_172]: (ifeq2(of(U_172, skc26, skc25), true, ifeq2(accessible_world(U_172, skc14), true, true, true), true)=true))). % 40.08/25.76 tff(c_33187, plain, (![V_175]: (ifeq2(accessible_world(skc14, V_175), true, of(V_175, skc18, skc19), true)=true))). % 40.08/25.76 tff(c_28334, plain, (![U_392]: (ifeq2(theme(U_392, skc17, skc14), true, ifeq2(accessible_world(U_392, skc13), true, true, true), true)=true))). % 40.08/25.76 tff(c_33132, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc25), true, true, true), true)=true))). % 40.08/25.76 tff(c_33102, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc25), true, true, true), true)=true))). % 40.08/25.76 tff(c_33081, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc19), true, true, true), true)=true))). % 40.08/25.76 tff(c_33056, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc26), true, true, true), true)=true))). % 40.08/25.76 tff(c_33035, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc18), true, true, true), true)=true))). % 40.31/25.76 tff(c_12837, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc19), true, true, true), true)=true))). % 40.31/25.76 tff(c_32997, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_12940, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_12719, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_10145, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_32918, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_32898, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_32873, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_32840, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_27497, plain, (![X_970, V_971]: (ifeq3(theme(skc13, X_970, V_971), true, ifeq3(agent(skc13, X_970, skc19), true, ifeq3(think_believe_consider(skc13, X_970), true, ifeq3(proposition(skc13, V_971), true, V_971, skc14), skc14), skc14), skc14)=skc14))). % 40.31/25.77 tff(c_32774, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_32754, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(existent(U_134, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_32733, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_32713, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32693, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_11383, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc14), true, ifeq2(entity(U_131, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_32653, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_25996, plain, (![W_893, V_895]: (ifeq3(theme(skc13, skc17, W_893), true, ifeq3(theme(skc13, skc17, V_895), true, ifeq3(proposition(skc13, W_893), true, ifeq3(proposition(skc13, V_895), true, V_895, W_893), W_893), W_893), W_893)=W_893))). % 40.31/25.77 tff(c_32608, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_32587, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32566, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc14), true, ifeq2(existent(U_134, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_32546, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc14), true, ifeq2(singleton(U_86, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_32526, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc14), true, ifeq2(general(U_116, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_32503, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32482, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_10714, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc13), true, ifeq2(specific(U_89, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_4443, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc13), true, ifeq2(existent(U_134, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_3791, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_3971, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_3544, plain, (![U_134]: (ifeq2(accessible_world(U_134, skc13), true, ifeq2(existent(U_134, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_3733, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc13), true, ifeq2(general(U_116, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_4239, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_10575, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc13), true, ifeq2(specific(U_89, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_32339, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32319, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_3828, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_32287, plain, (![U_116]: (ifeq2(accessible_world(U_116, skc13), true, ifeq2(general(U_116, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32271, plain, (![U_86]: (ifeq2(accessible_world(U_86, skc13), true, ifeq2(singleton(U_86, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_3647, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_32218, plain, (![Y_875, W_876]: (ifeq3(theme(skc13, Y_875, W_876), true, ifeq3(agent(skc13, Y_875, skc19), true, ifeq3(think_believe_consider(skc13, Y_875), true, ifeq3(proposition(skc13, W_876), true, skc14, W_876), W_876), W_876), W_876)=W_876))). % 40.31/25.77 tff(c_4354, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_32181, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_26203, plain, (![W_904, V_905]: (ifeq3(theme(skc13, skc15, W_904), true, ifeq3(theme(skc13, skc15, V_905), true, ifeq3(proposition(skc13, W_904), true, ifeq3(proposition(skc13, V_905), true, V_905, W_904), W_904), W_904), W_904)=W_904))). % 40.31/25.77 tff(c_32125, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_32105, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(living(U_140, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_27271, plain, (![W_958, V_959]: (ifeq3(theme(skc13, skc15, W_958), true, ifeq3(theme(skc13, skc17, V_959), true, ifeq3(proposition(skc13, W_958), true, ifeq3(proposition(skc13, V_959), true, V_959, W_958), W_958), W_958), W_958)=W_958))). % 40.31/25.77 tff(c_9703, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_9382, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_26202, plain, (![W_904, V_905]: (ifeq3(theme(skc13, skc17, W_904), true, ifeq3(theme(skc13, skc15, V_905), true, ifeq3(proposition(skc13, W_904), true, ifeq3(proposition(skc13, V_905), true, V_905, W_904), W_904), W_904), W_904)=W_904))). % 40.31/25.77 tff(c_7508, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(impartial(U_137, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_31969, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_31949, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc14), true, ifeq2(nonhuman(U_113, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31929, plain, (![U_131]: (ifeq2(accessible_world(U_131, skc14), true, ifeq2(entity(U_131, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_31909, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(organism(U_128, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_31887, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31866, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc14), true, ifeq2(living(U_140, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_7526, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc14), true, ifeq2(impartial(U_137, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_8396, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_31807, plain, (![U_89]: (ifeq2(accessible_world(U_89, skc14), true, ifeq2(specific(U_89, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_31787, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_8463, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31742, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_31722, plain, (![U_110]: (ifeq2(accessible_world(U_110, skc14), true, ifeq2(abstraction(U_110, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_31701, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc14), true, ifeq2(thing(U_83, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_31681, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(human(U_143, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_31659, plain, (![U_143]: (ifeq2(accessible_world(U_143, skc14), true, ifeq2(human(U_143, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_2967, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc13), true, ifeq2(impartial(U_137, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_3577, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_23478, plain, (![X_791]: (ifeq3(of(skc13, skc26, X_791), true, ifeq3(of(skc13, skc26, X_791), true, ifeq3(entity(skc13, X_791), true, skc26, skc26), skc26), skc26)=skc26))). % 40.31/25.77 tff(c_3519, plain, (![U_372]: (ifeq2(accessible_world(U_372, skc13), true, ifeq2(entity(U_372, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_31568, plain, (![U_330]: (ifeq2(accessible_world(U_330, skc13), true, ifeq2(general(U_330, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_3583, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_3525, plain, (![U_372]: (ifeq2(accessible_world(U_372, skc13), true, ifeq2(entity(U_372, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_2379, plain, (![U_113]: (ifeq2(accessible_world(U_113, skc13), true, ifeq2(nonhuman(U_113, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_3589, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc13), true, ifeq2(singleton(U_375, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_31489, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_3192, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc13), true, ifeq2(living(U_140, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_3676, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_3372, plain, (![U_140]: (ifeq2(accessible_world(U_140, skc13), true, ifeq2(living(U_140, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_3289, plain, (![U_137]: (ifeq2(accessible_world(U_137, skc13), true, ifeq2(impartial(U_137, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_3595, plain, (![U_375]: (ifeq2(accessible_world(U_375, skc14), true, ifeq2(singleton(U_375, skc21), true, true, true), true)=true))). % 40.31/25.77 tff(c_31394, plain, (![U_83]: (ifeq2(accessible_world(U_83, skc13), true, ifeq2(thing(U_83, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31378, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc13), true, ifeq2(unisex(U_95, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31353, plain, (![X_800]: (ifeq3(of(skc13, skc18, X_800), true, ifeq3(of(skc13, skc26, X_800), true, ifeq3(entity(skc13, X_800), true, skc18, skc26), skc26), skc26)=skc26))). % 40.31/25.77 tff(c_31328, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_31308, plain, (![U_149]: (ifeq2(accessible_world(U_149, skc14), true, ifeq2(male(U_149, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_6360, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_9998, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc15), true, true, true), true)=true))). % 40.31/25.77 tff(c_31245, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(human_person(U_125, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_8110, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc14), true, ifeq2(animate(U_146, skc25), true, true, true), true)=true))). % 40.31/25.77 tff(c_31204, plain, (![U_92]: (ifeq2(accessible_world(U_92, skc14), true, ifeq2(nonexistent(U_92, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_31179, plain, (![U_155]: (ifeq2(accessible_world(U_155, skc14), true, ifeq2(relname(U_155, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_5605, plain, (![U_125]: (ifeq2(accessible_world(U_125, skc14), true, ifeq2(human_person(U_125, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_8091, plain, (![U_146]: (ifeq2(accessible_world(U_146, skc14), true, ifeq2(animate(U_146, skc19), true, true, true), true)=true))). % 40.31/25.77 tff(c_7267, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc17), true, true, true), true)=true))). % 40.31/25.77 tff(c_31100, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc26), true, true, true), true)=true))). % 40.31/25.77 tff(c_6905, plain, (![U_80]: (ifeq2(accessible_world(U_80, skc14), true, ifeq2(eventuality(U_80, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_6691, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_31042, plain, (![U_107]: (ifeq2(accessible_world(U_107, skc14), true, ifeq2(relation(U_107, skc14), true, true, true), true)=true))). % 40.31/25.77 tff(c_31022, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc24), true, true, true), true)=true))). % 40.31/25.77 tff(c_31002, plain, (![U_155]: (ifeq2(accessible_world(U_155, skc14), true, ifeq2(relname(U_155, skc18), true, true, true), true)=true))). % 40.31/25.77 tff(c_23988, plain, (![U_360]: (ifeq2(accessible_world(U_360, skc13), true, ifeq2(jules_forename(U_360, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_30966, plain, (![U_95]: (ifeq2(accessible_world(U_95, skc14), true, ifeq2(unisex(U_95, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_30945, plain, (![U_149]: (ifeq2(accessible_world(U_149, skc14), true, ifeq2(male(U_149, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_30925, plain, (![U_128]: (ifeq2(accessible_world(U_128, skc14), true, ifeq2(organism(U_128, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_3236, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_2901, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc14), true, ifeq2(specific(U_342, skc21), true, true, true), true)=true))). % 40.31/25.78 tff(c_3230, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_2728, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc13), true, ifeq2(human(U_333, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_2907, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_2734, plain, (![U_333]: (ifeq2(accessible_world(U_333, skc13), true, ifeq2(human(U_333, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_2308, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc13), true, ifeq2(animate(U_312, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_2314, plain, (![U_312]: (ifeq2(accessible_world(U_312, skc13), true, ifeq2(animate(U_312, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_2562, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_2568, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_2895, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_2889, plain, (![U_342]: (ifeq2(accessible_world(U_342, skc13), true, ifeq2(specific(U_342, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_3700, plain, (![U_378]: (ifeq2(accessible_world(U_378, skc13), true, ifeq2(abstraction(U_378, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_3224, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc13), true, ifeq2(thing(U_357, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_3218, plain, (![U_357]: (ifeq2(accessible_world(U_357, skc14), true, ifeq2(thing(U_357, skc21), true, true, true), true)=true))). % 40.31/25.78 tff(c_2556, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc14), true, ifeq2(nonexistent(U_324, skc21), true, true, true), true)=true))). % 40.31/25.78 tff(c_2194, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc14), true, ifeq2(unisex(U_306, skc21), true, true, true), true)=true))). % 40.31/25.78 tff(c_2550, plain, (![U_324]: (ifeq2(accessible_world(U_324, skc13), true, ifeq2(nonexistent(U_324, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_2842, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc13), true, ifeq2(organism(U_339, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_2188, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_2176, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_30573, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_24634, plain, (![X_830]: (ifeq3(of(skc13, skc26, X_830), true, ifeq3(of(skc13, skc18, X_830), true, ifeq3(entity(skc13, X_830), true, skc26, skc18), skc18), skc18)=skc18))). % 40.31/25.78 tff(c_1910, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc26), true, true, true), true)=true))). % 40.31/25.78 tff(c_2836, plain, (![U_339]: (ifeq2(accessible_world(U_339, skc13), true, ifeq2(organism(U_339, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_2182, plain, (![U_306]: (ifeq2(accessible_world(U_306, skc13), true, ifeq2(unisex(U_306, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_30475, plain, (![X_807]: (ifeq3(of(skc13, skc18, X_807), true, ifeq3(of(skc13, skc18, X_807), true, ifeq3(entity(skc13, X_807), true, skc18, skc18), skc18), skc18)=skc18))). % 40.31/25.78 tff(c_4706, plain, (![U_119]: (ifeq2(accessible_world(U_119, skc14), true, ifeq2(state(U_119, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_4946, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(man(U_122, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_30399, plain, (![V_100]: (ifeq2(accessible_world(skc14, V_100), true, present(V_100, skc17), true)=true))). % 40.31/25.78 tff(c_6548, plain, (![U_158]: (ifeq2(accessible_world(U_158, skc14), true, ifeq2(vincent_forename(U_158, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_30338, plain, (![V_1084]: (ifeq2(accessible_world(skc14, V_1084), true, present(V_1084, skc15), true)=true))). % 40.31/25.78 tff(c_30310, plain, (![V_103]: (ifeq2(accessible_world(skc14, V_103), true, think_believe_consider(V_103, skc17), true)=true))). % 40.31/25.78 tff(c_30288, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc14), true, ifeq2(jules_forename(U_161, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_6015, plain, (![U_161]: (ifeq2(accessible_world(U_161, skc14), true, ifeq2(jules_forename(U_161, skc26), true, true, true), true)=true))). % 40.31/25.78 tff(c_30243, plain, (![U_122]: (ifeq2(accessible_world(U_122, skc14), true, ifeq2(man(U_122, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_5350, plain, (![U_152]: (ifeq2(accessible_world(U_152, skc14), true, ifeq2(forename(U_152, skc26), true, true, true), true)=true))). % 40.31/25.78 tff(c_5935, plain, (![U_98]: (ifeq2(present(U_98, skc17), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_30181, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_30160, plain, (![U_104]: (ifeq2(accessible_world(U_104, skc14), true, ifeq2(proposition(U_104, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_6295, plain, (![U_101]: (ifeq2(think_believe_consider(U_101, skc17), true, ifeq2(accessible_world(U_101, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_30116, plain, (![U_152]: (ifeq2(accessible_world(U_152, skc14), true, ifeq2(forename(U_152, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_6132, plain, (![U_77]: (ifeq2(accessible_world(U_77, skc14), true, ifeq2(event(U_77, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_30059, plain, (![V_1071]: (ifeq2(accessible_world(skc14, V_1071), true, think_believe_consider(V_1071, skc15), true)=true))). % 40.31/25.78 tff(c_6330, plain, (![U_101]: (ifeq2(think_believe_consider(U_101, skc15), true, ifeq2(accessible_world(U_101, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_30007, plain, (![U_98]: (ifeq2(present(U_98, skc15), true, ifeq2(accessible_world(U_98, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_25216, plain, (![Z_860]: (ifeq3(agent(skc13, skc15, Z_860), true, ifeq3(agent(skc13, skc15, Z_860), true, skc14, skc14), skc14)=skc14))). % 40.31/25.78 tff(c_3085, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc13), true, ifeq2(human_person(U_351, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_3079, plain, (![U_351]: (ifeq2(accessible_world(U_351, skc13), true, ifeq2(human_person(U_351, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_3762, plain, (![U_381]: (ifeq2(accessible_world(U_381, skc13), true, ifeq2(male(U_381, skc25), true, true, true), true)=true))). % 40.31/25.78 tff(c_3756, plain, (![U_381]: (ifeq2(accessible_world(U_381, skc13), true, ifeq2(male(U_381, skc19), true, true, true), true)=true))). % 40.31/25.78 tff(c_2232, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc14), true, ifeq2(eventuality(U_309, skc21), true, true, true), true)=true))). % 40.31/25.78 tff(c_2238, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc17), true, true, true), true)=true))). % 40.31/25.78 tff(c_3020, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_29864, plain, (![Z_869]: (ifeq3(agent(skc13, skc17, Z_869), true, ifeq3(agent(skc13, skc17, Z_869), true, skc14, skc14), skc14)=skc14))). % 40.31/25.78 tff(c_2106, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc13), true, ifeq2(relname(U_303, skc26), true, true, true), true)=true))). % 40.31/25.78 tff(c_29833, plain, (![U_303]: (ifeq2(accessible_world(U_303, skc13), true, ifeq2(relname(U_303, skc18), true, true, true), true)=true))). % 40.31/25.78 tff(c_2244, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc15), true, true, true), true)=true))). % 40.31/25.78 tff(c_2250, plain, (![U_309]: (ifeq2(accessible_world(U_309, skc13), true, ifeq2(eventuality(U_309, skc24), true, true, true), true)=true))). % 40.31/25.78 tff(c_1922, plain, (![U_294]: (ifeq2(accessible_world(U_294, skc13), true, ifeq2(relation(U_294, skc14), true, true, true), true)=true))). % 40.31/25.78 tff(c_29768, plain, (![Z_877]: (ifeq3(agent(skc13, skc15, Z_877), true, ifeq3(agent(skc13, skc17, Z_877), true, skc14, skc14), skc14)=skc14))). % 40.31/25.78 tff(c_29171, plain, (![V_1023]: (ifeq(tuple(true, male(skc14, skf1(V_1023))), tuple(true, true), a, b)=b))). % 40.31/25.78 tff(c_29146, plain, (![V_1022]: (ifeq(tuple(true, existent(skc14, skf1(V_1022))), tuple(true, true), a, b)=b))). % 40.31/25.78 tff(c_29743, plain, (![V_527]: (ifeq(tuple(true, general(skc14, skf1(V_527))), tuple(true, true), a, b)=b))). % 40.31/25.78 tff(c_29724, plain, (![Z_869]: (ifeq3(agent(skc13, skc17, Z_869), true, ifeq3(agent(skc13, skc15, Z_869), true, skc14, skc14), skc14)=skc14))). % 40.31/25.78 tff(c_13847, plain, (ifeq(tuple(true, general(skc14, skc25)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29691, plain, (ifeq(tuple(specific(skc14, skc26), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_12051, plain, (ifeq(tuple(specific(skc14, skc14), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29678, plain, (ifeq(tuple(true, general(skc14, skc19)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_10148, plain, (ifeq(tuple(true, male(skc14, skc26)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29667, plain, (ifeq(tuple(true, human(skc14, skc26)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29662, plain, (ifeq(tuple(true, male(skc14, skc18)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29657, plain, (ifeq(tuple(nonexistent(skc14, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29652, plain, (ifeq(tuple(specific(skc14, skc18), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29645, plain, (ifeq(tuple(nonexistent(skc14, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29640, plain, (ifeq(tuple(true, human(skc14, skc18)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_10578, plain, (ifeq(tuple(true, general(skc13, skc19)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_4242, plain, (ifeq(tuple(true, male(skc13, skc26)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_3547, plain, (ifeq(tuple(nonexistent(skc13, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_3736, plain, (ifeq(tuple(specific(skc13, skc26), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_3650, plain, (ifeq(tuple(true, human(skc13, skc26)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_10717, plain, (ifeq(tuple(true, general(skc13, skc25)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_4446, plain, (ifeq(tuple(nonexistent(skc13, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_10644, plain, (ifeq(tuple(true, human(skc13, skc18)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29596, plain, (ifeq(tuple(specific(skc13, skc18), true), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29590, plain, (ifeq(tuple(true, male(skc13, skc18)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_29581, plain, (ifeq(tuple(true, general(skc14, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_28229, plain, (ifeq(tuple(true, human(skc14, skc14)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_9706, plain, (ifeq(tuple(true, general(skc14, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_28230, plain, (ifeq(tuple(true, existent(skc14, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_8162, plain, (ifeq(tuple(true, general(skc14, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_28241, plain, (ifeq(tuple(true, male(skc14, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_28242, plain, (ifeq(tuple(true, existent(skc14, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.78 tff(c_28246, plain, (![V_87, V_537]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skf1(V_537)), true)=true))). % 40.31/25.78 tff(c_29154, plain, (![V_93, V_1022]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skf1(V_1022)), true)=true))). % 40.31/25.78 tff(c_29242, plain, (![V_84, V_1025]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skf1(V_1025)), true)=true))). % 40.31/25.78 tff(c_29182, plain, (![V_96, V_1023]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skf1(V_1023)), true)=true))). % 40.31/25.78 tff(c_29210, plain, (![V_90, V_1024]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skf1(V_1024)), true)=true))). % 40.31/25.78 tff(c_29101, plain, (![V_81, V_1020]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skf1(V_1020)), true)=true))). % 40.31/25.78 tff(c_28560, plain, (![U_197]: (ifeq2(man(skc14, U_197), true, agent(skc14, skf1(U_197), U_197), true)=true))). % 40.31/25.78 tff(c_29020, plain, (![V_75, V_1017]: (ifeq2(accessible_world(skc14, V_75), true, smoke(V_75, skf1(V_1017)), true)=true))). % 40.31/25.78 tff(c_29047, plain, (![V_78, V_1018]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skf1(V_1018)), true)=true))). % 40.31/25.78 tff(c_28322, plain, (![V_725]: (ifeq2(accessible_world(skc13, V_725), true, theme(V_725, skc17, skc14), true)=true))). % 40.31/25.78 tff(c_29177, plain, (![V_1023]: (ifeq2(abstraction(skc14, skf1(V_1023)), true, true, true)=true))). % 40.31/25.78 tff(c_29234, plain, (![V_1025]: (ifeq2(entity(skc14, skf1(V_1025)), true, true, true)=true))). % 40.31/25.78 tff(c_29036, plain, (![V_1018]: (ifeq2(state(skc14, skf1(V_1018)), true, true, true)=true))). % 40.31/25.78 tff(c_29342, plain, (![V_905]: (ifeq3(theme(skc13, skc15, V_905), true, ifeq3(proposition(skc13, V_905), true, V_905, skc14), skc14)=skc14))). % 40.31/25.78 tff(c_28410, plain, (![U_191]: (ifeq2(man(skc14, U_191), true, true, true)=true))). % 40.31/25.78 tff(c_28366, plain, (agent(skc14, skf1(skc19), skc19)=true)). % 40.31/25.78 tff(c_28365, plain, (agent(skc14, skf1(skc25), skc25)=true)). % 40.31/25.78 tff(c_28400, plain, (![V_536]: (singleton(skc14, skf1(V_536))=true))). % 40.31/25.78 tff(c_28403, plain, (![V_531]: (thing(skc14, skf1(V_531))=true))). % 40.31/25.78 tff(c_28405, plain, (![V_526]: (specific(skc14, skf1(V_526))=true))). % 40.31/25.78 tff(c_28404, plain, (![V_528]: (unisex(skc14, skf1(V_528))=true))). % 40.31/25.78 tff(c_28402, plain, (![V_533]: (nonexistent(skc14, skf1(V_533))=true))). % 40.31/25.78 tff(c_29104, plain, (![W_876]: (ifeq3(theme(skc13, skc17, W_876), true, ifeq3(proposition(skc13, W_876), true, skc14, W_876), W_876)=W_876))). % 40.31/25.78 tff(c_28407, plain, (![V_522]: (eventuality(skc14, skf1(V_522))=true))). % 40.31/25.78 tff(c_28408, plain, (![V_519]: (present(skc14, skf1(V_519))=true))). % 40.31/25.78 tff(c_28409, plain, (![V_516]: (event(skc14, skf1(V_516))=true))). % 40.31/25.78 tff(c_28411, plain, (![V_513]: (smoke(skc14, skf1(V_513))=true))). % 40.31/25.78 tff(c_28564, plain, (theme(skc13, skc17, skc14)=true)). % 40.31/25.78 tff(c_28414, plain, (theme(skc14, skc17, skc14)=true)). % 40.31/25.79 tff(c_28226, plain, (skc16=skc14)). % 40.31/25.79 tff(c_26361, plain, (![V_913]: (ifeq3(theme(skc13, skc17, V_913), true, ifeq3(proposition(skc13, V_913), true, V_913, skc14), skc14)=skc14))). % 40.31/25.79 tff(c_9773, plain, (ifeq(tuple(true, male(skc14, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_7468, plain, (ifeq(tuple(true, existent(skc14, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_8301, plain, (ifeq(tuple(nonhuman(skc14, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_8730, plain, (ifeq(tuple(nonhuman(skc14, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_10051, plain, (ifeq(tuple(true, male(skc14, skc14)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_2652, plain, (ifeq(tuple(specific(skc13, skc14), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_2382, plain, (ifeq(tuple(true, human(skc13, skc14)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_24995, plain, (![W_848]: (ifeq3(theme(skc13, skc15, W_848), true, ifeq3(proposition(skc13, W_848), true, skc14, W_848), W_848)=W_848))). % 40.31/25.79 tff(c_3141, plain, (ifeq(tuple(true, male(skc13, skc14)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_10001, plain, (ifeq(tuple(true, male(skc14, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_5538, plain, (ifeq(tuple(unisex(skc14, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_5877, plain, (ifeq(tuple(unisex(skc14, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.79 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))). % 40.31/25.79 tff(c_1832, plain, (ifeq(tuple(true, general(skc14, skc21)), tuple(true, true), a, b)=b)). % 40.31/25.79 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))). % 40.31/25.79 tff(c_1735, plain, (ifeq(tuple(true, existent(skc13, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_14413, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc25), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_13967, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc26), true)=true))). % 40.31/25.79 tff(c_13649, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc14), true)=true))). % 40.31/25.79 tff(c_2019, plain, (ifeq(tuple(nonhuman(skc13, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_27571, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc18), true)=true))). % 40.31/25.79 tff(c_13327, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc18), true)=true))). % 40.31/25.79 tff(c_14580, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc26), true)=true))). % 40.31/25.79 tff(c_13509, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc25), true)=true))). % 40.31/25.79 tff(c_1829, plain, (ifeq(tuple(true, general(skc13, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.79 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))). % 40.31/25.79 tff(c_13856, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc25), true)=true))). % 40.31/25.79 tff(c_27399, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc18), true)=true))). % 40.31/25.79 tff(c_13936, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc19), true)=true))). % 40.31/25.79 tff(c_1835, plain, (ifeq(tuple(true, general(skc13, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_13762, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc26), true)=true))). % 40.31/25.79 tff(c_14599, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc19), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_13286, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc26), true)=true))). % 40.31/25.79 tff(c_27163, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc18), true)=true))). % 40.31/25.79 tff(c_1877, plain, (ifeq(tuple(true, male(skc13, skc24)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_14030, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc19), true)=true))). % 40.31/25.79 tff(c_12946, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc26), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_12843, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc19), true)=true))). % 40.31/25.79 tff(c_12725, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc25), true)=true))). % 40.31/25.79 tff(c_13049, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc18), true)=true))). % 40.31/25.79 tff(c_1789, plain, (ifeq(tuple(true, male(skc14, skc21)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_10938, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc14), true)=true))). % 40.31/25.79 tff(c_11209, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, living(V_141, skc19), true)=true))). % 40.31/25.79 tff(c_12309, plain, (![V_132]: (ifeq2(accessible_world(skc14, V_132), true, entity(V_132, skc19), true)=true))). % 40.31/25.79 tff(c_1707, plain, (ifeq(tuple(nonhuman(skc13, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_4323, plain, (![Y_407, W_406, V_405]: (ifeq3(theme(skc14, Y_407, W_406), true, ifeq3(theme(skc14, skc21, V_405), true, ifeq3(agent(skc14, Y_407, skc19), true, ifeq3(think_believe_consider(skc14, Y_407), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.31/25.79 tff(c_11440, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc26), true)=true))). % 40.31/25.79 tff(c_1729, plain, (ifeq(tuple(true, existent(skc14, skc21)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_4322, plain, (![W_406, X_410, V_405]: (ifeq3(theme(skc14, skc21, W_406), true, ifeq3(theme(skc14, X_410, V_405), true, ifeq3(agent(skc14, X_410, skc19), true, ifeq3(think_believe_consider(skc14, skc21), 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))). % 40.31/25.79 tff(c_11469, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc17), true)=true))). % 40.31/25.79 tff(c_10158, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc26), true)=true))). % 40.31/25.79 tff(c_10874, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc24), true)=true))). % 40.31/25.79 tff(c_11125, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, existent(V_135, skc19), true)=true))). % 40.31/25.79 tff(c_1853, plain, (ifeq(tuple(true, existent(skc13, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_26390, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc18), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_11630, plain, (![V_141]: (ifeq2(accessible_world(skc14, V_141), true, living(V_141, skc25), true)=true))). % 40.31/25.79 tff(c_1959, plain, (ifeq(tuple(true, general(skc13, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.79 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))). % 40.31/25.79 tff(c_12057, plain, (![V_117]: (ifeq2(accessible_world(skc14, V_117), true, general(V_117, skc14), true)=true))). % 40.31/25.79 tff(c_11146, plain, (![V_135]: (ifeq2(accessible_world(skc14, V_135), true, existent(V_135, skc25), true)=true))). % 40.31/25.79 tff(c_12268, plain, (![V_114]: (ifeq2(accessible_world(skc14, V_114), true, nonhuman(V_114, skc14), true)=true))). % 40.31/25.79 tff(c_2124, plain, (ifeq(tuple(true, male(skc13, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.79 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))). % 40.31/25.79 tff(c_25911, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc18), true)=true))). % 40.31/25.79 tff(c_11399, plain, (![V_132]: (ifeq2(accessible_world(skc14, V_132), true, entity(V_132, skc25), true)=true))). % 40.31/25.79 tff(c_1732, plain, (ifeq(tuple(true, existent(skc13, skc17)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_12600, plain, (![V_87]: (ifeq2(accessible_world(skc14, V_87), true, singleton(V_87, skc15), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_3843, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc26), true)=true))). % 40.31/25.79 tff(c_10587, plain, (![V_90]: (ifeq2(accessible_world(skc13, V_90), true, specific(V_90, skc19), true)=true))). % 40.31/25.79 tff(c_2056, plain, (ifeq(tuple(true, male(skc13, skc15)), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_3986, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc25), true)=true))). % 40.31/25.79 tff(c_4251, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc26), true)=true))). % 40.31/25.79 tff(c_4452, plain, (![V_135]: (ifeq2(accessible_world(skc13, V_135), true, existent(V_135, skc19), true)=true))). % 40.31/25.79 tff(c_4403, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc18), true)=true))). % 40.31/25.79 tff(c_1795, plain, (ifeq(tuple(unisex(skc13, skc25), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_3553, plain, (![V_135]: (ifeq2(accessible_world(skc13, V_135), true, existent(V_135, skc25), true)=true))). % 40.31/25.79 tff(c_10488, plain, (![V_87]: (ifeq2(accessible_world(skc13, V_87), true, singleton(V_87, skc14), true)=true))). % 40.31/25.79 tff(c_3742, plain, (![V_117]: (ifeq2(accessible_world(skc13, V_117), true, general(V_117, skc26), true)=true))). % 40.31/25.79 tff(c_10651, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc18), true)=true))). % 40.31/25.79 tff(c_3656, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc26), true)=true))). % 40.31/25.79 tff(c_10726, plain, (![V_90]: (ifeq2(accessible_world(skc13, V_90), true, specific(V_90, skc25), true)=true))). % 40.31/25.79 tff(c_1792, plain, (ifeq(tuple(unisex(skc13, skc19), true), tuple(true, true), a, b)=b)). % 40.31/25.79 tff(c_4366, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc18), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_3806, plain, (![V_84]: (ifeq2(accessible_world(skc13, V_84), true, thing(V_84, skc19), true)=true))). % 40.31/25.79 tff(c_4044, plain, (![V_117]: (ifeq2(accessible_world(skc13, V_117), true, general(V_117, skc18), true)=true))). % 40.31/25.79 tff(c_7405, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc17), true)=true))). % 40.31/25.79 tff(c_8481, plain, (![V_111]: (ifeq2(accessible_world(skc14, V_111), true, abstraction(V_111, skc14), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_10061, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc14), true)=true))). % 40.31/25.79 tff(c_9715, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc15), true)=true))). % 40.31/25.79 tff(c_23235, plain, (![V_782]: (ifeq2(accessible_world(skc13, V_782), true, be(V_782, skc24, skc25, skc25), true)=true))). % 40.31/25.79 tff(c_8736, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, human(V_144, skc19), true)=true))). % 40.31/25.79 tff(c_9815, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc17), true)=true))). % 40.31/25.79 tff(c_9065, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, organism(V_129, skc25), true)=true))). % 40.31/25.79 tff(c_7474, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc24), true)=true))). % 40.31/25.79 tff(c_8171, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc24), true)=true))). % 40.31/25.79 tff(c_9782, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc17), true)=true))). % 40.31/25.79 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))). % 40.31/25.79 tff(c_9394, plain, (![V_90]: (ifeq2(accessible_world(skc14, V_90), true, specific(V_90, skc17), true)=true))). % 40.31/25.79 tff(c_9429, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc26), true)=true))). % 40.31/25.79 tff(c_23843, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc18), true)=true))). % 40.31/25.79 tff(c_7515, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, impartial(V_138, skc25), true)=true))). % 40.31/25.79 tff(c_24021, plain, (![V_361]: (ifeq2(accessible_world(skc13, V_361), true, jules_forename(V_361, skc18), true)=true))). % 40.31/25.79 tff(c_24240, plain, (ifeq3(of(skc13, skc18, skc25), true, skc18, skc26)=skc26)). % 40.31/25.79 tff(c_24207, 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))). % 40.31/25.79 tff(c_23983, plain, (![V_162]: (ifeq2(accessible_world(skc14, V_162), true, jules_forename(V_162, skc18), true)=true))). % 40.31/25.79 tff(c_24164, plain, (ifeq3(of(skc13, skc18, skc25), true, skc26, skc18)=skc18)). % 40.31/25.79 tff(c_24035, plain, (jules_forename(skc13, skc18)=true)). % 40.31/25.79 tff(c_24019, plain, (jules_forename(skc14, skc18)=true)). % 40.31/25.79 tff(c_23972, plain, (skc22=skc18)). % 40.31/25.79 tff(c_23836, plain, (skc20=skc18)). % 40.31/25.79 tff(c_7533, plain, (![V_138]: (ifeq2(accessible_world(skc14, V_138), true, impartial(V_138, skc19), true)=true))). % 40.31/25.79 tff(c_8987, plain, (![V_93]: (ifeq2(accessible_world(skc14, V_93), true, nonexistent(V_93, skc15), true)=true))). % 40.31/25.79 tff(c_7602, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc15), true)=true))). % 40.31/25.79 tff(c_23677, plain, (ifeq3(of(skc13, skc26, skc19), true, skc18, skc26)=skc26)). % 40.31/25.79 tff(c_4214, plain, (![W_402, X_403]: (ifeq3(of(skc13, W_402, X_403), true, ifeq3(of(skc13, skc26, X_403), true, ifeq3(forename(skc13, W_402), true, ifeq3(entity(skc13, X_403), true, W_402, skc26), skc26), skc26), skc26)=skc26))). % 40.31/25.79 tff(c_9915, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc24), true)=true))). % 40.31/25.79 tff(c_23476, plain, (ifeq3(of(skc13, skc26, skc19), true, skc26, skc18)=skc18)). % 40.31/25.79 tff(c_4213, plain, (![X_403, V_404]: (ifeq3(of(skc13, skc26, X_403), true, ifeq3(of(skc13, V_404, X_403), true, ifeq3(forename(skc13, V_404), true, ifeq3(entity(skc13, X_403), true, skc26, V_404), V_404), V_404), V_404)=V_404))). % 40.31/25.79 tff(c_8411, plain, (![V_84]: (ifeq2(accessible_world(skc14, V_84), true, thing(V_84, skc24), true)=true))). % 40.31/25.79 tff(c_9164, plain, (![V_129]: (ifeq2(accessible_world(skc14, V_129), true, organism(V_129, skc19), true)=true))). % 40.31/25.79 tff(c_8307, plain, (![V_144]: (ifeq2(accessible_world(skc14, V_144), true, human(V_144, skc25), true)=true))). % 40.31/25.79 tff(c_3710, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc26), true)=true))). % 40.31/25.79 tff(c_3150, plain, (![V_96]: (ifeq2(accessible_world(skc13, V_96), true, unisex(V_96, skc14), true)=true))). % 40.46/25.79 tff(c_3378, plain, (![V_141]: (ifeq2(accessible_world(skc13, V_141), true, living(V_141, skc19), true)=true))). % 40.46/25.79 tff(c_3604, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc24), true)=true))). % 40.46/25.79 tff(c_3606, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc15), true)=true))). % 40.46/25.79 tff(c_2686, plain, (![V_331]: (ifeq2(accessible_world(skc13, V_331), true, general(V_331, skc14), true)=true))). % 40.46/25.79 tff(c_3534, plain, (![V_373]: (ifeq2(accessible_world(skc13, V_373), true, entity(V_373, skc25), true)=true))). % 40.46/25.79 tff(c_3295, plain, (![V_138]: (ifeq2(accessible_world(skc13, V_138), true, impartial(V_138, skc25), true)=true))). % 40.46/25.80 tff(c_3709, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc18), true)=true))). % 40.46/25.80 tff(c_4068, plain, (![U_399]: (ifeq2(be(U_399, skc24, skc25, skc25), true, ifeq2(accessible_world(U_399, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_3535, plain, (![V_373]: (ifeq2(accessible_world(skc13, V_373), true, entity(V_373, skc19), true)=true))). % 40.46/25.80 tff(c_3605, plain, (![V_376]: (ifeq2(accessible_world(skc13, V_376), true, singleton(V_376, skc17), true)=true))). % 40.46/25.80 tff(c_2388, plain, (![V_114]: (ifeq2(accessible_world(skc13, V_114), true, nonhuman(V_114, skc14), true)=true))). % 40.46/25.80 tff(c_3607, plain, (![V_376]: (ifeq2(accessible_world(skc14, V_376), true, singleton(V_376, skc21), true)=true))). % 40.46/25.80 tff(c_3245, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc14), true)=true))). % 40.46/25.80 tff(c_2973, plain, (![V_138]: (ifeq2(accessible_world(skc13, V_138), true, impartial(V_138, skc19), true)=true))). % 40.46/25.80 tff(c_3198, plain, (![V_141]: (ifeq2(accessible_world(skc13, V_141), true, living(V_141, skc25), true)=true))). % 40.46/25.80 tff(c_21520, plain, (![V_708]: (ifeq2(accessible_world(skc13, V_708), true, agent(V_708, skc17, skc19), true)=true))). % 40.46/25.80 tff(c_7288, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc17), true)=true))). % 40.46/25.80 tff(c_6926, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc24), true)=true))). % 40.46/25.80 tff(c_5883, plain, (![V_150]: (ifeq2(accessible_world(skc14, V_150), true, male(V_150, skc25), true)=true))). % 40.46/25.80 tff(c_8117, plain, (![V_147]: (ifeq2(accessible_world(skc14, V_147), true, animate(V_147, skc25), true)=true))). % 40.46/25.80 tff(c_5544, plain, (![V_150]: (ifeq2(accessible_world(skc14, V_150), true, male(V_150, skc19), true)=true))). % 40.46/25.80 tff(c_6983, plain, (![V_108]: (ifeq2(accessible_world(skc14, V_108), true, relation(V_108, skc14), true)=true))). % 40.46/25.80 tff(c_20611, plain, (![V_671]: (ifeq2(accessible_world(skc14, V_671), true, agent(V_671, skc21, skc19), true)=true))). % 40.46/25.80 tff(c_8098, plain, (![V_147]: (ifeq2(accessible_world(skc14, V_147), true, animate(V_147, skc19), true)=true))). % 40.46/25.80 tff(c_3941, plain, (![U_388]: (ifeq2(agent(U_388, skc17, skc19), true, ifeq2(accessible_world(U_388, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_6381, plain, (![V_81]: (ifeq2(accessible_world(skc14, V_81), true, eventuality(V_81, skc15), true)=true))). % 40.46/25.80 tff(c_5751, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, human_person(V_126, skc25), true)=true))). % 40.46/25.80 tff(c_10011, plain, (![V_96]: (ifeq2(accessible_world(skc14, V_96), true, unisex(V_96, skc15), true)=true))). % 40.46/25.80 tff(c_6703, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc24), true)=true))). % 40.46/25.80 tff(c_19720, plain, (ifeq2(agent(skc13, skf1(skc19), skc19), true, true, true)=true)). % 40.46/25.80 tff(c_5620, plain, (![V_126]: (ifeq2(accessible_world(skc14, V_126), true, human_person(V_126, skc19), true)=true))). % 40.46/25.80 tff(c_6586, plain, (![V_156]: (ifeq2(accessible_world(skc14, V_156), true, relname(V_156, skc26), true)=true))). % 40.46/25.80 tff(c_3868, plain, (![U_384]: (ifeq2(of(U_384, skc18, skc19), true, ifeq2(accessible_world(U_384, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_5145, plain, (![V_156]: (ifeq2(accessible_world(skc14, V_156), true, relname(V_156, skc18), true)=true))). % 40.46/25.80 tff(c_19953, plain, (ifeq2(agent(skc13, skf1(skc25), skc25), true, true, true)=true)). % 40.46/25.80 tff(c_2206, plain, (![V_307]: (ifeq2(accessible_world(skc14, V_307), true, unisex(V_307, skc21), true)=true))). % 40.46/25.80 tff(c_2743, plain, (![V_334]: (ifeq2(accessible_world(skc13, V_334), true, human(V_334, skc19), true)=true))). % 40.46/25.80 tff(c_2578, plain, (![V_325]: (ifeq2(accessible_world(skc14, V_325), true, nonexistent(V_325, skc21), true)=true))). % 40.46/25.80 tff(c_2851, plain, (![V_340]: (ifeq2(accessible_world(skc13, V_340), true, organism(V_340, skc25), true)=true))). % 40.46/25.80 tff(c_2203, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc17), true)=true))). % 40.46/25.80 tff(c_3246, plain, (![V_358]: (ifeq2(accessible_world(skc14, V_358), true, thing(V_358, skc21), true)=true))). % 40.46/25.80 tff(c_2577, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc15), true)=true))). % 40.46/25.80 tff(c_2324, plain, (![V_313]: (ifeq2(accessible_world(skc13, V_313), true, animate(V_313, skc25), true)=true))). % 40.46/25.80 tff(c_2919, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc24), true)=true))). % 40.46/25.80 tff(c_20032, plain, (![V_645]: (ifeq2(accessible_world(skc13, V_645), true, of(V_645, skc18, skc19), true)=true))). % 40.46/25.80 tff(c_2918, plain, (![V_343]: (ifeq2(accessible_world(skc14, V_343), true, specific(V_343, skc21), true)=true))). % 40.46/25.80 tff(c_4016, plain, (![U_392]: (ifeq2(theme(U_392, skc15, skc14), true, ifeq2(accessible_world(U_392, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_2917, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc15), true)=true))). % 40.46/25.80 tff(c_3249, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc24), true)=true))). % 40.46/25.80 tff(c_2205, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc24), true)=true))). % 40.46/25.80 tff(c_2744, plain, (![V_334]: (ifeq2(accessible_world(skc13, V_334), true, human(V_334, skc25), true)=true))). % 40.46/25.80 tff(c_1937, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc18), true)=true))). % 40.46/25.80 tff(c_3247, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc15), true)=true))). % 40.46/25.80 tff(c_1939, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc26), true)=true))). % 40.46/25.80 tff(c_3248, plain, (![V_358]: (ifeq2(accessible_world(skc13, V_358), true, thing(V_358, skc17), true)=true))). % 40.46/25.80 tff(c_3856, plain, (![U_384]: (ifeq2(of(U_384, skc26, skc25), true, ifeq2(accessible_world(U_384, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_2579, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc17), true)=true))). % 40.46/25.80 tff(c_2204, plain, (![V_307]: (ifeq2(accessible_world(skc13, V_307), true, unisex(V_307, skc15), true)=true))). % 40.46/25.80 tff(c_2852, plain, (![V_340]: (ifeq2(accessible_world(skc13, V_340), true, organism(V_340, skc19), true)=true))). % 40.46/25.80 tff(c_2323, plain, (![V_313]: (ifeq2(accessible_world(skc13, V_313), true, animate(V_313, skc19), true)=true))). % 40.46/25.80 tff(c_2916, plain, (![V_343]: (ifeq2(accessible_world(skc13, V_343), true, specific(V_343, skc17), true)=true))). % 40.46/25.80 tff(c_19829, plain, (![V_639]: (ifeq2(accessible_world(skc13, V_639), true, of(V_639, skc26, skc25), true)=true))). % 40.46/25.80 tff(c_3714, plain, (![V_379]: (ifeq2(accessible_world(skc13, V_379), true, abstraction(V_379, skc14), true)=true))). % 40.46/25.80 tff(c_2580, plain, (![V_325]: (ifeq2(accessible_world(skc13, V_325), true, nonexistent(V_325, skc24), true)=true))). % 40.46/25.80 tff(c_3929, plain, (![U_388]: (ifeq2(agent(U_388, skc21, skc19), true, ifeq2(accessible_world(U_388, skc14), true, true, true), true)=true))). % 40.46/25.80 tff(c_4716, plain, (![V_120]: (ifeq2(accessible_world(skc14, V_120), true, state(V_120, skc24), true)=true))). % 40.46/25.80 tff(c_4580, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc17), true)=true))). % 40.46/25.80 tff(c_5224, plain, (![V_105]: (ifeq2(accessible_world(skc14, V_105), true, proposition(V_105, skc14), true)=true))). % 40.46/25.80 tff(c_19607, plain, (![V_632]: (ifeq2(accessible_world(skc13, V_632), true, theme(V_632, skc15, skc14), true)=true))). % 40.46/25.80 tff(c_6022, plain, (![V_162]: (ifeq2(accessible_world(skc14, V_162), true, jules_forename(V_162, skc26), true)=true))). % 40.46/25.80 tff(c_5365, plain, (![V_153]: (ifeq2(accessible_world(skc14, V_153), true, forename(V_153, skc26), true)=true))). % 40.46/25.80 tff(c_3935, plain, (![U_388]: (ifeq2(agent(U_388, skc15, skc19), true, ifeq2(accessible_world(U_388, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_6555, plain, (![V_159]: (ifeq2(accessible_world(skc14, V_159), true, vincent_forename(V_159, skc18), true)=true))). % 40.46/25.80 tff(c_4827, plain, (![V_153]: (ifeq2(accessible_world(skc14, V_153), true, forename(V_153, skc18), true)=true))). % 40.46/25.80 tff(c_4956, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, man(V_123, skc19), true)=true))). % 40.46/25.80 tff(c_6145, plain, (![V_78]: (ifeq2(accessible_world(skc14, V_78), true, event(V_78, skc15), true)=true))). % 40.46/25.80 tff(c_19400, plain, (![V_625]: (ifeq2(accessible_world(skc13, V_625), true, agent(V_625, skc15, skc19), true)=true))). % 40.46/25.80 tff(c_5715, plain, (![V_123]: (ifeq2(accessible_world(skc14, V_123), true, man(V_123, skc25), true)=true))). % 40.46/25.80 tff(c_2115, plain, (![V_304]: (ifeq2(accessible_world(skc13, V_304), true, relname(V_304, skc18), true)=true))). % 40.46/25.80 tff(c_2118, plain, (![V_304]: (ifeq2(accessible_world(skc13, V_304), true, relname(V_304, skc26), true)=true))). % 40.46/25.80 tff(c_3095, plain, (![V_352]: (ifeq2(accessible_world(skc13, V_352), true, human_person(V_352, skc25), true)=true))). % 40.46/25.80 tff(c_3094, plain, (![V_352]: (ifeq2(accessible_world(skc13, V_352), true, human_person(V_352, skc19), true)=true))). % 40.46/25.80 tff(c_2261, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc15), true)=true))). % 40.46/25.80 tff(c_1941, plain, (![V_295]: (ifeq2(accessible_world(skc13, V_295), true, relation(V_295, skc14), true)=true))). % 40.46/25.80 tff(c_3771, plain, (![V_382]: (ifeq2(accessible_world(skc13, V_382), true, male(V_382, skc19), true)=true))). % 40.46/25.80 tff(c_2260, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc17), true)=true))). % 40.46/25.80 tff(c_3772, plain, (![V_382]: (ifeq2(accessible_world(skc13, V_382), true, male(V_382, skc25), true)=true))). % 40.46/25.80 tff(c_2262, plain, (![V_310]: (ifeq2(accessible_world(skc13, V_310), true, eventuality(V_310, skc24), true)=true))). % 40.46/25.80 tff(c_2259, plain, (![V_310]: (ifeq2(accessible_world(skc14, V_310), true, eventuality(V_310, skc21), true)=true))). % 40.46/25.80 tff(c_3047, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc24), true)=true))). % 40.46/25.80 tff(c_19368, plain, (be(skc14, skc24, skc25, skc25)=true)). % 40.46/25.80 tff(c_8315, plain, (![W_450]: (ifeq2(vincent_forename(skc13, W_450), true, vincent_forename(skc14, W_450), true)=true))). % 40.46/25.80 tff(c_2948, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc13), true, ifeq2(man(U_345, skc25), true, true, true), true)=true))). % 40.46/25.80 tff(c_19152, plain, (![V_533]: (ifeq2(nonexistent(skc13, skf1(V_533)), true, true, true)=true))). % 40.46/25.80 tff(c_9075, plain, (![V_455]: (ifeq2(accessible_world(skc13, V_455), true, present(V_455, skc15), true)=true))). % 40.46/25.80 tff(c_19044, plain, (![V_513]: (ifeq2(smoke(skc13, skf1(V_513)), true, true, true)=true))). % 40.46/25.80 tff(c_10543, plain, (![W_466]: (ifeq2(organism(skc13, W_466), true, organism(skc14, W_466), true)=true))). % 40.46/25.80 tff(c_8077, plain, (![W_448]: (ifeq2(animate(skc13, W_448), true, animate(skc14, W_448), true)=true))). % 40.46/25.80 tff(c_18568, plain, (![W_597]: (ifeq2(abstraction(skc13, W_597), true, abstraction(skc14, W_597), true)=true))). % 40.46/25.80 tff(c_10441, plain, (![W_465]: (ifeq2(forename(skc13, W_465), true, forename(skc14, W_465), true)=true))). % 40.46/25.80 tff(c_7794, plain, (![W_446]: (ifeq2(proposition(skc13, W_446), true, proposition(skc14, W_446), true)=true))). % 40.46/25.80 tff(c_11100, plain, (![W_471]: (ifeq2(existent(skc13, W_471), true, existent(skc14, W_471), true)=true))). % 40.46/25.80 tff(c_11933, plain, (![V_477]: (ifeq2(accessible_world(skc13, V_477), true, think_believe_consider(V_477, skc17), true)=true))). % 40.46/25.80 tff(c_7494, plain, (![W_444]: (ifeq2(impartial(skc13, W_444), true, impartial(skc14, W_444), true)=true))). % 40.46/25.80 tff(c_18408, plain, (![V_526]: (ifeq2(specific(skc13, skf1(V_526)), true, true, true)=true))). % 40.46/25.80 tff(c_18097, plain, (![V_531]: (ifeq2(thing(skc13, skf1(V_531)), true, true, true)=true))). % 40.46/25.80 tff(c_18059, plain, (ifeq2(unisex(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_9975, plain, (![W_462]: (ifeq2(unisex(skc13, W_462), true, unisex(skc14, W_462), true)=true))). % 40.46/25.80 tff(c_12569, plain, (![W_486]: (ifeq2(human(skc13, W_486), true, human(skc14, W_486), true)=true))). % 40.46/25.80 tff(c_17907, plain, (![V_522]: (ifeq2(eventuality(skc13, skf1(V_522)), true, true, true)=true))). % 40.46/25.80 tff(c_17796, plain, (![V_536]: (ifeq2(singleton(skc13, skf1(V_536)), true, true, true)=true))). % 40.46/25.80 tff(c_17700, plain, (![V_528]: (ifeq2(unisex(skc13, skf1(V_528)), true, true, true)=true))). % 40.46/25.80 tff(c_8944, plain, (![W_454]: (ifeq2(state(skc13, W_454), true, state(skc14, W_454), true)=true))). % 40.46/25.80 tff(c_17493, plain, (ifeq2(thing(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_17259, plain, (![W_569]: (ifeq2(thing(skc13, W_569), true, thing(skc14, W_569), true)=true))). % 40.46/25.80 tff(c_10803, plain, (![W_468]: (ifeq2(relname(skc13, W_468), true, relname(skc14, W_468), true)=true))). % 40.46/25.80 tff(c_11488, plain, (![V_474]: (ifeq2(accessible_world(skc13, V_474), true, think_believe_consider(V_474, skc15), true)=true))). % 40.46/25.80 tff(c_12106, plain, (![W_479]: (ifeq2(human_person(skc13, W_479), true, human_person(skc14, W_479), true)=true))). % 40.46/25.80 tff(c_12963, plain, (![W_490]: (ifeq2(relation(skc13, W_490), true, relation(skc14, W_490), true)=true))). % 40.46/25.80 tff(c_13987, plain, (![W_500]: (ifeq2(man(skc13, W_500), true, man(skc14, W_500), true)=true))). % 40.46/25.80 tff(c_16940, plain, (ifeq2(singleton(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_14462, plain, (![W_505]: (ifeq2(singleton(skc13, W_505), true, singleton(skc14, W_505), true)=true))). % 40.46/25.80 tff(c_16809, plain, (ifeq2(eventuality(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_15214, plain, (![W_510]: (ifeq2(eventuality(skc13, W_510), true, eventuality(skc14, W_510), true)=true))). % 40.46/25.80 tff(c_8432, plain, (![W_451]: (ifeq2(jules_forename(skc13, W_451), true, jules_forename(skc14, W_451), true)=true))). % 40.46/25.80 tff(c_16724, plain, (![V_516]: (ifeq2(event(skc13, skf1(V_516)), true, true, true)=true))). % 40.46/25.80 tff(c_12666, plain, (![V_487]: (ifeq2(accessible_world(skc14, V_487), true, present(V_487, skc21), true)=true))). % 40.46/25.80 tff(c_13771, plain, (![W_498]: (ifeq2(male(skc13, W_498), true, male(skc14, W_498), true)=true))). % 40.46/25.80 tff(c_3314, plain, (![U_360]: (ifeq2(accessible_world(U_360, skc13), true, ifeq2(jules_forename(U_360, skc26), true, true, true), true)=true))). % 40.46/25.80 tff(c_15631, plain, (![W_518]: (ifeq2(entity(skc13, W_518), true, entity(skc14, W_518), true)=true))). % 40.46/25.80 tff(c_16466, plain, (![W_549]: (ifeq2(living(skc13, W_549), true, living(skc14, W_549), true)=true))). % 40.46/25.80 tff(c_13550, plain, (![V_496]: (ifeq2(accessible_world(skc13, V_496), true, present(V_496, skc17), true)=true))). % 40.46/25.80 tff(c_16427, plain, (ifeq2(specific(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_15053, plain, (![W_509]: (ifeq2(specific(skc13, W_509), true, specific(skc14, W_509), true)=true))). % 40.46/25.80 tff(c_14374, plain, (![W_504]: (ifeq2(nonhuman(skc13, W_504), true, nonhuman(skc14, W_504), true)=true))). % 40.46/25.80 tff(c_14721, plain, (![W_507]: (ifeq2(general(skc13, W_507), true, general(skc14, W_507), true)=true))). % 40.46/25.80 tff(c_16215, plain, (ifeq2(event(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_16161, plain, (![W_543]: (ifeq2(event(skc13, W_543), true, event(skc14, W_543), true)=true))). % 40.46/25.80 tff(c_16135, plain, (ifeq2(smoke(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_14073, plain, (![W_501]: (ifeq2(smoke(skc13, W_501), true, smoke(skc14, W_501), true)=true))). % 40.46/25.80 tff(c_16102, plain, (ifeq2(nonexistent(skc13, skc21), true, true, true)=true)). % 40.46/25.80 tff(c_16030, plain, (![W_538]: (ifeq2(nonexistent(skc13, W_538), true, nonexistent(skc14, W_538), true)=true))). % 40.46/25.80 tff(c_3356, plain, (![U_363]: (ifeq2(accessible_world(U_363, skc13), true, ifeq2(proposition(U_363, skc14), true, true, true), true)=true))). % 40.46/25.80 tff(c_15661, plain, (![V_520]: (ifeq2(present(skc13, skf1(V_520)), true, true, true)=true))). % 40.46/25.80 tff(c_7005, plain, (ifeq2(agent(skc13, skc21, skc19), true, true, true)=true)). % 40.46/25.80 tff(c_2418, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc13), true, ifeq2(forename(U_318, skc26), true, true, true), true)=true))). % 40.46/25.80 tff(c_15107, plain, (agent(skc14, skc17, skc19)=true)). % 40.46/25.80 tff(c_15016, plain, (agent(skc14, skc15, skc19)=true)). % 40.46/25.80 tff(c_14850, plain, (of(skc14, skc18, skc19)=true)). % 40.46/25.80 tff(c_14815, plain, (of(skc14, skc26, skc25)=true)). % 40.46/25.80 tff(c_14780, plain, (theme(skc14, skc15, skc14)=true)). % 40.46/25.80 tff(c_13933, plain, (ifeq2(eventuality(skc14, skc19), true, true, true)=true)). % 40.46/25.80 tff(c_13756, plain, (ifeq2(entity(skc14, skc26), true, true, true)=true)). % 40.46/25.80 tff(c_13924, plain, (ifeq2(abstraction(skc14, skc19), true, true, true)=true)). % 40.46/25.80 tff(c_14533, plain, (singleton(skc14, skc19)=true)). % 40.46/25.80 tff(c_14532, plain, (singleton(skc14, skc26)=true)). % 40.46/25.80 tff(c_14531, plain, (singleton(skc14, skc18)=true)). % 40.46/25.80 tff(c_13506, plain, (ifeq2(eventuality(skc14, skc25), true, true, true)=true)). % 40.46/25.80 tff(c_13497, plain, (ifeq2(abstraction(skc14, skc25), true, true, true)=true)). % 40.46/25.80 tff(c_14392, plain, (singleton(skc14, skc25)=true)). % 40.46/25.80 tff(c_13321, plain, (ifeq2(entity(skc14, skc18), true, true, true)=true)). % 40.46/25.80 tff(c_2627, plain, (![U_327]: (ifeq2(accessible_world(U_327, skc13), true, ifeq2(vincent_forename(U_327, skc18), true, true, true), true)=true))). % 40.46/25.80 tff(c_14003, plain, (specific(skc14, skc19)=true)). % 40.46/25.80 tff(c_13943, plain, (nonhuman(skc14, skc26)=true)). % 40.46/25.80 tff(c_13906, plain, (thing(skc14, skc19)=true)). % 40.46/25.80 tff(c_1986, plain, (![U_297]: (ifeq2(present(U_297, skc15), true, ifeq2(accessible_world(U_297, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_13829, plain, (specific(skc14, skc25)=true)). % 40.46/25.80 tff(c_13732, plain, (thing(skc14, skc26)=true)). % 40.46/25.80 tff(c_2436, plain, (![U_318]: (ifeq2(accessible_world(U_318, skc13), true, ifeq2(forename(U_318, skc18), true, true, true), true)=true))). % 40.46/25.80 tff(c_13628, plain, (singleton(skc14, skc14)=true)). % 40.46/25.80 tff(c_10932, plain, (ifeq2(entity(skc14, skc14), true, true, true)=true)). % 40.46/25.80 tff(c_13479, plain, (thing(skc14, skc25)=true)). % 40.46/25.80 tff(c_2954, plain, (![U_345]: (ifeq2(accessible_world(U_345, skc13), true, ifeq2(man(U_345, skc19), true, true, true), true)=true))). % 40.46/25.80 tff(c_10204, plain, (ifeq2(eventuality(skc14, skc18), true, true, true)=true)). % 40.46/25.80 tff(c_10151, plain, (ifeq2(eventuality(skc14, skc26), true, true, true)=true)). % 40.46/25.80 tff(c_1998, plain, (![U_297]: (ifeq2(present(U_297, skc17), true, ifeq2(accessible_world(U_297, skc13), true, true, true), true)=true))). % 40.46/25.80 tff(c_13297, plain, (thing(skc14, skc18)=true)). % 40.46/25.80 tff(c_13248, plain, (general(skc14, skc26)=true)). % 40.46/25.81 tff(c_3170, plain, (![U_354]: (ifeq2(accessible_world(U_354, skc14), true, ifeq2(smoke(U_354, skc21), true, true, true), true)=true))). % 40.46/25.81 tff(c_13151, plain, (nonhuman(skc14, skc18)=true)). % 40.46/25.81 tff(c_13061, plain, (general(skc14, skc18)=true)). % 40.46/25.81 tff(c_13028, plain, (singleton(skc13, skc18)=true)). % 40.46/25.81 tff(c_3794, plain, (ifeq2(abstraction(skc13, skc19), true, true, true)=true)). % 40.46/25.81 tff(c_3974, plain, (ifeq2(abstraction(skc13, skc25), true, true, true)=true)). % 40.46/25.81 tff(c_12925, plain, (singleton(skc13, skc26)=true)). % 40.46/25.81 tff(c_3983, plain, (ifeq2(eventuality(skc13, skc25), true, true, true)=true)). % 40.46/25.81 tff(c_4397, plain, (ifeq2(entity(skc13, skc18), true, true, true)=true)). % 40.46/25.81 tff(c_12822, plain, (singleton(skc13, skc19)=true)). % 40.46/25.81 tff(c_4360, plain, (ifeq2(eventuality(skc13, skc18), true, true, true)=true)). % 40.46/25.81 tff(c_3837, plain, (ifeq2(entity(skc13, skc26), true, true, true)=true)). % 40.46/25.81 tff(c_3840, plain, (ifeq2(eventuality(skc13, skc26), true, true, true)=true)). % 40.46/25.81 tff(c_12704, plain, (singleton(skc13, skc25)=true)). % 40.46/25.81 tff(c_10584, plain, (ifeq2(eventuality(skc13, skc19), true, true, true)=true)). % 40.46/25.81 tff(c_12579, plain, (singleton(skc14, skc15)=true)). % 40.46/25.81 tff(c_9912, plain, (ifeq2(abstraction(skc14, skc24), true, true, true)=true)). % 40.46/25.81 tff(c_3044, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc17), true, true, true), true)=true))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_9388, plain, (ifeq2(entity(skc14, skc17), true, true, true)=true)). % 40.46/25.81 tff(c_1992, plain, (![U_297]: (ifeq2(present(U_297, skc21), true, ifeq2(accessible_world(U_297, skc14), true, true, true), true)=true))). % 40.46/25.81 tff(c_12275, plain, (entity(skc14, skc19)=true)). % 40.46/25.81 tff(c_12244, plain, (nonhuman(skc14, skc14)=true)). % 40.46/25.81 tff(c_7393, plain, (ifeq2(abstraction(skc14, skc17), true, true, true)=true)). % 40.46/25.81 tff(c_8926, plain, (ifeq2(proposition(skc14, skc18), true, true, true)=true)). % 40.46/25.81 tff(c_12033, plain, (general(skc14, skc14)=true)). % 40.46/25.81 tff(c_3038, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc14), true, ifeq2(event(U_348, skc21), true, true, true), true)=true))). % 40.46/25.81 tff(c_11973, plain, (abstraction(skc14, skc18)=true)). % 40.46/25.81 tff(c_11609, plain, (living(skc14, skc25)=true)). % 40.46/25.81 tff(c_8165, plain, (ifeq2(entity(skc14, skc24), true, true, true)=true)). % 40.46/25.81 tff(c_2489, plain, (![U_321]: (ifeq2(accessible_world(U_321, skc13), true, ifeq2(state(U_321, skc24), true, true, true), true)=true))). % 40.46/25.81 tff(c_11448, plain, (singleton(skc14, skc17)=true)). % 40.46/25.81 tff(c_11407, plain, (abstraction(skc14, skc26)=true)). % 40.46/25.81 tff(c_11365, plain, (entity(skc14, skc25)=true)). % 40.46/25.81 tff(c_11188, plain, (living(skc14, skc19)=true)). % 40.46/25.81 tff(c_11104, plain, (existent(skc14, skc25)=true)). % 40.46/25.81 tff(c_11103, plain, (existent(skc14, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_7596, plain, (ifeq2(entity(skc14, skc15), true, true, true)=true)). % 40.46/25.81 tff(c_10908, plain, (thing(skc14, skc14)=true)). % 40.46/25.81 tff(c_10054, plain, (ifeq2(eventuality(skc14, skc14), true, true, true)=true)). % 40.46/25.81 tff(c_10853, plain, (singleton(skc14, skc24)=true)). % 40.46/25.81 tff(c_9420, plain, (ifeq2(proposition(skc14, skc26), true, true, true)=true)). % 40.46/25.81 tff(c_10699, plain, (specific(skc13, skc25)=true)). % 40.46/25.81 tff(c_10623, plain, (nonhuman(skc13, skc18)=true)). % 40.46/25.81 tff(c_10531, plain, (specific(skc13, skc19)=true)). % 40.46/25.81 tff(c_2817, plain, (ifeq2(entity(skc13, skc14), true, true, true)=true)). % 40.46/25.81 tff(c_10467, plain, (singleton(skc13, skc14)=true)). % 40.46/25.81 tff(c_10007, plain, (ifeq2(abstraction(skc14, skc15), true, true, true)=true)). % 40.46/25.81 tff(c_9980, plain, (unisex(skc14, skc18)=true)). % 40.46/25.81 tff(c_9981, plain, (unisex(skc14, skc26)=true)). % 40.46/25.81 tff(c_9984, plain, (unisex(skc14, skc14)=true)). % 40.46/25.81 tff(c_6980, plain, (ifeq2(relname(skc14, skc14), true, true, true)=true)). % 40.46/25.81 tff(c_9987, plain, (unisex(skc14, skc15)=true)). % 40.46/25.81 tff(c_9888, plain, (unisex(skc14, skc24)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_9791, plain, (nonexistent(skc14, skc17)=true)). % 40.46/25.81 tff(c_9755, plain, (unisex(skc14, skc17)=true)). % 40.46/25.81 tff(c_9741, plain, (ifeq2(accessible_world(skc14, skc13), true, true, true)=true)). % 40.46/25.81 tff(c_3032, plain, (![U_348]: (ifeq2(accessible_world(U_348, skc13), true, ifeq2(event(U_348, skc15), true, true, true), true)=true))). % 40.46/25.81 tff(c_9688, plain, (specific(skc14, skc15)=true)). % 40.46/25.81 tff(c_6700, plain, (ifeq2(smoke(skc14, skc24), true, true, true)=true)). % 40.46/25.81 tff(c_9402, plain, (relation(skc14, skc26)=true)). % 40.46/25.81 tff(c_9367, plain, (specific(skc14, skc17)=true)). % 40.46/25.81 tff(c_9134, plain, (organism(skc14, skc19)=true)). % 40.46/25.81 tff(c_9035, plain, (organism(skc14, skc25)=true)). % 40.46/25.81 tff(c_8963, plain, (nonexistent(skc14, skc15)=true)). % 40.46/25.81 tff(c_8908, plain, (relation(skc14, skc18)=true)). % 40.46/25.81 tff(c_8688, plain, (human(skc14, skc19)=true)). % 40.46/25.81 tff(c_8448, plain, (abstraction(skc14, skc14)=true)). % 40.46/25.81 tff(c_8381, plain, (thing(skc14, skc24)=true)). % 40.46/25.81 tff(c_8283, plain, (human(skc14, skc25)=true)). % 40.46/25.81 tff(c_8144, plain, (specific(skc14, skc24)=true)). % 40.46/25.81 tff(c_8081, plain, (animate(skc14, skc25)=true)). % 40.46/25.81 tff(c_8080, plain, (animate(skc14, skc19)=true)). % 40.46/25.81 tff(c_7572, plain, (thing(skc14, skc15)=true)). % 40.46/25.81 tff(c_7498, plain, (impartial(skc14, skc19)=true)). % 40.46/25.81 tff(c_7497, plain, (impartial(skc14, skc25)=true)). % 40.46/25.81 tff(c_7450, plain, (nonexistent(skc14, skc24)=true)). % 40.46/25.81 tff(c_7362, plain, (thing(skc14, skc17)=true)). % 40.46/25.81 tff(c_7233, plain, (eventuality(skc14, skc17)=true)). % 40.46/25.81 tff(c_3884, plain, (![W_385, X_386]: (ifeq2(of(skc13, W_385, X_386), true, of(skc14, W_385, X_386), true)=true))). % 40.46/25.81 tff(c_3951, plain, (![W_389, X_390]: (ifeq2(agent(skc13, W_389, X_390), true, agent(skc14, W_389, X_390), true)=true))). % 40.46/25.81 tff(c_6141, plain, (ifeq2(smoke(skc14, skc15), true, true, true)=true)). % 40.46/25.81 tff(c_6956, plain, (relation(skc14, skc14)=true)). % 40.46/25.81 tff(c_5353, plain, (ifeq2(vincent_forename(skc14, skc26), true, true, true)=true)). % 40.46/25.81 tff(c_6890, plain, (eventuality(skc14, skc24)=true)). % 40.46/25.81 tff(c_4026, plain, (![W_393, X_394]: (ifeq2(theme(skc13, W_393, X_394), true, theme(skc14, W_393, X_394), true)=true))). % 40.46/25.81 tff(c_6676, plain, (event(skc14, skc24)=true)). % 40.46/25.81 tff(c_6562, plain, (relname(skc14, skc26)=true)). % 40.46/25.81 tff(c_6530, plain, (vincent_forename(skc14, skc18)=true)). % 40.46/25.81 tff(c_2631, plain, (![V_328]: (ifeq2(accessible_world(skc13, V_328), true, vincent_forename(V_328, skc18), true)=true))). % 40.46/25.81 tff(c_6135, plain, (ifeq2(state(skc14, skc15), true, true, true)=true)). % 40.46/25.81 tff(c_6345, plain, (eventuality(skc14, skc15)=true)). % 40.46/25.81 tff(c_6306, plain, (think_believe_consider(skc14, skc15)=true)). % 40.46/25.81 tff(c_6271, plain, (think_believe_consider(skc14, skc17)=true)). % 40.46/25.81 tff(c_3494, plain, (![W_370]: (ifeq2(think_believe_consider(skc13, W_370), true, think_believe_consider(skc14, W_370), true)=true))). % 40.46/25.81 tff(c_4576, plain, (ifeq2(smoke(skc14, skc17), true, true, true)=true)). % 40.46/25.81 tff(c_6114, plain, (event(skc14, skc15)=true)). % 40.46/25.81 tff(c_3048, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc15), true)=true))). % 40.46/25.81 tff(c_5997, plain, (jules_forename(skc14, skc26)=true)). % 40.46/25.81 tff(c_3323, plain, (![V_361]: (ifeq2(accessible_world(skc13, V_361), true, jules_forename(V_361, skc26), true)=true))). % 40.46/25.81 tff(c_5860, plain, (ifeq2(present(skc13, skc21), true, true, true)=true)). % 40.46/25.81 tff(c_5917, plain, (present(skc14, skc17)=true)). % 40.46/25.81 tff(c_5890, plain, (present(skc14, skc15)=true)). % 40.46/25.81 tff(c_5843, plain, (male(skc14, skc25)=true)). % 40.46/25.81 tff(c_2002, plain, (![W_298]: (ifeq2(present(skc13, W_298), true, present(skc14, W_298), true)=true))). % 40.46/25.81 tff(c_5721, plain, (human_person(skc14, skc25)=true)). % 40.46/25.81 tff(c_5687, plain, (man(skc14, skc25)=true)). % 40.46/25.81 tff(c_2957, plain, (![V_346]: (ifeq2(accessible_world(skc13, V_346), true, man(V_346, skc25), true)=true))). % 40.46/25.81 tff(c_5590, plain, (human_person(skc14, skc19)=true)). % 40.46/25.81 tff(c_5509, plain, (male(skc14, skc19)=true)). % 40.46/25.81 tff(c_3173, plain, (![V_355]: (ifeq2(accessible_world(skc14, V_355), true, smoke(V_355, skc21), true)=true))). % 40.46/25.81 tff(c_5326, plain, (forename(skc14, skc26)=true)). % 40.46/25.81 tff(c_2439, plain, (![V_319]: (ifeq2(accessible_world(skc13, V_319), true, forename(V_319, skc26), true)=true))). % 40.46/25.81 tff(c_5191, plain, (proposition(skc14, skc14)=true)). % 40.46/25.81 tff(c_5104, plain, (relname(skc14, skc18)=true)). % 40.46/25.81 tff(c_3363, plain, (![V_364]: (ifeq2(accessible_world(skc13, V_364), true, proposition(V_364, skc14), true)=true))). % 40.46/25.81 tff(c_4928, plain, (man(skc14, skc19)=true)). % 40.46/25.81 tff(c_2958, plain, (![V_346]: (ifeq2(accessible_world(skc13, V_346), true, man(V_346, skc19), true)=true))). % 40.46/25.81 tff(c_4788, plain, (forename(skc14, skc18)=true)). % 40.46/25.81 tff(c_2442, plain, (![V_319]: (ifeq2(accessible_world(skc13, V_319), true, forename(V_319, skc18), true)=true))). % 40.46/25.81 tff(c_4570, plain, (ifeq2(state(skc14, skc17), true, true, true)=true)). % 40.46/25.81 tff(c_4688, plain, (state(skc14, skc24)=true)). % 40.46/25.81 tff(c_2492, plain, (![V_322]: (ifeq2(accessible_world(skc13, V_322), true, state(V_322, skc24), true)=true))). % 40.46/25.81 tff(c_4506, plain, (ifeq2(accessible_world(skc13, skc13), true, true, true)=true)). % 40.46/25.81 tff(c_4549, plain, (event(skc14, skc17)=true)). % 40.46/25.81 tff(c_3050, plain, (![V_349]: (ifeq2(accessible_world(skc13, V_349), true, event(V_349, skc17), true)=true))). % 40.46/25.81 tff(c_4428, plain, (existent(skc13, skc19)=true)). % 40.46/25.81 tff(c_2820, plain, (ifeq2(eventuality(skc13, skc14), true, true, true)=true)). % 40.46/25.81 tff(c_4413, plain, (ifeq2(accessible_world(skc14, skc14), true, true, true)=true)). % 40.46/25.81 tff(c_3049, plain, (![V_349]: (ifeq2(accessible_world(skc14, V_349), true, event(V_349, skc21), true)=true))). % 40.46/25.81 tff(c_4373, plain, (thing(skc13, skc18)=true)). % 40.46/25.81 tff(c_4339, plain, (unisex(skc13, skc18)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_4224, plain, (unisex(skc13, skc26)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3993, plain, (general(skc13, skc18)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3956, plain, (thing(skc13, skc25)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3813, plain, (thing(skc13, skc26)=true)). % 40.46/25.81 tff(c_3776, plain, (thing(skc13, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3718, plain, (general(skc13, skc26)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3632, plain, (nonhuman(skc13, skc26)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3502, plain, (existent(skc13, skc25)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3439, plain, (abstraction(skc13, skc18)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_977, plain, (ifeq2(proposition(skc13, skc26), true, true, true)=true)). % 40.46/25.81 tff(c_3330, plain, (living(skc13, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3274, plain, (impartial(skc13, skc25)=true)). % 40.46/25.81 tff(c_3253, plain, (singleton(skc13, skc24)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3177, plain, (living(skc13, skc25)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_3123, plain, (unisex(skc13, skc14)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2062, plain, (ifeq2(abstraction(skc13, skc15), true, true, true)=true)). % 40.46/25.81 tff(c_1418, plain, (ifeq2(entity(skc13, skc24), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2980, plain, (abstraction(skc13, skc26)=true)). % 40.46/25.81 tff(c_2925, plain, (impartial(skc13, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_1374, plain, (ifeq2(abstraction(skc13, skc24), true, true, true)=true)). % 40.46/25.81 tff(c_2856, plain, (singleton(skc13, skc17)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2799, plain, (thing(skc13, skc14)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2691, plain, (entity(skc13, skc25)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2640, plain, (general(skc13, skc14)=true)). % 40.46/25.81 tff(c_1773, plain, (ifeq2(entity(skc13, skc15), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2588, plain, (singleton(skc13, skc15)=true)). % 40.46/25.81 tff(c_1962, plain, (ifeq2(entity(skc13, skc17), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2395, plain, (entity(skc13, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2364, plain, (nonhuman(skc13, skc14)=true)). % 40.46/25.81 tff(c_1093, plain, (ifeq2(proposition(skc13, skc18), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_1478, plain, (ifeq2(abstraction(skc14, skc21), true, true, true)=true)). % 40.46/25.81 tff(c_1579, plain, (ifeq2(abstraction(skc13, skc17), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2219, plain, (singleton(skc14, skc21)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2157, plain, (ifeq2(entity(skc14, skc21), true, true, true)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2139, plain, (thing(skc14, skc21)=true)). % 40.46/25.81 tff(c_2071, plain, (unisex(skc13, skc17)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2031, plain, (unisex(skc13, skc15)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_2007, plain, (human(skc13, skc19)=true)). % 40.46/25.81 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))). % 40.46/25.81 tff(c_1947, plain, (specific(skc13, skc17)=true)). % 40.46/25.82 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))). % 40.46/25.82 tff(c_1865, plain, (unisex(skc13, skc24)=true)). % 40.46/25.82 tff(c_1841, plain, (nonexistent(skc13, skc15)=true)). % 40.46/25.82 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))). % 40.46/25.82 tff(c_1801, plain, (specific(skc13, skc15)=true)). % 40.46/25.82 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))). % 40.46/25.82 tff(c_1755, plain, (thing(skc13, skc15)=true)). % 40.46/25.82 tff(c_1715, plain, (specific(skc14, skc21)=true)). % 40.46/25.82 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))). % 40.46/25.82 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))). % 40.46/25.82 tff(c_1683, plain, (human(skc13, skc25)=true)). % 40.46/25.82 tff(c_1653, plain, (organism(skc13, skc25)=true)). % 40.46/25.82 tff(c_1625, plain, (nonexistent(skc14, skc21)=true)). % 40.46/25.82 tff(c_1597, plain, (nonexistent(skc13, skc17)=true)). % 40.46/25.82 tff(c_1564, plain, (thing(skc13, skc17)=true)). % 40.46/25.82 tff(c_1531, plain, (nonexistent(skc13, skc24)=true)). % 40.46/25.82 tff(c_1510, plain, (animate(skc13, skc19)=true)). % 40.46/25.82 tff(c_18, plain, (![U_20, V_21]: (ifeq2(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 40.46/25.82 tff(c_1446, plain, (ifeq2(smoke(skc13, skc24), true, true, true)=true)). % 40.46/25.82 tff(c_1456, plain, (unisex(skc14, skc21)=true)). % 40.46/25.82 tff(c_48, plain, (![U_50, V_51]: (ifeq2(entity(U_50, V_51), true, existent(U_50, V_51), true)=true))). % 40.46/25.82 tff(c_1428, plain, (event(skc13, skc24)=true)). % 40.46/25.82 tff(c_1317, plain, (ifeq2(state(skc13, skc17), true, true, true)=true)). % 40.46/25.82 tff(c_46, plain, (![U_48, V_49]: (ifeq2(entity(U_48, V_49), true, specific(U_48, V_49), true)=true))). % 40.46/25.82 tff(c_1380, plain, (eventuality(skc14, skc21)=true)). % 40.46/25.82 tff(c_26, plain, (![U_28, V_29]: (ifeq2(abstraction(U_28, V_29), true, thing(U_28, V_29), true)=true))). % 40.46/25.82 tff(c_1311, plain, (ifeq2(state(skc14, skc21), true, true, true)=true)). % 40.46/25.82 tff(c_1308, plain, (ifeq2(state(skc13, skc15), true, true, true)=true)). % 40.46/25.82 tff(c_1323, plain, (eventuality(skc13, skc17)=true)). % 40.46/25.82 tff(c_36, plain, (![U_38, V_39]: (ifeq2(state(U_38, V_39), true, event(U_38, V_39), true)=true))). % 40.46/25.82 tff(c_1271, plain, (eventuality(skc13, skc15)=true)). % 40.46/25.82 tff(c_10, plain, (![U_12, V_13]: (ifeq2(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 40.46/25.82 tff(c_1222, plain, (organism(skc13, skc19)=true)). % 40.46/25.82 tff(c_1195, plain, (animate(skc13, skc25)=true)). % 40.46/25.82 tff(c_14, plain, (![U_16, V_17]: (ifeq2(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 40.46/25.82 tff(c_1155, plain, (human_person(skc13, skc19)=true)). % 40.46/25.82 tff(c_20, plain, (![U_22, V_23]: (ifeq2(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 40.46/25.82 tff(c_1121, plain, (human_person(skc13, skc25)=true)). % 40.46/25.82 tff(c_38, plain, (![U_40, V_41]: (ifeq2(man(U_40, V_41), true, human_person(U_40, V_41), true)=true))). % 40.46/25.82 tff(c_1081, plain, (relation(skc13, skc18)=true)). % 40.46/25.82 tff(c_799, plain, (ifeq2(relname(skc13, skc14), true, true, true)=true)). % 40.46/25.82 tff(c_42, plain, (![U_44, V_45]: (ifeq2(organism(U_44, V_45), true, entity(U_44, V_45), true)=true))). % 40.46/25.82 tff(c_40, plain, (![U_42, V_43]: (ifeq2(human_person(U_42, V_43), true, organism(U_42, V_43), true)=true))). % 40.46/25.82 tff(c_30, plain, (![U_32, V_33]: (ifeq2(abstraction(U_32, V_33), true, general(U_32, V_33), true)=true))). % 40.46/25.82 tff(c_965, plain, (relation(skc13, skc26)=true)). % 40.46/25.82 tff(c_28, plain, (![U_30, V_31]: (ifeq2(abstraction(U_30, V_31), true, nonhuman(U_30, V_31), true)=true))). % 40.46/25.82 tff(c_894, plain, (ifeq2(vincent_forename(skc13, skc26), true, true, true)=true)). % 40.46/25.82 tff(c_64, plain, (![U_66, V_67]: (ifeq2(vincent_forename(U_66, V_67), true, forename(U_66, V_67), true)=true))). % 40.46/25.82 tff(c_867, plain, (abstraction(skc13, skc14)=true)). % 40.46/25.82 tff(c_846, plain, (specific(skc13, skc24)=true)). % 40.46/25.82 tff(c_44, plain, (![U_46, V_47]: (ifeq2(entity(U_46, V_47), true, thing(U_46, V_47), true)=true))). % 40.46/25.82 tff(c_815, plain, (thing(skc13, skc24)=true)). % 40.46/25.82 tff(c_50, plain, (![U_52, V_53]: (ifeq2(organism(U_52, V_53), true, impartial(U_52, V_53), true)=true))). % 40.46/25.82 tff(c_781, plain, (relation(skc13, skc14)=true)). % 40.46/25.82 tff(c_745, plain, (eventuality(skc13, skc24)=true)). % 40.46/25.82 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))). % 40.46/25.82 tff(c_34, plain, (![U_36, V_37]: (ifeq2(state(U_36, V_37), true, eventuality(U_36, V_37), true)=true))). % 40.46/25.82 tff(c_680, plain, (relname(skc13, skc18)=true)). % 40.46/25.82 tff(c_22, plain, (![U_24, V_25]: (ifeq2(proposition(U_24, V_25), true, relation(U_24, V_25), true)=true))). % 40.46/25.82 tff(c_52, plain, (![U_54, V_55]: (ifeq2(organism(U_54, V_55), true, living(U_54, V_55), true)=true))). % 40.46/25.82 tff(c_588, plain, (relname(skc13, skc26)=true)). % 40.46/25.82 tff(c_60, plain, (![U_62, V_63]: (ifeq2(forename(U_62, V_63), true, relname(U_62, V_63), true)=true))). % 40.46/25.82 tff(c_24, plain, (![U_26, V_27]: (ifeq2(relation(U_26, V_27), true, abstraction(U_26, V_27), true)=true))). % 40.46/25.82 tff(c_32, plain, (![U_34, V_35]: (ifeq2(abstraction(U_34, V_35), true, unisex(U_34, V_35), true)=true))). % 40.46/25.82 tff(c_526, plain, (male(skc13, skc19)=true)). % 40.46/25.82 tff(c_476, plain, (male(skc13, skc25)=true)). % 40.46/25.82 tff(c_66, plain, (![U_68, V_69]: (ifeq2(jules_forename(U_68, V_69), true, forename(U_68, V_69), true)=true))). % 40.46/25.82 tff(c_58, plain, (![U_60, V_61]: (ifeq2(man(U_60, V_61), true, male(U_60, V_61), true)=true))). % 40.46/25.82 tff(c_62, plain, (![U_64, V_65]: (ifeq2(relname(U_64, V_65), true, relation(U_64, V_65), true)=true))). % 40.46/25.82 tff(c_12, plain, (![U_14, V_15]: (ifeq2(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 40.46/25.82 tff(c_56, plain, (![U_58, V_59]: (ifeq2(human_person(U_58, V_59), true, animate(U_58, V_59), true)=true))). % 40.46/25.82 tff(c_423, plain, (ifeq2(smoke(skc13, skc17), true, true, true)=true)). % 40.46/25.82 tff(c_417, plain, (ifeq2(smoke(skc13, skc15), true, true, true)=true)). % 40.46/25.82 tff(c_8, plain, (![U_10, V_11]: (ifeq2(smoke(U_10, V_11), true, event(U_10, V_11), true)=true))). % 40.46/25.82 tff(c_16, plain, (![U_18, V_19]: (ifeq2(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 40.46/25.82 tff(c_54, plain, (![U_56, V_57]: (ifeq2(human_person(U_56, V_57), true, human(U_56, V_57), true)=true))). % 40.46/25.82 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 40.46/25.82 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 40.46/25.82 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 40.46/25.82 tff(c_210, plain, (be(skc13, skc24, skc25, skc25)=true)). % 40.46/25.82 tff(c_208, plain, (theme(skc13, skc15, skc14)=true)). % 40.46/25.82 tff(c_192, plain, (of(skc13, skc26, skc25)=true)). % 40.46/25.82 tff(c_198, plain, (of(skc13, skc18, skc19)=true)). % 40.46/25.82 tff(c_204, plain, (agent(skc14, skc21, skc19)=true)). % 40.46/25.82 tff(c_202, plain, (agent(skc13, skc15, skc19)=true)). % 40.46/25.82 tff(c_200, plain, (agent(skc13, skc17, skc19)=true)). % 40.46/25.82 tff(c_186, plain, (proposition(skc13, skc14)=true)). % 40.46/25.82 tff(c_188, plain, (accessible_world(skc13, skc14)=true)). % 40.46/25.82 tff(c_144, plain, (jules_forename(skc13, skc26)=true)). % 40.46/25.82 tff(c_146, plain, (forename(skc13, skc26)=true)). % 40.46/25.82 tff(c_180, plain, (event(skc13, skc15)=true)). % 40.46/25.82 tff(c_178, plain, (present(skc13, skc15)=true)). % 40.46/25.82 tff(c_150, plain, (event(skc14, skc21)=true)). % 40.46/25.82 tff(c_174, plain, (think_believe_consider(skc13, skc17)=true)). % 40.46/25.82 tff(c_148, plain, (man(skc13, skc25)=true)). % 40.46/25.82 tff(c_190, plain, (state(skc13, skc24)=true)). % 40.46/25.82 tff(c_176, plain, (think_believe_consider(skc13, skc15)=true)). % 40.46/25.82 tff(c_158, plain, (present(skc14, skc21)=true)). % 40.46/25.82 tff(c_172, plain, (present(skc13, skc17)=true)). % 40.46/25.82 tff(c_156, plain, (man(skc13, skc19)=true)). % 40.46/25.82 tff(c_170, plain, (event(skc13, skc17)=true)). % 40.46/25.82 tff(c_168, plain, (vincent_forename(skc13, skc18)=true)). % 40.46/25.82 tff(c_160, plain, (smoke(skc14, skc21)=true)). % 40.46/25.82 tff(c_166, plain, (forename(skc13, skc18)=true)). % 40.46/25.82 tff(c_142, plain, (actual_world(skc13)=true)). % 40.46/25.82 tff(c_228, plain, (b!=a)). % 40.46/25.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.46/25.82 %------------------------------------------------------------------------------