%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NLP208+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 : art07.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 17:11:40 EST 2010
% Result : Theorem 1.08s
% Output : Solution 1.08s
% 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/SystemOnTPTP3349/NLP208+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3349/NLP208+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3349/NLP208+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 3445
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(17, axiom,![X1]:![X2]:![X3]:![X4]:(be(X1,X2,X3,X4)=>X3=X4),file('/tmp/SRASS.s.p', ax71)).
% fof(24, axiom,![X1]:![X2]:(man(X1,X2)=>male(X1,X2)),file('/tmp/SRASS.s.p', ax24)).
% fof(28, axiom,![X1]:![X2]:(wheel(X1,X2)=>device(X1,X2)),file('/tmp/SRASS.s.p', ax48)).
% fof(40, axiom,![X1]:![X2]:(device(X1,X2)=>instrumentality(X1,X2)),file('/tmp/SRASS.s.p', ax47)).
% fof(43, axiom,![X1]:![X2]:(unisex(X1,X2)=>~(male(X1,X2))),file('/tmp/SRASS.s.p', ax63)).
% fof(55, axiom,![X1]:![X2]:(object(X1,X2)=>unisex(X1,X2)),file('/tmp/SRASS.s.p', ax38)).
% fof(56, axiom,![X1]:![X2]:(artifact(X1,X2)=>object(X1,X2)),file('/tmp/SRASS.s.p', ax45)).
% fof(57, axiom,![X1]:![X2]:(instrumentality(X1,X2)=>artifact(X1,X2)),file('/tmp/SRASS.s.p', ax46)).
% fof(72, conjecture,~(?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X6))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&of(X1,X5,X6))&city(X1,X6))&hollywood_placename(X1,X5))&placename(X1,X5))&street(X1,X6))&lonely(X1,X6))&event(X1,X7))&agent(X1,X7,X4))&present(X1,X7))&barrel(X1,X7))&down(X1,X7,X6))&in(X1,X7,X6))&![X12]:(member(X1,X12,X8)=>?[X13]:?[X14]:((state(X1,X13)&be(X1,X13,X12,X14))&in(X1,X14,X6))))&two(X1,X8))&group(X1,X8))&![X15]:(member(X1,X15,X8)=>(fellow(X1,X15)&young(X1,X15))))&![X16]:(member(X1,X16,X9)=>![X17]:(member(X1,X17,X8)=>?[X18]:(((((event(X1,X18)&agent(X1,X18,X17))&patient(X1,X18,X16))&present(X1,X18))&nonreflexive(X1,X18))&wear(X1,X18)))))&group(X1,X9))&![X19]:(member(X1,X19,X9)=>((coat(X1,X19)&black(X1,X19))&cheap(X1,X19))))&wheel(X1,X11))&state(X1,X10))&be(X1,X10,X2,X11))&behind(X1,X11,X11)))),file('/tmp/SRASS.s.p', co1)).
% fof(73, negated_conjecture,~(~(?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X6))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&of(X1,X5,X6))&city(X1,X6))&hollywood_placename(X1,X5))&placename(X1,X5))&street(X1,X6))&lonely(X1,X6))&event(X1,X7))&agent(X1,X7,X4))&present(X1,X7))&barrel(X1,X7))&down(X1,X7,X6))&in(X1,X7,X6))&![X12]:(member(X1,X12,X8)=>?[X13]:?[X14]:((state(X1,X13)&be(X1,X13,X12,X14))&in(X1,X14,X6))))&two(X1,X8))&group(X1,X8))&![X15]:(member(X1,X15,X8)=>(fellow(X1,X15)&young(X1,X15))))&![X16]:(member(X1,X16,X9)=>![X17]:(member(X1,X17,X8)=>?[X18]:(((((event(X1,X18)&agent(X1,X18,X17))&patient(X1,X18,X16))&present(X1,X18))&nonreflexive(X1,X18))&wear(X1,X18)))))&group(X1,X9))&![X19]:(member(X1,X19,X9)=>((coat(X1,X19)&black(X1,X19))&cheap(X1,X19))))&wheel(X1,X11))&state(X1,X10))&be(X1,X10,X2,X11))&behind(X1,X11,X11))))),inference(assume_negation,[status(cth)],[72])).
% fof(76, plain,![X1]:![X2]:(unisex(X1,X2)=>~(male(X1,X2))),inference(fof_simplification,[status(thm)],[43,theory(equality)])).
% fof(142, plain,![X1]:![X2]:![X3]:![X4]:(~(be(X1,X2,X3,X4))|X3=X4),inference(fof_nnf,[status(thm)],[17])).
% fof(143, plain,![X5]:![X6]:![X7]:![X8]:(~(be(X5,X6,X7,X8))|X7=X8),inference(variable_rename,[status(thm)],[142])).
% cnf(144,plain,(X1=X2|~be(X3,X4,X1,X2)),inference(split_conjunct,[status(thm)],[143])).
% fof(163, plain,![X1]:![X2]:(~(man(X1,X2))|male(X1,X2)),inference(fof_nnf,[status(thm)],[24])).
% fof(164, plain,![X3]:![X4]:(~(man(X3,X4))|male(X3,X4)),inference(variable_rename,[status(thm)],[163])).
% cnf(165,plain,(male(X1,X2)|~man(X1,X2)),inference(split_conjunct,[status(thm)],[164])).
% fof(175, plain,![X1]:![X2]:(~(wheel(X1,X2))|device(X1,X2)),inference(fof_nnf,[status(thm)],[28])).
% fof(176, plain,![X3]:![X4]:(~(wheel(X3,X4))|device(X3,X4)),inference(variable_rename,[status(thm)],[175])).
% cnf(177,plain,(device(X1,X2)|~wheel(X1,X2)),inference(split_conjunct,[status(thm)],[176])).
% fof(211, plain,![X1]:![X2]:(~(device(X1,X2))|instrumentality(X1,X2)),inference(fof_nnf,[status(thm)],[40])).
% fof(212, plain,![X3]:![X4]:(~(device(X3,X4))|instrumentality(X3,X4)),inference(variable_rename,[status(thm)],[211])).
% cnf(213,plain,(instrumentality(X1,X2)|~device(X1,X2)),inference(split_conjunct,[status(thm)],[212])).
% fof(220, plain,![X1]:![X2]:(~(unisex(X1,X2))|~(male(X1,X2))),inference(fof_nnf,[status(thm)],[76])).
% fof(221, plain,![X3]:![X4]:(~(unisex(X3,X4))|~(male(X3,X4))),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(~male(X1,X2)|~unisex(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% fof(256, plain,![X1]:![X2]:(~(object(X1,X2))|unisex(X1,X2)),inference(fof_nnf,[status(thm)],[55])).
% fof(257, plain,![X3]:![X4]:(~(object(X3,X4))|unisex(X3,X4)),inference(variable_rename,[status(thm)],[256])).
% cnf(258,plain,(unisex(X1,X2)|~object(X1,X2)),inference(split_conjunct,[status(thm)],[257])).
% fof(259, plain,![X1]:![X2]:(~(artifact(X1,X2))|object(X1,X2)),inference(fof_nnf,[status(thm)],[56])).
% fof(260, plain,![X3]:![X4]:(~(artifact(X3,X4))|object(X3,X4)),inference(variable_rename,[status(thm)],[259])).
% cnf(261,plain,(object(X1,X2)|~artifact(X1,X2)),inference(split_conjunct,[status(thm)],[260])).
% fof(262, plain,![X1]:![X2]:(~(instrumentality(X1,X2))|artifact(X1,X2)),inference(fof_nnf,[status(thm)],[57])).
% fof(263, plain,![X3]:![X4]:(~(instrumentality(X3,X4))|artifact(X3,X4)),inference(variable_rename,[status(thm)],[262])).
% cnf(264,plain,(artifact(X1,X2)|~instrumentality(X1,X2)),inference(split_conjunct,[status(thm)],[263])).
% fof(307, negated_conjecture,?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X6))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&of(X1,X5,X6))&city(X1,X6))&hollywood_placename(X1,X5))&placename(X1,X5))&street(X1,X6))&lonely(X1,X6))&event(X1,X7))&agent(X1,X7,X4))&present(X1,X7))&barrel(X1,X7))&down(X1,X7,X6))&in(X1,X7,X6))&![X12]:(~(member(X1,X12,X8))|?[X13]:?[X14]:((state(X1,X13)&be(X1,X13,X12,X14))&in(X1,X14,X6))))&two(X1,X8))&group(X1,X8))&![X15]:(~(member(X1,X15,X8))|(fellow(X1,X15)&young(X1,X15))))&![X16]:(~(member(X1,X16,X9))|![X17]:(~(member(X1,X17,X8))|?[X18]:(((((event(X1,X18)&agent(X1,X18,X17))&patient(X1,X18,X16))&present(X1,X18))&nonreflexive(X1,X18))&wear(X1,X18)))))&group(X1,X9))&![X19]:(~(member(X1,X19,X9))|((coat(X1,X19)&black(X1,X19))&cheap(X1,X19))))&wheel(X1,X11))&state(X1,X10))&be(X1,X10,X2,X11))&behind(X1,X11,X11))),inference(fof_nnf,[status(thm)],[73])).
% fof(308, negated_conjecture,?[X20]:(actual_world(X20)&?[X21]:?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:?[X28]:?[X29]:?[X30]:(((((((((((((((((((((((((((((((of(X20,X22,X21)&man(X20,X21))&jules_forename(X20,X22))&forename(X20,X22))&frontseat(X20,X25))&chevy(X20,X23))&white(X20,X23))&dirty(X20,X23))&old(X20,X23))&of(X20,X24,X25))&city(X20,X25))&hollywood_placename(X20,X24))&placename(X20,X24))&street(X20,X25))&lonely(X20,X25))&event(X20,X26))&agent(X20,X26,X23))&present(X20,X26))&barrel(X20,X26))&down(X20,X26,X25))&in(X20,X26,X25))&![X31]:(~(member(X20,X31,X27))|?[X32]:?[X33]:((state(X20,X32)&be(X20,X32,X31,X33))&in(X20,X33,X25))))&two(X20,X27))&group(X20,X27))&![X34]:(~(member(X20,X34,X27))|(fellow(X20,X34)&young(X20,X34))))&![X35]:(~(member(X20,X35,X28))|![X36]:(~(member(X20,X36,X27))|?[X37]:(((((event(X20,X37)&agent(X20,X37,X36))&patient(X20,X37,X35))&present(X20,X37))&nonreflexive(X20,X37))&wear(X20,X37)))))&group(X20,X28))&![X38]:(~(member(X20,X38,X28))|((coat(X20,X38)&black(X20,X38))&cheap(X20,X38))))&wheel(X20,X30))&state(X20,X29))&be(X20,X29,X21,X30))&behind(X20,X30,X30))),inference(variable_rename,[status(thm)],[307])).
% fof(309, negated_conjecture,(actual_world(esk4_0)&(((((((((((((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk9_0))&chevy(esk4_0,esk7_0))&white(esk4_0,esk7_0))&dirty(esk4_0,esk7_0))&old(esk4_0,esk7_0))&of(esk4_0,esk8_0,esk9_0))&city(esk4_0,esk9_0))&hollywood_placename(esk4_0,esk8_0))&placename(esk4_0,esk8_0))&street(esk4_0,esk9_0))&lonely(esk4_0,esk9_0))&event(esk4_0,esk10_0))&agent(esk4_0,esk10_0,esk7_0))&present(esk4_0,esk10_0))&barrel(esk4_0,esk10_0))&down(esk4_0,esk10_0,esk9_0))&in(esk4_0,esk10_0,esk9_0))&![X31]:(~(member(esk4_0,X31,esk11_0))|((state(esk4_0,esk15_1(X31))&be(esk4_0,esk15_1(X31),X31,esk16_1(X31)))&in(esk4_0,esk16_1(X31),esk9_0))))&two(esk4_0,esk11_0))&group(esk4_0,esk11_0))&![X34]:(~(member(esk4_0,X34,esk11_0))|(fellow(esk4_0,X34)&young(esk4_0,X34))))&![X35]:(~(member(esk4_0,X35,esk12_0))|![X36]:(~(member(esk4_0,X36,esk11_0))|(((((event(esk4_0,esk17_2(X35,X36))&agent(esk4_0,esk17_2(X35,X36),X36))&patient(esk4_0,esk17_2(X35,X36),X35))&present(esk4_0,esk17_2(X35,X36)))&nonreflexive(esk4_0,esk17_2(X35,X36)))&wear(esk4_0,esk17_2(X35,X36))))))&group(esk4_0,esk12_0))&![X38]:(~(member(esk4_0,X38,esk12_0))|((coat(esk4_0,X38)&black(esk4_0,X38))&cheap(esk4_0,X38))))&wheel(esk4_0,esk14_0))&state(esk4_0,esk13_0))&be(esk4_0,esk13_0,esk5_0,esk14_0))&behind(esk4_0,esk14_0,esk14_0))),inference(skolemize,[status(esa)],[308])).
% fof(310, negated_conjecture,![X31]:![X34]:![X35]:![X36]:![X38]:(((((((~(member(esk4_0,X38,esk12_0))|((coat(esk4_0,X38)&black(esk4_0,X38))&cheap(esk4_0,X38)))&((((~(member(esk4_0,X36,esk11_0))|(((((event(esk4_0,esk17_2(X35,X36))&agent(esk4_0,esk17_2(X35,X36),X36))&patient(esk4_0,esk17_2(X35,X36),X35))&present(esk4_0,esk17_2(X35,X36)))&nonreflexive(esk4_0,esk17_2(X35,X36)))&wear(esk4_0,esk17_2(X35,X36))))|~(member(esk4_0,X35,esk12_0)))&((~(member(esk4_0,X34,esk11_0))|(fellow(esk4_0,X34)&young(esk4_0,X34)))&((((~(member(esk4_0,X31,esk11_0))|((state(esk4_0,esk15_1(X31))&be(esk4_0,esk15_1(X31),X31,esk16_1(X31)))&in(esk4_0,esk16_1(X31),esk9_0)))&((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk9_0))&chevy(esk4_0,esk7_0))&white(esk4_0,esk7_0))&dirty(esk4_0,esk7_0))&old(esk4_0,esk7_0))&of(esk4_0,esk8_0,esk9_0))&city(esk4_0,esk9_0))&hollywood_placename(esk4_0,esk8_0))&placename(esk4_0,esk8_0))&street(esk4_0,esk9_0))&lonely(esk4_0,esk9_0))&event(esk4_0,esk10_0))&agent(esk4_0,esk10_0,esk7_0))&present(esk4_0,esk10_0))&barrel(esk4_0,esk10_0))&down(esk4_0,esk10_0,esk9_0))&in(esk4_0,esk10_0,esk9_0)))&two(esk4_0,esk11_0))&group(esk4_0,esk11_0))))&group(esk4_0,esk12_0)))&wheel(esk4_0,esk14_0))&state(esk4_0,esk13_0))&be(esk4_0,esk13_0,esk5_0,esk14_0))&behind(esk4_0,esk14_0,esk14_0))&actual_world(esk4_0)),inference(shift_quantors,[status(thm)],[309])).
% fof(311, negated_conjecture,![X31]:![X34]:![X35]:![X36]:![X38]:(((((((((coat(esk4_0,X38)|~(member(esk4_0,X38,esk12_0)))&(black(esk4_0,X38)|~(member(esk4_0,X38,esk12_0))))&(cheap(esk4_0,X38)|~(member(esk4_0,X38,esk12_0))))&(((((((((event(esk4_0,esk17_2(X35,X36))|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0)))&((agent(esk4_0,esk17_2(X35,X36),X36)|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0))))&((patient(esk4_0,esk17_2(X35,X36),X35)|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0))))&((present(esk4_0,esk17_2(X35,X36))|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0))))&((nonreflexive(esk4_0,esk17_2(X35,X36))|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0))))&((wear(esk4_0,esk17_2(X35,X36))|~(member(esk4_0,X36,esk11_0)))|~(member(esk4_0,X35,esk12_0))))&(((fellow(esk4_0,X34)|~(member(esk4_0,X34,esk11_0)))&(young(esk4_0,X34)|~(member(esk4_0,X34,esk11_0))))&((((((state(esk4_0,esk15_1(X31))|~(member(esk4_0,X31,esk11_0)))&(be(esk4_0,esk15_1(X31),X31,esk16_1(X31))|~(member(esk4_0,X31,esk11_0))))&(in(esk4_0,esk16_1(X31),esk9_0)|~(member(esk4_0,X31,esk11_0))))&((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk9_0))&chevy(esk4_0,esk7_0))&white(esk4_0,esk7_0))&dirty(esk4_0,esk7_0))&old(esk4_0,esk7_0))&of(esk4_0,esk8_0,esk9_0))&city(esk4_0,esk9_0))&hollywood_placename(esk4_0,esk8_0))&placename(esk4_0,esk8_0))&street(esk4_0,esk9_0))&lonely(esk4_0,esk9_0))&event(esk4_0,esk10_0))&agent(esk4_0,esk10_0,esk7_0))&present(esk4_0,esk10_0))&barrel(esk4_0,esk10_0))&down(esk4_0,esk10_0,esk9_0))&in(esk4_0,esk10_0,esk9_0)))&two(esk4_0,esk11_0))&group(esk4_0,esk11_0))))&group(esk4_0,esk12_0)))&wheel(esk4_0,esk14_0))&state(esk4_0,esk13_0))&be(esk4_0,esk13_0,esk5_0,esk14_0))&behind(esk4_0,esk14_0,esk14_0))&actual_world(esk4_0)),inference(distribute,[status(thm)],[310])).
% cnf(314,negated_conjecture,(be(esk4_0,esk13_0,esk5_0,esk14_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(316,negated_conjecture,(wheel(esk4_0,esk14_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(339,negated_conjecture,(man(esk4_0,esk5_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(362,negated_conjecture,(esk5_0=esk14_0),inference(spm,[status(thm)],[144,314,theory(equality)])).
% cnf(370,plain,(~unisex(X1,X2)|~man(X1,X2)),inference(spm,[status(thm)],[222,165,theory(equality)])).
% cnf(376,plain,(instrumentality(X1,X2)|~wheel(X1,X2)),inference(spm,[status(thm)],[213,177,theory(equality)])).
% cnf(398,negated_conjecture,(man(esk4_0,esk14_0)),inference(rw,[status(thm)],[339,362,theory(equality)])).
% cnf(409,plain,(~man(X1,X2)|~object(X1,X2)),inference(spm,[status(thm)],[370,258,theory(equality)])).
% cnf(415,negated_conjecture,(~object(esk4_0,esk14_0)),inference(spm,[status(thm)],[409,398,theory(equality)])).
% cnf(434,negated_conjecture,(instrumentality(esk4_0,esk14_0)),inference(spm,[status(thm)],[376,316,theory(equality)])).
% cnf(435,negated_conjecture,(artifact(esk4_0,esk14_0)),inference(spm,[status(thm)],[264,434,theory(equality)])).
% cnf(437,negated_conjecture,(object(esk4_0,esk14_0)),inference(spm,[status(thm)],[261,435,theory(equality)])).
% cnf(438,negated_conjecture,($false),inference(sr,[status(thm)],[437,415,theory(equality)])).
% cnf(439,negated_conjecture,($false),438,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 163
% # ...of these trivial : 0
% # ...subsumed : 2
% # ...remaining for further processing: 161
% # Other redundant clauses eliminated : 1
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 3
% # Generated clauses : 70
% # ...of the previous two non-trivial : 67
% # Contextual simplify-reflections : 0
% # Paramodulations : 69
% # Factorizations : 0
% # Equation resolutions : 1
% # Current number of processed clauses: 157
% # Positive orientable unit clauses: 38
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 8
% # Non-unit-clauses : 111
% # Current number of unprocessed clauses: 22
% # ...number of literals in the above : 57
% # Clause-clause subsumption calls (NU) : 2719
% # Rec. Clause-clause subsumption calls : 2628
% # Unit Clause-clause subsumption calls : 79
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 152 leaves, 1.09+/-0.396 terms/leaf
% # Paramod-from index: 91 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 138 leaves, 1.01+/-0.120 terms/leaf
% # -------------------------------------------------
% # User time : 0.028 s
% # System time : 0.001 s
% # Total time : 0.029 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.11 CPU 0.20 WC
% FINAL PrfWatch: 0.11 CPU 0.20 WC
% SZS output end Solution for /tmp/SystemOnTPTP3349/NLP208+1.tptp
%
%------------------------------------------------------------------------------