%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP245-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art04.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:08:32 EST 2011 % Result : Satisfiable 102.26s % Output : Assurance 102.26s % 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/NLP245-1+eq_rstfp.tme % result written to : /tmp/NLP245-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP245-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP245-1+eq_rstfp-eqt.tme % System...................: Linux art04.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...: [+(_483101)] % 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...: 1199 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 101.77 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc21, skf1(V_2447_483175))) % -(tpos(skc18, skf1(V_2447_483185))) % -(tpos(skc19, skf1(V_2447_483195))) % -(tpos(skc24, skf1(V_2447_483205))) % -(skc19(skf1(V_2447_483214))) % -(skc18(skf1(V_2447_483223))) % -(skc21(skf1(V_2447_483232))) % -(skc24(skf1(V_2447_483241))) % -(jules_forename(skc13, skf1(V_2447_483251))) % -(vincent_forename(skc13, skf1(V_2447_483261))) % -(tpos(skc22, skf1(V_2447_483271))) % -(tpos(skc14, skf1(V_2447_483281))) % -(be(U_2501_483291, V_2502_483292, skf1(V_2447_483295), skc19)) % -(be(U_2479_483305, V_2480_483306, skc19, skf1(V_2447_483309))) % -(be(U_2501_483319, V_2502_483320, skf1(V_2447_483323), skc18)) % -(be(U_2479_483333, V_2480_483334, skc18, skf1(V_2447_483337))) % -(be(U_2501_483347, V_2502_483348, skc18, skc20)) % -(be(U_2479_483358, V_2480_483359, skc20, skc18)) % -(be(U_2501_483369, V_2502_483370, skc19, skc20)) % -(be(U_2479_483380, V_2480_483381, skc20, skc19)) % -(be(U_2501_483391, V_2502_483392, skc20, skc21)) % -(be(U_2479_483402, V_2480_483403, skc21, skc20)) % -(be(U_2501_483413, V_2502_483414, skf1(V_2447_483417), skc21)) % -(be(U_2479_483427, V_2480_483428, skc21, skf1(V_2447_483431))) % -(be(U_2501_483441, V_2502_483442, skc20, skc24)) % -(be(U_2479_483452, V_2480_483453, skc24, skc20)) % -(be(U_2501_483463, V_2502_483464, skf1(V_2447_483467), skc24)) % -(be(U_2479_483477, V_2480_483478, skc24, skf1(V_2447_483481))) % -(be(U_2501_483491, V_2502_483492, skf1(V_2447_483495), skc22)) % -(be(U_2479_483505, V_2480_483506, skc22, skf1(V_2447_483509))) % -(forename(skc13, skf1(V_2447_483519))) % -(jules_forename(skc22, skf1(V_2447_483529))) % -(vincent_forename(skc22, skf1(V_2447_483539))) % -(skc22(skf1(V_2447_483548))) % -(skc14(skf1(V_2447_483557))) % -(tpos(skc20, skc19)) % -(tpos(skf1(V_2447_483574), skc19)) % -(be(U_2501_483584, V_2502_483585, skc16, skc19)) % -(be(U_2479_483595, V_2480_483596, skc19, skc16)) % -(be(U_2501_483606, V_2502_483607, skc15, skc19)) % -(be(U_2479_483617, V_2480_483618, skc19, skc15)) % -(tpos(skc20, skc18)) % -(tpos(skf1(V_2447_483635), skc18)) % -(be(U_2501_483645, V_2502_483646, skc16, skc18)) % -(be(U_2479_483656, V_2480_483657, skc18, skc16)) % -(be(U_2501_483667, V_2502_483668, skc15, skc18)) % -(be(U_2479_483678, V_2480_483679, skc18, skc15)) % -(tpos(skc21, skc20)) % -(tpos(skc18, skc20)) % -(tpos(skc19, skc20)) % -(tpos(skc24, skc20)) % -(be(U_2501_483717, V_2502_483718, skc22, skc20)) % -(be(U_2479_483728, V_2480_483729, skc20, skc22)) % -(be(U_2501_483739, V_2502_483740, skc20, skc14)) % -(be(U_2479_483750, V_2480_483751, skc14, skc20)) % -(be(U_2501_483761, V_2502_483762, skf1(V_2447_483765), skc14)) % -(be(U_2479_483775, V_2480_483776, skc14, skf1(V_2447_483779))) % -(tpos(skc20, skc21)) % -(tpos(skf1(V_2447_483796), skc21)) % -(be(U_2501_483806, V_2502_483807, skc16, skc21)) % -(be(U_2479_483817, V_2480_483818, skc21, skc16)) % -(be(U_2501_483828, V_2502_483829, skc15, skc21)) % -(be(U_2479_483839, V_2480_483840, skc21, skc15)) % -(be(U_2501_483850, V_2502_483851, skc21, skc23)) % -(be(U_2479_483861, V_2480_483862, skc23, skc21)) % -(be(U_2501_483872, V_2502_483873, skc18, skc23)) % -(be(U_2479_483883, V_2480_483884, skc23, skc18)) % -(be(U_2501_483894, V_2502_483895, skc19, skc23)) % -(be(U_2479_483905, V_2480_483906, skc23, skc19)) % -(tpos(skc20, skc24)) % -(tpos(skf1(V_2447_483923), skc24)) % -(be(U_2501_483933, V_2502_483934, skc16, skc24)) % -(be(U_2479_483944, V_2480_483945, skc24, skc16)) % -(be(U_2501_483955, V_2502_483956, skc15, skc24)) % -(be(U_2479_483966, V_2480_483967, skc24, skc15)) % -(be(U_2501_483977, V_2502_483978, skc23, skc24)) % -(be(U_2479_483988, V_2480_483989, skc24, skc23)) % -(tpos(skc20, skc22)) % -(tpos(skf1(V_2447_484006), skc22)) % -(tpos(skc17, skf1(V_2447_484016))) % -(tpos(skc25, skf1(V_2447_484026))) % -(human_person(skc13, skf1(V_2447_484036))) % -(relname(skc13, skf1(V_2447_484046))) % -(forename(skc22, skf1(V_2447_484056))) % -(proposition(skc13, skf1(V_2447_484066))) % -(jules_forename(skc14, skc15)) % -(vincent_forename(skc14, skc15)) % -(jules_forename(skc22, skc15)) % -(vincent_forename(skc22, skc15)) % -(tpos(skc21, skc15)) % -(tpos(skc18, skc15)) % -(tpos(skc19, skc15)) % -(tpos(skc24, skc15)) % -(be(U_2501_484132, V_2502_484133, skc22, skc15)) % -(be(U_2479_484143, V_2480_484144, skc15, skc22)) % -(jules_forename(skc14, skc16)) % -(vincent_forename(skc14, skc16)) % -(jules_forename(skc22, skc16)) % -(vincent_forename(skc22, skc16)) % -(tpos(skc21, skc16)) % -(tpos(skc18, skc16)) % -(tpos(skc19, skc16)) % -(tpos(skc24, skc16)) % -(be(U_2501_484210, V_2502_484211, skc22, skc16)) % -(be(U_2479_484221, V_2480_484222, skc16, skc22)) % -(be(U_2501_484232, V_2502_484233, skc17, skc19)) % -(be(U_2479_484243, V_2480_484244, skc19, skc17)) % -(skc20(skc19)) % -(smoke(skc14, skc19)) % -(skf1(V_2447_484265, skc19)) % -(smoke(skc22, skc19)) % -(tpos(skc16, skc19)) % -(tpos(skc15, skc19)) % -(tpos(skc23, skc19)) % -(be(U_2501_484303, V_2502_484304, skc17, skc18)) % -(be(U_2479_484314, V_2480_484315, skc18, skc17)) % -(skc20(skc18)) % -(smoke(skc14, skc18)) % -(skf1(V_2447_484336, skc18)) % -(smoke(skc22, skc18)) % -(tpos(skc16, skc18)) % -(tpos(skc15, skc18)) % -(tpos(skc23, skc18)) % -(skc19(skc20)) % -(skc18(skc20)) % -(skc21(skc20)) % -(skc24(skc20)) % -(jules_forename(skc13, skc20)) % -(vincent_forename(skc13, skc20)) % -(tpos(skc22, skc20)) % -(tpos(skc14, skc20)) % -(tpos(skc20, skc14)) % -(tpos(skf1(V_2447_484433), skc14)) % -(be(U_2501_484443, V_2502_484444, skc16, skc14)) % -(be(U_2479_484454, V_2480_484455, skc14, skc16)) % -(be(U_2501_484465, V_2502_484466, skc15, skc14)) % -(be(U_2479_484476, V_2480_484477, skc14, skc15)) % -(be(U_2501_484487, V_2502_484488, skc17, skc21)) % -(be(U_2479_484498, V_2480_484499, skc21, skc17)) % -(skc20(skc21)) % -(smoke(skc14, skc21)) % -(skf1(V_2447_484520, skc21)) % -(smoke(skc22, skc21)) % -(tpos(skc16, skc21)) % -(tpos(skc15, skc21)) % -(tpos(skc23, skc21)) % -(jules_forename(skc14, skc23)) % -(vincent_forename(skc14, skc23)) % -(jules_forename(skc22, skc23)) % -(vincent_forename(skc22, skc23)) % -(tpos(skc21, skc23)) % -(tpos(skc18, skc23)) % -(tpos(skc19, skc23)) % -(tpos(skc24, skc23)) % -(be(U_2501_484614, V_2502_484615, skc22, skc23)) % -(be(U_2479_484625, V_2480_484626, skc23, skc22)) % -(be(U_2501_484636, V_2502_484637, skc14, skc23)) % -(be(U_2479_484647, V_2480_484648, skc23, skc14)) % -(be(U_2501_484658, V_2502_484659, skc17, skc24)) % -(be(U_2479_484669, V_2480_484670, skc24, skc17)) % -(skc20(skc24)) % -(smoke(skc14, skc24)) % -(skf1(V_2447_484691, skc24)) % -(smoke(skc22, skc24)) % -(tpos(skc16, skc24)) % -(tpos(skc15, skc24)) % -(tpos(skc23, skc24)) % -(be(U_2501_484729, V_2502_484730, skc21, skc25)) % -(be(U_2479_484740, V_2480_484741, skc25, skc21)) % -(be(U_2501_484751, V_2502_484752, skc18, skc25)) % -(be(U_2479_484762, V_2480_484763, skc25, skc18)) % -(be(U_2501_484773, V_2502_484774, skc19, skc25)) % -(be(U_2479_484784, V_2480_484785, skc25, skc19)) % -(be(U_2501_484795, V_2502_484796, skc24, skc25)) % -(be(U_2479_484806, V_2480_484807, skc25, skc24)) % -(skc20(skc22)) % -(smoke(skc14, skc22)) % -(skf1(V_2447_484828, skc22)) % -(smoke(skc22, skc22)) % -(tpos(skc16, skc22)) % -(tpos(skc15, skc22)) % -(tpos(skc23, skc22)) % -(skc17(skf1(V_2447_484865))) % -(skc25(skf1(V_2447_484874))) % -(organism(skc13, skf1(V_2447_484884))) % -(human_person(skc22, skf1(V_2447_484894))) % -(relation(skc13, skf1(V_2447_484904))) % -(relname(skc22, skf1(V_2447_484914))) % -(proposition(skc22, skf1(V_2447_484924))) % -(forename(skc14, skc15)) % -(forename(skc22, skc15)) % -(skc19(skc15)) % -(skc18(skc15)) % -(skc21(skc15)) % -(skc24(skc15)) % -(jules_forename(skc13, skc15)) % -(vincent_forename(skc13, skc15)) % -(tpos(skc22, skc15)) % -(tpos(skc14, skc15)) % -(forename(skc14, skc16)) % -(forename(skc22, skc16)) % -(skc19(skc16)) % -(skc18(skc16)) % -(skc21(skc16)) % -(skc24(skc16)) % -(jules_forename(skc13, skc16)) % -(vincent_forename(skc13, skc16)) % -(tpos(skc22, skc16)) % -(tpos(skc14, skc16)) % -(jules_forename(skc14, skc17)) % -(vincent_forename(skc14, skc17)) % -(jules_forename(skc22, skc17)) % -(vincent_forename(skc22, skc17)) % -(be(U_2501_485094, V_2502_485095, skf1(V_2447_485098), skc17)) % -(be(U_2479_485108, V_2480_485109, skc17, skf1(V_2447_485112))) % -(tpos(skc21, skc17)) % -(tpos(skc18, skc17)) % -(tpos(skc19, skc17)) % -(tpos(skc24, skc17)) % -(be(U_2501_485150, V_2502_485151, skc22, skc17)) % -(be(U_2479_485161, V_2480_485162, skc17, skc22)) % -(tpos(skc17, skc19)) % -(tpos(skc25, skc19)) % -(organism(skc14, skc19)) % -(state(skc14, skc19)) % -(event(skc14, skc19)) % -(organism(skc22, skc19)) % -(state(skc22, skc19)) % -(event(skc22, skc19)) % -(skc16(skc19)) % -(skc15(skc19)) % -(skc23(skc19)) % -(smoke(skc13, skc19)) % -(tpos(skc17, skc18)) % -(tpos(skc25, skc18)) % -(organism(skc14, skc18)) % -(state(skc14, skc18)) % -(event(skc14, skc18)) % -(organism(skc22, skc18)) % -(state(skc22, skc18)) % -(event(skc22, skc18)) % -(skc16(skc18)) % -(skc15(skc18)) % -(skc23(skc18)) % -(smoke(skc13, skc18)) % -(be(U_2501_485334, V_2502_485335, skc17, skc20)) % -(be(U_2479_485345, V_2480_485346, skc20, skc17)) % -(forename(skc13, skc20)) % -(jules_forename(skc14, skc20)) % -(vincent_forename(skc14, skc20)) % -(skc22(skc20)) % -(skc14(skc20)) % -(be(U_2501_485389, V_2502_485390, skc17, skc14)) % -(be(U_2479_485400, V_2480_485401, skc14, skc17)) % -(skc20(skc14)) % -(smoke(skc14, skc14)) % -(skf1(V_2447_485422, skc14)) % -(smoke(skc22, skc14)) % -(tpos(skc16, skc14)) % -(tpos(skc15, skc14)) % -(tpos(skc23, skc14)) % -(tpos(skc17, skc21)) % -(tpos(skc25, skc21)) % -(organism(skc14, skc21)) % -(state(skc14, skc21)) % -(event(skc14, skc21)) % -(organism(skc22, skc21)) % -(state(skc22, skc21)) % -(event(skc22, skc21)) % -(skc16(skc21)) % -(skc15(skc21)) % -(skc23(skc21)) % -(smoke(skc13, skc21)) % -(forename(skc14, skc23)) % -(forename(skc22, skc23)) % -(skc19(skc23)) % -(skc18(skc23)) % -(skc21(skc23)) % -(skc24(skc23)) % -(jules_forename(skc13, skc23)) % -(vincent_forename(skc13, skc23)) % -(tpos(skc22, skc23)) % -(tpos(skc14, skc23)) % -(tpos(skc17, skc24)) % -(tpos(skc25, skc24)) % -(organism(skc14, skc24)) % -(state(skc14, skc24)) % -(event(skc14, skc24)) % -(organism(skc22, skc24)) % -(state(skc22, skc24)) % -(event(skc22, skc24)) % -(skc16(skc24)) % -(skc15(skc24)) % -(skc23(skc24)) % -(smoke(skc13, skc24)) % -(jules_forename(skc14, skc25)) % -(vincent_forename(skc14, skc25)) % -(be(U_2501_485702, V_2502_485703, skc20, skc25)) % -(be(U_2479_485713, V_2480_485714, skc25, skc20)) % -(jules_forename(skc22, skc25)) % -(vincent_forename(skc22, skc25)) % -(be(U_2501_485738, V_2502_485739, skf1(V_2447_485742), skc25)) % -(be(U_2479_485752, V_2480_485753, skc25, skf1(V_2447_485756))) % -(tpos(skc21, skc25)) % -(tpos(skc18, skc25)) % -(tpos(skc19, skc25)) % -(tpos(skc24, skc25)) % -(be(U_2501_485794, V_2502_485795, skc22, skc25)) % -(be(U_2479_485805, V_2480_485806, skc25, skc22)) % -(be(U_2501_485816, V_2502_485817, skc14, skc25)) % -(be(U_2479_485827, V_2480_485828, skc25, skc14)) % -(tpos(skc17, skc22)) % -(tpos(skc25, skc22)) % -(organism(skc14, skc22)) % -(state(skc14, skc22)) % -(event(skc14, skc22)) % -(organism(skc22, skc22)) % -(state(skc22, skc22)) % -(event(skc22, skc22)) % -(skc16(skc22)) % -(skc15(skc22)) % -(skc23(skc22)) % -(smoke(skc13, skc22)) % -(man(skc13, skf1(V_2447_485919))) % -(entity(skc13, skf1(V_2447_485929))) % -(organism(skc22, skf1(V_2447_485939))) % -(abstraction(skc13, skf1(V_2447_485949))) % -(relation(skc22, skf1(V_2447_485959))) % -(human_person(skc14, skc15)) % -(human_person(skc22, skc15)) % -(relname(skc14, skc15)) % -(proposition(skc14, skc15)) % -(relname(skc22, skc15)) % -(proposition(skc22, skc15)) % -(forename(skc13, skc15)) % -(skc22(skc15)) % -(skc14(skc15)) % -(human_person(skc14, skc16)) % -(human_person(skc22, skc16)) % -(relname(skc14, skc16)) % -(proposition(skc14, skc16)) % -(relname(skc22, skc16)) % -(proposition(skc22, skc16)) % -(forename(skc13, skc16)) % -(skc22(skc16)) % -(skc14(skc16)) % -(forename(skc14, skc17)) % -(tpos(skc20, skc17)) % -(forename(skc22, skc17)) % -(tpos(skf1(V_2447_486112), skc17)) % -(skc19(skc17)) % -(skc18(skc17)) % -(skc21(skc17)) % -(skc24(skc17)) % -(jules_forename(skc13, skc17)) % -(vincent_forename(skc13, skc17)) % -(tpos(skc22, skc17)) % -(tpos(skc14, skc17)) % -(be(U_2501_486174, V_2502_486175, skc16, skc17)) % -(be(U_2479_486185, V_2480_486186, skc17, skc16)) % -(be(U_2501_486196, V_2502_486197, skc15, skc17)) % -(be(U_2479_486207, V_2480_486208, skc17, skc15)) % +(vincent_forename(skc14, skc19)) % +(vincent_forename(skc22, skc19)) % +(vincent_forename(skc14, skc18)) % +(vincent_forename(skc22, skc18)) % +(jules_forename(skc14, skc21)) % +(jules_forename(skc22, skc21)) % -(man(skc14, skc19)) % -(man(skc22, skc19)) % -(skc17(skc19)) % -(skc25(skc19)) % -(entity(skc14, skc19)) % -(eventuality(skc14, skc19)) % -(entity(skc22, skc19)) % -(eventuality(skc22, skc19)) % -(organism(skc13, skc19)) % -(state(skc13, skc19)) % -(event(skc13, skc19)) % -(human_person(skc14, skc19)) % -(human_person(skc22, skc19)) % -(man(skc14, skc18)) % -(man(skc22, skc18)) % -(skc17(skc18)) % -(skc25(skc18)) % -(entity(skc14, skc18)) % -(eventuality(skc14, skc18)) % -(entity(skc22, skc18)) % -(eventuality(skc22, skc18)) % -(organism(skc13, skc18)) % -(state(skc13, skc18)) % -(event(skc13, skc18)) % -(human_person(skc14, skc18)) % -(human_person(skc22, skc18)) % -(tpos(skc17, skc20)) % -(tpos(skc25, skc20)) % -(human_person(skc13, skc20)) % -(relname(skc13, skc20)) % -(forename(skc14, skc20)) % -(proposition(skc13, skc20)) % -(tpos(skc17, skc14)) % -(tpos(skc25, skc14)) % -(organism(skc14, skc14)) % -(state(skc14, skc14)) % -(event(skc14, skc14)) % -(organism(skc22, skc14)) % -(state(skc22, skc14)) % -(event(skc22, skc14)) % -(skc16(skc14)) % -(skc15(skc14)) % -(skc23(skc14)) % -(smoke(skc13, skc14)) % -(man(skc14, skc21)) % -(man(skc22, skc21)) % -(skc17(skc21)) % -(skc25(skc21)) % -(entity(skc14, skc21)) % -(eventuality(skc14, skc21)) % -(entity(skc22, skc21)) % -(eventuality(skc22, skc21)) % -(organism(skc13, skc21)) % -(state(skc13, skc21)) % -(event(skc13, skc21)) % -(human_person(skc14, skc21)) % -(human_person(skc22, skc21)) % -(be(U_2501_486650, V_2502_486651, skc17, skc23)) % -(be(U_2479_486661, V_2480_486662, skc23, skc17)) % -(human_person(skc14, skc23)) % -(human_person(skc22, skc23)) % -(relname(skc14, skc23)) % -(proposition(skc14, skc23)) % -(relname(skc22, skc23)) % -(proposition(skc22, skc23)) % -(forename(skc13, skc23)) % -(skc22(skc23)) % -(skc14(skc23)) % -(man(skc14, skc24)) % -(man(skc22, skc24)) % -(skc17(skc24)) % -(skc25(skc24)) % -(entity(skc14, skc24)) % -(eventuality(skc14, skc24)) % -(entity(skc22, skc24)) % -(eventuality(skc22, skc24)) % -(organism(skc13, skc24)) % -(state(skc13, skc24)) % -(event(skc13, skc24)) % -(human_person(skc14, skc24)) % -(human_person(skc22, skc24)) % -(forename(skc14, skc25)) % -(tpos(skc20, skc25)) % -(forename(skc22, skc25)) % -(tpos(skf1(V_2447_486843), skc25)) % -(skc19(skc25)) % -(skc18(skc25)) % -(skc21(skc25)) % -(skc24(skc25)) % -(jules_forename(skc13, skc25)) % -(vincent_forename(skc13, skc25)) % -(tpos(skc22, skc25)) % -(tpos(skc14, skc25)) % -(be(U_2501_486905, V_2502_486906, skc16, skc25)) % -(be(U_2479_486916, V_2480_486917, skc25, skc16)) % -(be(U_2501_486927, V_2502_486928, skc15, skc25)) % -(be(U_2479_486938, V_2480_486939, skc25, skc15)) % -(be(U_2501_486949, V_2502_486950, skc23, skc25)) % -(be(U_2479_486960, V_2480_486961, skc25, skc23)) % -(man(skc14, skc22)) % -(man(skc22, skc22)) % -(skc17(skc22)) % -(skc25(skc22)) % -(entity(skc14, skc22)) % -(eventuality(skc14, skc22)) % -(entity(skc22, skc22)) % -(eventuality(skc22, skc22)) % -(organism(skc13, skc22)) % -(state(skc13, skc22)) % -(event(skc13, skc22)) % -(human_person(skc14, skc22)) % -(human_person(skc22, skc22)) % -(male(skc13, skf1(V_2447_487060))) % -(man(skc22, skf1(V_2447_487070))) % -(existent(skc13, skf1(V_2447_487080))) % -(entity(skc22, skf1(V_2447_487090))) % -(general(skc13, skf1(V_2447_487100))) % -(abstraction(skc22, skf1(V_2447_487110))) % -(tpos(skc17, skc15)) % -(tpos(skc25, skc15)) % -(organism(skc14, skc15)) % -(organism(skc22, skc15)) % -(human_person(skc13, skc15)) % -(relation(skc14, skc15)) % -(relation(skc22, skc15)) % -(relname(skc13, skc15)) % -(proposition(skc13, skc15)) % -(tpos(skc17, skc16)) % -(tpos(skc25, skc16)) % -(organism(skc14, skc16)) % -(organism(skc22, skc16)) % -(human_person(skc13, skc16)) % -(relation(skc14, skc16)) % -(relation(skc22, skc16)) % -(relname(skc13, skc16)) % -(proposition(skc13, skc16)) % -(relname(skc14, skc17)) % -(proposition(skc14, skc17)) % -(skc20(skc17)) % -(smoke(skc14, skc17)) % -(relname(skc22, skc17)) % -(proposition(skc22, skc17)) % -(skf1(V_2447_487285, skc17)) % -(smoke(skc22, skc17)) % -(forename(skc13, skc17)) % -(skc22(skc17)) % -(skc14(skc17)) % -(tpos(skc16, skc17)) % -(tpos(skc15, skc17)) % -(tpos(skc23, skc17)) % +(vincent_forename(skc13, skc19)) % +(vincent_forename(skc13, skc18)) % +(jules_forename(skc13, skc21)) % -(nonexistent(skc14, skc17)) % -(nonexistent(skc22, skc17)) % -(general(skc14, skc17)) % -(general(skc22, skc17)) % +(singleton(skc14, skc17)) % +(singleton(skc22, skc17)) % -(male(skc14, skc19)) % -(male(skc22, skc19)) % -(man(skc13, skc19)) % -(specific(skc14, skc19)) % -(specific(skc22, skc19)) % -(entity(skc13, skc19)) % -(eventuality(skc13, skc19)) % -(human(skc14, skc19)) % -(human(skc22, skc19)) % -(human_person(skc13, skc19)) % +(singleton(skc14, skc19)) % +(singleton(skc22, skc19)) % -(male(skc14, skc18)) % -(male(skc22, skc18)) % -(man(skc13, skc18)) % -(specific(skc14, skc18)) % -(specific(skc22, skc18)) % -(entity(skc13, skc18)) % -(eventuality(skc13, skc18)) % -(human(skc14, skc18)) % -(human(skc22, skc18)) % -(human_person(skc13, skc18)) % +(singleton(skc14, skc18)) % +(singleton(skc22, skc18)) % -(skc17(skc20)) % -(skc25(skc20)) % -(organism(skc13, skc20)) % -(human_person(skc14, skc20)) % -(relation(skc13, skc20)) % -(relname(skc14, skc20)) % -(proposition(skc14, skc20)) % -(man(skc14, skc14)) % -(man(skc22, skc14)) % -(skc17(skc14)) % -(skc25(skc14)) % -(entity(skc14, skc14)) % -(eventuality(skc14, skc14)) % -(entity(skc22, skc14)) % -(eventuality(skc22, skc14)) % -(organism(skc13, skc14)) % -(state(skc13, skc14)) % -(event(skc13, skc14)) % -(human_person(skc14, skc14)) % -(human_person(skc22, skc14)) % -(male(skc14, skc21)) % -(male(skc22, skc21)) % -(man(skc13, skc21)) % -(specific(skc14, skc21)) % -(specific(skc22, skc21)) % -(entity(skc13, skc21)) % -(eventuality(skc13, skc21)) % -(human(skc14, skc21)) % -(human(skc22, skc21)) % -(human_person(skc13, skc21)) % +(singleton(skc14, skc21)) % +(singleton(skc22, skc21)) % -(tpos(skc17, skc23)) % -(tpos(skc25, skc23)) % -(organism(skc14, skc23)) % -(organism(skc22, skc23)) % -(human_person(skc13, skc23)) % -(relation(skc14, skc23)) % -(relation(skc22, skc23)) % -(relname(skc13, skc23)) % -(proposition(skc13, skc23)) % -(male(skc14, skc24)) % -(male(skc22, skc24)) % -(man(skc13, skc24)) % -(specific(skc14, skc24)) % -(specific(skc22, skc24)) % -(entity(skc13, skc24)) % -(eventuality(skc13, skc24)) % -(human(skc14, skc24)) % -(human(skc22, skc24)) % -(human_person(skc13, skc24)) % +(singleton(skc14, skc24)) % +(singleton(skc22, skc24)) % -(relname(skc14, skc25)) % -(proposition(skc14, skc25)) % -(skc20(skc25)) % -(smoke(skc14, skc25)) % -(relname(skc22, skc25)) % -(proposition(skc22, skc25)) % -(skf1(V_2447_487979, skc25)) % -(smoke(skc22, skc25)) % -(forename(skc13, skc25)) % -(skc22(skc25)) % -(skc14(skc25)) % -(tpos(skc16, skc25)) % -(tpos(skc15, skc25)) % -(tpos(skc23, skc25)) % -(nonexistent(skc14, skc25)) % -(nonexistent(skc22, skc25)) % -(general(skc14, skc25)) % -(general(skc22, skc25)) % +(singleton(skc14, skc25)) % +(singleton(skc22, skc25)) % -(male(skc14, skc22)) % -(male(skc22, skc22)) % -(man(skc13, skc22)) % -(specific(skc14, skc22)) % -(specific(skc22, skc22)) % -(entity(skc13, skc22)) % -(eventuality(skc13, skc22)) % -(human(skc14, skc22)) % -(human(skc22, skc22)) % -(human_person(skc13, skc22)) % +(singleton(skc14, skc22)) % +(singleton(skc22, skc22)) % -(male(skc22, skf1(V_2447_488162))) % -(existent(skc22, skf1(V_2447_488172))) % -(general(skc22, skf1(V_2447_488182))) % +(singleton(skc22, skf1(V_2447_488192))) % -(man(skc14, skc15)) % -(man(skc22, skc15)) % -(skc17(skc15)) % -(skc25(skc15)) % -(entity(skc14, skc15)) % -(entity(skc22, skc15)) % -(organism(skc13, skc15)) % -(abstraction(skc14, skc15)) % -(abstraction(skc22, skc15)) % -(relation(skc13, skc15)) % -(man(skc14, skc16)) % -(man(skc22, skc16)) % -(skc17(skc16)) % -(skc25(skc16)) % -(entity(skc14, skc16)) % -(entity(skc22, skc16)) % -(organism(skc13, skc16)) % -(abstraction(skc14, skc16)) % -(abstraction(skc22, skc16)) % -(relation(skc13, skc16)) % -(relation(skc14, skc17)) % -(state(skc14, skc17)) % -(event(skc14, skc17)) % -(relation(skc22, skc17)) % -(state(skc22, skc17)) % -(event(skc22, skc17)) % -(relname(skc13, skc17)) % -(proposition(skc13, skc17)) % -(skc16(skc17)) % -(skc15(skc17)) % -(skc23(skc17)) % -(smoke(skc13, skc17)) % +(skc21(skc19)) % +(skc21(skc18)) % +(skc18(skc19)) % +(skc18(skc21)) % +(skc19(skc18)) % +(skc19(skc21)) % +(existent(skc14, skc17)) % +(existent(skc22, skc17)) % -(nonexistent(skc13, skc17)) % +(specific(skc14, skc17)) % +(specific(skc22, skc17)) % -(general(skc13, skc17)) % +(thing(skc14, skc17)) % +(thing(skc22, skc17)) % +(singleton(skc13, skc17)) % +(unisex(skc14, skc19)) % +(unisex(skc22, skc19)) % -(male(skc13, skc19)) % +(general(skc14, skc19)) % +(general(skc22, skc19)) % -(specific(skc13, skc19)) % +(nonhuman(skc14, skc19)) % +(nonhuman(skc22, skc19)) % -(human(skc13, skc19)) % +(thing(skc14, skc19)) % +(thing(skc22, skc19)) % +(singleton(skc13, skc19)) % +(unisex(skc14, skc18)) % +(unisex(skc22, skc18)) % -(male(skc13, skc18)) % +(general(skc14, skc18)) % +(general(skc22, skc18)) % -(specific(skc13, skc18)) % +(nonhuman(skc14, skc18)) % +(nonhuman(skc22, skc18)) % -(human(skc13, skc18)) % +(thing(skc14, skc18)) % +(thing(skc22, skc18)) % +(singleton(skc13, skc18)) % -(man(skc13, skc20)) % -(entity(skc13, skc20)) % -(organism(skc14, skc20)) % -(abstraction(skc13, skc20)) % -(relation(skc14, skc20)) % -(male(skc14, skc14)) % -(male(skc22, skc14)) % -(man(skc13, skc14)) % -(specific(skc14, skc14)) % -(specific(skc22, skc14)) % -(entity(skc13, skc14)) % -(eventuality(skc13, skc14)) % -(human(skc14, skc14)) % -(human(skc22, skc14)) % -(human_person(skc13, skc14)) % +(singleton(skc14, skc14)) % +(singleton(skc22, skc14)) % +(unisex(skc14, skc21)) % +(unisex(skc22, skc21)) % -(male(skc13, skc21)) % +(general(skc14, skc21)) % +(general(skc22, skc21)) % -(specific(skc13, skc21)) % +(nonhuman(skc14, skc21)) % +(nonhuman(skc22, skc21)) % -(human(skc13, skc21)) % +(thing(skc14, skc21)) % +(thing(skc22, skc21)) % +(singleton(skc13, skc21)) % -(man(skc14, skc23)) % -(man(skc22, skc23)) % -(skc17(skc23)) % -(skc25(skc23)) % -(entity(skc14, skc23)) % -(entity(skc22, skc23)) % -(organism(skc13, skc23)) % -(abstraction(skc14, skc23)) % -(abstraction(skc22, skc23)) % -(relation(skc13, skc23)) % +(unisex(skc14, skc24)) % +(unisex(skc22, skc24)) % -(male(skc13, skc24)) % +(general(skc14, skc24)) % +(general(skc22, skc24)) % -(specific(skc13, skc24)) % +(nonhuman(skc14, skc24)) % +(nonhuman(skc22, skc24)) % -(human(skc13, skc24)) % +(thing(skc14, skc24)) % +(thing(skc22, skc24)) % +(singleton(skc13, skc24)) % -(relation(skc14, skc25)) % -(state(skc14, skc25)) % -(event(skc14, skc25)) % -(relation(skc22, skc25)) % -(state(skc22, skc25)) % -(event(skc22, skc25)) % -(relname(skc13, skc25)) % -(proposition(skc13, skc25)) % -(skc16(skc25)) % -(skc15(skc25)) % -(skc23(skc25)) % -(smoke(skc13, skc25)) % +(existent(skc14, skc25)) % +(existent(skc22, skc25)) % -(nonexistent(skc13, skc25)) % +(specific(skc14, skc25)) % +(specific(skc22, skc25)) % -(general(skc13, skc25)) % +(thing(skc14, skc25)) % +(thing(skc22, skc25)) % +(singleton(skc13, skc25)) % +(unisex(skc14, skc22)) % +(unisex(skc22, skc22)) % -(male(skc13, skc22)) % +(general(skc14, skc22)) % +(general(skc22, skc22)) % -(specific(skc13, skc22)) % +(nonhuman(skc14, skc22)) % +(nonhuman(skc22, skc22)) % -(human(skc13, skc22)) % +(thing(skc14, skc22)) % +(thing(skc22, skc22)) % +(singleton(skc13, skc22)) % +(unisex(skc22, skf1(V_2447_489269))) % +(nonexistent(skc22, skf1(V_2447_489279))) % +(specific(skc22, skf1(V_2447_489289))) % +(thing(skc22, skf1(V_2447_489299))) % -(male(skc14, skc15)) % -(male(skc22, skc15)) % -(man(skc13, skc15)) % -(existent(skc14, skc15)) % -(existent(skc22, skc15)) % -(entity(skc13, skc15)) % -(general(skc14, skc15)) % -(general(skc22, skc15)) % -(abstraction(skc13, skc15)) % +(singleton(skc14, skc15)) % +(singleton(skc22, skc15)) % -(male(skc14, skc16)) % -(male(skc22, skc16)) % -(man(skc13, skc16)) % -(existent(skc14, skc16)) % -(existent(skc22, skc16)) % -(entity(skc13, skc16)) % -(general(skc14, skc16)) % -(general(skc22, skc16)) % -(abstraction(skc13, skc16)) % +(singleton(skc14, skc16)) % +(singleton(skc22, skc16)) % -(abstraction(skc14, skc17)) % -(eventuality(skc14, skc17)) % -(abstraction(skc22, skc17)) % -(eventuality(skc22, skc17)) % -(relation(skc13, skc17)) % -(state(skc13, skc17)) % -(event(skc13, skc17)) % -(nonhuman(skc14, skc17)) % -(nonhuman(skc22, skc17)) % +(living(skc14, skc17)) % +(living(skc22, skc17)) % +(impartial(skc14, skc17)) % +(impartial(skc22, skc17)) % +(tpos(skc21, skc19)) % +(tpos(skc21, skc18)) % +(tpos(skc21, skc21)) % +(tpos(skc18, skc19)) % +(tpos(skc18, skc18)) % +(tpos(skc18, skc21)) % +(tpos(skc19, skc19)) % +(tpos(skc19, skc18)) % +(tpos(skc19, skc21)) % +(entity(skc14, skc17)) % +(entity(skc22, skc17)) % +(existent(skc13, skc17)) % +(specific(skc13, skc17)) % +(thing(skc13, skc17)) % +(abstraction(skc14, skc19)) % +(abstraction(skc22, skc19)) % +(unisex(skc13, skc19)) % +(general(skc13, skc19)) % +(nonhuman(skc13, skc19)) % +(thing(skc13, skc19)) % +(abstraction(skc14, skc18)) % +(abstraction(skc22, skc18)) % +(unisex(skc13, skc18)) % +(general(skc13, skc18)) % +(nonhuman(skc13, skc18)) % +(thing(skc13, skc18)) % -(male(skc13, skc20)) % -(man(skc14, skc20)) % -(existent(skc13, skc20)) % -(entity(skc14, skc20)) % -(general(skc13, skc20)) % -(abstraction(skc14, skc20)) % +(unisex(skc14, skc14)) % +(unisex(skc22, skc14)) % -(male(skc13, skc14)) % +(general(skc14, skc14)) % +(general(skc22, skc14)) % -(specific(skc13, skc14)) % +(nonhuman(skc14, skc14)) % +(nonhuman(skc22, skc14)) % -(human(skc13, skc14)) % +(thing(skc14, skc14)) % +(thing(skc22, skc14)) % +(singleton(skc13, skc14)) % +(abstraction(skc14, skc21)) % +(abstraction(skc22, skc21)) % +(unisex(skc13, skc21)) % +(general(skc13, skc21)) % +(nonhuman(skc13, skc21)) % +(thing(skc13, skc21)) % -(male(skc14, skc23)) % -(male(skc22, skc23)) % -(man(skc13, skc23)) % -(existent(skc14, skc23)) % -(existent(skc22, skc23)) % -(entity(skc13, skc23)) % -(general(skc14, skc23)) % -(general(skc22, skc23)) % -(abstraction(skc13, skc23)) % +(singleton(skc14, skc23)) % +(singleton(skc22, skc23)) % +(abstraction(skc14, skc24)) % +(abstraction(skc22, skc24)) % +(unisex(skc13, skc24)) % +(general(skc13, skc24)) % +(nonhuman(skc13, skc24)) % +(thing(skc13, skc24)) % -(abstraction(skc14, skc25)) % -(eventuality(skc14, skc25)) % -(abstraction(skc22, skc25)) % -(eventuality(skc22, skc25)) % -(relation(skc13, skc25)) % -(state(skc13, skc25)) % -(event(skc13, skc25)) % -(nonhuman(skc14, skc25)) % -(nonhuman(skc22, skc25)) % +(living(skc14, skc25)) % +(living(skc22, skc25)) % +(impartial(skc14, skc25)) % +(impartial(skc22, skc25)) % +(tpos(skc24, skc24)) % +(entity(skc14, skc25)) % +(entity(skc22, skc25)) % +(existent(skc13, skc25)) % +(specific(skc13, skc25)) % +(thing(skc13, skc25)) % +(abstraction(skc14, skc22)) % +(abstraction(skc22, skc22)) % +(unisex(skc13, skc22)) % +(general(skc13, skc22)) % +(nonhuman(skc13, skc22)) % +(thing(skc13, skc22)) % +(eventuality(skc22, skf1(V_2447_490198))) % +(unisex(skc14, skc15)) % +(unisex(skc22, skc15)) % -(male(skc13, skc15)) % +(nonexistent(skc14, skc15)) % +(nonexistent(skc22, skc15)) % -(existent(skc13, skc15)) % +(specific(skc14, skc15)) % +(specific(skc22, skc15)) % -(general(skc13, skc15)) % +(thing(skc14, skc15)) % +(thing(skc22, skc15)) % +(singleton(skc13, skc15)) % +(unisex(skc14, skc16)) % +(unisex(skc22, skc16)) % -(male(skc13, skc16)) % +(nonexistent(skc14, skc16)) % +(nonexistent(skc22, skc16)) % -(existent(skc13, skc16)) % +(specific(skc14, skc16)) % +(specific(skc22, skc16)) % -(general(skc13, skc16)) % +(thing(skc14, skc16)) % +(thing(skc22, skc16)) % +(singleton(skc13, skc16)) % -(unisex(skc14, skc17)) % -(unisex(skc22, skc17)) % -(abstraction(skc13, skc17)) % -(eventuality(skc13, skc17)) % +(animate(skc14, skc17)) % +(animate(skc22, skc17)) % +(human(skc14, skc17)) % +(human(skc22, skc17)) % -(nonhuman(skc13, skc17)) % +(organism(skc14, skc17)) % +(organism(skc22, skc17)) % +(living(skc13, skc17)) % +(impartial(skc13, skc17)) % +(entity(skc13, skc17)) % +(relation(skc14, skc19)) % +(relation(skc22, skc19)) % +(abstraction(skc13, skc19)) % +(relation(skc14, skc18)) % +(relation(skc22, skc18)) % +(abstraction(skc13, skc18)) % -(male(skc14, skc20)) % -(existent(skc14, skc20)) % -(general(skc14, skc20)) % +(singleton(skc14, skc20)) % +(abstraction(skc14, skc14)) % +(abstraction(skc22, skc14)) % +(unisex(skc13, skc14)) % +(general(skc13, skc14)) % +(nonhuman(skc13, skc14)) % +(thing(skc13, skc14)) % +(relation(skc14, skc21)) % +(relation(skc22, skc21)) % +(abstraction(skc13, skc21)) % +(unisex(skc14, skc23)) % +(unisex(skc22, skc23)) % -(male(skc13, skc23)) % +(nonexistent(skc14, skc23)) % +(nonexistent(skc22, skc23)) % -(existent(skc13, skc23)) % +(specific(skc14, skc23)) % +(specific(skc22, skc23)) % -(general(skc13, skc23)) % +(thing(skc14, skc23)) % +(thing(skc22, skc23)) % +(singleton(skc13, skc23)) % +(relation(skc14, skc24)) % +(relation(skc22, skc24)) % +(abstraction(skc13, skc24)) % -(unisex(skc14, skc25)) % -(unisex(skc22, skc25)) % -(abstraction(skc13, skc25)) % -(eventuality(skc13, skc25)) % +(animate(skc14, skc25)) % +(animate(skc22, skc25)) % +(human(skc14, skc25)) % +(human(skc22, skc25)) % -(nonhuman(skc13, skc25)) % +(organism(skc14, skc25)) % +(organism(skc22, skc25)) % +(living(skc13, skc25)) % +(impartial(skc13, skc25)) % +(entity(skc13, skc25)) % +(relation(skc14, skc22)) % +(relation(skc22, skc22)) % +(abstraction(skc13, skc22)) % +(agent(skc22, skf1(skc25), skc25)) % +(agent(skc22, skf1(skc17), skc17)) % +(event(skc22, skf1(V_2447_490851))) % +(present(skc22, skf1(V_2447_490861))) % +(smoke(skc22, skf1(V_2447_490871))) % +(eventuality(skc14, skc15)) % +(eventuality(skc22, skc15)) % +(unisex(skc13, skc15)) % +(nonexistent(skc13, skc15)) % +(specific(skc13, skc15)) % +(thing(skc13, skc15)) % +(event(skc14, skc16)) % +(event(skc22, skc16)) % +(eventuality(skc14, skc16)) % +(eventuality(skc22, skc16)) % +(unisex(skc13, skc16)) % +(nonexistent(skc13, skc16)) % +(specific(skc13, skc16)) % +(thing(skc13, skc16)) % +(male(skc14, skc17)) % +(male(skc22, skc17)) % -(unisex(skc13, skc17)) % +(human_person(skc14, skc17)) % +(human_person(skc22, skc17)) % +(animate(skc13, skc17)) % +(human(skc13, skc17)) % +(organism(skc13, skc17)) % +(relname(skc14, skc19)) % +(relname(skc22, skc19)) % +(relation(skc13, skc19)) % +(relname(skc14, skc18)) % +(relname(skc22, skc18)) % +(relation(skc13, skc18)) % +(unisex(skc14, skc20)) % +(nonexistent(skc14, skc20)) % +(specific(skc14, skc20)) % +(thing(skc14, skc20)) % +(relation(skc14, skc14)) % +(relation(skc22, skc14)) % +(abstraction(skc13, skc14)) % +(relname(skc14, skc21)) % +(relname(skc22, skc21)) % +(relation(skc13, skc21)) % +(eventuality(skc14, skc23)) % +(eventuality(skc22, skc23)) % +(unisex(skc13, skc23)) % +(nonexistent(skc13, skc23)) % +(specific(skc13, skc23)) % +(thing(skc13, skc23)) % +(relname(skc14, skc24)) % +(relname(skc22, skc24)) % +(relation(skc13, skc24)) % +(male(skc14, skc25)) % +(male(skc22, skc25)) % -(unisex(skc13, skc25)) % +(human_person(skc14, skc25)) % +(human_person(skc22, skc25)) % +(animate(skc13, skc25)) % +(human(skc13, skc25)) % +(organism(skc13, skc25)) % +(tpos(skc22, skc22)) % +(theme(skc14, skc23, skc22)) % +(theme(skc22, skc23, skc22)) % +(proposition(skc14, skc22)) % +(proposition(skc22, skc22)) % +(relation(skc13, skc22)) % +(be(skc22, skc16, skc17, skc17)) % +(of(skc22, skc24, skc25)) % +(of(skc22, skc19, skc17)) % +(of(skc22, skc18, skc17)) % +(of(skc22, skc21, skc17)) % +(theme(skc22, skc15, skc14)) % +(agent(skc22, skc23, skc25)) % +(agent(skc22, skc15, skc17)) % +(jules_forename(skc22, skc18)) % +(jules_forename(skc22, skc19)) % +(vincent_forename(skc22, skc24)) % +(vincent_forename(skc22, skc21)) % +(forename(skc22, skc24)) % +(forename(skc22, skc21)) % +(forename(skc22, skc18)) % +(forename(skc22, skc19)) % +(man(skc22, skc25)) % +(man(skc22, skc17)) % +(state(skc22, skc16)) % +(proposition(skc22, skc14)) % +(think_believe_consider(skc22, skc23)) % +(think_believe_consider(skc22, skc15)) % +(present(skc22, skc23)) % +(present(skc22, skc15)) % +(event(skc22, skc23)) % +(event(skc22, skc15)) % +(tpos(skc14, skc14)) % +(theme(skc14, skc15, skc14)) % +(agent(skc14, skc15, skc17)) % +(event(skc14, skc15)) % +(eventuality(skc13, skc15)) % +(present(skc14, skc15)) % +(think_believe_consider(skc14, skc15)) % +(be(skc14, skc16, skc17, skc17)) % +(tpos(skc17, skc17)) % +(state(skc14, skc16)) % +(event(skc13, skc16)) % +(eventuality(skc13, skc16)) % +(of(skc14, skc21, skc17)) % +(of(skc14, skc18, skc17)) % +(of(skc14, skc19, skc17)) % +(man(skc14, skc17)) % +(male(skc13, skc17)) % +(human_person(skc13, skc17)) % +(forename(skc14, skc19)) % +(relname(skc13, skc19)) % +(jules_forename(skc14, skc19)) % +(forename(skc14, skc18)) % +(relname(skc13, skc18)) % +(jules_forename(skc14, skc18)) % +(eventuality(skc14, skc20)) % +(of(skc14, skc24, skc25)) % +(agent(skc14, skc23, skc25)) % +(vincent_forename(skc14, skc24)) % +(vincent_forename(skc14, skc21)) % +(forename(skc14, skc24)) % +(forename(skc14, skc21)) % +(man(skc14, skc25)) % +(proposition(skc14, skc14)) % +(think_believe_consider(skc14, skc23)) % +(present(skc14, skc23)) % +(event(skc14, skc23)) % +(relation(skc13, skc14)) % +(relname(skc13, skc21)) % +(eventuality(skc13, skc23)) % +(relname(skc13, skc24)) % +(male(skc13, skc25)) % +(human_person(skc13, skc25)) % +(theme(skc13, skc23, skc22)) % +(proposition(skc13, skc22)) % +(accessible_world(skc13, skc22)) % +(theme(skc13, skc15, skc14)) % +(agent(skc13, skc15, skc17)) % +(event(skc13, skc15)) % +(present(skc13, skc15)) % +(think_believe_consider(skc13, skc15)) % +(be(skc13, skc16, skc17, skc17)) % +(state(skc13, skc16)) % +(of(skc13, skc21, skc17)) % +(agent(skc14, skc20, skc17)) % +(of(skc13, skc18, skc17)) % +(of(skc13, skc19, skc17)) % +(man(skc13, skc17)) % +(forename(skc13, skc19)) % +(jules_forename(skc13, skc19)) % +(forename(skc13, skc18)) % +(jules_forename(skc13, skc18)) % +(smoke(skc14, skc20)) % +(present(skc14, skc20)) % +(event(skc14, skc20)) % +(accessible_world(skc13, skc14)) % +(proposition(skc13, skc14)) % +(vincent_forename(skc13, skc21)) % +(forename(skc13, skc21)) % +(agent(skc13, skc23, skc25)) % +(think_believe_consider(skc13, skc23)) % +(present(skc13, skc23)) % +(event(skc13, skc23)) % +(of(skc13, skc24, skc25)) % +(vincent_forename(skc13, skc24)) % +(forename(skc13, skc24)) % +(man(skc13, skc25)) % +(actual_world(skc13)) % +(skc22(skc22)) % +(skc15(skc15)) % +(skc16(skc16)) % +(skc17(skc17)) % +(skc19(skc19)) % +(skc18(skc18)) % +(skc20(skc20)) % +(skc14(skc14)) % +(skc21(skc21)) % +(skc23(skc23)) % +(skc24(skc24)) % +(skc25(skc25)) % +(skc13(skc13)) % +(skf1(_2418_492135, skf1(_2418_492135))) % +(_492141) % %------------------------------------------------------------------------------