↑ Up

FDP---0.9.16.SAT-Ass.s

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

% Computer : art06.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:49 EST 2011

% Result   : Satisfiable 158.74s
% Output   : Assurance 158.74s
% 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/NLP163-1+noeq ...
% Done.
% Input File...............: /tmp/NLP163-1+noeq.tme
% System...................: Linux art06.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...: [+(_113869)]
% 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.................: 65
% # Commits................: 1
% # Unit extension steps...: 122
% # Unit back subsumptions.: 0
% # Branches closed........: 0
% # Level cuts.............: 0
% Time.....................: 158.44 seconds.
% Result...................: SATISFIABLE with model:
%   +(actual_world(skc19))
%   +(actual_world(skc63))
%   +(_113947)
%   +(ssSkP2(skc65, skc64, skc63))
%   +(down(skc63, skc66, skc67))
%   +(of(skc63, skc68, skc69))
%   +(in(skc63, skc66, skc69))
%   +(agent(skc63, skc66, skc70))
%   +(ssSkP1(skc72, skc71, skc63))
%   +(group(skc63, skc64))
%   +(group(skc63, skc65))
%   +(lonely(skc63, skc67))
%   +(street(skc63, skc67))
%   +(city(skc63, skc69))
%   +(placename(skc63, skc68))
%   +(hollywood_placename(skc63, skc68))
%   +(event(skc63, skc66))
%   +(present(skc63, skc66))
%   +(barrel(skc63, skc66))
%   +(chevy(skc63, skc70))
%   +(white(skc63, skc70))
%   +(dirty(skc63, skc70))
%   +(old(skc63, skc70))
%   +(ssSkP0(skc71, skc63))
%   +(group(skc63, skc71))
%   +(two(skc63, skc71))
%   +(frontseat(skc63, skc72))
%   -(ssSkC0)
%   -(city(skc63, skc72))
%   +(be(skc63, skf13(skc63, Y_114197, skf19(skc71, skc63, skc71)), skf19(skc71, skc63, skc71), skf12(skf19(skc71, skc63, skc71), skc63, Y_114197)))
%   +(in(skc63, skf12(skf19(skc71, skc63, skc71), skc63, skc72), skc72))
%   +(be(skc63, skf13(skc63, Y_114243, skf21(skc71, skc63, X_114248)), skf21(skc71, skc63, X_114248), skf12(skf21(skc71, skc63, X_114248), skc63, Y_114243)))
%   +(in(skc63, skf12(skf21(skc71, skc63, X_114277), skc63, skc72), skc72))
%   +(young(skc63, skf19(skc71, skc63, skc71)))
%   +(fellow(skc63, skf19(skc71, skc63, skc71)))
%   +(state(skc63, skf13(skc63, Y_114311, Z_114312)))
%   +(young(skc63, skf21(skc71, skc63, X_114324)))
%   +(fellow(skc63, skf21(skc71, skc63, X_114336)))
%   +(member(skc63, skf19(skc71, skc63, skc71), skc71))
%   +(member(skc63, skf21(skc71, skc63, X_114361), skc71))
%   -(ssSkP2(skc71, skc71, skc63))
%   -(nonreflexive(skc63, skc66))
%   -(in(skc63, skf12(skf16(skc69, skc63, skc71), skc63, Y_114427), skc69))
%   +(be(skc63, skf13(skc63, Y_114441, skf16(skc69, skc63, skc71)), skf16(skc69, skc63, skc71), skf12(skf16(skc69, skc63, skc71), skc63, Y_114441)))
%   +(in(skc63, skf12(skf16(skc69, skc63, skc71), skc63, skc72), skc72))
%   +(young(skc63, skf16(skc69, skc63, skc71)))
%   +(fellow(skc63, skf16(skc69, skc63, skc71)))
%   -(be(skc63, skf13(skc63, Y_114509, Z_114510), skf16(skc69, skc63, Y_114515), skc66))
%   +(member(skc63, skf16(skc69, skc63, skc71), skc71))
%   -(ssSkP1(skc69, skc71, skc63))
%   -(frontseat(skc63, skc69))
%   +(member(skc63, skf19(skc65, skc63, skc65), skc65))
%   +(member(skc63, skf21(skc65, skc63, X_114601), skc65))
%   -(ssSkP2(skc65, skc65, skc63))
%   +(member(skc63, skf19(skc71, skc63, skc65), skc65))
%   -(ssSkP2(skc71, skc65, skc63))
%   -(two(skc63, skc65))
%   +(be(skc63, skf13(skc63, Y_114701, skf19(skc65, skc63, skc71)), skf19(skc65, skc63, skc71), skf12(skf19(skc65, skc63, skc71), skc63, Y_114701)))
%   +(in(skc63, skf12(skf19(skc65, skc63, skc71), skc63, skc72), skc72))
%   +(young(skc63, skf19(skc65, skc63, skc71)))
%   +(fellow(skc63, skf19(skc65, skc63, skc71)))
%   +(member(skc63, skf19(skc65, skc63, skc71), skc71))
%   -(ssSkP2(skc65, skc71, skc63))
%   -(member(skc63, skf19(skc65, skc63, skc64), skc64))
%   -(member(skc63, skf19(skc65, skc63, X_114817), skc64))
%   -(agent(skc63, skf17(skc63, skf21(skc65, skc63, X_114834), skf19(skc64, skc63, skc64)), skf21(skc64, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf19(skc64, skc63, skc64)), skf21(skc64, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf19(skc64, skc63, skc64)), skf21(skc64, skc63, skc64)))
%   -(patient(skc63, skf17(skc63, skf21(skc65, skc63, X_114907), Z_114908), skf19(skc65, skc63, X_114907)))
%   +(patient(skc63, skf17(skc63, skf21(skc65, skc63, X_114929), skf19(skc64, skc63, skc64)), skf19(skc64, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf19(skc64, skc63, skc64)), skf19(skc64, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf19(skc64, skc63, skc64)), skf19(skc64, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf21(skc65, skc63, X_115002), skf21(skc64, skc63, X_115007)), skf21(skc64, skc63, X_115007)))
%   +(patient(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf21(skc64, skc63, X_115032)), skf21(skc64, skc63, X_115032)))
%   +(patient(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf21(skc64, skc63, X_115057)), skf21(skc64, skc63, X_115057)))
%   +(agent(skc63, skf17(skc63, skf21(skc65, skc63, X_115078), Z_115079), skf21(skc65, skc63, X_115078)))
%   +(agent(skc63, skf17(skc63, skf19(skc65, skc63, skc65), Z_115100), skf19(skc65, skc63, skc65)))
%   +(agent(skc63, skf17(skc63, skf19(skc71, skc63, skc65), Z_115121), skf19(skc71, skc63, skc65)))
%   +(cheap(skc63, skf19(skc64, skc63, skc64)))
%   +(black(skc63, skf19(skc64, skc63, skc64)))
%   +(coat(skc63, skf19(skc64, skc63, skc64)))
%   +(event(skc63, skf17(skc63, Z_115170, X1_115171)))
%   +(present(skc63, skf17(skc63, Z_115183, X1_115184)))
%   +(nonreflexive(skc63, skf17(skc63, Z_115196, X1_115197)))
%   +(wear(skc63, skf17(skc63, Z_115209, X1_115210)))
%   +(cheap(skc63, skf21(skc64, skc63, X_115222)))
%   +(black(skc63, skf21(skc64, skc63, X_115234)))
%   +(coat(skc63, skf21(skc64, skc63, X_115246)))
%   +(member(skc63, skf19(skc64, skc63, skc64), skc64))
%   +(member(skc63, skf21(skc64, skc63, X_115271), skc64))
%   -(ssSkP2(skc64, skc64, skc63))
%   -(agent(skc63, skf17(skc63, skf21(skc65, skc63, X_115313), skf19(skc71, skc63, skc64)), skf21(skc71, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf19(skc71, skc63, skc64)), skf21(skc71, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf19(skc71, skc63, skc64)), skf21(skc71, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf21(skc65, skc63, X_115386), skf19(skc71, skc63, skc64)), skf19(skc71, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf19(skc71, skc63, skc64)), skf19(skc71, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf19(skc71, skc63, skc64)), skf19(skc71, skc63, skc64)))
%   +(cheap(skc63, skf19(skc71, skc63, skc64)))
%   +(black(skc63, skf19(skc71, skc63, skc64)))
%   +(coat(skc63, skf19(skc71, skc63, skc64)))
%   +(member(skc63, skf19(skc71, skc63, skc64), skc64))
%   -(ssSkP2(skc71, skc64, skc63))
%   -(two(skc63, skc64))
%   -(agent(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf19(skc64, skc63, skc64)), skf21(skc64, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf19(skc71, skc63, skc64)), skf21(skc71, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf21(skc64, skc63, X_115605)), skf21(skc64, skc63, X_115605)))
%   +(patient(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf19(skc64, skc63, skc64)), skf19(skc64, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf19(skc71, skc63, skc64)), skf19(skc71, skc63, skc64)))
%   +(agent(skc63, skf17(skc63, skf19(skc64, skc63, skc65), Z_115674), skf19(skc64, skc63, skc65)))
%   +(member(skc63, skf19(skc64, skc63, skc65), skc65))
%   -(ssSkP2(skc64, skc65, skc63))
%   +(be(skc63, skf13(skc63, Y_115729, skf19(skc64, skc63, skc71)), skf19(skc64, skc63, skc71), skf12(skf19(skc64, skc63, skc71), skc63, Y_115729)))
%   +(in(skc63, skf12(skf19(skc64, skc63, skc71), skc63, skc72), skc72))
%   +(young(skc63, skf19(skc64, skc63, skc71)))
%   +(fellow(skc63, skf19(skc64, skc63, skc71)))
%   +(member(skc63, skf19(skc64, skc63, skc71), skc71))
%   -(ssSkP2(skc64, skc71, skc63))
%   -(state(skc63, X_115828))
%   -(in(skc63, V_115854, skc69))
%   -(ssSkP1(skc69, W_115880, skc63))
%   -(agent(skc63, skf17(skc63, Z_115910, X1_115911), skf21(skc71, skc63, X_115916)))
%   -(event(skc63, V_115941))
%   -(agent(skc63, skf17(skc63, Z_115971, X1_115972), skf21(skc65, skc63, X_115977)))
%   -(agent(skc63, skf17(skc63, Z_116007, X1_116008), skf21(skc64, skc63, X_116013)))
%   -(ssSkP1(Z_116039, skc71, skc63))
%   -(in(skc63, V_116065, W_116066))
%   -(member(skc63, V_116092, skc71))
%   +(member(skc63, skf16(U_116122, skc63, skc71), skc71))
%   -(ssSkP1(X_116148, W_116149, skc63))
%   -(group(skc19, X4_116174))
%   -(actual_world(V_116198))
%   +(in(skc63, skf12(skf16(U_116232, skc63, skc71), skc63, skc72), skc72))
%   -(ssSkP2(skc71, Y_116258, skc63))
%   -(ssSkP2(W_116284, skc71, skc63))
%   +(member(skc63, skf19(U_116314, skc63, skc71), skc71))
%   +(in(skc63, skf12(skf19(U_116348, skc63, skc71), skc63, skc72), skc72))
%   -(ssSkP2(W_116374, skc65, skc63))
%   -(member(skc63, skf21(skc71, skc63, X_116404), skc65))
%   -(ssSkP2(W_116430, skc64, skc63))
%   -(ssSkP2(W_116456, Y_116457, skc63))
%   -(member(skc63, skf21(skc64, skc63, X_116487), skc65))
%   +(ssSkP1(skc72, Z_116513, skc63))
%   -(agent(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf19(skc64, skc63, skc64)), skf21(skc64, skc63, skc64)))
%   -(agent(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf19(skc71, skc63, skc64)), skf21(skc71, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf21(skc64, skc63, X_116599)), skf21(skc64, skc63, X_116599)))
%   +(patient(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf19(skc64, skc63, skc64)), skf19(skc64, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf19(skc71, skc63, skc64)), skf19(skc71, skc63, skc64)))
%   +(agent(skc63, skf17(skc63, skf16(skc72, skc63, skc65), Z_116668), skf16(skc72, skc63, skc65)))
%   -(be(skc63, skf13(skc63, Y_116686, Z_116687), skf16(skc72, skc63, Y_116692), skf12(skf21(skc71, skc63, X_116701), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_116715, Z_116716), skf16(skc72, skc63, Y_116721), skf12(skf19(skc71, skc63, skc71), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_116743, Z_116744), skf16(skc72, skc63, Y_116749), skf12(skf16(skc69, skc63, skc71), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_116771, Z_116772), skf16(skc72, skc63, Y_116777), skf12(skf19(skc65, skc63, skc71), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_116799, Z_116800), skf16(skc72, skc63, Y_116805), skf12(skf19(skc64, skc63, skc71), skc63, skc72)))
%   +(member(skc63, skf16(skc72, skc63, skc65), skc65))
%   -(ssSkP1(skc72, skc65, skc63))
%   +(patient(skc63, skf17(skc63, skf21(skc65, skc63, X_116867), skf16(skc72, skc63, skc64)), skf16(skc72, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc65, skc63, skc65), skf16(skc72, skc63, skc64)), skf16(skc72, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc71, skc63, skc65), skf16(skc72, skc63, skc64)), skf16(skc72, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf19(skc64, skc63, skc65), skf16(skc72, skc63, skc64)), skf16(skc72, skc63, skc64)))
%   +(patient(skc63, skf17(skc63, skf16(skc72, skc63, skc65), skf16(skc72, skc63, skc64)), skf16(skc72, skc63, skc64)))
%   +(cheap(skc63, skf16(skc72, skc63, skc64)))
%   +(black(skc63, skf16(skc72, skc63, skc64)))
%   +(coat(skc63, skf16(skc72, skc63, skc64)))
%   +(member(skc63, skf16(skc72, skc63, skc64), skc64))
%   -(ssSkP1(skc72, skc64, skc63))
%   -(member(skc63, V_117050, W_117051))
%   +(member(skc63, skf16(skc69, skc63, V_117081), V_117081))
%   +(member(skc63, skf16(U_117111, skc63, V_117112), V_117112))
%   +(member(skc63, skf21(U_117142, skc63, X_117143), U_117142))
%   +(member(skc63, skf19(skc71, skc63, V_117173), V_117173))
%   +(member(skc63, skf19(U_117203, skc63, skc65), skc65))
%   +(member(skc63, skf19(U_117233, skc63, skc64), skc64))
%   +(member(skc63, skf19(U_117263, skc63, V_117264), V_117264))
%   +(in(skc63, skf12(skf16(skc69, skc63, W_117298), skc63, skc72), skc72))
%   +(in(skc63, skf12(skf16(U_117332, skc63, W_117333), skc63, skc72), skc72))
%   +(in(skc63, skf12(skf21(W_117367, skc63, X_117368), skc63, skc72), skc72))
%   +(in(skc63, skf12(skf19(skc71, skc63, W_117402), skc63, skc72), skc72))
%   +(in(skc63, skf12(skf19(U_117436, skc63, W_117437), skc63, skc72), skc72))
%   -(be(skc63, skf13(skc63, Y_117468, Z_117469), skf16(skc72, skc63, Y_117474), skf12(skf16(U_117483, skc63, skc71), skc63, skc72)))
%   -(member(skc63, skf16(skc72, skc63, skc71), skc71))
%   -(be(skc63, skf13(skc63, Y_117543, Z_117544), skf16(skc72, skc63, Y_117549), skf12(skf19(U_117558, skc63, skc71), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_117589, Z_117590), skf16(skc72, skc63, Y_117595), skf12(skf16(skc69, skc63, W_117604), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_117635, Z_117636), skf16(skc72, skc63, Y_117641), skf12(skf16(U_117650, skc63, W_117651), skc63, skc72)))
%   -(member(skc63, skf16(skc72, skc63, W_117681), W_117681))
%   -(be(skc63, skf13(skc63, Y_117712, Z_117713), skf16(skc72, skc63, Y_117718), skf12(skf21(W_117727, skc63, X_117728), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_117759, Z_117760), skf16(skc72, skc63, Y_117765), skf12(skf19(skc71, skc63, W_117774), skc63, skc72)))
%   -(be(skc63, skf13(skc63, Y_117805, Z_117806), skf16(skc72, skc63, Y_117811), skf12(skf19(U_117820, skc63, W_117821), skc63, skc72)))
%   -(agent(skc63, skf17(skc63, Z_117851, X1_117852), skf21(W_117857, skc63, X_117858)))
% 
%------------------------------------------------------------------------------