FDP---0.9.16.SAT-Ass.s

%------------------------------------------------------------------------------
% File     : FDP---0.9.16
% Problem  : NLP162-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 22:27:24 EST 2011

% Result   : Satisfiable 152.89s
% Output   : Assurance 152.89s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% FDPLL - A First-Order Davis-Putnam Theorem Prover
% Version 0.9.16 (26/06/2002)
% Proving /tmp/NLP162-1+noeq ...
% Done.
% Input File...............: /tmp/NLP162-1+noeq.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.: 210 seconds
% Restart with =-axioms....: off
% Initial interpretation...: [+(_137892)]
% Clause set type..........: Non-Horn, without equality
% Equality transformation..: off
% Non-constant functions...: yes
% Term depth settings......: 3/2 (Init/Increment)
% unit_extend..............: on
% splitting type...........: exact
% Final tree statistics:
% Tree for clause set......: as initially given
% # Restarts...............: 0
% Term depth limit.........: 5
% # Splits.................: 70
% # Commits................: 0
% # Unit extension steps...: 149
% # Unit back subsumptions.: 0
% # Branches closed........: 0
% # Level cuts.............: 0
% Time.....................: 152.62 seconds.
% Result...................: SATISFIABLE with model:
%   +(actual_world(skc18))
%   +(actual_world(skc62))
%   +(_137970)
%   +(ssSkP2(skc64, skc63, skc62))
%   +(down(skc62, skc66, skc67))
%   +(ssSkP1(skc67, skc65, skc62))
%   +(in(skc62, skc66, skc69))
%   +(of(skc62, skc68, skc69))
%   +(agent(skc62, skc66, skc70))
%   +(group(skc62, skc64))
%   +(group(skc62, skc63))
%   +(frontseat(skc62, skc67))
%   +(street(skc62, skc67))
%   +(lonely(skc62, skc67))
%   +(city(skc62, skc69))
%   +(hollywood_placename(skc62, skc68))
%   +(placename(skc62, skc68))
%   +(barrel(skc62, skc66))
%   +(present(skc62, skc66))
%   +(event(skc62, skc66))
%   +(old(skc62, skc70))
%   +(dirty(skc62, skc70))
%   +(white(skc62, skc70))
%   +(chevy(skc62, skc70))
%   +(two(skc62, skc65))
%   +(group(skc62, skc65))
%   +(ssSkP0(skc65, skc62))
%   -(ssSkC0)
%   +(be(skc62, skf13(skc62, Y_138196, skf19(skc65, skc62, skc65)), skf19(skc65, skc62, skc65), skf12(skf19(skc65, skc62, skc65), skc62, Y_138196)))
%   +(in(skc62, skf12(skf19(skc65, skc62, skc65), skc62, skc67), skc67))
%   +(be(skc62, skf13(skc62, Y_138242, skf21(skc65, skc62, X_138247)), skf21(skc65, skc62, X_138247), skf12(skf21(skc65, skc62, X_138247), skc62, Y_138242)))
%   +(in(skc62, skf12(skf21(skc65, skc62, X_138276), skc62, skc67), skc67))
%   +(young(skc62, skf19(skc65, skc62, skc65)))
%   +(fellow(skc62, skf19(skc65, skc62, skc65)))
%   +(state(skc62, skf13(skc62, Y_138310, Z_138311)))
%   +(young(skc62, skf21(skc65, skc62, X_138323)))
%   +(fellow(skc62, skf21(skc65, skc62, X_138335)))
%   +(member(skc62, skf19(skc65, skc62, skc65), skc65))
%   +(member(skc62, skf21(skc65, skc62, X_138360), skc65))
%   -(ssSkP2(skc65, skc65, skc62))
%   -(in(skc62, skf12(skf16(skc70, skc62, skc65), skc62, Y_138402), skc70))
%   +(be(skc62, skf13(skc62, Y_138416, skf16(skc70, skc62, skc65)), skf16(skc70, skc62, skc65), skf12(skf16(skc70, skc62, skc65), skc62, Y_138416)))
%   +(in(skc62, skf12(skf16(skc70, skc62, skc65), skc62, skc67), skc67))
%   +(young(skc62, skf16(skc70, skc62, skc65)))
%   +(fellow(skc62, skf16(skc70, skc62, skc65)))
%   +(member(skc62, skf16(skc70, skc62, skc65), skc65))
%   -(ssSkP1(skc70, skc65, skc62))
%   -(frontseat(skc62, skc70))
%   -(nonreflexive(skc62, skc66))
%   -(agent(skc62, skc66, skc67))
%   -(old(skc62, skc67))
%   +(cheap(skc62, skf19(skc63, skc62, skc63)))
%   +(black(skc62, skf19(skc63, skc62, skc63)))
%   +(coat(skc62, skf19(skc63, skc62, skc63)))
%   +(cheap(skc62, skf21(skc63, skc62, X_138649)))
%   +(black(skc62, skf21(skc63, skc62, X_138661)))
%   +(coat(skc62, skf21(skc63, skc62, X_138673)))
%   +(member(skc62, skf19(skc63, skc62, skc63), skc63))
%   +(member(skc62, skf21(skc63, skc62, X_138698), skc63))
%   -(ssSkP2(skc63, skc63, skc62))
%   +(cheap(skc62, skf19(skc65, skc62, skc63)))
%   +(black(skc62, skf19(skc65, skc62, skc63)))
%   +(coat(skc62, skf19(skc65, skc62, skc63)))
%   +(member(skc62, skf19(skc65, skc62, skc63), skc63))
%   -(ssSkP2(skc65, skc63, skc62))
%   -(two(skc62, skc63))
%   +(be(skc62, skf13(skc62, Y_138831, skf19(skc63, skc62, skc65)), skf19(skc63, skc62, skc65), skf12(skf19(skc63, skc62, skc65), skc62, Y_138831)))
%   +(in(skc62, skf12(skf19(skc63, skc62, skc65), skc62, skc67), skc67))
%   +(young(skc62, skf19(skc63, skc62, skc65)))
%   +(fellow(skc62, skf19(skc63, skc62, skc65)))
%   +(member(skc62, skf19(skc63, skc62, skc65), skc65))
%   -(ssSkP2(skc63, skc65, skc62))
%   -(member(skc62, skf19(skc64, skc62, X_138935), skc63))
%   -(agent(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_139000), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_139025), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   -(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_139050), Z_139051), skf19(skc64, skc62, X_139050)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf21(skc63, skc62, X_139076)), skf21(skc63, skc62, X_139076)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf19(skc64, skc62, skc64), Z_139145), skf19(skc64, skc62, skc64)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_139166), skf21(skc63, skc62, X_139171)), skf21(skc63, skc62, X_139171)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_139192), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_139217), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_139242), Z_139243), skf21(skc64, skc62, X_139242)))
%   +(event(skc62, skf17(skc62, Z_139259, X1_139260)))
%   +(present(skc62, skf17(skc62, Z_139272, X1_139273)))
%   +(nonreflexive(skc62, skf17(skc62, Z_139285, X1_139286)))
%   +(wear(skc62, skf17(skc62, Z_139298, X1_139299)))
%   +(member(skc62, skf19(skc64, skc62, skc64), skc64))
%   +(member(skc62, skf21(skc64, skc62, X_139324), skc64))
%   -(ssSkP2(skc64, skc64, skc62))
%   -(agent(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf21(skc63, skc62, X_139418)), skf21(skc63, skc62, X_139418)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf19(skc63, skc62, skc64), Z_139487), skf19(skc63, skc62, skc64)))
%   +(member(skc62, skf19(skc63, skc62, skc64), skc64))
%   -(ssSkP2(skc63, skc64, skc62))
%   -(agent(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf21(skc63, skc62, X_139597)), skf21(skc63, skc62, X_139597)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf19(skc65, skc62, skc64), Z_139666), skf19(skc65, skc62, skc64)))
%   +(member(skc62, skf19(skc65, skc62, skc64), skc64))
%   -(ssSkP2(skc65, skc64, skc62))
%   -(two(skc62, skc64))
%   +(be(skc62, skf13(skc62, Y_139745, skf19(skc64, skc62, skc65)), skf19(skc64, skc62, skc65), skf12(skf19(skc64, skc62, skc65), skc62, Y_139745)))
%   +(in(skc62, skf12(skf19(skc64, skc62, skc65), skc62, skc67), skc67))
%   +(young(skc62, skf19(skc64, skc62, skc65)))
%   +(fellow(skc62, skf19(skc64, skc62, skc65)))
%   +(member(skc62, skf19(skc64, skc62, skc65), skc65))
%   -(ssSkP2(skc64, skc65, skc62))
%   -(in(skc62, V_139845, skc70))
%   -(ssSkP1(skc70, W_139871, skc62))
%   -(agent(skc62, skf17(skc62, Z_139901, X1_139902), skf21(skc65, skc62, X_139907)))
%   -(event(skc62, V_139932))
%   -(agent(skc62, skf17(skc62, Z_139962, X1_139963), skf21(skc63, skc62, X_139968)))
%   -(agent(skc62, skf17(skc62, Z_139998, X1_139999), skf21(skc64, skc62, X_140004)))
%   -(group(skc62, X4_140029))
%   -(ssSkP1(W_140055, skc65, skc62))
%   -(in(skc62, V_140081, W_140082))
%   -(member(skc62, V_140108, skc65))
%   +(member(skc62, skf16(U_140138, skc62, skc65), skc65))
%   -(ssSkP1(X_140164, W_140165, skc62))
%   +(in(skc62, skf12(skf19(skc64, skc62, skc65), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf19(skc63, skc62, skc65), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf16(skc70, skc62, skc65), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf19(skc65, skc62, skc65), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf21(skc65, skc62, X_140263), skc62, skc69), skc69))
%   +(ssSkP1(skc69, skc65, skc62))
%   -(agent(skc62, skc66, skc69))
%   +(ssSkP1(skc69, Z_140322, skc62))
%   -(member(skc62, V_140348, W_140349))
%   +(member(skc62, skf16(skc70, skc62, V_140379), V_140379))
%   +(member(skc62, skf16(U_140409, skc62, V_140410), V_140410))
%   -(group(skc18, X4_140435))
%   -(actual_world(V_140459))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_140493), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(cheap(skc62, skf16(skc69, skc62, skc63)))
%   +(black(skc62, skf16(skc69, skc62, skc63)))
%   +(coat(skc62, skf16(skc69, skc62, skc63)))
%   -(be(skc62, skf13(skc62, Y_140620, Z_140621), skf16(skc69, skc62, Y_140626), skc66))
%   -(be(skc62, skf13(skc62, Y_140640, Z_140641), skf16(skc69, skc62, Y_140646), skf12(skf21(skc65, skc62, X_140655), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_140669, Z_140670), skf16(skc69, skc62, Y_140675), skf12(skf19(skc65, skc62, skc65), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_140697, Z_140698), skf16(skc69, skc62, Y_140703), skf12(skf16(skc70, skc62, skc65), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_140725, Z_140726), skf16(skc69, skc62, Y_140731), skf12(skf19(skc63, skc62, skc65), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_140753, Z_140754), skf16(skc69, skc62, Y_140759), skf12(skf19(skc64, skc62, skc65), skc62, skc69)))
%   +(member(skc62, skf16(skc69, skc62, skc63), skc63))
%   -(ssSkP1(skc69, skc63, skc62))
%   -(agent(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf21(skc63, skc62, X_140873)), skf21(skc63, skc62, X_140873)))
%   +(patient(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf16(skc69, skc62, skc64), Z_140966), skf16(skc69, skc62, skc64)))
%   +(member(skc62, skf16(skc69, skc62, skc64), skc64))
%   -(ssSkP1(skc69, skc64, skc62))
%   +(in(skc62, skf12(skf16(U_141024, skc62, skc65), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf16(U_141058, skc62, skc65), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf16(skc70, skc62, W_141092), skc62, skc69), skc69))
%   +(in(skc62, skf12(skf16(U_141126, skc62, W_141127), skc62, skc69), skc69))
%   -(ssSkP2(skc65, Y_141153, skc62))
%   +(member(skc62, skf19(skc65, skc62, V_141183), V_141183))
%   +(in(skc62, skf12(skf19(skc65, skc62, W_141217), skc62, skc69), skc69))
%   -(ssSkP2(skc63, Y_141243, skc62))
%   +(member(skc62, skf19(skc63, skc62, V_141273), V_141273))
%   +(in(skc62, skf12(skf19(skc63, skc62, W_141307), skc62, skc69), skc69))
%   -(state(skc62, X_141332))
%   -(be(skc62, skf13(skc62, Y_141363, Z_141364), skf16(skc69, skc62, Y_141369), skf12(skf16(U_141378, skc62, skc65), skc62, skc69)))
%   -(member(skc62, skf16(skc69, skc62, skc65), skc65))
%   -(be(skc62, skf13(skc62, Y_141438, Z_141439), skf16(skc69, skc62, Y_141444), skf12(skf16(skc70, skc62, W_141453), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_141484, Z_141485), skf16(skc69, skc62, Y_141490), skf12(skf16(U_141499, skc62, W_141500), skc62, skc69)))
%   -(member(skc62, skf16(skc69, skc62, W_141530), W_141530))
%   -(be(skc62, skf13(skc62, Y_141561, Z_141562), skf16(skc69, skc62, Y_141567), skf12(skf19(skc65, skc62, W_141576), skc62, skc69)))
%   -(be(skc62, skf13(skc62, Y_141607, Z_141608), skf16(skc69, skc62, Y_141613), skf12(skf19(skc63, skc62, W_141622), skc62, skc69)))
%   +(ssSkP1(skc67, Z_141648, skc62))
%   -(agent(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf21(skc63, skc62, X_141734)), skf21(skc63, skc62, X_141734)))
%   +(patient(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf16(skc69, skc62, skc63)), skf16(skc69, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf16(skc67, skc62, skc64), Z_141827), skf16(skc67, skc62, skc64)))
%   -(be(skc62, skf13(skc62, Y_141845, Z_141846), skf16(skc67, skc62, Y_141851), skf12(skf21(skc65, skc62, X_141860), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_141874, Z_141875), skf16(skc67, skc62, Y_141880), skf12(skf19(skc65, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_141902, Z_141903), skf16(skc67, skc62, Y_141908), skf12(skf16(skc70, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_141930, Z_141931), skf16(skc67, skc62, Y_141936), skf12(skf19(skc63, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_141958, Z_141959), skf16(skc67, skc62, Y_141964), skf12(skf19(skc64, skc62, skc65), skc62, skc67)))
%   +(member(skc62, skf16(skc67, skc62, skc64), skc64))
%   -(ssSkP1(skc67, skc64, skc62))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_142026), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc69, skc62, skc64), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc67, skc62, skc64), skf16(skc67, skc62, skc63)), skf16(skc67, skc62, skc63)))
%   +(cheap(skc62, skf16(skc67, skc62, skc63)))
%   +(black(skc62, skf16(skc67, skc62, skc63)))
%   +(coat(skc62, skf16(skc67, skc62, skc63)))
%   +(member(skc62, skf16(skc67, skc62, skc63), skc63))
%   -(ssSkP1(skc67, skc63, skc62))
%   +(in(skc62, skf12(skf16(skc70, skc62, W_142241), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf16(U_142275, skc62, W_142276), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf19(skc65, skc62, W_142310), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf19(skc63, skc62, W_142344), skc62, skc67), skc67))
%   -(be(skc62, skf13(skc62, Y_142375, Z_142376), skf16(skc67, skc62, Y_142381), skf12(skf16(U_142390, skc62, skc65), skc62, skc67)))
%   -(member(skc62, skf16(skc67, skc62, skc65), skc65))
%   -(be(skc62, skf13(skc62, Y_142450, Z_142451), skf16(skc67, skc62, Y_142456), skf12(skf16(skc70, skc62, W_142465), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_142496, Z_142497), skf16(skc67, skc62, Y_142502), skf12(skf16(U_142511, skc62, W_142512), skc62, skc67)))
%   -(member(skc62, skf16(skc67, skc62, W_142542), W_142542))
%   -(be(skc62, skf13(skc62, Y_142573, Z_142574), skf16(skc67, skc62, Y_142579), skf12(skf19(skc65, skc62, W_142588), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_142619, Z_142620), skf16(skc67, skc62, Y_142625), skf12(skf19(skc63, skc62, W_142634), skc62, skc67)))
% 
%------------------------------------------------------------------------------