%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP249-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art09.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:10:28 EST 2011 % Result : Satisfiable 139.02s % Output : Assurance 139.02s % 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/NLP249-1+eq_rstfp.tme % result written to : /tmp/NLP249-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP249-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP249-1+eq_rstfp-eqt.tme % System...................: Linux art09.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...: [+(_9036)] % 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...: 1258 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 138.52 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc20, skf1(V_2447_9110))) % -(tpos(skc18, skf1(V_2447_9120))) % -(tpos(skc22, skf1(V_2447_9130))) % -(tpos(skc26, skf1(V_2447_9140))) % -(jules_forename(skc14, skf1(V_2447_9150))) % -(vincent_forename(skc14, skf1(V_2447_9160))) % -(jules_forename(skc16, skc21)) % -(vincent_forename(skc16, skc21)) % -(skc18(skf1(V_2447_9183))) % -(skc22(skf1(V_2447_9192))) % -(skc20(skf1(V_2447_9201))) % -(skc26(skf1(V_2447_9210))) % -(jules_forename(skc13, skf1(V_2447_9220))) % -(vincent_forename(skc13, skf1(V_2447_9230))) % -(tpos(skc16, skf1(V_2447_9240))) % -(tpos(skc14, skf1(V_2447_9250))) % -(be(U_2501_9260, V_2502_9261, skf1(V_2447_9264), skc18)) % -(be(U_2479_9274, V_2480_9275, skc18, skf1(V_2447_9278))) % -(be(U_2501_9288, V_2502_9289, skf1(V_2447_9292), skc22)) % -(be(U_2479_9302, V_2480_9303, skc22, skf1(V_2447_9306))) % -(be(U_2501_9316, V_2502_9317, skf1(V_2447_9320), skc20)) % -(be(U_2479_9330, V_2480_9331, skc20, skf1(V_2447_9334))) % -(be(U_2501_9344, V_2502_9345, skc20, skc21)) % -(be(U_2479_9355, V_2480_9356, skc21, skc20)) % -(be(U_2501_9366, V_2502_9367, skc18, skc21)) % -(be(U_2479_9377, V_2480_9378, skc21, skc18)) % -(be(U_2501_9388, V_2502_9389, skc22, skc21)) % -(be(U_2479_9399, V_2480_9400, skc21, skc22)) % -(be(U_2501_9410, V_2502_9411, skf1(V_2447_9414), skc26)) % -(be(U_2479_9424, V_2480_9425, skc26, skf1(V_2447_9428))) % -(be(U_2501_9438, V_2502_9439, skc21, skc26)) % -(be(U_2479_9449, V_2480_9450, skc26, skc21)) % -(forename(skc14, skf1(V_2447_9460))) % -(forename(skc16, skc21)) % -(be(U_2501_9477, V_2502_9478, skf1(V_2447_9481), skc16)) % -(be(U_2479_9491, V_2480_9492, skc16, skf1(V_2447_9495))) % -(forename(skc13, skf1(V_2447_9505))) % -(jules_forename(skc16, skf1(V_2447_9515))) % -(vincent_forename(skc16, skf1(V_2447_9525))) % -(skc14(skf1(V_2447_9534))) % -(skc16(skf1(V_2447_9543))) % -(tpos(skf1(V_2447_9553), skc18)) % -(tpos(skc21, skc18)) % -(be(U_2501_9570, V_2502_9571, skc24, skc18)) % -(be(U_2479_9581, V_2480_9582, skc18, skc24)) % -(be(U_2501_9592, V_2502_9593, skc15, skc18)) % -(be(U_2479_9603, V_2480_9604, skc18, skc15)) % -(be(U_2501_9614, V_2502_9615, skc17, skc18)) % -(be(U_2479_9625, V_2480_9626, skc18, skc17)) % -(tpos(skf1(V_2447_9636), skc22)) % -(tpos(skc21, skc22)) % -(be(U_2501_9653, V_2502_9654, skc24, skc22)) % -(be(U_2479_9664, V_2480_9665, skc22, skc24)) % -(be(U_2501_9675, V_2502_9676, skc15, skc22)) % -(be(U_2479_9686, V_2480_9687, skc22, skc15)) % -(be(U_2501_9697, V_2502_9698, skc17, skc22)) % -(be(U_2479_9708, V_2480_9709, skc22, skc17)) % -(tpos(skf1(V_2447_9719), skc20)) % -(tpos(skc21, skc20)) % -(be(U_2501_9736, V_2502_9737, skc24, skc20)) % -(be(U_2479_9747, V_2480_9748, skc20, skc24)) % -(be(U_2501_9758, V_2502_9759, skc15, skc20)) % -(be(U_2479_9769, V_2480_9770, skc20, skc15)) % -(be(U_2501_9780, V_2502_9781, skc17, skc20)) % -(be(U_2479_9791, V_2480_9792, skc20, skc17)) % -(tpos(skc20, skc21)) % -(tpos(skc18, skc21)) % -(tpos(skc22, skc21)) % -(tpos(skc26, skc21)) % -(be(U_2501_9830, V_2502_9831, skc16, skc21)) % -(be(U_2479_9841, V_2480_9842, skc21, skc16)) % -(be(U_2501_9852, V_2502_9853, skf1(V_2447_9856), skc14)) % -(be(U_2479_9866, V_2480_9867, skc14, skf1(V_2447_9870))) % -(be(U_2501_9880, V_2502_9881, skc21, skc14)) % -(be(U_2479_9891, V_2480_9892, skc14, skc21)) % -(tpos(skf1(V_2447_9902), skc26)) % -(tpos(skc21, skc26)) % -(be(U_2501_9919, V_2502_9920, skc24, skc26)) % -(be(U_2479_9930, V_2480_9931, skc26, skc24)) % -(be(U_2501_9941, V_2502_9942, skc15, skc26)) % -(be(U_2479_9952, V_2480_9953, skc26, skc15)) % -(be(U_2501_9963, V_2502_9964, skc17, skc26)) % -(be(U_2479_9974, V_2480_9975, skc26, skc17)) % -(jules_forename(skc14, skc24)) % -(vincent_forename(skc14, skc24)) % -(jules_forename(skc16, skc24)) % -(vincent_forename(skc16, skc24)) % -(tpos(skc20, skc24)) % -(tpos(skc18, skc24)) % -(tpos(skc22, skc24)) % -(tpos(skc26, skc24)) % -(human_person(skc14, skf1(V_2447_10041))) % -(relname(skc14, skf1(V_2447_10051))) % -(proposition(skc14, skf1(V_2447_10061))) % -(human_person(skc16, skc21)) % -(relname(skc16, skc21)) % -(proposition(skc16, skc21)) % -(tpos(skf1(V_2447_10092), skc16)) % -(tpos(skc21, skc16)) % -(be(U_2501_10109, V_2502_10110, skc24, skc16)) % -(be(U_2479_10120, V_2480_10121, skc16, skc24)) % -(tpos(skc19, skf1(V_2447_10131))) % -(tpos(skc25, skf1(V_2447_10141))) % -(human_person(skc13, skf1(V_2447_10151))) % -(relname(skc13, skf1(V_2447_10161))) % -(forename(skc16, skf1(V_2447_10171))) % -(proposition(skc13, skf1(V_2447_10181))) % -(jules_forename(skc14, skc15)) % -(vincent_forename(skc14, skc15)) % -(jules_forename(skc16, skc15)) % -(vincent_forename(skc16, skc15)) % -(tpos(skc20, skc15)) % -(tpos(skc18, skc15)) % -(tpos(skc22, skc15)) % -(tpos(skc26, skc15)) % -(be(U_2501_10247, V_2502_10248, skc16, skc15)) % -(be(U_2479_10258, V_2480_10259, 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(skc22, skc17)) % -(tpos(skc26, skc17)) % -(be(U_2501_10325, V_2502_10326, skc16, skc17)) % -(be(U_2479_10336, V_2480_10337, skc17, skc16)) % -(smoke(skc14, skc18)) % -(skf1(V_2447_10352, skc18)) % -(skc21(skc18)) % -(smoke(skc16, skc18)) % -(tpos(skc24, skc18)) % -(tpos(skc15, skc18)) % -(tpos(skc17, skc18)) % -(smoke(skc14, skc22)) % -(skf1(V_2447_10401, skc22)) % -(skc21(skc22)) % -(smoke(skc16, skc22)) % -(tpos(skc24, skc22)) % -(tpos(skc15, skc22)) % -(tpos(skc17, skc22)) % -(be(U_2501_10445, V_2502_10446, skc18, skc19)) % -(be(U_2479_10456, V_2480_10457, skc19, skc18)) % -(be(U_2501_10467, V_2502_10468, skc22, skc19)) % -(be(U_2479_10478, V_2480_10479, skc19, skc22)) % -(be(U_2501_10489, V_2502_10490, skc19, skc20)) % -(be(U_2479_10500, V_2480_10501, skc20, skc19)) % -(smoke(skc14, skc20)) % -(skf1(V_2447_10516, skc20)) % -(skc21(skc20)) % -(smoke(skc16, skc20)) % -(tpos(skc24, skc20)) % -(tpos(skc15, skc20)) % -(tpos(skc17, skc20)) % -(skc18(skc21)) % -(skc22(skc21)) % -(skc20(skc21)) % -(skc26(skc21)) % -(jules_forename(skc13, skc21)) % -(vincent_forename(skc13, skc21)) % -(tpos(skc16, skc21)) % -(tpos(skc14, skc21)) % -(tpos(skf1(V_2447_10612), skc14)) % -(tpos(skc21, skc14)) % -(be(U_2501_10629, V_2502_10630, skc24, skc14)) % -(be(U_2479_10640, V_2480_10641, skc14, skc24)) % -(be(U_2501_10651, V_2502_10652, skc15, skc14)) % -(be(U_2479_10662, V_2480_10663, skc14, skc15)) % -(be(U_2501_10673, V_2502_10674, skc17, skc14)) % -(be(U_2479_10684, V_2480_10685, skc14, skc17)) % -(be(U_2501_10695, V_2502_10696, skc20, skc25)) % -(be(U_2479_10706, V_2480_10707, skc25, skc20)) % -(be(U_2501_10717, V_2502_10718, skc18, skc25)) % -(be(U_2479_10728, V_2480_10729, skc25, skc18)) % -(be(U_2501_10739, V_2502_10740, skc22, skc25)) % -(be(U_2479_10750, V_2480_10751, skc25, skc22)) % -(be(U_2501_10761, V_2502_10762, skc19, skc26)) % -(be(U_2479_10772, V_2480_10773, skc26, skc19)) % -(be(U_2501_10783, V_2502_10784, skc25, skc26)) % -(be(U_2479_10794, V_2480_10795, skc26, skc25)) % -(smoke(skc14, skc26)) % -(skf1(V_2447_10810, skc26)) % -(skc21(skc26)) % -(smoke(skc16, skc26)) % -(tpos(skc24, skc26)) % -(tpos(skc15, skc26)) % -(tpos(skc17, skc26)) % -(forename(skc14, skc24)) % -(forename(skc16, skc24)) % -(skc18(skc24)) % -(skc22(skc24)) % -(skc20(skc24)) % -(skc26(skc24)) % -(jules_forename(skc13, skc24)) % -(vincent_forename(skc13, skc24)) % -(tpos(skc16, skc24)) % -(tpos(skc14, skc24)) % -(organism(skc14, skf1(V_2447_10920))) % -(relation(skc14, skf1(V_2447_10930))) % -(organism(skc16, skc21)) % -(relation(skc16, skc21)) % -(smoke(skc14, skc16)) % -(skf1(V_2447_10959, skc16)) % -(skc21(skc16)) % -(smoke(skc16, skc16)) % -(tpos(skc24, skc16)) % -(tpos(skc15, skc16)) % -(tpos(skc17, skc16)) % -(skc19(skf1(V_2447_11002))) % -(skc25(skf1(V_2447_11011))) % -(organism(skc13, skf1(V_2447_11021))) % -(human_person(skc16, skf1(V_2447_11031))) % -(relation(skc13, skf1(V_2447_11041))) % -(relname(skc16, skf1(V_2447_11051))) % -(proposition(skc16, skf1(V_2447_11061))) % -(forename(skc14, skc15)) % -(forename(skc16, skc15)) % -(skc18(skc15)) % -(skc22(skc15)) % -(skc20(skc15)) % -(skc26(skc15)) % -(jules_forename(skc13, skc15)) % -(vincent_forename(skc13, skc15)) % -(tpos(skc16, skc15)) % -(tpos(skc14, skc15)) % -(forename(skc14, skc17)) % -(forename(skc16, skc17)) % -(skc18(skc17)) % -(skc22(skc17)) % -(skc20(skc17)) % -(skc26(skc17)) % -(jules_forename(skc13, skc17)) % -(vincent_forename(skc13, skc17)) % -(tpos(skc16, skc17)) % -(tpos(skc14, skc17)) % -(tpos(skc19, skc18)) % -(tpos(skc25, skc18)) % -(organism(skc14, skc18)) % -(state(skc14, skc18)) % -(event(skc14, skc18)) % -(organism(skc16, skc18)) % -(state(skc16, skc18)) % -(event(skc16, skc18)) % -(skc24(skc18)) % -(skc15(skc18)) % -(skc17(skc18)) % -(smoke(skc13, skc18)) % -(tpos(skc19, skc22)) % -(tpos(skc25, skc22)) % -(organism(skc14, skc22)) % -(state(skc14, skc22)) % -(event(skc14, skc22)) % -(organism(skc16, skc22)) % -(state(skc16, skc22)) % -(event(skc16, skc22)) % -(skc24(skc22)) % -(skc15(skc22)) % -(skc17(skc22)) % -(smoke(skc13, skc22)) % -(jules_forename(skc14, skc19)) % -(vincent_forename(skc14, skc19)) % -(jules_forename(skc16, skc19)) % -(vincent_forename(skc16, skc19)) % -(be(U_2501_11393, V_2502_11394, skf1(V_2447_11397), skc19)) % -(be(U_2479_11407, V_2480_11408, skc19, skf1(V_2447_11411))) % -(tpos(skc20, skc19)) % -(tpos(skc18, skc19)) % -(tpos(skc22, skc19)) % -(tpos(skc26, skc19)) % -(be(U_2501_11449, V_2502_11450, skc16, skc19)) % -(be(U_2479_11460, V_2480_11461, skc19, skc16)) % -(tpos(skc19, skc20)) % -(tpos(skc25, skc20)) % -(organism(skc14, skc20)) % -(state(skc14, skc20)) % -(event(skc14, skc20)) % -(organism(skc16, skc20)) % -(state(skc16, skc20)) % -(event(skc16, skc20)) % -(skc24(skc20)) % -(skc15(skc20)) % -(skc17(skc20)) % -(smoke(skc13, skc20)) % -(be(U_2501_11552, V_2502_11553, skc19, skc21)) % -(be(U_2479_11563, V_2480_11564, skc21, skc19)) % -(forename(skc13, skc21)) % -(jules_forename(skc14, skc21)) % -(vincent_forename(skc14, skc21)) % -(skc14(skc21)) % -(skc16(skc21)) % -(be(U_2501_11607, V_2502_11608, skc19, skc14)) % -(be(U_2479_11618, V_2480_11619, skc14, skc19)) % -(smoke(skc14, skc14)) % -(skf1(V_2447_11634, skc14)) % -(skc21(skc14)) % -(smoke(skc16, skc14)) % -(tpos(skc24, skc14)) % -(tpos(skc15, skc14)) % -(tpos(skc17, skc14)) % -(jules_forename(skc14, skc25)) % -(vincent_forename(skc14, skc25)) % -(jules_forename(skc16, skc25)) % -(vincent_forename(skc16, skc25)) % -(be(U_2501_11706, V_2502_11707, skf1(V_2447_11710), skc25)) % -(be(U_2479_11720, V_2480_11721, skc25, skf1(V_2447_11724))) % -(be(U_2501_11734, V_2502_11735, skc21, skc25)) % -(be(U_2479_11745, V_2480_11746, skc25, skc21)) % -(tpos(skc20, skc25)) % -(tpos(skc18, skc25)) % -(tpos(skc22, skc25)) % -(tpos(skc26, skc25)) % -(be(U_2501_11784, V_2502_11785, skc16, skc25)) % -(be(U_2479_11795, V_2480_11796, skc25, skc16)) % -(be(U_2501_11806, V_2502_11807, skc14, skc25)) % -(be(U_2479_11817, V_2480_11818, skc25, skc14)) % -(tpos(skc19, skc26)) % -(tpos(skc25, skc26)) % -(organism(skc14, skc26)) % -(state(skc14, skc26)) % -(event(skc14, skc26)) % -(organism(skc16, skc26)) % -(state(skc16, skc26)) % -(event(skc16, skc26)) % -(skc24(skc26)) % -(skc15(skc26)) % -(skc17(skc26)) % -(smoke(skc13, skc26)) % -(human_person(skc14, skc24)) % -(human_person(skc16, skc24)) % -(relname(skc14, skc24)) % -(proposition(skc14, skc24)) % -(relname(skc16, skc24)) % -(proposition(skc16, skc24)) % -(forename(skc13, skc24)) % -(skc14(skc24)) % -(skc16(skc24)) % -(man(skc14, skf1(V_2447_11970))) % -(entity(skc14, skf1(V_2447_11980))) % -(abstraction(skc14, skf1(V_2447_11990))) % -(man(skc16, skc21)) % -(entity(skc16, skc21)) % -(abstraction(skc16, skc21)) % -(tpos(skc19, skc16)) % -(tpos(skc25, skc16)) % -(organism(skc14, skc16)) % -(state(skc14, skc16)) % -(event(skc14, skc16)) % -(organism(skc16, skc16)) % -(state(skc16, skc16)) % -(event(skc16, skc16)) % -(skc24(skc16)) % -(skc15(skc16)) % -(skc17(skc16)) % -(smoke(skc13, skc16)) % -(man(skc13, skf1(V_2447_12102))) % -(entity(skc13, skf1(V_2447_12112))) % -(organism(skc16, skf1(V_2447_12122))) % -(abstraction(skc13, skf1(V_2447_12132))) % -(relation(skc16, skf1(V_2447_12142))) % -(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)) % -(skc25(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)) % -(man(skc14, skc22)) % -(man(skc16, skc22)) % -(skc19(skc22)) % -(skc25(skc22)) % -(entity(skc14, skc22)) % -(eventuality(skc14, skc22)) % -(entity(skc16, skc22)) % -(eventuality(skc16, skc22)) % -(organism(skc13, skc22)) % -(state(skc13, skc22)) % -(event(skc13, skc22)) % -(human_person(skc14, skc22)) % -(human_person(skc16, skc22)) % -(forename(skc14, skc19)) % -(forename(skc16, skc19)) % -(tpos(skf1(V_2447_12466), skc19)) % -(tpos(skc21, skc19)) % -(skc18(skc19)) % -(skc22(skc19)) % -(skc20(skc19)) % -(skc26(skc19)) % -(jules_forename(skc13, skc19)) % -(vincent_forename(skc13, skc19)) % -(tpos(skc16, skc19)) % -(tpos(skc14, skc19)) % -(be(U_2501_12535, V_2502_12536, skc24, skc19)) % -(be(U_2479_12546, V_2480_12547, skc19, skc24)) % -(be(U_2501_12557, V_2502_12558, skc15, skc19)) % -(be(U_2479_12568, V_2480_12569, skc19, skc15)) % -(be(U_2501_12579, V_2502_12580, skc17, skc19)) % -(be(U_2479_12590, V_2480_12591, skc19, skc17)) % +(jules_forename(skc14, skc20)) % +(jules_forename(skc16, skc20)) % +(jules_forename(skc14, skc18)) % +(jules_forename(skc16, skc18)) % +(vincent_forename(skc14, skc22)) % +(vincent_forename(skc16, skc22)) % -(man(skc14, skc20)) % -(man(skc16, skc20)) % -(skc19(skc20)) % -(skc25(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)) % -(tpos(skc19, skc21)) % -(tpos(skc25, skc21)) % -(human_person(skc13, skc21)) % -(relname(skc13, skc21)) % -(forename(skc14, skc21)) % -(proposition(skc13, skc21)) % -(tpos(skc19, skc14)) % -(tpos(skc25, skc14)) % -(organism(skc14, skc14)) % -(state(skc14, skc14)) % -(event(skc14, skc14)) % -(organism(skc16, skc14)) % -(state(skc16, skc14)) % -(event(skc16, skc14)) % -(skc24(skc14)) % -(skc15(skc14)) % -(skc17(skc14)) % -(smoke(skc13, skc14)) % -(forename(skc14, skc25)) % -(forename(skc16, skc25)) % -(tpos(skf1(V_2447_12869), skc25)) % -(tpos(skc21, skc25)) % -(skc18(skc25)) % -(skc22(skc25)) % -(skc20(skc25)) % -(skc26(skc25)) % -(jules_forename(skc13, skc25)) % -(vincent_forename(skc13, skc25)) % -(tpos(skc16, skc25)) % -(tpos(skc14, skc25)) % -(be(U_2501_12938, V_2502_12939, skc24, skc25)) % -(be(U_2479_12949, V_2480_12950, skc25, skc24)) % -(be(U_2501_12960, V_2502_12961, skc15, skc25)) % -(be(U_2479_12971, V_2480_12972, skc25, skc15)) % -(be(U_2501_12982, V_2502_12983, skc17, skc25)) % -(be(U_2479_12993, V_2480_12994, skc25, skc17)) % -(man(skc14, skc26)) % -(man(skc16, skc26)) % -(skc19(skc26)) % -(skc25(skc26)) % -(entity(skc14, skc26)) % -(eventuality(skc14, skc26)) % -(entity(skc16, skc26)) % -(eventuality(skc16, skc26)) % -(organism(skc13, skc26)) % -(state(skc13, skc26)) % -(event(skc13, skc26)) % -(human_person(skc14, skc26)) % -(human_person(skc16, skc26)) % -(tpos(skc19, skc24)) % -(tpos(skc25, skc24)) % -(organism(skc14, skc24)) % -(organism(skc16, skc24)) % -(human_person(skc13, skc24)) % -(relation(skc14, skc24)) % -(relation(skc16, skc24)) % -(relname(skc13, skc24)) % -(proposition(skc13, skc24)) % -(male(skc14, skf1(V_2447_13156))) % -(existent(skc14, skf1(V_2447_13166))) % -(general(skc14, skf1(V_2447_13176))) % +(singleton(skc14, skf1(V_2447_13186))) % -(male(skc16, skc21)) % -(existent(skc16, skc21)) % -(general(skc16, skc21)) % +(singleton(skc16, skc21)) % -(man(skc14, skc16)) % -(man(skc16, skc16)) % -(skc19(skc16)) % -(skc25(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_13313))) % -(man(skc16, skf1(V_2447_13323))) % -(existent(skc13, skf1(V_2447_13333))) % -(entity(skc16, skf1(V_2447_13343))) % -(general(skc13, skf1(V_2447_13353))) % -(abstraction(skc16, skf1(V_2447_13363))) % -(tpos(skc19, skc15)) % -(tpos(skc25, 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(skc25, 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)) % -(male(skc14, skc22)) % -(male(skc16, skc22)) % -(man(skc13, skc22)) % -(specific(skc14, skc22)) % -(specific(skc16, skc22)) % -(entity(skc13, skc22)) % -(eventuality(skc13, skc22)) % -(human(skc14, skc22)) % -(human(skc16, skc22)) % -(human_person(skc13, skc22)) % +(singleton(skc14, skc22)) % +(singleton(skc16, skc22)) % -(relname(skc14, skc19)) % -(proposition(skc14, skc19)) % -(smoke(skc14, skc19)) % -(relname(skc16, skc19)) % -(proposition(skc16, skc19)) % -(skf1(V_2447_13700, skc19)) % -(skc21(skc19)) % -(smoke(skc16, skc19)) % -(forename(skc13, skc19)) % -(skc14(skc19)) % -(skc16(skc19)) % -(tpos(skc24, skc19)) % -(tpos(skc15, skc19)) % -(tpos(skc17, skc19)) % +(jules_forename(skc13, skc20)) % +(jules_forename(skc13, skc18)) % +(vincent_forename(skc13, skc22)) % -(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)) % -(skc19(skc21)) % -(skc25(skc21)) % -(organism(skc13, skc21)) % -(human_person(skc14, skc21)) % -(relation(skc13, skc21)) % -(relname(skc14, skc21)) % -(proposition(skc14, skc21)) % -(man(skc14, skc14)) % -(man(skc16, skc14)) % -(skc19(skc14)) % -(skc25(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)) % -(relname(skc14, skc25)) % -(proposition(skc14, skc25)) % -(smoke(skc14, skc25)) % -(relname(skc16, skc25)) % -(proposition(skc16, skc25)) % -(skf1(V_2447_14079, skc25)) % -(skc21(skc25)) % -(smoke(skc16, skc25)) % -(forename(skc13, skc25)) % -(skc14(skc25)) % -(skc16(skc25)) % -(tpos(skc24, skc25)) % -(tpos(skc15, skc25)) % -(tpos(skc17, skc25)) % -(nonexistent(skc14, skc25)) % -(nonexistent(skc16, skc25)) % -(general(skc14, skc25)) % -(general(skc16, skc25)) % +(singleton(skc14, skc25)) % +(singleton(skc16, skc25)) % -(male(skc14, skc26)) % -(male(skc16, skc26)) % -(man(skc13, skc26)) % -(specific(skc14, skc26)) % -(specific(skc16, skc26)) % -(entity(skc13, skc26)) % -(eventuality(skc13, skc26)) % -(human(skc14, skc26)) % -(human(skc16, skc26)) % -(human_person(skc13, skc26)) % +(singleton(skc14, skc26)) % +(singleton(skc16, skc26)) % -(man(skc14, skc24)) % -(man(skc16, skc24)) % -(skc19(skc24)) % -(skc25(skc24)) % -(entity(skc14, skc24)) % -(entity(skc16, skc24)) % -(organism(skc13, skc24)) % -(abstraction(skc14, skc24)) % -(abstraction(skc16, skc24)) % -(relation(skc13, skc24)) % +(unisex(skc14, skf1(V_2447_14336))) % +(nonexistent(skc14, skf1(V_2447_14346))) % +(specific(skc14, skf1(V_2447_14356))) % +(thing(skc14, skf1(V_2447_14366))) % +(unisex(skc16, skc21)) % +(nonexistent(skc16, skc21)) % +(specific(skc16, skc21)) % +(thing(skc16, skc21)) % -(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_14488))) % -(existent(skc16, skf1(V_2447_14498))) % -(general(skc16, skf1(V_2447_14508))) % +(singleton(skc16, skf1(V_2447_14518))) % -(man(skc14, skc15)) % -(man(skc16, skc15)) % -(skc19(skc15)) % -(skc25(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)) % -(skc25(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)) % +(unisex(skc14, skc22)) % +(unisex(skc16, skc22)) % -(male(skc13, skc22)) % +(general(skc14, skc22)) % +(general(skc16, skc22)) % -(specific(skc13, skc22)) % +(nonhuman(skc14, skc22)) % +(nonhuman(skc16, skc22)) % -(human(skc13, skc22)) % +(thing(skc14, skc22)) % +(thing(skc16, skc22)) % +(singleton(skc13, skc22)) % -(relation(skc14, skc19)) % -(state(skc14, skc19)) % -(event(skc14, skc19)) % -(relation(skc16, skc19)) % -(state(skc16, skc19)) % -(event(skc16, skc19)) % -(relname(skc13, skc19)) % -(proposition(skc13, skc19)) % -(skc24(skc19)) % -(skc15(skc19)) % -(skc17(skc19)) % -(smoke(skc13, skc19)) % +(skc20(skc22)) % +(skc20(skc18)) % +(skc22(skc20)) % +(skc22(skc18)) % +(skc18(skc20)) % +(skc18(skc22)) % +(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)) % -(man(skc13, skc21)) % -(entity(skc13, skc21)) % -(organism(skc14, skc21)) % -(abstraction(skc13, skc21)) % -(relation(skc14, skc21)) % -(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)) % -(relation(skc14, skc25)) % -(state(skc14, skc25)) % -(event(skc14, skc25)) % -(relation(skc16, skc25)) % -(state(skc16, skc25)) % -(event(skc16, skc25)) % -(relname(skc13, skc25)) % -(proposition(skc13, skc25)) % -(skc24(skc25)) % -(skc15(skc25)) % -(skc17(skc25)) % -(smoke(skc13, skc25)) % +(existent(skc14, skc25)) % +(existent(skc16, skc25)) % -(nonexistent(skc13, skc25)) % +(specific(skc14, skc25)) % +(specific(skc16, skc25)) % -(general(skc13, skc25)) % +(thing(skc14, skc25)) % +(thing(skc16, skc25)) % +(singleton(skc13, skc25)) % +(unisex(skc14, skc26)) % +(unisex(skc16, skc26)) % -(male(skc13, skc26)) % +(general(skc14, skc26)) % +(general(skc16, skc26)) % -(specific(skc13, skc26)) % +(nonhuman(skc14, skc26)) % +(nonhuman(skc16, skc26)) % -(human(skc13, skc26)) % +(thing(skc14, skc26)) % +(thing(skc16, skc26)) % +(singleton(skc13, skc26)) % -(male(skc14, skc24)) % -(male(skc16, skc24)) % -(man(skc13, skc24)) % -(existent(skc14, skc24)) % -(existent(skc16, skc24)) % -(entity(skc13, skc24)) % -(general(skc14, skc24)) % -(general(skc16, skc24)) % -(abstraction(skc13, skc24)) % +(singleton(skc14, skc24)) % +(singleton(skc16, skc24)) % +(eventuality(skc14, skf1(V_2447_15520))) % +(theme(skc14, skc17, skc14)) % +(theme(skc16, skc17, skc14)) % +(theme(skc14, skc15, skc16)) % +(theme(skc16, skc15, skc16)) % +(eventuality(skc16, skc21)) % +(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_15653))) % +(nonexistent(skc16, skf1(V_2447_15663))) % +(specific(skc16, skf1(V_2447_15673))) % +(thing(skc16, skf1(V_2447_15683))) % -(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, skc22)) % +(abstraction(skc16, skc22)) % +(unisex(skc13, skc22)) % +(general(skc13, skc22)) % +(nonhuman(skc13, skc22)) % +(thing(skc13, skc22)) % -(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, skc22)) % +(tpos(skc20, skc18)) % +(tpos(skc22, skc20)) % +(tpos(skc22, skc22)) % +(tpos(skc22, skc18)) % +(tpos(skc18, skc20)) % +(tpos(skc18, skc22)) % +(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)) % -(male(skc13, skc21)) % -(man(skc14, skc21)) % -(existent(skc13, skc21)) % -(entity(skc14, skc21)) % -(general(skc13, skc21)) % -(abstraction(skc14, skc21)) % +(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)) % -(abstraction(skc14, skc25)) % -(eventuality(skc14, skc25)) % -(abstraction(skc16, skc25)) % -(eventuality(skc16, skc25)) % -(relation(skc13, skc25)) % -(state(skc13, skc25)) % -(event(skc13, skc25)) % -(nonhuman(skc14, skc25)) % -(nonhuman(skc16, skc25)) % +(living(skc14, skc25)) % +(living(skc16, skc25)) % +(impartial(skc14, skc25)) % +(impartial(skc16, skc25)) % +(tpos(skc26, skc26)) % +(entity(skc14, skc25)) % +(entity(skc16, skc25)) % +(existent(skc13, skc25)) % +(specific(skc13, skc25)) % +(thing(skc13, skc25)) % +(abstraction(skc14, skc26)) % +(abstraction(skc16, skc26)) % +(unisex(skc13, skc26)) % +(general(skc13, skc26)) % +(nonhuman(skc13, skc26)) % +(thing(skc13, skc26)) % +(unisex(skc14, skc24)) % +(unisex(skc16, skc24)) % -(male(skc13, skc24)) % +(nonexistent(skc14, skc24)) % +(nonexistent(skc16, skc24)) % -(existent(skc13, skc24)) % +(specific(skc14, skc24)) % +(specific(skc16, skc24)) % -(general(skc13, skc24)) % +(thing(skc14, skc24)) % +(thing(skc16, skc24)) % +(singleton(skc13, skc24)) % +(agent(skc14, skf1(skc19), skc19)) % +(agent(skc14, skf1(skc25), skc25)) % +(event(skc14, skf1(V_2447_16567))) % +(present(skc14, skf1(V_2447_16577))) % +(smoke(skc14, skf1(V_2447_16587))) % +(theme(skc13, skc17, skc14)) % +(theme(skc13, skc15, skc16)) % +(agent(skc16, skc21, skc19)) % +(smoke(skc16, skc21)) % +(present(skc16, skc21)) % +(event(skc16, skc21)) % +(abstraction(skc14, skc16)) % +(abstraction(skc16, skc16)) % +(unisex(skc13, skc16)) % +(general(skc13, skc16)) % +(nonhuman(skc13, skc16)) % +(thing(skc13, skc16)) % +(eventuality(skc16, skf1(V_2447_16684))) % +(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)) % +(relation(skc14, skc22)) % +(relation(skc16, skc22)) % +(abstraction(skc13, skc22)) % -(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)) % -(male(skc14, skc21)) % -(existent(skc14, skc21)) % -(general(skc14, skc21)) % +(singleton(skc14, skc21)) % +(abstraction(skc14, skc14)) % +(abstraction(skc16, skc14)) % +(unisex(skc13, skc14)) % +(general(skc13, skc14)) % +(nonhuman(skc13, skc14)) % +(thing(skc13, skc14)) % -(unisex(skc14, skc25)) % -(unisex(skc16, skc25)) % -(abstraction(skc13, skc25)) % -(eventuality(skc13, skc25)) % +(animate(skc14, skc25)) % +(animate(skc16, skc25)) % +(human(skc14, skc25)) % +(human(skc16, skc25)) % -(nonhuman(skc13, skc25)) % +(organism(skc14, skc25)) % +(organism(skc16, skc25)) % +(living(skc13, skc25)) % +(impartial(skc13, skc25)) % +(entity(skc13, skc25)) % +(relation(skc14, skc26)) % +(relation(skc16, skc26)) % +(abstraction(skc13, skc26)) % +(event(skc14, skc24)) % +(event(skc16, skc24)) % +(eventuality(skc14, skc24)) % +(eventuality(skc16, skc24)) % +(unisex(skc13, skc24)) % +(nonexistent(skc13, skc24)) % +(specific(skc13, skc24)) % +(thing(skc13, skc24)) % +(skc16(skc14)) % +(skc14(skc16)) % +(relation(skc14, skc16)) % +(relation(skc16, skc16)) % +(abstraction(skc13, skc16)) % +(agent(skc16, skf1(skc25), skc25)) % +(agent(skc16, skf1(skc19), skc19)) % +(event(skc16, skf1(V_2447_17321))) % +(present(skc16, skf1(V_2447_17331))) % +(smoke(skc16, skf1(V_2447_17341))) % +(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)) % +(relname(skc14, skc22)) % +(relname(skc16, skc22)) % +(relation(skc13, skc22)) % +(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)) % +(unisex(skc14, skc21)) % +(nonexistent(skc14, skc21)) % +(specific(skc14, skc21)) % +(thing(skc14, skc21)) % +(relation(skc14, skc14)) % +(relation(skc16, skc14)) % +(abstraction(skc13, skc14)) % +(male(skc14, skc25)) % +(male(skc16, skc25)) % -(unisex(skc13, skc25)) % +(human_person(skc14, skc25)) % +(human_person(skc16, skc25)) % +(animate(skc13, skc25)) % +(human(skc13, skc25)) % +(organism(skc13, skc25)) % +(relname(skc14, skc26)) % +(relname(skc16, skc26)) % +(relation(skc13, skc26)) % +(be(skc14, skc24, skc25, skc25)) % +(be(skc16, skc24, skc25, skc25)) % +(tpos(skc25, skc25)) % +(state(skc14, skc24)) % +(state(skc16, skc24)) % +(event(skc13, skc24)) % +(eventuality(skc13, skc24)) % +(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, skc26, skc25)) % +(of(skc16, skc20, skc19)) % +(of(skc16, skc22, skc19)) % +(of(skc16, skc18, skc19)) % +(theme(skc16, skc15, skc14)) % +(agent(skc16, skc17, skc19)) % +(agent(skc16, skc15, skc19)) % +(jules_forename(skc16, skc26)) % +(jules_forename(skc16, skc22)) % +(vincent_forename(skc16, skc20)) % +(vincent_forename(skc16, skc18)) % +(forename(skc16, skc26)) % +(forename(skc16, skc20)) % +(forename(skc16, skc22)) % +(forename(skc16, skc18)) % +(man(skc16, skc25)) % +(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, skc22, skc19)) % +(forename(skc14, skc22)) % +(relname(skc13, skc22)) % +(jules_forename(skc14, skc22)) % +(of(skc14, skc20, skc19)) % +(man(skc14, skc19)) % +(male(skc13, skc19)) % +(human_person(skc13, skc19)) % +(vincent_forename(skc14, skc20)) % +(forename(skc14, skc20)) % +(relname(skc13, skc20)) % +(eventuality(skc14, skc21)) % +(of(skc14, skc26, skc25)) % +(jules_forename(skc14, skc26)) % +(forename(skc14, skc26)) % +(man(skc14, skc25)) % +(proposition(skc14, skc14)) % +(relation(skc13, skc14)) % +(male(skc13, skc25)) % +(human_person(skc13, skc25)) % +(relname(skc13, skc26)) % +(be(skc13, skc24, skc25, skc25)) % +(state(skc13, skc24)) % +(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, skc22, skc19)) % +(forename(skc13, skc22)) % +(jules_forename(skc13, skc22)) % +(agent(skc14, skc21, skc19)) % +(of(skc13, skc20, skc19)) % +(man(skc13, skc19)) % +(vincent_forename(skc13, skc20)) % +(forename(skc13, skc20)) % +(smoke(skc14, skc21)) % +(present(skc14, skc21)) % +(event(skc14, skc21)) % +(accessible_world(skc13, skc14)) % +(proposition(skc13, skc14)) % +(of(skc13, skc26, skc25)) % +(man(skc13, skc25)) % +(forename(skc13, skc26)) % +(jules_forename(skc13, skc26)) % +(actual_world(skc13)) % +(skc24(skc24)) % +(skc16(skc16)) % +(skc15(skc15)) % +(skc17(skc17)) % +(skc18(skc18)) % +(skc22(skc22)) % +(skc19(skc19)) % +(skc20(skc20)) % +(skc21(skc21)) % +(skc14(skc14)) % +(skc25(skc25)) % +(skc26(skc26)) % +(skc13(skc13)) % +(skf1(_2418_18563, skf1(_2418_18563))) % +(_18569) % %------------------------------------------------------------------------------