↑ Up

FDP---0.9.16.SAT-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : FDP---0.9.16
% Problem  : NLP160-1 : TPTP v5.0.0. Released v2.4.0.
% Transfm  : add_equality
% Format   : protein
% Command  : fdp-casc %s %d

% Computer : art01.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:01 EST 2011

% Result   : Satisfiable 107.27s
% Output   : Assurance 107.27s
% 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/NLP160-1+noeq ...
% Done.
% Input File...............: /tmp/NLP160-1+noeq.tme
% System...................: Linux art01.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...: [+(_115430)]
% 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.................: 66
% # Commits................: 1
% # Unit extension steps...: 122
% # Unit back subsumptions.: 0
% # Branches closed........: 0
% # Level cuts.............: 0
% Time.....................: 106.98 seconds.
% Result...................: SATISFIABLE with model:
%   +(actual_world(skc18))
%   +(actual_world(skc62))
%   +(_115508)
%   +(ssSkP2(skc64, skc63, skc62))
%   +(down(skc62, skc66, skc67))
%   +(in(skc62, skc66, skc69))
%   +(of(skc62, skc68, skc69))
%   +(ssSkP1(skc70, skc65, skc62))
%   +(agent(skc62, skc66, skc70))
%   +(group(skc62, skc64))
%   +(group(skc62, skc63))
%   +(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))
%   +(frontseat(skc62, skc70))
%   +(two(skc62, skc65))
%   +(group(skc62, skc65))
%   +(ssSkP0(skc65, skc62))
%   -(ssSkC0)
%   +(be(skc62, skf13(skc62, Y_115734, skf19(skc65, skc62, skc65)), skf19(skc65, skc62, skc65), skf12(skf19(skc65, skc62, skc65), skc62, Y_115734)))
%   +(in(skc62, skf12(skf19(skc65, skc62, skc65), skc62, skc70), skc70))
%   +(be(skc62, skf13(skc62, Y_115780, skf21(skc65, skc62, X_115785)), skf21(skc65, skc62, X_115785), skf12(skf21(skc65, skc62, X_115785), skc62, Y_115780)))
%   +(in(skc62, skf12(skf21(skc65, skc62, X_115814), skc62, skc70), skc70))
%   +(young(skc62, skf19(skc65, skc62, skc65)))
%   +(fellow(skc62, skf19(skc65, skc62, skc65)))
%   +(state(skc62, skf13(skc62, Y_115848, Z_115849)))
%   +(young(skc62, skf21(skc65, skc62, X_115861)))
%   +(fellow(skc62, skf21(skc65, skc62, X_115873)))
%   +(member(skc62, skf19(skc65, skc62, skc65), skc65))
%   +(member(skc62, skf21(skc65, skc62, X_115898), skc65))
%   -(ssSkP2(skc65, skc65, skc62))
%   -(city(skc62, skc70))
%   -(nonreflexive(skc62, skc66))
%   -(in(skc62, skf12(skf16(skc69, skc62, skc65), skc62, Y_115988), skc69))
%   +(be(skc62, skf13(skc62, Y_116002, skf16(skc69, skc62, skc65)), skf16(skc69, skc62, skc65), skf12(skf16(skc69, skc62, skc65), skc62, Y_116002)))
%   +(in(skc62, skf12(skf16(skc69, skc62, skc65), skc62, skc70), skc70))
%   +(young(skc62, skf16(skc69, skc62, skc65)))
%   +(fellow(skc62, skf16(skc69, skc62, skc65)))
%   -(be(skc62, skf13(skc62, Y_116070, Z_116071), skf16(skc69, skc62, Y_116076), skc66))
%   +(member(skc62, skf16(skc69, skc62, skc65), skc65))
%   -(ssSkP1(skc69, skc65, skc62))
%   -(frontseat(skc62, skc69))
%   +(cheap(skc62, skf19(skc63, skc62, skc63)))
%   +(black(skc62, skf19(skc63, skc62, skc63)))
%   +(coat(skc62, skf19(skc63, skc62, skc63)))
%   +(cheap(skc62, skf21(skc63, skc62, X_116182)))
%   +(black(skc62, skf21(skc63, skc62, X_116194)))
%   +(coat(skc62, skf21(skc63, skc62, X_116206)))
%   +(member(skc62, skf19(skc63, skc62, skc63), skc63))
%   +(member(skc62, skf21(skc63, skc62, X_116231), 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_116364, skf19(skc63, skc62, skc65)), skf19(skc63, skc62, skc65), skf12(skf19(skc63, skc62, skc65), skc62, Y_116364)))
%   +(in(skc62, skf12(skf19(skc63, skc62, skc65), skc62, skc70), skc70))
%   +(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, skc63), skc63))
%   -(member(skc62, skf19(skc64, skc62, X_116480), 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_116545), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_116570), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   -(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116595), Z_116596), skf19(skc64, skc62, X_116595)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf21(skc63, skc62, X_116621)), skf21(skc63, skc62, X_116621)))
%   +(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_116690), skf19(skc64, skc62, skc64)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116711), skf21(skc63, skc62, X_116716)), skf21(skc63, skc62, X_116716)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116737), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116762), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_116787), Z_116788), skf21(skc64, skc62, X_116787)))
%   +(event(skc62, skf17(skc62, Z_116804, X1_116805)))
%   +(present(skc62, skf17(skc62, Z_116817, X1_116818)))
%   +(nonreflexive(skc62, skf17(skc62, Z_116830, X1_116831)))
%   +(wear(skc62, skf17(skc62, Z_116843, X1_116844)))
%   +(member(skc62, skf19(skc64, skc62, skc64), skc64))
%   +(member(skc62, skf21(skc64, skc62, X_116869), 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_116963)), skf21(skc63, skc62, X_116963)))
%   +(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_117032), 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_117142)), skf21(skc63, skc62, X_117142)))
%   +(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_117211), skf19(skc65, skc62, skc64)))
%   +(member(skc62, skf19(skc65, skc62, skc64), skc64))
%   -(ssSkP2(skc65, skc64, skc62))
%   -(two(skc62, skc64))
%   +(be(skc62, skf13(skc62, Y_117290, skf19(skc64, skc62, skc65)), skf19(skc64, skc62, skc65), skf12(skf19(skc64, skc62, skc65), skc62, Y_117290)))
%   +(in(skc62, skf12(skf19(skc64, skc62, skc65), skc62, skc70), skc70))
%   +(young(skc62, skf19(skc64, skc62, skc65)))
%   +(fellow(skc62, skf19(skc64, skc62, skc65)))
%   +(member(skc62, skf19(skc64, skc62, skc65), skc65))
%   -(ssSkP2(skc64, skc65, skc62))
%   -(state(skc62, X_117389))
%   -(in(skc62, V_117415, skc69))
%   -(ssSkP1(skc69, W_117441, skc62))
%   -(agent(skc62, skf17(skc62, Z_117471, X1_117472), skf21(skc65, skc62, X_117477)))
%   -(event(skc62, V_117502))
%   -(agent(skc62, skf17(skc62, Z_117532, X1_117533), skf21(skc63, skc62, X_117538)))
%   -(agent(skc62, skf17(skc62, Z_117568, X1_117569), skf21(skc64, skc62, X_117574)))
%   -(group(skc62, X4_117599))
%   -(ssSkP1(Z_117625, skc65, skc62))
%   -(in(skc62, V_117651, W_117652))
%   -(member(skc62, V_117678, skc65))
%   +(member(skc62, skf16(U_117708, skc62, skc65), skc65))
%   -(ssSkP1(X_117734, W_117735, skc62))
%   -(group(skc18, X4_117760))
%   -(actual_world(V_117784))
%   +(in(skc62, skf12(skf16(U_117818, skc62, skc65), skc62, skc70), skc70))
%   -(ssSkP2(skc65, Y_117844, skc62))
%   -(ssSkP2(W_117870, skc65, skc62))
%   +(member(skc62, skf19(U_117900, skc62, skc65), skc65))
%   +(in(skc62, skf12(skf19(U_117934, skc62, skc65), skc62, skc70), skc70))
%   -(ssSkP2(W_117960, skc64, skc62))
%   -(member(skc62, skf21(skc65, skc62, X_117990), skc64))
%   -(ssSkP2(W_118016, skc63, skc62))
%   -(ssSkP2(W_118042, Y_118043, skc62))
%   -(member(skc62, skf21(skc63, skc62, X_118073), skc64))
%   +(ssSkP1(skc70, Z_118099, skc62))
%   -(agent(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf21(skc63, skc62, X_118185)), skf21(skc63, skc62, X_118185)))
%   +(patient(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf16(skc70, skc62, skc64), Z_118254), skf16(skc70, skc62, skc64)))
%   -(be(skc62, skf13(skc62, Y_118272, Z_118273), skf16(skc70, skc62, Y_118278), skf12(skf21(skc65, skc62, X_118287), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_118301, Z_118302), skf16(skc70, skc62, Y_118307), skf12(skf19(skc65, skc62, skc65), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_118329, Z_118330), skf16(skc70, skc62, Y_118335), skf12(skf16(skc69, skc62, skc65), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_118357, Z_118358), skf16(skc70, skc62, Y_118363), skf12(skf19(skc63, skc62, skc65), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_118385, Z_118386), skf16(skc70, skc62, Y_118391), skf12(skf19(skc64, skc62, skc65), skc62, skc70)))
%   +(member(skc62, skf16(skc70, skc62, skc64), skc64))
%   -(ssSkP1(skc70, skc64, skc62))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_118453), skf16(skc70, skc62, skc63)), skf16(skc70, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf16(skc70, skc62, skc63)), skf16(skc70, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc63, skc62, skc64), skf16(skc70, skc62, skc63)), skf16(skc70, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf19(skc65, skc62, skc64), skf16(skc70, skc62, skc63)), skf16(skc70, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf16(skc70, skc62, skc64), skf16(skc70, skc62, skc63)), skf16(skc70, skc62, skc63)))
%   +(cheap(skc62, skf16(skc70, skc62, skc63)))
%   +(black(skc62, skf16(skc70, skc62, skc63)))
%   +(coat(skc62, skf16(skc70, skc62, skc63)))
%   +(member(skc62, skf16(skc70, skc62, skc63), skc63))
%   -(ssSkP1(skc70, skc63, skc62))
%   -(member(skc62, V_118636, W_118637))
%   +(member(skc62, skf16(skc69, skc62, V_118667), V_118667))
%   +(member(skc62, skf16(U_118697, skc62, V_118698), V_118698))
%   +(member(skc62, skf21(U_118728, skc62, X_118729), U_118728))
%   +(member(skc62, skf19(skc65, skc62, V_118759), V_118759))
%   +(member(skc62, skf19(U_118789, skc62, skc64), skc64))
%   +(member(skc62, skf19(U_118819, skc62, skc63), skc63))
%   +(member(skc62, skf19(U_118849, skc62, V_118850), V_118850))
%   +(in(skc62, skf12(skf16(skc69, skc62, W_118884), skc62, skc70), skc70))
%   +(in(skc62, skf12(skf16(U_118918, skc62, W_118919), skc62, skc70), skc70))
%   +(in(skc62, skf12(skf21(W_118953, skc62, X_118954), skc62, skc70), skc70))
%   +(in(skc62, skf12(skf19(skc65, skc62, W_118988), skc62, skc70), skc70))
%   +(in(skc62, skf12(skf19(U_119022, skc62, W_119023), skc62, skc70), skc70))
%   -(be(skc62, skf13(skc62, Y_119054, Z_119055), skf16(skc70, skc62, Y_119060), skf12(skf16(U_119069, skc62, skc65), skc62, skc70)))
%   -(member(skc62, skf16(skc70, skc62, skc65), skc65))
%   -(be(skc62, skf13(skc62, Y_119129, Z_119130), skf16(skc70, skc62, Y_119135), skf12(skf19(U_119144, skc62, skc65), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_119175, Z_119176), skf16(skc70, skc62, Y_119181), skf12(skf16(skc69, skc62, W_119190), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_119221, Z_119222), skf16(skc70, skc62, Y_119227), skf12(skf16(U_119236, skc62, W_119237), skc62, skc70)))
%   -(member(skc62, skf16(skc70, skc62, W_119267), W_119267))
%   -(be(skc62, skf13(skc62, Y_119298, Z_119299), skf16(skc70, skc62, Y_119304), skf12(skf21(W_119313, skc62, X_119314), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_119345, Z_119346), skf16(skc70, skc62, Y_119351), skf12(skf19(skc65, skc62, W_119360), skc62, skc70)))
%   -(be(skc62, skf13(skc62, Y_119391, Z_119392), skf16(skc70, skc62, Y_119397), skf12(skf19(U_119406, skc62, W_119407), skc62, skc70)))
%   -(agent(skc62, skf17(skc62, Z_119437, X1_119438), skf21(W_119443, skc62, X_119444)))
% 
%------------------------------------------------------------------------------