↑ Up

FDP---0.9.16.SAT-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : FDP---0.9.16
% Problem  : NLP161-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:27:07 EST 2011

% Result   : Satisfiable 83.46s
% Output   : Assurance 83.46s
% 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/NLP161-1+noeq ...
% Done.
% Input File...............: /tmp/NLP161-1+noeq.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.: 210 seconds
% Restart with =-axioms....: off
% Initial interpretation...: [+(_115243)]
% 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.....................: 83.2 seconds.
% Result...................: SATISFIABLE with model:
%   +(actual_world(skc18))
%   +(actual_world(skc62))
%   +(_115321)
%   +(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_115547, skf19(skc65, skc62, skc65)), skf19(skc65, skc62, skc65), skf12(skf19(skc65, skc62, skc65), skc62, Y_115547)))
%   +(in(skc62, skf12(skf19(skc65, skc62, skc65), skc62, skc67), skc67))
%   +(be(skc62, skf13(skc62, Y_115593, skf21(skc65, skc62, X_115598)), skf21(skc65, skc62, X_115598), skf12(skf21(skc65, skc62, X_115598), skc62, Y_115593)))
%   +(in(skc62, skf12(skf21(skc65, skc62, X_115627), skc62, skc67), skc67))
%   +(young(skc62, skf19(skc65, skc62, skc65)))
%   +(fellow(skc62, skf19(skc65, skc62, skc65)))
%   +(state(skc62, skf13(skc62, Y_115661, Z_115662)))
%   +(young(skc62, skf21(skc65, skc62, X_115674)))
%   +(fellow(skc62, skf21(skc65, skc62, X_115686)))
%   +(member(skc62, skf19(skc65, skc62, skc65), skc65))
%   +(member(skc62, skf21(skc65, skc62, X_115711), skc65))
%   -(ssSkP2(skc65, skc65, skc62))
%   -(nonreflexive(skc62, skc66))
%   -(in(skc62, skf12(skf16(skc69, skc62, skc65), skc62, Y_115777), skc69))
%   +(be(skc62, skf13(skc62, Y_115791, skf16(skc69, skc62, skc65)), skf16(skc69, skc62, skc65), skf12(skf16(skc69, skc62, skc65), skc62, Y_115791)))
%   +(in(skc62, skf12(skf16(skc69, skc62, skc65), skc62, skc67), skc67))
%   +(young(skc62, skf16(skc69, skc62, skc65)))
%   +(fellow(skc62, skf16(skc69, skc62, skc65)))
%   -(be(skc62, skf13(skc62, Y_115859, Z_115860), skf16(skc69, skc62, Y_115865), skc66))
%   +(member(skc62, skf16(skc69, skc62, skc65), skc65))
%   -(ssSkP1(skc69, skc65, skc62))
%   -(frontseat(skc62, skc69))
%   -(city(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_115995)))
%   +(black(skc62, skf21(skc63, skc62, X_116007)))
%   +(coat(skc62, skf21(skc63, skc62, X_116019)))
%   +(member(skc62, skf19(skc63, skc62, skc63), skc63))
%   +(member(skc62, skf21(skc63, skc62, X_116044), 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_116177, skf19(skc63, skc62, skc65)), skf19(skc63, skc62, skc65), skf12(skf19(skc63, skc62, skc65), skc62, Y_116177)))
%   +(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, skc63), skc63))
%   -(member(skc62, skf19(skc64, skc62, X_116293), 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_116358), skf19(skc63, skc62, skc63)), skf21(skc63, skc62, skc63)))
%   -(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_116383), skf19(skc65, skc62, skc63)), skf21(skc65, skc62, skc63)))
%   -(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116408), Z_116409), skf19(skc64, skc62, X_116408)))
%   +(patient(skc62, skf17(skc62, skf19(skc64, skc62, skc64), skf21(skc63, skc62, X_116434)), skf21(skc63, skc62, X_116434)))
%   +(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_116503), skf19(skc64, skc62, skc64)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116524), skf21(skc63, skc62, X_116529)), skf21(skc63, skc62, X_116529)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116550), skf19(skc63, skc62, skc63)), skf19(skc63, skc62, skc63)))
%   +(patient(skc62, skf17(skc62, skf21(skc64, skc62, X_116575), skf19(skc65, skc62, skc63)), skf19(skc65, skc62, skc63)))
%   +(agent(skc62, skf17(skc62, skf21(skc64, skc62, X_116600), Z_116601), skf21(skc64, skc62, X_116600)))
%   +(event(skc62, skf17(skc62, Z_116617, X1_116618)))
%   +(present(skc62, skf17(skc62, Z_116630, X1_116631)))
%   +(nonreflexive(skc62, skf17(skc62, Z_116643, X1_116644)))
%   +(wear(skc62, skf17(skc62, Z_116656, X1_116657)))
%   +(member(skc62, skf19(skc64, skc62, skc64), skc64))
%   +(member(skc62, skf21(skc64, skc62, X_116682), 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_116776)), skf21(skc63, skc62, X_116776)))
%   +(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_116845), 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_116955)), skf21(skc63, skc62, X_116955)))
%   +(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_117024), skf19(skc65, skc62, skc64)))
%   +(member(skc62, skf19(skc65, skc62, skc64), skc64))
%   -(ssSkP2(skc65, skc64, skc62))
%   -(two(skc62, skc64))
%   +(be(skc62, skf13(skc62, Y_117103, skf19(skc64, skc62, skc65)), skf19(skc64, skc62, skc65), skf12(skf19(skc64, skc62, skc65), skc62, Y_117103)))
%   +(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))
%   -(state(skc62, X_117202))
%   -(in(skc62, V_117228, skc69))
%   -(ssSkP1(skc69, W_117254, skc62))
%   -(agent(skc62, skf17(skc62, Z_117284, X1_117285), skf21(skc65, skc62, X_117290)))
%   -(event(skc62, V_117315))
%   -(agent(skc62, skf17(skc62, Z_117345, X1_117346), skf21(skc63, skc62, X_117351)))
%   -(agent(skc62, skf17(skc62, Z_117381, X1_117382), skf21(skc64, skc62, X_117387)))
%   -(group(skc62, X4_117412))
%   -(ssSkP1(Z_117438, skc65, skc62))
%   -(in(skc62, V_117464, W_117465))
%   -(member(skc62, V_117491, skc65))
%   +(member(skc62, skf16(U_117521, skc62, skc65), skc65))
%   -(ssSkP1(X_117547, W_117548, skc62))
%   -(group(skc18, X4_117573))
%   -(actual_world(V_117597))
%   +(in(skc62, skf12(skf16(U_117631, skc62, skc65), skc62, skc67), skc67))
%   -(ssSkP2(skc65, Y_117657, skc62))
%   -(ssSkP2(W_117683, skc65, skc62))
%   +(member(skc62, skf19(U_117713, skc62, skc65), skc65))
%   +(in(skc62, skf12(skf19(U_117747, skc62, skc65), skc62, skc67), skc67))
%   -(ssSkP2(W_117773, skc64, skc62))
%   -(member(skc62, skf21(skc65, skc62, X_117803), skc64))
%   -(ssSkP2(W_117829, skc63, skc62))
%   -(ssSkP2(W_117855, Y_117856, skc62))
%   -(member(skc62, skf21(skc63, skc62, X_117886), skc64))
%   +(ssSkP1(skc67, Z_117912, 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_117998)), skf21(skc63, skc62, X_117998)))
%   +(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)))
%   +(agent(skc62, skf17(skc62, skf16(skc67, skc62, skc64), Z_118067), skf16(skc67, skc62, skc64)))
%   -(be(skc62, skf13(skc62, Y_118085, Z_118086), skf16(skc67, skc62, Y_118091), skf12(skf21(skc65, skc62, X_118100), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_118114, Z_118115), skf16(skc67, skc62, Y_118120), skf12(skf19(skc65, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_118142, Z_118143), skf16(skc67, skc62, Y_118148), skf12(skf16(skc69, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_118170, Z_118171), skf16(skc67, skc62, Y_118176), skf12(skf19(skc63, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_118198, Z_118199), skf16(skc67, skc62, Y_118204), 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_118266), 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(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))
%   -(member(skc62, V_118449, W_118450))
%   +(member(skc62, skf16(skc69, skc62, V_118480), V_118480))
%   +(member(skc62, skf16(U_118510, skc62, V_118511), V_118511))
%   +(member(skc62, skf21(U_118541, skc62, X_118542), U_118541))
%   +(member(skc62, skf19(skc65, skc62, V_118572), V_118572))
%   +(member(skc62, skf19(U_118602, skc62, skc64), skc64))
%   +(member(skc62, skf19(U_118632, skc62, skc63), skc63))
%   +(member(skc62, skf19(U_118662, skc62, V_118663), V_118663))
%   +(in(skc62, skf12(skf16(skc69, skc62, W_118697), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf16(U_118731, skc62, W_118732), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf21(W_118766, skc62, X_118767), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf19(skc65, skc62, W_118801), skc62, skc67), skc67))
%   +(in(skc62, skf12(skf19(U_118835, skc62, W_118836), skc62, skc67), skc67))
%   -(be(skc62, skf13(skc62, Y_118867, Z_118868), skf16(skc67, skc62, Y_118873), skf12(skf16(U_118882, skc62, skc65), skc62, skc67)))
%   -(member(skc62, skf16(skc67, skc62, skc65), skc65))
%   -(be(skc62, skf13(skc62, Y_118942, Z_118943), skf16(skc67, skc62, Y_118948), skf12(skf19(U_118957, skc62, skc65), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_118988, Z_118989), skf16(skc67, skc62, Y_118994), skf12(skf16(skc69, skc62, W_119003), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_119034, Z_119035), skf16(skc67, skc62, Y_119040), skf12(skf16(U_119049, skc62, W_119050), skc62, skc67)))
%   -(member(skc62, skf16(skc67, skc62, W_119080), W_119080))
%   -(be(skc62, skf13(skc62, Y_119111, Z_119112), skf16(skc67, skc62, Y_119117), skf12(skf21(W_119126, skc62, X_119127), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_119158, Z_119159), skf16(skc67, skc62, Y_119164), skf12(skf19(skc65, skc62, W_119173), skc62, skc67)))
%   -(be(skc62, skf13(skc62, Y_119204, Z_119205), skf16(skc67, skc62, Y_119210), skf12(skf19(U_119219, skc62, W_119220), skc62, skc67)))
%   -(agent(skc62, skf17(skc62, Z_119250, X1_119251), skf21(W_119256, skc62, X_119257)))
% 
%------------------------------------------------------------------------------