%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NLP009+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.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 : Wed Dec 29 16:14:32 EST 2010
% Result : Theorem 0.97s
% Output : Solution 0.97s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP7088/NLP009+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP7088/NLP009+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP7088/NLP009+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 7184
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.013 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, conjecture,((?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:(((((((((((((((((((((((((((hollywood(X1)&city(X1))&event(X2))&street(X3))&way(X3))&lonely(X3))&chevy(X4))&car(X4))&white(X4))&dirty(X4))&old(X4))&barrel(X2,X4))&down(X2,X3))&in(X2,X1))&seat(X7))&furniture(X7))&front(X7))&~(X5=X6))&fellow(X5))&man(X5))&young(X5))&fellow(X6))&man(X6))&young(X6))&X5=X8)&in(X8,X7))&X6=X9)&in(X9,X7))=>?[X10]:?[X11]:?[X12]:?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:(((((((((((((((((((((((((((hollywood(X10)&city(X10))&event(X11))&chevy(X12))&car(X12))&white(X12))&dirty(X12))&old(X12))&street(X13))&way(X13))&lonely(X13))&barrel(X11,X12))&down(X11,X13))&in(X11,X10))&seat(X16))&furniture(X16))&front(X16))&~(X14=X15))&fellow(X14))&man(X14))&young(X14))&fellow(X15))&man(X15))&young(X15))&X14=X17)&in(X17,X16))&X15=X18)&in(X18,X16)))&(?[X19]:?[X20]:?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:(((((((((((((((((((((((((((hollywood(X19)&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&seat(X25))&furniture(X25))&front(X25))&~(X23=X24))&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X25))&X24=X27)&in(X27,X25))=>?[X28]:?[X29]:?[X30]:?[X31]:?[X32]:?[X33]:?[X34]:?[X35]:?[X36]:(((((((((((((((((((((((((((hollywood(X28)&city(X28))&event(X29))&street(X30))&way(X30))&lonely(X30))&chevy(X31))&car(X31))&white(X31))&dirty(X31))&old(X31))&barrel(X29,X31))&down(X29,X30))&in(X29,X28))&seat(X34))&furniture(X34))&front(X34))&~(X32=X33))&fellow(X32))&man(X32))&young(X32))&fellow(X33))&man(X33))&young(X33))&X32=X35)&in(X35,X34))&X33=X36)&in(X36,X34)))),file('/tmp/SRASS.s.p', co1)).
% fof(2, negated_conjecture,~(((?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:(((((((((((((((((((((((((((hollywood(X1)&city(X1))&event(X2))&street(X3))&way(X3))&lonely(X3))&chevy(X4))&car(X4))&white(X4))&dirty(X4))&old(X4))&barrel(X2,X4))&down(X2,X3))&in(X2,X1))&seat(X7))&furniture(X7))&front(X7))&~(X5=X6))&fellow(X5))&man(X5))&young(X5))&fellow(X6))&man(X6))&young(X6))&X5=X8)&in(X8,X7))&X6=X9)&in(X9,X7))=>?[X10]:?[X11]:?[X12]:?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:(((((((((((((((((((((((((((hollywood(X10)&city(X10))&event(X11))&chevy(X12))&car(X12))&white(X12))&dirty(X12))&old(X12))&street(X13))&way(X13))&lonely(X13))&barrel(X11,X12))&down(X11,X13))&in(X11,X10))&seat(X16))&furniture(X16))&front(X16))&~(X14=X15))&fellow(X14))&man(X14))&young(X14))&fellow(X15))&man(X15))&young(X15))&X14=X17)&in(X17,X16))&X15=X18)&in(X18,X16)))&(?[X19]:?[X20]:?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:(((((((((((((((((((((((((((hollywood(X19)&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&seat(X25))&furniture(X25))&front(X25))&~(X23=X24))&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X25))&X24=X27)&in(X27,X25))=>?[X28]:?[X29]:?[X30]:?[X31]:?[X32]:?[X33]:?[X34]:?[X35]:?[X36]:(((((((((((((((((((((((((((hollywood(X28)&city(X28))&event(X29))&street(X30))&way(X30))&lonely(X30))&chevy(X31))&car(X31))&white(X31))&dirty(X31))&old(X31))&barrel(X29,X31))&down(X29,X30))&in(X29,X28))&seat(X34))&furniture(X34))&front(X34))&~(X32=X33))&fellow(X32))&man(X32))&young(X32))&fellow(X33))&man(X33))&young(X33))&X32=X35)&in(X35,X34))&X33=X36)&in(X36,X34))))),inference(assume_negation,[status(cth)],[1])).
% fof(3, plain,((?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:(((((((((((((((((((((((((((hollywood(X1)&city(X1))&event(X2))&street(X3))&way(X3))&lonely(X3))&chevy(X4))&car(X4))&white(X4))&dirty(X4))&old(X4))&barrel(X2,X4))&down(X2,X3))&in(X2,X1))&seat(X7))&furniture(X7))&front(X7))&~(X5=X6))&fellow(X5))&man(X5))&young(X5))&fellow(X6))&man(X6))&young(X6))&X5=X8)&in(X8,X7))&X6=X9)&in(X9,X7))=>?[X10]:?[X11]:?[X12]:?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:(((((((((((((((((((((((((((hollywood(X10)&city(X10))&event(X11))&chevy(X12))&car(X12))&white(X12))&dirty(X12))&old(X12))&street(X13))&way(X13))&lonely(X13))&barrel(X11,X12))&down(X11,X13))&in(X11,X10))&seat(X16))&furniture(X16))&front(X16))&~(X14=X15))&fellow(X14))&man(X14))&young(X14))&fellow(X15))&man(X15))&young(X15))&X14=X17)&in(X17,X16))&X15=X18)&in(X18,X16)))=>epred1_0),introduced(definition)).
% fof(4, plain,((?[X19]:?[X20]:?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:(((((((((((((((((((((((((((hollywood(X19)&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&seat(X25))&furniture(X25))&front(X25))&~(X23=X24))&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X25))&X24=X27)&in(X27,X25))=>?[X28]:?[X29]:?[X30]:?[X31]:?[X32]:?[X33]:?[X34]:?[X35]:?[X36]:(((((((((((((((((((((((((((hollywood(X28)&city(X28))&event(X29))&street(X30))&way(X30))&lonely(X30))&chevy(X31))&car(X31))&white(X31))&dirty(X31))&old(X31))&barrel(X29,X31))&down(X29,X30))&in(X29,X28))&seat(X34))&furniture(X34))&front(X34))&~(X32=X33))&fellow(X32))&man(X32))&young(X32))&fellow(X33))&man(X33))&young(X33))&X32=X35)&in(X35,X34))&X33=X36)&in(X36,X34)))=>epred2_0),introduced(definition)).
% fof(5, negated_conjecture,~((epred1_0&epred2_0)),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[2,3,theory(equality)]),4,theory(equality)])).
% fof(6, negated_conjecture,(~(epred1_0)|~(epred2_0)),inference(fof_nnf,[status(thm)],[5])).
% cnf(7,negated_conjecture,(~epred2_0|~epred1_0),inference(split_conjunct,[status(thm)],[6])).
% fof(8, plain,((?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:(((((((((((((((((((((((((((hollywood(X1)&city(X1))&event(X2))&street(X3))&way(X3))&lonely(X3))&chevy(X4))&car(X4))&white(X4))&dirty(X4))&old(X4))&barrel(X2,X4))&down(X2,X3))&in(X2,X1))&seat(X7))&furniture(X7))&front(X7))&~(X5=X6))&fellow(X5))&man(X5))&young(X5))&fellow(X6))&man(X6))&young(X6))&X5=X8)&in(X8,X7))&X6=X9)&in(X9,X7))&![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:![X17]:![X18]:(((((((((((((((((((((((((((~(hollywood(X10))|~(city(X10)))|~(event(X11)))|~(chevy(X12)))|~(car(X12)))|~(white(X12)))|~(dirty(X12)))|~(old(X12)))|~(street(X13)))|~(way(X13)))|~(lonely(X13)))|~(barrel(X11,X12)))|~(down(X11,X13)))|~(in(X11,X10)))|~(seat(X16)))|~(furniture(X16)))|~(front(X16)))|X14=X15)|~(fellow(X14)))|~(man(X14)))|~(young(X14)))|~(fellow(X15)))|~(man(X15)))|~(young(X15)))|~(X14=X17))|~(in(X17,X16)))|~(X15=X18))|~(in(X18,X16))))|epred1_0),inference(fof_nnf,[status(thm)],[3])).
% fof(9, plain,((?[X19]:?[X20]:?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:(((((((((((((((((((((((((((hollywood(X19)&city(X19))&event(X20))&street(X21))&way(X21))&lonely(X21))&chevy(X22))&car(X22))&white(X22))&dirty(X22))&old(X22))&barrel(X20,X22))&down(X20,X21))&in(X20,X19))&seat(X25))&furniture(X25))&front(X25))&~(X23=X24))&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X25))&X24=X27)&in(X27,X25))&![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:(((((((((((((((((((((((((((~(hollywood(X28))|~(city(X28)))|~(event(X29)))|~(chevy(X30)))|~(car(X30)))|~(white(X30)))|~(dirty(X30)))|~(old(X30)))|~(street(X31)))|~(way(X31)))|~(lonely(X31)))|~(barrel(X29,X30)))|~(down(X29,X31)))|~(in(X29,X28)))|~(seat(X34)))|~(furniture(X34)))|~(front(X34)))|X32=X33)|~(fellow(X32)))|~(man(X32)))|~(young(X32)))|~(fellow(X33)))|~(man(X33)))|~(young(X33)))|~(X32=X35))|~(in(X35,X34)))|~(X33=X36))|~(in(X36,X34))))|epred1_0),inference(variable_rename,[status(thm)],[8])).
% fof(10, plain,(((((((((((((((((((((((((((((hollywood(esk1_0)&city(esk1_0))&event(esk2_0))&street(esk3_0))&way(esk3_0))&lonely(esk3_0))&chevy(esk4_0))&car(esk4_0))&white(esk4_0))&dirty(esk4_0))&old(esk4_0))&barrel(esk2_0,esk4_0))&down(esk2_0,esk3_0))&in(esk2_0,esk1_0))&seat(esk7_0))&furniture(esk7_0))&front(esk7_0))&~(esk5_0=esk6_0))&fellow(esk5_0))&man(esk5_0))&young(esk5_0))&fellow(esk6_0))&man(esk6_0))&young(esk6_0))&esk5_0=esk8_0)&in(esk8_0,esk7_0))&esk6_0=esk9_0)&in(esk9_0,esk7_0))&![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:(((((((((((((((((((((((((((~(hollywood(X28))|~(city(X28)))|~(event(X29)))|~(chevy(X30)))|~(car(X30)))|~(white(X30)))|~(dirty(X30)))|~(old(X30)))|~(street(X31)))|~(way(X31)))|~(lonely(X31)))|~(barrel(X29,X30)))|~(down(X29,X31)))|~(in(X29,X28)))|~(seat(X34)))|~(furniture(X34)))|~(front(X34)))|X32=X33)|~(fellow(X32)))|~(man(X32)))|~(young(X32)))|~(fellow(X33)))|~(man(X33)))|~(young(X33)))|~(X32=X35))|~(in(X35,X34)))|~(X33=X36))|~(in(X36,X34))))|epred1_0),inference(skolemize,[status(esa)],[9])).
% fof(11, plain,![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:(((((((((((((((((((((((((((((~(hollywood(X28))|~(city(X28)))|~(event(X29)))|~(chevy(X30)))|~(car(X30)))|~(white(X30)))|~(dirty(X30)))|~(old(X30)))|~(street(X31)))|~(way(X31)))|~(lonely(X31)))|~(barrel(X29,X30)))|~(down(X29,X31)))|~(in(X29,X28)))|~(seat(X34)))|~(furniture(X34)))|~(front(X34)))|X32=X33)|~(fellow(X32)))|~(man(X32)))|~(young(X32)))|~(fellow(X33)))|~(man(X33)))|~(young(X33)))|~(X32=X35))|~(in(X35,X34)))|~(X33=X36))|~(in(X36,X34)))&(((((((((((((((((((((((((((hollywood(esk1_0)&city(esk1_0))&event(esk2_0))&street(esk3_0))&way(esk3_0))&lonely(esk3_0))&chevy(esk4_0))&car(esk4_0))&white(esk4_0))&dirty(esk4_0))&old(esk4_0))&barrel(esk2_0,esk4_0))&down(esk2_0,esk3_0))&in(esk2_0,esk1_0))&seat(esk7_0))&furniture(esk7_0))&front(esk7_0))&~(esk5_0=esk6_0))&fellow(esk5_0))&man(esk5_0))&young(esk5_0))&fellow(esk6_0))&man(esk6_0))&young(esk6_0))&esk5_0=esk8_0)&in(esk8_0,esk7_0))&esk6_0=esk9_0)&in(esk9_0,esk7_0)))|epred1_0),inference(shift_quantors,[status(thm)],[10])).
% fof(12, plain,![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:(((((((((((((((((((((((((((((~(hollywood(X28))|~(city(X28)))|~(event(X29)))|~(chevy(X30)))|~(car(X30)))|~(white(X30)))|~(dirty(X30)))|~(old(X30)))|~(street(X31)))|~(way(X31)))|~(lonely(X31)))|~(barrel(X29,X30)))|~(down(X29,X31)))|~(in(X29,X28)))|~(seat(X34)))|~(furniture(X34)))|~(front(X34)))|X32=X33)|~(fellow(X32)))|~(man(X32)))|~(young(X32)))|~(fellow(X33)))|~(man(X33)))|~(young(X33)))|~(X32=X35))|~(in(X35,X34)))|~(X33=X36))|~(in(X36,X34)))|epred1_0)&((((((((((((((((((((((((((((hollywood(esk1_0)|epred1_0)&(city(esk1_0)|epred1_0))&(event(esk2_0)|epred1_0))&(street(esk3_0)|epred1_0))&(way(esk3_0)|epred1_0))&(lonely(esk3_0)|epred1_0))&(chevy(esk4_0)|epred1_0))&(car(esk4_0)|epred1_0))&(white(esk4_0)|epred1_0))&(dirty(esk4_0)|epred1_0))&(old(esk4_0)|epred1_0))&(barrel(esk2_0,esk4_0)|epred1_0))&(down(esk2_0,esk3_0)|epred1_0))&(in(esk2_0,esk1_0)|epred1_0))&(seat(esk7_0)|epred1_0))&(furniture(esk7_0)|epred1_0))&(front(esk7_0)|epred1_0))&(~(esk5_0=esk6_0)|epred1_0))&(fellow(esk5_0)|epred1_0))&(man(esk5_0)|epred1_0))&(young(esk5_0)|epred1_0))&(fellow(esk6_0)|epred1_0))&(man(esk6_0)|epred1_0))&(young(esk6_0)|epred1_0))&(esk5_0=esk8_0|epred1_0))&(in(esk8_0,esk7_0)|epred1_0))&(esk6_0=esk9_0|epred1_0))&(in(esk9_0,esk7_0)|epred1_0))),inference(distribute,[status(thm)],[11])).
% cnf(13,plain,(epred1_0|in(esk9_0,esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(14,plain,(epred1_0|esk6_0=esk9_0),inference(split_conjunct,[status(thm)],[12])).
% cnf(15,plain,(epred1_0|in(esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(16,plain,(epred1_0|esk5_0=esk8_0),inference(split_conjunct,[status(thm)],[12])).
% cnf(17,plain,(epred1_0|young(esk6_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(18,plain,(epred1_0|man(esk6_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(19,plain,(epred1_0|fellow(esk6_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(20,plain,(epred1_0|young(esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(21,plain,(epred1_0|man(esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(22,plain,(epred1_0|fellow(esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(23,plain,(epred1_0|esk5_0!=esk6_0),inference(split_conjunct,[status(thm)],[12])).
% cnf(24,plain,(epred1_0|front(esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(25,plain,(epred1_0|furniture(esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(26,plain,(epred1_0|seat(esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(27,plain,(epred1_0|in(esk2_0,esk1_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(28,plain,(epred1_0|down(esk2_0,esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(29,plain,(epred1_0|barrel(esk2_0,esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(30,plain,(epred1_0|old(esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(31,plain,(epred1_0|dirty(esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(32,plain,(epred1_0|white(esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(33,plain,(epred1_0|car(esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(34,plain,(epred1_0|chevy(esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(35,plain,(epred1_0|lonely(esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(36,plain,(epred1_0|way(esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(37,plain,(epred1_0|street(esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(38,plain,(epred1_0|event(esk2_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(39,plain,(epred1_0|city(esk1_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(40,plain,(epred1_0|hollywood(esk1_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(41,plain,(epred1_0|X5=X3|~in(X1,X2)|X3!=X1|~in(X4,X2)|X5!=X4|~young(X3)|~man(X3)|~fellow(X3)|~young(X5)|~man(X5)|~fellow(X5)|~front(X2)|~furniture(X2)|~seat(X2)|~in(X6,X7)|~down(X6,X8)|~barrel(X6,X9)|~lonely(X8)|~way(X8)|~street(X8)|~old(X9)|~dirty(X9)|~white(X9)|~car(X9)|~chevy(X9)|~event(X6)|~city(X7)|~hollywood(X7)),inference(split_conjunct,[status(thm)],[12])).
% fof(42, plain,((?[X19]:?[X20]:?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:(((((((((((((((((((((((((((hollywood(X19)&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&seat(X25))&furniture(X25))&front(X25))&~(X23=X24))&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X25))&X24=X27)&in(X27,X25))&![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:(((((((((((((((((((((((((((~(hollywood(X28))|~(city(X28)))|~(event(X29)))|~(street(X30)))|~(way(X30)))|~(lonely(X30)))|~(chevy(X31)))|~(car(X31)))|~(white(X31)))|~(dirty(X31)))|~(old(X31)))|~(barrel(X29,X31)))|~(down(X29,X30)))|~(in(X29,X28)))|~(seat(X34)))|~(furniture(X34)))|~(front(X34)))|X32=X33)|~(fellow(X32)))|~(man(X32)))|~(young(X32)))|~(fellow(X33)))|~(man(X33)))|~(young(X33)))|~(X32=X35))|~(in(X35,X34)))|~(X33=X36))|~(in(X36,X34))))|epred2_0),inference(fof_nnf,[status(thm)],[4])).
% fof(43, plain,((?[X37]:?[X38]:?[X39]:?[X40]:?[X41]:?[X42]:?[X43]:?[X44]:?[X45]:(((((((((((((((((((((((((((hollywood(X37)&city(X37))&event(X38))&chevy(X39))&car(X39))&white(X39))&dirty(X39))&old(X39))&street(X40))&way(X40))&lonely(X40))&barrel(X38,X39))&down(X38,X40))&in(X38,X37))&seat(X43))&furniture(X43))&front(X43))&~(X41=X42))&fellow(X41))&man(X41))&young(X41))&fellow(X42))&man(X42))&young(X42))&X41=X44)&in(X44,X43))&X42=X45)&in(X45,X43))&![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:(((((((((((((((((((((((((((~(hollywood(X46))|~(city(X46)))|~(event(X47)))|~(street(X48)))|~(way(X48)))|~(lonely(X48)))|~(chevy(X49)))|~(car(X49)))|~(white(X49)))|~(dirty(X49)))|~(old(X49)))|~(barrel(X47,X49)))|~(down(X47,X48)))|~(in(X47,X46)))|~(seat(X52)))|~(furniture(X52)))|~(front(X52)))|X50=X51)|~(fellow(X50)))|~(man(X50)))|~(young(X50)))|~(fellow(X51)))|~(man(X51)))|~(young(X51)))|~(X50=X53))|~(in(X53,X52)))|~(X51=X54))|~(in(X54,X52))))|epred2_0),inference(variable_rename,[status(thm)],[42])).
% fof(44, plain,(((((((((((((((((((((((((((((hollywood(esk10_0)&city(esk10_0))&event(esk11_0))&chevy(esk12_0))&car(esk12_0))&white(esk12_0))&dirty(esk12_0))&old(esk12_0))&street(esk13_0))&way(esk13_0))&lonely(esk13_0))&barrel(esk11_0,esk12_0))&down(esk11_0,esk13_0))&in(esk11_0,esk10_0))&seat(esk16_0))&furniture(esk16_0))&front(esk16_0))&~(esk14_0=esk15_0))&fellow(esk14_0))&man(esk14_0))&young(esk14_0))&fellow(esk15_0))&man(esk15_0))&young(esk15_0))&esk14_0=esk17_0)&in(esk17_0,esk16_0))&esk15_0=esk18_0)&in(esk18_0,esk16_0))&![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:(((((((((((((((((((((((((((~(hollywood(X46))|~(city(X46)))|~(event(X47)))|~(street(X48)))|~(way(X48)))|~(lonely(X48)))|~(chevy(X49)))|~(car(X49)))|~(white(X49)))|~(dirty(X49)))|~(old(X49)))|~(barrel(X47,X49)))|~(down(X47,X48)))|~(in(X47,X46)))|~(seat(X52)))|~(furniture(X52)))|~(front(X52)))|X50=X51)|~(fellow(X50)))|~(man(X50)))|~(young(X50)))|~(fellow(X51)))|~(man(X51)))|~(young(X51)))|~(X50=X53))|~(in(X53,X52)))|~(X51=X54))|~(in(X54,X52))))|epred2_0),inference(skolemize,[status(esa)],[43])).
% fof(45, plain,![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:(((((((((((((((((((((((((((((~(hollywood(X46))|~(city(X46)))|~(event(X47)))|~(street(X48)))|~(way(X48)))|~(lonely(X48)))|~(chevy(X49)))|~(car(X49)))|~(white(X49)))|~(dirty(X49)))|~(old(X49)))|~(barrel(X47,X49)))|~(down(X47,X48)))|~(in(X47,X46)))|~(seat(X52)))|~(furniture(X52)))|~(front(X52)))|X50=X51)|~(fellow(X50)))|~(man(X50)))|~(young(X50)))|~(fellow(X51)))|~(man(X51)))|~(young(X51)))|~(X50=X53))|~(in(X53,X52)))|~(X51=X54))|~(in(X54,X52)))&(((((((((((((((((((((((((((hollywood(esk10_0)&city(esk10_0))&event(esk11_0))&chevy(esk12_0))&car(esk12_0))&white(esk12_0))&dirty(esk12_0))&old(esk12_0))&street(esk13_0))&way(esk13_0))&lonely(esk13_0))&barrel(esk11_0,esk12_0))&down(esk11_0,esk13_0))&in(esk11_0,esk10_0))&seat(esk16_0))&furniture(esk16_0))&front(esk16_0))&~(esk14_0=esk15_0))&fellow(esk14_0))&man(esk14_0))&young(esk14_0))&fellow(esk15_0))&man(esk15_0))&young(esk15_0))&esk14_0=esk17_0)&in(esk17_0,esk16_0))&esk15_0=esk18_0)&in(esk18_0,esk16_0)))|epred2_0),inference(shift_quantors,[status(thm)],[44])).
% fof(46, plain,![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:(((((((((((((((((((((((((((((~(hollywood(X46))|~(city(X46)))|~(event(X47)))|~(street(X48)))|~(way(X48)))|~(lonely(X48)))|~(chevy(X49)))|~(car(X49)))|~(white(X49)))|~(dirty(X49)))|~(old(X49)))|~(barrel(X47,X49)))|~(down(X47,X48)))|~(in(X47,X46)))|~(seat(X52)))|~(furniture(X52)))|~(front(X52)))|X50=X51)|~(fellow(X50)))|~(man(X50)))|~(young(X50)))|~(fellow(X51)))|~(man(X51)))|~(young(X51)))|~(X50=X53))|~(in(X53,X52)))|~(X51=X54))|~(in(X54,X52)))|epred2_0)&((((((((((((((((((((((((((((hollywood(esk10_0)|epred2_0)&(city(esk10_0)|epred2_0))&(event(esk11_0)|epred2_0))&(chevy(esk12_0)|epred2_0))&(car(esk12_0)|epred2_0))&(white(esk12_0)|epred2_0))&(dirty(esk12_0)|epred2_0))&(old(esk12_0)|epred2_0))&(street(esk13_0)|epred2_0))&(way(esk13_0)|epred2_0))&(lonely(esk13_0)|epred2_0))&(barrel(esk11_0,esk12_0)|epred2_0))&(down(esk11_0,esk13_0)|epred2_0))&(in(esk11_0,esk10_0)|epred2_0))&(seat(esk16_0)|epred2_0))&(furniture(esk16_0)|epred2_0))&(front(esk16_0)|epred2_0))&(~(esk14_0=esk15_0)|epred2_0))&(fellow(esk14_0)|epred2_0))&(man(esk14_0)|epred2_0))&(young(esk14_0)|epred2_0))&(fellow(esk15_0)|epred2_0))&(man(esk15_0)|epred2_0))&(young(esk15_0)|epred2_0))&(esk14_0=esk17_0|epred2_0))&(in(esk17_0,esk16_0)|epred2_0))&(esk15_0=esk18_0|epred2_0))&(in(esk18_0,esk16_0)|epred2_0))),inference(distribute,[status(thm)],[45])).
% cnf(47,plain,(epred2_0|in(esk18_0,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(48,plain,(epred2_0|esk15_0=esk18_0),inference(split_conjunct,[status(thm)],[46])).
% cnf(49,plain,(epred2_0|in(esk17_0,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(50,plain,(epred2_0|esk14_0=esk17_0),inference(split_conjunct,[status(thm)],[46])).
% cnf(51,plain,(epred2_0|young(esk15_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(52,plain,(epred2_0|man(esk15_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(53,plain,(epred2_0|fellow(esk15_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(54,plain,(epred2_0|young(esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(55,plain,(epred2_0|man(esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(56,plain,(epred2_0|fellow(esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(57,plain,(epred2_0|esk14_0!=esk15_0),inference(split_conjunct,[status(thm)],[46])).
% cnf(58,plain,(epred2_0|front(esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(59,plain,(epred2_0|furniture(esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(60,plain,(epred2_0|seat(esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(61,plain,(epred2_0|in(esk11_0,esk10_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(62,plain,(epred2_0|down(esk11_0,esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(63,plain,(epred2_0|barrel(esk11_0,esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(64,plain,(epred2_0|lonely(esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(65,plain,(epred2_0|way(esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(66,plain,(epred2_0|street(esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(67,plain,(epred2_0|old(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(68,plain,(epred2_0|dirty(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(69,plain,(epred2_0|white(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(70,plain,(epred2_0|car(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(71,plain,(epred2_0|chevy(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(72,plain,(epred2_0|event(esk11_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(73,plain,(epred2_0|city(esk10_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(74,plain,(epred2_0|hollywood(esk10_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(75,plain,(epred2_0|X5=X3|~in(X1,X2)|X3!=X1|~in(X4,X2)|X5!=X4|~young(X3)|~man(X3)|~fellow(X3)|~young(X5)|~man(X5)|~fellow(X5)|~front(X2)|~furniture(X2)|~seat(X2)|~in(X6,X7)|~down(X6,X8)|~barrel(X6,X9)|~old(X9)|~dirty(X9)|~white(X9)|~car(X9)|~chevy(X9)|~lonely(X8)|~way(X8)|~street(X8)|~event(X6)|~city(X7)|~hollywood(X7)),inference(split_conjunct,[status(thm)],[46])).
% cnf(76,plain,(X1=X2|epred1_0|X3!=X1|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X4)|~furniture(X4)|~seat(X4)|~in(X5,X6)|~in(X2,X4)|~in(X3,X4)|~down(X5,X7)|~barrel(X5,X8)|~old(X8)|~dirty(X8)|~white(X8)|~car(X8)|~chevy(X8)|~lonely(X7)|~way(X7)|~street(X7)|~event(X5)|~city(X6)|~hollywood(X6)),inference(er,[status(thm)],[41,theory(equality)])).
% cnf(77,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X4,X5)|~in(X2,X3)|~in(X1,X3)|~down(X4,X6)|~barrel(X4,X7)|~old(X7)|~dirty(X7)|~white(X7)|~car(X7)|~chevy(X7)|~lonely(X6)|~way(X6)|~street(X6)|~event(X4)|~city(X5)|~hollywood(X5)),inference(er,[status(thm)],[76,theory(equality)])).
% cnf(78,plain,(X1=X2|epred2_0|X3!=X1|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X4)|~furniture(X4)|~seat(X4)|~in(X5,X6)|~in(X2,X4)|~in(X3,X4)|~down(X5,X7)|~barrel(X5,X8)|~old(X8)|~dirty(X8)|~white(X8)|~car(X8)|~chevy(X8)|~lonely(X7)|~way(X7)|~street(X7)|~event(X5)|~city(X6)|~hollywood(X6)),inference(er,[status(thm)],[75,theory(equality)])).
% cnf(79,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X4,X5)|~in(X2,X3)|~in(X1,X3)|~down(X4,X6)|~barrel(X4,X7)|~old(X7)|~dirty(X7)|~white(X7)|~car(X7)|~chevy(X7)|~lonely(X6)|~way(X6)|~street(X6)|~event(X4)|~city(X5)|~hollywood(X5)),inference(er,[status(thm)],[78,theory(equality)])).
% cnf(80,negated_conjecture,(esk17_0=esk14_0|~epred1_0),inference(spm,[status(thm)],[7,50,theory(equality)])).
% cnf(81,negated_conjecture,(esk18_0=esk15_0|~epred1_0),inference(spm,[status(thm)],[7,48,theory(equality)])).
% cnf(82,negated_conjecture,(~epred1_0|esk15_0!=esk14_0),inference(spm,[status(thm)],[7,57,theory(equality)])).
% cnf(88,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk2_0,X4)|~barrel(esk2_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk2_0)|~city(esk1_0)|~hollywood(esk1_0)),inference(spm,[status(thm)],[77,27,theory(equality)])).
% cnf(91,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk11_0,X4)|~barrel(esk11_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk11_0)|~city(esk10_0)|~hollywood(esk10_0)),inference(spm,[status(thm)],[79,61,theory(equality)])).
% cnf(95,plain,(esk17_0=esk14_0|esk8_0=esk5_0),inference(spm,[status(thm)],[80,16,theory(equality)])).
% cnf(96,plain,(esk17_0=esk14_0|esk9_0=esk6_0),inference(spm,[status(thm)],[80,14,theory(equality)])).
% cnf(97,plain,(esk17_0=esk14_0|esk6_0!=esk5_0),inference(spm,[status(thm)],[80,23,theory(equality)])).
% cnf(98,plain,(esk18_0=esk15_0|esk8_0=esk5_0),inference(spm,[status(thm)],[81,16,theory(equality)])).
% cnf(99,plain,(esk18_0=esk15_0|esk9_0=esk6_0),inference(spm,[status(thm)],[81,14,theory(equality)])).
% cnf(100,plain,(esk18_0=esk15_0|esk6_0!=esk5_0),inference(spm,[status(thm)],[81,23,theory(equality)])).
% cnf(102,plain,(epred2_0|in(esk14_0,esk16_0)|esk9_0=esk6_0),inference(spm,[status(thm)],[49,96,theory(equality)])).
% cnf(103,plain,(esk8_0=esk5_0|esk15_0!=esk14_0),inference(spm,[status(thm)],[82,16,theory(equality)])).
% cnf(104,plain,(esk9_0=esk6_0|esk15_0!=esk14_0),inference(spm,[status(thm)],[82,14,theory(equality)])).
% cnf(105,plain,(esk15_0!=esk14_0|esk6_0!=esk5_0),inference(spm,[status(thm)],[82,23,theory(equality)])).
% cnf(112,plain,(epred1_0|in(esk5_0,esk7_0)|esk15_0!=esk14_0),inference(spm,[status(thm)],[15,103,theory(equality)])).
% cnf(130,plain,(in(esk5_0,esk7_0)|esk15_0!=esk14_0),inference(csr,[status(thm)],[112,82])).
% cnf(276,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk2_0,X4)|~barrel(esk2_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk2_0)|~city(esk1_0)),inference(csr,[status(thm)],[88,40])).
% cnf(277,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk2_0,X4)|~barrel(esk2_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk2_0)),inference(csr,[status(thm)],[276,39])).
% cnf(278,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk2_0,X4)|~barrel(esk2_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)),inference(csr,[status(thm)],[277,38])).
% cnf(279,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk2_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk3_0)|~way(esk3_0)|~street(esk3_0)),inference(spm,[status(thm)],[278,28,theory(equality)])).
% cnf(413,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk2_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk3_0)|~way(esk3_0)),inference(csr,[status(thm)],[279,37])).
% cnf(414,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk2_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk3_0)),inference(csr,[status(thm)],[413,36])).
% cnf(415,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk2_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)),inference(csr,[status(thm)],[414,35])).
% cnf(416,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk4_0)|~dirty(esk4_0)|~white(esk4_0)|~car(esk4_0)|~chevy(esk4_0)),inference(spm,[status(thm)],[415,29,theory(equality)])).
% cnf(417,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk4_0)|~dirty(esk4_0)|~white(esk4_0)|~car(esk4_0)),inference(csr,[status(thm)],[416,34])).
% cnf(418,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk4_0)|~dirty(esk4_0)|~white(esk4_0)),inference(csr,[status(thm)],[417,33])).
% cnf(419,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk4_0)|~dirty(esk4_0)),inference(csr,[status(thm)],[418,32])).
% cnf(420,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk4_0)),inference(csr,[status(thm)],[419,31])).
% cnf(421,plain,(X1=X2|epred1_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)),inference(csr,[status(thm)],[420,30])).
% cnf(429,plain,(X1=esk9_0|epred1_0|~young(esk9_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~front(esk7_0)|~furniture(esk7_0)|~seat(esk7_0)|~in(X1,esk7_0)),inference(spm,[status(thm)],[421,13,theory(equality)])).
% cnf(430,plain,(X1=esk8_0|epred1_0|~young(esk8_0)|~young(X1)|~man(esk8_0)|~man(X1)|~fellow(esk8_0)|~fellow(X1)|~front(esk7_0)|~furniture(esk7_0)|~seat(esk7_0)|~in(X1,esk7_0)),inference(spm,[status(thm)],[421,15,theory(equality)])).
% cnf(436,plain,(X1=esk9_0|epred1_0|~young(esk9_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~front(esk7_0)|~furniture(esk7_0)|~in(X1,esk7_0)),inference(csr,[status(thm)],[429,26])).
% cnf(437,plain,(X1=esk9_0|epred1_0|~young(esk9_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~front(esk7_0)|~in(X1,esk7_0)),inference(csr,[status(thm)],[436,25])).
% cnf(438,plain,(X1=esk9_0|epred1_0|~young(esk9_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[437,24])).
% cnf(439,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(esk6_0)|~man(X1)|~fellow(esk6_0)|~fellow(X1)|~in(X1,esk7_0)|esk15_0!=esk14_0),inference(spm,[status(thm)],[438,104,theory(equality)])).
% cnf(442,plain,(X1=esk6_0|epred1_0|esk15_0!=esk14_0|~young(esk6_0)|~young(X1)|~man(esk6_0)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[439,19])).
% cnf(443,plain,(X1=esk6_0|epred1_0|esk15_0!=esk14_0|~young(esk6_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[442,18])).
% cnf(444,plain,(X1=esk6_0|epred1_0|esk15_0!=esk14_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[443,17])).
% cnf(445,plain,(X1=esk6_0|esk15_0!=esk14_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[444,82])).
% cnf(448,plain,(esk5_0=esk6_0|epred1_0|esk15_0!=esk14_0|~man(esk5_0)|~fellow(esk5_0)|~in(esk5_0,esk7_0)),inference(spm,[status(thm)],[445,20,theory(equality)])).
% cnf(457,plain,(esk6_0=esk5_0|epred1_0|esk15_0!=esk14_0|~man(esk5_0)|~fellow(esk5_0)),inference(csr,[status(thm)],[448,130])).
% cnf(458,plain,(esk6_0=esk5_0|epred1_0|esk15_0!=esk14_0|~man(esk5_0)),inference(csr,[status(thm)],[457,22])).
% cnf(459,plain,(esk6_0=esk5_0|epred1_0|esk15_0!=esk14_0),inference(csr,[status(thm)],[458,21])).
% cnf(460,plain,(esk6_0=esk5_0|esk15_0!=esk14_0),inference(csr,[status(thm)],[459,82])).
% cnf(461,plain,(esk15_0!=esk14_0),inference(csr,[status(thm)],[460,105])).
% cnf(462,plain,(X1=esk8_0|epred1_0|~young(esk8_0)|~young(X1)|~man(esk8_0)|~man(X1)|~fellow(esk8_0)|~fellow(X1)|~front(esk7_0)|~furniture(esk7_0)|~in(X1,esk7_0)),inference(csr,[status(thm)],[430,26])).
% cnf(463,plain,(X1=esk8_0|epred1_0|~young(esk8_0)|~young(X1)|~man(esk8_0)|~man(X1)|~fellow(esk8_0)|~fellow(X1)|~front(esk7_0)|~in(X1,esk7_0)),inference(csr,[status(thm)],[462,25])).
% cnf(464,plain,(X1=esk8_0|epred1_0|~young(esk8_0)|~young(X1)|~man(esk8_0)|~man(X1)|~fellow(esk8_0)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[463,24])).
% cnf(465,plain,(X1=esk5_0|epred1_0|esk17_0=esk14_0|~young(esk5_0)|~young(X1)|~man(esk5_0)|~man(X1)|~fellow(esk5_0)|~fellow(X1)|~in(X1,esk7_0)),inference(spm,[status(thm)],[464,95,theory(equality)])).
% cnf(466,plain,(X1=esk5_0|epred1_0|esk18_0=esk15_0|~young(esk5_0)|~young(X1)|~man(esk5_0)|~man(X1)|~fellow(esk5_0)|~fellow(X1)|~in(X1,esk7_0)),inference(spm,[status(thm)],[464,98,theory(equality)])).
% cnf(468,plain,(esk17_0=esk14_0|X1=esk5_0|epred1_0|~young(esk5_0)|~young(X1)|~man(esk5_0)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[465,22])).
% cnf(469,plain,(esk17_0=esk14_0|X1=esk5_0|epred1_0|~young(esk5_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[468,21])).
% cnf(470,plain,(esk17_0=esk14_0|X1=esk5_0|epred1_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[469,20])).
% cnf(471,plain,(esk17_0=esk14_0|X1=esk5_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[470,80])).
% cnf(474,plain,(esk17_0=esk14_0|esk6_0=esk5_0|epred1_0|~man(esk6_0)|~fellow(esk6_0)|~in(esk6_0,esk7_0)),inference(spm,[status(thm)],[471,17,theory(equality)])).
% cnf(483,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk11_0,X4)|~barrel(esk11_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk11_0)|~city(esk10_0)),inference(csr,[status(thm)],[91,74])).
% cnf(484,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk11_0,X4)|~barrel(esk11_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)|~event(esk11_0)),inference(csr,[status(thm)],[483,73])).
% cnf(485,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~down(esk11_0,X4)|~barrel(esk11_0,X5)|~old(X5)|~dirty(X5)|~white(X5)|~car(X5)|~chevy(X5)|~lonely(X4)|~way(X4)|~street(X4)),inference(csr,[status(thm)],[484,72])).
% cnf(486,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk11_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk13_0)|~way(esk13_0)|~street(esk13_0)),inference(spm,[status(thm)],[485,62,theory(equality)])).
% cnf(487,plain,(esk17_0=esk14_0|esk6_0=esk5_0|epred1_0|~man(esk6_0)|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[474,19])).
% cnf(488,plain,(esk17_0=esk14_0|esk6_0=esk5_0|epred1_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[487,18])).
% cnf(489,plain,(esk17_0=esk14_0|esk6_0=esk5_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[488,80])).
% cnf(490,plain,(esk17_0=esk14_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[489,97])).
% cnf(492,plain,(esk18_0=esk15_0|X1=esk5_0|epred1_0|~young(esk5_0)|~young(X1)|~man(esk5_0)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[466,22])).
% cnf(493,plain,(esk18_0=esk15_0|X1=esk5_0|epred1_0|~young(esk5_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[492,21])).
% cnf(494,plain,(esk18_0=esk15_0|X1=esk5_0|epred1_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[493,20])).
% cnf(495,plain,(esk18_0=esk15_0|X1=esk5_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[494,81])).
% cnf(498,plain,(esk18_0=esk15_0|esk6_0=esk5_0|epred1_0|~man(esk6_0)|~fellow(esk6_0)|~in(esk6_0,esk7_0)),inference(spm,[status(thm)],[495,17,theory(equality)])).
% cnf(507,plain,(esk18_0=esk15_0|esk6_0=esk5_0|epred1_0|~man(esk6_0)|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[498,19])).
% cnf(508,plain,(esk18_0=esk15_0|esk6_0=esk5_0|epred1_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[507,18])).
% cnf(509,plain,(esk18_0=esk15_0|esk6_0=esk5_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[508,81])).
% cnf(510,plain,(esk18_0=esk15_0|~in(esk6_0,esk7_0)),inference(csr,[status(thm)],[509,100])).
% cnf(626,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk11_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk13_0)|~way(esk13_0)),inference(csr,[status(thm)],[486,66])).
% cnf(627,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk11_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)|~lonely(esk13_0)),inference(csr,[status(thm)],[626,65])).
% cnf(628,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~barrel(esk11_0,X4)|~old(X4)|~dirty(X4)|~white(X4)|~car(X4)|~chevy(X4)),inference(csr,[status(thm)],[627,64])).
% cnf(629,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk12_0)|~dirty(esk12_0)|~white(esk12_0)|~car(esk12_0)|~chevy(esk12_0)),inference(spm,[status(thm)],[628,63,theory(equality)])).
% cnf(630,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk12_0)|~dirty(esk12_0)|~white(esk12_0)|~car(esk12_0)),inference(csr,[status(thm)],[629,71])).
% cnf(631,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk12_0)|~dirty(esk12_0)|~white(esk12_0)),inference(csr,[status(thm)],[630,70])).
% cnf(632,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk12_0)|~dirty(esk12_0)),inference(csr,[status(thm)],[631,69])).
% cnf(633,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)|~old(esk12_0)),inference(csr,[status(thm)],[632,68])).
% cnf(634,plain,(X1=X2|epred2_0|~young(X2)|~young(X1)|~man(X2)|~man(X1)|~fellow(X2)|~fellow(X1)|~front(X3)|~furniture(X3)|~seat(X3)|~in(X2,X3)|~in(X1,X3)),inference(csr,[status(thm)],[633,67])).
% cnf(635,plain,(X1=esk18_0|epred2_0|~young(esk18_0)|~young(X1)|~man(esk18_0)|~man(X1)|~fellow(esk18_0)|~fellow(X1)|~front(esk16_0)|~furniture(esk16_0)|~seat(esk16_0)|~in(X1,esk16_0)),inference(spm,[status(thm)],[634,47,theory(equality)])).
% cnf(636,plain,(X1=esk17_0|epred2_0|~young(esk17_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~front(esk16_0)|~furniture(esk16_0)|~seat(esk16_0)|~in(X1,esk16_0)),inference(spm,[status(thm)],[634,49,theory(equality)])).
% cnf(649,plain,(X1=esk18_0|epred2_0|~young(esk18_0)|~young(X1)|~man(esk18_0)|~man(X1)|~fellow(esk18_0)|~fellow(X1)|~front(esk16_0)|~furniture(esk16_0)|~in(X1,esk16_0)),inference(csr,[status(thm)],[635,60])).
% cnf(650,plain,(X1=esk18_0|epred2_0|~young(esk18_0)|~young(X1)|~man(esk18_0)|~man(X1)|~fellow(esk18_0)|~fellow(X1)|~front(esk16_0)|~in(X1,esk16_0)),inference(csr,[status(thm)],[649,59])).
% cnf(651,plain,(X1=esk18_0|epred2_0|~young(esk18_0)|~young(X1)|~man(esk18_0)|~man(X1)|~fellow(esk18_0)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[650,58])).
% cnf(652,plain,(X1=esk15_0|epred2_0|esk9_0=esk6_0|~young(esk15_0)|~young(X1)|~man(esk15_0)|~man(X1)|~fellow(esk15_0)|~fellow(X1)|~in(X1,esk16_0)),inference(spm,[status(thm)],[651,99,theory(equality)])).
% cnf(654,plain,(esk9_0=esk6_0|X1=esk15_0|epred2_0|~young(esk15_0)|~young(X1)|~man(esk15_0)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[652,53])).
% cnf(655,plain,(esk9_0=esk6_0|X1=esk15_0|epred2_0|~young(esk15_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[654,52])).
% cnf(656,plain,(esk9_0=esk6_0|X1=esk15_0|epred2_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[655,51])).
% cnf(657,plain,(esk9_0=esk6_0|esk14_0=esk15_0|epred2_0|~man(esk14_0)|~fellow(esk14_0)|~in(esk14_0,esk16_0)),inference(spm,[status(thm)],[656,54,theory(equality)])).
% cnf(660,plain,(esk9_0=esk6_0|epred2_0|~man(esk14_0)|~fellow(esk14_0)|~in(esk14_0,esk16_0)),inference(sr,[status(thm)],[657,461,theory(equality)])).
% cnf(661,plain,(X1=esk17_0|epred2_0|~young(esk17_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~front(esk16_0)|~furniture(esk16_0)|~in(X1,esk16_0)),inference(csr,[status(thm)],[636,60])).
% cnf(662,plain,(X1=esk17_0|epred2_0|~young(esk17_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~front(esk16_0)|~in(X1,esk16_0)),inference(csr,[status(thm)],[661,59])).
% cnf(663,plain,(X1=esk17_0|epred2_0|~young(esk17_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[662,58])).
% cnf(666,plain,(esk9_0=esk6_0|epred2_0|~man(esk14_0)|~fellow(esk14_0)),inference(csr,[status(thm)],[660,102])).
% cnf(667,plain,(esk9_0=esk6_0|epred2_0|~man(esk14_0)),inference(csr,[status(thm)],[666,56])).
% cnf(668,plain,(esk9_0=esk6_0|epred2_0),inference(csr,[status(thm)],[667,55])).
% cnf(669,negated_conjecture,(esk9_0=esk6_0|~epred1_0),inference(spm,[status(thm)],[7,668,theory(equality)])).
% cnf(670,negated_conjecture,(esk9_0=esk6_0),inference(csr,[status(thm)],[669,14])).
% cnf(674,plain,(X1=esk6_0|epred1_0|~young(esk9_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~in(X1,esk7_0)),inference(rw,[status(thm)],[438,670,theory(equality)])).
% cnf(675,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(esk9_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~in(X1,esk7_0)),inference(rw,[status(thm)],[674,670,theory(equality)])).
% cnf(676,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(esk6_0)|~man(X1)|~fellow(esk9_0)|~fellow(X1)|~in(X1,esk7_0)),inference(rw,[status(thm)],[675,670,theory(equality)])).
% cnf(677,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(esk6_0)|~man(X1)|~fellow(esk6_0)|~fellow(X1)|~in(X1,esk7_0)),inference(rw,[status(thm)],[676,670,theory(equality)])).
% cnf(678,plain,(epred1_0|in(esk6_0,esk7_0)),inference(rw,[status(thm)],[13,670,theory(equality)])).
% cnf(682,plain,(esk17_0=esk14_0|epred1_0),inference(spm,[status(thm)],[490,678,theory(equality)])).
% cnf(683,plain,(esk18_0=esk15_0|epred1_0),inference(spm,[status(thm)],[510,678,theory(equality)])).
% cnf(684,plain,(esk17_0=esk14_0),inference(csr,[status(thm)],[682,80])).
% cnf(687,plain,(X1=esk14_0|epred2_0|~young(esk17_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~in(X1,esk16_0)),inference(rw,[status(thm)],[663,684,theory(equality)])).
% cnf(688,plain,(X1=esk14_0|epred2_0|~young(esk14_0)|~young(X1)|~man(esk17_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~in(X1,esk16_0)),inference(rw,[status(thm)],[687,684,theory(equality)])).
% cnf(689,plain,(X1=esk14_0|epred2_0|~young(esk14_0)|~young(X1)|~man(esk14_0)|~man(X1)|~fellow(esk17_0)|~fellow(X1)|~in(X1,esk16_0)),inference(rw,[status(thm)],[688,684,theory(equality)])).
% cnf(690,plain,(X1=esk14_0|epred2_0|~young(esk14_0)|~young(X1)|~man(esk14_0)|~man(X1)|~fellow(esk14_0)|~fellow(X1)|~in(X1,esk16_0)),inference(rw,[status(thm)],[689,684,theory(equality)])).
% cnf(697,plain,(esk18_0=esk15_0),inference(csr,[status(thm)],[683,81])).
% cnf(708,plain,(epred2_0|in(esk15_0,esk16_0)),inference(rw,[status(thm)],[47,697,theory(equality)])).
% cnf(714,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(esk6_0)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[677,19])).
% cnf(715,plain,(X1=esk6_0|epred1_0|~young(esk6_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[714,18])).
% cnf(716,plain,(X1=esk6_0|epred1_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk7_0)),inference(csr,[status(thm)],[715,17])).
% cnf(720,plain,(X1=esk14_0|epred2_0|~young(esk14_0)|~young(X1)|~man(esk14_0)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[690,56])).
% cnf(721,plain,(X1=esk14_0|epred2_0|~young(esk14_0)|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[720,55])).
% cnf(722,plain,(X1=esk14_0|epred2_0|~young(X1)|~man(X1)|~fellow(X1)|~in(X1,esk16_0)),inference(csr,[status(thm)],[721,54])).
% cnf(723,plain,(esk15_0=esk14_0|epred2_0|~man(esk15_0)|~fellow(esk15_0)|~in(esk15_0,esk16_0)),inference(spm,[status(thm)],[722,51,theory(equality)])).
% cnf(726,plain,(epred2_0|~man(esk15_0)|~fellow(esk15_0)|~in(esk15_0,esk16_0)),inference(sr,[status(thm)],[723,461,theory(equality)])).
% cnf(727,plain,(epred2_0|~man(esk15_0)|~fellow(esk15_0)),inference(csr,[status(thm)],[726,708])).
% cnf(728,plain,(epred2_0|~man(esk15_0)),inference(csr,[status(thm)],[727,53])).
% cnf(729,plain,(epred2_0),inference(csr,[status(thm)],[728,52])).
% cnf(758,negated_conjecture,($false|~epred1_0),inference(rw,[status(thm)],[7,729,theory(equality)])).
% cnf(759,negated_conjecture,(~epred1_0),inference(cn,[status(thm)],[758,theory(equality)])).
% cnf(760,plain,(esk6_0!=esk5_0),inference(spm,[status(thm)],[759,23,theory(equality)])).
% cnf(761,plain,(esk8_0=esk5_0),inference(sr,[status(thm)],[16,759,theory(equality)])).
% cnf(776,plain,(fellow(esk5_0)),inference(sr,[status(thm)],[22,759,theory(equality)])).
% cnf(778,plain,(man(esk5_0)),inference(sr,[status(thm)],[21,759,theory(equality)])).
% cnf(780,plain,(young(esk5_0)),inference(sr,[status(thm)],[20,759,theory(equality)])).
% cnf(785,plain,(in(esk8_0,esk7_0)),inference(sr,[status(thm)],[15,759,theory(equality)])).
% cnf(793,plain,(esk5_0=esk6_0|epred1_0|~man(esk5_0)|~fellow(esk5_0)|~in(esk5_0,esk7_0)),inference(spm,[status(thm)],[716,780,theory(equality)])).
% cnf(795,plain,(esk5_0=esk6_0|epred1_0|$false|~fellow(esk5_0)|~in(esk5_0,esk7_0)),inference(rw,[status(thm)],[793,778,theory(equality)])).
% cnf(796,plain,(esk5_0=esk6_0|epred1_0|$false|$false|~in(esk5_0,esk7_0)),inference(rw,[status(thm)],[795,776,theory(equality)])).
% cnf(797,plain,(esk5_0=esk6_0|epred1_0|~in(esk5_0,esk7_0)),inference(cn,[status(thm)],[796,theory(equality)])).
% cnf(798,plain,(epred1_0|~in(esk5_0,esk7_0)),inference(sr,[status(thm)],[797,760,theory(equality)])).
% cnf(799,plain,(~in(esk5_0,esk7_0)),inference(sr,[status(thm)],[798,759,theory(equality)])).
% cnf(806,plain,(in(esk5_0,esk7_0)),inference(rw,[status(thm)],[785,761,theory(equality)])).
% cnf(825,plain,($false),inference(rw,[status(thm)],[799,806,theory(equality)])).
% cnf(826,plain,($false),inference(cn,[status(thm)],[825,theory(equality)])).
% cnf(827,plain,($false),826,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 256
% # ...of these trivial : 1
% # ...subsumed : 40
% # ...remaining for further processing: 215
% # Other redundant clauses eliminated : 4
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 33
% # Backward-rewritten : 54
% # Generated clauses : 187
% # ...of the previous two non-trivial : 195
% # Contextual simplify-reflections : 462
% # Paramodulations : 159
% # Factorizations : 0
% # Equation resolutions : 4
% # Current number of processed clauses: 40
% # Positive orientable unit clauses: 30
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 7
% # Current number of unprocessed clauses: 5
% # ...number of literals in the above : 31
% # Clause-clause subsumption calls (NU) : 7652
% # Rec. Clause-clause subsumption calls : 1139
% # Unit Clause-clause subsumption calls : 62
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 7
% # Indexed BW rewrite successes : 7
% # Backwards rewriting index: 56 leaves, 1.07+/-0.258 terms/leaf
% # Paramod-from index: 31 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 42 leaves, 1.00+/-0.000 terms/leaf
% # -------------------------------------------------
% # User time : 0.058 s
% # System time : 0.003 s
% # Total time : 0.061 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.26 WC
% FINAL PrfWatch: 0.16 CPU 0.26 WC
% SZS output end Solution for /tmp/SystemOnTPTP7088/NLP009+1.tptp
%
%------------------------------------------------------------------------------