%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP250-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 : n003.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:47 PM UTC 2025 % Result : Satisfiable 17.06s 5.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : NLP250-1 : TPTP v9.0.0. Released v2.4.0. % 0.09/0.10 % 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.09/0.30 % Computer : n003.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Tue Apr 8 09:48:18 EDT 2025 % 0.09/0.30 % CPUTime : % 17.06/5.74 % 17.06/5.75 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.06/5.75 % 17.06/5.75 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.06/5.75 %$ 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 % 17.06/5.75 % 17.06/5.75 %Foreground sorts: % 17.06/5.75 % 17.06/5.75 % 17.06/5.75 %Background operators: % 17.06/5.75 % 17.06/5.75 % 17.06/5.75 %Foreground operators: % 17.06/5.75 tff(relation, type, relation: ($i * $i) > $o). % 17.06/5.75 tff(skf4, type, skf4: $i > $i). % 17.06/5.75 tff(forename, type, forename: ($i * $i) > $o). % 17.06/5.75 tff(be, type, be: ($i * $i * $i * $i) > $o). % 17.06/5.75 tff(theme, type, theme: ($i * $i * $i) > $o). % 17.06/5.75 tff(living, type, living: ($i * $i) > $o). % 17.06/5.75 tff(human_person, type, human_person: ($i * $i) > $o). % 17.06/5.75 tff(present, type, present: ($i * $i) > $o). % 17.06/5.75 tff(skc11, type, skc11: $i). % 17.06/5.75 tff(entity, type, entity: ($i * $i) > $o). % 17.06/5.75 tff(skc9, type, skc9: $i). % 17.06/5.75 tff(eventuality, type, eventuality: ($i * $i) > $o). % 17.06/5.75 tff(existent, type, existent: ($i * $i) > $o). % 17.06/5.75 tff(abstraction, type, abstraction: ($i * $i) > $o). % 17.06/5.75 tff(skc8, type, skc8: $i). % 17.06/5.75 tff(proposition, type, proposition: ($i * $i) > $o). % 17.06/5.75 tff(relname, type, relname: ($i * $i) > $o). % 17.06/5.75 tff(skc14, type, skc14: $i). % 17.06/5.75 tff(singleton, type, singleton: ($i * $i) > $o). % 17.06/5.75 tff(skc13, type, skc13: $i). % 17.06/5.75 tff(male, type, male: ($i * $i) > $o). % 17.06/5.75 tff(organism, type, organism: ($i * $i) > $o). % 17.06/5.75 tff(animate, type, animate: ($i * $i) > $o). % 17.06/5.75 tff(of, type, of: ($i * $i * $i) > $o). % 17.06/5.75 tff(actual_world, type, actual_world: $i > $o). % 17.06/5.75 tff(agent, type, agent: ($i * $i * $i) > $o). % 17.06/5.75 tff(jules_forename, type, jules_forename: ($i * $i) > $o). % 17.06/5.75 tff(general, type, general: ($i * $i) > $o). % 17.06/5.75 tff(smoke, type, smoke: ($i * $i) > $o). % 17.06/5.75 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 17.06/5.75 tff(event, type, event: ($i * $i) > $o). % 17.06/5.75 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 17.06/5.75 tff(state, type, state: ($i * $i) > $o). % 17.06/5.75 tff(thing, type, thing: ($i * $i) > $o). % 17.06/5.75 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o). % 17.06/5.75 tff(skc15, type, skc15: $i). % 17.06/5.75 tff(human, type, human: ($i * $i) > $o). % 17.06/5.75 tff(skf2, type, skf2: $i > $i). % 17.06/5.75 tff(man, type, man: ($i * $i) > $o). % 17.06/5.75 tff(unisex, type, unisex: ($i * $i) > $o). % 17.06/5.75 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o). % 17.06/5.75 tff(impartial, type, impartial: ($i * $i) > $o). % 17.06/5.75 tff(skc12, type, skc12: $i). % 17.06/5.75 tff(accessible_world, type, accessible_world: ($i * $i) > $o). % 17.06/5.75 tff(specific, type, specific: ($i * $i) > $o). % 17.06/5.75 tff(skc10, type, skc10: $i). % 17.06/5.75 % 17.06/5.75 %Saturated clause set: % 17.06/5.76 tff(c_5168, plain, (![V_905, U_1559, V_1556]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc10) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~jules_forename(V_905, skc11) | ~state(V_905, skc9) | ~man(V_905, skc10) | ~vincent_forename(V_905, skc11) | ~forename(V_905, skc11) | ~think_believe_consider(V_905, skf2(skc10)) | ~present(V_905, skf2(skc10)) | ~event(V_905, skf2(skc10)) | ~theme(V_905, skf2(skc10), U_1559) | ~proposition(V_905, U_1559) | ~accessible_world(V_905, U_1559) | ~event(U_1559, V_1556) | ~agent(U_1559, V_1556, skf4(U_1559)) | ~present(U_1559, V_1556) | ~smoke(U_1559, V_1556) | ~accessible_world(skc12, V_905) | ~accessible_world(skc8, V_905)))). % 17.06/5.76 tff(c_5137, plain, (![V_923, V_1550, U_196, U_1545, Y_1548]: (~actual_world(V_923) | ~event(V_923, skc13) | ~present(V_923, skc13) | ~think_believe_consider(V_923, skc13) | ~agent(V_923, skc13, skc10) | ~vincent_forename(V_923, skc11) | ~accessible_world(V_923, skc12) | ~proposition(V_923, skc12) | ~forename(V_923, skc11) | ~jules_forename(V_923, skc11) | ~man(V_923, skc10) | ~state(V_923, skc9) | ~man(V_923, U_196) | ~of(V_923, Y_1548, U_196) | ~vincent_forename(V_923, Y_1548) | ~forename(V_923, Y_1548) | ~think_believe_consider(V_923, skf2(U_196)) | ~present(V_923, skf2(U_196)) | ~event(V_923, skf2(U_196)) | ~theme(V_923, skf2(U_196), U_1545) | ~proposition(V_923, U_1545) | ~accessible_world(V_923, U_1545) | ~event(U_1545, V_1550) | ~agent(U_1545, V_1550, skf4(U_1545)) | ~present(U_1545, V_1550) | ~smoke(U_1545, V_1550) | ~accessible_world(skc8, V_923) | ~accessible_world(skc12, V_923) | ~man(skc12, U_196)))). % 17.06/5.76 tff(c_5138, plain, (![V_923, Y_1548, U_1545, V_1550]: (~actual_world(V_923) | ~agent(V_923, skc13, skc10) | ~vincent_forename(V_923, skc11) | ~accessible_world(V_923, skc12) | ~proposition(V_923, skc12) | ~forename(V_923, skc11) | ~jules_forename(V_923, skc11) | ~man(V_923, skc10) | ~state(V_923, skc9) | ~man(V_923, skc15) | ~of(V_923, Y_1548, skc15) | ~vincent_forename(V_923, Y_1548) | ~forename(V_923, Y_1548) | ~think_believe_consider(V_923, skc13) | ~present(V_923, skc13) | ~event(V_923, skc13) | ~theme(V_923, skc13, U_1545) | ~proposition(V_923, U_1545) | ~accessible_world(V_923, U_1545) | ~event(U_1545, V_1550) | ~agent(U_1545, V_1550, skf4(U_1545)) | ~present(U_1545, V_1550) | ~smoke(U_1545, V_1550) | ~accessible_world(skc8, V_923)))). % 17.06/5.76 tff(c_5124, plain, (![V_1544, Z_1538, U_1541, X_1543, Y_1540, V_932]: (~actual_world(V_932) | ~event(V_932, skc13) | ~present(V_932, skc13) | ~think_believe_consider(V_932, skc13) | ~agent(V_932, skc13, skc10) | ~vincent_forename(V_932, skc11) | ~accessible_world(V_932, skc12) | ~proposition(V_932, skc12) | ~forename(V_932, skc11) | ~jules_forename(V_932, skc11) | ~man(V_932, skc10) | ~state(V_932, skc9) | ~agent(V_932, X_1543, Z_1538) | ~man(V_932, Z_1538) | ~of(V_932, Y_1540, Z_1538) | ~vincent_forename(V_932, Y_1540) | ~forename(V_932, Y_1540) | ~think_believe_consider(V_932, X_1543) | ~present(V_932, X_1543) | ~event(V_932, X_1543) | ~theme(V_932, X_1543, U_1541) | ~proposition(V_932, U_1541) | ~accessible_world(V_932, U_1541) | ~event(U_1541, V_1544) | ~agent(U_1541, V_1544, skf4(U_1541)) | ~present(U_1541, V_1544) | ~smoke(U_1541, V_1544) | ~accessible_world(skc8, V_932)))). % 17.06/5.76 tff(c_5111, plain, (![Y_1525, X1_1522, U_1528, V_1527, X_1523, V_905, Z_1529]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc10) | ~vincent_forename(V_905, skc11) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, skc11) | ~jules_forename(V_905, skc11) | ~man(V_905, skc10) | ~be(V_905, X1_1522, skc10, skc10) | ~state(V_905, X1_1522) | ~agent(V_905, X_1523, Z_1529) | ~man(V_905, Z_1529) | ~of(V_905, Y_1525, Z_1529) | ~vincent_forename(V_905, Y_1525) | ~forename(V_905, Y_1525) | ~think_believe_consider(V_905, X_1523) | ~present(V_905, X_1523) | ~event(V_905, X_1523) | ~theme(V_905, X_1523, U_1528) | ~proposition(V_905, U_1528) | ~accessible_world(V_905, U_1528) | ~event(U_1528, V_1527) | ~agent(U_1528, V_1527, skf4(U_1528)) | ~present(U_1528, V_1527) | ~smoke(U_1528, V_1527) | ~accessible_world(skc8, V_905)))). % 17.06/5.76 tff(c_4964, plain, (![X_1507, V_905, Y_1504, Z_1508, V_1506, U_1509, X1_1511]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc15) | ~vincent_forename(V_905, skc14) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, skc14) | ~jules_forename(V_905, skc14) | ~man(V_905, skc15) | ~be(V_905, X1_1511, skc15, skc15) | ~state(V_905, X1_1511) | ~agent(V_905, X_1507, Z_1508) | ~man(V_905, Z_1508) | ~of(V_905, Y_1504, Z_1508) | ~vincent_forename(V_905, Y_1504) | ~forename(V_905, Y_1504) | ~think_believe_consider(V_905, X_1507) | ~present(V_905, X_1507) | ~event(V_905, X_1507) | ~theme(V_905, X_1507, U_1509) | ~proposition(V_905, U_1509) | ~accessible_world(V_905, U_1509) | ~event(U_1509, V_1506) | ~agent(U_1509, V_1506, skf4(U_1509)) | ~present(U_1509, V_1506) | ~smoke(U_1509, V_1506) | ~accessible_world(skc8, V_905)))). % 17.06/5.76 tff(c_4622, plain, (![V_1435, X3_1436, X2_1428, X_1429, U_1432, X1_1433, V_905, Z_1430, Y_1437]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc11) | ~agent(V_905, skc13, skc10) | ~man(V_905, skc10) | ~vincent_forename(V_905, skc11) | ~forename(V_905, skc11) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X3_1436) | ~jules_forename(V_905, X3_1436) | ~of(V_905, X3_1436, X2_1428) | ~man(V_905, X2_1428) | ~be(V_905, X1_1433, X2_1428, X2_1428) | ~state(V_905, X1_1433) | ~agent(V_905, X_1429, Z_1430) | ~man(V_905, Z_1430) | ~of(V_905, Y_1437, Z_1430) | ~vincent_forename(V_905, Y_1437) | ~forename(V_905, Y_1437) | ~think_believe_consider(V_905, X_1429) | ~present(V_905, X_1429) | ~event(V_905, X_1429) | ~theme(V_905, X_1429, U_1432) | ~proposition(V_905, U_1432) | ~accessible_world(V_905, U_1432) | ~event(U_1432, V_1435) | ~agent(U_1432, V_1435, skf4(U_1432)) | ~present(U_1432, V_1435) | ~smoke(U_1432, V_1435) | ~accessible_world(skc8, V_905)))). % 17.06/5.76 tff(c_5096, plain, (![V_846]: (~actual_world(V_846) | ~jules_forename(V_846, skc14) | ~forename(V_846, skc11) | ~jules_forename(V_846, skc11) | ~forename(V_846, skc14) | ~event(V_846, skc13) | ~accessible_world(V_846, skc12) | ~accessible_world(skc8, V_846)))). % 17.06/5.77 tff(c_4824, plain, (![Z_1450, U_1452, X_1449, X1_1453, V_905, V_1455, Y_1457, X2_1448, X3_1456]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc14) | ~agent(V_905, skc13, skc15) | ~man(V_905, skc15) | ~vincent_forename(V_905, skc14) | ~forename(V_905, skc14) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X3_1456) | ~jules_forename(V_905, X3_1456) | ~of(V_905, X3_1456, X2_1448) | ~man(V_905, X2_1448) | ~be(V_905, X1_1453, X2_1448, X2_1448) | ~state(V_905, X1_1453) | ~agent(V_905, X_1449, Z_1450) | ~man(V_905, Z_1450) | ~of(V_905, Y_1457, Z_1450) | ~vincent_forename(V_905, Y_1457) | ~forename(V_905, Y_1457) | ~think_believe_consider(V_905, X_1449) | ~present(V_905, X_1449) | ~event(V_905, X_1449) | ~theme(V_905, X_1449, U_1452) | ~proposition(V_905, U_1452) | ~accessible_world(V_905, U_1452) | ~event(U_1452, V_1455) | ~agent(U_1452, V_1455, skf4(U_1452)) | ~present(U_1452, V_1455) | ~smoke(U_1452, V_1455) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4890, plain, (![V_1470, W_1475, Z_1474, V_905, X_1468, Y_1469]: (man(V_1470, skf4(V_1470)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc15) | ~vincent_forename(V_905, skc14) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, skc14) | ~jules_forename(V_905, skc14) | ~man(V_905, skc15) | ~be(V_905, Z_1474, skc15, skc15) | ~state(V_905, Z_1474) | ~agent(V_905, W_1475, Y_1469) | ~man(V_905, Y_1469) | ~of(V_905, X_1468, Y_1469) | ~vincent_forename(V_905, X_1468) | ~forename(V_905, X_1468) | ~think_believe_consider(V_905, W_1475) | ~present(V_905, W_1475) | ~event(V_905, W_1475) | ~theme(V_905, W_1475, V_1470) | ~proposition(V_905, V_1470) | ~accessible_world(V_905, V_1470) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4664, plain, (![V_1441, V_905]: (man(V_1441, skf4(V_1441)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc10) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~jules_forename(V_905, skc11) | ~state(V_905, skc9) | ~man(V_905, skc10) | ~vincent_forename(V_905, skc11) | ~forename(V_905, skc11) | ~think_believe_consider(V_905, skf2(skc10)) | ~present(V_905, skf2(skc10)) | ~event(V_905, skf2(skc10)) | ~theme(V_905, skf2(skc10), V_1441) | ~proposition(V_905, V_1441) | ~accessible_world(V_905, V_1441) | ~accessible_world(skc12, V_905) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4843, plain, (![V_143, V_1458]: (human(V_143, skc10) | ~accessible_world(V_1458, V_143) | ~accessible_world(skc12, V_1458)))). % 17.06/5.77 tff(c_4848, plain, (![V_146, V_1459]: (animate(V_146, skc10) | ~accessible_world(V_1459, V_146) | ~accessible_world(skc12, V_1459)))). % 17.06/5.77 tff(c_4415, plain, (![W_1408, Z_1407, X2_1411, X1_1410, V_905, X_1414, V_1406, Y_1413]: (man(V_1406, skf4(V_1406)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc14) | ~agent(V_905, skc13, skc15) | ~man(V_905, skc15) | ~vincent_forename(V_905, skc14) | ~forename(V_905, skc14) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X2_1411) | ~jules_forename(V_905, X2_1411) | ~of(V_905, X2_1411, X1_1410) | ~man(V_905, X1_1410) | ~be(V_905, Z_1407, X1_1410, X1_1410) | ~state(V_905, Z_1407) | ~agent(V_905, W_1408, Y_1413) | ~man(V_905, Y_1413) | ~of(V_905, X_1414, Y_1413) | ~vincent_forename(V_905, X_1414) | ~forename(V_905, X_1414) | ~think_believe_consider(V_905, W_1408) | ~present(V_905, W_1408) | ~event(V_905, W_1408) | ~theme(V_905, W_1408, V_1406) | ~proposition(V_905, V_1406) | ~accessible_world(V_905, V_1406) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4816, plain, (![V_149, V_1447]: (male(V_149, skc10) | ~accessible_world(V_1447, V_149) | ~accessible_world(skc12, V_1447)))). % 17.06/5.77 tff(c_4785, plain, (![V_125, V_1446]: (human_person(V_125, skc10) | ~accessible_world(V_1446, V_125) | ~accessible_world(skc12, V_1446)))). % 17.06/5.77 tff(c_4760, plain, (![V_122, V_1445]: (man(V_122, skc10) | ~accessible_world(V_1445, V_122) | ~accessible_world(skc12, V_1445)))). % 17.06/5.77 tff(c_4864, plain, (![U_3]: (~accessible_world(skc12, U_3) | ~event(U_3, skc10)))). % 17.06/5.77 tff(c_4818, plain, (![V_1447]: (~eventuality(V_1447, skc10) | ~accessible_world(skc12, V_1447)))). % 17.06/5.77 tff(c_4723, plain, (![V_146]: (animate(V_146, skc10) | ~accessible_world(skc12, V_146)))). % 17.06/5.77 tff(c_4788, plain, (![V_1446]: (human(V_1446, skc10) | ~accessible_world(skc12, V_1446)))). % 17.06/5.77 tff(c_4720, plain, (![X1_1363, X3_1368, V_1371, X_1365, V_905, U_1369, X2_1373, X5_1364, Y_1372, Z_1374]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc14) | ~forename(V_905, skc14) | ~agent(V_905, skc13, skc15) | ~man(V_905, skc15) | ~of(V_905, X5_1364, skc15) | ~vincent_forename(V_905, X5_1364) | ~forename(V_905, X5_1364) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X3_1368) | ~jules_forename(V_905, X3_1368) | ~of(V_905, X3_1368, X2_1373) | ~man(V_905, X2_1373) | ~be(V_905, X1_1363, X2_1373, X2_1373) | ~state(V_905, X1_1363) | ~agent(V_905, X_1365, Z_1374) | ~man(V_905, Z_1374) | ~of(V_905, Y_1372, Z_1374) | ~vincent_forename(V_905, Y_1372) | ~forename(V_905, Y_1372) | ~think_believe_consider(V_905, X_1365) | ~present(V_905, X_1365) | ~event(V_905, X_1365) | ~theme(V_905, X_1365, U_1369) | ~proposition(V_905, U_1369) | ~accessible_world(V_905, U_1369) | ~event(U_1369, V_1371) | ~agent(U_1369, V_1371, skf4(U_1369)) | ~present(U_1369, V_1371) | ~smoke(U_1369, V_1371) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4717, plain, (![V_149]: (male(V_149, skc10) | ~accessible_world(skc12, V_149)))). % 17.06/5.77 tff(c_4688, plain, (![V_125]: (human_person(V_125, skc10) | ~accessible_world(skc12, V_125)))). % 17.06/5.77 tff(c_4674, plain, (![V_122]: (man(V_122, skc10) | ~accessible_world(skc12, V_122)))). % 17.06/5.77 tff(c_4735, plain, (~event(skc12, skc10))). % 17.06/5.77 tff(c_4692, plain, (human(skc12, skc10))). % 17.06/5.77 tff(c_4719, plain, (~eventuality(skc12, skc10))). % 17.06/5.77 tff(c_4691, plain, (animate(skc12, skc10))). % 17.06/5.77 tff(c_4676, plain, (male(skc12, skc10))). % 17.06/5.77 tff(c_4675, plain, (human_person(skc12, skc10))). % 17.06/5.77 tff(c_4665, plain, (man(skc12, skc10))). % 17.06/5.77 tff(c_4402, plain, (![V_1401, V_923, U_196, X_1404]: (man(V_1401, skf4(V_1401)) | ~actual_world(V_923) | ~event(V_923, skc13) | ~present(V_923, skc13) | ~think_believe_consider(V_923, skc13) | ~agent(V_923, skc13, skc10) | ~vincent_forename(V_923, skc11) | ~accessible_world(V_923, skc12) | ~proposition(V_923, skc12) | ~forename(V_923, skc11) | ~jules_forename(V_923, skc11) | ~man(V_923, skc10) | ~state(V_923, skc9) | ~man(V_923, U_196) | ~of(V_923, X_1404, U_196) | ~vincent_forename(V_923, X_1404) | ~forename(V_923, X_1404) | ~think_believe_consider(V_923, skf2(U_196)) | ~present(V_923, skf2(U_196)) | ~event(V_923, skf2(U_196)) | ~theme(V_923, skf2(U_196), V_1401) | ~proposition(V_923, V_1401) | ~accessible_world(V_923, V_1401) | ~accessible_world(skc8, V_923) | ~accessible_world(skc12, V_923) | ~man(skc12, U_196)))). % 17.06/5.77 tff(c_4635, plain, (![V_912]: (~actual_world(V_912) | ~agent(V_912, skc13, skc10) | ~vincent_forename(V_912, skc11) | ~forename(V_912, skc11) | ~jules_forename(V_912, skc11) | ~man(V_912, skc10) | ~state(V_912, skc9) | ~man(V_912, skc15) | ~vincent_forename(V_912, skc14) | ~forename(V_912, skc14) | ~think_believe_consider(V_912, skc13) | ~present(V_912, skc13) | ~event(V_912, skc13) | ~proposition(V_912, skc12) | ~accessible_world(V_912, skc12) | ~accessible_world(skc8, V_912)))). % 17.06/5.77 tff(c_4590, plain, (![X1_1363, X3_1368, V_1371, X_1365, V_905, U_1369, X2_1373, X5_1364, Y_1372, Z_1374]: (~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc11) | ~forename(V_905, skc11) | ~agent(V_905, skc13, skc10) | ~man(V_905, skc10) | ~of(V_905, X5_1364, skc10) | ~vincent_forename(V_905, X5_1364) | ~forename(V_905, X5_1364) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X3_1368) | ~jules_forename(V_905, X3_1368) | ~of(V_905, X3_1368, X2_1373) | ~man(V_905, X2_1373) | ~be(V_905, X1_1363, X2_1373, X2_1373) | ~state(V_905, X1_1363) | ~agent(V_905, X_1365, Z_1374) | ~man(V_905, Z_1374) | ~of(V_905, Y_1372, Z_1374) | ~vincent_forename(V_905, Y_1372) | ~forename(V_905, Y_1372) | ~think_believe_consider(V_905, X_1365) | ~present(V_905, X_1365) | ~event(V_905, X_1365) | ~theme(V_905, X_1365, U_1369) | ~proposition(V_905, U_1369) | ~accessible_world(V_905, U_1369) | ~event(U_1369, V_1371) | ~agent(U_1369, V_1371, skf4(U_1369)) | ~present(U_1369, V_1371) | ~smoke(U_1369, V_1371) | ~accessible_world(skc8, V_905)))). % 17.06/5.77 tff(c_4403, plain, (![V_1401, V_923, X_1404]: (man(V_1401, skf4(V_1401)) | ~actual_world(V_923) | ~agent(V_923, skc13, skc10) | ~vincent_forename(V_923, skc11) | ~accessible_world(V_923, skc12) | ~proposition(V_923, skc12) | ~forename(V_923, skc11) | ~jules_forename(V_923, skc11) | ~man(V_923, skc10) | ~state(V_923, skc9) | ~man(V_923, skc15) | ~of(V_923, X_1404, skc15) | ~vincent_forename(V_923, X_1404) | ~forename(V_923, X_1404) | ~think_believe_consider(V_923, skc13) | ~present(V_923, skc13) | ~event(V_923, skc13) | ~theme(V_923, skc13, V_1401) | ~proposition(V_923, V_1401) | ~accessible_world(V_923, V_1401) | ~accessible_world(skc8, V_923)))). % 17.06/5.77 tff(c_4607, plain, (~actual_world(skc12))). % 17.06/5.77 tff(c_4587, plain, (![V_80, V_1417]: (eventuality(V_80, skc9) | ~accessible_world(V_1417, V_80) | ~accessible_world(skc12, V_1417)))). % 17.06/5.77 tff(c_4543, plain, (![V_77, V_1416]: (event(V_77, skc9) | ~accessible_world(V_1416, V_77) | ~accessible_world(skc12, V_1416)))). % 17.06/5.77 tff(c_4503, plain, (![V_119, V_1415]: (state(V_119, skc9) | ~accessible_world(V_1415, V_119) | ~accessible_world(skc12, V_1415)))). % 17.06/5.77 tff(c_4589, plain, (![V_1417]: (~abstraction(V_1417, skc9) | ~accessible_world(skc12, V_1417)))). % 17.06/5.77 tff(c_4491, plain, (![V_80]: (eventuality(V_80, skc9) | ~accessible_world(skc12, V_80)))). % 17.06/5.77 tff(c_4464, plain, (![V_77]: (event(V_77, skc9) | ~accessible_world(skc12, V_77)))). % 17.06/5.77 tff(c_4437, plain, (![V_119]: (state(V_119, skc9) | ~accessible_world(skc12, V_119)))). % 17.06/5.77 tff(c_4439, plain, (eventuality(skc12, skc9))). % 17.06/5.77 tff(c_4438, plain, (event(skc12, skc9))). % 17.06/5.77 tff(c_4428, plain, (state(skc12, skc9))). % 17.06/5.78 tff(c_4357, plain, (![V_1352, W_1345, X2_1346, Y_1351, X4_1342, V_905, Z_1349, X_1353, X1_1344]: (man(V_1352, skf4(V_1352)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc14) | ~forename(V_905, skc14) | ~agent(V_905, skc13, skc15) | ~man(V_905, skc15) | ~of(V_905, X4_1342, skc15) | ~vincent_forename(V_905, X4_1342) | ~forename(V_905, X4_1342) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X2_1346) | ~jules_forename(V_905, X2_1346) | ~of(V_905, X2_1346, X1_1344) | ~man(V_905, X1_1344) | ~be(V_905, Z_1349, X1_1344, X1_1344) | ~state(V_905, Z_1349) | ~agent(V_905, W_1345, Y_1351) | ~man(V_905, Y_1351) | ~of(V_905, X_1353, Y_1351) | ~vincent_forename(V_905, X_1353) | ~forename(V_905, X_1353) | ~think_believe_consider(V_905, W_1345) | ~present(V_905, W_1345) | ~event(V_905, W_1345) | ~theme(V_905, W_1345, V_1352) | ~proposition(V_905, V_1352) | ~accessible_world(V_905, V_1352) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_4389, plain, (![W_1395, Y_1396, X_1398, V_932, V_1400]: (man(V_1400, skf4(V_1400)) | ~actual_world(V_932) | ~event(V_932, skc13) | ~present(V_932, skc13) | ~think_believe_consider(V_932, skc13) | ~agent(V_932, skc13, skc10) | ~vincent_forename(V_932, skc11) | ~accessible_world(V_932, skc12) | ~proposition(V_932, skc12) | ~forename(V_932, skc11) | ~jules_forename(V_932, skc11) | ~man(V_932, skc10) | ~state(V_932, skc9) | ~agent(V_932, W_1395, Y_1396) | ~man(V_932, Y_1396) | ~of(V_932, X_1398, Y_1396) | ~vincent_forename(V_932, X_1398) | ~forename(V_932, X_1398) | ~think_believe_consider(V_932, W_1395) | ~present(V_932, W_1395) | ~event(V_932, W_1395) | ~theme(V_932, W_1395, V_1400) | ~proposition(V_932, V_1400) | ~accessible_world(V_932, V_1400) | ~accessible_world(skc8, V_932)))). % 17.06/5.78 tff(c_4377, plain, (![Z_1389, X_1390, W_1388, V_905, Y_1387, V_1391]: (man(V_1391, skf4(V_1391)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~agent(V_905, skc13, skc10) | ~vincent_forename(V_905, skc11) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, skc11) | ~jules_forename(V_905, skc11) | ~man(V_905, skc10) | ~be(V_905, Z_1389, skc10, skc10) | ~state(V_905, Z_1389) | ~agent(V_905, W_1388, Y_1387) | ~man(V_905, Y_1387) | ~of(V_905, X_1390, Y_1387) | ~vincent_forename(V_905, X_1390) | ~forename(V_905, X_1390) | ~think_believe_consider(V_905, W_1388) | ~present(V_905, W_1388) | ~event(V_905, W_1388) | ~theme(V_905, W_1388, V_1391) | ~proposition(V_905, V_1391) | ~accessible_world(V_905, V_1391) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_4363, plain, (![W_1380, V_1378, Y_1385, V_905, X2_1383, Z_1379, X1_1382, X_1386]: (man(V_1378, skf4(V_1378)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc11) | ~agent(V_905, skc13, skc10) | ~man(V_905, skc10) | ~vincent_forename(V_905, skc11) | ~forename(V_905, skc11) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X2_1383) | ~jules_forename(V_905, X2_1383) | ~of(V_905, X2_1383, X1_1382) | ~man(V_905, X1_1382) | ~be(V_905, Z_1379, X1_1382, X1_1382) | ~state(V_905, Z_1379) | ~agent(V_905, W_1380, Y_1385) | ~man(V_905, Y_1385) | ~of(V_905, X_1386, Y_1385) | ~vincent_forename(V_905, X_1386) | ~forename(V_905, X_1386) | ~think_believe_consider(V_905, W_1380) | ~present(V_905, W_1380) | ~event(V_905, W_1380) | ~theme(V_905, W_1380, V_1378) | ~proposition(V_905, V_1378) | ~accessible_world(V_905, V_1378) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_4332, plain, (![V_1352, W_1345, X2_1346, Y_1351, X4_1342, V_905, Z_1349, X_1353, X1_1344]: (man(V_1352, skf4(V_1352)) | ~actual_world(V_905) | ~event(V_905, skc13) | ~present(V_905, skc13) | ~think_believe_consider(V_905, skc13) | ~jules_forename(V_905, skc11) | ~forename(V_905, skc11) | ~agent(V_905, skc13, skc10) | ~man(V_905, skc10) | ~of(V_905, X4_1342, skc10) | ~vincent_forename(V_905, X4_1342) | ~forename(V_905, X4_1342) | ~accessible_world(V_905, skc12) | ~proposition(V_905, skc12) | ~forename(V_905, X2_1346) | ~jules_forename(V_905, X2_1346) | ~of(V_905, X2_1346, X1_1344) | ~man(V_905, X1_1344) | ~be(V_905, Z_1349, X1_1344, X1_1344) | ~state(V_905, Z_1349) | ~agent(V_905, W_1345, Y_1351) | ~man(V_905, Y_1351) | ~of(V_905, X_1353, Y_1351) | ~vincent_forename(V_905, X_1353) | ~forename(V_905, X_1353) | ~think_believe_consider(V_905, W_1345) | ~present(V_905, W_1345) | ~event(V_905, W_1345) | ~theme(V_905, W_1345, V_1352) | ~proposition(V_905, V_1352) | ~accessible_world(V_905, V_1352) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_2644, plain, (![Z_981, X1_987, Y_985, X3_984, V_988, V_912, X2_990, X6_992, X5_983, U_982, X8_989, X_993, X9_986]: (~actual_world(V_912) | ~event(V_912, skc13) | ~present(V_912, skc13) | ~think_believe_consider(V_912, skc13) | ~of(V_912, X9_986, X6_992) | ~jules_forename(V_912, X9_986) | ~forename(V_912, X9_986) | ~event(skc12, X8_989) | ~agent(skc12, X8_989, X6_992) | ~present(skc12, X8_989) | ~smoke(skc12, X8_989) | ~agent(V_912, skc13, X6_992) | ~man(V_912, X6_992) | ~of(V_912, X5_983, X6_992) | ~vincent_forename(V_912, X5_983) | ~forename(V_912, X5_983) | ~accessible_world(V_912, skc12) | ~proposition(V_912, skc12) | ~forename(V_912, X3_984) | ~jules_forename(V_912, X3_984) | ~of(V_912, X3_984, X2_990) | ~man(V_912, X2_990) | ~be(V_912, X1_987, X2_990, X2_990) | ~state(V_912, X1_987) | ~agent(V_912, X_993, Z_981) | ~man(V_912, Z_981) | ~of(V_912, Y_985, Z_981) | ~vincent_forename(V_912, Y_985) | ~forename(V_912, Y_985) | ~think_believe_consider(V_912, X_993) | ~present(V_912, X_993) | ~event(V_912, X_993) | ~theme(V_912, X_993, U_982) | ~proposition(V_912, U_982) | ~accessible_world(V_912, U_982) | ~event(U_982, V_988) | ~agent(U_982, V_988, skf4(U_982)) | ~present(U_982, V_988) | ~smoke(U_982, V_988) | ~accessible_world(skc8, V_912)))). % 17.06/5.78 tff(c_4287, plain, (![V_1359, V_912]: (skc12=V_1359 | ~think_believe_consider(V_912, skc13) | ~think_believe_consider(V_912, skf2(skc15)) | ~theme(V_912, skf2(skc15), V_1359) | ~proposition(V_912, skc12) | ~proposition(V_912, V_1359) | ~accessible_world(skc12, V_912) | ~accessible_world(skc8, V_912)))). % 17.06/5.78 tff(c_4258, plain, (![W_1340, V_1338, V_923]: (W_1340=V_1338 | ~theme(V_923, skc13, W_1340) | ~think_believe_consider(V_923, skc13) | ~think_believe_consider(V_923, skf2(skc15)) | ~theme(V_923, skf2(skc15), V_1338) | ~proposition(V_923, W_1340) | ~proposition(V_923, V_1338) | ~accessible_world(skc12, V_923) | ~accessible_world(skc8, V_923)))). % 17.06/5.78 tff(c_4255, plain, (![W_1340, V_1338, V_923, U_196]: (W_1340=V_1338 | ~theme(V_923, skf2(U_196), W_1340) | ~think_believe_consider(V_923, skf2(U_196)) | ~theme(V_923, skf2(U_196), V_1338) | ~proposition(V_923, W_1340) | ~proposition(V_923, V_1338) | ~accessible_world(skc12, V_923) | ~man(skc12, U_196)))). % 17.06/5.78 tff(c_4280, plain, (~accessible_world(skc12, skc8))). % 17.06/5.78 tff(c_2606, plain, (![X4_964, X_962, Y_966, V_912, X1_970, X7_961, X8_963, X5_965, V_971, W_968, Z_960, X2_973]: (man(V_971, skf4(V_971)) | ~actual_world(V_912) | ~event(V_912, skc13) | ~present(V_912, skc13) | ~think_believe_consider(V_912, skc13) | ~of(V_912, X8_963, X5_965) | ~jules_forename(V_912, X8_963) | ~forename(V_912, X8_963) | ~event(skc12, X7_961) | ~agent(skc12, X7_961, X5_965) | ~present(skc12, X7_961) | ~smoke(skc12, X7_961) | ~agent(V_912, skc13, X5_965) | ~man(V_912, X5_965) | ~of(V_912, X4_964, X5_965) | ~vincent_forename(V_912, X4_964) | ~forename(V_912, X4_964) | ~accessible_world(V_912, skc12) | ~proposition(V_912, skc12) | ~forename(V_912, X2_973) | ~jules_forename(V_912, X2_973) | ~of(V_912, X2_973, X1_970) | ~man(V_912, X1_970) | ~be(V_912, Z_960, X1_970, X1_970) | ~state(V_912, Z_960) | ~agent(V_912, W_968, Y_966) | ~man(V_912, Y_966) | ~of(V_912, X_962, Y_966) | ~vincent_forename(V_912, X_962) | ~forename(V_912, X_962) | ~think_believe_consider(V_912, W_968) | ~present(V_912, W_968) | ~event(V_912, W_968) | ~theme(V_912, W_968, V_971) | ~proposition(V_912, V_971) | ~accessible_world(V_912, V_971) | ~accessible_world(skc8, V_912)))). % 17.06/5.78 tff(c_3061, plain, (![V_1052, V_189, Y_188, U_1053, W_184]: (W_184=V_189 | ~agent(V_1052, Y_188, U_1053) | ~theme(V_1052, Y_188, W_184) | ~think_believe_consider(V_1052, Y_188) | ~think_believe_consider(V_1052, skf2(U_1053)) | ~theme(V_1052, skf2(U_1053), V_189) | ~proposition(V_1052, W_184) | ~proposition(V_1052, V_189) | ~accessible_world(skc12, V_1052) | ~man(skc12, U_1053)))). % 17.06/5.78 tff(c_4245, plain, (~agent(skc8, skc13, skc10))). % 17.06/5.78 tff(c_4179, plain, (![V_146, V_1321]: (animate(V_146, skc15) | ~accessible_world(V_1321, V_146) | ~accessible_world(skc12, V_1321)))). % 17.06/5.78 tff(c_4211, plain, (![V_143, V_1323]: (human(V_143, skc15) | ~accessible_world(V_1323, V_143) | ~accessible_world(skc12, V_1323)))). % 17.06/5.78 tff(c_4155, plain, (![V_125, V_1319]: (human_person(V_125, skc15) | ~accessible_world(V_1319, V_125) | ~accessible_world(skc12, V_1319)))). % 17.06/5.78 tff(c_4130, plain, (![V_149, V_1318]: (male(V_149, skc15) | ~accessible_world(V_1318, V_149) | ~accessible_world(skc12, V_1318)))). % 17.06/5.78 tff(c_4175, plain, (![V_101, V_1320]: (think_believe_consider(V_101, skc13) | ~accessible_world(V_1320, V_101) | ~accessible_world(skc12, V_1320)))). % 17.06/5.78 tff(c_4100, plain, (![V_122, V_1317]: (man(V_122, skc15) | ~accessible_world(V_1317, V_122) | ~accessible_world(skc12, V_1317)))). % 17.06/5.78 tff(c_4195, plain, (![U_3]: (~accessible_world(skc12, U_3) | ~event(U_3, skc15)))). % 17.06/5.78 tff(c_4213, plain, (~think_believe_consider(skc12, skf2(skc15)))). % 17.06/5.78 tff(c_4077, plain, (![V_143]: (human(V_143, skc15) | ~accessible_world(skc12, V_143)))). % 17.06/5.78 tff(c_4132, plain, (![V_1318]: (~eventuality(V_1318, skc15) | ~accessible_world(skc12, V_1318)))). % 17.06/5.78 tff(c_4157, plain, (![V_1319]: (animate(V_1319, skc15) | ~accessible_world(skc12, V_1319)))). % 17.06/5.78 tff(c_4171, plain, (![V_101]: (think_believe_consider(V_101, skc13) | ~accessible_world(skc12, V_101)))). % 17.06/5.78 tff(c_4168, plain, (think_believe_consider(skc12, skc13))). % 17.06/5.78 tff(c_4029, plain, (![V_125]: (human_person(V_125, skc15) | ~accessible_world(skc12, V_125)))). % 17.06/5.78 tff(c_4058, plain, (![V_149]: (male(V_149, skc15) | ~accessible_world(skc12, V_149)))). % 17.06/5.78 tff(c_4015, plain, (![V_122]: (man(V_122, skc15) | ~accessible_world(skc12, V_122)))). % 17.06/5.78 tff(c_4090, plain, (~event(skc12, skc15))). % 17.06/5.78 tff(c_4060, plain, (~eventuality(skc12, skc15))). % 17.06/5.78 tff(c_4033, plain, (human(skc12, skc15))). % 17.06/5.78 tff(c_4032, plain, (animate(skc12, skc15))). % 17.06/5.78 tff(c_4017, plain, (male(skc12, skc15))). % 17.06/5.78 tff(c_4016, plain, (human_person(skc12, skc15))). % 17.06/5.78 tff(c_4006, plain, (man(skc12, skc15))). % 17.06/5.78 tff(c_3996, plain, (~jules_forename(skc8, skc14))). % 17.06/5.78 tff(c_3980, plain, (![V_1312, V_912]: (skc12=V_1312 | ~agent(V_912, skc13, skc15) | ~think_believe_consider(V_912, skc13) | ~theme(V_912, skc13, V_1312) | ~proposition(V_912, skc12) | ~proposition(V_912, V_1312) | ~accessible_world(skc8, V_912)))). % 17.06/5.78 tff(c_2530, plain, (![W_949, V_947, V_923, Y_948]: (W_949=V_947 | ~agent(V_923, Y_948, skc15) | ~theme(V_923, Y_948, W_949) | ~think_believe_consider(V_923, Y_948) | ~think_believe_consider(V_923, skc13) | ~theme(V_923, skc13, V_947) | ~proposition(V_923, W_949) | ~proposition(V_923, V_947) | ~accessible_world(skc8, V_923)))). % 17.06/5.78 tff(c_3199, plain, (![W_1087, V_1088, U_196]: (W_1087=V_1088 | ~theme(skc12, skf2(U_196), W_1087) | ~think_believe_consider(skc12, skf2(U_196)) | ~theme(skc12, skf2(U_196), V_1088) | ~proposition(skc12, W_1087) | ~proposition(skc12, V_1088) | ~man(skc12, U_196)))). % 17.06/5.78 tff(c_3618, plain, (![V_86, V_1179, V_1178]: (singleton(V_86, V_1179) | ~accessible_world(V_1178, V_86) | ~accessible_world(skc12, V_1178) | ~abstraction(skc8, V_1179)))). % 17.06/5.78 tff(c_3643, plain, (![V_137, V_1183, V_1182]: (impartial(V_137, V_1183) | ~accessible_world(V_1182, V_137) | ~accessible_world(skc12, V_1182) | ~human_person(skc8, V_1183)))). % 17.06/5.78 tff(c_2499, plain, (![W_936, V_905]: (skc14=W_936 | ~entity(V_905, skc15) | ~forename(V_905, W_936) | ~of(V_905, W_936, skc15) | ~forename(V_905, skc14) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_3606, plain, (![V_140, V_1175, V_1174]: (living(V_140, V_1175) | ~accessible_world(V_1174, V_140) | ~accessible_world(skc12, V_1174) | ~human_person(skc8, V_1175)))). % 17.06/5.78 tff(c_3613, plain, (![V_107, V_1177, V_1176]: (relation(V_107, V_1177) | ~accessible_world(V_1176, V_107) | ~accessible_world(skc12, V_1176) | ~forename(skc8, V_1177)))). % 17.06/5.78 tff(c_3542, plain, (![V_86, V_1163, V_1162]: (singleton(V_86, V_1163) | ~accessible_world(V_1162, V_86) | ~accessible_world(skc12, V_1162) | ~eventuality(skc8, V_1163)))). % 17.06/5.78 tff(c_3686, plain, (![V_86, V_1192, V_1191]: (singleton(V_86, V_1192) | ~accessible_world(V_1191, V_86) | ~accessible_world(skc12, V_1191) | ~entity(skc8, V_1192)))). % 17.06/5.78 tff(c_3405, plain, (![V_134, V_1147, V_1146]: (existent(V_134, V_1147) | ~accessible_world(V_1146, V_134) | ~accessible_world(skc12, V_1146) | ~entity(skc8, V_1147)))). % 17.06/5.78 tff(c_3287, plain, (![V_83, V_1119, V_1118]: (thing(V_83, V_1119) | ~accessible_world(V_1118, V_83) | ~accessible_world(skc12, V_1118) | ~entity(skc8, V_1119)))). % 17.06/5.78 tff(c_3315, plain, (![V_155, V_1127, V_1126]: (relname(V_155, V_1127) | ~accessible_world(V_1126, V_155) | ~accessible_world(skc12, V_1126) | ~forename(skc8, V_1127)))). % 17.06/5.78 tff(c_3450, plain, (![V_80, V_1149, V_1148]: (eventuality(V_80, V_1149) | ~accessible_world(V_1148, V_80) | ~accessible_world(skc12, V_1148) | ~event(skc8, V_1149)))). % 17.06/5.78 tff(c_3259, plain, (![V_92, V_1113, V_1112]: (nonexistent(V_92, V_1113) | ~accessible_world(V_1112, V_92) | ~accessible_world(skc12, V_1112) | ~eventuality(skc8, V_1113)))). % 17.06/5.78 tff(c_2500, plain, (![W_936, V_905]: (skc11=W_936 | ~entity(V_905, skc10) | ~forename(V_905, W_936) | ~of(V_905, W_936, skc10) | ~forename(V_905, skc11) | ~accessible_world(skc8, V_905)))). % 17.06/5.78 tff(c_3242, plain, (![V_113, V_1109, V_1108]: (nonhuman(V_113, V_1109) | ~accessible_world(V_1108, V_113) | ~accessible_world(skc12, V_1108) | ~abstraction(skc8, V_1109)))). % 17.06/5.78 tff(c_3307, plain, (![V_95, V_1125, V_1124]: (unisex(V_95, V_1125) | ~accessible_world(V_1124, V_95) | ~accessible_world(skc12, V_1124) | ~eventuality(skc8, V_1125)))). % 17.06/5.78 tff(c_3350, plain, (![V_89, V_1135, V_1134]: (specific(V_89, V_1135) | ~accessible_world(V_1134, V_89) | ~accessible_world(skc12, V_1134) | ~eventuality(skc8, V_1135)))). % 17.06/5.78 tff(c_3273, plain, (![V_128, V_1115, V_1114]: (organism(V_128, V_1115) | ~accessible_world(V_1114, V_128) | ~accessible_world(skc12, V_1114) | ~human_person(skc8, V_1115)))). % 17.06/5.78 tff(c_3463, plain, (![V_107, V_1151, V_1150]: (relation(V_107, V_1151) | ~accessible_world(V_1150, V_107) | ~accessible_world(skc12, V_1150) | ~proposition(skc8, V_1151)))). % 17.06/5.78 tff(c_3299, plain, (![V_83, V_1123, V_1122]: (thing(V_83, V_1123) | ~accessible_world(V_1122, V_83) | ~accessible_world(skc12, V_1122) | ~abstraction(skc8, V_1123)))). % 17.06/5.78 tff(c_3251, plain, (![V_89, V_1111, V_1110]: (specific(V_89, V_1111) | ~accessible_world(V_1110, V_89) | ~accessible_world(skc12, V_1110) | ~entity(skc8, V_1111)))). % 17.06/5.78 tff(c_3387, plain, (![V_116, V_1143, V_1142]: (general(V_116, V_1143) | ~accessible_world(V_1142, V_116) | ~accessible_world(skc12, V_1142) | ~abstraction(skc8, V_1143)))). % 17.06/5.78 tff(c_3358, plain, (![V_95, V_1137, V_1136]: (unisex(V_95, V_1137) | ~accessible_world(V_1136, V_95) | ~accessible_world(skc12, V_1136) | ~abstraction(skc8, V_1137)))). % 17.06/5.79 tff(c_3062, plain, (![V_164, U_1053, V_1052]: (agent(V_164, skf2(U_1053), U_1053) | ~accessible_world(V_1052, V_164) | ~accessible_world(skc12, V_1052) | ~man(skc12, U_1053)))). % 17.06/5.79 tff(c_3226, plain, (![V_83, V_1103, V_1102]: (thing(V_83, V_1103) | ~accessible_world(V_1102, V_83) | ~accessible_world(skc12, V_1102) | ~eventuality(skc8, V_1103)))). % 17.06/5.79 tff(c_2487, plain, (![V_179, V_935]: (be(V_179, skc9, skc10, skc10) | ~accessible_world(V_935, V_179) | ~accessible_world(skc8, V_935)))). % 17.06/5.79 tff(c_2396, plain, (![V_172, V_911]: (of(V_172, skc11, skc10) | ~accessible_world(V_911, V_172) | ~accessible_world(skc8, V_911)))). % 17.06/5.79 tff(c_2408, plain, (![V_168, V_917]: (theme(V_168, skc13, skc12) | ~accessible_world(V_917, V_168) | ~accessible_world(skc8, V_917)))). % 17.06/5.79 tff(c_2969, plain, (![V_131, V_1033]: (entity(V_131, skc15) | ~accessible_world(V_1033, V_131) | ~accessible_world(skc12, V_1033)))). % 17.06/5.79 tff(c_2987, plain, (![V_131, V_1034]: (entity(V_131, skc10) | ~accessible_world(V_1034, V_131) | ~accessible_world(skc12, V_1034)))). % 17.06/5.79 tff(c_3837, plain, (![U_1225]: (~accessible_world(skc12, U_1225) | ~entity(U_1225, skc9)))). % 17.06/5.79 tff(c_3764, plain, (![U_41, V_42]: (~accessible_world(skc12, U_41) | ~eventuality(skc8, V_42) | ~entity(U_41, V_42)))). % 17.06/5.79 tff(c_3720, plain, (![U_23, V_24]: (~accessible_world(skc12, U_23) | ~entity(skc8, V_24) | ~abstraction(U_23, V_24)))). % 17.06/5.79 tff(c_2276, plain, (![V_98, V_872, V_871]: (present(V_98, skf2(V_872)) | ~accessible_world(V_871, V_98) | ~accessible_world(skc12, V_871)))). % 17.06/5.79 tff(c_3639, plain, (![U_3, V_4]: (~accessible_world(skc12, U_3) | ~entity(skc8, V_4) | ~event(U_3, V_4)))). % 17.06/5.79 tff(c_3518, plain, (![U_3, V_4]: (~accessible_world(skc12, U_3) | ~abstraction(skc8, V_4) | ~event(U_3, V_4)))). % 17.06/5.79 tff(c_3614, plain, (![V_1176, V_1177]: (abstraction(V_1176, V_1177) | ~accessible_world(skc12, V_1176) | ~forename(skc8, V_1177)))). % 17.06/5.79 tff(c_3699, plain, (![U_23, V_24]: (~accessible_world(skc12, U_23) | ~eventuality(skc8, V_24) | ~abstraction(U_23, V_24)))). % 17.06/5.79 tff(c_3260, plain, (![V_1112, V_1113]: (~existent(V_1112, V_1113) | ~accessible_world(skc12, V_1112) | ~eventuality(skc8, V_1113)))). % 17.06/5.79 tff(c_2335, plain, (![V_890, V_766]: (entity(V_890, skc10) | ~accessible_world(V_766, V_890) | ~accessible_world(skc8, V_766)))). % 17.06/5.79 tff(c_3243, plain, (![V_1108, V_1109]: (~human(V_1108, V_1109) | ~accessible_world(skc12, V_1108) | ~abstraction(skc8, V_1109)))). % 17.06/5.79 tff(c_2188, plain, (![V_77, V_843, V_842]: (event(V_77, skf2(V_843)) | ~accessible_world(V_842, V_77) | ~accessible_world(skc12, V_842)))). % 17.06/5.79 tff(c_2168, plain, (![V_832, V_755]: (animate(V_832, skc15) | ~accessible_world(V_755, V_832) | ~accessible_world(skc8, V_755)))). % 17.06/5.79 tff(c_3252, plain, (![V_1110, V_1111]: (~general(V_1110, V_1111) | ~accessible_world(skc12, V_1110) | ~entity(skc8, V_1111)))). % 17.06/5.79 tff(c_2266, plain, (![V_867, V_766]: (human(V_867, skc10) | ~accessible_world(V_766, V_867) | ~accessible_world(skc8, V_766)))). % 17.06/5.79 tff(c_2265, plain, (![V_867, V_755]: (human(V_867, skc15) | ~accessible_world(V_755, V_867) | ~accessible_world(skc8, V_755)))). % 17.06/5.79 tff(c_3351, plain, (![V_1134, V_1135]: (~general(V_1134, V_1135) | ~accessible_world(skc12, V_1134) | ~eventuality(skc8, V_1135)))). % 17.06/5.79 tff(c_3022, plain, (![V_86, V_1046]: (singleton(V_86, V_1046) | ~accessible_world(skc12, V_86) | ~entity(skc8, V_1046)))). % 17.06/5.79 tff(c_2360, plain, (![V_74, V_901, V_900]: (smoke(V_74, skf2(V_901)) | ~accessible_world(V_900, V_74) | ~accessible_world(skc12, V_900)))). % 17.06/5.79 tff(c_3308, plain, (![V_1124, V_1125]: (~male(V_1124, V_1125) | ~accessible_world(skc12, V_1124) | ~eventuality(skc8, V_1125)))). % 17.06/5.79 tff(c_3359, plain, (![V_1136, V_1137]: (~male(V_1136, V_1137) | ~accessible_world(skc12, V_1136) | ~abstraction(skc8, V_1137)))). % 17.06/5.79 tff(c_3275, plain, (![V_1114, V_1115]: (impartial(V_1114, V_1115) | ~accessible_world(skc12, V_1114) | ~human_person(skc8, V_1115)))). % 17.06/5.79 tff(c_3406, plain, (![V_1146, V_1147]: (~eventuality(V_1146, V_1147) | ~accessible_world(skc12, V_1146) | ~entity(skc8, V_1147)))). % 17.06/5.79 tff(c_3300, plain, (![V_1122, V_1123]: (singleton(V_1122, V_1123) | ~accessible_world(skc12, V_1122) | ~abstraction(skc8, V_1123)))). % 17.06/5.79 tff(c_2707, plain, (![V_107, V_1005]: (relation(V_107, V_1005) | ~accessible_world(skc12, V_107) | ~forename(skc8, V_1005)))). % 17.06/5.79 tff(c_2835, plain, (![V_140, V_1022]: (living(V_140, V_1022) | ~accessible_world(skc12, V_140) | ~human_person(skc8, V_1022)))). % 17.06/5.79 tff(c_2480, plain, (![V_164, V_934]: (agent(V_164, skc13, skc15) | ~accessible_world(V_934, V_164) | ~accessible_world(skc8, V_934)))). % 17.06/5.79 tff(c_3598, plain, (~event(skc8, skc11))). % 17.06/5.79 tff(c_3592, plain, (~event(skc8, skc14))). % 17.06/5.79 tff(c_2334, plain, (![V_890, V_755]: (entity(V_890, skc15) | ~accessible_world(V_755, V_890) | ~accessible_world(skc8, V_755)))). % 17.06/5.79 tff(c_3591, plain, (~event(skc8, skc12))). % 17.06/5.79 tff(c_2404, plain, (![V_172, V_916]: (of(V_172, skc14, skc15) | ~accessible_world(V_916, V_172) | ~accessible_world(skc8, V_916)))). % 17.06/5.79 tff(c_3454, plain, (![V_1148, V_1149]: (~abstraction(V_1148, V_1149) | ~accessible_world(skc12, V_1148) | ~event(skc8, V_1149)))). % 17.06/5.79 tff(c_3453, plain, (![V_1148, V_1149]: (~entity(V_1148, V_1149) | ~accessible_world(skc12, V_1148) | ~event(skc8, V_1149)))). % 17.06/5.79 tff(c_3006, plain, (![V_86, V_1041]: (singleton(V_86, V_1041) | ~accessible_world(skc12, V_86) | ~eventuality(skc8, V_1041)))). % 17.06/5.79 tff(c_3464, plain, (![V_1150, V_1151]: (abstraction(V_1150, V_1151) | ~accessible_world(skc12, V_1150) | ~proposition(skc8, V_1151)))). % 17.06/5.79 tff(c_3274, plain, (![V_1114, V_1115]: (entity(V_1114, V_1115) | ~accessible_world(skc12, V_1114) | ~human_person(skc8, V_1115)))). % 17.06/5.79 tff(c_2167, plain, (![V_832, V_766]: (animate(V_832, skc10) | ~accessible_world(V_766, V_832) | ~accessible_world(skc8, V_766)))). % 17.06/5.79 tff(c_3388, plain, (![V_1142, V_1143]: (~eventuality(V_1142, V_1143) | ~accessible_world(skc12, V_1142) | ~abstraction(skc8, V_1143)))). % 17.06/5.79 tff(c_3389, plain, (![V_1142, V_1143]: (~entity(V_1142, V_1143) | ~accessible_world(skc12, V_1142) | ~abstraction(skc8, V_1143)))). % 17.06/5.79 tff(c_2379, plain, (![V_107, V_909]: (relation(V_107, V_909) | ~accessible_world(skc12, V_107) | ~proposition(skc8, V_909)))). % 17.06/5.79 tff(c_2556, plain, (![V_80, V_954]: (eventuality(V_80, V_954) | ~accessible_world(skc12, V_80) | ~event(skc8, V_954)))). % 17.06/5.79 tff(c_3037, plain, (![V_134, V_1050]: (existent(V_134, V_1050) | ~accessible_world(skc12, V_134) | ~entity(skc8, V_1050)))). % 17.06/5.79 tff(c_2150, plain, (![V_80, V_830]: (eventuality(V_80, skc9) | ~accessible_world(V_830, V_80) | ~accessible_world(skc8, V_830)))). % 17.06/5.79 tff(c_2885, plain, (![V_116, V_1028]: (general(V_116, V_1028) | ~accessible_world(skc12, V_116) | ~abstraction(skc8, V_1028)))). % 17.06/5.79 tff(c_1913, plain, (![V_149, V_772]: (male(V_149, skc10) | ~accessible_world(V_772, V_149) | ~accessible_world(skc8, V_772)))). % 17.06/5.79 tff(c_2108, plain, (![V_77, V_819]: (event(V_77, skc9) | ~accessible_world(V_819, V_77) | ~accessible_world(skc8, V_819)))). % 17.06/5.79 tff(c_2654, plain, (![V_95, V_994]: (unisex(V_95, V_994) | ~accessible_world(skc12, V_95) | ~abstraction(skc8, V_994)))). % 17.06/5.79 tff(c_2681, plain, (![V_89, V_999]: (specific(V_89, V_999) | ~accessible_world(skc12, V_89) | ~eventuality(skc8, V_999)))). % 17.06/5.79 tff(c_1887, plain, (![V_125, V_766]: (human_person(V_125, skc10) | ~accessible_world(V_766, V_125) | ~accessible_world(skc8, V_766)))). % 17.06/5.79 tff(c_3244, plain, (![X8_963, X5_965, X7_961, X4_964]: (~of(skc8, X8_963, X5_965) | ~jules_forename(skc8, X8_963) | ~forename(skc8, X8_963) | ~event(skc12, X7_961) | ~agent(skc12, X7_961, X5_965) | ~present(skc12, X7_961) | ~smoke(skc12, X7_961) | ~agent(skc8, skc13, X5_965) | ~man(skc8, X5_965) | ~of(skc8, X4_964, X5_965) | ~vincent_forename(skc8, X4_964) | ~forename(skc8, X4_964)))). % 17.06/5.79 tff(c_2699, plain, (![V_155, V_1004]: (relname(V_155, V_1004) | ~accessible_world(skc12, V_155) | ~forename(skc8, V_1004)))). % 17.06/5.79 tff(c_2757, plain, (![V_95, V_1011]: (unisex(V_95, V_1011) | ~accessible_world(skc12, V_95) | ~eventuality(skc8, V_1011)))). % 17.06/5.79 tff(c_2517, plain, (![V_83, V_943]: (thing(V_83, V_943) | ~accessible_world(skc12, V_83) | ~abstraction(skc8, V_943)))). % 17.06/5.79 tff(c_1836, plain, (![V_125, V_755]: (human_person(V_125, skc15) | ~accessible_world(V_755, V_125) | ~accessible_world(skc8, V_755)))). % 17.06/5.79 tff(c_3017, plain, (![V_83, V_1045]: (thing(V_83, V_1045) | ~accessible_world(skc12, V_83) | ~entity(skc8, V_1045)))). % 17.06/5.79 tff(c_1925, plain, (![V_149, V_773]: (male(V_149, skc15) | ~accessible_world(V_773, V_149) | ~accessible_world(skc8, V_773)))). % 17.06/5.79 tff(c_2790, plain, (![V_128, V_1016]: (organism(V_128, V_1016) | ~accessible_world(skc12, V_128) | ~human_person(skc8, V_1016)))). % 17.06/5.79 tff(c_2419, plain, (![V_92, V_921]: (nonexistent(V_92, V_921) | ~accessible_world(skc12, V_92) | ~eventuality(skc8, V_921)))). % 17.06/5.79 tff(c_2599, plain, (![V_89, V_959]: (specific(V_89, V_959) | ~accessible_world(skc12, V_89) | ~entity(skc8, V_959)))). % 17.06/5.79 tff(c_2804, plain, (![V_113, V_1020]: (nonhuman(V_113, V_1020) | ~accessible_world(skc12, V_113) | ~abstraction(skc8, V_1020)))). % 17.06/5.79 tff(c_2322, plain, (![V_887, V_823]: (forename(V_887, skc14) | ~accessible_world(V_823, V_887) | ~accessible_world(skc8, V_823)))). % 17.06/5.79 tff(c_2321, plain, (![V_887, V_862]: (forename(V_887, skc11) | ~accessible_world(V_862, V_887) | ~accessible_world(skc8, V_862)))). % 17.06/5.79 tff(c_3001, plain, (![V_83, V_1040]: (thing(V_83, V_1040) | ~accessible_world(skc12, V_83) | ~eventuality(skc8, V_1040)))). % 17.06/5.79 tff(c_2348, plain, (![V_104, V_896]: (proposition(V_104, skc12) | ~accessible_world(V_896, V_104) | ~accessible_world(skc8, V_896)))). % 17.06/5.79 tff(c_1849, plain, (![V_756, V_6, U_5]: (singleton(V_756, V_6) | ~accessible_world(U_5, V_756) | ~eventuality(U_5, V_6)))). % 17.06/5.79 tff(c_2291, plain, (![V_101, V_879]: (think_believe_consider(V_101, skc13) | ~accessible_world(V_879, V_101) | ~accessible_world(skc8, V_879)))). % 17.06/5.79 tff(c_2309, plain, (![V_119, V_886]: (state(V_119, skc9) | ~accessible_world(V_886, V_119) | ~accessible_world(skc8, V_886)))). % 17.06/5.79 tff(c_2242, plain, (![V_161, V_862]: (jules_forename(V_161, skc11) | ~accessible_world(V_862, V_161) | ~accessible_world(skc8, V_862)))). % 17.06/5.79 tff(c_2531, plain, (![W_949, V_947, Y_948, U_196]: (W_949=V_947 | ~agent(skc12, Y_948, U_196) | ~theme(skc12, Y_948, W_949) | ~think_believe_consider(skc12, Y_948) | ~think_believe_consider(skc12, skf2(U_196)) | ~theme(skc12, skf2(U_196), V_947) | ~proposition(skc12, W_949) | ~proposition(skc12, V_947) | ~man(skc12, U_196)))). % 17.06/5.79 tff(c_2177, plain, (![V_838, V_231, U_230]: (living(V_838, V_231) | ~accessible_world(U_230, V_838) | ~human_person(U_230, V_231)))). % 17.06/5.79 tff(c_3127, plain, (![V_1065]: (skc12=V_1065 | ~theme(skc8, skc13, V_1065) | ~proposition(skc8, V_1065)))). % 17.06/5.79 tff(c_2506, plain, (![W_936]: (skc14=W_936 | ~forename(skc8, W_936) | ~of(skc8, W_936, skc15)))). % 17.06/5.79 tff(c_2044, plain, (![V_804, V_54, U_53]: (relation(V_804, V_54) | ~accessible_world(U_53, V_804) | ~forename(U_53, V_54)))). % 17.06/5.79 tff(c_2272, plain, (![V_98, V_870]: (present(V_98, skc13) | ~accessible_world(V_870, V_98) | ~accessible_world(skc8, V_870)))). % 17.06/5.79 tff(c_1847, plain, (![V_756, V_38, U_37]: (singleton(V_756, V_38) | ~accessible_world(U_37, V_756) | ~entity(U_37, V_38)))). % 17.06/5.79 tff(c_2227, plain, (![V_853, V_34, U_33]: (impartial(V_853, V_34) | ~accessible_world(U_33, V_853) | ~human_person(U_33, V_34)))). % 17.06/5.79 tff(c_2208, plain, (![V_122, V_849]: (man(V_122, skc15) | ~accessible_world(V_849, V_122) | ~accessible_world(skc8, V_849)))). % 17.06/5.79 tff(c_2220, plain, (![V_122, V_850]: (man(V_122, skc10) | ~accessible_world(V_850, V_122) | ~accessible_world(skc8, V_850)))). % 17.06/5.79 tff(c_2534, plain, (![W_949, V_947, Y_948]: (W_949=V_947 | ~agent(skc8, Y_948, skc15) | ~theme(skc8, Y_948, W_949) | ~think_believe_consider(skc8, Y_948) | ~theme(skc8, skc13, V_947) | ~proposition(skc8, W_949) | ~proposition(skc8, V_947)))). % 17.06/5.80 tff(c_1848, plain, (![V_756, V_20, U_19]: (singleton(V_756, V_20) | ~accessible_world(U_19, V_756) | ~abstraction(U_19, V_20)))). % 17.06/5.80 tff(c_2503, plain, (![W_936]: (skc11=W_936 | ~forename(skc8, W_936) | ~of(skc8, W_936, skc10)))). % 17.06/5.80 tff(c_2121, plain, (![V_158, V_823]: (vincent_forename(V_158, skc14) | ~accessible_world(V_823, V_158) | ~accessible_world(skc8, V_823)))). % 17.06/5.80 tff(c_3092, plain, (~accessible_world(skc8, skc8))). % 17.06/5.80 tff(c_2096, plain, (![V_77, V_818]: (event(V_77, skc13) | ~accessible_world(V_818, V_77) | ~accessible_world(skc8, V_818)))). % 17.06/5.80 tff(c_3086, plain, (![V_195]: (~entity(skc8, skf2(V_195))))). % 17.06/5.80 tff(c_3055, plain, (![V_4]: (~entity(skc8, V_4) | ~event(skc12, V_4)))). % 17.06/5.80 tff(c_2432, plain, (![V_923, U_196]: (agent(V_923, skf2(U_196), U_196) | ~accessible_world(skc12, V_923) | ~man(skc12, U_196)))). % 17.06/5.80 tff(c_3038, plain, (![V_1050]: (~eventuality(skc12, V_1050) | ~entity(skc8, V_1050)))). % 17.06/5.80 tff(c_3026, plain, (![V_1048]: (existent(skc12, V_1048) | ~entity(skc8, V_1048)))). % 17.06/5.80 tff(c_2231, plain, (![V_856, V_42, U_41]: (existent(V_856, V_42) | ~accessible_world(U_41, V_856) | ~entity(U_41, V_42)))). % 17.06/5.80 tff(c_3018, plain, (![V_1045]: (singleton(skc12, V_1045) | ~entity(skc8, V_1045)))). % 17.06/5.80 tff(c_3010, plain, (![V_1043]: (thing(skc12, V_1043) | ~entity(skc8, V_1043)))). % 17.06/5.80 tff(c_1965, plain, (![V_779, V_38, U_37]: (thing(V_779, V_38) | ~accessible_world(U_37, V_779) | ~entity(U_37, V_38)))). % 17.06/5.80 tff(c_3002, plain, (![V_1040]: (singleton(skc12, V_1040) | ~eventuality(skc8, V_1040)))). % 17.06/5.80 tff(c_2994, plain, (![V_1038]: (thing(skc12, V_1038) | ~eventuality(skc8, V_1038)))). % 17.06/5.80 tff(c_1964, plain, (![V_779, V_6, U_5]: (thing(V_779, V_6) | ~accessible_world(U_5, V_779) | ~eventuality(U_5, V_6)))). % 17.06/5.80 tff(c_2988, plain, (![V_1034]: (~abstraction(V_1034, skc10) | ~accessible_world(skc12, V_1034)))). % 17.06/5.80 tff(c_2970, plain, (![V_1033]: (~abstraction(V_1033, skc15) | ~accessible_world(skc12, V_1033)))). % 17.06/5.80 tff(c_2830, plain, (![V_131]: (entity(V_131, skc10) | ~accessible_world(skc12, V_131)))). % 17.06/5.80 tff(c_2841, plain, (![V_131]: (entity(V_131, skc15) | ~accessible_world(skc12, V_131)))). % 17.06/5.80 tff(c_2951, plain, (![V_195]: (~abstraction(skc8, skf2(V_195))))). % 17.06/5.80 tff(c_2904, plain, (![V_4]: (~abstraction(skc8, V_4) | ~event(skc12, V_4)))). % 17.06/5.80 tff(c_2887, plain, (![V_1028]: (~entity(skc12, V_1028) | ~abstraction(skc8, V_1028)))). % 17.06/5.80 tff(c_2886, plain, (![V_1028]: (~eventuality(skc12, V_1028) | ~abstraction(skc8, V_1028)))). % 17.06/5.80 tff(c_2867, plain, (![V_1026]: (general(skc12, V_1026) | ~abstraction(skc8, V_1026)))). % 17.06/5.80 tff(c_2295, plain, (![V_880, V_24, U_23]: (general(V_880, V_24) | ~accessible_world(U_23, V_880) | ~abstraction(U_23, V_24)))). % 17.06/5.80 tff(c_2792, plain, (![V_1016]: (impartial(skc12, V_1016) | ~human_person(skc8, V_1016)))). % 17.06/5.80 tff(c_2805, plain, (![V_1020]: (~human(skc12, V_1020) | ~abstraction(skc8, V_1020)))). % 17.06/5.80 tff(c_2824, plain, (entity(skc12, skc15))). % 17.06/5.80 tff(c_2793, plain, (![V_1016]: (living(skc12, V_1016) | ~human_person(skc8, V_1016)))). % 17.06/5.80 tff(c_2823, plain, (entity(skc12, skc10))). % 17.06/5.80 tff(c_2791, plain, (![V_1016]: (entity(skc12, V_1016) | ~human_person(skc8, V_1016)))). % 17.06/5.80 tff(c_2797, plain, (![V_1018]: (nonhuman(skc12, V_1018) | ~abstraction(skc8, V_1018)))). % 17.06/5.80 tff(c_1903, plain, (![V_769, V_22, U_21]: (nonhuman(V_769, V_22) | ~accessible_world(U_21, V_769) | ~abstraction(U_21, V_22)))). % 17.06/5.80 tff(c_2777, plain, (![V_1014]: (organism(skc12, V_1014) | ~human_person(skc8, V_1014)))). % 17.06/5.80 tff(c_2058, plain, (![V_808, V_34, U_33]: (organism(V_808, V_34) | ~accessible_world(U_33, V_808) | ~human_person(U_33, V_34)))). % 17.06/5.80 tff(c_2758, plain, (![V_1011]: (~male(skc12, V_1011) | ~eventuality(skc8, V_1011)))). % 17.06/5.80 tff(c_2750, plain, (![V_1009]: (unisex(skc12, V_1009) | ~eventuality(skc8, V_1009)))). % 17.06/5.80 tff(c_2025, plain, (![V_797, V_14, U_13]: (unisex(V_797, V_14) | ~accessible_world(U_13, V_797) | ~eventuality(U_13, V_14)))). % 17.06/5.80 tff(c_2708, plain, (![V_1005]: (abstraction(skc12, V_1005) | ~forename(skc8, V_1005)))). % 17.06/5.80 tff(c_2688, plain, (![V_24]: (~eventuality(skc8, V_24) | ~abstraction(skc12, V_24)))). % 17.06/5.80 tff(c_2700, plain, (![V_1004]: (relation(skc12, V_1004) | ~forename(skc8, V_1004)))). % 17.06/5.80 tff(c_2692, plain, (![V_1002]: (relname(skc12, V_1002) | ~forename(skc8, V_1002)))). % 17.06/5.80 tff(c_1814, plain, (![V_750, V_54, U_53]: (relname(V_750, V_54) | ~accessible_world(U_53, V_750) | ~forename(U_53, V_54)))). % 17.06/5.80 tff(c_2682, plain, (![V_999]: (~general(skc12, V_999) | ~eventuality(skc8, V_999)))). % 17.06/5.80 tff(c_2674, plain, (![V_997]: (specific(skc12, V_997) | ~eventuality(skc8, V_997)))). % 17.06/5.80 tff(c_2282, plain, (![V_873, V_10, U_9]: (specific(V_873, V_10) | ~accessible_world(U_9, V_873) | ~eventuality(U_9, V_10)))). % 17.06/5.80 tff(c_2655, plain, (![V_994]: (~male(skc12, V_994) | ~abstraction(skc8, V_994)))). % 17.06/5.80 tff(c_2638, plain, (![V_977]: (unisex(skc12, V_977) | ~abstraction(skc8, V_977)))). % 17.06/5.80 tff(c_190, plain, (![Y_222, X_221, X8_224, X9_216, X7_218, X4_225, X6_212, W_213, X3_214, U_215, X1_219, Z_217, X5_211, V_223, X2_220]: (~actual_world(W_213) | ~theme(W_213, X7_218, X4_225) | ~event(W_213, X7_218) | ~present(W_213, X7_218) | ~think_believe_consider(W_213, X7_218) | ~of(W_213, X9_216, X6_212) | ~jules_forename(W_213, X9_216) | ~forename(W_213, X9_216) | ~event(X4_225, X8_224) | ~agent(X4_225, X8_224, X6_212) | ~present(X4_225, X8_224) | ~smoke(X4_225, X8_224) | ~agent(W_213, X7_218, X6_212) | ~man(W_213, X6_212) | ~of(W_213, X5_211, X6_212) | ~vincent_forename(W_213, X5_211) | ~forename(W_213, X5_211) | ~accessible_world(W_213, X4_225) | ~proposition(W_213, X4_225) | ~forename(W_213, X3_214) | ~jules_forename(W_213, X3_214) | ~of(W_213, X3_214, X2_220) | ~man(W_213, X2_220) | ~be(W_213, X1_219, X2_220, X2_220) | ~state(W_213, X1_219) | ~agent(W_213, X_221, Z_217) | ~man(W_213, Z_217) | ~of(W_213, Y_222, Z_217) | ~vincent_forename(W_213, Y_222) | ~forename(W_213, Y_222) | ~think_believe_consider(W_213, X_221) | ~present(W_213, X_221) | ~event(W_213, X_221) | ~theme(W_213, X_221, U_215) | ~proposition(W_213, U_215) | ~accessible_world(W_213, U_215) | ~event(U_215, V_223) | ~agent(U_215, V_223, skf4(U_215)) | ~present(U_215, V_223) | ~smoke(U_215, V_223)))). % 17.06/5.80 tff(c_2026, plain, (![V_797, V_26, U_25]: (unisex(V_797, V_26) | ~accessible_world(U_25, V_797) | ~abstraction(U_25, V_26)))). % 17.06/5.80 tff(c_2615, plain, (![V_24]: (~entity(skc8, V_24) | ~abstraction(skc12, V_24)))). % 17.06/5.80 tff(c_2600, plain, (![V_959]: (~general(skc12, V_959) | ~entity(skc8, V_959)))). % 17.06/5.80 tff(c_188, plain, (![X4_210, X_206, W_199, X1_204, Z_202, X5_197, V_208, X6_198, X2_205, X7_203, X8_209, Y_207, U_201, X3_200]: (man(V_208, skf4(V_208)) | ~actual_world(U_201) | ~theme(U_201, X6_198, X3_200) | ~event(U_201, X6_198) | ~present(U_201, X6_198) | ~think_believe_consider(U_201, X6_198) | ~of(U_201, X8_209, X5_197) | ~jules_forename(U_201, X8_209) | ~forename(U_201, X8_209) | ~event(X3_200, X7_203) | ~agent(X3_200, X7_203, X5_197) | ~present(X3_200, X7_203) | ~smoke(X3_200, X7_203) | ~agent(U_201, X6_198, X5_197) | ~man(U_201, X5_197) | ~of(U_201, X4_210, X5_197) | ~vincent_forename(U_201, X4_210) | ~forename(U_201, X4_210) | ~accessible_world(U_201, X3_200) | ~proposition(U_201, X3_200) | ~forename(U_201, X2_205) | ~jules_forename(U_201, X2_205) | ~of(U_201, X2_205, X1_204) | ~man(U_201, X1_204) | ~be(U_201, Z_202, X1_204, X1_204) | ~state(U_201, Z_202) | ~agent(U_201, W_199, Y_207) | ~man(U_201, Y_207) | ~of(U_201, X_206, Y_207) | ~vincent_forename(U_201, X_206) | ~forename(U_201, X_206) | ~think_believe_consider(U_201, W_199) | ~present(U_201, W_199) | ~event(U_201, W_199) | ~theme(U_201, W_199, V_208) | ~proposition(U_201, V_208) | ~accessible_world(U_201, V_208)))). % 17.06/5.80 tff(c_2592, plain, (![V_957]: (specific(skc12, V_957) | ~entity(skc8, V_957)))). % 17.06/5.80 tff(c_2283, plain, (![V_873, V_40, U_39]: (specific(V_873, V_40) | ~accessible_world(U_39, V_873) | ~entity(U_39, V_40)))). % 17.06/5.80 tff(c_2564, plain, (![V_954]: (~abstraction(skc12, V_954) | ~event(skc8, V_954)))). % 17.06/5.80 tff(c_2538, plain, (![V_952]: (eventuality(skc12, V_952) | ~event(skc8, V_952)))). % 17.06/5.80 tff(c_2140, plain, (![V_827, V_4, U_3]: (eventuality(V_827, V_4) | ~accessible_world(U_3, V_827) | ~event(U_3, V_4)))). % 17.06/5.80 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)))). % 17.06/5.80 tff(c_2518, plain, (![V_943]: (singleton(skc12, V_943) | ~abstraction(skc8, V_943)))). % 17.06/5.80 tff(c_2510, plain, (![V_941]: (thing(skc12, V_941) | ~abstraction(skc8, V_941)))). % 17.06/5.80 tff(c_1963, plain, (![V_779, V_20, U_19]: (thing(V_779, V_20) | ~accessible_world(U_19, V_779) | ~abstraction(U_19, V_20)))). % 17.06/5.80 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)))). % 17.06/5.80 tff(c_2452, plain, (![V_932]: (be(V_932, skc9, skc10, skc10) | ~accessible_world(skc8, V_932)))). % 17.06/5.80 tff(c_2433, plain, (![V_923]: (agent(V_923, skc13, skc15) | ~accessible_world(skc8, V_923)))). % 17.06/5.80 tff(c_2476, plain, (~entity(skc12, skc13))). % 17.06/5.80 tff(c_2448, plain, (![V_4]: (~entity(skc12, V_4) | ~event(skc8, V_4)))). % 17.06/5.80 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)))). % 17.06/5.80 tff(c_2447, plain, (~entity(skc12, skc9))). % 17.06/5.80 tff(c_2426, plain, (![V_42]: (~eventuality(skc8, V_42) | ~entity(skc12, V_42)))). % 17.06/5.80 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)))). % 17.06/5.80 tff(c_2420, plain, (![V_921]: (~existent(skc12, V_921) | ~eventuality(skc8, V_921)))). % 17.06/5.80 tff(c_2412, plain, (![V_919]: (nonexistent(skc12, V_919) | ~eventuality(skc8, V_919)))). % 17.06/5.80 tff(c_1975, plain, (![V_784, V_12, U_11]: (nonexistent(V_784, V_12) | ~accessible_world(U_11, V_784) | ~eventuality(U_11, V_12)))). % 17.06/5.80 tff(c_2400, plain, (![V_912]: (theme(V_912, skc13, skc12) | ~accessible_world(skc8, V_912)))). % 17.06/5.80 tff(c_2372, plain, (![V_905]: (of(V_905, skc14, skc15) | ~accessible_world(skc8, V_905)))). % 17.06/5.81 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)))). % 17.06/5.81 tff(c_2371, plain, (![V_905]: (of(V_905, skc11, skc10) | ~accessible_world(skc8, V_905)))). % 17.06/5.81 tff(c_2380, plain, (![V_909]: (abstraction(skc12, V_909) | ~proposition(skc8, V_909)))). % 17.06/5.81 tff(c_2365, plain, (![V_903]: (relation(skc12, V_903) | ~proposition(skc8, V_903)))). % 17.06/5.81 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)))). % 17.06/5.81 tff(c_2045, plain, (![V_804, V_16, U_15]: (relation(V_804, V_16) | ~accessible_world(U_15, V_804) | ~proposition(U_15, V_16)))). % 17.06/5.81 tff(c_2353, plain, (![V_897, V_191]: (smoke(V_897, skf2(V_191)) | ~accessible_world(skc12, V_897)))). % 17.06/5.81 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)))). % 17.06/5.81 tff(c_2341, plain, (![V_893]: (proposition(V_893, skc12) | ~accessible_world(skc8, V_893)))). % 17.06/5.81 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)))). % 17.06/5.81 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)))). % 17.06/5.81 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)))). % 17.06/5.81 tff(c_2299, plain, (![V_883]: (state(V_883, skc9) | ~accessible_world(skc8, V_883)))). % 17.06/5.81 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)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2287, plain, (![V_876]: (think_believe_consider(V_876, skc13) | ~accessible_world(skc8, V_876)))). % 17.34/5.81 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)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2254, plain, (![V_864, V_193]: (present(V_864, skf2(V_193)) | ~accessible_world(skc12, V_864)))). % 17.34/5.81 tff(c_2255, plain, (![V_864]: (present(V_864, skc13) | ~accessible_world(skc8, V_864)))). % 17.34/5.81 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)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2243, plain, (![V_862]: (forename(V_862, skc11) | ~accessible_world(skc8, V_862)))). % 17.34/5.81 tff(c_2235, plain, (![V_859]: (jules_forename(V_859, skc11) | ~accessible_world(skc8, V_859)))). % 17.34/5.81 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)))). % 17.34/5.81 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)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2190, plain, (![V_842, V_843]: (~entity(V_842, skf2(V_843)) | ~accessible_world(skc12, V_842)))). % 17.34/5.81 tff(c_2198, plain, (![V_846]: (man(V_846, skc10) | ~accessible_world(skc8, V_846)))). % 17.34/5.81 tff(c_2197, plain, (![V_846]: (man(V_846, skc15) | ~accessible_world(skc8, V_846)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2189, plain, (![V_842, V_843]: (~abstraction(V_842, skf2(V_843)) | ~accessible_world(skc12, V_842)))). % 17.34/5.81 tff(c_2081, plain, (![V_815, V_195]: (event(V_815, skf2(V_195)) | ~accessible_world(skc12, V_815)))). % 17.34/5.81 tff(c_2068, plain, (![V_110]: (abstraction(V_110, skc14) | ~accessible_world(skc12, V_110)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2086, plain, (![V_110]: (abstraction(V_110, skc11) | ~accessible_world(skc12, V_110)))). % 17.34/5.81 tff(c_2048, plain, (![V_110]: (abstraction(V_110, skc12) | ~accessible_world(skc12, V_110)))). % 17.34/5.81 tff(c_2098, plain, (![V_818]: (~entity(V_818, skc13) | ~accessible_world(skc8, V_818)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2157, plain, (~abstraction(skc12, skc9))). % 17.34/5.81 tff(c_2152, plain, (![V_830]: (~abstraction(V_830, skc9) | ~accessible_world(skc8, V_830)))). % 17.34/5.81 tff(c_2139, plain, (![V_827]: (eventuality(V_827, skc9) | ~accessible_world(skc8, V_827)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2110, plain, (![V_819]: (~entity(V_819, skc9) | ~accessible_world(skc8, V_819)))). % 17.34/5.81 tff(c_2132, plain, (~abstraction(skc12, skc13))). % 17.34/5.81 tff(c_2097, plain, (![V_818]: (~abstraction(V_818, skc13) | ~accessible_world(skc8, V_818)))). % 17.34/5.81 tff(c_2122, plain, (![V_823]: (forename(V_823, skc14) | ~accessible_world(skc8, V_823)))). % 17.34/5.81 tff(c_2114, plain, (![V_820]: (vincent_forename(V_820, skc14) | ~accessible_world(skc8, V_820)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2082, plain, (![V_815]: (event(V_815, skc9) | ~accessible_world(skc8, V_815)))). % 17.34/5.81 tff(c_2083, plain, (![V_815]: (event(V_815, skc13) | ~accessible_world(skc8, V_815)))). % 17.34/5.81 tff(c_2073, plain, (abstraction(skc12, skc11))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_1999, plain, (![V_791]: (abstraction(V_791, skc11) | ~accessible_world(skc8, V_791)))). % 17.34/5.81 tff(c_2065, plain, (abstraction(skc12, skc14))). % 17.34/5.81 tff(c_2000, plain, (![V_791]: (abstraction(V_791, skc14) | ~accessible_world(skc8, V_791)))). % 17.34/5.81 tff(c_2054, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc10)))). % 17.34/5.81 tff(c_1942, plain, (![U_3]: (~accessible_world(skc8, U_3) | ~event(U_3, skc15)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_1915, plain, (![V_772]: (~eventuality(V_772, skc10) | ~accessible_world(skc8, V_772)))). % 17.34/5.81 tff(c_2038, plain, (abstraction(skc12, skc12))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2001, plain, (![V_791]: (abstraction(V_791, skc12) | ~accessible_world(skc8, V_791)))). % 17.34/5.81 tff(c_2033, plain, (~abstraction(skc12, skc10))). % 17.34/5.81 tff(c_1914, plain, (![V_772]: (~abstraction(V_772, skc10) | ~accessible_world(skc8, V_772)))). % 17.34/5.81 tff(c_1889, plain, (![V_766]: (animate(V_766, skc10) | ~accessible_world(skc8, V_766)))). % 17.34/5.81 tff(c_2017, plain, (![V_195]: (~abstraction(skc12, skf2(V_195))))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_2019, plain, (~abstraction(skc8, skc13))). % 17.34/5.81 tff(c_1858, plain, (![U_3, V_4]: (~abstraction(U_3, V_4) | ~event(U_3, V_4)))). % 17.34/5.81 tff(c_1837, plain, (![V_755]: (entity(V_755, skc15) | ~accessible_world(skc8, V_755)))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_1839, plain, (![V_755]: (human(V_755, skc15) | ~accessible_world(skc8, V_755)))). % 17.34/5.81 tff(c_1890, plain, (![V_766]: (human(V_766, skc10) | ~accessible_world(skc8, V_766)))). % 17.34/5.81 tff(c_1838, plain, (![V_755]: (animate(V_755, skc15) | ~accessible_world(skc8, V_755)))). % 17.34/5.81 tff(c_1888, plain, (![V_766]: (entity(V_766, skc10) | ~accessible_world(skc8, V_766)))). % 17.34/5.81 tff(c_1971, plain, (~abstraction(skc12, skc15))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_1926, plain, (![V_773]: (~abstraction(V_773, skc15) | ~accessible_world(skc8, V_773)))). % 17.34/5.81 tff(c_1953, plain, (![V_195]: (~entity(skc12, skf2(V_195))))). % 17.34/5.81 tff(c_1955, plain, (~entity(skc8, skc13))). % 17.34/5.81 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)))). % 17.34/5.81 tff(c_1899, plain, (![U_3, V_4]: (~entity(U_3, V_4) | ~event(U_3, V_4)))). % 17.34/5.81 tff(c_1927, plain, (![V_773]: (~eventuality(V_773, skc15) | ~accessible_world(skc8, V_773)))). % 17.34/5.81 tff(c_1773, plain, (![U_23, V_24]: (~entity(U_23, V_24) | ~abstraction(U_23, V_24)))). % 17.34/5.82 tff(c_1874, plain, (![V_763]: (male(V_763, skc15) | ~accessible_world(skc8, V_763)))). % 17.34/5.82 tff(c_1873, plain, (![V_763]: (male(V_763, skc10) | ~accessible_world(skc8, V_763)))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_1898, plain, (~entity(skc8, skc9))). % 17.34/5.82 tff(c_335, plain, (![U_41, V_42]: (~eventuality(U_41, V_42) | ~entity(U_41, V_42)))). % 17.34/5.82 tff(c_1794, plain, (![V_741]: (human_person(V_741, skc10) | ~accessible_world(skc8, V_741)))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_1867, plain, (abstraction(skc8, skc11))). % 17.34/5.82 tff(c_1866, plain, (abstraction(skc8, skc14))). % 17.34/5.82 tff(c_844, plain, (![U_451, V_452]: (abstraction(U_451, V_452) | ~forename(U_451, V_452)))). % 17.34/5.82 tff(c_1857, plain, (~abstraction(skc8, skc9))). % 17.34/5.82 tff(c_1800, plain, (![U_23, V_24]: (~eventuality(U_23, V_24) | ~abstraction(U_23, V_24)))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_1795, plain, (![V_741]: (human_person(V_741, skc15) | ~accessible_world(skc8, V_741)))). % 17.34/5.82 tff(c_291, plain, (![U_278, V_279]: (~male(U_278, V_279) | ~abstraction(U_278, V_279)))). % 17.34/5.82 tff(c_1810, plain, (~abstraction(skc8, skc10))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_1809, plain, (~abstraction(skc8, skc15))). % 17.34/5.82 tff(c_285, plain, (![U_274, V_275]: (~human(U_274, V_275) | ~abstraction(U_274, V_275)))). % 17.34/5.82 tff(c_319, plain, (![U_37, V_38]: (singleton(U_37, V_38) | ~entity(U_37, V_38)))). % 17.34/5.82 tff(c_324, plain, (![U_288, V_289]: (~general(U_288, V_289) | ~eventuality(U_288, V_289)))). % 17.34/5.82 tff(c_1788, plain, (entity(skc8, skc15))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_1787, plain, (entity(skc8, skc10))). % 17.34/5.82 tff(c_248, plain, (![U_33, V_34]: (entity(U_33, V_34) | ~human_person(U_33, V_34)))). % 17.34/5.82 tff(c_1778, plain, (abstraction(skc8, skc12))). % 17.34/5.82 tff(c_186, plain, (![U_196]: (agent(skc12, skf2(U_196), U_196) | ~man(skc12, U_196)))). % 17.34/5.82 tff(c_296, plain, (![U_280, V_281]: (abstraction(U_280, V_281) | ~proposition(U_280, V_281)))). % 17.34/5.82 tff(c_241, plain, (![U_258, V_259]: (~general(U_258, V_259) | ~entity(U_258, V_259)))). % 17.34/5.82 tff(c_236, plain, (![U_33, V_34]: (impartial(U_33, V_34) | ~human_person(U_33, V_34)))). % 17.34/5.82 tff(c_1761, plain, (![V_191]: (smoke(skc12, skf2(V_191))))). % 17.34/5.82 tff(c_317, plain, (![U_19, V_20]: (singleton(U_19, V_20) | ~abstraction(U_19, V_20)))). % 17.34/5.82 tff(c_318, plain, (![U_5, V_6]: (singleton(U_5, V_6) | ~eventuality(U_5, V_6)))). % 17.34/5.82 tff(c_197, plain, (![U_230, V_231]: (living(U_230, V_231) | ~human_person(U_230, V_231)))). % 17.34/5.82 tff(c_1226, plain, (![V_195]: (event(skc12, skf2(V_195))))). % 17.34/5.82 tff(c_231, plain, (![U_53, V_54]: (relation(U_53, V_54) | ~forename(U_53, V_54)))). % 17.34/5.82 tff(c_828, plain, (![V_193]: (present(skc12, skf2(V_193))))). % 17.34/5.82 tff(c_838, plain, (~event(skc8, skc15))). % 17.34/5.82 tff(c_348, plain, (~event(skc8, skc10))). % 17.34/5.82 tff(c_344, plain, (~eventuality(skc8, skc15))). % 17.34/5.82 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)))). % 17.34/5.82 tff(c_343, plain, (~eventuality(skc8, skc10))). % 17.34/5.82 tff(c_301, plain, (![U_282, V_283]: (~male(U_282, V_283) | ~eventuality(U_282, V_283)))). % 17.34/5.82 tff(c_306, plain, (![U_284, V_285]: (~existent(U_284, V_285) | ~eventuality(U_284, V_285)))). % 17.34/5.82 tff(c_330, plain, (event(skc8, skc9))). % 17.34/5.82 tff(c_30, plain, (![U_29, V_30]: (event(U_29, V_30) | ~state(U_29, V_30)))). % 17.34/5.82 tff(c_24, plain, (![U_23, V_24]: (general(U_23, V_24) | ~abstraction(U_23, V_24)))). % 17.34/5.82 tff(c_10, plain, (![U_9, V_10]: (specific(U_9, V_10) | ~eventuality(U_9, V_10)))). % 17.34/5.82 tff(c_8, plain, (![U_7, V_8]: (singleton(U_7, V_8) | ~thing(U_7, V_8)))). % 17.34/5.82 tff(c_12, plain, (![U_11, V_12]: (nonexistent(U_11, V_12) | ~eventuality(U_11, V_12)))). % 17.34/5.82 tff(c_14, plain, (![U_13, V_14]: (unisex(U_13, V_14) | ~eventuality(U_13, V_14)))). % 17.34/5.82 tff(c_16, plain, (![U_15, V_16]: (relation(U_15, V_16) | ~proposition(U_15, V_16)))). % 17.34/5.82 tff(c_26, plain, (![U_25, V_26]: (unisex(U_25, V_26) | ~abstraction(U_25, V_26)))). % 17.34/5.82 tff(c_20, plain, (![U_19, V_20]: (thing(U_19, V_20) | ~abstraction(U_19, V_20)))). % 17.34/5.82 tff(c_267, plain, (human(skc8, skc15))). % 17.34/5.82 tff(c_274, plain, (animate(skc8, skc10))). % 17.34/5.82 tff(c_22, plain, (![U_21, V_22]: (nonhuman(U_21, V_22) | ~abstraction(U_21, V_22)))). % 17.34/5.82 tff(c_275, plain, (human(skc8, skc10))). % 17.34/5.82 tff(c_266, plain, (animate(skc8, skc15))). % 17.34/5.82 tff(c_280, plain, (eventuality(skc8, skc9))). % 17.34/5.82 tff(c_28, plain, (![U_27, V_28]: (eventuality(U_27, V_28) | ~state(U_27, V_28)))). % 17.34/5.82 tff(c_259, plain, (human_person(skc8, skc10))). % 17.34/5.82 tff(c_258, plain, (human_person(skc8, skc15))). % 17.34/5.82 tff(c_32, plain, (![U_31, V_32]: (human_person(U_31, V_32) | ~man(U_31, V_32)))). % 17.34/5.82 tff(c_4, plain, (![U_3, V_4]: (eventuality(U_3, V_4) | ~event(U_3, V_4)))). % 17.34/5.82 tff(c_2, plain, (![U_1, V_2]: (event(U_1, V_2) | ~smoke(U_1, V_2)))). % 17.34/5.82 tff(c_36, plain, (![U_35, V_36]: (entity(U_35, V_36) | ~organism(U_35, V_36)))). % 17.34/5.82 tff(c_18, plain, (![U_17, V_18]: (abstraction(U_17, V_18) | ~relation(U_17, V_18)))). % 17.34/5.82 tff(c_68, plain, (![U_67, V_68]: (~existent(U_67, V_68) | ~nonexistent(U_67, V_68)))). % 17.34/5.82 tff(c_40, plain, (![U_39, V_40]: (specific(U_39, V_40) | ~entity(U_39, V_40)))). % 17.34/5.82 tff(c_44, plain, (![U_43, V_44]: (impartial(U_43, V_44) | ~organism(U_43, V_44)))). % 17.34/5.82 tff(c_56, plain, (![U_55, V_56]: (relation(U_55, V_56) | ~relname(U_55, V_56)))). % 17.34/5.82 tff(c_6, plain, (![U_5, V_6]: (thing(U_5, V_6) | ~eventuality(U_5, V_6)))). % 17.34/5.82 tff(c_58, plain, (![U_57, V_58]: (forename(U_57, V_58) | ~vincent_forename(U_57, V_58)))). % 17.34/5.82 tff(c_218, plain, (male(skc8, skc10))). % 17.34/5.82 tff(c_217, plain, (male(skc8, skc15))). % 17.34/5.82 tff(c_54, plain, (![U_53, V_54]: (relname(U_53, V_54) | ~forename(U_53, V_54)))). % 17.34/5.82 tff(c_52, plain, (![U_51, V_52]: (male(U_51, V_52) | ~man(U_51, V_52)))). % 17.34/5.82 tff(c_42, plain, (![U_41, V_42]: (existent(U_41, V_42) | ~entity(U_41, V_42)))). % 17.34/5.82 tff(c_66, plain, (![U_65, V_66]: (~nonhuman(U_65, V_66) | ~human(U_65, V_66)))). % 17.34/5.82 tff(c_60, plain, (![U_59, V_60]: (forename(U_59, V_60) | ~jules_forename(U_59, V_60)))). % 17.34/5.82 tff(c_62, plain, (![U_61, V_62]: (~unisex(U_61, V_62) | ~male(U_61, V_62)))). % 17.34/5.82 tff(c_50, plain, (![U_49, V_50]: (animate(U_49, V_50) | ~human_person(U_49, V_50)))). % 17.34/5.82 tff(c_38, plain, (![U_37, V_38]: (thing(U_37, V_38) | ~entity(U_37, V_38)))). % 17.34/5.82 tff(c_64, plain, (![U_63, V_64]: (~specific(U_63, V_64) | ~general(U_63, V_64)))). % 17.34/5.82 tff(c_34, plain, (![U_33, V_34]: (organism(U_33, V_34) | ~human_person(U_33, V_34)))). % 17.34/5.82 tff(c_48, plain, (![U_47, V_48]: (human(U_47, V_48) | ~human_person(U_47, V_48)))). % 17.34/5.82 tff(c_46, plain, (![U_45, V_46]: (living(U_45, V_46) | ~organism(U_45, V_46)))). % 17.34/5.82 tff(c_178, plain, (be(skc8, skc9, skc10, skc10))). % 17.34/5.82 tff(c_176, plain, (of(skc8, skc11, skc10))). % 17.34/5.82 tff(c_170, plain, (of(skc8, skc14, skc15))). % 17.34/5.83 tff(c_172, plain, (agent(skc8, skc13, skc15))). % 17.34/5.83 tff(c_174, plain, (theme(skc8, skc13, skc12))). % 17.34/5.83 tff(c_146, plain, (man(skc8, skc15))). % 17.34/5.83 tff(c_148, plain, (forename(skc8, skc14))). % 17.34/5.83 tff(c_150, plain, (vincent_forename(skc8, skc14))). % 17.34/5.83 tff(c_168, plain, (proposition(skc8, skc12))). % 17.34/5.83 tff(c_166, plain, (accessible_world(skc8, skc12))). % 17.34/5.83 tff(c_164, plain, (state(skc8, skc9))). % 17.34/5.83 tff(c_162, plain, (man(skc8, skc10))). % 17.34/5.83 tff(c_152, plain, (event(skc8, skc13))). % 17.34/5.83 tff(c_154, plain, (present(skc8, skc13))). % 17.34/5.83 tff(c_156, plain, (think_believe_consider(skc8, skc13))). % 17.34/5.83 tff(c_158, plain, (jules_forename(skc8, skc11))). % 17.34/5.83 tff(c_160, plain, (forename(skc8, skc11))). % 17.34/5.83 tff(c_144, plain, (actual_world(skc8))). % 17.34/5.83 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.34/5.83 %------------------------------------------------------------------------------