FDP---0.9.16.SAT-Ass.s

%------------------------------------------------------------------------------
% File     : FDP---0.9.16
% Problem  : NLP224-1 : TPTP v5.0.0. Released v2.4.0.
% Transfm  : add_equality
% Format   : protein
% Command  : fdp-casc %s %d

% Computer : art05.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 22:59:15 EST 2011

% Result   : Satisfiable 16.22s
% Output   : Assurance 16.22s
% 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/NLP224-1+eq_rstfp.tme
% result written to : /tmp/NLP224-1+eq_rstfp-eqt.tme
% FDPLL - A First-Order Davis-Putnam Theorem Prover
% Version 0.9.16 (26/06/2002)
% Proving /tmp/NLP224-1+eq_rstfp-eqt ...
% Done.
% Input File...............: /tmp/NLP224-1+eq_rstfp-eqt.tme
% System...................: Linux art05.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...: [+(_240864)]
% 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...: 621
% # Unit back subsumptions.: 0
% # Branches closed........: 0
% # Level cuts.............: 0
% Time.....................: 15.78 seconds.
% Result...................: SATISFIABLE with model:
%   -(tpos(skc12, skf1(V_2447_240938)))
%   -(tpos(skc16, skf1(V_2447_240948)))
%   -(tpos(skc14, skf1(V_2447_240958)))
%   -(skc12(skf1(V_2447_240967)))
%   -(skc16(skf1(V_2447_240976)))
%   -(vincent_forename(skc9, skf1(V_2447_240986)))
%   -(jules_forename(skc9, skf1(V_2447_240996)))
%   -(be(U_2501_241006, V_2502_241007, skf1(V_2447_241010), skc12))
%   -(be(U_2479_241020, V_2480_241021, skc12, skf1(V_2447_241024)))
%   -(be(U_2501_241034, V_2502_241035, skf1(V_2447_241038), skc16))
%   -(be(U_2479_241048, V_2480_241049, skc16, skf1(V_2447_241052)))
%   -(be(U_2501_241062, V_2502_241063, skf1(V_2447_241066), skc14))
%   -(be(U_2479_241076, V_2480_241077, skc14, skf1(V_2447_241080)))
%   -(skc14(skf1(V_2447_241089)))
%   -(forename(skc9, skf1(V_2447_241099)))
%   -(vincent_forename(skc14, skf1(V_2447_241109)))
%   -(jules_forename(skc14, skf1(V_2447_241119)))
%   -(tpos(skf1(V_2447_241129), skc12))
%   -(be(U_2501_241139, V_2502_241140, skc10, skc12))
%   -(be(U_2479_241150, V_2480_241151, skc12, skc10))
%   -(be(U_2501_241161, V_2502_241162, skc12, skc15))
%   -(be(U_2479_241172, V_2480_241173, skc15, skc12))
%   -(tpos(skf1(V_2447_241183), skc16))
%   -(be(U_2501_241193, V_2502_241194, skc15, skc16))
%   -(be(U_2479_241204, V_2480_241205, skc16, skc15))
%   -(be(U_2501_241215, V_2502_241216, skc10, skc16))
%   -(be(U_2479_241226, V_2480_241227, skc16, skc10))
%   -(tpos(skf1(V_2447_241237), skc14))
%   -(tpos(skc13, skf1(V_2447_241247)))
%   -(tpos(skc11, skf1(V_2447_241257)))
%   -(tpos(skc17, skf1(V_2447_241267)))
%   -(human_person(skc9, skf1(V_2447_241277)))
%   -(proposition(skc9, skf1(V_2447_241287)))
%   -(relname(skc9, skf1(V_2447_241297)))
%   -(forename(skc14, skf1(V_2447_241307)))
%   -(vincent_forename(skc14, skc10))
%   -(jules_forename(skc14, skc10))
%   -(be(U_2501_241331, V_2502_241332, skc14, skc10))
%   -(be(U_2479_241342, V_2480_241343, skc10, skc14))
%   -(tpos(skc12, skc10))
%   -(tpos(skc16, skc10))
%   -(be(U_2501_241367, V_2502_241368, skc11, skc12))
%   -(be(U_2479_241378, V_2480_241379, skc12, skc11))
%   -(skf1(V_2447_241387, skc12))
%   -(smoke(skc14, skc12))
%   -(tpos(skc15, skc12))
%   -(tpos(skc10, skc12))
%   -(be(U_2501_241418, V_2502_241419, skc12, skc13))
%   -(be(U_2479_241429, V_2480_241430, skc13, skc12))
%   -(vincent_forename(skc14, skc15))
%   -(jules_forename(skc14, skc15))
%   -(be(U_2501_241454, V_2502_241455, skc14, skc15))
%   -(be(U_2479_241465, V_2480_241466, skc15, skc14))
%   -(tpos(skc12, skc15))
%   -(tpos(skc16, skc15))
%   -(be(U_2501_241490, V_2502_241491, skc13, skc16))
%   -(be(U_2479_241501, V_2480_241502, skc16, skc13))
%   -(be(U_2501_241512, V_2502_241513, skc11, skc16))
%   -(be(U_2479_241523, V_2480_241524, skc16, skc11))
%   -(skf1(V_2447_241532, skc16))
%   -(smoke(skc14, skc16))
%   -(tpos(skc15, skc16))
%   -(tpos(skc10, skc16))
%   -(be(U_2501_241563, V_2502_241564, skc12, skc17))
%   -(be(U_2479_241574, V_2480_241575, skc17, skc12))
%   -(be(U_2501_241585, V_2502_241586, skc16, skc17))
%   -(be(U_2479_241596, V_2480_241597, skc17, skc16))
%   -(skf1(V_2447_241605, skc14))
%   -(smoke(skc14, skc14))
%   -(tpos(skc15, skc14))
%   -(tpos(skc10, skc14))
%   -(skc11(skf1(V_2447_241635)))
%   -(skc13(skf1(V_2447_241644)))
%   -(skc17(skf1(V_2447_241653)))
%   -(organism(skc9, skf1(V_2447_241663)))
%   -(human_person(skc14, skf1(V_2447_241673)))
%   -(relation(skc9, skf1(V_2447_241683)))
%   -(proposition(skc14, skf1(V_2447_241693)))
%   -(relname(skc14, skf1(V_2447_241703)))
%   -(forename(skc14, skc10))
%   -(tpos(skc14, skc10))
%   -(skc12(skc10))
%   -(skc16(skc10))
%   -(vincent_forename(skc9, skc10))
%   -(jules_forename(skc9, skc10))
%   -(vincent_forename(skc14, skc11))
%   -(jules_forename(skc14, skc11))
%   -(be(U_2501_241767, V_2502_241768, skf1(V_2447_241771), skc11))
%   -(be(U_2479_241781, V_2480_241782, skc11, skf1(V_2447_241785)))
%   -(be(U_2501_241795, V_2502_241796, skc14, skc11))
%   -(be(U_2479_241806, V_2480_241807, skc11, skc14))
%   -(tpos(skc12, skc11))
%   -(tpos(skc16, skc11))
%   -(tpos(skc13, skc12))
%   -(tpos(skc11, skc12))
%   -(tpos(skc17, skc12))
%   -(organism(skc14, skc12))
%   -(event(skc14, skc12))
%   -(state(skc14, skc12))
%   -(skc15(skc12))
%   -(smoke(skc9, skc12))
%   -(skc10(skc12))
%   -(vincent_forename(skc14, skc13))
%   -(jules_forename(skc14, skc13))
%   -(be(U_2501_241906, V_2502_241907, skf1(V_2447_241910), skc13))
%   -(be(U_2479_241920, V_2480_241921, skc13, skf1(V_2447_241924)))
%   -(be(U_2501_241934, V_2502_241935, skc14, skc13))
%   -(be(U_2479_241945, V_2480_241946, skc13, skc14))
%   -(tpos(skc12, skc13))
%   -(tpos(skc16, skc13))
%   -(forename(skc14, skc15))
%   -(tpos(skc14, skc15))
%   -(skc12(skc15))
%   -(skc16(skc15))
%   -(vincent_forename(skc9, skc15))
%   -(jules_forename(skc9, skc15))
%   -(tpos(skc13, skc16))
%   -(tpos(skc11, skc16))
%   -(tpos(skc17, skc16))
%   -(organism(skc14, skc16))
%   -(event(skc14, skc16))
%   -(state(skc14, skc16))
%   -(skc15(skc16))
%   -(smoke(skc9, skc16))
%   -(skc10(skc16))
%   -(vincent_forename(skc14, skc17))
%   -(jules_forename(skc14, skc17))
%   -(be(U_2501_242085, V_2502_242086, skf1(V_2447_242089), skc17))
%   -(be(U_2479_242099, V_2480_242100, skc17, skf1(V_2447_242103)))
%   -(be(U_2501_242113, V_2502_242114, skc14, skc17))
%   -(be(U_2479_242124, V_2480_242125, skc17, skc14))
%   -(tpos(skc12, skc17))
%   -(tpos(skc16, skc17))
%   -(tpos(skc13, skc14))
%   -(tpos(skc11, skc14))
%   -(tpos(skc17, skc14))
%   -(organism(skc14, skc14))
%   -(event(skc14, skc14))
%   -(state(skc14, skc14))
%   -(skc15(skc14))
%   -(smoke(skc9, skc14))
%   -(skc10(skc14))
%   -(man(skc9, skf1(V_2447_242210)))
%   -(entity(skc9, skf1(V_2447_242220)))
%   -(organism(skc14, skf1(V_2447_242230)))
%   -(abstraction(skc9, skf1(V_2447_242240)))
%   -(relation(skc14, skf1(V_2447_242250)))
%   -(human_person(skc14, skc10))
%   -(proposition(skc14, skc10))
%   -(relname(skc14, skc10))
%   -(skc14(skc10))
%   -(forename(skc9, skc10))
%   -(forename(skc14, skc11))
%   -(tpos(skf1(V_2447_242301), skc11))
%   -(tpos(skc14, skc11))
%   -(skc12(skc11))
%   -(skc16(skc11))
%   -(vincent_forename(skc9, skc11))
%   -(jules_forename(skc9, skc11))
%   -(be(U_2501_242344, V_2502_242345, skc10, skc11))
%   -(be(U_2479_242355, V_2480_242356, skc11, skc10))
%   -(man(skc14, skc12))
%   -(skc11(skc12))
%   -(skc13(skc12))
%   -(skc17(skc12))
%   -(entity(skc14, skc12))
%   -(eventuality(skc14, skc12))
%   -(organism(skc9, skc12))
%   -(event(skc9, skc12))
%   -(state(skc9, skc12))
%   -(human_person(skc14, skc12))
%   -(forename(skc14, skc13))
%   -(tpos(skf1(V_2447_242440), skc13))
%   -(tpos(skc14, skc13))
%   -(skc12(skc13))
%   -(skc16(skc13))
%   -(vincent_forename(skc9, skc13))
%   -(jules_forename(skc9, skc13))
%   -(be(U_2501_242483, V_2502_242484, skc10, skc13))
%   -(be(U_2479_242494, V_2480_242495, skc13, skc10))
%   -(be(U_2501_242505, V_2502_242506, skc13, skc15))
%   -(be(U_2479_242516, V_2480_242517, skc15, skc13))
%   -(be(U_2501_242527, V_2502_242528, skc11, skc15))
%   -(be(U_2479_242538, V_2480_242539, skc15, skc11))
%   -(human_person(skc14, skc15))
%   -(proposition(skc14, skc15))
%   -(relname(skc14, skc15))
%   -(skc14(skc15))
%   -(forename(skc9, skc15))
%   -(man(skc14, skc16))
%   -(skc11(skc16))
%   -(skc13(skc16))
%   -(skc17(skc16))
%   -(entity(skc14, skc16))
%   -(eventuality(skc14, skc16))
%   -(organism(skc9, skc16))
%   -(event(skc9, skc16))
%   -(state(skc9, skc16))
%   -(human_person(skc14, skc16))
%   -(forename(skc14, skc17))
%   -(tpos(skf1(V_2447_242657), skc17))
%   -(tpos(skc14, skc17))
%   -(skc12(skc17))
%   -(skc16(skc17))
%   -(vincent_forename(skc9, skc17))
%   -(jules_forename(skc9, skc17))
%   -(be(U_2501_242700, V_2502_242701, skc15, skc17))
%   -(be(U_2479_242711, V_2480_242712, skc17, skc15))
%   -(be(U_2501_242722, V_2502_242723, skc10, skc17))
%   -(be(U_2479_242733, V_2480_242734, skc17, skc10))
%   -(man(skc14, skc14))
%   -(skc11(skc14))
%   -(skc13(skc14))
%   -(skc17(skc14))
%   -(entity(skc14, skc14))
%   -(eventuality(skc14, skc14))
%   -(organism(skc9, skc14))
%   -(event(skc9, skc14))
%   -(state(skc9, skc14))
%   -(human_person(skc14, skc14))
%   -(male(skc9, skf1(V_2447_242811)))
%   -(man(skc14, skf1(V_2447_242821)))
%   -(existent(skc9, skf1(V_2447_242831)))
%   -(entity(skc14, skf1(V_2447_242841)))
%   -(general(skc9, skf1(V_2447_242851)))
%   -(abstraction(skc14, skf1(V_2447_242861)))
%   -(tpos(skc13, skc10))
%   -(tpos(skc11, skc10))
%   -(tpos(skc17, skc10))
%   -(organism(skc14, skc10))
%   -(human_person(skc9, skc10))
%   -(relation(skc14, skc10))
%   -(proposition(skc9, skc10))
%   -(relname(skc9, skc10))
%   -(proposition(skc14, skc11))
%   -(relname(skc14, skc11))
%   -(skf1(V_2447_242939, skc11))
%   -(smoke(skc14, skc11))
%   -(skc14(skc11))
%   -(forename(skc9, skc11))
%   -(tpos(skc15, skc11))
%   -(tpos(skc10, skc11))
%   -(nonexistent(skc14, skc11))
%   -(general(skc14, skc11))
%   +(singleton(skc14, skc11))
%   -(male(skc14, skc12))
%   -(man(skc9, skc12))
%   -(specific(skc14, skc12))
%   -(entity(skc9, skc12))
%   -(eventuality(skc9, skc12))
%   -(human(skc14, skc12))
%   -(human_person(skc9, skc12))
%   +(singleton(skc14, skc12))
%   -(proposition(skc14, skc13))
%   -(relname(skc14, skc13))
%   -(skf1(V_2447_243072, skc13))
%   -(smoke(skc14, skc13))
%   -(skc14(skc13))
%   -(forename(skc9, skc13))
%   -(tpos(skc15, skc13))
%   -(tpos(skc10, skc13))
%   -(nonexistent(skc14, skc13))
%   -(general(skc14, skc13))
%   +(singleton(skc14, skc13))
%   -(tpos(skc13, skc15))
%   -(tpos(skc11, skc15))
%   -(tpos(skc17, skc15))
%   -(organism(skc14, skc15))
%   -(human_person(skc9, skc15))
%   -(relation(skc14, skc15))
%   -(proposition(skc9, skc15))
%   -(relname(skc9, skc15))
%   -(male(skc14, skc16))
%   -(man(skc9, skc16))
%   -(specific(skc14, skc16))
%   -(entity(skc9, skc16))
%   -(eventuality(skc9, skc16))
%   -(human(skc14, skc16))
%   -(human_person(skc9, skc16))
%   +(singleton(skc14, skc16))
%   -(proposition(skc14, skc17))
%   -(relname(skc14, skc17))
%   -(skf1(V_2447_243261, skc17))
%   -(smoke(skc14, skc17))
%   -(skc14(skc17))
%   -(forename(skc9, skc17))
%   -(tpos(skc15, skc17))
%   -(tpos(skc10, skc17))
%   -(nonexistent(skc14, skc17))
%   -(general(skc14, skc17))
%   +(singleton(skc14, skc17))
%   -(male(skc14, skc14))
%   -(man(skc9, skc14))
%   -(specific(skc14, skc14))
%   -(entity(skc9, skc14))
%   -(eventuality(skc9, skc14))
%   -(human(skc14, skc14))
%   -(human_person(skc9, skc14))
%   +(singleton(skc14, skc14))
%   -(male(skc14, skf1(V_2447_243382)))
%   -(existent(skc14, skf1(V_2447_243392)))
%   -(general(skc14, skf1(V_2447_243402)))
%   +(singleton(skc14, skf1(V_2447_243412)))
%   -(man(skc14, skc10))
%   -(skc11(skc10))
%   -(skc13(skc10))
%   -(skc17(skc10))
%   -(entity(skc14, skc10))
%   -(organism(skc9, skc10))
%   -(abstraction(skc14, skc10))
%   -(relation(skc9, skc10))
%   -(relation(skc14, skc11))
%   -(event(skc14, skc11))
%   -(state(skc14, skc11))
%   -(proposition(skc9, skc11))
%   -(relname(skc9, skc11))
%   -(skc15(skc11))
%   -(smoke(skc9, skc11))
%   -(skc10(skc11))
%   +(existent(skc14, skc11))
%   -(nonexistent(skc9, skc11))
%   +(specific(skc14, skc11))
%   -(general(skc9, skc11))
%   +(thing(skc14, skc11))
%   +(singleton(skc9, skc11))
%   +(unisex(skc14, skc12))
%   -(male(skc9, skc12))
%   +(general(skc14, skc12))
%   -(specific(skc9, skc12))
%   +(nonhuman(skc14, skc12))
%   -(human(skc9, skc12))
%   +(thing(skc14, skc12))
%   +(singleton(skc9, skc12))
%   -(relation(skc14, skc13))
%   -(event(skc14, skc13))
%   -(state(skc14, skc13))
%   -(proposition(skc9, skc13))
%   -(relname(skc9, skc13))
%   -(skc15(skc13))
%   -(smoke(skc9, skc13))
%   -(skc10(skc13))
%   +(existent(skc14, skc13))
%   -(nonexistent(skc9, skc13))
%   +(specific(skc14, skc13))
%   -(general(skc9, skc13))
%   +(thing(skc14, skc13))
%   +(singleton(skc9, skc13))
%   -(man(skc14, skc15))
%   -(skc11(skc15))
%   -(skc13(skc15))
%   -(skc17(skc15))
%   -(entity(skc14, skc15))
%   -(organism(skc9, skc15))
%   -(abstraction(skc14, skc15))
%   -(relation(skc9, skc15))
%   +(unisex(skc14, skc16))
%   -(male(skc9, skc16))
%   +(general(skc14, skc16))
%   -(specific(skc9, skc16))
%   +(nonhuman(skc14, skc16))
%   -(human(skc9, skc16))
%   +(thing(skc14, skc16))
%   +(singleton(skc9, skc16))
%   -(relation(skc14, skc17))
%   -(event(skc14, skc17))
%   -(state(skc14, skc17))
%   -(proposition(skc9, skc17))
%   -(relname(skc9, skc17))
%   -(skc15(skc17))
%   -(smoke(skc9, skc17))
%   -(skc10(skc17))
%   +(existent(skc14, skc17))
%   -(nonexistent(skc9, skc17))
%   +(specific(skc14, skc17))
%   -(general(skc9, skc17))
%   +(thing(skc14, skc17))
%   +(singleton(skc9, skc17))
%   +(unisex(skc14, skc14))
%   -(male(skc9, skc14))
%   +(general(skc14, skc14))
%   -(specific(skc9, skc14))
%   +(nonhuman(skc14, skc14))
%   -(human(skc9, skc14))
%   +(thing(skc14, skc14))
%   +(singleton(skc9, skc14))
%   +(unisex(skc14, skf1(V_2447_243984)))
%   +(nonexistent(skc14, skf1(V_2447_243994)))
%   +(specific(skc14, skf1(V_2447_244004)))
%   +(thing(skc14, skf1(V_2447_244014)))
%   +(be(skc14, skc10, skc11, skc11))
%   +(tpos(skc11, skc11))
%   +(be(skc14, skc10, skc11, skc13))
%   +(of(skc14, skc12, skc11))
%   +(be(skc14, skc10, skc13, skc13))
%   +(tpos(skc13, skc13))
%   -(male(skc14, skc10))
%   -(man(skc9, skc10))
%   -(existent(skc14, skc10))
%   -(entity(skc9, skc10))
%   -(general(skc14, skc10))
%   -(abstraction(skc9, skc10))
%   +(singleton(skc14, skc10))
%   -(abstraction(skc14, skc11))
%   -(eventuality(skc14, skc11))
%   -(relation(skc9, skc11))
%   -(event(skc9, skc11))
%   -(state(skc9, skc11))
%   -(nonhuman(skc14, skc11))
%   +(living(skc14, skc11))
%   +(impartial(skc14, skc11))
%   +(entity(skc14, skc11))
%   +(existent(skc9, skc11))
%   +(specific(skc9, skc11))
%   +(thing(skc9, skc11))
%   +(abstraction(skc14, skc12))
%   +(unisex(skc9, skc12))
%   +(general(skc9, skc12))
%   +(nonhuman(skc9, skc12))
%   +(thing(skc9, skc12))
%   -(abstraction(skc14, skc13))
%   -(eventuality(skc14, skc13))
%   -(relation(skc9, skc13))
%   -(event(skc9, skc13))
%   -(state(skc9, skc13))
%   -(nonhuman(skc14, skc13))
%   +(living(skc14, skc13))
%   +(impartial(skc14, skc13))
%   +(tpos(skc12, skc12))
%   +(entity(skc14, skc13))
%   +(existent(skc9, skc13))
%   +(specific(skc9, skc13))
%   +(thing(skc9, skc13))
%   -(male(skc14, skc15))
%   -(man(skc9, skc15))
%   -(existent(skc14, skc15))
%   -(entity(skc9, skc15))
%   -(general(skc14, skc15))
%   -(abstraction(skc9, skc15))
%   +(singleton(skc14, skc15))
%   +(abstraction(skc14, skc16))
%   +(unisex(skc9, skc16))
%   +(general(skc9, skc16))
%   +(nonhuman(skc9, skc16))
%   +(thing(skc9, skc16))
%   -(abstraction(skc14, skc17))
%   -(eventuality(skc14, skc17))
%   -(relation(skc9, skc17))
%   -(event(skc9, skc17))
%   -(state(skc9, skc17))
%   -(nonhuman(skc14, skc17))
%   +(living(skc14, skc17))
%   +(impartial(skc14, skc17))
%   +(tpos(skc16, skc16))
%   +(entity(skc14, skc17))
%   +(existent(skc9, skc17))
%   +(specific(skc9, skc17))
%   +(thing(skc9, skc17))
%   +(abstraction(skc14, skc14))
%   +(unisex(skc9, skc14))
%   +(general(skc9, skc14))
%   +(nonhuman(skc9, skc14))
%   +(thing(skc9, skc14))
%   +(eventuality(skc14, skf1(V_2447_244542)))
%   +(be(skc9, skc10, skc11, skc11))
%   +(be(skc9, skc10, skc11, skc13))
%   +(of(skc9, skc12, skc11))
%   +(be(skc9, skc10, skc13, skc13))
%   +(unisex(skc14, skc10))
%   -(male(skc9, skc10))
%   +(nonexistent(skc14, skc10))
%   -(existent(skc9, skc10))
%   +(specific(skc14, skc10))
%   -(general(skc9, skc10))
%   +(thing(skc14, skc10))
%   +(singleton(skc9, skc10))
%   -(unisex(skc14, skc11))
%   -(abstraction(skc9, skc11))
%   -(eventuality(skc9, skc11))
%   +(animate(skc14, skc11))
%   +(human(skc14, skc11))
%   -(nonhuman(skc9, skc11))
%   +(organism(skc14, skc11))
%   +(living(skc9, skc11))
%   +(impartial(skc9, skc11))
%   +(entity(skc9, skc11))
%   +(relation(skc14, skc12))
%   +(abstraction(skc9, skc12))
%   -(unisex(skc14, skc13))
%   -(abstraction(skc9, skc13))
%   -(eventuality(skc9, skc13))
%   +(animate(skc14, skc13))
%   +(human(skc14, skc13))
%   -(nonhuman(skc9, skc13))
%   +(organism(skc14, skc13))
%   +(living(skc9, skc13))
%   +(impartial(skc9, skc13))
%   +(entity(skc9, skc13))
%   +(unisex(skc14, skc15))
%   -(male(skc9, skc15))
%   +(nonexistent(skc14, skc15))
%   -(existent(skc9, skc15))
%   +(specific(skc14, skc15))
%   -(general(skc9, skc15))
%   +(thing(skc14, skc15))
%   +(singleton(skc9, skc15))
%   +(relation(skc14, skc16))
%   +(abstraction(skc9, skc16))
%   -(unisex(skc14, skc17))
%   -(abstraction(skc9, skc17))
%   -(eventuality(skc9, skc17))
%   +(animate(skc14, skc17))
%   +(human(skc14, skc17))
%   -(nonhuman(skc9, skc17))
%   +(organism(skc14, skc17))
%   +(living(skc9, skc17))
%   +(impartial(skc9, skc17))
%   +(entity(skc9, skc17))
%   +(relation(skc14, skc14))
%   +(abstraction(skc9, skc14))
%   +(agent(skc14, skf1(skc17), skc17))
%   +(agent(skc14, skf1(skc13), skc13))
%   +(agent(skc14, skf1(skc11), skc11))
%   +(event(skc14, skf1(V_2447_244981)))
%   +(present(skc14, skf1(V_2447_244991)))
%   +(smoke(skc14, skf1(V_2447_245001)))
%   +(skc13(skc11))
%   +(skc11(skc13))
%   +(event(skc14, skc10))
%   +(eventuality(skc14, skc10))
%   +(unisex(skc9, skc10))
%   +(nonexistent(skc9, skc10))
%   +(specific(skc9, skc10))
%   +(thing(skc9, skc10))
%   +(male(skc14, skc11))
%   -(unisex(skc9, skc11))
%   +(human_person(skc14, skc11))
%   +(animate(skc9, skc11))
%   +(human(skc9, skc11))
%   +(organism(skc9, skc11))
%   +(relname(skc14, skc12))
%   +(relation(skc9, skc12))
%   +(male(skc14, skc13))
%   -(unisex(skc9, skc13))
%   +(human_person(skc14, skc13))
%   +(animate(skc9, skc13))
%   +(human(skc9, skc13))
%   +(organism(skc9, skc13))
%   +(eventuality(skc14, skc15))
%   +(unisex(skc9, skc15))
%   +(nonexistent(skc9, skc15))
%   +(specific(skc9, skc15))
%   +(thing(skc9, skc15))
%   +(relname(skc14, skc16))
%   +(relation(skc9, skc16))
%   +(male(skc14, skc17))
%   -(unisex(skc9, skc17))
%   +(human_person(skc14, skc17))
%   +(animate(skc9, skc17))
%   +(human(skc9, skc17))
%   +(organism(skc9, skc17))
%   +(tpos(skc14, skc14))
%   +(theme(skc14, skc15, skc14))
%   +(proposition(skc14, skc14))
%   +(relation(skc9, skc14))
%   +(be(skc14, skc10, skc13, skc11))
%   +(agent(skc14, skc15, skc17))
%   +(of(skc14, skc16, skc17))
%   +(of(skc14, skc12, skc13))
%   +(vincent_forename(skc14, skc16))
%   +(think_believe_consider(skc14, skc15))
%   +(present(skc14, skc15))
%   +(jules_forename(skc14, skc12))
%   +(forename(skc14, skc16))
%   +(forename(skc14, skc12))
%   +(man(skc14, skc17))
%   +(man(skc14, skc13))
%   +(man(skc14, skc11))
%   +(event(skc14, skc15))
%   +(state(skc14, skc10))
%   +(tpos(skc13, skc11))
%   +(tpos(skc11, skc13))
%   +(event(skc9, skc10))
%   +(eventuality(skc9, skc10))
%   +(male(skc9, skc11))
%   +(human_person(skc9, skc11))
%   +(relname(skc9, skc12))
%   +(male(skc9, skc13))
%   +(human_person(skc9, skc13))
%   +(eventuality(skc9, skc15))
%   +(relname(skc9, skc16))
%   +(male(skc9, skc17))
%   +(human_person(skc9, skc17))
%   +(theme(skc9, skc15, skc14))
%   +(proposition(skc9, skc14))
%   +(accessible_world(skc9, skc14))
%   +(be(skc9, skc10, skc13, skc11))
%   +(state(skc9, skc10))
%   +(man(skc9, skc11))
%   +(of(skc9, skc12, skc13))
%   +(jules_forename(skc9, skc12))
%   +(forename(skc9, skc12))
%   +(man(skc9, skc13))
%   +(agent(skc9, skc15, skc17))
%   +(think_believe_consider(skc9, skc15))
%   +(present(skc9, skc15))
%   +(event(skc9, skc15))
%   +(of(skc9, skc16, skc17))
%   +(vincent_forename(skc9, skc16))
%   +(forename(skc9, skc16))
%   +(man(skc9, skc17))
%   +(actual_world(skc9))
%   +(skc14(skc14))
%   +(skc10(skc10))
%   +(skc11(skc11))
%   +(skc12(skc12))
%   +(skc13(skc13))
%   +(skc15(skc15))
%   +(skc16(skc16))
%   +(skc17(skc17))
%   +(skc9(skc9))
%   +(skf1(_2418_245674, skf1(_2418_245674)))
%   +(_245680)
% 
%------------------------------------------------------------------------------