%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP255-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.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:48 PM UTC 2025 % Result : Satisfiable 11.63s 3.77s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP255-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n013.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 09:50:17 EDT 2025 % 0.13/0.34 % CPUTime : % 11.63/3.77 % 11.63/3.77 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.63/3.77 % 11.63/3.77 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.63/3.78 %$ be > theme > of > agent > vincent_forename > unisex > 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 > actual_world > #nlpp > skf4 > skf2 > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 % 11.63/3.78 % 11.63/3.78 %Foreground sorts: % 11.63/3.78 % 11.63/3.78 % 11.63/3.78 %Background operators: % 11.63/3.78 % 11.63/3.78 % 11.63/3.78 %Foreground operators: % 11.63/3.78 tff(relation, type, relation: ($i * $i) > $o). % 11.63/3.78 tff(skf4, type, skf4: $i > $i). % 11.63/3.78 tff(forename, type, forename: ($i * $i) > $o). % 11.63/3.78 tff(be, type, be: ($i * $i * $i * $i) > $o). % 11.63/3.78 tff(theme, type, theme: ($i * $i * $i) > $o). % 11.63/3.78 tff(living, type, living: ($i * $i) > $o). % 11.63/3.78 tff(human_person, type, human_person: ($i * $i) > $o). % 11.63/3.78 tff(present, type, present: ($i * $i) > $o). % 11.63/3.78 tff(skc11, type, skc11: $i). % 11.63/3.78 tff(entity, type, entity: ($i * $i) > $o). % 11.63/3.78 tff(skc9, type, skc9: $i). % 11.63/3.78 tff(eventuality, type, eventuality: ($i * $i) > $o). % 11.63/3.78 tff(existent, type, existent: ($i * $i) > $o). % 11.63/3.78 tff(abstraction, type, abstraction: ($i * $i) > $o). % 11.63/3.78 tff(skc8, type, skc8: $i). % 11.63/3.78 tff(proposition, type, proposition: ($i * $i) > $o). % 11.63/3.78 tff(relname, type, relname: ($i * $i) > $o). % 11.63/3.78 tff(skc14, type, skc14: $i). % 11.63/3.78 tff(singleton, type, singleton: ($i * $i) > $o). % 11.63/3.78 tff(skc13, type, skc13: $i). % 11.63/3.78 tff(male, type, male: ($i * $i) > $o). % 11.63/3.78 tff(organism, type, organism: ($i * $i) > $o). % 11.63/3.78 tff(animate, type, animate: ($i * $i) > $o). % 11.63/3.78 tff(of, type, of: ($i * $i * $i) > $o). % 11.63/3.78 tff(actual_world, type, actual_world: $i > $o). % 11.63/3.78 tff(agent, type, agent: ($i * $i * $i) > $o). % 11.63/3.78 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 11.63/3.78 tff(general, type, general: ($i * $i) > $o). % 11.63/3.78 tff(smoke, type, smoke: ($i * $i) > $o). % 11.63/3.78 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 11.63/3.78 tff(event, type, event: ($i * $i) > $o). % 11.63/3.78 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 11.63/3.78 tff(state, type, state: ($i * $i) > $o). % 11.63/3.78 tff(thing, type, thing: ($i * $i) > $o). % 11.63/3.78 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 11.63/3.78 tff(skc15, type, skc15: $i). % 11.63/3.78 tff(human, type, human: ($i * $i) > $o). % 11.63/3.78 tff(skf2, type, skf2: $i > $i). % 11.63/3.78 tff(man, type, man: ($i * $i) > $o). % 11.63/3.78 tff(unisex, type, unisex: ($i * $i) > $o). % 11.63/3.78 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 11.63/3.78 tff(impartial, type, impartial: ($i * $i) > $o). % 11.63/3.78 tff(skc12, type, skc12: $i). % 11.63/3.78 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 11.63/3.78 tff(specific, type, specific: ($i * $i) > $o). % 11.63/3.78 tff(skc10, type, skc10: $i). % 11.63/3.78 % 11.63/3.78 %Saturated clause set: % 11.63/3.78 tff(c_4830, plain, (![Z_1661, V_1656, X2_1664, V_901, Y_1660, X_1663, W_1657, V_1659]: (~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~agent(V_901, X2_1664, skc10) | ~man(V_901, skc10) | ~forename(V_901, skc11) | ~vincent_forename(V_901, skc11) | ~state(V_901, skc9) | ~think_believe_consider(V_901, X2_1664) | ~present(V_901, X2_1664) | ~event(V_901, X2_1664) | ~theme(V_901, X2_1664, V_1656) | ~proposition(V_901, V_1656) | ~accessible_world(V_901, V_1656) | ~of(V_901, Y_1660, Z_1661) | ~man(V_901, Z_1661) | ~agent(V_901, X_1663, Z_1661) | ~forename(V_901, Y_1660) | ~vincent_forename(V_901, Y_1660) | ~theme(V_901, X_1663, V_1659) | ~event(V_901, X_1663) | ~present(V_901, X_1663) | ~think_believe_consider(V_901, X_1663) | ~event(V_1659, W_1657) | ~agent(V_1659, W_1657, skf4(V_1659)) | ~present(V_1659, W_1657) | ~smoke(V_1659, W_1657) | ~accessible_world(V_901, V_1659) | ~proposition(V_901, V_1659) | ~accessible_world(skc12, V_1656) | ~accessible_world(skc8, V_901)))). % 11.63/3.78 tff(c_4821, plain, (![V_1655, Z_1649, V_928, X2_1654, X4_1648, Y_1647, W_1650, X_1652, V_1651]: (~actual_world(V_928) | ~jules_forename(V_928, skc11) | ~forename(V_928, skc11) | ~agent(V_928, X2_1654, skc10) | ~man(V_928, skc10) | ~forename(V_928, X4_1648) | ~vincent_forename(V_928, X4_1648) | ~of(V_928, X4_1648, skc10) | ~state(V_928, skc9) | ~think_believe_consider(V_928, X2_1654) | ~present(V_928, X2_1654) | ~event(V_928, X2_1654) | ~theme(V_928, X2_1654, V_1655) | ~proposition(V_928, V_1655) | ~accessible_world(V_928, V_1655) | ~of(V_928, Y_1647, Z_1649) | ~man(V_928, Z_1649) | ~agent(V_928, X_1652, Z_1649) | ~forename(V_928, Y_1647) | ~vincent_forename(V_928, Y_1647) | ~theme(V_928, X_1652, V_1651) | ~event(V_928, X_1652) | ~present(V_928, X_1652) | ~think_believe_consider(V_928, X_1652) | ~event(V_1651, W_1650) | ~agent(V_1651, W_1650, skf4(V_1651)) | ~present(V_1651, W_1650) | ~smoke(V_1651, W_1650) | ~accessible_world(V_928, V_1651) | ~proposition(V_928, V_1651) | ~accessible_world(skc12, V_1655) | ~accessible_world(skc8, V_928)))). % 11.63/3.78 tff(c_4814, plain, (![Y_1643, Z_1641, X_1645, V_1636, X2_1637, V_811, X3_1638, X4_1639, W_1642, V_1640]: (~actual_world(V_1640) | ~jules_forename(V_1640, skc11) | ~forename(V_1640, skc11) | ~agent(V_1640, X2_1637, skc10) | ~be(V_1640, X3_1638, skc10, skc10) | ~man(V_1640, skc10) | ~forename(V_1640, X4_1639) | ~vincent_forename(V_1640, X4_1639) | ~of(V_1640, X4_1639, skc10) | ~state(V_1640, X3_1638) | ~think_believe_consider(V_1640, X2_1637) | ~present(V_1640, X2_1637) | ~event(V_1640, X2_1637) | ~theme(V_1640, X2_1637, V_811) | ~proposition(V_1640, V_811) | ~accessible_world(V_1640, V_811) | ~of(V_1640, Y_1643, Z_1641) | ~man(V_1640, Z_1641) | ~agent(V_1640, X_1645, Z_1641) | ~forename(V_1640, Y_1643) | ~vincent_forename(V_1640, Y_1643) | ~theme(V_1640, X_1645, V_1636) | ~event(V_1640, X_1645) | ~present(V_1640, X_1645) | ~think_believe_consider(V_1640, X_1645) | ~event(V_1636, W_1642) | ~agent(V_1636, W_1642, skf4(V_1636)) | ~present(V_1636, W_1642) | ~smoke(V_1636, W_1642) | ~accessible_world(V_1640, V_1636) | ~proposition(V_1640, V_1636) | ~accessible_world(skc8, V_1640) | ~accessible_world(skc12, V_811)))). % 11.63/3.78 tff(c_4780, plain, (![X_1604, V_1597, X2_1599, W_1603, X4_1605, V_811, Y_1598, X3_1600, Z_1596, V_1601]: (~actual_world(V_1597) | ~jules_forename(V_1597, skc14) | ~forename(V_1597, skc14) | ~agent(V_1597, X2_1599, skc15) | ~be(V_1597, X3_1600, skc15, skc15) | ~man(V_1597, skc15) | ~forename(V_1597, X4_1605) | ~vincent_forename(V_1597, X4_1605) | ~of(V_1597, X4_1605, skc15) | ~state(V_1597, X3_1600) | ~think_believe_consider(V_1597, X2_1599) | ~present(V_1597, X2_1599) | ~event(V_1597, X2_1599) | ~theme(V_1597, X2_1599, V_811) | ~proposition(V_1597, V_811) | ~accessible_world(V_1597, V_811) | ~of(V_1597, Y_1598, Z_1596) | ~man(V_1597, Z_1596) | ~agent(V_1597, X_1604, Z_1596) | ~forename(V_1597, Y_1598) | ~vincent_forename(V_1597, Y_1598) | ~theme(V_1597, X_1604, V_1601) | ~event(V_1597, X_1604) | ~present(V_1597, X_1604) | ~think_believe_consider(V_1597, X_1604) | ~event(V_1601, W_1603) | ~agent(V_1601, W_1603, skf4(V_1601)) | ~present(V_1601, W_1603) | ~smoke(V_1601, W_1603) | ~accessible_world(V_1597, V_1601) | ~proposition(V_1597, V_1601) | ~accessible_world(skc8, V_1597) | ~accessible_world(skc12, V_811)))). % 11.63/3.78 tff(c_4738, plain, (![Y_1568, W_1561, V_901, V_1564, X_1562, X1_1565, V_1566]: (man(V_1566, skf4(V_1566)) | ~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~agent(V_901, X1_1565, skc10) | ~man(V_901, skc10) | ~forename(V_901, skc11) | ~vincent_forename(V_901, skc11) | ~state(V_901, skc9) | ~think_believe_consider(V_901, X1_1565) | ~present(V_901, X1_1565) | ~event(V_901, X1_1565) | ~theme(V_901, X1_1565, V_1564) | ~proposition(V_901, V_1564) | ~accessible_world(V_901, V_1564) | ~of(V_901, X_1562, Y_1568) | ~man(V_901, Y_1568) | ~agent(V_901, W_1561, Y_1568) | ~forename(V_901, X_1562) | ~vincent_forename(V_901, X_1562) | ~theme(V_901, W_1561, V_1566) | ~event(V_901, W_1561) | ~present(V_901, W_1561) | ~think_believe_consider(V_901, W_1561) | ~accessible_world(V_901, V_1566) | ~proposition(V_901, V_1566) | ~accessible_world(skc12, V_1564) | ~accessible_world(skc8, V_901)))). % 11.76/3.78 tff(c_4729, plain, (![W_1558, V_1559, X3_1552, X_1557, Y_1553, V_928, V_1560, X1_1554]: (man(V_1559, skf4(V_1559)) | ~actual_world(V_928) | ~jules_forename(V_928, skc11) | ~forename(V_928, skc11) | ~agent(V_928, X1_1554, skc10) | ~man(V_928, skc10) | ~forename(V_928, X3_1552) | ~vincent_forename(V_928, X3_1552) | ~of(V_928, X3_1552, skc10) | ~state(V_928, skc9) | ~think_believe_consider(V_928, X1_1554) | ~present(V_928, X1_1554) | ~event(V_928, X1_1554) | ~theme(V_928, X1_1554, V_1560) | ~proposition(V_928, V_1560) | ~accessible_world(V_928, V_1560) | ~of(V_928, X_1557, Y_1553) | ~man(V_928, Y_1553) | ~agent(V_928, W_1558, Y_1553) | ~forename(V_928, X_1557) | ~vincent_forename(V_928, X_1557) | ~theme(V_928, W_1558, V_1559) | ~event(V_928, W_1558) | ~present(V_928, W_1558) | ~think_believe_consider(V_928, W_1558) | ~accessible_world(V_928, V_1559) | ~proposition(V_928, V_1559) | ~accessible_world(skc12, V_1560) | ~accessible_world(skc8, V_928)))). % 11.76/3.78 tff(c_4722, plain, (![V_1547, V_1544, X2_1545, Y_1550, X3_1546, W_1549, V_811, X_1551, X1_1543]: (man(V_1544, skf4(V_1544)) | ~actual_world(V_1547) | ~jules_forename(V_1547, skc11) | ~forename(V_1547, skc11) | ~agent(V_1547, X1_1543, skc10) | ~be(V_1547, X2_1545, skc10, skc10) | ~man(V_1547, skc10) | ~forename(V_1547, X3_1546) | ~vincent_forename(V_1547, X3_1546) | ~of(V_1547, X3_1546, skc10) | ~state(V_1547, X2_1545) | ~think_believe_consider(V_1547, X1_1543) | ~present(V_1547, X1_1543) | ~event(V_1547, X1_1543) | ~theme(V_1547, X1_1543, V_811) | ~proposition(V_1547, V_811) | ~accessible_world(V_1547, V_811) | ~of(V_1547, X_1551, Y_1550) | ~man(V_1547, Y_1550) | ~agent(V_1547, W_1549, Y_1550) | ~forename(V_1547, X_1551) | ~vincent_forename(V_1547, X_1551) | ~theme(V_1547, W_1549, V_1544) | ~event(V_1547, W_1549) | ~present(V_1547, W_1549) | ~think_believe_consider(V_1547, W_1549) | ~accessible_world(V_1547, V_1544) | ~proposition(V_1547, V_1544) | ~accessible_world(skc8, V_1547) | ~accessible_world(skc12, V_811)))). % 11.76/3.79 tff(c_4421, plain, (![X3_1389, X4_1379, Z_1388, W_1387, V_1384, X2_1385, Y_1380, V_1383, V_919, X_1382]: (~actual_world(V_1384) | ~jules_forename(V_1384, skc14) | ~forename(V_1384, skc14) | ~event(V_919, skc13) | ~present(V_919, skc13) | ~smoke(V_919, skc13) | ~agent(V_1384, X2_1385, skc15) | ~be(V_1384, X3_1389, skc15, skc15) | ~man(V_1384, skc15) | ~forename(V_1384, X4_1379) | ~vincent_forename(V_1384, X4_1379) | ~of(V_1384, X4_1379, skc15) | ~state(V_1384, X3_1389) | ~think_believe_consider(V_1384, X2_1385) | ~present(V_1384, X2_1385) | ~event(V_1384, X2_1385) | ~theme(V_1384, X2_1385, V_919) | ~proposition(V_1384, V_919) | ~accessible_world(V_1384, V_919) | ~of(V_1384, Y_1380, Z_1388) | ~man(V_1384, Z_1388) | ~agent(V_1384, X_1382, Z_1388) | ~forename(V_1384, Y_1380) | ~vincent_forename(V_1384, Y_1380) | ~theme(V_1384, X_1382, V_1383) | ~event(V_1384, X_1382) | ~present(V_1384, X_1382) | ~think_believe_consider(V_1384, X_1382) | ~event(V_1383, W_1387) | ~agent(V_1383, W_1387, skf4(V_1383)) | ~present(V_1383, W_1387) | ~smoke(V_1383, W_1387) | ~accessible_world(V_1384, V_1383) | ~proposition(V_1384, V_1383) | ~accessible_world(skc8, V_1384) | ~accessible_world(skc8, V_919)))). % 11.76/3.79 tff(c_4687, plain, (![X1_1505, Y_1497, X2_1501, W_1503, V_1502, V_811, V_1499, X_1504, X3_1498]: (man(V_1499, skf4(V_1499)) | ~actual_world(V_1502) | ~jules_forename(V_1502, skc14) | ~forename(V_1502, skc14) | ~agent(V_1502, X1_1505, skc15) | ~be(V_1502, X2_1501, skc15, skc15) | ~man(V_1502, skc15) | ~forename(V_1502, X3_1498) | ~vincent_forename(V_1502, X3_1498) | ~of(V_1502, X3_1498, skc15) | ~state(V_1502, X2_1501) | ~think_believe_consider(V_1502, X1_1505) | ~present(V_1502, X1_1505) | ~event(V_1502, X1_1505) | ~theme(V_1502, X1_1505, V_811) | ~proposition(V_1502, V_811) | ~accessible_world(V_1502, V_811) | ~of(V_1502, X_1504, Y_1497) | ~man(V_1502, Y_1497) | ~agent(V_1502, W_1503, Y_1497) | ~forename(V_1502, X_1504) | ~vincent_forename(V_1502, X_1504) | ~theme(V_1502, W_1503, V_1499) | ~event(V_1502, W_1503) | ~present(V_1502, W_1503) | ~think_believe_consider(V_1502, W_1503) | ~accessible_world(V_1502, V_1499) | ~proposition(V_1502, V_1499) | ~accessible_world(skc8, V_1502) | ~accessible_world(skc12, V_811)))). % 11.76/3.79 tff(c_4645, plain, (![Y_1466, X2_1467, V_901, W_1465, V_1468, X_1469, Z_1464]: (~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~agent(V_901, X2_1467, skc10) | ~man(V_901, skc10) | ~forename(V_901, skc11) | ~vincent_forename(V_901, skc11) | ~state(V_901, skc9) | ~think_believe_consider(V_901, X2_1467) | ~present(V_901, X2_1467) | ~event(V_901, X2_1467) | ~theme(V_901, X2_1467, skc12) | ~proposition(V_901, skc12) | ~accessible_world(V_901, skc12) | ~of(V_901, Y_1466, Z_1464) | ~man(V_901, Z_1464) | ~agent(V_901, X_1469, Z_1464) | ~forename(V_901, Y_1466) | ~vincent_forename(V_901, Y_1466) | ~theme(V_901, X_1469, V_1468) | ~event(V_901, X_1469) | ~present(V_901, X_1469) | ~think_believe_consider(V_901, X_1469) | ~event(V_1468, W_1465) | ~agent(V_1468, W_1465, skf4(V_1468)) | ~present(V_1468, W_1465) | ~smoke(V_1468, W_1465) | ~accessible_world(V_901, V_1468) | ~proposition(V_901, V_1468) | ~accessible_world(skc8, V_901)))). % 11.76/3.79 tff(c_4636, plain, (![X2_1457, V_1459, Y_1455, W_1460, V_928, X4_1461, Z_1463, X_1458]: (~actual_world(V_928) | ~jules_forename(V_928, skc11) | ~forename(V_928, skc11) | ~agent(V_928, X2_1457, skc10) | ~man(V_928, skc10) | ~forename(V_928, X4_1461) | ~vincent_forename(V_928, X4_1461) | ~of(V_928, X4_1461, skc10) | ~state(V_928, skc9) | ~think_believe_consider(V_928, X2_1457) | ~present(V_928, X2_1457) | ~event(V_928, X2_1457) | ~theme(V_928, X2_1457, skc12) | ~proposition(V_928, skc12) | ~accessible_world(V_928, skc12) | ~of(V_928, Y_1455, Z_1463) | ~man(V_928, Z_1463) | ~agent(V_928, X_1458, Z_1463) | ~forename(V_928, Y_1455) | ~vincent_forename(V_928, Y_1455) | ~theme(V_928, X_1458, V_1459) | ~event(V_928, X_1458) | ~present(V_928, X_1458) | ~think_believe_consider(V_928, X_1458) | ~event(V_1459, W_1460) | ~agent(V_1459, W_1460, skf4(V_1459)) | ~present(V_1459, W_1460) | ~smoke(V_1459, W_1460) | ~accessible_world(V_928, V_1459) | ~proposition(V_928, V_1459) | ~accessible_world(skc8, V_928)))). % 11.76/3.79 tff(c_4630, plain, (![X3_1378, X_1371, Z_1377, X4_1368, Y_1369, X2_1374, V_1373, W_1376, V_1372]: (~actual_world(V_1373) | ~jules_forename(V_1373, skc11) | ~forename(V_1373, skc11) | ~agent(V_1373, X2_1374, skc10) | ~be(V_1373, X3_1378, skc10, skc10) | ~man(V_1373, skc10) | ~forename(V_1373, X4_1368) | ~vincent_forename(V_1373, X4_1368) | ~of(V_1373, X4_1368, skc10) | ~state(V_1373, X3_1378) | ~think_believe_consider(V_1373, X2_1374) | ~present(V_1373, X2_1374) | ~event(V_1373, X2_1374) | ~theme(V_1373, X2_1374, skc12) | ~proposition(V_1373, skc12) | ~accessible_world(V_1373, skc12) | ~of(V_1373, Y_1369, Z_1377) | ~man(V_1373, Z_1377) | ~agent(V_1373, X_1371, Z_1377) | ~forename(V_1373, Y_1369) | ~vincent_forename(V_1373, Y_1369) | ~theme(V_1373, X_1371, V_1372) | ~event(V_1373, X_1371) | ~present(V_1373, X_1371) | ~think_believe_consider(V_1373, X_1371) | ~event(V_1372, W_1376) | ~agent(V_1372, W_1376, skf4(V_1372)) | ~present(V_1372, W_1376) | ~smoke(V_1372, W_1376) | ~accessible_world(V_1373, V_1372) | ~proposition(V_1373, V_1372) | ~accessible_world(skc8, V_1373)))). % 11.76/3.79 tff(c_4283, plain, (![V_1337, Y_1338, X2_1335, W_1333, X_1339, V_1332, V_919, X3_1331, X1_1340]: (man(V_1332, skf4(V_1332)) | ~actual_world(V_1337) | ~jules_forename(V_1337, skc14) | ~forename(V_1337, skc14) | ~event(V_919, skc13) | ~present(V_919, skc13) | ~smoke(V_919, skc13) | ~agent(V_1337, X1_1340, skc15) | ~be(V_1337, X2_1335, skc15, skc15) | ~man(V_1337, skc15) | ~forename(V_1337, X3_1331) | ~vincent_forename(V_1337, X3_1331) | ~of(V_1337, X3_1331, skc15) | ~state(V_1337, X2_1335) | ~think_believe_consider(V_1337, X1_1340) | ~present(V_1337, X1_1340) | ~event(V_1337, X1_1340) | ~theme(V_1337, X1_1340, V_919) | ~proposition(V_1337, V_919) | ~accessible_world(V_1337, V_919) | ~of(V_1337, X_1339, Y_1338) | ~man(V_1337, Y_1338) | ~agent(V_1337, W_1333, Y_1338) | ~forename(V_1337, X_1339) | ~vincent_forename(V_1337, X_1339) | ~theme(V_1337, W_1333, V_1332) | ~event(V_1337, W_1333) | ~present(V_1337, W_1333) | ~think_believe_consider(V_1337, W_1333) | ~accessible_world(V_1337, V_1332) | ~proposition(V_1337, V_1332) | ~accessible_world(skc8, V_1337) | ~accessible_world(skc8, V_919)))). % 11.76/3.79 tff(c_4424, plain, (![X3_1389, X4_1379, Z_1388, W_1387, V_1384, X2_1385, Y_1380, V_1383, X_1382]: (~actual_world(V_1384) | ~jules_forename(V_1384, skc14) | ~forename(V_1384, skc14) | ~agent(V_1384, X2_1385, skc15) | ~be(V_1384, X3_1389, skc15, skc15) | ~man(V_1384, skc15) | ~forename(V_1384, X4_1379) | ~vincent_forename(V_1384, X4_1379) | ~of(V_1384, X4_1379, skc15) | ~state(V_1384, X3_1389) | ~think_believe_consider(V_1384, X2_1385) | ~present(V_1384, X2_1385) | ~event(V_1384, X2_1385) | ~theme(V_1384, X2_1385, skc12) | ~proposition(V_1384, skc12) | ~accessible_world(V_1384, skc12) | ~of(V_1384, Y_1380, Z_1388) | ~man(V_1384, Z_1388) | ~agent(V_1384, X_1382, Z_1388) | ~forename(V_1384, Y_1380) | ~vincent_forename(V_1384, Y_1380) | ~theme(V_1384, X_1382, V_1383) | ~event(V_1384, X_1382) | ~present(V_1384, X_1382) | ~think_believe_consider(V_1384, X_1382) | ~event(V_1383, W_1387) | ~agent(V_1383, W_1387, skf4(V_1383)) | ~present(V_1383, W_1387) | ~smoke(V_1383, W_1387) | ~accessible_world(V_1384, V_1383) | ~proposition(V_1384, V_1383) | ~accessible_world(skc8, V_1384)))). % 11.76/3.79 tff(c_4625, plain, (![V_908]: (~actual_world(V_908) | ~jules_forename(V_908, skc11) | ~state(V_908, skc9) | ~man(V_908, skc10) | ~agent(V_908, skc13, skc10) | ~forename(V_908, skc11) | ~vincent_forename(V_908, skc11) | ~event(V_908, skc13) | ~present(V_908, skc13) | ~think_believe_consider(V_908, skc13) | ~accessible_world(V_908, skc12) | ~proposition(V_908, skc12) | ~accessible_world(skc8, V_908)))). % 11.76/3.79 tff(c_4586, plain, (![W_1421, Y_1417, V_901, X1_1418, V_1415, X_1419]: (man(V_1415, skf4(V_1415)) | ~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~agent(V_901, X1_1418, skc10) | ~man(V_901, skc10) | ~forename(V_901, skc11) | ~vincent_forename(V_901, skc11) | ~state(V_901, skc9) | ~think_believe_consider(V_901, X1_1418) | ~present(V_901, X1_1418) | ~event(V_901, X1_1418) | ~theme(V_901, X1_1418, skc12) | ~proposition(V_901, skc12) | ~accessible_world(V_901, skc12) | ~of(V_901, X_1419, Y_1417) | ~man(V_901, Y_1417) | ~agent(V_901, W_1421, Y_1417) | ~forename(V_901, X_1419) | ~vincent_forename(V_901, X_1419) | ~theme(V_901, W_1421, V_1415) | ~event(V_901, W_1421) | ~present(V_901, W_1421) | ~think_believe_consider(V_901, W_1421) | ~accessible_world(V_901, V_1415) | ~proposition(V_901, V_1415) | ~accessible_world(skc8, V_901)))). % 11.76/3.79 tff(c_4533, plain, (![X3_1400, V_928, V_1395, W_1398, Y_1402, X1_1401, X_1397]: (man(V_1395, skf4(V_1395)) | ~actual_world(V_928) | ~jules_forename(V_928, skc11) | ~forename(V_928, skc11) | ~agent(V_928, X1_1401, skc10) | ~man(V_928, skc10) | ~forename(V_928, X3_1400) | ~vincent_forename(V_928, X3_1400) | ~of(V_928, X3_1400, skc10) | ~state(V_928, skc9) | ~think_believe_consider(V_928, X1_1401) | ~present(V_928, X1_1401) | ~event(V_928, X1_1401) | ~theme(V_928, X1_1401, skc12) | ~proposition(V_928, skc12) | ~accessible_world(V_928, skc12) | ~of(V_928, X_1397, Y_1402) | ~man(V_928, Y_1402) | ~agent(V_928, W_1398, Y_1402) | ~forename(V_928, X_1397) | ~vincent_forename(V_928, X_1397) | ~theme(V_928, W_1398, V_1395) | ~event(V_928, W_1398) | ~present(V_928, W_1398) | ~think_believe_consider(V_928, W_1398) | ~accessible_world(V_928, V_1395) | ~proposition(V_928, V_1395) | ~accessible_world(skc8, V_928)))). % 11.76/3.79 tff(c_4580, plain, (~smoke(skc8, skc13))). % 11.76/3.79 tff(c_4552, plain, (![V_143, V_1403]: (human(V_143, skc10) | ~accessible_world(V_1403, V_143) | ~accessible_world(skc12, V_1403)))). % 11.76/3.79 tff(c_4527, plain, (![V_146, V_1394]: (animate(V_146, skc10) | ~accessible_world(V_1394, V_146) | ~accessible_world(skc12, V_1394)))). % 11.76/3.79 tff(c_4479, plain, (![V_149, V_1391]: (male(V_149, skc10) | ~accessible_world(V_1391, V_149) | ~accessible_world(skc12, V_1391)))). % 11.76/3.79 tff(c_4504, plain, (![V_125, V_1392]: (human_person(V_125, skc10) | ~accessible_world(V_1392, V_125) | ~accessible_world(skc12, V_1392)))). % 11.76/3.79 tff(c_4449, plain, (![V_122, V_1390]: (man(V_122, skc10) | ~accessible_world(V_1390, V_122) | ~accessible_world(skc12, V_1390)))). % 11.76/3.79 tff(c_4523, plain, (![U_3]: (~accessible_world(skc12, U_3) | ~event(U_3, skc10)))). % 11.76/3.79 tff(c_4405, plain, (![V_143]: (human(V_143, skc10) | ~accessible_world(skc12, V_143)))). % 11.76/3.79 tff(c_4322, plain, (![X3_1350, X_1358, V_1351, V_1356, X1_1359, W_1352, Y_1357, X2_1354]: (man(V_1351, skf4(V_1351)) | ~actual_world(V_1356) | ~jules_forename(V_1356, skc11) | ~forename(V_1356, skc11) | ~agent(V_1356, X1_1359, skc10) | ~be(V_1356, X2_1354, skc10, skc10) | ~man(V_1356, skc10) | ~forename(V_1356, X3_1350) | ~vincent_forename(V_1356, X3_1350) | ~of(V_1356, X3_1350, skc10) | ~state(V_1356, X2_1354) | ~think_believe_consider(V_1356, X1_1359) | ~present(V_1356, X1_1359) | ~event(V_1356, X1_1359) | ~theme(V_1356, X1_1359, skc12) | ~proposition(V_1356, skc12) | ~accessible_world(V_1356, skc12) | ~of(V_1356, X_1358, Y_1357) | ~man(V_1356, Y_1357) | ~agent(V_1356, W_1352, Y_1357) | ~forename(V_1356, X_1358) | ~vincent_forename(V_1356, X_1358) | ~theme(V_1356, W_1352, V_1351) | ~event(V_1356, W_1352) | ~present(V_1356, W_1352) | ~think_believe_consider(V_1356, W_1352) | ~accessible_world(V_1356, V_1351) | ~proposition(V_1356, V_1351) | ~accessible_world(skc8, V_1356)))). % 11.76/3.79 tff(c_4506, plain, (![V_1392]: (animate(V_1392, skc10) | ~accessible_world(skc12, V_1392)))). % 11.76/3.79 tff(c_4481, plain, (![V_1391]: (~eventuality(V_1391, skc10) | ~accessible_world(skc12, V_1391)))). % 11.76/3.79 tff(c_4450, plain, (![V_1390]: (human_person(V_1390, skc10) | ~accessible_world(skc12, V_1390)))). % 11.76/3.79 tff(c_4386, plain, (![V_149]: (male(V_149, skc10) | ~accessible_world(skc12, V_149)))). % 11.76/3.79 tff(c_4343, plain, (![V_122]: (man(V_122, skc10) | ~accessible_world(skc12, V_122)))). % 11.76/3.79 tff(c_4439, plain, (~event(skc12, skc10))). % 11.76/3.79 tff(c_4388, plain, (~eventuality(skc12, skc10))). % 11.76/3.80 tff(c_2656, plain, (![W_980, X2_985, V_983, V_901, X4_974, Z_979, X1_981, Y_978, X_976, X6_975, X3_977]: (~actual_world(V_901) | ~jules_forename(V_901, skc14) | ~forename(V_901, skc14) | ~event(X1_981, X6_975) | ~agent(X1_981, X6_975, skc15) | ~present(X1_981, X6_975) | ~smoke(X1_981, X6_975) | ~agent(V_901, X2_985, skc15) | ~be(V_901, X3_977, skc15, skc15) | ~man(V_901, skc15) | ~forename(V_901, X4_974) | ~vincent_forename(V_901, X4_974) | ~of(V_901, X4_974, skc15) | ~state(V_901, X3_977) | ~think_believe_consider(V_901, X2_985) | ~present(V_901, X2_985) | ~event(V_901, X2_985) | ~theme(V_901, X2_985, X1_981) | ~proposition(V_901, X1_981) | ~accessible_world(V_901, X1_981) | ~of(V_901, Y_978, Z_979) | ~man(V_901, Z_979) | ~agent(V_901, X_976, Z_979) | ~forename(V_901, Y_978) | ~vincent_forename(V_901, Y_978) | ~theme(V_901, X_976, V_983) | ~event(V_901, X_976) | ~present(V_901, X_976) | ~think_believe_consider(V_901, X_976) | ~event(V_983, W_980) | ~agent(V_983, W_980, skf4(V_983)) | ~present(V_983, W_980) | ~smoke(V_983, W_980) | ~accessible_world(V_901, V_983) | ~proposition(V_901, V_983) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_4361, plain, (human(skc12, skc10))). % 11.76/3.80 tff(c_4360, plain, (animate(skc12, skc10))). % 11.76/3.80 tff(c_4345, plain, (male(skc12, skc10))). % 11.76/3.80 tff(c_4344, plain, (human_person(skc12, skc10))). % 11.76/3.80 tff(c_4323, plain, (man(skc12, skc10))). % 11.76/3.80 tff(c_2657, plain, (![W_980, X2_985, V_983, V_901, X4_974, Z_979, X1_981, Y_978, X_976, X6_975, X3_977]: (~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~forename(V_901, skc11) | ~event(X1_981, X6_975) | ~agent(X1_981, X6_975, skc10) | ~present(X1_981, X6_975) | ~smoke(X1_981, X6_975) | ~agent(V_901, X2_985, skc10) | ~be(V_901, X3_977, skc10, skc10) | ~man(V_901, skc10) | ~forename(V_901, X4_974) | ~vincent_forename(V_901, X4_974) | ~of(V_901, X4_974, skc10) | ~state(V_901, X3_977) | ~think_believe_consider(V_901, X2_985) | ~present(V_901, X2_985) | ~event(V_901, X2_985) | ~theme(V_901, X2_985, X1_981) | ~proposition(V_901, X1_981) | ~accessible_world(V_901, X1_981) | ~of(V_901, Y_978, Z_979) | ~man(V_901, Z_979) | ~agent(V_901, X_976, Z_979) | ~forename(V_901, Y_978) | ~vincent_forename(V_901, Y_978) | ~theme(V_901, X_976, V_983) | ~event(V_901, X_976) | ~present(V_901, X_976) | ~think_believe_consider(V_901, X_976) | ~event(V_983, W_980) | ~agent(V_983, W_980, skf4(V_983)) | ~present(V_983, W_980) | ~smoke(V_983, W_980) | ~accessible_world(V_901, V_983) | ~proposition(V_901, V_983) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_4286, plain, (![V_1337, Y_1338, X2_1335, W_1333, X_1339, V_1332, X3_1331, X1_1340]: (man(V_1332, skf4(V_1332)) | ~actual_world(V_1337) | ~jules_forename(V_1337, skc14) | ~forename(V_1337, skc14) | ~agent(V_1337, X1_1340, skc15) | ~be(V_1337, X2_1335, skc15, skc15) | ~man(V_1337, skc15) | ~forename(V_1337, X3_1331) | ~vincent_forename(V_1337, X3_1331) | ~of(V_1337, X3_1331, skc15) | ~state(V_1337, X2_1335) | ~think_believe_consider(V_1337, X1_1340) | ~present(V_1337, X1_1340) | ~event(V_1337, X1_1340) | ~theme(V_1337, X1_1340, skc12) | ~proposition(V_1337, skc12) | ~accessible_world(V_1337, skc12) | ~of(V_1337, X_1339, Y_1338) | ~man(V_1337, Y_1338) | ~agent(V_1337, W_1333, Y_1338) | ~forename(V_1337, X_1339) | ~vincent_forename(V_1337, X_1339) | ~theme(V_1337, W_1333, V_1332) | ~event(V_1337, W_1333) | ~present(V_1337, W_1333) | ~think_believe_consider(V_1337, W_1333) | ~accessible_world(V_1337, V_1332) | ~proposition(V_1337, V_1332) | ~accessible_world(skc8, V_1337)))). % 11.76/3.80 tff(c_2611, plain, (![X1_960, X3_959, X2_961, X_962, Y_966, V_901, V_965, X5_957, Z_956, W_963]: (man(V_965, skf4(V_965)) | ~actual_world(V_901) | ~jules_forename(V_901, skc11) | ~forename(V_901, skc11) | ~event(Z_956, X5_957) | ~agent(Z_956, X5_957, skc10) | ~present(Z_956, X5_957) | ~smoke(Z_956, X5_957) | ~agent(V_901, X1_960, skc10) | ~be(V_901, X2_961, skc10, skc10) | ~man(V_901, skc10) | ~forename(V_901, X3_959) | ~vincent_forename(V_901, X3_959) | ~of(V_901, X3_959, skc10) | ~state(V_901, X2_961) | ~think_believe_consider(V_901, X1_960) | ~present(V_901, X1_960) | ~event(V_901, X1_960) | ~theme(V_901, X1_960, Z_956) | ~proposition(V_901, Z_956) | ~accessible_world(V_901, Z_956) | ~of(V_901, X_962, Y_966) | ~man(V_901, Y_966) | ~agent(V_901, W_963, Y_966) | ~forename(V_901, X_962) | ~vincent_forename(V_901, X_962) | ~theme(V_901, W_963, V_965) | ~event(V_901, W_963) | ~present(V_901, W_963) | ~think_believe_consider(V_901, W_963) | ~accessible_world(V_901, V_965) | ~proposition(V_901, V_965) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_4297, plain, (![V_1346, V_908]: (skc12=V_1346 | ~think_believe_consider(V_908, skc13) | ~think_believe_consider(V_908, skf2(skc15)) | ~theme(V_908, skf2(skc15), V_1346) | ~proposition(V_908, skc12) | ~proposition(V_908, V_1346) | ~accessible_world(skc12, V_908) | ~accessible_world(skc8, V_908)))). % 11.76/3.80 tff(c_4264, plain, (![W_1330, V_1328, V_919]: (W_1330=V_1328 | ~theme(V_919, skc13, W_1330) | ~think_believe_consider(V_919, skc13) | ~think_believe_consider(V_919, skf2(skc15)) | ~theme(V_919, skf2(skc15), V_1328) | ~proposition(V_919, W_1330) | ~proposition(V_919, V_1328) | ~accessible_world(skc12, V_919) | ~accessible_world(skc8, V_919)))). % 11.76/3.80 tff(c_4261, plain, (![W_1330, V_1328, V_919, U_196]: (W_1330=V_1328 | ~theme(V_919, skf2(U_196), W_1330) | ~think_believe_consider(V_919, skf2(U_196)) | ~theme(V_919, skf2(U_196), V_1328) | ~proposition(V_919, W_1330) | ~proposition(V_919, V_1328) | ~accessible_world(skc12, V_919) | ~man(skc12, U_196)))). % 11.76/3.80 tff(c_4290, plain, (~accessible_world(skc12, skc8))). % 11.76/3.80 tff(c_2610, plain, (![X1_960, X3_959, X2_961, X_962, Y_966, V_901, V_965, X5_957, Z_956, W_963]: (man(V_965, skf4(V_965)) | ~actual_world(V_901) | ~jules_forename(V_901, skc14) | ~forename(V_901, skc14) | ~event(Z_956, X5_957) | ~agent(Z_956, X5_957, skc15) | ~present(Z_956, X5_957) | ~smoke(Z_956, X5_957) | ~agent(V_901, X1_960, skc15) | ~be(V_901, X2_961, skc15, skc15) | ~man(V_901, skc15) | ~forename(V_901, X3_959) | ~vincent_forename(V_901, X3_959) | ~of(V_901, X3_959, skc15) | ~state(V_901, X2_961) | ~think_believe_consider(V_901, X1_960) | ~present(V_901, X1_960) | ~event(V_901, X1_960) | ~theme(V_901, X1_960, Z_956) | ~proposition(V_901, Z_956) | ~accessible_world(V_901, Z_956) | ~of(V_901, X_962, Y_966) | ~man(V_901, Y_966) | ~agent(V_901, W_963, Y_966) | ~forename(V_901, X_962) | ~vincent_forename(V_901, X_962) | ~theme(V_901, W_963, V_965) | ~event(V_901, W_963) | ~present(V_901, W_963) | ~think_believe_consider(V_901, W_963) | ~accessible_world(V_901, V_965) | ~proposition(V_901, V_965) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_3134, plain, (![V_189, Y_188, U_1057, V_1056, W_184]: (W_184=V_189 | ~agent(V_1056, Y_188, U_1057) | ~theme(V_1056, Y_188, W_184) | ~think_believe_consider(V_1056, Y_188) | ~think_believe_consider(V_1056, skf2(U_1057)) | ~theme(V_1056, skf2(U_1057), V_189) | ~proposition(V_1056, W_184) | ~proposition(V_1056, V_189) | ~accessible_world(skc12, V_1056) | ~man(skc12, U_1057)))). % 11.76/3.80 tff(c_4236, plain, (![V_1321, V_908]: (skc12=V_1321 | ~agent(V_908, skc13, skc15) | ~think_believe_consider(V_908, skc13) | ~theme(V_908, skc13, V_1321) | ~proposition(V_908, skc12) | ~proposition(V_908, V_1321) | ~accessible_world(skc8, V_908)))). % 11.76/3.80 tff(c_2530, plain, (![W_945, V_943, V_919, Y_944]: (W_945=V_943 | ~agent(V_919, Y_944, skc15) | ~theme(V_919, Y_944, W_945) | ~think_believe_consider(V_919, Y_944) | ~think_believe_consider(V_919, skc13) | ~theme(V_919, skc13, V_943) | ~proposition(V_919, W_945) | ~proposition(V_919, V_943) | ~accessible_world(skc8, V_919)))). % 11.76/3.80 tff(c_4182, plain, (![V_146, V_1305]: (animate(V_146, skc15) | ~accessible_world(V_1305, V_146) | ~accessible_world(skc12, V_1305)))). % 11.76/3.80 tff(c_4177, plain, (![V_143, V_1304]: (human(V_143, skc15) | ~accessible_world(V_1304, V_143) | ~accessible_world(skc12, V_1304)))). % 11.76/3.80 tff(c_4116, plain, (![V_149, V_1301]: (male(V_149, skc15) | ~accessible_world(V_1301, V_149) | ~accessible_world(skc12, V_1301)))). % 11.76/3.80 tff(c_4141, plain, (![V_125, V_1302]: (human_person(V_125, skc15) | ~accessible_world(V_1302, V_125) | ~accessible_world(skc12, V_1302)))). % 11.76/3.80 tff(c_4161, plain, (![V_101, V_1303]: (think_believe_consider(V_101, skc13) | ~accessible_world(V_1303, V_101) | ~accessible_world(skc12, V_1303)))). % 11.76/3.80 tff(c_4086, plain, (![V_122, V_1300]: (man(V_122, skc15) | ~accessible_world(V_1300, V_122) | ~accessible_world(skc12, V_1300)))). % 11.76/3.80 tff(c_4199, plain, (![U_3]: (~accessible_world(skc12, U_3) | ~event(U_3, skc15)))). % 11.76/3.80 tff(c_4118, plain, (![V_1301]: (~eventuality(V_1301, skc15) | ~accessible_world(skc12, V_1301)))). % 11.76/3.80 tff(c_4183, plain, (~think_believe_consider(skc12, skf2(skc15)))). % 11.76/3.80 tff(c_4143, plain, (![V_1302]: (animate(V_1302, skc15) | ~accessible_world(skc12, V_1302)))). % 11.76/3.80 tff(c_4144, plain, (![V_1302]: (human(V_1302, skc15) | ~accessible_world(skc12, V_1302)))). % 11.76/3.80 tff(c_4157, plain, (![V_101]: (think_believe_consider(V_101, skc13) | ~accessible_world(skc12, V_101)))). % 11.76/3.80 tff(c_4154, plain, (think_believe_consider(skc12, skc13))). % 11.76/3.80 tff(c_4015, plain, (![V_125]: (human_person(V_125, skc15) | ~accessible_world(skc12, V_125)))). % 11.76/3.80 tff(c_4044, plain, (![V_149]: (male(V_149, skc15) | ~accessible_world(skc12, V_149)))). % 11.76/3.80 tff(c_4001, plain, (![V_122]: (man(V_122, skc15) | ~accessible_world(skc12, V_122)))). % 11.76/3.80 tff(c_4076, plain, (~event(skc12, skc15))). % 11.76/3.80 tff(c_4046, plain, (~eventuality(skc12, skc15))). % 11.76/3.80 tff(c_4019, plain, (human(skc12, skc15))). % 11.76/3.80 tff(c_4018, plain, (animate(skc12, skc15))). % 11.76/3.80 tff(c_4003, plain, (male(skc12, skc15))). % 11.76/3.80 tff(c_4002, plain, (human_person(skc12, skc15))). % 11.76/3.80 tff(c_3992, plain, (man(skc12, skc15))). % 11.76/3.80 tff(c_3281, plain, (![W_1100, V_1101, U_196]: (W_1100=V_1101 | ~theme(skc12, skf2(U_196), W_1100) | ~think_believe_consider(skc12, skf2(U_196)) | ~theme(skc12, skf2(U_196), V_1101) | ~proposition(skc12, W_1100) | ~proposition(skc12, V_1101) | ~man(skc12, U_196)))). % 11.76/3.80 tff(c_2499, plain, (![W_932, V_901]: (skc14=W_932 | ~entity(V_901, skc15) | ~forename(V_901, W_932) | ~of(V_901, W_932, skc15) | ~forename(V_901, skc14) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_3475, plain, (![V_140, V_1142, V_1141]: (living(V_140, V_1142) | ~accessible_world(V_1141, V_140) | ~accessible_world(skc12, V_1141) | ~human_person(skc8, V_1142)))). % 11.76/3.80 tff(c_3518, plain, (![V_86, V_1152, V_1151]: (singleton(V_86, V_1152) | ~accessible_world(V_1151, V_86) | ~accessible_world(skc12, V_1151) | ~entity(skc8, V_1152)))). % 11.76/3.80 tff(c_3563, plain, (![V_86, V_1162, V_1161]: (singleton(V_86, V_1162) | ~accessible_world(V_1161, V_86) | ~accessible_world(skc12, V_1161) | ~eventuality(skc8, V_1162)))). % 11.76/3.80 tff(c_3652, plain, (![V_107, V_1174, V_1173]: (relation(V_107, V_1174) | ~accessible_world(V_1173, V_107) | ~accessible_world(skc12, V_1173) | ~forename(skc8, V_1174)))). % 11.76/3.80 tff(c_3524, plain, (![V_86, V_1156, V_1155]: (singleton(V_86, V_1156) | ~accessible_world(V_1155, V_86) | ~accessible_world(skc12, V_1155) | ~abstraction(skc8, V_1156)))). % 11.76/3.80 tff(c_2500, plain, (![W_932, V_901]: (skc11=W_932 | ~entity(V_901, skc10) | ~forename(V_901, W_932) | ~of(V_901, W_932, skc10) | ~forename(V_901, skc11) | ~accessible_world(skc8, V_901)))). % 11.76/3.80 tff(c_3514, plain, (![V_137, V_1150, V_1149]: (impartial(V_137, V_1150) | ~accessible_world(V_1149, V_137) | ~accessible_world(skc12, V_1149) | ~human_person(skc8, V_1150)))). % 11.76/3.80 tff(c_3424, plain, (![V_83, V_1133, V_1132]: (thing(V_83, V_1133) | ~accessible_world(V_1132, V_83) | ~accessible_world(skc12, V_1132) | ~entity(skc8, V_1133)))). % 11.76/3.80 tff(c_3404, plain, (![V_89, V_1127, V_1126]: (specific(V_89, V_1127) | ~accessible_world(V_1126, V_89) | ~accessible_world(skc12, V_1126) | ~entity(skc8, V_1127)))). % 11.76/3.80 tff(c_3304, plain, (![V_155, V_1111, V_1110]: (relname(V_155, V_1111) | ~accessible_world(V_1110, V_155) | ~accessible_world(skc12, V_1110) | ~forename(skc8, V_1111)))). % 11.76/3.80 tff(c_3349, plain, (![V_80, V_1113, V_1112]: (eventuality(V_80, V_1113) | ~accessible_world(V_1112, V_80) | ~accessible_world(skc12, V_1112) | ~event(skc8, V_1113)))). % 11.76/3.80 tff(c_3412, plain, (![V_92, V_1129, V_1128]: (nonexistent(V_92, V_1129) | ~accessible_world(V_1128, V_92) | ~accessible_world(skc12, V_1128) | ~eventuality(skc8, V_1129)))). % 11.76/3.80 tff(c_3371, plain, (![V_134, V_1117, V_1116]: (existent(V_134, V_1117) | ~accessible_world(V_1116, V_134) | ~accessible_world(skc12, V_1116) | ~entity(skc8, V_1117)))). % 11.76/3.80 tff(c_3262, plain, (![V_95, V_1097, V_1096]: (unisex(V_95, V_1097) | ~accessible_world(V_1096, V_95) | ~accessible_world(skc12, V_1096) | ~eventuality(skc8, V_1097)))). % 11.76/3.80 tff(c_3392, plain, (![V_83, V_1123, V_1122]: (thing(V_83, V_1123) | ~accessible_world(V_1122, V_83) | ~accessible_world(skc12, V_1122) | ~eventuality(skc8, V_1123)))). % 11.76/3.80 tff(c_3135, plain, (![V_164, U_1057, V_1056]: (agent(V_164, skf2(U_1057), U_1057) | ~accessible_world(V_1056, V_164) | ~accessible_world(skc12, V_1056) | ~man(skc12, U_1057)))). % 11.76/3.80 tff(c_3213, plain, (![V_113, V_1090, V_1089]: (nonhuman(V_113, V_1090) | ~accessible_world(V_1089, V_113) | ~accessible_world(skc12, V_1089) | ~abstraction(skc8, V_1090)))). % 11.76/3.80 tff(c_3253, plain, (![V_116, V_1095, V_1094]: (general(V_116, V_1095) | ~accessible_world(V_1094, V_116) | ~accessible_world(skc12, V_1094) | ~abstraction(skc8, V_1095)))). % 11.76/3.80 tff(c_3292, plain, (![V_95, V_1107, V_1106]: (unisex(V_95, V_1107) | ~accessible_world(V_1106, V_95) | ~accessible_world(skc12, V_1106) | ~abstraction(skc8, V_1107)))). % 11.76/3.80 tff(c_3440, plain, (![V_89, V_1137, V_1136]: (specific(V_89, V_1137) | ~accessible_world(V_1136, V_89) | ~accessible_world(skc12, V_1136) | ~eventuality(skc8, V_1137)))). % 11.76/3.80 tff(c_3454, plain, (![V_128, V_1139, V_1138]: (organism(V_128, V_1139) | ~accessible_world(V_1138, V_128) | ~accessible_world(skc12, V_1138) | ~human_person(skc8, V_1139)))). % 11.76/3.80 tff(c_3379, plain, (![V_83, V_1119, V_1118]: (thing(V_83, V_1119) | ~accessible_world(V_1118, V_83) | ~accessible_world(skc12, V_1118) | ~abstraction(skc8, V_1119)))). % 11.76/3.81 tff(c_3432, plain, (![V_107, V_1135, V_1134]: (relation(V_107, V_1135) | ~accessible_world(V_1134, V_107) | ~accessible_world(skc12, V_1134) | ~proposition(skc8, V_1135)))). % 11.76/3.81 tff(c_2487, plain, (![V_179, V_931]: (be(V_179, skc9, skc10, skc10) | ~accessible_world(V_931, V_179) | ~accessible_world(skc8, V_931)))). % 11.76/3.81 tff(c_2480, plain, (![V_164, V_930]: (agent(V_164, skc13, skc15) | ~accessible_world(V_930, V_164) | ~accessible_world(skc8, V_930)))). % 11.76/3.81 tff(c_2404, plain, (![V_172, V_912]: (of(V_172, skc14, skc15) | ~accessible_world(V_912, V_172) | ~accessible_world(skc8, V_912)))). % 11.76/3.81 tff(c_2188, plain, (![V_77, V_839, V_838]: (event(V_77, skf2(V_839)) | ~accessible_world(V_838, V_77) | ~accessible_world(skc12, V_838)))). % 11.76/3.81 tff(c_2396, plain, (![V_172, V_907]: (of(V_172, skc11, skc10) | ~accessible_world(V_907, V_172) | ~accessible_world(skc8, V_907)))). % 11.76/3.81 tff(c_2408, plain, (![V_168, V_913]: (theme(V_168, skc13, skc12) | ~accessible_world(V_913, V_168) | ~accessible_world(skc8, V_913)))). % 11.76/3.81 tff(c_2865, plain, (![V_131, V_1009]: (entity(V_131, skc15) | ~accessible_world(V_1009, V_131) | ~accessible_world(skc12, V_1009)))). % 11.76/3.81 tff(c_3832, plain, (![U_1207]: (~accessible_world(skc12, U_1207) | ~entity(U_1207, skc9)))). % 11.76/3.81 tff(c_2852, plain, (![V_131, V_1008]: (entity(V_131, skc10) | ~accessible_world(V_1008, V_131) | ~accessible_world(skc12, V_1008)))). % 11.76/3.81 tff(c_3488, plain, (![U_41, V_42]: (~accessible_world(skc12, U_41) | ~eventuality(skc8, V_42) | ~entity(U_41, V_42)))). % 11.76/3.81 tff(c_3653, plain, (![V_1173, V_1174]: (abstraction(V_1173, V_1174) | ~accessible_world(skc12, V_1173) | ~forename(skc8, V_1174)))). % 11.76/3.81 tff(c_3556, plain, (![U_23, V_24]: (~accessible_world(skc12, U_23) | ~eventuality(skc8, V_24) | ~abstraction(U_23, V_24)))). % 11.76/3.81 tff(c_2360, plain, (![V_74, V_897, V_896]: (smoke(V_74, skf2(V_897)) | ~accessible_world(V_896, V_74) | ~accessible_world(skc12, V_896)))). % 11.76/3.81 tff(c_3645, plain, (![U_3, V_4]: (~accessible_world(skc12, U_3) | ~entity(skc8, V_4) | ~event(U_3, V_4)))). % 11.76/3.81 tff(c_3750, plain, (![U_23, V_24]: (~accessible_world(skc12, U_23) | ~entity(skc8, V_24) | ~abstraction(U_23, V_24)))). % 11.76/3.81 tff(c_3737, plain, (![U_3, V_4]: (~accessible_world(skc12, U_3) | ~abstraction(skc8, V_4) | ~event(U_3, V_4)))). % 11.76/3.81 tff(c_2335, plain, (![V_886, V_762]: (entity(V_886, skc10) | ~accessible_world(V_762, V_886) | ~accessible_world(skc8, V_762)))). % 11.76/3.81 tff(c_2265, plain, (![V_863, V_751]: (human(V_863, skc15) | ~accessible_world(V_751, V_863) | ~accessible_world(skc8, V_751)))). % 11.76/3.81 tff(c_3405, plain, (![V_1126, V_1127]: (~general(V_1126, V_1127) | ~accessible_world(skc12, V_1126) | ~entity(skc8, V_1127)))). % 11.76/3.81 tff(c_3254, plain, (![V_1094, V_1095]: (~eventuality(V_1094, V_1095) | ~accessible_world(skc12, V_1094) | ~abstraction(skc8, V_1095)))). % 11.76/3.81 tff(c_2276, plain, (![V_98, V_868, V_867]: (present(V_98, skf2(V_868)) | ~accessible_world(V_867, V_98) | ~accessible_world(skc12, V_867)))). % 11.76/3.81 tff(c_2168, plain, (![V_828, V_751]: (animate(V_828, skc15) | ~accessible_world(V_751, V_828) | ~accessible_world(skc8, V_751)))). % 11.76/3.81 tff(c_3293, plain, (![V_1106, V_1107]: (~male(V_1106, V_1107) | ~accessible_world(skc12, V_1106) | ~abstraction(skc8, V_1107)))). % 11.76/3.81 tff(c_2266, plain, (![V_863, V_762]: (human(V_863, skc10) | ~accessible_world(V_762, V_863) | ~accessible_world(skc8, V_762)))). % 11.76/3.81 tff(c_3255, plain, (![V_1094, V_1095]: (~entity(V_1094, V_1095) | ~accessible_world(skc12, V_1094) | ~abstraction(skc8, V_1095)))). % 11.76/3.81 tff(c_2903, plain, (![V_107, V_1021]: (relation(V_107, V_1021) | ~accessible_world(skc12, V_107) | ~forename(skc8, V_1021)))). % 11.76/3.81 tff(c_3372, plain, (![V_1116, V_1117]: (~eventuality(V_1116, V_1117) | ~accessible_world(skc12, V_1116) | ~entity(skc8, V_1117)))). % 11.76/3.81 tff(c_3263, plain, (![V_1096, V_1097]: (~male(V_1096, V_1097) | ~accessible_world(skc12, V_1096) | ~eventuality(skc8, V_1097)))). % 11.76/3.81 tff(c_2167, plain, (![V_828, V_762]: (animate(V_828, skc10) | ~accessible_world(V_762, V_828) | ~accessible_world(skc8, V_762)))). % 11.76/3.81 tff(c_3455, plain, (![V_1138, V_1139]: (entity(V_1138, V_1139) | ~accessible_world(skc12, V_1138) | ~human_person(skc8, V_1139)))). % 11.76/3.81 tff(c_3352, plain, (![V_1112, V_1113]: (~entity(V_1112, V_1113) | ~accessible_world(skc12, V_1112) | ~event(skc8, V_1113)))). % 11.76/3.81 tff(c_3393, plain, (![V_1122, V_1123]: (singleton(V_1122, V_1123) | ~accessible_world(skc12, V_1122) | ~eventuality(skc8, V_1123)))). % 11.76/3.81 tff(c_3559, plain, (~event(skc8, skc11))). % 11.76/3.81 tff(c_3558, plain, (~event(skc8, skc14))). % 11.76/3.81 tff(c_3557, plain, (~event(skc8, skc12))). % 11.76/3.81 tff(c_3441, plain, (![V_1136, V_1137]: (~general(V_1136, V_1137) | ~accessible_world(skc12, V_1136) | ~eventuality(skc8, V_1137)))). % 11.76/3.81 tff(c_3353, plain, (![V_1112, V_1113]: (~abstraction(V_1112, V_1113) | ~accessible_world(skc12, V_1112) | ~event(skc8, V_1113)))). % 11.76/3.81 tff(c_3380, plain, (![V_1118, V_1119]: (singleton(V_1118, V_1119) | ~accessible_world(skc12, V_1118) | ~abstraction(skc8, V_1119)))). % 11.76/3.81 tff(c_3520, plain, (~jules_forename(skc8, skc14))). % 11.76/3.81 tff(c_3433, plain, (![V_1134, V_1135]: (abstraction(V_1134, V_1135) | ~accessible_world(skc12, V_1134) | ~proposition(skc8, V_1135)))). % 11.76/3.81 tff(c_3425, plain, (![V_1132, V_1133]: (singleton(V_1132, V_1133) | ~accessible_world(skc12, V_1132) | ~entity(skc8, V_1133)))). % 11.76/3.81 tff(c_2759, plain, (![V_137, V_997]: (impartial(V_137, V_997) | ~accessible_world(skc12, V_137) | ~human_person(skc8, V_997)))). % 11.76/3.81 tff(c_2334, plain, (![V_886, V_751]: (entity(V_886, skc15) | ~accessible_world(V_751, V_886) | ~accessible_world(skc8, V_751)))). % 11.76/3.81 tff(c_3214, plain, (![V_1089, V_1090]: (~human(V_1089, V_1090) | ~accessible_world(skc12, V_1089) | ~abstraction(skc8, V_1090)))). % 11.76/3.81 tff(c_3413, plain, (![V_1128, V_1129]: (~existent(V_1128, V_1129) | ~accessible_world(skc12, V_1128) | ~eventuality(skc8, V_1129)))). % 11.76/3.81 tff(c_3457, plain, (![V_1138, V_1139]: (living(V_1138, V_1139) | ~accessible_world(skc12, V_1138) | ~human_person(skc8, V_1139)))). % 11.76/3.81 tff(c_3471, plain, (~vincent_forename(skc8, skc11))). % 11.76/3.81 tff(c_3385, plain, (![X3_959]: (~forename(skc8, X3_959) | ~vincent_forename(skc8, X3_959) | ~of(skc8, X3_959, skc10)))). % 11.76/3.81 tff(c_2703, plain, (![V_128, V_991]: (organism(V_128, V_991) | ~accessible_world(skc12, V_128) | ~human_person(skc8, V_991)))). % 11.76/3.81 tff(c_2818, plain, (![V_89, V_1005]: (specific(V_89, V_1005) | ~accessible_world(skc12, V_89) | ~eventuality(skc8, V_1005)))). % 11.76/3.81 tff(c_2379, plain, (![V_107, V_905]: (relation(V_107, V_905) | ~accessible_world(skc12, V_107) | ~proposition(skc8, V_905)))). % 11.76/3.81 tff(c_2879, plain, (![V_83, V_1015]: (thing(V_83, V_1015) | ~accessible_world(skc12, V_83) | ~entity(skc8, V_1015)))). % 11.76/3.81 tff(c_1913, plain, (![V_149, V_768]: (male(V_149, skc10) | ~accessible_world(V_768, V_149) | ~accessible_world(skc8, V_768)))). % 11.76/3.81 tff(c_2419, plain, (![V_92, V_917]: (nonexistent(V_92, V_917) | ~accessible_world(skc12, V_92) | ~eventuality(skc8, V_917)))). % 11.76/3.81 tff(c_2599, plain, (![V_89, V_955]: (specific(V_89, V_955) | ~accessible_world(skc12, V_89) | ~entity(skc8, V_955)))). % 11.76/3.81 tff(c_1925, plain, (![V_149, V_769]: (male(V_149, skc15) | ~accessible_world(V_769, V_149) | ~accessible_world(skc8, V_769)))). % 11.76/3.81 tff(c_2938, plain, (![V_83, V_1026]: (thing(V_83, V_1026) | ~accessible_world(skc12, V_83) | ~eventuality(skc8, V_1026)))). % 11.76/3.81 tff(c_2322, plain, (![V_883, V_819]: (forename(V_883, skc14) | ~accessible_world(V_819, V_883) | ~accessible_world(skc8, V_819)))). % 11.76/3.81 tff(c_2517, plain, (![V_83, V_939]: (thing(V_83, V_939) | ~accessible_world(skc12, V_83) | ~abstraction(skc8, V_939)))). % 11.76/3.81 tff(c_2754, plain, (![V_134, V_996]: (existent(V_134, V_996) | ~accessible_world(skc12, V_134) | ~entity(skc8, V_996)))). % 11.76/3.81 tff(c_2108, plain, (![V_77, V_815]: (event(V_77, skc9) | ~accessible_world(V_815, V_77) | ~accessible_world(skc8, V_815)))). % 11.76/3.81 tff(c_2556, plain, (![V_80, V_950]: (eventuality(V_80, V_950) | ~accessible_world(skc12, V_80) | ~event(skc8, V_950)))). % 11.76/3.81 tff(c_2895, plain, (![V_155, V_1020]: (relname(V_155, V_1020) | ~accessible_world(skc12, V_155) | ~forename(skc8, V_1020)))). % 11.76/3.81 tff(c_2150, plain, (![V_80, V_826]: (eventuality(V_80, skc9) | ~accessible_world(V_826, V_80) | ~accessible_world(skc8, V_826)))). % 11.76/3.81 tff(c_2670, plain, (![V_95, V_986]: (unisex(V_95, V_986) | ~accessible_world(skc12, V_95) | ~abstraction(skc8, V_986)))). % 11.76/3.81 tff(c_1887, plain, (![V_125, V_762]: (human_person(V_125, skc10) | ~accessible_world(V_762, V_125) | ~accessible_world(skc8, V_762)))). % 11.76/3.81 tff(c_2531, plain, (![W_945, V_943, Y_944, U_196]: (W_945=V_943 | ~agent(skc12, Y_944, U_196) | ~theme(skc12, Y_944, W_945) | ~think_believe_consider(skc12, Y_944) | ~think_believe_consider(skc12, skf2(U_196)) | ~theme(skc12, skf2(U_196), V_943) | ~proposition(skc12, W_945) | ~proposition(skc12, V_943) | ~man(skc12, U_196)))). % 11.76/3.81 tff(c_1836, plain, (![V_125, V_751]: (human_person(V_125, skc15) | ~accessible_world(V_751, V_125) | ~accessible_world(skc8, V_751)))). % 11.76/3.81 tff(c_3053, plain, (![V_95, V_1039]: (unisex(V_95, V_1039) | ~accessible_world(skc12, V_95) | ~eventuality(skc8, V_1039)))). % 11.76/3.81 tff(c_2965, plain, (![V_116, V_1031]: (general(V_116, V_1031) | ~accessible_world(skc12, V_116) | ~abstraction(skc8, V_1031)))). % 11.76/3.81 tff(c_2321, plain, (![V_883, V_858]: (forename(V_883, skc11) | ~accessible_world(V_858, V_883) | ~accessible_world(skc8, V_858)))). % 11.76/3.81 tff(c_3194, plain, (![V_1080]: (skc12=V_1080 | ~theme(skc8, skc13, V_1080) | ~proposition(skc8, V_1080)))). % 11.76/3.81 tff(c_3080, plain, (![V_113, V_1044]: (nonhuman(V_113, V_1044) | ~accessible_world(skc12, V_113) | ~abstraction(skc8, V_1044)))). % 11.76/3.81 tff(c_2348, plain, (![V_104, V_892]: (proposition(V_104, skc12) | ~accessible_world(V_892, V_104) | ~accessible_world(skc8, V_892)))). % 11.76/3.81 tff(c_1849, plain, (![V_752, V_6, U_5]: (singleton(V_752, V_6) | ~accessible_world(U_5, V_752) | ~eventuality(U_5, V_6)))). % 11.76/3.81 tff(c_2242, plain, (![V_161, V_858]: (jules_forename(V_161, skc11) | ~accessible_world(V_858, V_161) | ~accessible_world(skc8, V_858)))). % 11.76/3.81 tff(c_2534, plain, (![W_945, V_943, Y_944]: (W_945=V_943 | ~agent(skc8, Y_944, skc15) | ~theme(skc8, Y_944, W_945) | ~think_believe_consider(skc8, Y_944) | ~theme(skc8, skc13, V_943) | ~proposition(skc8, W_945) | ~proposition(skc8, V_943)))). % 11.76/3.81 tff(c_2272, plain, (![V_98, V_866]: (present(V_98, skc13) | ~accessible_world(V_866, V_98) | ~accessible_world(skc8, V_866)))). % 11.76/3.81 tff(c_2503, plain, (![W_932]: (skc11=W_932 | ~forename(skc8, W_932) | ~of(skc8, W_932, skc10)))). % 11.76/3.81 tff(c_2291, plain, (![V_101, V_875]: (think_believe_consider(V_101, skc13) | ~accessible_world(V_875, V_101) | ~accessible_world(skc8, V_875)))). % 11.76/3.81 tff(c_2220, plain, (![V_122, V_846]: (man(V_122, skc10) | ~accessible_world(V_846, V_122) | ~accessible_world(skc8, V_846)))). % 11.76/3.81 tff(c_2177, plain, (![V_834, V_227, U_226]: (living(V_834, V_227) | ~accessible_world(U_226, V_834) | ~human_person(U_226, V_227)))). % 11.76/3.81 tff(c_2309, plain, (![V_119, V_882]: (state(V_119, skc9) | ~accessible_world(V_882, V_119) | ~accessible_world(skc8, V_882)))). % 11.76/3.82 tff(c_2044, plain, (![V_800, V_54, U_53]: (relation(V_800, V_54) | ~accessible_world(U_53, V_800) | ~forename(U_53, V_54)))). % 11.76/3.82 tff(c_2227, plain, (![V_849, V_34, U_33]: (impartial(V_849, V_34) | ~accessible_world(U_33, V_849) | ~human_person(U_33, V_34)))). % 11.76/3.82 tff(c_1848, plain, (![V_752, V_20, U_19]: (singleton(V_752, V_20) | ~accessible_world(U_19, V_752) | ~abstraction(U_19, V_20)))). % 11.76/3.82 tff(c_2432, plain, (![V_919, U_196]: (agent(V_919, skf2(U_196), U_196) | ~accessible_world(skc12, V_919) | ~man(skc12, U_196)))). % 11.76/3.82 tff(c_2506, plain, (![W_932]: (skc14=W_932 | ~forename(skc8, W_932) | ~of(skc8, W_932, skc15)))). % 11.76/3.82 tff(c_2121, plain, (![V_158, V_819]: (vincent_forename(V_158, skc14) | ~accessible_world(V_819, V_158) | ~accessible_world(skc8, V_819)))). % 11.76/3.82 tff(c_2096, plain, (![V_77, V_814]: (event(V_77, skc13) | ~accessible_world(V_814, V_77) | ~accessible_world(skc8, V_814)))). % 11.76/3.82 tff(c_3105, plain, (~accessible_world(skc8, skc8))). % 11.76/3.82 tff(c_2208, plain, (![V_122, V_845]: (man(V_122, skc15) | ~accessible_world(V_845, V_122) | ~accessible_world(skc8, V_845)))). % 11.76/3.82 tff(c_1847, plain, (![V_752, V_38, U_37]: (singleton(V_752, V_38) | ~accessible_world(U_37, V_752) | ~entity(U_37, V_38)))). % 11.76/3.82 tff(c_3081, plain, (![V_1044]: (~human(skc12, V_1044) | ~abstraction(skc8, V_1044)))). % 11.76/3.82 tff(c_3073, plain, (![V_1042]: (nonhuman(skc12, V_1042) | ~abstraction(skc8, V_1042)))). % 11.76/3.82 tff(c_1903, plain, (![V_765, V_22, U_21]: (nonhuman(V_765, V_22) | ~accessible_world(U_21, V_765) | ~abstraction(U_21, V_22)))). % 11.76/3.82 tff(c_3054, plain, (![V_1039]: (~male(skc12, V_1039) | ~eventuality(skc8, V_1039)))). % 11.76/3.82 tff(c_3046, plain, (![V_1037]: (unisex(skc12, V_1037) | ~eventuality(skc8, V_1037)))). % 11.76/3.82 tff(c_2025, plain, (![V_793, V_14, U_13]: (unisex(V_793, V_14) | ~accessible_world(U_13, V_793) | ~eventuality(U_13, V_14)))). % 11.76/3.82 tff(c_3041, plain, (![V_195]: (~abstraction(skc8, skf2(V_195))))). % 11.76/3.82 tff(c_2984, plain, (![V_4]: (~abstraction(skc8, V_4) | ~event(skc12, V_4)))). % 11.76/3.82 tff(c_2967, plain, (![V_1031]: (~entity(skc12, V_1031) | ~abstraction(skc8, V_1031)))). % 11.76/3.82 tff(c_2966, plain, (![V_1031]: (~eventuality(skc12, V_1031) | ~abstraction(skc8, V_1031)))). % 11.76/3.82 tff(c_2947, plain, (![V_1029]: (general(skc12, V_1029) | ~abstraction(skc8, V_1029)))). % 11.76/3.82 tff(c_2295, plain, (![V_876, V_24, U_23]: (general(V_876, V_24) | ~accessible_world(U_23, V_876) | ~abstraction(U_23, V_24)))). % 11.76/3.82 tff(c_2939, plain, (![V_1026]: (singleton(skc12, V_1026) | ~eventuality(skc8, V_1026)))). % 11.76/3.82 tff(c_2931, plain, (![V_1024]: (thing(skc12, V_1024) | ~eventuality(skc8, V_1024)))). % 11.76/3.82 tff(c_1964, plain, (![V_775, V_6, U_5]: (thing(V_775, V_6) | ~accessible_world(U_5, V_775) | ~eventuality(U_5, V_6)))). % 11.76/3.82 tff(c_2904, plain, (![V_1021]: (abstraction(skc12, V_1021) | ~forename(skc8, V_1021)))). % 11.76/3.82 tff(c_2896, plain, (![V_1020]: (relation(skc12, V_1020) | ~forename(skc8, V_1020)))). % 11.76/3.82 tff(c_2888, plain, (![V_1018]: (relname(skc12, V_1018) | ~forename(skc8, V_1018)))). % 11.76/3.82 tff(c_1814, plain, (![V_746, V_54, U_53]: (relname(V_746, V_54) | ~accessible_world(U_53, V_746) | ~forename(U_53, V_54)))). % 11.76/3.82 tff(c_2880, plain, (![V_1015]: (singleton(skc12, V_1015) | ~entity(skc8, V_1015)))). % 11.76/3.82 tff(c_2872, plain, (![V_1013]: (thing(skc12, V_1013) | ~entity(skc8, V_1013)))). % 11.76/3.82 tff(c_1965, plain, (![V_775, V_38, U_37]: (thing(V_775, V_38) | ~accessible_world(U_37, V_775) | ~entity(U_37, V_38)))). % 11.76/3.82 tff(c_2866, plain, (![V_1009]: (~abstraction(V_1009, skc15) | ~accessible_world(skc12, V_1009)))). % 11.76/3.82 tff(c_2853, plain, (![V_1008]: (~abstraction(V_1008, skc10) | ~accessible_world(skc12, V_1008)))). % 11.76/3.82 tff(c_2742, plain, (![V_131]: (entity(V_131, skc15) | ~accessible_world(skc12, V_131)))). % 11.76/3.82 tff(c_2735, plain, (![V_131]: (entity(V_131, skc10) | ~accessible_world(skc12, V_131)))). % 11.76/3.82 tff(c_2825, plain, (![V_24]: (~eventuality(skc8, V_24) | ~abstraction(skc12, V_24)))). % 11.76/3.82 tff(c_2819, plain, (![V_1005]: (~general(skc12, V_1005) | ~eventuality(skc8, V_1005)))). % 11.76/3.82 tff(c_2810, plain, (![V_1002]: (specific(skc12, V_1002) | ~eventuality(skc8, V_1002)))). % 11.76/3.82 tff(c_2806, plain, (![V_195]: (~entity(skc8, skf2(V_195))))). % 11.76/3.82 tff(c_2282, plain, (![V_869, V_10, U_9]: (specific(V_869, V_10) | ~accessible_world(U_9, V_869) | ~eventuality(U_9, V_10)))). % 11.76/3.82 tff(c_2776, plain, (![V_4]: (~entity(skc8, V_4) | ~event(skc12, V_4)))). % 11.76/3.82 tff(c_2706, plain, (![V_991]: (living(skc12, V_991) | ~human_person(skc8, V_991)))). % 11.76/3.82 tff(c_2755, plain, (![V_996]: (~eventuality(skc12, V_996) | ~entity(skc8, V_996)))). % 11.76/3.82 tff(c_2705, plain, (![V_991]: (impartial(skc12, V_991) | ~human_person(skc8, V_991)))). % 11.76/3.82 tff(c_2729, plain, (![V_994]: (existent(skc12, V_994) | ~entity(skc8, V_994)))). % 11.76/3.82 tff(c_2725, plain, (entity(skc12, skc15))). % 11.76/3.82 tff(c_2724, plain, (entity(skc12, skc10))). % 11.76/3.82 tff(c_2231, plain, (![V_852, V_42, U_41]: (existent(V_852, V_42) | ~accessible_world(U_41, V_852) | ~entity(U_41, V_42)))). % 11.76/3.82 tff(c_2704, plain, (![V_991]: (entity(skc12, V_991) | ~human_person(skc8, V_991)))). % 11.76/3.82 tff(c_2690, plain, (![V_989]: (organism(skc12, V_989) | ~human_person(skc8, V_989)))). % 11.76/3.82 tff(c_2058, plain, (![V_804, V_34, U_33]: (organism(V_804, V_34) | ~accessible_world(U_33, V_804) | ~human_person(U_33, V_34)))). % 11.76/3.82 tff(c_2671, plain, (![V_986]: (~male(skc12, V_986) | ~abstraction(skc8, V_986)))). % 11.76/3.82 tff(c_2646, plain, (![V_971]: (unisex(skc12, V_971) | ~abstraction(skc8, V_971)))). % 11.76/3.82 tff(c_190, plain, (![X3_212, W_211, V_220, X2_217, Y_219, U_213, X1_216, X7_215, X5_209, X6_210, X4_221, X_218, Z_214]: (~actual_world(U_213) | ~of(U_213, X7_215, X5_209) | ~jules_forename(U_213, X7_215) | ~forename(U_213, X7_215) | ~event(X1_216, X6_210) | ~agent(X1_216, X6_210, X5_209) | ~present(X1_216, X6_210) | ~smoke(X1_216, X6_210) | ~agent(U_213, X2_217, X5_209) | ~be(U_213, X3_212, X5_209, X5_209) | ~man(U_213, X5_209) | ~forename(U_213, X4_221) | ~vincent_forename(U_213, X4_221) | ~of(U_213, X4_221, X5_209) | ~state(U_213, X3_212) | ~think_believe_consider(U_213, X2_217) | ~present(U_213, X2_217) | ~event(U_213, X2_217) | ~theme(U_213, X2_217, X1_216) | ~proposition(U_213, X1_216) | ~accessible_world(U_213, X1_216) | ~of(U_213, Y_219, Z_214) | ~man(U_213, Z_214) | ~agent(U_213, X_218, Z_214) | ~forename(U_213, Y_219) | ~vincent_forename(U_213, Y_219) | ~theme(U_213, X_218, V_220) | ~event(U_213, X_218) | ~present(U_213, X_218) | ~think_believe_consider(U_213, X_218) | ~event(V_220, W_211) | ~agent(V_220, W_211, skf4(V_220)) | ~present(V_220, W_211) | ~smoke(V_220, W_211) | ~accessible_world(U_213, V_220) | ~proposition(U_213, V_220)))). % 11.76/3.82 tff(c_2026, plain, (![V_793, V_26, U_25]: (unisex(V_793, V_26) | ~accessible_world(U_25, V_793) | ~abstraction(U_25, V_26)))). % 11.76/3.82 tff(c_2623, plain, (![V_24]: (~entity(skc8, V_24) | ~abstraction(skc12, V_24)))). % 11.76/3.82 tff(c_2600, plain, (![V_955]: (~general(skc12, V_955) | ~entity(skc8, V_955)))). % 11.76/3.82 tff(c_188, plain, (![W_199, Z_202, X4_208, X5_197, X_205, X6_198, V_207, U_201, X2_204, X3_200, X1_203, Y_206]: (man(V_207, skf4(V_207)) | ~actual_world(U_201) | ~of(U_201, X6_198, X4_208) | ~jules_forename(U_201, X6_198) | ~forename(U_201, X6_198) | ~event(Z_202, X5_197) | ~agent(Z_202, X5_197, X4_208) | ~present(Z_202, X5_197) | ~smoke(Z_202, X5_197) | ~agent(U_201, X1_203, X4_208) | ~be(U_201, X2_204, X4_208, X4_208) | ~man(U_201, X4_208) | ~forename(U_201, X3_200) | ~vincent_forename(U_201, X3_200) | ~of(U_201, X3_200, X4_208) | ~state(U_201, X2_204) | ~think_believe_consider(U_201, X1_203) | ~present(U_201, X1_203) | ~event(U_201, X1_203) | ~theme(U_201, X1_203, Z_202) | ~proposition(U_201, Z_202) | ~accessible_world(U_201, Z_202) | ~of(U_201, X_205, Y_206) | ~man(U_201, Y_206) | ~agent(U_201, W_199, Y_206) | ~forename(U_201, X_205) | ~vincent_forename(U_201, X_205) | ~theme(U_201, W_199, V_207) | ~event(U_201, W_199) | ~present(U_201, W_199) | ~think_believe_consider(U_201, W_199) | ~accessible_world(U_201, V_207) | ~proposition(U_201, V_207)))). % 11.76/3.82 tff(c_2592, plain, (![V_953]: (specific(skc12, V_953) | ~entity(skc8, V_953)))). % 11.76/3.82 tff(c_2283, plain, (![V_869, V_40, U_39]: (specific(V_869, V_40) | ~accessible_world(U_39, V_869) | ~entity(U_39, V_40)))). % 11.76/3.82 tff(c_2564, plain, (![V_950]: (~abstraction(skc12, V_950) | ~event(skc8, V_950)))). % 11.76/3.82 tff(c_2538, plain, (![V_948]: (eventuality(skc12, V_948) | ~event(skc8, V_948)))). % 11.76/3.82 tff(c_2140, plain, (![V_823, V_4, U_3]: (eventuality(V_823, V_4) | ~accessible_world(U_3, V_823) | ~event(U_3, V_4)))). % 11.76/3.82 tff(c_142, plain, (![Z_186, V_189, X_187, Y_188, U_185, W_184]: (W_184=V_189 | ~agent(U_185, X_187, Z_186) | ~agent(U_185, Y_188, Z_186) | ~theme(U_185, Y_188, W_184) | ~think_believe_consider(U_185, Y_188) | ~think_believe_consider(U_185, X_187) | ~theme(U_185, X_187, V_189) | ~proposition(U_185, W_184) | ~proposition(U_185, V_189)))). % 11.76/3.82 tff(c_2518, plain, (![V_939]: (singleton(skc12, V_939) | ~abstraction(skc8, V_939)))). % 11.76/3.82 tff(c_2510, plain, (![V_937]: (thing(skc12, V_937) | ~abstraction(skc8, V_937)))). % 11.76/3.82 tff(c_1963, plain, (![V_775, V_20, U_19]: (thing(V_775, V_20) | ~accessible_world(U_19, V_775) | ~abstraction(U_19, V_20)))). % 11.76/3.82 tff(c_140, plain, (![W_182, V_181, U_180, X_183]: (W_182=V_181 | ~entity(U_180, X_183) | ~of(U_180, V_181, X_183) | ~forename(U_180, W_182) | ~of(U_180, W_182, X_183) | ~forename(U_180, V_181)))). % 11.76/3.82 tff(c_2452, plain, (![V_928]: (be(V_928, skc9, skc10, skc10) | ~accessible_world(skc8, V_928)))). % 11.76/3.82 tff(c_2433, plain, (![V_919]: (agent(V_919, skc13, skc15) | ~accessible_world(skc8, V_919)))). % 11.76/3.82 tff(c_2476, plain, (~entity(skc12, skc13))). % 11.76/3.82 tff(c_2448, plain, (![V_4]: (~entity(skc12, V_4) | ~event(skc8, V_4)))). % 11.76/3.82 tff(c_138, plain, (![X_177, Y_178, U_176, W_175, V_179]: (be(V_179, W_175, X_177, Y_178) | ~be(U_176, W_175, X_177, Y_178) | ~accessible_world(U_176, V_179)))). % 11.76/3.82 tff(c_2447, plain, (~entity(skc12, skc9))). % 11.76/3.82 tff(c_2426, plain, (![V_42]: (~eventuality(skc8, V_42) | ~entity(skc12, V_42)))). % 11.76/3.82 tff(c_132, plain, (![V_164, W_165, X_166, U_163]: (agent(V_164, W_165, X_166) | ~agent(U_163, W_165, X_166) | ~accessible_world(U_163, V_164)))). % 11.76/3.82 tff(c_2420, plain, (![V_917]: (~existent(skc12, V_917) | ~eventuality(skc8, V_917)))). % 11.76/3.82 tff(c_2412, plain, (![V_915]: (nonexistent(skc12, V_915) | ~eventuality(skc8, V_915)))). % 11.76/3.82 tff(c_1975, plain, (![V_780, V_12, U_11]: (nonexistent(V_780, V_12) | ~accessible_world(U_11, V_780) | ~eventuality(U_11, V_12)))). % 11.76/3.82 tff(c_2400, plain, (![V_908]: (theme(V_908, skc13, skc12) | ~accessible_world(skc8, V_908)))). % 11.76/3.82 tff(c_2372, plain, (![V_901]: (of(V_901, skc14, skc15) | ~accessible_world(skc8, V_901)))). % 11.76/3.82 tff(c_134, plain, (![V_168, W_169, X_170, U_167]: (theme(V_168, W_169, X_170) | ~theme(U_167, W_169, X_170) | ~accessible_world(U_167, V_168)))). % 11.76/3.82 tff(c_2371, plain, (![V_901]: (of(V_901, skc11, skc10) | ~accessible_world(skc8, V_901)))). % 11.76/3.82 tff(c_2380, plain, (![V_905]: (abstraction(skc12, V_905) | ~proposition(skc8, V_905)))). % 11.76/3.82 tff(c_2365, plain, (![V_899]: (relation(skc12, V_899) | ~proposition(skc8, V_899)))). % 11.76/3.82 tff(c_136, plain, (![V_172, W_173, X_174, U_171]: (of(V_172, W_173, X_174) | ~of(U_171, W_173, X_174) | ~accessible_world(U_171, V_172)))). % 11.76/3.82 tff(c_2045, plain, (![V_800, V_16, U_15]: (relation(V_800, V_16) | ~accessible_world(U_15, V_800) | ~proposition(U_15, V_16)))). % 11.76/3.82 tff(c_2353, plain, (![V_893, V_191]: (smoke(V_893, skf2(V_191)) | ~accessible_world(skc12, V_893)))). % 11.76/3.82 tff(c_72, plain, (![V_74, W_75, U_73]: (smoke(V_74, W_75) | ~smoke(U_73, W_75) | ~accessible_world(U_73, V_74)))). % 11.76/3.82 tff(c_2341, plain, (![V_889]: (proposition(V_889, skc12) | ~accessible_world(skc8, V_889)))). % 11.76/3.82 tff(c_92, plain, (![V_104, W_105, U_103]: (proposition(V_104, W_105) | ~proposition(U_103, W_105) | ~accessible_world(U_103, V_104)))). % 11.76/3.82 tff(c_110, plain, (![V_131, W_132, U_130]: (entity(V_131, W_132) | ~entity(U_130, W_132) | ~accessible_world(U_130, V_131)))). % 11.76/3.82 tff(c_124, plain, (![V_152, W_153, U_151]: (forename(V_152, W_153) | ~forename(U_151, W_153) | ~accessible_world(U_151, V_152)))). % 11.76/3.82 tff(c_2299, plain, (![V_879]: (state(V_879, skc9) | ~accessible_world(skc8, V_879)))). % 11.76/3.83 tff(c_102, plain, (![V_119, W_120, U_118]: (state(V_119, W_120) | ~state(U_118, W_120) | ~accessible_world(U_118, V_119)))). % 11.76/3.83 tff(c_100, plain, (![V_116, W_117, U_115]: (general(V_116, W_117) | ~general(U_115, W_117) | ~accessible_world(U_115, V_116)))). % 11.76/3.83 tff(c_2287, plain, (![V_872]: (think_believe_consider(V_872, skc13) | ~accessible_world(skc8, V_872)))). % 11.76/3.83 tff(c_90, plain, (![V_101, W_102, U_100]: (think_believe_consider(V_101, W_102) | ~think_believe_consider(U_100, W_102) | ~accessible_world(U_100, V_101)))). % 11.76/3.83 tff(c_82, plain, (![V_89, W_90, U_88]: (specific(V_89, W_90) | ~specific(U_88, W_90) | ~accessible_world(U_88, V_89)))). % 11.76/3.83 tff(c_2254, plain, (![V_860, V_193]: (present(V_860, skf2(V_193)) | ~accessible_world(skc12, V_860)))). % 11.76/3.83 tff(c_2255, plain, (![V_860]: (present(V_860, skc13) | ~accessible_world(skc8, V_860)))). % 11.76/3.83 tff(c_118, plain, (![V_143, W_144, U_142]: (human(V_143, W_144) | ~human(U_142, W_144) | ~accessible_world(U_142, V_143)))). % 11.76/3.83 tff(c_88, plain, (![V_98, W_99, U_97]: (present(V_98, W_99) | ~present(U_97, W_99) | ~accessible_world(U_97, V_98)))). % 11.76/3.83 tff(c_2243, plain, (![V_858]: (forename(V_858, skc11) | ~accessible_world(skc8, V_858)))). % 11.76/3.83 tff(c_2235, plain, (![V_855]: (jules_forename(V_855, skc11) | ~accessible_world(skc8, V_855)))). % 11.76/3.83 tff(c_130, plain, (![V_161, W_162, U_160]: (jules_forename(V_161, W_162) | ~jules_forename(U_160, W_162) | ~accessible_world(U_160, V_161)))). % 11.76/3.83 tff(c_112, plain, (![V_134, W_135, U_133]: (existent(V_134, W_135) | ~existent(U_133, W_135) | ~accessible_world(U_133, V_134)))). % 11.76/3.83 tff(c_114, plain, (![V_137, W_138, U_136]: (impartial(V_137, W_138) | ~impartial(U_136, W_138) | ~accessible_world(U_136, V_137)))). % 11.76/3.83 tff(c_2190, plain, (![V_838, V_839]: (~entity(V_838, skf2(V_839)) | ~accessible_world(skc12, V_838)))). % 11.76/3.83 tff(c_2198, plain, (![V_842]: (man(V_842, skc10) | ~accessible_world(skc8, V_842)))). % 11.76/3.83 tff(c_2197, plain, (![V_842]: (man(V_842, skc15) | ~accessible_world(skc8, V_842)))). % 11.76/3.83 tff(c_104, plain, (![V_122, W_123, U_121]: (man(V_122, W_123) | ~man(U_121, W_123) | ~accessible_world(U_121, V_122)))). % 11.76/3.83 tff(c_2189, plain, (![V_838, V_839]: (~abstraction(V_838, skf2(V_839)) | ~accessible_world(skc12, V_838)))). % 11.76/3.83 tff(c_2081, plain, (![V_811, V_195]: (event(V_811, skf2(V_195)) | ~accessible_world(skc12, V_811)))). % 11.76/3.83 tff(c_2068, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc12, V_110)))). % 11.76/3.83 tff(c_116, plain, (![V_140, W_141, U_139]: (living(V_140, W_141) | ~living(U_139, W_141) | ~accessible_world(U_139, V_140)))). % 11.76/3.83 tff(c_2086, plain, (![V_110]: (abstraction(V_110, skc11) | ~accessible_world(skc12, V_110)))). % 11.76/3.83 tff(c_2048, plain, (![V_110]: (abstraction(V_110, skc12) | ~accessible_world(skc12, V_110)))). % 11.76/3.83 tff(c_2098, plain, (![V_814]: (~entity(V_814, skc13) | ~accessible_world(skc8, V_814)))). % 11.76/3.83 tff(c_120, plain, (![V_146, W_147, U_145]: (animate(V_146, W_147) | ~animate(U_145, W_147) | ~accessible_world(U_145, V_146)))). % 11.76/3.83 tff(c_2157, plain, (~abstraction(skc12, skc9))). % 11.76/3.83 tff(c_2152, plain, (![V_826]: (~abstraction(V_826, skc9) | ~accessible_world(skc8, V_826)))). % 11.76/3.83 tff(c_2139, plain, (![V_823]: (eventuality(V_823, skc9) | ~accessible_world(skc8, V_823)))). % 11.76/3.83 tff(c_76, plain, (![V_80, W_81, U_79]: (eventuality(V_80, W_81) | ~eventuality(U_79, W_81) | ~accessible_world(U_79, V_80)))). % 11.76/3.83 tff(c_2110, plain, (![V_815]: (~entity(V_815, skc9) | ~accessible_world(skc8, V_815)))). % 11.76/3.83 tff(c_2132, plain, (~abstraction(skc12, skc13))). % 11.76/3.83 tff(c_2097, plain, (![V_814]: (~abstraction(V_814, skc13) | ~accessible_world(skc8, V_814)))). % 11.76/3.83 tff(c_2122, plain, (![V_819]: (forename(V_819, skc14) | ~accessible_world(skc8, V_819)))). % 11.76/3.83 tff(c_2114, plain, (![V_816]: (vincent_forename(V_816, skc14) | ~accessible_world(skc8, V_816)))). % 11.76/3.83 tff(c_128, plain, (![V_158, W_159, U_157]: (vincent_forename(V_158, W_159) | ~vincent_forename(U_157, W_159) | ~accessible_world(U_157, V_158)))). % 11.76/3.83 tff(c_2082, plain, (![V_811]: (event(V_811, skc9) | ~accessible_world(skc8, V_811)))). % 11.76/3.83 tff(c_2083, plain, (![V_811]: (event(V_811, skc13) | ~accessible_world(skc8, V_811)))). % 11.76/3.83 tff(c_2073, plain, (abstraction(skc12, skc11))). % 11.76/3.83 tff(c_74, plain, (![V_77, W_78, U_76]: (event(V_77, W_78) | ~event(U_76, W_78) | ~accessible_world(U_76, V_77)))). % 11.76/3.83 tff(c_1999, plain, (![V_787]: (abstraction(V_787, skc11) | ~accessible_world(skc8, V_787)))). % 11.76/3.83 tff(c_2065, plain, (abstraction(skc12, skc14))). % 11.76/3.83 tff(c_2000, plain, (![V_787]: (abstraction(V_787, skc14) | ~accessible_world(skc8, V_787)))). % 11.76/3.83 tff(c_2054, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc10)))). % 11.76/3.83 tff(c_1942, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc15)))). % 11.76/3.83 tff(c_108, plain, (![V_128, W_129, U_127]: (organism(V_128, W_129) | ~organism(U_127, W_129) | ~accessible_world(U_127, V_128)))). % 11.76/3.83 tff(c_1915, plain, (![V_768]: (~eventuality(V_768, skc10) | ~accessible_world(skc8, V_768)))). % 11.76/3.83 tff(c_2038, plain, (abstraction(skc12, skc12))). % 11.76/3.83 tff(c_94, plain, (![V_107, W_108, U_106]: (relation(V_107, W_108) | ~relation(U_106, W_108) | ~accessible_world(U_106, V_107)))). % 11.76/3.83 tff(c_2001, plain, (![V_787]: (abstraction(V_787, skc12) | ~accessible_world(skc8, V_787)))). % 11.76/3.83 tff(c_2033, plain, (~abstraction(skc12, skc10))). % 11.76/3.83 tff(c_1914, plain, (![V_768]: (~abstraction(V_768, skc10) | ~accessible_world(skc8, V_768)))). % 11.76/3.83 tff(c_1889, plain, (![V_762]: (animate(V_762, skc10) | ~accessible_world(skc8, V_762)))). % 11.76/3.83 tff(c_2017, plain, (![V_195]: (~abstraction(skc12, skf2(V_195))))). % 11.76/3.83 tff(c_86, plain, (![V_95, W_96, U_94]: (unisex(V_95, W_96) | ~unisex(U_94, W_96) | ~accessible_world(U_94, V_95)))). % 11.76/3.83 tff(c_2019, plain, (~abstraction(skc8, skc13))). % 11.76/3.83 tff(c_1858, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 11.76/3.83 tff(c_1837, plain, (![V_751]: (entity(V_751, skc15) | ~accessible_world(skc8, V_751)))). % 11.76/3.83 tff(c_96, plain, (![V_110, W_111, U_109]: (abstraction(V_110, W_111) | ~abstraction(U_109, W_111) | ~accessible_world(U_109, V_110)))). % 11.76/3.83 tff(c_1839, plain, (![V_751]: (human(V_751, skc15) | ~accessible_world(skc8, V_751)))). % 11.76/3.83 tff(c_1890, plain, (![V_762]: (human(V_762, skc10) | ~accessible_world(skc8, V_762)))). % 11.76/3.83 tff(c_1838, plain, (![V_751]: (animate(V_751, skc15) | ~accessible_world(skc8, V_751)))). % 11.76/3.83 tff(c_1888, plain, (![V_762]: (entity(V_762, skc10) | ~accessible_world(skc8, V_762)))). % 11.76/3.83 tff(c_1971, plain, (~abstraction(skc12, skc15))). % 11.76/3.83 tff(c_84, plain, (![V_92, W_93, U_91]: (nonexistent(V_92, W_93) | ~nonexistent(U_91, W_93) | ~accessible_world(U_91, V_92)))). % 11.76/3.83 tff(c_1926, plain, (![V_769]: (~abstraction(V_769, skc15) | ~accessible_world(skc8, V_769)))). % 11.76/3.83 tff(c_1953, plain, (![V_195]: (~entity(skc12, skf2(V_195))))). % 11.76/3.83 tff(c_1955, plain, (~entity(skc8, skc13))). % 11.76/3.83 tff(c_78, plain, (![V_83, W_84, U_82]: (thing(V_83, W_84) | ~thing(U_82, W_84) | ~accessible_world(U_82, V_83)))). % 11.76/3.83 tff(c_1899, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 11.76/3.83 tff(c_1927, plain, (![V_769]: (~eventuality(V_769, skc15) | ~accessible_world(skc8, V_769)))). % 11.76/3.83 tff(c_1773, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 11.76/3.83 tff(c_1874, plain, (![V_759]: (male(V_759, skc15) | ~accessible_world(skc8, V_759)))). % 11.76/3.83 tff(c_1873, plain, (![V_759]: (male(V_759, skc10) | ~accessible_world(skc8, V_759)))). % 11.76/3.83 tff(c_98, plain, (![V_113, W_114, U_112]: (nonhuman(V_113, W_114) | ~nonhuman(U_112, W_114) | ~accessible_world(U_112, V_113)))). % 11.76/3.83 tff(c_1898, plain, (~entity(skc8, skc9))). % 11.76/3.83 tff(c_335, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 11.76/3.83 tff(c_1794, plain, (![V_737]: (human_person(V_737, skc10) | ~accessible_world(skc8, V_737)))). % 11.76/3.83 tff(c_122, plain, (![V_149, W_150, U_148]: (male(V_149, W_150) | ~male(U_148, W_150) | ~accessible_world(U_148, V_149)))). % 11.76/3.83 tff(c_1867, plain, (abstraction(skc8, skc11))). % 11.76/3.83 tff(c_1866, plain, (abstraction(skc8, skc14))). % 11.76/3.83 tff(c_844, plain, (![U_447, V_448]: (abstraction(U_447, V_448) | ~forename(U_447, V_448)))). % 11.76/3.83 tff(c_1857, plain, (~abstraction(skc8, skc9))). % 11.76/3.83 tff(c_1800, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 11.76/3.83 tff(c_80, plain, (![V_86, W_87, U_85]: (singleton(V_86, W_87) | ~singleton(U_85, W_87) | ~accessible_world(U_85, V_86)))). % 11.76/3.83 tff(c_1795, plain, (![V_737]: (human_person(V_737, skc15) | ~accessible_world(skc8, V_737)))). % 11.76/3.83 tff(c_291, plain, (![U_274, V_275]: (~male(U_274, V_275) | ~abstraction(U_274, V_275)))). % 11.76/3.83 tff(c_1810, plain, (~abstraction(skc8, skc10))). % 11.76/3.83 tff(c_126, plain, (![V_155, W_156, U_154]: (relname(V_155, W_156) | ~relname(U_154, W_156) | ~accessible_world(U_154, V_155)))). % 11.76/3.83 tff(c_1809, plain, (~abstraction(skc8, skc15))). % 11.76/3.83 tff(c_285, plain, (![U_270, V_271]: (~human(U_270, V_271) | ~abstraction(U_270, V_271)))). % 11.76/3.83 tff(c_319, plain, (![U_37, V_38]: (singleton(U_37, V_38) | ~entity(U_37, V_38)))). % 11.76/3.83 tff(c_324, plain, (![U_284, V_285]: (~general(U_284, V_285) | ~eventuality(U_284, V_285)))). % 11.76/3.83 tff(c_1788, plain, (entity(skc8, skc15))). % 11.76/3.83 tff(c_106, plain, (![V_125, W_126, U_124]: (human_person(V_125, W_126) | ~human_person(U_124, W_126) | ~accessible_world(U_124, V_125)))). % 11.76/3.83 tff(c_1787, plain, (entity(skc8, skc10))). % 11.76/3.83 tff(c_248, plain, (![U_33, V_34]: (entity(U_33, V_34) | ~human_person(U_33, V_34)))). % 11.76/3.83 tff(c_1778, plain, (abstraction(skc8, skc12))). % 11.76/3.83 tff(c_186, plain, (![U_196]: (agent(skc12, skf2(U_196), U_196) | ~man(skc12, U_196)))). % 11.76/3.83 tff(c_296, plain, (![U_276, V_277]: (abstraction(U_276, V_277) | ~proposition(U_276, V_277)))). % 11.76/3.83 tff(c_241, plain, (![U_254, V_255]: (~general(U_254, V_255) | ~entity(U_254, V_255)))). % 11.76/3.83 tff(c_236, plain, (![U_33, V_34]: (impartial(U_33, V_34) | ~human_person(U_33, V_34)))). % 11.76/3.83 tff(c_1761, plain, (![V_191]: (smoke(skc12, skf2(V_191))))). % 11.76/3.83 tff(c_317, plain, (![U_19, V_20]: (singleton(U_19, V_20) | ~abstraction(U_19, V_20)))). % 11.76/3.83 tff(c_318, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 11.76/3.83 tff(c_197, plain, (![U_226, V_227]: (living(U_226, V_227) | ~human_person(U_226, V_227)))). % 11.76/3.83 tff(c_1226, plain, (![V_195]: (event(skc12, skf2(V_195))))). % 11.76/3.83 tff(c_231, plain, (![U_53, V_54]: (relation(U_53, V_54) | ~forename(U_53, V_54)))). % 11.76/3.83 tff(c_828, plain, (![V_193]: (present(skc12, skf2(V_193))))). % 11.76/3.83 tff(c_838, plain, (~event(skc8, skc15))). % 11.76/3.83 tff(c_348, plain, (~event(skc8, skc10))). % 11.76/3.83 tff(c_344, plain, (~eventuality(skc8, skc15))). % 11.76/3.83 tff(c_70, plain, (![X_72, W_71, U_69, V_70]: (X_72=W_71 | ~be(U_69, V_70, W_71, X_72)))). % 11.76/3.84 tff(c_343, plain, (~eventuality(skc8, skc10))). % 11.76/3.84 tff(c_301, plain, (![U_278, V_279]: (~male(U_278, V_279) | ~eventuality(U_278, V_279)))). % 11.76/3.84 tff(c_306, plain, (![U_280, V_281]: (~existent(U_280, V_281) | ~eventuality(U_280, V_281)))). % 11.76/3.84 tff(c_330, plain, (event(skc8, skc9))). % 11.76/3.84 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 11.76/3.84 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 11.76/3.84 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 11.76/3.84 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 11.76/3.84 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 11.76/3.84 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 11.76/3.84 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 11.76/3.84 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 11.76/3.84 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 11.76/3.84 tff(c_267, plain, (human(skc8, skc15))). % 11.76/3.84 tff(c_274, plain, (animate(skc8, skc10))). % 11.76/3.84 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 11.76/3.84 tff(c_275, plain, (human(skc8, skc10))). % 11.76/3.84 tff(c_266, plain, (animate(skc8, skc15))). % 11.76/3.84 tff(c_280, plain, (eventuality(skc8, skc9))). % 11.76/3.84 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 11.76/3.84 tff(c_259, plain, (human_person(skc8, skc10))). % 11.76/3.84 tff(c_258, plain, (human_person(skc8, skc15))). % 11.76/3.84 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 11.76/3.84 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 11.76/3.84 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 11.76/3.84 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 11.76/3.84 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 11.76/3.84 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 11.76/3.84 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 11.76/3.84 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 11.76/3.84 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 11.76/3.84 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 11.76/3.84 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 11.76/3.84 tff(c_218, plain, (male(skc8, skc10))). % 11.76/3.84 tff(c_217, plain, (male(skc8, skc15))). % 11.76/3.84 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 11.76/3.84 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 11.76/3.84 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 11.76/3.84 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 11.76/3.84 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 11.76/3.84 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 11.76/3.84 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 11.76/3.84 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 11.76/3.84 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 11.76/3.84 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 11.76/3.84 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 11.76/3.84 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 11.76/3.84 tff(c_178, plain, (be(skc8, skc9, skc10, skc10))). % 11.76/3.84 tff(c_176, plain, (of(skc8, skc11, skc10))). % 11.76/3.84 tff(c_170, plain, (of(skc8, skc14, skc15))). % 11.76/3.84 tff(c_172, plain, (agent(skc8, skc13, skc15))). % 11.76/3.84 tff(c_174, plain, (theme(skc8, skc13, skc12))). % 11.76/3.84 tff(c_146, plain, (man(skc8, skc15))). % 11.76/3.84 tff(c_148, plain, (forename(skc8, skc14))). % 11.76/3.84 tff(c_150, plain, (vincent_forename(skc8, skc14))). % 11.76/3.84 tff(c_168, plain, (proposition(skc8, skc12))). % 11.76/3.84 tff(c_166, plain, (accessible_world(skc8, skc12))). % 11.76/3.84 tff(c_164, plain, (state(skc8, skc9))). % 11.76/3.84 tff(c_162, plain, (man(skc8, skc10))). % 11.76/3.84 tff(c_152, plain, (event(skc8, skc13))). % 11.76/3.84 tff(c_154, plain, (present(skc8, skc13))). % 11.76/3.84 tff(c_156, plain, (think_believe_consider(skc8, skc13))). % 11.76/3.84 tff(c_158, plain, (jules_forename(skc8, skc11))). % 11.76/3.84 tff(c_160, plain, (forename(skc8, skc11))). % 11.76/3.84 tff(c_144, plain, (actual_world(skc8))). % 11.76/3.84 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.76/3.84 %------------------------------------------------------------------------------