%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP248-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art07.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 2018MB % OS : Linux 2.6.26.8-57.fc8 % CPULimit : 300s % DateTime : Sun Jan 9 23:09:25 EST 2011 % Result : Satisfiable 108.62s % Output : Assurance 108.62s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % o===================================o % | EQuality TRAnsFOrmation | % | bthomas@informatik.uni-koblenz.de | % o===================================o % $Revision: 1.14 $ % reading /tmp/NLP248-1+eq_rstfp.tme % result written to : /tmp/NLP248-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP248-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP248-1+eq_rstfp-eqt.tme % System...................: Linux art07.cs.miami.edu 2.6.26.8-57.fc8 #1 SMP Thu Dec 18 19:19:45 EST 2008 i686 i686 i386 GNU/Linux % Automatic mode...........: on % Time limit...............: 300 seconds % Current restart interval.: 157 seconds % Restart with =-axioms....: 225 seconds % Initial interpretation...: [+(_9667)] % Clause set type..........: Horn, with equality % Equality transformation..: on % Non-constant functions...: yes % Term depth settings......: 3/2 (Init/Increment) % unit_extend..............: on % splitting type...........: exact % Final tree statistics: % Tree for clause set......: with equality transformation applied % # Restarts...............: 0 % Term depth limit.........: 5 % # Splits.................: 0 % # Commits................: 0 % # Unit extension steps...: 1245 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 108.13 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc20, skf1(V_2447_9741))) % -(tpos(skc18, skf1(V_2447_9751))) % -(tpos(skc24, skf1(V_2447_9761))) % -(tpos(skc25, skf1(V_2447_9771))) % -(jules_forename(skc14, skf1(V_2447_9781))) % -(vincent_forename(skc14, skf1(V_2447_9791))) % -(jules_forename(skc16, skc26)) % -(vincent_forename(skc16, skc26)) % -(skc18(skf1(V_2447_9814))) % -(skc20(skf1(V_2447_9823))) % -(skc25(skf1(V_2447_9832))) % -(skc24(skf1(V_2447_9841))) % -(jules_forename(skc13, skf1(V_2447_9851))) % -(vincent_forename(skc13, skf1(V_2447_9861))) % -(tpos(skc16, skf1(V_2447_9871))) % -(tpos(skc14, skf1(V_2447_9881))) % -(be(U_2501_9891, V_2502_9892, skf1(V_2447_9895), skc18)) % -(be(U_2479_9905, V_2480_9906, skc18, skf1(V_2447_9909))) % -(be(U_2501_9919, V_2502_9920, skf1(V_2447_9923), skc20)) % -(be(U_2479_9933, V_2480_9934, skc20, skf1(V_2447_9937))) % -(be(U_2501_9947, V_2502_9948, skf1(V_2447_9951), skc25)) % -(be(U_2479_9961, V_2480_9962, skc25, skf1(V_2447_9965))) % -(be(U_2501_9975, V_2502_9976, skf1(V_2447_9979), skc24)) % -(be(U_2479_9989, V_2480_9990, skc24, skf1(V_2447_9993))) % -(be(U_2501_10003, V_2502_10004, skc20, skc26)) % -(be(U_2479_10014, V_2480_10015, skc26, skc20)) % -(be(U_2501_10025, V_2502_10026, skc18, skc26)) % -(be(U_2479_10036, V_2480_10037, skc26, skc18)) % -(be(U_2501_10047, V_2502_10048, skc24, skc26)) % -(be(U_2479_10058, V_2480_10059, skc26, skc24)) % -(be(U_2501_10069, V_2502_10070, skc25, skc26)) % -(be(U_2479_10080, V_2480_10081, skc26, skc25)) % -(forename(skc14, skf1(V_2447_10091))) % -(forename(skc16, skc26)) % -(be(U_2501_10108, V_2502_10109, skf1(V_2447_10112), skc16)) % -(be(U_2479_10122, V_2480_10123, skc16, skf1(V_2447_10126))) % -(forename(skc13, skf1(V_2447_10136))) % -(jules_forename(skc16, skf1(V_2447_10146))) % -(vincent_forename(skc16, skf1(V_2447_10156))) % -(skc14(skf1(V_2447_10165))) % -(skc16(skf1(V_2447_10174))) % -(tpos(skf1(V_2447_10184), skc18)) % -(tpos(skc26, skc18)) % -(be(U_2501_10201, V_2502_10202, skc22, skc18)) % -(be(U_2479_10212, V_2480_10213, skc18, skc22)) % -(be(U_2501_10223, V_2502_10224, skc15, skc18)) % -(be(U_2479_10234, V_2480_10235, skc18, skc15)) % -(be(U_2501_10245, V_2502_10246, skc17, skc18)) % -(be(U_2479_10256, V_2480_10257, skc18, skc17)) % -(tpos(skf1(V_2447_10267), skc20)) % -(tpos(skc26, skc20)) % -(be(U_2501_10284, V_2502_10285, skc22, skc20)) % -(be(U_2479_10295, V_2480_10296, skc20, skc22)) % -(be(U_2501_10306, V_2502_10307, skc15, skc20)) % -(be(U_2479_10317, V_2480_10318, skc20, skc15)) % -(be(U_2501_10328, V_2502_10329, skc17, skc20)) % -(be(U_2479_10339, V_2480_10340, skc20, skc17)) % -(tpos(skf1(V_2447_10350), skc25)) % -(tpos(skc26, skc25)) % -(be(U_2501_10367, V_2502_10368, skc22, skc25)) % -(be(U_2479_10378, V_2480_10379, skc25, skc22)) % -(be(U_2501_10389, V_2502_10390, skc15, skc25)) % -(be(U_2479_10400, V_2480_10401, skc25, skc15)) % -(be(U_2501_10411, V_2502_10412, skc17, skc25)) % -(be(U_2479_10422, V_2480_10423, skc25, skc17)) % -(tpos(skf1(V_2447_10433), skc24)) % -(tpos(skc26, skc24)) % -(be(U_2501_10450, V_2502_10451, skc22, skc24)) % -(be(U_2479_10461, V_2480_10462, skc24, skc22)) % -(be(U_2501_10472, V_2502_10473, skc15, skc24)) % -(be(U_2479_10483, V_2480_10484, skc24, skc15)) % -(be(U_2501_10494, V_2502_10495, skc17, skc24)) % -(be(U_2479_10505, V_2480_10506, skc24, skc17)) % -(tpos(skc20, skc26)) % -(tpos(skc18, skc26)) % -(tpos(skc24, skc26)) % -(tpos(skc25, skc26)) % -(be(U_2501_10544, V_2502_10545, skc16, skc26)) % -(be(U_2479_10555, V_2480_10556, skc26, skc16)) % -(be(U_2501_10566, V_2502_10567, skf1(V_2447_10570), skc14)) % -(be(U_2479_10580, V_2480_10581, skc14, skf1(V_2447_10584))) % -(be(U_2501_10594, V_2502_10595, skc26, skc14)) % -(be(U_2479_10605, V_2480_10606, skc14, skc26)) % -(jules_forename(skc14, skc22)) % -(vincent_forename(skc14, skc22)) % -(jules_forename(skc16, skc22)) % -(vincent_forename(skc16, skc22)) % -(tpos(skc20, skc22)) % -(tpos(skc18, skc22)) % -(tpos(skc24, skc22)) % -(tpos(skc25, skc22)) % -(human_person(skc14, skf1(V_2447_10672))) % -(relname(skc14, skf1(V_2447_10682))) % -(proposition(skc14, skf1(V_2447_10692))) % -(human_person(skc16, skc26)) % -(relname(skc16, skc26)) % -(proposition(skc16, skc26)) % -(tpos(skf1(V_2447_10723), skc16)) % -(tpos(skc26, skc16)) % -(be(U_2501_10740, V_2502_10741, skc22, skc16)) % -(be(U_2479_10751, V_2480_10752, skc16, skc22)) % -(tpos(skc19, skf1(V_2447_10762))) % -(tpos(skc23, skf1(V_2447_10772))) % -(human_person(skc13, skf1(V_2447_10782))) % -(relname(skc13, skf1(V_2447_10792))) % -(forename(skc16, skf1(V_2447_10802))) % -(proposition(skc13, skf1(V_2447_10812))) % -(jules_forename(skc14, skc15)) % -(vincent_forename(skc14, skc15)) % -(jules_forename(skc16, skc15)) % -(vincent_forename(skc16, skc15)) % -(tpos(skc20, skc15)) % -(tpos(skc18, skc15)) % -(tpos(skc24, skc15)) % -(tpos(skc25, skc15)) % -(be(U_2501_10878, V_2502_10879, skc16, skc15)) % -(be(U_2479_10889, V_2480_10890, skc15, skc16)) % -(jules_forename(skc14, skc17)) % -(vincent_forename(skc14, skc17)) % -(jules_forename(skc16, skc17)) % -(vincent_forename(skc16, skc17)) % -(tpos(skc20, skc17)) % -(tpos(skc18, skc17)) % -(tpos(skc24, skc17)) % -(tpos(skc25, skc17)) % -(be(U_2501_10956, V_2502_10957, skc16, skc17)) % -(be(U_2479_10967, V_2480_10968, skc17, skc16)) % -(smoke(skc14, skc18)) % -(skf1(V_2447_10983, skc18)) % -(skc26(skc18)) % -(smoke(skc16, skc18)) % -(tpos(skc22, skc18)) % -(tpos(skc15, skc18)) % -(tpos(skc17, skc18)) % -(be(U_2501_11027, V_2502_11028, skc18, skc19)) % -(be(U_2479_11038, V_2480_11039, skc19, skc18)) % -(be(U_2501_11049, V_2502_11050, skc19, skc20)) % -(be(U_2479_11060, V_2480_11061, skc20, skc19)) % -(smoke(skc14, skc20)) % -(skf1(V_2447_11076, skc20)) % -(skc26(skc20)) % -(smoke(skc16, skc20)) % -(tpos(skc22, skc20)) % -(tpos(skc15, skc20)) % -(tpos(skc17, skc20)) % -(be(U_2501_11120, V_2502_11121, skc20, skc23)) % -(be(U_2479_11131, V_2480_11132, skc23, skc20)) % -(be(U_2501_11142, V_2502_11143, skc18, skc23)) % -(be(U_2479_11153, V_2480_11154, skc23, skc18)) % -(be(U_2501_11164, V_2502_11165, skc19, skc25)) % -(be(U_2479_11175, V_2480_11176, skc25, skc19)) % -(be(U_2501_11186, V_2502_11187, skc23, skc25)) % -(be(U_2479_11197, V_2480_11198, skc25, skc23)) % -(smoke(skc14, skc25)) % -(skf1(V_2447_11213, skc25)) % -(skc26(skc25)) % -(smoke(skc16, skc25)) % -(tpos(skc22, skc25)) % -(tpos(skc15, skc25)) % -(tpos(skc17, skc25)) % -(be(U_2501_11257, V_2502_11258, skc19, skc24)) % -(be(U_2479_11268, V_2480_11269, skc24, skc19)) % -(be(U_2501_11279, V_2502_11280, skc23, skc24)) % -(be(U_2479_11290, V_2480_11291, skc24, skc23)) % -(smoke(skc14, skc24)) % -(skf1(V_2447_11306, skc24)) % -(skc26(skc24)) % -(smoke(skc16, skc24)) % -(tpos(skc22, skc24)) % -(tpos(skc15, skc24)) % -(tpos(skc17, skc24)) % -(skc18(skc26)) % -(skc20(skc26)) % -(skc25(skc26)) % -(skc24(skc26)) % -(jules_forename(skc13, skc26)) % -(vincent_forename(skc13, skc26)) % -(tpos(skc16, skc26)) % -(tpos(skc14, skc26)) % -(tpos(skf1(V_2447_11402), skc14)) % -(tpos(skc26, skc14)) % -(be(U_2501_11419, V_2502_11420, skc22, skc14)) % -(be(U_2479_11430, V_2480_11431, skc14, skc22)) % -(be(U_2501_11441, V_2502_11442, skc15, skc14)) % -(be(U_2479_11452, V_2480_11453, skc14, skc15)) % -(be(U_2501_11463, V_2502_11464, skc17, skc14)) % -(be(U_2479_11474, V_2480_11475, skc14, skc17)) % -(forename(skc14, skc22)) % -(forename(skc16, skc22)) % -(skc18(skc22)) % -(skc20(skc22)) % -(skc25(skc22)) % -(skc24(skc22)) % -(jules_forename(skc13, skc22)) % -(vincent_forename(skc13, skc22)) % -(tpos(skc16, skc22)) % -(tpos(skc14, skc22)) % -(organism(skc14, skf1(V_2447_11551))) % -(relation(skc14, skf1(V_2447_11561))) % -(organism(skc16, skc26)) % -(relation(skc16, skc26)) % -(smoke(skc14, skc16)) % -(skf1(V_2447_11590, skc16)) % -(skc26(skc16)) % -(smoke(skc16, skc16)) % -(tpos(skc22, skc16)) % -(tpos(skc15, skc16)) % -(tpos(skc17, skc16)) % -(skc19(skf1(V_2447_11633))) % -(skc23(skf1(V_2447_11642))) % -(organism(skc13, skf1(V_2447_11652))) % -(human_person(skc16, skf1(V_2447_11662))) % -(relation(skc13, skf1(V_2447_11672))) % -(relname(skc16, skf1(V_2447_11682))) % -(proposition(skc16, skf1(V_2447_11692))) % -(forename(skc14, skc15)) % -(forename(skc16, skc15)) % -(skc18(skc15)) % -(skc20(skc15)) % -(skc25(skc15)) % -(skc24(skc15)) % -(jules_forename(skc13, skc15)) % -(vincent_forename(skc13, skc15)) % -(tpos(skc16, skc15)) % -(tpos(skc14, skc15)) % -(forename(skc14, skc17)) % -(forename(skc16, skc17)) % -(skc18(skc17)) % -(skc20(skc17)) % -(skc25(skc17)) % -(skc24(skc17)) % -(jules_forename(skc13, skc17)) % -(vincent_forename(skc13, skc17)) % -(tpos(skc16, skc17)) % -(tpos(skc14, skc17)) % -(tpos(skc19, skc18)) % -(tpos(skc23, skc18)) % -(organism(skc14, skc18)) % -(state(skc14, skc18)) % -(event(skc14, skc18)) % -(organism(skc16, skc18)) % -(state(skc16, skc18)) % -(event(skc16, skc18)) % -(skc22(skc18)) % -(skc15(skc18)) % -(skc17(skc18)) % -(smoke(skc13, skc18)) % -(jules_forename(skc14, skc19)) % -(vincent_forename(skc14, skc19)) % -(jules_forename(skc16, skc19)) % -(vincent_forename(skc16, skc19)) % -(be(U_2501_11943, V_2502_11944, skf1(V_2447_11947), skc19)) % -(be(U_2479_11957, V_2480_11958, skc19, skf1(V_2447_11961))) % -(tpos(skc20, skc19)) % -(tpos(skc18, skc19)) % -(tpos(skc24, skc19)) % -(tpos(skc25, skc19)) % -(be(U_2501_11999, V_2502_12000, skc16, skc19)) % -(be(U_2479_12010, V_2480_12011, skc19, skc16)) % -(tpos(skc19, skc20)) % -(tpos(skc23, skc20)) % -(organism(skc14, skc20)) % -(state(skc14, skc20)) % -(event(skc14, skc20)) % -(organism(skc16, skc20)) % -(state(skc16, skc20)) % -(event(skc16, skc20)) % -(skc22(skc20)) % -(skc15(skc20)) % -(skc17(skc20)) % -(smoke(skc13, skc20)) % -(jules_forename(skc14, skc23)) % -(vincent_forename(skc14, skc23)) % -(jules_forename(skc16, skc23)) % -(vincent_forename(skc16, skc23)) % -(be(U_2501_12130, V_2502_12131, skf1(V_2447_12134), skc23)) % -(be(U_2479_12144, V_2480_12145, skc23, skf1(V_2447_12148))) % -(tpos(skc20, skc23)) % -(tpos(skc18, skc23)) % -(tpos(skc24, skc23)) % -(tpos(skc25, skc23)) % -(be(U_2501_12186, V_2502_12187, skc16, skc23)) % -(be(U_2479_12197, V_2480_12198, skc23, skc16)) % -(tpos(skc19, skc25)) % -(tpos(skc23, skc25)) % -(organism(skc14, skc25)) % -(state(skc14, skc25)) % -(event(skc14, skc25)) % -(organism(skc16, skc25)) % -(state(skc16, skc25)) % -(event(skc16, skc25)) % -(skc22(skc25)) % -(skc15(skc25)) % -(skc17(skc25)) % -(smoke(skc13, skc25)) % -(tpos(skc19, skc24)) % -(tpos(skc23, skc24)) % -(organism(skc14, skc24)) % -(state(skc14, skc24)) % -(event(skc14, skc24)) % -(organism(skc16, skc24)) % -(state(skc16, skc24)) % -(event(skc16, skc24)) % -(skc22(skc24)) % -(skc15(skc24)) % -(skc17(skc24)) % -(smoke(skc13, skc24)) % -(be(U_2501_12370, V_2502_12371, skc19, skc26)) % -(be(U_2479_12381, V_2480_12382, skc26, skc19)) % -(be(U_2501_12392, V_2502_12393, skc23, skc26)) % -(be(U_2479_12403, V_2480_12404, skc26, skc23)) % -(forename(skc13, skc26)) % -(jules_forename(skc14, skc26)) % -(vincent_forename(skc14, skc26)) % -(skc14(skc26)) % -(skc16(skc26)) % -(be(U_2501_12447, V_2502_12448, skc19, skc14)) % -(be(U_2479_12458, V_2480_12459, skc14, skc19)) % -(be(U_2501_12469, V_2502_12470, skc23, skc14)) % -(be(U_2479_12480, V_2480_12481, skc14, skc23)) % -(smoke(skc14, skc14)) % -(skf1(V_2447_12496, skc14)) % -(skc26(skc14)) % -(smoke(skc16, skc14)) % -(tpos(skc22, skc14)) % -(tpos(skc15, skc14)) % -(tpos(skc17, skc14)) % -(human_person(skc14, skc22)) % -(human_person(skc16, skc22)) % -(relname(skc14, skc22)) % -(proposition(skc14, skc22)) % -(relname(skc16, skc22)) % -(proposition(skc16, skc22)) % -(forename(skc13, skc22)) % -(skc14(skc22)) % -(skc16(skc22)) % -(man(skc14, skf1(V_2447_12601))) % -(entity(skc14, skf1(V_2447_12611))) % -(abstraction(skc14, skf1(V_2447_12621))) % -(man(skc16, skc26)) % -(entity(skc16, skc26)) % -(abstraction(skc16, skc26)) % -(tpos(skc19, skc16)) % -(tpos(skc23, skc16)) % -(organism(skc14, skc16)) % -(state(skc14, skc16)) % -(event(skc14, skc16)) % -(organism(skc16, skc16)) % -(state(skc16, skc16)) % -(event(skc16, skc16)) % -(skc22(skc16)) % -(skc15(skc16)) % -(skc17(skc16)) % -(smoke(skc13, skc16)) % -(man(skc13, skf1(V_2447_12733))) % -(entity(skc13, skf1(V_2447_12743))) % -(organism(skc16, skf1(V_2447_12753))) % -(abstraction(skc13, skf1(V_2447_12763))) % -(relation(skc16, skf1(V_2447_12773))) % -(human_person(skc14, skc15)) % -(human_person(skc16, skc15)) % -(relname(skc14, skc15)) % -(proposition(skc14, skc15)) % -(relname(skc16, skc15)) % -(proposition(skc16, skc15)) % -(forename(skc13, skc15)) % -(skc14(skc15)) % -(skc16(skc15)) % -(human_person(skc14, skc17)) % -(human_person(skc16, skc17)) % -(relname(skc14, skc17)) % -(proposition(skc14, skc17)) % -(relname(skc16, skc17)) % -(proposition(skc16, skc17)) % -(forename(skc13, skc17)) % -(skc14(skc17)) % -(skc16(skc17)) % -(man(skc14, skc18)) % -(man(skc16, skc18)) % -(skc19(skc18)) % -(skc23(skc18)) % -(entity(skc14, skc18)) % -(eventuality(skc14, skc18)) % -(entity(skc16, skc18)) % -(eventuality(skc16, skc18)) % -(organism(skc13, skc18)) % -(state(skc13, skc18)) % -(event(skc13, skc18)) % -(human_person(skc14, skc18)) % -(human_person(skc16, skc18)) % -(forename(skc14, skc19)) % -(forename(skc16, skc19)) % -(tpos(skf1(V_2447_13008), skc19)) % -(tpos(skc26, skc19)) % -(skc18(skc19)) % -(skc20(skc19)) % -(skc25(skc19)) % -(skc24(skc19)) % -(jules_forename(skc13, skc19)) % -(vincent_forename(skc13, skc19)) % -(tpos(skc16, skc19)) % -(tpos(skc14, skc19)) % -(be(U_2501_13077, V_2502_13078, skc22, skc19)) % -(be(U_2479_13088, V_2480_13089, skc19, skc22)) % -(be(U_2501_13099, V_2502_13100, skc15, skc19)) % -(be(U_2479_13110, V_2480_13111, skc19, skc15)) % -(be(U_2501_13121, V_2502_13122, skc17, skc19)) % -(be(U_2479_13132, V_2480_13133, skc19, skc17)) % -(man(skc14, skc20)) % -(man(skc16, skc20)) % -(skc19(skc20)) % -(skc23(skc20)) % -(entity(skc14, skc20)) % -(eventuality(skc14, skc20)) % -(entity(skc16, skc20)) % -(eventuality(skc16, skc20)) % -(organism(skc13, skc20)) % -(state(skc13, skc20)) % -(event(skc13, skc20)) % -(human_person(skc14, skc20)) % -(human_person(skc16, skc20)) % -(forename(skc14, skc23)) % -(forename(skc16, skc23)) % -(tpos(skf1(V_2447_13246), skc23)) % -(tpos(skc26, skc23)) % -(skc18(skc23)) % -(skc20(skc23)) % -(skc25(skc23)) % -(skc24(skc23)) % -(jules_forename(skc13, skc23)) % -(vincent_forename(skc13, skc23)) % -(tpos(skc16, skc23)) % -(tpos(skc14, skc23)) % -(be(U_2501_13315, V_2502_13316, skc22, skc23)) % -(be(U_2479_13326, V_2480_13327, skc23, skc22)) % -(be(U_2501_13337, V_2502_13338, skc15, skc23)) % -(be(U_2479_13348, V_2480_13349, skc23, skc15)) % -(be(U_2501_13359, V_2502_13360, skc17, skc23)) % -(be(U_2479_13370, V_2480_13371, skc23, skc17)) % -(man(skc14, skc25)) % -(man(skc16, skc25)) % -(skc19(skc25)) % -(skc23(skc25)) % -(entity(skc14, skc25)) % -(eventuality(skc14, skc25)) % -(entity(skc16, skc25)) % -(eventuality(skc16, skc25)) % -(organism(skc13, skc25)) % -(state(skc13, skc25)) % -(event(skc13, skc25)) % -(human_person(skc14, skc25)) % -(human_person(skc16, skc25)) % -(man(skc14, skc24)) % -(man(skc16, skc24)) % -(skc19(skc24)) % -(skc23(skc24)) % -(entity(skc14, skc24)) % -(eventuality(skc14, skc24)) % -(entity(skc16, skc24)) % -(eventuality(skc16, skc24)) % -(organism(skc13, skc24)) % -(state(skc13, skc24)) % -(event(skc13, skc24)) % -(human_person(skc14, skc24)) % -(human_person(skc16, skc24)) % -(tpos(skc19, skc26)) % -(tpos(skc23, skc26)) % -(human_person(skc13, skc26)) % -(relname(skc13, skc26)) % -(forename(skc14, skc26)) % -(proposition(skc13, skc26)) % -(tpos(skc19, skc14)) % -(tpos(skc23, skc14)) % -(organism(skc14, skc14)) % -(state(skc14, skc14)) % -(event(skc14, skc14)) % -(organism(skc16, skc14)) % -(state(skc16, skc14)) % -(event(skc16, skc14)) % -(skc22(skc14)) % -(skc15(skc14)) % -(skc17(skc14)) % -(smoke(skc13, skc14)) % -(tpos(skc19, skc22)) % -(tpos(skc23, skc22)) % -(organism(skc14, skc22)) % -(organism(skc16, skc22)) % -(human_person(skc13, skc22)) % -(relation(skc14, skc22)) % -(relation(skc16, skc22)) % -(relname(skc13, skc22)) % -(proposition(skc13, skc22)) % -(male(skc14, skf1(V_2447_13745))) % -(existent(skc14, skf1(V_2447_13755))) % -(general(skc14, skf1(V_2447_13765))) % +(singleton(skc14, skf1(V_2447_13775))) % -(male(skc16, skc26)) % -(existent(skc16, skc26)) % -(general(skc16, skc26)) % +(singleton(skc16, skc26)) % -(man(skc14, skc16)) % -(man(skc16, skc16)) % -(skc19(skc16)) % -(skc23(skc16)) % -(entity(skc14, skc16)) % -(eventuality(skc14, skc16)) % -(entity(skc16, skc16)) % -(eventuality(skc16, skc16)) % -(organism(skc13, skc16)) % -(state(skc13, skc16)) % -(event(skc13, skc16)) % -(human_person(skc14, skc16)) % -(human_person(skc16, skc16)) % -(male(skc13, skf1(V_2447_13902))) % -(man(skc16, skf1(V_2447_13912))) % -(existent(skc13, skf1(V_2447_13922))) % -(entity(skc16, skf1(V_2447_13932))) % -(general(skc13, skf1(V_2447_13942))) % -(abstraction(skc16, skf1(V_2447_13952))) % -(tpos(skc19, skc15)) % -(tpos(skc23, skc15)) % -(organism(skc14, skc15)) % -(organism(skc16, skc15)) % -(human_person(skc13, skc15)) % -(relation(skc14, skc15)) % -(relation(skc16, skc15)) % -(relname(skc13, skc15)) % -(proposition(skc13, skc15)) % -(tpos(skc19, skc17)) % -(tpos(skc23, skc17)) % -(organism(skc14, skc17)) % -(organism(skc16, skc17)) % -(human_person(skc13, skc17)) % -(relation(skc14, skc17)) % -(relation(skc16, skc17)) % -(relname(skc13, skc17)) % -(proposition(skc13, skc17)) % -(male(skc14, skc18)) % -(male(skc16, skc18)) % -(man(skc13, skc18)) % -(specific(skc14, skc18)) % -(specific(skc16, skc18)) % -(entity(skc13, skc18)) % -(eventuality(skc13, skc18)) % -(human(skc14, skc18)) % -(human(skc16, skc18)) % -(human_person(skc13, skc18)) % +(singleton(skc14, skc18)) % +(singleton(skc16, skc18)) % -(relname(skc14, skc19)) % -(proposition(skc14, skc19)) % -(smoke(skc14, skc19)) % -(relname(skc16, skc19)) % -(proposition(skc16, skc19)) % -(skf1(V_2447_14205, skc19)) % -(skc26(skc19)) % -(smoke(skc16, skc19)) % -(forename(skc13, skc19)) % -(skc14(skc19)) % -(skc16(skc19)) % -(tpos(skc22, skc19)) % -(tpos(skc15, skc19)) % -(tpos(skc17, skc19)) % -(nonexistent(skc14, skc19)) % -(nonexistent(skc16, skc19)) % -(general(skc14, skc19)) % -(general(skc16, skc19)) % +(singleton(skc14, skc19)) % +(singleton(skc16, skc19)) % -(male(skc14, skc20)) % -(male(skc16, skc20)) % -(man(skc13, skc20)) % -(specific(skc14, skc20)) % -(specific(skc16, skc20)) % -(entity(skc13, skc20)) % -(eventuality(skc13, skc20)) % -(human(skc14, skc20)) % -(human(skc16, skc20)) % -(human_person(skc13, skc20)) % +(singleton(skc14, skc20)) % +(singleton(skc16, skc20)) % -(relname(skc14, skc23)) % -(proposition(skc14, skc23)) % -(smoke(skc14, skc23)) % -(relname(skc16, skc23)) % -(proposition(skc16, skc23)) % -(skf1(V_2447_14427, skc23)) % -(skc26(skc23)) % -(smoke(skc16, skc23)) % -(forename(skc13, skc23)) % -(skc14(skc23)) % -(skc16(skc23)) % -(tpos(skc22, skc23)) % -(tpos(skc15, skc23)) % -(tpos(skc17, skc23)) % -(nonexistent(skc14, skc23)) % -(nonexistent(skc16, skc23)) % -(general(skc14, skc23)) % -(general(skc16, skc23)) % +(singleton(skc14, skc23)) % +(singleton(skc16, skc23)) % -(male(skc14, skc25)) % -(male(skc16, skc25)) % -(man(skc13, skc25)) % -(specific(skc14, skc25)) % -(specific(skc16, skc25)) % -(entity(skc13, skc25)) % -(eventuality(skc13, skc25)) % -(human(skc14, skc25)) % -(human(skc16, skc25)) % -(human_person(skc13, skc25)) % +(singleton(skc14, skc25)) % +(singleton(skc16, skc25)) % -(male(skc14, skc24)) % -(male(skc16, skc24)) % -(man(skc13, skc24)) % -(specific(skc14, skc24)) % -(specific(skc16, skc24)) % -(entity(skc13, skc24)) % -(eventuality(skc13, skc24)) % -(human(skc14, skc24)) % -(human(skc16, skc24)) % -(human_person(skc13, skc24)) % +(singleton(skc14, skc24)) % +(singleton(skc16, skc24)) % -(skc19(skc26)) % -(skc23(skc26)) % -(organism(skc13, skc26)) % -(human_person(skc14, skc26)) % -(relation(skc13, skc26)) % -(relname(skc14, skc26)) % -(proposition(skc14, skc26)) % -(man(skc14, skc14)) % -(man(skc16, skc14)) % -(skc19(skc14)) % -(skc23(skc14)) % -(entity(skc14, skc14)) % -(eventuality(skc14, skc14)) % -(entity(skc16, skc14)) % -(eventuality(skc16, skc14)) % -(organism(skc13, skc14)) % -(state(skc13, skc14)) % -(event(skc13, skc14)) % -(human_person(skc14, skc14)) % -(human_person(skc16, skc14)) % -(man(skc14, skc22)) % -(man(skc16, skc22)) % -(skc19(skc22)) % -(skc23(skc22)) % -(entity(skc14, skc22)) % -(entity(skc16, skc22)) % -(organism(skc13, skc22)) % -(abstraction(skc14, skc22)) % -(abstraction(skc16, skc22)) % -(relation(skc13, skc22)) % +(unisex(skc14, skf1(V_2447_14904))) % +(nonexistent(skc14, skf1(V_2447_14914))) % +(specific(skc14, skf1(V_2447_14924))) % +(thing(skc14, skf1(V_2447_14934))) % +(unisex(skc16, skc26)) % +(nonexistent(skc16, skc26)) % +(specific(skc16, skc26)) % +(thing(skc16, skc26)) % -(male(skc14, skc16)) % -(male(skc16, skc16)) % -(man(skc13, skc16)) % -(specific(skc14, skc16)) % -(specific(skc16, skc16)) % -(entity(skc13, skc16)) % -(eventuality(skc13, skc16)) % -(human(skc14, skc16)) % -(human(skc16, skc16)) % -(human_person(skc13, skc16)) % +(singleton(skc14, skc16)) % +(singleton(skc16, skc16)) % -(male(skc16, skf1(V_2447_15056))) % -(existent(skc16, skf1(V_2447_15066))) % -(general(skc16, skf1(V_2447_15076))) % +(singleton(skc16, skf1(V_2447_15086))) % -(man(skc14, skc15)) % -(man(skc16, skc15)) % -(skc19(skc15)) % -(skc23(skc15)) % -(entity(skc14, skc15)) % -(entity(skc16, skc15)) % -(organism(skc13, skc15)) % -(abstraction(skc14, skc15)) % -(abstraction(skc16, skc15)) % -(relation(skc13, skc15)) % -(man(skc14, skc17)) % -(man(skc16, skc17)) % -(skc19(skc17)) % -(skc23(skc17)) % -(entity(skc14, skc17)) % -(entity(skc16, skc17)) % -(organism(skc13, skc17)) % -(abstraction(skc14, skc17)) % -(abstraction(skc16, skc17)) % -(relation(skc13, skc17)) % +(unisex(skc14, skc18)) % +(unisex(skc16, skc18)) % -(male(skc13, skc18)) % +(general(skc14, skc18)) % +(general(skc16, skc18)) % -(specific(skc13, skc18)) % +(nonhuman(skc14, skc18)) % +(nonhuman(skc16, skc18)) % -(human(skc13, skc18)) % +(thing(skc14, skc18)) % +(thing(skc16, skc18)) % +(singleton(skc13, skc18)) % -(relation(skc14, skc19)) % -(state(skc14, skc19)) % -(event(skc14, skc19)) % -(relation(skc16, skc19)) % -(state(skc16, skc19)) % -(event(skc16, skc19)) % -(relname(skc13, skc19)) % -(proposition(skc13, skc19)) % -(skc22(skc19)) % -(skc15(skc19)) % -(skc17(skc19)) % -(smoke(skc13, skc19)) % +(skc20(skc18)) % +(skc18(skc20)) % +(existent(skc14, skc19)) % +(existent(skc16, skc19)) % -(nonexistent(skc13, skc19)) % +(specific(skc14, skc19)) % +(specific(skc16, skc19)) % -(general(skc13, skc19)) % +(thing(skc14, skc19)) % +(thing(skc16, skc19)) % +(singleton(skc13, skc19)) % +(unisex(skc14, skc20)) % +(unisex(skc16, skc20)) % -(male(skc13, skc20)) % +(general(skc14, skc20)) % +(general(skc16, skc20)) % -(specific(skc13, skc20)) % +(nonhuman(skc14, skc20)) % +(nonhuman(skc16, skc20)) % -(human(skc13, skc20)) % +(thing(skc14, skc20)) % +(thing(skc16, skc20)) % +(singleton(skc13, skc20)) % -(relation(skc14, skc23)) % -(state(skc14, skc23)) % -(event(skc14, skc23)) % -(relation(skc16, skc23)) % -(state(skc16, skc23)) % -(event(skc16, skc23)) % -(relname(skc13, skc23)) % -(proposition(skc13, skc23)) % -(skc22(skc23)) % -(skc15(skc23)) % -(skc17(skc23)) % -(smoke(skc13, skc23)) % +(skc24(skc25)) % +(skc25(skc24)) % +(existent(skc14, skc23)) % +(existent(skc16, skc23)) % -(nonexistent(skc13, skc23)) % +(specific(skc14, skc23)) % +(specific(skc16, skc23)) % -(general(skc13, skc23)) % +(thing(skc14, skc23)) % +(thing(skc16, skc23)) % +(singleton(skc13, skc23)) % +(unisex(skc14, skc25)) % +(unisex(skc16, skc25)) % -(male(skc13, skc25)) % +(general(skc14, skc25)) % +(general(skc16, skc25)) % -(specific(skc13, skc25)) % +(nonhuman(skc14, skc25)) % +(nonhuman(skc16, skc25)) % -(human(skc13, skc25)) % +(thing(skc14, skc25)) % +(thing(skc16, skc25)) % +(singleton(skc13, skc25)) % +(unisex(skc14, skc24)) % +(unisex(skc16, skc24)) % -(male(skc13, skc24)) % +(general(skc14, skc24)) % +(general(skc16, skc24)) % -(specific(skc13, skc24)) % +(nonhuman(skc14, skc24)) % +(nonhuman(skc16, skc24)) % -(human(skc13, skc24)) % +(thing(skc14, skc24)) % +(thing(skc16, skc24)) % +(singleton(skc13, skc24)) % -(man(skc13, skc26)) % -(entity(skc13, skc26)) % -(organism(skc14, skc26)) % -(abstraction(skc13, skc26)) % -(relation(skc14, skc26)) % -(male(skc14, skc14)) % -(male(skc16, skc14)) % -(man(skc13, skc14)) % -(specific(skc14, skc14)) % -(specific(skc16, skc14)) % -(entity(skc13, skc14)) % -(eventuality(skc13, skc14)) % -(human(skc14, skc14)) % -(human(skc16, skc14)) % -(human_person(skc13, skc14)) % +(singleton(skc14, skc14)) % +(singleton(skc16, skc14)) % -(male(skc14, skc22)) % -(male(skc16, skc22)) % -(man(skc13, skc22)) % -(existent(skc14, skc22)) % -(existent(skc16, skc22)) % -(entity(skc13, skc22)) % -(general(skc14, skc22)) % -(general(skc16, skc22)) % -(abstraction(skc13, skc22)) % +(singleton(skc14, skc22)) % +(singleton(skc16, skc22)) % +(eventuality(skc14, skf1(V_2447_16076))) % +(theme(skc14, skc17, skc14)) % +(theme(skc16, skc17, skc14)) % +(theme(skc14, skc15, skc16)) % +(theme(skc16, skc15, skc16)) % +(eventuality(skc16, skc26)) % +(unisex(skc14, skc16)) % +(unisex(skc16, skc16)) % -(male(skc13, skc16)) % +(general(skc14, skc16)) % +(general(skc16, skc16)) % -(specific(skc13, skc16)) % +(nonhuman(skc14, skc16)) % +(nonhuman(skc16, skc16)) % -(human(skc13, skc16)) % +(thing(skc14, skc16)) % +(thing(skc16, skc16)) % +(singleton(skc13, skc16)) % +(unisex(skc16, skf1(V_2447_16209))) % +(nonexistent(skc16, skf1(V_2447_16219))) % +(specific(skc16, skf1(V_2447_16229))) % +(thing(skc16, skf1(V_2447_16239))) % -(male(skc14, skc15)) % -(male(skc16, skc15)) % -(man(skc13, skc15)) % -(existent(skc14, skc15)) % -(existent(skc16, skc15)) % -(entity(skc13, skc15)) % -(general(skc14, skc15)) % -(general(skc16, skc15)) % -(abstraction(skc13, skc15)) % +(singleton(skc14, skc15)) % +(singleton(skc16, skc15)) % -(male(skc14, skc17)) % -(male(skc16, skc17)) % -(man(skc13, skc17)) % -(existent(skc14, skc17)) % -(existent(skc16, skc17)) % -(entity(skc13, skc17)) % -(general(skc14, skc17)) % -(general(skc16, skc17)) % -(abstraction(skc13, skc17)) % +(singleton(skc14, skc17)) % +(singleton(skc16, skc17)) % +(abstraction(skc14, skc18)) % +(abstraction(skc16, skc18)) % +(unisex(skc13, skc18)) % +(general(skc13, skc18)) % +(nonhuman(skc13, skc18)) % +(thing(skc13, skc18)) % -(abstraction(skc14, skc19)) % -(eventuality(skc14, skc19)) % -(abstraction(skc16, skc19)) % -(eventuality(skc16, skc19)) % -(relation(skc13, skc19)) % -(state(skc13, skc19)) % -(event(skc13, skc19)) % -(nonhuman(skc14, skc19)) % -(nonhuman(skc16, skc19)) % +(living(skc14, skc19)) % +(living(skc16, skc19)) % +(impartial(skc14, skc19)) % +(impartial(skc16, skc19)) % +(tpos(skc20, skc20)) % +(tpos(skc20, skc18)) % +(tpos(skc18, skc20)) % +(tpos(skc18, skc18)) % +(entity(skc14, skc19)) % +(entity(skc16, skc19)) % +(existent(skc13, skc19)) % +(specific(skc13, skc19)) % +(thing(skc13, skc19)) % +(abstraction(skc14, skc20)) % +(abstraction(skc16, skc20)) % +(unisex(skc13, skc20)) % +(general(skc13, skc20)) % +(nonhuman(skc13, skc20)) % +(thing(skc13, skc20)) % -(abstraction(skc14, skc23)) % -(eventuality(skc14, skc23)) % -(abstraction(skc16, skc23)) % -(eventuality(skc16, skc23)) % -(relation(skc13, skc23)) % -(state(skc13, skc23)) % -(event(skc13, skc23)) % -(nonhuman(skc14, skc23)) % -(nonhuman(skc16, skc23)) % +(living(skc14, skc23)) % +(living(skc16, skc23)) % +(impartial(skc14, skc23)) % +(impartial(skc16, skc23)) % +(tpos(skc24, skc25)) % +(tpos(skc24, skc24)) % +(tpos(skc25, skc25)) % +(tpos(skc25, skc24)) % +(entity(skc14, skc23)) % +(entity(skc16, skc23)) % +(existent(skc13, skc23)) % +(specific(skc13, skc23)) % +(thing(skc13, skc23)) % +(abstraction(skc14, skc25)) % +(abstraction(skc16, skc25)) % +(unisex(skc13, skc25)) % +(general(skc13, skc25)) % +(nonhuman(skc13, skc25)) % +(thing(skc13, skc25)) % +(abstraction(skc14, skc24)) % +(abstraction(skc16, skc24)) % +(unisex(skc13, skc24)) % +(general(skc13, skc24)) % +(nonhuman(skc13, skc24)) % +(thing(skc13, skc24)) % -(male(skc13, skc26)) % -(man(skc14, skc26)) % -(existent(skc13, skc26)) % -(entity(skc14, skc26)) % -(general(skc13, skc26)) % -(abstraction(skc14, skc26)) % +(unisex(skc14, skc14)) % +(unisex(skc16, skc14)) % -(male(skc13, skc14)) % +(general(skc14, skc14)) % +(general(skc16, skc14)) % -(specific(skc13, skc14)) % +(nonhuman(skc14, skc14)) % +(nonhuman(skc16, skc14)) % -(human(skc13, skc14)) % +(thing(skc14, skc14)) % +(thing(skc16, skc14)) % +(singleton(skc13, skc14)) % +(unisex(skc14, skc22)) % +(unisex(skc16, skc22)) % -(male(skc13, skc22)) % +(nonexistent(skc14, skc22)) % +(nonexistent(skc16, skc22)) % -(existent(skc13, skc22)) % +(specific(skc14, skc22)) % +(specific(skc16, skc22)) % -(general(skc13, skc22)) % +(thing(skc14, skc22)) % +(thing(skc16, skc22)) % +(singleton(skc13, skc22)) % +(agent(skc14, skf1(skc19), skc19)) % +(agent(skc14, skf1(skc23), skc23)) % +(event(skc14, skf1(V_2447_17109))) % +(present(skc14, skf1(V_2447_17119))) % +(smoke(skc14, skf1(V_2447_17129))) % +(theme(skc13, skc17, skc14)) % +(theme(skc13, skc15, skc16)) % +(agent(skc16, skc26, skc23)) % +(smoke(skc16, skc26)) % +(present(skc16, skc26)) % +(event(skc16, skc26)) % +(abstraction(skc14, skc16)) % +(abstraction(skc16, skc16)) % +(unisex(skc13, skc16)) % +(general(skc13, skc16)) % +(nonhuman(skc13, skc16)) % +(thing(skc13, skc16)) % +(eventuality(skc16, skf1(V_2447_17226))) % +(unisex(skc14, skc15)) % +(unisex(skc16, skc15)) % -(male(skc13, skc15)) % +(nonexistent(skc14, skc15)) % +(nonexistent(skc16, skc15)) % -(existent(skc13, skc15)) % +(specific(skc14, skc15)) % +(specific(skc16, skc15)) % -(general(skc13, skc15)) % +(thing(skc14, skc15)) % +(thing(skc16, skc15)) % +(singleton(skc13, skc15)) % +(unisex(skc14, skc17)) % +(unisex(skc16, skc17)) % -(male(skc13, skc17)) % +(nonexistent(skc14, skc17)) % +(nonexistent(skc16, skc17)) % -(existent(skc13, skc17)) % +(specific(skc14, skc17)) % +(specific(skc16, skc17)) % -(general(skc13, skc17)) % +(thing(skc14, skc17)) % +(thing(skc16, skc17)) % +(singleton(skc13, skc17)) % +(relation(skc14, skc18)) % +(relation(skc16, skc18)) % +(abstraction(skc13, skc18)) % -(unisex(skc14, skc19)) % -(unisex(skc16, skc19)) % -(abstraction(skc13, skc19)) % -(eventuality(skc13, skc19)) % +(animate(skc14, skc19)) % +(animate(skc16, skc19)) % +(human(skc14, skc19)) % +(human(skc16, skc19)) % -(nonhuman(skc13, skc19)) % +(organism(skc14, skc19)) % +(organism(skc16, skc19)) % +(living(skc13, skc19)) % +(impartial(skc13, skc19)) % +(entity(skc13, skc19)) % +(relation(skc14, skc20)) % +(relation(skc16, skc20)) % +(abstraction(skc13, skc20)) % -(unisex(skc14, skc23)) % -(unisex(skc16, skc23)) % -(abstraction(skc13, skc23)) % -(eventuality(skc13, skc23)) % +(animate(skc14, skc23)) % +(animate(skc16, skc23)) % +(human(skc14, skc23)) % +(human(skc16, skc23)) % -(nonhuman(skc13, skc23)) % +(organism(skc14, skc23)) % +(organism(skc16, skc23)) % +(living(skc13, skc23)) % +(impartial(skc13, skc23)) % +(entity(skc13, skc23)) % +(relation(skc14, skc25)) % +(relation(skc16, skc25)) % +(abstraction(skc13, skc25)) % +(relation(skc14, skc24)) % +(relation(skc16, skc24)) % +(abstraction(skc13, skc24)) % -(male(skc14, skc26)) % -(existent(skc14, skc26)) % -(general(skc14, skc26)) % +(singleton(skc14, skc26)) % +(abstraction(skc14, skc14)) % +(abstraction(skc16, skc14)) % +(unisex(skc13, skc14)) % +(general(skc13, skc14)) % +(nonhuman(skc13, skc14)) % +(thing(skc13, skc14)) % +(event(skc14, skc22)) % +(event(skc16, skc22)) % +(eventuality(skc14, skc22)) % +(eventuality(skc16, skc22)) % +(unisex(skc13, skc22)) % +(nonexistent(skc13, skc22)) % +(specific(skc13, skc22)) % +(thing(skc13, skc22)) % +(skc16(skc14)) % +(skc14(skc16)) % +(relation(skc14, skc16)) % +(relation(skc16, skc16)) % +(abstraction(skc13, skc16)) % +(agent(skc16, skf1(skc23), skc23)) % +(agent(skc16, skf1(skc19), skc19)) % +(event(skc16, skf1(V_2447_17863))) % +(present(skc16, skf1(V_2447_17873))) % +(smoke(skc16, skf1(V_2447_17883))) % +(eventuality(skc14, skc15)) % +(eventuality(skc16, skc15)) % +(unisex(skc13, skc15)) % +(nonexistent(skc13, skc15)) % +(specific(skc13, skc15)) % +(thing(skc13, skc15)) % +(eventuality(skc14, skc17)) % +(eventuality(skc16, skc17)) % +(unisex(skc13, skc17)) % +(nonexistent(skc13, skc17)) % +(specific(skc13, skc17)) % +(thing(skc13, skc17)) % +(relname(skc14, skc18)) % +(relname(skc16, skc18)) % +(relation(skc13, skc18)) % +(male(skc14, skc19)) % +(male(skc16, skc19)) % -(unisex(skc13, skc19)) % +(human_person(skc14, skc19)) % +(human_person(skc16, skc19)) % +(animate(skc13, skc19)) % +(human(skc13, skc19)) % +(organism(skc13, skc19)) % +(relname(skc14, skc20)) % +(relname(skc16, skc20)) % +(relation(skc13, skc20)) % +(male(skc14, skc23)) % +(male(skc16, skc23)) % -(unisex(skc13, skc23)) % +(human_person(skc14, skc23)) % +(human_person(skc16, skc23)) % +(animate(skc13, skc23)) % +(human(skc13, skc23)) % +(organism(skc13, skc23)) % +(relname(skc14, skc25)) % +(relname(skc16, skc25)) % +(relation(skc13, skc25)) % +(relname(skc14, skc24)) % +(relname(skc16, skc24)) % +(relation(skc13, skc24)) % +(unisex(skc14, skc26)) % +(nonexistent(skc14, skc26)) % +(specific(skc14, skc26)) % +(thing(skc14, skc26)) % +(relation(skc14, skc14)) % +(relation(skc16, skc14)) % +(abstraction(skc13, skc14)) % +(be(skc14, skc22, skc23, skc23)) % +(be(skc16, skc22, skc23, skc23)) % +(tpos(skc23, skc23)) % +(state(skc14, skc22)) % +(state(skc16, skc22)) % +(event(skc13, skc22)) % +(eventuality(skc13, skc22)) % +(tpos(skc16, skc14)) % +(tpos(skc14, skc16)) % +(tpos(skc16, skc16)) % +(theme(skc14, skc17, skc16)) % +(theme(skc16, skc17, skc16)) % +(proposition(skc14, skc16)) % +(proposition(skc16, skc16)) % +(relation(skc13, skc16)) % +(of(skc16, skc25, skc23)) % +(of(skc16, skc24, skc23)) % +(of(skc16, skc20, skc19)) % +(of(skc16, skc18, skc19)) % +(theme(skc16, skc15, skc14)) % +(agent(skc16, skc17, skc19)) % +(agent(skc16, skc15, skc19)) % +(jules_forename(skc16, skc24)) % +(jules_forename(skc16, skc25)) % +(vincent_forename(skc16, skc20)) % +(vincent_forename(skc16, skc18)) % +(forename(skc16, skc24)) % +(forename(skc16, skc25)) % +(forename(skc16, skc20)) % +(forename(skc16, skc18)) % +(man(skc16, skc23)) % +(man(skc16, skc19)) % +(proposition(skc16, skc14)) % +(think_believe_consider(skc16, skc17)) % +(think_believe_consider(skc16, skc15)) % +(present(skc16, skc17)) % +(present(skc16, skc15)) % +(event(skc16, skc17)) % +(event(skc16, skc15)) % +(tpos(skc14, skc14)) % +(theme(skc14, skc15, skc14)) % +(agent(skc14, skc15, skc19)) % +(event(skc14, skc15)) % +(eventuality(skc13, skc15)) % +(present(skc14, skc15)) % +(think_believe_consider(skc14, skc15)) % +(agent(skc14, skc17, skc19)) % +(think_believe_consider(skc14, skc17)) % +(present(skc14, skc17)) % +(event(skc14, skc17)) % +(eventuality(skc13, skc17)) % +(of(skc14, skc18, skc19)) % +(vincent_forename(skc14, skc18)) % +(forename(skc14, skc18)) % +(relname(skc13, skc18)) % +(of(skc14, skc20, skc19)) % +(man(skc14, skc19)) % +(male(skc13, skc19)) % +(human_person(skc13, skc19)) % +(vincent_forename(skc14, skc20)) % +(forename(skc14, skc20)) % +(relname(skc13, skc20)) % +(of(skc14, skc24, skc23)) % +(of(skc14, skc25, skc23)) % +(man(skc14, skc23)) % +(male(skc13, skc23)) % +(human_person(skc13, skc23)) % +(forename(skc14, skc25)) % +(relname(skc13, skc25)) % +(jules_forename(skc14, skc25)) % +(forename(skc14, skc24)) % +(relname(skc13, skc24)) % +(jules_forename(skc14, skc24)) % +(eventuality(skc14, skc26)) % +(proposition(skc14, skc14)) % +(relation(skc13, skc14)) % +(be(skc13, skc22, skc23, skc23)) % +(state(skc13, skc22)) % +(theme(skc13, skc17, skc16)) % +(proposition(skc13, skc16)) % +(accessible_world(skc13, skc16)) % +(theme(skc13, skc15, skc14)) % +(agent(skc13, skc15, skc19)) % +(event(skc13, skc15)) % +(present(skc13, skc15)) % +(think_believe_consider(skc13, skc15)) % +(agent(skc13, skc17, skc19)) % +(think_believe_consider(skc13, skc17)) % +(present(skc13, skc17)) % +(event(skc13, skc17)) % +(of(skc13, skc18, skc19)) % +(vincent_forename(skc13, skc18)) % +(forename(skc13, skc18)) % +(of(skc13, skc20, skc19)) % +(man(skc13, skc19)) % +(vincent_forename(skc13, skc20)) % +(forename(skc13, skc20)) % +(agent(skc14, skc26, skc23)) % +(of(skc13, skc24, skc23)) % +(of(skc13, skc25, skc23)) % +(man(skc13, skc23)) % +(forename(skc13, skc25)) % +(jules_forename(skc13, skc25)) % +(forename(skc13, skc24)) % +(jules_forename(skc13, skc24)) % +(smoke(skc14, skc26)) % +(present(skc14, skc26)) % +(event(skc14, skc26)) % +(accessible_world(skc13, skc14)) % +(proposition(skc13, skc14)) % +(actual_world(skc13)) % +(skc22(skc22)) % +(skc16(skc16)) % +(skc15(skc15)) % +(skc17(skc17)) % +(skc18(skc18)) % +(skc19(skc19)) % +(skc20(skc20)) % +(skc23(skc23)) % +(skc25(skc25)) % +(skc24(skc24)) % +(skc26(skc26)) % +(skc14(skc14)) % +(skc13(skc13)) % +(skf1(_2418_19105, skf1(_2418_19105))) % +(_19111) % %------------------------------------------------------------------------------